My project is all SPARK. It’s been proving and running fine, until recently when I nested a couple records. It now proves fine, but it produces Invalid_Data when run:
PS D:\dev\ada\anteforth> alr run
Note: Building anteforth=0.1.0-dev/anteforth.gpr...
Compile
[Ada] anteforth.adb
[Ada] machines.adb
[Ada] machines-builtins.adb
Bind
[gprbind] anteforth.bexch
[Ada] anteforth.ali
Link
[link] anteforth.adb
Success: Build finished successfully in 1.82 seconds.
raised CONSTRAINT_ERROR : scanners.ads:149 invalid data
[D:\dev\ada\anteforth\bin\anteforth.exe]
0x7ff62eb67ceb Anteforth at scanners.ads:149
0x7ff62eb6946b _ada_anteforth at ???
0x7ff62eb659b2 _ada_anteforth at ???
0x7ff62eb664b9 Anteforth at machines.ads:84
0x7ff62eb6084c Anteforth at anteforth.adb:8
0x7ff62eb66ff0 Anteforth at b__anteforth.adb:255
0x7ff62eb2133e __tmainCRTStartup at ???
0x7ff62eb21144 mainCRTStartup at ???
[C:\WINDOWS\System32\KERNEL32.DLL]
0x7ff87318e8d5
[C:\WINDOWS\SYSTEM32\ntdll.dll]
0x7ff87466c53a
This is the proof:
=========================
Summary of SPARK analysis
=========================
------------------------------------------------------------------------------------------------------------
SPARK Analysis results Total Flow Provers Justified Unproved
------------------------------------------------------------------------------------------------------------
Data Dependencies 22 22 . . .
Flow Dependencies 2 2 . . .
Initialization 21 21 . . .
Non-Aliasing . . . . .
Run-time Checks 263 . 263 (CVC5 95%, Trivial 5%) . .
Assertions 24 . 24 (CVC5 98%, Trivial 2%) . .
Functional Contracts 136 . 136 (CVC5 86%, Trivial 14%, Z3 1%) . .
LSP Verification . . . . .
Termination 48 45 3 (CVC5) . .
Concurrency . . . . .
------------------------------------------------------------------------------------------------------------
Total 516 90 (17%) 426 (83%) . .
max steps used for successful proof: 194
============================
Most difficult proved checks
============================
No check found with max time greater than 1 second
========================
Detailed analysis report
========================
Analyzed 6 units
in unit anteforth, 1 subprograms and packages out of 1 analyzed
Anteforth at anteforth.adb:4 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
in unit foo, 0 subprograms and packages out of 1 analyzed
Foo.Get_Value at foo.ads:5 skipped; SPARK_Mode => Off
in unit machines, 27 subprograms and packages out of 27 analyzed
Machines at machines.ads:5 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Machines.Accept_Input at machines.ads:40 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (2 checks)
Machines.Allocate_Word at machines.ads:196 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (22 checks)
Machines.Can_Allocate_Name at machines.ads:189 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Machines.Can_Allocate_Word at machines.ads:186 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Machines.Contains at machines.ads:193 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Machines.Execute at machines.ads:106 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (14 checks)
Machines.Initialize at machines.ads:35 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (24 checks)
Machines.Is_Running at machines.ads:51 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Machines.Is_Stack_Empty at machines.ads:64 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Machines.Is_Stack_Full at machines.ads:68 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Machines.Is_Stopped at machines.ads:55 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Machines.Is_Word at machines.ads:117 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Machines.Lookup at machines.ads:214 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Machines.Machine at machines.ads:217 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Machines.Op_Procedure at machines.ads:123 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Machines.Peek at machines.ads:72 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Machines.Peek at machines.ads:75 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Machines.Pop at machines.ads:93 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (5 checks)
Machines.Print_Words at machines.ads:132 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (2 checks)
Machines.Push at machines.ads:80 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (13 checks)
Machines.Register at machines.ads:128 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (2 checks)
Machines.Register at machines.ads:140 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (2 checks)
Machines.Stack_Size at machines.ads:61 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Machines.Status at machines.ads:48 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Machines.To_Machine_Op at machines.ads:120 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Machines.Word at machines.ads:168 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
in unit machines-builtins, 12 subprograms and packages out of 12 analyzed
Machines.Builtins at machines-builtins.ads:1 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Machines.Builtins.Op_Add at machines-builtins.ads:5 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (10 checks)
Machines.Builtins.Op_Divide at machines-builtins.ads:41 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (13 checks)
Machines.Builtins.Op_Drop at machines-builtins.ads:117 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (8 checks)
Machines.Builtins.Op_Dupe at machines-builtins.ads:102 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (9 checks)
Machines.Builtins.Op_Multiply at machines-builtins.ads:29 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (10 checks)
Machines.Builtins.Op_Negate at machines-builtins.ads:53 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (7 checks)
Machines.Builtins.Op_Over at machines-builtins.ads:73 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (15 checks)
Machines.Builtins.Op_Print at machines-builtins.ads:127 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (3 checks)
Machines.Builtins.Op_Rotate at machines-builtins.ads:89 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (14 checks)
Machines.Builtins.Op_Subtract at machines-builtins.ads:17 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (11 checks)
Machines.Builtins.Op_Swap at machines-builtins.ads:64 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (10 checks)
in unit scanners, 27 subprograms and packages out of 27 analyzed
Scanners at scanners.ads:4 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (4 checks)
Scanners.Contains at scanners.ads:101 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (2 checks)
Scanners.Contains at scanners.ads:102 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Scanners.Has_Input at scanners.ads:26 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Scanners.Has_Lexeme at scanners.ads:30 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Scanners.Has_More_Characters at scanners.ads:28 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Scanners.Has_Next at scanners.ads:61 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (5 checks)
Scanners.Has_Valid_Cursor at scanners.ads:148 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Scanners.Has_Valid_State at scanners.ads:151 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Scanners.Ignore_Lexeme at scanners.ads:32 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (9 checks)
Scanners.Image at scanners.ads:99 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Scanners.Input_Size at scanners.ads:45 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Scanners.Is_Number at scanners.ads:113 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (14 checks)
Scanners.Is_Valid at scanners.ads:136 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Scanners.Is_Word at scanners.ads:103 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Scanners.Lexeme_Range at scanners.ads:123 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Scanners.Lexeme_Size at scanners.ads:40 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (3 checks)
Scanners.Load_Input at scanners.ads:47 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (20 checks)
Scanners.Next at scanners.ads:70 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (15 checks)
Scanners.Next_Token at scanners.ads:89 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (43 checks)
Scanners.Peek at scanners.ads:68 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (2 checks)
Scanners.Remaining_Characters at scanners.ads:43 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Scanners.Scanner at scanners.ads:138 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Scanners.Skip_Whitespace at scanners.ads:188 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (34 checks)
Scanners.Take_Lexeme at scanners.ads:222 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (21 checks)
Scanners.Tokenize at scanners.ads:105 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (24 checks)
Scanners.Width at scanners.ads:18 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
in unit terminal_input_buffers, 13 subprograms and packages out of 13 analyzed
Terminal_Input_Buffers at terminal_input_buffers.ads:7 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Terminal_Input_Buffers.Advance at terminal_input_buffers.ads:42 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Terminal_Input_Buffers.Buffer at terminal_input_buffers.ads:66 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Terminal_Input_Buffers.Contents at terminal_input_buffers.ads:40 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Terminal_Input_Buffers.Current_Word at terminal_input_buffers.ads:34 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Terminal_Input_Buffers.Find_Word_End at terminal_input_buffers.adb:12 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (6 checks)
Terminal_Input_Buffers.Has_Word at terminal_input_buffers.ads:31 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Terminal_Input_Buffers.Input_Size at terminal_input_buffers.ads:37 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Terminal_Input_Buffers.Is_At_End at terminal_input_buffers.ads:28 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Terminal_Input_Buffers.Is_Empty at terminal_input_buffers.ads:63 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
Terminal_Input_Buffers.Load_Input at terminal_input_buffers.ads:46 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (12 checks)
Terminal_Input_Buffers.Peek at terminal_input_buffers.ads:95 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
Terminal_Input_Buffers.Skip_Whitespace at terminal_input_buffers.adb:34 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (3 checks)
I have nested records, a Scanner and a Machine. Both of these are private types in their respective packages.
type Scanner is record
Input : String (1 .. Max_Input_Length) :=
(others => No_More_Characters);
Start : Range_Lower := 1;
Cursor : Range_Upper := 1;
Length : Range_Size := 0;
State : Scanner_State := Empty;
end record
with Invariant => Is_Valid (Scanner);
type Machine is record
Status : Machine_Status := Ok;
Stack : Machine_Stack;
Top : Element_Count := 0;
Words : Word_Table;
TIB : Scanners.Scanner;
end record;
My minimized test runner replicating the issue is this:
with Machines;
procedure Anteforth with SPARK_Mode => On is
M : Machines.Machine;
begin
Machines.Push (M, 10);
end Anteforth;
Push points to a procedure with this signature. The program is dying on the entrance to this (the debugger points at Contract_Cases).
procedure Push (Self : in out Machine; Element : Bounded_Value)
with
Global => null,
Depends => (Self => +Element),
Contract_Cases =>
(Is_Stack_Full (Self) => Status (Self) = Stack_Overflow,
others =>
not Is_Stack_Empty (Self)
and then Stack_Size (Self) = Stack_Size (Self'Old) + 1
and then Peek (Self) = Element
and then (for all X in 0 .. Stack_Size (Self'Old) - 1 =>
Peek (Self, X + 1) = Peek (Self'Old, X)));
The failure occurs when checking the Scanner invariant here:
function Is_Valid (Self : Scanner) return Boolean
is (Has_Valid_Cursor (Self) and then Has_Valid_State (Self));
The actual error is inside Has_Valid_Cursor:
function Has_Valid_Cursor (Self : Scanner) return Boolean
is (Self.Start <= Self.Cursor and then Self.Cursor <= Self.Length + 1);
After breaking this up, Self.Length is OK and considered initialized, the error is from the initialization of Self.Start and Self.Cursor.
I thought I was initializing these in the record with this:
Start : Range_Lower := 1;
Cursor : Range_Upper := 1;
Range_Lower and Range_Upper are Integer subtypes.
subtype Small_Int is Integer range 0 .. Max_Input_Length + 1;
subtype Range_Lower is Small_Int range 1 .. Max_Input_Length + 1;
subtype Range_Upper is Small_Int range 1 .. Max_Input_Length + 1;
When I change the lower bound to 0, I no longer get the Invalid_Data error, but it breaks a bunch of proofs.
Could someone help me understand why this is not considered initialized properly?