Merge branch 'topic/kanig-272-fail2' into 'master'

Compute status for unproved VC in why3

Issue: eng/spark/spark2014#272

See merge request eng/spark/why3!104

Author: kanigsson

src/gnat/gnat_checks.ml

@@ -896,6 +896,38 @@ module Save_VCs = struct
     Sysutil.write_file vc_fn "";
     vc_fn
 
+  let unproved_prover_answer session check =
+    let check_rec = Gnat_expl.HCheck.find explmap check in
+    let status = ref Gnat_expl.Unknown in
+    let proof_attempt_status pa =
+      match pa.Session_itp.proof_obsolete, pa.Session_itp.proof_state with
+      | false, Some pr -> Gnat_expl.compress pr.Call_provers.pr_answer
+      | _, _ -> Gnat_expl.Unknown
+    in
+    let rec transformation_status tfid =
+      let subgoals = Session_itp.get_sub_tasks session tfid in
+      List.fold_left (fun acc g -> Gnat_expl.merge_all_needed acc (goal_status g)) Gnat_expl.Unknown subgoals
+    and transformation_list_status tl =
+      List.fold_left (fun acc tfid ->
+        Gnat_expl.merge_one_needed acc (transformation_status tfid))
+        Gnat_expl.Unknown tl
+    and proof_attempt_list_status proof_attempts =
+      List.fold_left (fun acc pa ->
+        Gnat_expl.merge_one_needed acc (proof_attempt_status pa))
+        Gnat_expl.Unknown proof_attempts
+    and goal_status g =
+      let proof_attempts = Session_itp.get_proof_attempts session g in
+      let transformations = Session_itp.get_transformations session g in
+      let pa_status = proof_attempt_list_status proof_attempts in
+      let tf_status = transformation_list_status transformations in
+      Gnat_expl.merge_one_needed pa_status tf_status
+    in
+    GoalSet.iter (fun g ->
+      let g_status = goal_status g in
+      status := Gnat_expl.merge_all_needed !status g_status)
+      check_rec.toplevel;
+    !status
+
   (* Group of functions to build a json object for a session tree.
      More precisely a session forest, because we start with a list of
      goals for a given check. See gnat_report.mli for the JSON

src/gnat/gnat_checks.mli

@@ -167,6 +167,10 @@ module Save_VCs : sig
    (* get the file name for a given goal *)
 
    val check_to_json : Session_itp.session -> Gnat_expl.check -> Json_base.json
+
+   val unproved_prover_answer :
+      Session_itp.session -> Gnat_expl.check -> Gnat_expl.unproved_status
+   (* get the unproved status for a given goal *)
 end
 
 val all_split_leaf_goals : unit -> unit

src/gnat/gnat_expl.ml

@@ -648,3 +648,44 @@ module HCheck = Hashtbl.Make (struct
 
    let hash = check_hash
 end)
+
+type unproved_status =
+  | Unknown
+  | Gave_up
+  | Limit of { timeout : bool ; step : bool ; memory : bool }
+
+let compress ans =
+  match ans with
+  | Call_provers.Valid
+  | Call_provers.Invalid
+  | Call_provers.Unknown _
+  | Call_provers.Failure _
+  | Call_provers.HighFailure _ -> Gave_up
+  | Call_provers.Timeout ->
+      Limit { timeout = true ; step = false ; memory = false }
+  | Call_provers.OutOfMemory ->
+      Limit { timeout = false ; step = false ; memory = true }
+  | Call_provers.StepLimitExceeded ->
+      Limit { timeout = false ; step = true ; memory = false }
+
+let merge_all_needed s1 s2 =
+    match s1, s2 with
+    Unknown, _ -> s2
+  | _, Unknown -> s1
+  | Gave_up, _ -> Gave_up
+  | _, Gave_up -> Gave_up
+  | Limit l1, Limit l2 ->
+      Limit { timeout = l1.timeout || l2.timeout ;
+              step = l1.step || l2.step ;
+              memory = l1.memory || l2.memory }
+
+let merge_one_needed s1 s2 =
+  match s1, s2 with
+    Unknown, _ -> s2
+  | _, Unknown -> s1
+  | Gave_up, _ -> s2
+  | _, Gave_up -> s1
+  | Limit l1, Limit l2 ->
+      Limit { timeout = l1.timeout || l2.timeout ;
+              step = l1.step || l2.step ;
+              memory = l1.memory || l2.memory }

src/gnat/gnat_expl.mli

@@ -165,3 +165,22 @@ val search_labels: Why3.Term.term -> vc_info option
 
 val parse_line_spec : string -> limit_mode
 val parse_region_spec : string -> Gnat_loc.region
+
+type unproved_status =
+  | Unknown
+  | Gave_up
+  | Limit of { timeout : bool ; step : bool ; memory : bool }
+(* The unproved status of a goal contains information about the reason
+   why the goal could not be proved. Note that "unknown" means the
+   status is unknown, not that the prover answered unknown.*)
+
+val compress : Call_provers.prover_answer -> unproved_status
+(* Convert a prover answer into an unproved status *)
+
+val merge_all_needed : unproved_status -> unproved_status -> unproved_status
+(* Merge two statuses into one, assuming all proofs are needed
+  for the check to prove. *)
+
+val merge_one_needed : unproved_status -> unproved_status -> unproved_status
+(* Merge two statuses into one, assuming only one proof is needed
+   for the check to prove. *)

src/gnat/gnat_main.ml

@@ -258,7 +258,8 @@ let report_messages c check =
                   with Not_found -> default
               else { Gnat_expl.pretty_node = None; inlined = None }
       in
-      Gnat_report.Not_Proved (extra_info, models, manual_info) in
+      let answer_status = C.Save_VCs.unproved_prover_answer s check in
+      Gnat_report.Not_Proved (extra_info, models, manual_info, answer_status) in
   Gnat_report.register check (C.Save_VCs.check_to_json s check) result
 
 (* Escaping all debug printings *)

src/gnat/gnat_report.ml

@@ -15,16 +15,18 @@ type result_info =
   | Not_Proved of
        Gnat_expl.extra_info *
        (Model_parser.model * Check_ce.rac_result option) list *
-       (string * string) option
+       (string * string) option *
+        Gnat_expl.unproved_status
 
 type msg =
-  { result         : bool;
-    stats          : stats option;
-    stats_checker  : int;
-    check_tree     : Json_base.json;
-    extra_info     : Gnat_expl.extra_info;
-    cntexmp_models : (Model_parser.model * Check_ce.rac_result option) list;
-    manual_proof   : (string * string) option
+  { result           : bool;
+    stats            : stats option;
+    stats_checker    : int;
+    check_tree       : Json_base.json;
+    extra_info       : Gnat_expl.extra_info;
+    cntexmp_models   : (Model_parser.model * Check_ce.rac_result option) list;
+    manual_proof     : (string * string) option;
+    unproved_status : Gnat_expl.unproved_status
   }
 
 let msg_set : msg Gnat_expl.HCheck.t = Gnat_expl.HCheck.create 17
@@ -55,16 +57,17 @@ let adapt_stats statsopt =
       Some newstats
 
 let register check check_tree result =
-  let valid, extra_info, stats, models, manual =
+  let valid, extra_info, stats, models, manual, unproved_status =
     match result with
     | Proved (stats, stats_checker) ->
         true,
         {Gnat_expl.pretty_node = None; inlined = None},
         Some (stats, stats_checker),
         [],
-        None
-    | Not_Proved (extra_info, models, manual) ->
-        false, extra_info, None, models, manual
+        None,
+        Gnat_expl.Unknown
+    | Not_Proved (extra_info, models, manual, unproved_status) ->
+        false, extra_info, None, models, manual, unproved_status
   in
   if (Gnat_expl.HCheck.mem msg_set check) then assert false
   else begin
@@ -77,11 +80,12 @@ let register check check_tree result =
       stats_checker  = Option.value ~default:0 stats_checker;
       check_tree     = check_tree;
       cntexmp_models = models;
-      manual_proof   = manual } in
+      manual_proof   = manual;
+      unproved_status = unproved_status } in
     Gnat_expl.HCheck.add msg_set check msg
   end
 
