Skip to content

Commit

Permalink
Merge branch 'fixes-1.1'
Browse files Browse the repository at this point in the history
  • Loading branch information
@Jellix
Jellix committed Jul 15, 2020
2 parents a8ea376 + a942ad4 commit 9a79b3c
Show file tree
Hide file tree
Showing 59 changed files with 57,256 additions and 2,608 deletions.
127 changes: 64 additions & 63 deletions src/core/spat-spark_info-heuristics.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -167,78 +167,79 @@ package body SPAT.Spark_Info.Heuristics is
begin
-- Collect all proof items in the Per_File/Proof_Records structure.
for E of Info.Entities loop
for Proof in E.The_Tree.Iterate_Children (Parent => E.Proofs) loop
declare
SPARK_File : constant SPARK_File_Name :=
Spark_Info.File_Sets.Element (E.SPARK_File);
begin
Times_Position := SPARK_List.Find (Key => SPARK_File);

if Times_Position = Per_File.No_Element then
SPARK_List.Insert
(Key => SPARK_File,
New_Item => Prover_Maps.Empty_Map,
Position => Times_Position,
Inserted => Dummy_Inserted);
end if;
declare
SPARK_File : constant SPARK_File_Name :=
Spark_Info.File_Sets.Element (E.SPARK_File);
begin
Times_Position := SPARK_List.Find (Key => SPARK_File);

-- Iterate over all the verification conditions within the
-- proof.
for VC in
E.The_Tree.Iterate_Children
(Parent => Entity.Tree.First_Child (Position => Proof))
loop
declare
-- Extract our VC component from the tree.
The_Attempt : constant Proof_Attempt.T'Class :=
Proof_Attempt.T'Class
(Entity.Tree.Element (Position => VC));
use type Proof_Attempt.Prover_Result;
begin
declare
File_Ref : constant Per_File.Reference_Type :=
SPARK_List.Reference
(Position => Times_Position);
Prover_Cursor : Prover_Maps.Cursor :=
File_Ref.Element.Find (The_Attempt.Prover);
use type Prover_Maps.Cursor;
begin
if Prover_Cursor = Prover_Maps.No_Element then
-- New prover name, insert it.
File_Ref.Element.Insert
(Key => The_Attempt.Prover,
New_Item => Null_Times,
Position => Prover_Cursor,
Inserted => Dummy_Inserted);
end if;
if Times_Position = Per_File.No_Element then
SPARK_List.Insert
(Key => SPARK_File,
New_Item => Prover_Maps.Empty_Map,
Position => Times_Position,
Inserted => Dummy_Inserted);
end if;

declare
File_Ref : constant Per_File.Reference_Type :=
SPARK_List.Reference (Position => Times_Position);
begin
for Proof in E.The_Tree.Iterate_Children (Parent => E.Proofs) loop
-- Iterate over all the verification conditions within the
-- proof.
for VC in E.The_Tree.Iterate_Children (Parent => Proof) loop
for Attempt in E.The_Tree.Iterate_Children (Parent => VC) loop
declare
Prover_Element : constant Prover_Maps.Reference_Type :=
File_Ref.Reference (Position => Prover_Cursor);
-- Extract our VC component from the tree.
The_Attempt : constant Proof_Attempt.T'Class :=
Proof_Attempt.T'Class
(Entity.Tree.Element (Position => Attempt));
use type Proof_Attempt.Prover_Result;
begin
if The_Attempt.Result = Proof_Attempt.Valid then
Prover_Element.Success :=
Prover_Element.Success + The_Attempt.Time;
declare
Prover_Cursor : Prover_Maps.Cursor :=
File_Ref.Element.Find (The_Attempt.Prover);
use type Prover_Maps.Cursor;
begin
if Prover_Cursor = Prover_Maps.No_Element then
-- New prover name, insert it.
File_Ref.Element.Insert
(Key => The_Attempt.Prover,
New_Item => Null_Times,
Position => Prover_Cursor,
Inserted => Dummy_Inserted);
end if;

Prover_Element.Max_Success :=
Duration'Max (Prover_Element.Max_Success,
The_Attempt.Time);
declare
Prover_Element : constant Prover_Maps.Reference_Type :=
File_Ref.Reference (Position => Prover_Cursor);
begin
if The_Attempt.Result = Proof_Attempt.Valid then
Prover_Element.Success :=
Prover_Element.Success + The_Attempt.Time;

Prover_Element.Max_Steps :=
Prover_Steps'Max
(Prover_Element.Max_Steps,
Scaled (Prover => The_Attempt.Prover,
Raw_Steps => The_Attempt.Steps));
else
Prover_Element.Failed :=
Prover_Element.Failed + The_Attempt.Time;
end if;
Prover_Element.Max_Success :=
Duration'Max (Prover_Element.Max_Success,
The_Attempt.Time);

