Skip to content

Commit

Permalink
Fixes for issue #6
Browse files Browse the repository at this point in the history 
* Collect all gnatwhy3 prefixed timings into the proof timing entity.
  Gets rid of warnings about missing required fields, as these fields are technically not 'required'.
* Implemented summing of proof times for GNAT CE 2020.
* Fixed a bug in the time accumulation function.
  • Loading branch information
@Jellix
Jellix committed May 28, 2020
1 parent ccaaec2 commit 112a032
Show file tree
Hide file tree
Showing 5 changed files with 106 additions and 40 deletions.
8 changes: 4 additions & 4 deletions src/spat-field_names.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,9 +43,9 @@ package SPAT.Field_Names is
"translation of compilation unit";

-- GNAT_CE_2020
Register_VCs : constant UTF8_String := "gnatwhy3.register_vcs";
Run_VCs : constant UTF8_String := "gnatwhy3.run_vcs";
Schedule_VCs : constant UTF8_String := "gnatwhy3.schedule_vcs";
Session_Map : constant UTF8_String := "session_map";
GNAT_Why3_Prefixed : constant UTF8_String := "gnatwhy3.";
-- Not really a single field name, but a collection of subfields containing
-- timing information.
Session_Map : constant UTF8_String := "session_map";

end SPAT.Field_Names;
63 changes: 51 additions & 12 deletions src/spat-spark_info.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,9 @@ package body SPAT.Spark_Info is
---------------------------------------------------------------------------
-- Map_Entities
---------------------------------------------------------------------------
procedure Map_Entities (This : in out T;
Root : in JSON_Value) with
procedure Map_Entities (This : in out T;
Root : in JSON_Value;
From_File : in Subject_Name) with
Pre => (Preconditions.Ensure_Field (Object => Root,
Field => Field_Names.Name,
Kind => JSON_String_Type) and then
Expand Down Expand Up @@ -74,8 +75,9 @@ package body SPAT.Spark_Info is
---------------------------------------------------------------------------
-- Map_Spark_Elements
---------------------------------------------------------------------------
procedure Map_Spark_Elements (This : in out T;
Root : in JSON_Array);
procedure Map_Spark_Elements (This : in out T;
Root : in JSON_Array;
From_File : in Subject_Name);

---------------------------------------------------------------------------
-- Map_Timings
Expand Down Expand Up @@ -241,8 +243,9 @@ package body SPAT.Spark_Info is
---------------------------------------------------------------------------
-- Map_Entities
---------------------------------------------------------------------------
procedure Map_Entities (This : in out T;
Root : in JSON_Value)
procedure Map_Entities (This : in out T;
Root : in JSON_Value;
From_File : in Subject_Name)
is
Obj_Name : constant Subject_Name := Root.Get (Field => Field_Names.Name);
Slocs : constant JSON_Array := Root.Get (Field => Field_Names.Sloc);
Expand All @@ -254,6 +257,8 @@ package body SPAT.Spark_Info is
Element : Analyzed_Entity;
Dummy_Inserted : Boolean;
begin
Element.SPARK_File := From_File;

This.Entities.Insert (Key => Obj_Name,
New_Item => Element,
Position => Index,
Expand Down Expand Up @@ -413,8 +418,9 @@ package body SPAT.Spark_Info is
---------------------------------------------------------------------------
-- Map_Spark_Elements
---------------------------------------------------------------------------
procedure Map_Spark_Elements (This : in out T;
Root : in JSON_Array)
procedure Map_Spark_Elements (This : in out T;
Root : in JSON_Array;
From_File : in Subject_Name)
is
Length : constant Natural := GNATCOLL.JSON.Length (Arr => Root);
begin
Expand All @@ -434,7 +440,8 @@ package body SPAT.Spark_Info is
Field => Field_Names.Sloc,
Kind => JSON_Array_Type)
then
This.Map_Entities (Root => Element);
This.Map_Entities (Root => Element,
From_File => From_File);
end if;
end;
end loop;
Expand All @@ -458,7 +465,8 @@ package body SPAT.Spark_Info is
Kind => JSON_Array_Type)
then
This.Map_Spark_Elements
(Root => Root.Get (Field => Field_Names.Spark));
(Root => Root.Get (Field => Field_Names.Spark),
From_File => File);
end if;

if
Expand Down Expand Up @@ -574,7 +582,38 @@ package body SPAT.Spark_Info is
---------------------------------------------------------------------------
function Proof_Time (This : in T;
File : in Subject_Name) return Duration is
(This.Files (File).Proof);
Timings : constant Timing_Items.T := This.Files (File);
begin
case Timings.Version is
when GNAT_CE_2019 =>
-- In this version we have a "proof" timing field, report it
-- directly.
return Timings.Proof;

when GNAT_CE_2020 =>
declare
Summed_Proof_Time : Duration := Timings.Proof;
begin
-- In this version there's no proof timing field anymore, so we
-- need to sum the proof times of the entities, too.
for Position in This.Entities.Iterate loop
declare
Name : constant Subject_Name :=
Analyzed_Entities.Key (Position);
begin
if
Analyzed_Entities.Element (Position).SPARK_File = File
then
Summed_Proof_Time :=
Summed_Proof_Time + This.Total_Proof_Time (Name);
end if;
end;
end loop;

