Merge pull request #64 from HeisenbugLtd/devel-1.2

doc/inheritance-tree.dot

@@ -9,9 +9,9 @@ digraph "Inheritance Tree"
   "SPAT.Entity.T"          [label="{Entity.T\l|{abstract\l|}}"];
   "SPAT.Entity_Line.T"     [label="{Entity_Line.T\l|{|{+File : Source_File_Name\l|+Line : Natural\l}}}"];
   "SPAT.Entity_Location.T" [label="{SPAT.Entity_Location.T\l|{|{+Column : Natural\l}}}"];
-  "SPAT.Flow_Item.T"       [label="{SPAT.Flow_Item.T\l|{|{+Rule : Subject_Name\l|+Severity : Subject_Name\l}}}"];
-  "SPAT.Proof_Item.T"      [label="{SPAT.Proof_Item.T\l|{|{+Suppressed : Subject_Name\l|+Rule : Subject_Name\l|+Severity : Subject_Name\l|+Max_Success_Time : Duration\l|+Max_Time : Duration\l|+Total_Time : Duration\l|+Id : Proof_Item_Ids.Id\l|+Has_Failed_Attempts : Boolean\l|+Has_Unproved_Attempts : Boolean\l|+Is_Unjustified : Boolean\l}}}"];
-  "SPAT.Proof_Attempt.T"   [label="{SPAT.Proof_Attempt.T\l|{|{+Prover : Subject_Name\l|+Result : Subject_Name\l|+Time : Duration\l|+Steps : Prover_Steps\l|+Id : Proof_Attempt_Ids.Id}}}"];
+  "SPAT.Flow_Item.T"       [label="{SPAT.Flow_Item.T\l|{|{+Rule : Rule_Name\l|+Severity : Severity_Name\l}}}"];
+  "SPAT.Proof_Item.T"      [label="{SPAT.Proof_Item.T\l|{|{+Suppressed : Justification\l|+Rule : Rule_Name\l|+Severity : Severity_Name\l|+Max_Success : Time_And_Steps\l|+Max_Proof : Time_And_Steps\l|+Total_Time : Duration\l|+Id : Proof_Item_Ids.Id\l|+Has_Failed_Attempts : Boolean\l|+Has_Unproved_Attempts : Boolean\l|+Is_Unjustified : Boolean\l}}}"];
+  "SPAT.Proof_Attempt.T"   [label="{SPAT.Proof_Attempt.T\l|{|{+Prover : Prover_Name\l|+Result : Result_Name\l|+Workload : Time_And_Steps\l|+Id : Proof_Attempt_Ids.Id\l}}}"];
   "SPAT.Timing_Item.T"     [label="{SPAT.Timing_Item.T\l|{|{+Version : File_Version\l|+Proof : Duration\l|+Flow : Duration\l}}}"];
 
   "dummy" [style="invis"];

plug-ins/spat.py

@@ -32,7 +32,7 @@ def __init__(self, file, line, column, vc, times):
         self.line = int(line)
         self.column = int(column)
         self.vc = vc