-let get_cntexmp_models = 
+let get_cntexmp_models =
   List.map (function
   (m, r) ->
       let json_result_state (state, _log) =
@@ -161,14 +165,32 @@ let get_extra_info i =
         "inline", Int (opt_int inline)
       ]
 
+let get_unproved_status status =
+  let status, time, steps, memory =
+    match status with
+    | Gnat_expl.Unknown ->
+        "unknown", false, false, false
+    | Gnat_expl.Gave_up ->
+        "gave_up", false, false, false
+    | Gnat_expl.Limit { timeout; step; memory } ->
+        "limit", timeout, step, memory
+  in
+  Record [
+    "status", String status;
+    "time", Bool time;
+    "steps", Bool steps;
+    "memory", Bool memory
+  ]
+
 let get_msg (check, m) =
   Record (
     List.concat [
       [ "id", Int check.Gnat_expl.id ;
         "check_kind", String (Gnat_expl.check_kind_to_ada check.Gnat_expl.check_kind) ;
         "result", Bool m.result ;
         "check_tree", m.check_tree ;
-        "extra_info", get_extra_info m.extra_info
+        "extra_info", get_extra_info m.extra_info ;
+        "unproved_status", get_unproved_status m.unproved_status
       ] ;
       get_stats (m.stats, m.stats_checker);
       ["cntexmps", List (get_cntexmp_models m.cntexmp_models)];

src/gnat/gnat_report.mli

@@ -27,14 +27,15 @@ open Why3
    The "warnings" field is optional. If present, it contains a list of warnings
    that occured during execution of gnatwhy3.
 
-     result = { "id"             : int,
-                "check_kind"     : string,
-                "result"         : bool,
-                "extra_info"     : extra_info,
-                "vc_file"        : string,
-                "editor_cmd"     : string,
-                "check_tree"     : list goal,
-                "cntexmp"        : cntexmp_rec
+     result = { "id"               : int,
+                "check_kind"       : string,
+                "result"           : bool,
+                "extra_info"       : extra_info,
+                "vc_file"          : string,
+                "editor_cmd"       : string,
+                "check_tree"       : list goal,
+                "cntexmp"          : cntexmp_rec,
+                "unproved_status"  : unproved_status
                 }
 
    The field "id" contains the id of the VC. The field "check_kind" identifies the
@@ -105,6 +106,19 @@ open Why3
              steps : integer,
              result : string }
 
+  The "unproved_status" field contains a summary of the reasons why
+  the goal could not be proved. It is a record with the following fields:
+      unproved_status = { "status" : string,
+                          "time"   : bool,
+                          "steps"  : bool,
+                          "memory" : bool}
+  The "status" field contains one of the following strings:
+    - "gave_up"  : the prover gave up
+    - "limit"    : the prover reached some resource limit
+    - "unknown"  : the prover status is unknown (e.g., no proof attempt
+                   was made, or the goal was proved)
+  The "time", "steps" and "memory" fields are booleans indicating whether
+  the corresponding resource limit was reached.
    *)
 
 type prover_stat =
@@ -125,8 +139,9 @@ type result_info =
       (Model_parser.model * Check_ce.rac_result option) list *
                                  (* counterexample models and their
                                     giant-step RAC result *)
-      (string * string) option   (* for manual provers, pair of
+      (string * string) option *  (* for manual provers, pair of
                                     (vc_file, editor_cmd) *)
+      Gnat_expl.unproved_status
 
 val register : Gnat_expl.check -> Json_base.json -> result_info -> unit
 (* [register check check_tree info] registers a proof result,