return Summed_Proof_Time;
end;
end case;
end Proof_Time;

---------------------------------------------------------------------------
-- Sort_Entity_By_Name
Expand Down Expand Up @@ -647,7 +686,7 @@ package body SPAT.Spark_Info is
Total_Time : Duration := 0.0;
begin
for P of This.Entities (Entity).Proofs loop
Total_Time := Duration'Max (Total_Time, P.Total_Time);
Total_Time := Total_Time + P.Total_Time;
end loop;

return Total_Time;
Expand Down
6 changes: 4 additions & 2 deletions src/spat-spark_info.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,8 +93,9 @@ package SPAT.Spark_Info is
--
-- Reported time taken for all the proofs for File.
---------------------------------------------------------------------------
not overriding function Proof_Time (This : in T;
File : in Subject_Name) return Duration;
not overriding
function Proof_Time (This : in T;
File : in Subject_Name) return Duration;

---------------------------------------------------------------------------
-- Max_Proof_Time
Expand Down Expand Up @@ -136,6 +137,7 @@ private

type Analyzed_Entity is
record
SPARK_File : Subject_Name; -- Which file this entity was found in.
Source_Lines : Entity_Lines.Vector;
Flows : Flow_Items.Vector;
Proofs : Proof_Items.Vector;
Expand Down
45 changes: 36 additions & 9 deletions src/spat-timing_items.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,21 +7,48 @@
------------------------------------------------------------------------------
pragma License (Unrestricted);

with Ada.Strings.Fixed;

package body SPAT.Timing_Items is

function Create (Object : in JSON_Value;
Version : in File_Version) return T is
Proof_Time : Duration;
begin
case Version is
when GNAT_CE_2019 =>
Proof_Time :=
Duration (Object.Get_Long_Float (Field => Field_Names.Proof));
when GNAT_CE_2020 =>
declare
-- Callback when mapping the timing object. If the name of the
-- JSON value matches "gnatwhy3." we assume it's a timing value
-- that should be added to the proof time.
procedure Add_Why3_Time (Name : in UTF8_String;
Value : in JSON_Value);

procedure Add_Why3_Time (Name : in UTF8_String;
Value : in JSON_Value) is
begin
if
Ada.Strings.Fixed.Index
(Source => Name,
Pattern => Field_Names.GNAT_Why3_Prefixed) = 1
then
Proof_Time := Proof_Time + Duration (Value.Get_Long_Float);
end if;
end Add_Why3_Time;
begin
Proof_Time := 0.0;
GNATCOLL.JSON.Map_JSON_Object (Val => Object,
CB => Add_Why3_Time'Access);
end;
end case;

return
T'(Proof =>
(case Version is
when GNAT_CE_2019 =>
Duration (Object.Get_Long_Float (Field => Field_Names.Proof)),
when GNAT_CE_2020 =>
Duration (Object.Get_Long_Float (Field => Field_Names.Register_VCs) +
Object.Get_Long_Float (Field => Field_Names.Schedule_VCs) +
Object.Get_Long_Float (Field => Field_Names.Run_VCs))),
Flow =>
T'(Version => Version,
Proof => Proof_Time,
Flow =>
Duration
(Object.Get_Long_Float (Field => Field_Names.Flow_Analysis)));
end Create;
Expand Down
24 changes: 11 additions & 13 deletions src/spat-timing_items.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,33 +29,31 @@ private package SPAT.Timing_Items is
Preconditions.Ensure_Field (Object => Object,
Field => Field_Names.Proof,
Kind => JSON_Float_Type),
-- Here, we don't really check for required fields anymore, there
-- is a whole bunch of items starting with "gnatwhy3.". If they are not
-- present that means the "corresponding phase wasn't run at all" (@kanigsson)
-- and we just assume 0.0 s.
when GNAT_CE_2020 =>
Preconditions.Ensure_Field (Object => Object,
Field => Field_Names.Run_VCs,
Kind => JSON_Float_Type) and
Preconditions.Ensure_Field (Object => Object,
Field => Field_Names.Register_VCs,
Kind => JSON_Float_Type) and
Preconditions.Ensure_Field (Object => Object,
Field => Field_Names.Schedule_VCs,
Kind => JSON_Float_Type)) and
True) and
Preconditions.Ensure_Field (Object => Object,
Field => Field_Names.Flow_Analysis,
Kind => JSON_Float_Type));

-- Information obtained from the timing section of a .spark file.
type T is
record
Proof : Duration; -- Total time the prover spent.
Flow : Duration; -- Total time of flow analysis.
Version : File_Version; -- version of file encountered.
Proof : Duration; -- Total time the prover spent.
Flow : Duration; -- Total time of flow analysis.
end record;

function Create (Object : in JSON_Value;
Version : in File_Version) return T with
Pre => Has_Required_Fields (Object => Object,
Version => Version);

None : constant T := T'(Proof => 0.0,
Flow => 0.0);
None : constant T := T'(Version => File_Version'First,
Proof => 0.0,
Flow => 0.0);

end SPAT.Timing_Items;

0 comments on commit 112a032

Please sign in to comment.