-        self.times = float(max_proof)
+        self.times = float(max_proof.split(" ")[1])
 
 def by_time(elem):
     """

src/app/run_spat-print_entities.adb

@@ -224,9 +224,17 @@ begin --  Print_Entities
                 (Source =>
                    (if Info.Has_Unproved_Attempts (Entity => Entity)
                     then "--" -- Useless if nothing is proven.
-                    else SPAT.Image (Value => Info.Max_Success_Proof_Time (Entity => Entity))) &
-                   "/" & SPAT.Image (Value => Info.Max_Proof_Time (Entity => Entity)) &
-                   "/" & SPAT.Image (Value => Info.Total_Proof_Time (Entity => Entity))));
+                    else
+                      SPAT.Image
+                        (Value => Info.Max_Success_Proof_Time (Entity => Entity),
+                         Steps => Info.Max_Success_Proof_Steps (Entity => Entity))) &
+                      "/" &
+                      SPAT.Image
+                        (Value => Info.Max_Proof_Time (Entity => Entity),
+                         Steps => Info.Max_Proof_Steps (Entity => Entity)) &
+                      "/" &
+                      SPAT.Image
+                        (Value => Info.Total_Proof_Time (Entity => Entity))));
          Output_List.Append (New_Item => Current_Row);
 
          if Detail_Level > SPAT.Command_Line.None then

src/app/run_spat-print_suggestion.adb

@@ -64,10 +64,11 @@ begin
             For_Each_Prover :
             for Prover in File.Provers.Iterate loop
                Min_Steps :=
-                 SPAT.Prover_Steps'Max (File.Provers (Prover).Time.Max_Steps,
-                                        Min_Steps);
+                 SPAT.Prover_Steps'Max
+                   (File.Provers (Prover).Workload.Max_Success.Steps,
+                    Min_Steps);
                Min_Timeout :=
-                 Duration'Max (File.Provers (Prover).Time.Max_Success,
+                 Duration'Max (File.Provers (Prover).Workload.Max_Success.Time,
                                Min_Timeout);
 
                SPAT.Log.Message

src/app/run_spat-print_summary.adb

@@ -14,6 +14,7 @@ pragma License (Unrestricted);
 --  S.P.A.T. - Main program - separate Print_Summary
 --
 ------------------------------------------------------------------------------
+
 with Ada.Text_IO;
 
 with SPAT.Strings;
@@ -78,8 +79,14 @@ begin
                  "Proof => " &
                  (if Max_Success_Proof_Time = -1.0 --  nothing valid found
                   then "--"
-                  else SPAT.Image (Value => Max_Success_Proof_Time)) & "/" &
-                 SPAT.Image (Value => Info.Max_Proof_Time (File => File)) & "/" &
+                  else
+                    SPAT.Image
+                      (Value => Max_Success_Proof_Time,
+                       Steps => Info.Max_Success_Proof_Steps (File => File))) &
+                 "/" &
+                 SPAT.Image (Value => Info.Max_Proof_Time (File => File),
+                             Steps => Info.Max_Proof_Steps (File => File)) &
+                 "/" &
                  SPAT.Image (Value => Info.Proof_Time (File => File)) & ")");
          end;
       end if;

src/app/spat-command_line.ads

@@ -74,6 +74,8 @@ package SPAT.Command_Line is
      (if    Value = "a" then SPAT.Spark_Info.Name
       elsif Value = "s" then SPAT.Spark_Info.Max_Success_Time
       elsif Value = "t" then SPAT.Spark_Info.Max_Time
+      elsif Value = "p" then SPAT.Spark_Info.Max_Steps
+      elsif Value = "q" then SPAT.Spark_Info.Max_Success_Steps
       else  (raise GNATCOLL.Opt_Parse.Opt_Parse_Error with
                  "unknown parameter """ & Value & """"));
 
@@ -150,7 +152,9 @@ package SPAT.Command_Line is
         Help        =>
            "Sorting criterion (SORT-BY: a = alphabetical, " &
            "s = by minimum time for successful proof, " &
-           "t = by maximum proof time)",
+           "t = by maximum proof time, " &
+           "p = by minimum steps for successful proof, " &
+           "q = by maximum steps)",
         Arg_Type    => SPAT.Spark_Info.Sorting_Criterion,
         Convert     => Convert,
         Default_Val => SPAT.Spark_Info.None);

src/core/spat-flow_item.adb

@@ -17,7 +17,9 @@ package body SPAT.Flow_Item is
    overriding
    function Create (Object : in JSON_Value) return T is
      (Entity_Location.Create (Object => Object) with
-        Rule     => Object.Get (Field => Field_Names.Rule),
-        Severity => Object.Get (Field => Field_Names.Severity));
+        Rule     =>
+          Rule_Name (Subject_Name'(Object.Get (Field => Field_Names.Rule))),
+        Severity =>
+          Severity_Name (Subject_Name'(Object.Get (Field => Field_Names.Severity))));
 
 end SPAT.Flow_Item;

src/core/spat-flow_item.ads

@@ -59,8 +59,8 @@ private
 
    type T is new Entity_Location.T with
       record
-         Rule     : Subject_Name;
-         Severity : Subject_Name;
+         Rule     : Rule_Name;
+         Severity : Severity_Name;
       end record;
 
 end SPAT.Flow_Item;

src/core/spat-proof_attempt.adb

@@ -53,20 +53,27 @@ package body SPAT.Proof_Attempt is
                   Result =>
                     Result_Name
                       (Subject_Name'(Object.Get (Field => Field_Names.Result))),
-                  Time   =>
-                    (case Time_Field.Kind is
-                        when JSON_Float_Type =>
-                          Duration (Time_Field.Get_Long_Float),
-                        when JSON_Int_Type   =>
-                          Duration (Long_Long_Integer'(Time_Field.Get)),
-                        when others          =>
-                           raise Program_Error
-                             with
-                               "Fatal: Impossible Kind """ &
-                               Time_Field.Kind'Image & """ of JSON object!"),
-                  Steps  =>
-                    Prover_Steps
-                      (Long_Integer'(Object.Get (Field => Field_Names.Steps))),
+                  Workload =>
+                    Time_And_Steps'
+                      (Time   =>
+                         (case Time_Field.Kind is
+                             when JSON_Float_Type =>
+                               Duration (Time_Field.Get_Long_Float),
+                             when JSON_Int_Type   =>
+                               Duration (Long_Long_Integer'(Time_Field.Get)),
+                             when others          =>
+                                raise Program_Error
+                                  with
+                                    "Fatal: Impossible Kind """ &
+                                    Time_Field.Kind'Image & """ of JSON object!"),
+                       Steps  =>
+                         --  FIXME: Step scaling will not be necessary anymore for
+                         --         the SPARK development version (i.e. SPARK CE 2021).
+                         Scaled (Prover    => Prover,
+                                 Raw_Steps =>
+                                   Prover_Steps
+                                     (Long_Integer'
+                                        (Object.Get (Field => Field_Names.Steps))))),
                   Id     => Proof_Attempt_Ids.Next);
    end Create;
 

src/core/spat-proof_attempt.ads

@@ -106,31 +106,31 @@ private
 
    type T is new Entity.T with
       record
-         Prover : Prover_Name;          --  Prover involved.
-         Result : Result_Name;          --  "Valid", "Unknown", etc.
-         Time   : Duration;             --  time spent during proof
-         Steps  : Prover_Steps;         --  number of steps the prover took
-                                        --  This might be negative (e.g. with
-                                        --  Z3, the number of steps is recorded
-                                        --  as -1, if Z3 ran out of memory.
-         Id     : Proof_Attempt_Ids.Id; --  unique id for stable sorting
+         Prover   : Prover_Name;          --  Prover involved.
+         Result   : Result_Name;          --  "Valid", "Unknown", etc.
+         Workload : Time_And_Steps;
+         --  time spent during proof, and number of steps the prover took
+         --  Steps might be negative (e.g. with Z3, the number of steps is
+         --  recorded as -1 if Z3 ran out of memory).
+         Id       : Proof_Attempt_Ids.Id; --  unique id for stable sorting
       end record;
 
    ---------------------------------------------------------------------------
    --  Image
    ---------------------------------------------------------------------------
    overriding
    function Image (This : in T) return String is
-     (To_String (This.Prover) & ": " & Image (Value => This.Time) &
-        " (" & To_String (This.Result) & "," & This.Steps'Image & " steps)");
+     (To_String (This.Prover) & ": " &
+      Image (Value => This.Time,
+             Steps => This.Steps) & ", " &
+      To_String (This.Result));
 
    function Trivial_True return T is
       (T'(Entity.T with
-              Prover => Prover_Name (To_Name (Source => "Trivial")),
-              Result => Result_Name (To_Name (Source => "Valid")),
-              Time   => 0.0,
-              Steps  => 0,
-              Id     => Proof_Attempt_Ids.Next));
+              Prover    => Prover_Name (To_Name (Source => "Trivial")),
+              Result    => Result_Name (To_Name (Source => "Valid")),
+              Workload  => None,
+              Id        => Proof_Attempt_Ids.Next));
 
    ---------------------------------------------------------------------------
    --  Prover
@@ -153,13 +153,13 @@ private
    ---------------------------------------------------------------------------
    not overriding
    function Steps (This : in T) return Prover_Steps is
-     (This.Steps);
+     (This.Workload.Steps);
 
    ---------------------------------------------------------------------------
    --  Time
    ---------------------------------------------------------------------------
    not overriding
    function Time (This : in T) return Duration is
-     (This.Time);
+     (This.Workload.Time);
 
 end SPAT.Proof_Attempt;

src/core/spat-proof_item.adb

@@ -47,15 +47,14 @@ package body SPAT.Proof_Item is
       --  By Severity (i.e. "info", "warning", ...)
       if Left.Severity /= Right.Severity then
          --  TODO: We should get a list of severities and actually sort them by
-         --        by priority.   For now, textual is all we have.
+         --        priority.   For now, textual is all we have.
          return Left.Severity < Right.Severity;
       end if;
 
       --  Locations are equal, go for last resort, the unique id.
       if Entity_Location."=" (X => Entity_Location.T (Left),
                               Y => Entity_Location.T (Right))
       then
-         --  Last resort. By unique id.
          return Left.Id < Right.Id;
       end if;
 
@@ -75,9 +74,9 @@ package body SPAT.Proof_Item is
       pragma Unreferenced (Version); --  Only for precondition.
 
       --  Collect information about the timing of dependent attempts.
-      Max_Time         : Duration := 0.0;
-      Max_Success_Time : Duration := 0.0;
-      Total_Time       : Duration := 0.0;
+      Max_Proof   : Time_And_Steps := None;
+      Max_Success : Time_And_Steps := None;
+      Total_Time  : Duration := 0.0;
 
       Checks_List : Checks_Lists.Vector;
       Check_Tree  : constant JSON_Array :=
@@ -131,12 +130,24 @@ package body SPAT.Proof_Item is
                         begin
                            Attempts.Append (New_Item => Attempt);
 
-                           Max_Time := Duration'Max (Max_Time, Attempt.Time);
+                           Max_Proof :=
+                             Time_And_Steps'
+                               (Time  =>
+                                  Duration'Max (Max_Proof.Time,
+                                                Attempt.Time),
+                                Steps =>
+                                  Prover_Steps'Max (Max_Proof.Steps,
+                                                    Attempt.Steps));
 
                            if Attempt.Result = Proof_Attempt.Valid then