Prover_Element.Max_Steps :=
Prover_Steps'Max
(Prover_Element.Max_Steps,
Scaled (Prover => The_Attempt.Prover,
Raw_Steps => The_Attempt.Steps));
else
Prover_Element.Failed :=
Prover_Element.Failed + The_Attempt.Time;
end if;
end;
end;
end;
end;
end;
end loop;
end loop;
end loop;
end;
end loop;
end;
end loop;

-- Debug output result.
Expand Down
3 changes: 2 additions & 1 deletion test/spat.test-issues.g.template
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ Warning: This feature is highly experimental.
Warning: Please consult the documentation.

package Prove is
for Proof_Switches ("rflx-rflx_types.ads") use ("--prover=altergo,CVC4,Z3", "--steps=94470", "--timeout=55");
for Proof_Switches ("rflx-arrays-tests.adb") use ("--prover=Z3", "--steps=1768", "--timeout=1");
for Proof_Switches ("rflx-rflx_types.ads") use ("--prover=altergo,CVC4,Z3", "--steps=99104", "--timeout=55");
end Prove;

47 changes: 34 additions & 13 deletions test/spat.test-issues.raca.template
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,34 @@
RFLX.RFLX_Types => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Byte_Index => 10.0 ms/10.0 ms/30.0 ms
RFLX.RFLX_Types.First_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Last_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks
RFLX.RFLX_Types.U64_Extract.D => 4.7 s/9.5 s/70.6 s
RFLX.RFLX_Types.U64_Extract.D.ES => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s
RFLX.RFLX_Types.U64_Extract_Remaining => 10.1 s/120.0 s/376.5 s
RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks
RFLX.RFLX_Types.U64_Insert.Read => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.U64_Insert.Write => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.Unreachable_Bit_Length => 10.0 ms/10.0 ms/10.0 ms
RFLX.Arrays.Tests.Name => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Register_Tests => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671 => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload.Buffer_First => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload.Buffer_Last => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_AV_Enumeration_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_AV_Enumeration_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Enumeration_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Enumeration_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Messages_Message_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Messages_Message_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Modular_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Modular_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Range_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Range_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Valid_Data_Length => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Write_Data => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Byte_Index => 10.0 ms/10.0 ms/30.0 ms
RFLX.RFLX_Types.First_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Last_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks
RFLX.RFLX_Types.U64_Extract.D => 4.7 s/9.5 s/70.6 s
RFLX.RFLX_Types.U64_Extract.D.ES => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s
RFLX.RFLX_Types.U64_Extract_Remaining => 10.1 s/120.0 s/376.5 s
RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks
RFLX.RFLX_Types.U64_Insert.Read => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.U64_Insert.Write => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.Unreachable_Bit_Length => 10.0 ms/10.0 ms/10.0 ms
47 changes: 34 additions & 13 deletions test/spat.test-issues.racs.template
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,34 @@
RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks
RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks
RFLX.RFLX_Types.U64_Extract_Remaining => 10.1 s/120.0 s/376.5 s
RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s
RFLX.RFLX_Types.U64_Extract.D => 4.7 s/9.5 s/70.6 s
RFLX.RFLX_Types.U64_Insert.Read => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.U64_Insert.Write => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.Byte_Index => 10.0 ms/10.0 ms/30.0 ms
RFLX.RFLX_Types.U64_Extract.D.ES => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types.Unreachable_Bit_Length => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.First_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Last_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks
RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks
RFLX.RFLX_Types.U64_Extract_Remaining => 10.1 s/120.0 s/376.5 s
RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s
RFLX.RFLX_Types.U64_Extract.D => 4.7 s/9.5 s/70.6 s
RFLX.RFLX_Types.U64_Insert.Read => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.U64_Insert.Write => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.Byte_Index => 10.0 ms/10.0 ms/30.0 ms
RFLX.RFLX_Types.U64_Extract.D.ES => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types.Unreachable_Bit_Length => 10.0 ms/10.0 ms/10.0 ms
RFLX.Arrays.Tests.Name => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Register_Tests => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671 => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload.Buffer_First => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload.Buffer_Last => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_AV_Enumeration_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_AV_Enumeration_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Enumeration_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Enumeration_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Messages_Message_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Messages_Message_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Modular_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Modular_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Range_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Range_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Valid_Data_Length => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Write_Data => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.First_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Last_Bit_Index => 0.0 s/0.0 s/0.0 s
Loading

0 comments on commit 9a79b3c

Please sign in to comment.