-                              Max_Success_Time :=
-                                Duration'Max (Max_Success_Time,
-                                              Attempt.Time);
+                              Max_Success :=
+                                Time_And_Steps'
+                                  (Time  =>
+                                     Duration'Max (Max_Success.Time,
+                                                   Attempt.Time),
+                                   Steps =>
+                                     Prover_Steps'Max (Max_Success.Steps,
+                                                       Attempt.Steps));
                            end if;
 
                            Total_Time := Total_Time + Attempt.Time;
@@ -247,10 +258,11 @@ package body SPAT.Proof_Item is
                         Severity_Name
                           (Subject_Name'(Object.Get
                                            (Field => Field_Names.Severity))),
-                      Max_Success_Time      => (if Has_Unproved_Attempts
-                                                then 0.0
-                                                else Max_Success_Time),
-                      Max_Time              => Max_Time,
+                      Max_Success           =>
+                        (if Has_Unproved_Attempts
+                         then None
+                         else Max_Success),
+                      Max_Proof             => Max_Proof,
                       Total_Time            => Total_Time,
                       Id                    => Proof_Item_Ids.Next,
                       Has_Failed_Attempts   => Has_Failed_Attempts,

src/core/spat-proof_item.ads

@@ -101,12 +101,24 @@ package SPAT.Proof_Item is
    not overriding
    function Rule (This : in T) return Rule_Name;
 
+   ---------------------------------------------------------------------------
+   --  Max_Success_Steps
+   ---------------------------------------------------------------------------
+   not overriding
+   function Max_Success_Steps (This : in T) return Prover_Steps;
+
    ---------------------------------------------------------------------------
    --  Max_Success_Time
    ---------------------------------------------------------------------------
    not overriding
    function Max_Success_Time (This : in T) return Duration;
 
+   ---------------------------------------------------------------------------
+   --  Max_Steps
+   ---------------------------------------------------------------------------
+   not overriding
+   function Max_Steps (This : in T) return Prover_Steps;
+
    ---------------------------------------------------------------------------
    --  Max_Time
    ---------------------------------------------------------------------------
@@ -200,10 +212,14 @@ private
          Suppressed            : Justification;
          Rule                  : Rule_Name;
          Severity              : Severity_Name;
-         Max_Success_Time      : Duration; --  Longest time for a successful proof.
-         Max_Time              : Duration; --  Longest time spent in proof (successful or not)
-         Total_Time            : Duration; --  Accumulated proof time.
-         Id                    : Proof_Item_Ids.Id; --  Id for stable sorting.
+         Max_Success           : Time_And_Steps;
+         --  Longest time/steps for a successful proof.
+         Max_Proof             : Time_And_Steps;
+         --  Longest time/steps spent in proof (successful or not).
+         Total_Time            : Duration;
+         --  Accumulated proof time.
+         Id                    : Proof_Item_Ids.Id;
+         --  Id for stable sorting.
          Has_Failed_Attempts   : Boolean;
          Has_Unproved_Attempts : Boolean;
          Is_Unjustified        : Boolean;
@@ -225,8 +241,10 @@ private
         Entity_Location.T (This).Image & " => " &
         (if This.Has_Unproved_Attempts
          then "--"
-         else Image (Value => This.Max_Success_Time)) & "/" &
-        Image (Value => This.Max_Time) & "/" &
+         else Image (Value => This.Max_Success_Time,
+                     Steps => This.Max_Success_Steps)) & "/" &
+        Image (Value => This.Max_Time,
+               Steps => This.Max_Steps) & "/" &
         Image (Value => This.Total_Time));
 
    ---------------------------------------------------------------------------
@@ -243,19 +261,33 @@ private
    function Has_Unproved_Attempts (This : in T) return Boolean is
       (This.Has_Unproved_Attempts);
 
+   ---------------------------------------------------------------------------
+   --  Max_Steps
+   ---------------------------------------------------------------------------
+   not overriding
+   function Max_Steps (This : in T) return Prover_Steps is
+     (This.Max_Proof.Steps);
+
+   ---------------------------------------------------------------------------
+   --  Max_Success_Steps
+   ---------------------------------------------------------------------------
+   not overriding
+   function Max_Success_Steps (This : in T) return Prover_Steps is
+     (This.Max_Success.Steps);
+
    ---------------------------------------------------------------------------
    --  Max_Success_Time
    ---------------------------------------------------------------------------
    not overriding
    function Max_Success_Time (This : in T) return Duration is
-     (This.Max_Success_Time);
+     (This.Max_Success.Time);
 
    ---------------------------------------------------------------------------
    --  Max_Time
    ---------------------------------------------------------------------------
    not overriding
    function Max_Time (This : in T) return Duration is
-     (This.Max_Time);
+     (This.Max_Proof.Time);
 
    ---------------------------------------------------------------------------
    --  Rule