[eco]: add a compilation trace (messages + goals)

ECO version is now 4.

The trace field is optional. The -trace command line option triggers
the trace recording in the generated .eco file.

Author: strub

src/ec.ml

@@ -382,13 +382,34 @@ let main () =
   (* Initialize I/O + interaction module *)
   let module State = struct
     type t = {
-      prvopts     : prv_options;
-      input       : string option;
-      terminal    : T.terminal lazy_t;
-      interactive : bool;
-      eco         : bool;
-      gccompact   : int option;
+      (*---*) prvopts     : prv_options;
+      (*---*) input       : string option;
+      (*---*) terminal    : T.terminal lazy_t;
+      (*---*) interactive : bool;
+      (*---*) eco         : bool;
+      (*---*) gccompact   : int option;
+      mutable trace       : trace1 list option;
     }
+
+    and trace1 =
+      { position : int
+      ; goal     : string option
+      ; messages : (EcGState.loglevel * string) list }
+
+    module Trace = struct
+      let trace0 : trace1 =
+        { position = 0; goal = None; messages = []; }
+
+      let push1_message (trace1 : trace1) (msg, lvl) : trace1 =
+        { trace1 with messages = (msg, lvl) :: trace1.messages }
+
+      let push_message (trace : trace1 list) msg =
+        match trace with
+        | [] ->
+          [push1_message trace0 msg] 
+        | trace1 :: trace ->
+          push1_message trace1 msg :: trace
+    end
   end in
 
   let state : State.t =
@@ -442,7 +463,8 @@ let main () =
         ; terminal    = terminal
         ; interactive = true
         ; eco         = false
-        ; gccompact   = None }
+        ; gccompact   = None
+        ; trace       = None }
 
     end
 
@@ -464,12 +486,15 @@ let main () =
           lazy (T.from_channel ~name ~gcstats ~progress (open_in name))
         in
 
+        let trace0 = State.{ position = 0; goal = None; messages = [] } in
+
         { prvopts     = {cmpopts.cmpo_provers with prvo_iterate = true}
         ; input       = Some name
         ; terminal    = terminal
         ; interactive = false
         ; eco         = cmpopts.cmpo_noeco
-        ; gccompact   = cmpopts.cmpo_compact }
+        ; gccompact   = cmpopts.cmpo_compact
+        ; trace       = Some [trace0] }
 
       end
 
@@ -500,7 +525,20 @@ let main () =
 
         assert (nameo <> input);
 
-        let eco = EcEco.{
+        let eco =
+          let mktrace (trace : State.trace1 list) : EcEco.ecotrace =
+            let mktrace1 (trace1 : State.trace1) : int * EcEco.ecotrace1 =
+              let goal = Option.value ~default:"" trace1.goal in
+              let messages =
+                let for1 (lvl, msg) =
+                  Format.sprintf "%s: %s"
+                    (EcGState.string_of_loglevel lvl)
+                    msg in
+                String.concat "\n" (List.rev_map for1 trace1.messages) in
+              (trace1.position, EcEco.{ goal; messages; })
+            in List.rev_map mktrace1 trace in 
+
+          EcEco.{
             eco_root    = EcEco.{
               eco_digest  = Digest.file input;
               eco_kind    = kind;
@@ -513,6 +551,7 @@ let main () =
                      eco_kind   = x.rqd_kind;
                    } in (x.rqd_name, (ecr, x.rqd_direct)))
                 (EcScope.Theory.required scope));
+            eco_trace = Option.map mktrace state.trace;
         } in
 
         let out = open_out nameo in
@@ -589,7 +628,10 @@ let main () =
                EcScope.hierror "invalid pragma: `%s'\n%!" x);
 
             let notifier (lvl : EcGState.loglevel) (lazy msg) =
-              T.notice ~immediate:true lvl msg terminal
+              state.trace <- state.trace |> Option.map (fun trace ->
+                State.Trace.push_message trace (lvl, msg)
+              );
+              T.notice ~immediate:true lvl msg terminal;
             in
 
             EcCommands.addnotifier notifier;
@@ -617,8 +659,30 @@ let main () =
                    let timed = p.EP.gl_debug = Some `Timed in
                    let break = p.EP.gl_debug = Some `Break in
                    let ignore_fail = ref false in
+
+                     state.trace <- state.trace |> Option.map (fun trace ->
+                      { State.Trace.trace0 with position = loc.loc_echar } :: trace
+                     );
+
                      try
                        let tdelta = EcCommands.process ~timed ~break p.EP.gl_action in
+
+                       state.trace <- state.trace |> Option.map (fun trace ->
+                        match trace with
+                        | [] -> assert false
+                        | trace1 :: trace ->
+                          assert (Option.is_none trace1.State.goal);
+                          let goal =
+                            let buffer = Buffer.create 0 in
+                            Format.fprintf
+                              (Format.formatter_of_buffer buffer)
+                              "%t@?" (EcCommands.pp_current_goal ~all:false);
+                            Buffer.contents buffer in
+                          let goal = if String.is_empty goal then None else Some goal in
+                          let trace1 = { trace1 with goal } in
+                          trace1 :: trace
+                       );
+
                        if p.EP.gl_fail then begin
                          ignore_fail := true;
                          raise (EcScope.HiScopeError (None, "this command is expected to fail"))
@@ -636,10 +700,10 @@ let main () =
                          raise (EcScope.toperror_of_exn ~gloc:loc e)
                        end;
                        if T.interactive terminal then begin
-                         let error =
-                           Format.asprintf
-                             "The following error has been ignored:@.@.@%a"
-                             EcPException.exn_printer e in
+                        let error =
+                          Format.asprintf
+                            "The following error has been ignored:@.@.@%a"
+                            EcPException.exn_printer e in
                          T.notice ~immediate:true `Info error terminal
                        end
                    end)

src/ecCommands.ml

@@ -773,6 +773,11 @@ let addnotifier (notifier : notifier) =
   let gstate = EcScope.gstate (oget !context).ct_root in
   ignore (EcGState.add_notifier notifier gstate)
 
+(* -------------------------------------------------------------------- *)
+let notify (level : EcGState.loglevel) fmt =
+  assert (EcUtils.is_some !context);
+  EcScope.notify (oget !context).ct_root level fmt
+
 (* -------------------------------------------------------------------- *)
 let current () =
   (oget !context).ct_current

src/ecCommands.mli

@@ -30,6 +30,7 @@ val initialize  :
 
 val current     : unit -> EcScope.scope
 val addnotifier : notifier -> unit
+val notify      : EcGState.loglevel -> ('a, Format.formatter, unit, unit) format4 -> 'a
 
 (* -------------------------------------------------------------------- *)
 val process : ?timed:bool -> ?break:bool ->

src/ecEco.ml

@@ -5,7 +5,7 @@ module Json = Yojson
 
 (* -------------------------------------------------------------------- *)
 module Version = struct
-  let current : int = 3
+  let current : int = 4
 end
 
 (* -------------------------------------------------------------------- *)
@@ -16,9 +16,16 @@ type ecoroot = {
   eco_digest : digest;
 }
 
+type ecorange = int
+
+type ecotrace1 = { goal: string; messages: string; }
+
+type ecotrace = (ecorange * ecotrace1) list
+
 type eco = {
   eco_root    : ecoroot;
   eco_depends : ecodepend Mstr.t;
+  eco_trace   : ecotrace option;
 }
 
 and ecodepend =
@@ -37,6 +44,18 @@ let flag_to_json (flag : bool) : Json.t =
   `Bool flag
 
 (* -------------------------------------------------------------------- *)
+let int_of_json (data : Json.t) : int =
+  match data with
+  | `Int i -> i
+  | _ -> raise InvalidEco
+
+(* -------------------------------------------------------------------- *)
+let string_of_json (data : Json.t) : string =
+  match data with
+  | `String s -> s
+  | _ -> raise InvalidEco
+
+  (* -------------------------------------------------------------------- *)
 let kind_to_json (k : EcLoader.kind) =
   match k with
   | `Ec  -> `String "ec"
@@ -71,9 +90,9 @@ let ecoroot_to_map (ecor : ecoroot) : (string * Json.t) list =
     "digest", digest_to_json ecor.eco_digest ]
 
 let ecoroot_of_map (data : Json.t Mstr.t) : ecoroot =
-  let kd = kind_of_json (Mstr.find_exn InvalidEco "kind" data) in
-  let dg = digest_of_json (Mstr.find_exn InvalidEco "digest" data) in
-  { eco_kind = kd; eco_digest = dg; }
+  let eco_kind   = kind_of_json (Mstr.find_exn InvalidEco "kind" data) in
+  let eco_digest = digest_of_json (Mstr.find_exn InvalidEco "digest" data) in
+  { eco_kind; eco_digest; }
 
 (* -------------------------------------------------------------------- *)
 let ecoroot_to_json (ecor : ecoroot) : Json.t =
@@ -86,6 +105,43 @@ let ecoroot_of_json (data : Json.t) : ecoroot =
 
   | _ -> raise InvalidEco
 
+(* -------------------------------------------------------------------- *)
+let trace_to_json (trace : ecotrace option) : Json.t =
+  match trace with
+  | None ->
+    `Null
+
+  | Some trace ->
+    let for1 ((position, { goal; messages; })) =
+      `Assoc [
+        ("position", `Int position);
+        ("goal"    , `String goal);
+        ("messages", `String messages);
+      ]
+    in `List (List.map for1 trace)
+
+let trace_of_json (data : Json.t) : ecotrace option =
+  match data with
+  | `Null ->
+    None
+
+  | `List data ->
+    let for1 (data : Json.t) =
+      match data with
+      | `Assoc data ->
+        let data = Mstr.of_list data in
+        let position = Mstr.find_exn InvalidEco "position" data |> int_of_json in
+        let goal = Mstr.find_exn InvalidEco "goal" data |> string_of_json in
+        let messages = Mstr.find_exn InvalidEco "messages" data |> string_of_json in
+        (position, { goal; messages; })
+      | _ ->
+        raise InvalidEco
+
+    in Some (List.map for1 data)
+
+  | _ ->
+    raise InvalidEco
+
 (* -------------------------------------------------------------------- *)
 let ecodepend_to_json ((ecor, direct) : ecodepend) : Json.t =
   `Assoc ([ "direct", flag_to_json direct] @ (ecoroot_to_map ecor))
@@ -119,6 +175,7 @@ let to_json (eco : eco) : Json.t =
     [ "version", `Int Version.current;
       "echash" , `String EcVersion.hash;
       "root"   , ecoroot_to_json eco.eco_root;
+      "trace"  , trace_to_json eco.eco_trace;
       "depends", `Assoc depends ]
 
 (* -------------------------------------------------------------------- *)
@@ -135,10 +192,11 @@ let of_json (data : Json.t) : eco =
       if echash <> `String EcVersion.hash then
         raise InvalidEco;
 
-      let root    = ecoroot_of_json (Mstr.find_exn InvalidEco "root" data) in
-      let depends = depends_of_json (Mstr.find_exn InvalidEco "depends" data) in
+      let eco_root    = ecoroot_of_json (Mstr.find_exn InvalidEco "root" data) in
+      let eco_depends = depends_of_json (Mstr.find_exn InvalidEco "depends" data) in
+      let eco_trace   = trace_of_json   (Mstr.find_exn InvalidEco "trace" data) in
 
-      { eco_root = root; eco_depends = depends; }
+      { eco_root; eco_depends; eco_trace; }
 
   | _ -> raise InvalidEco
 

src/ecOptions.ml

@@ -24,6 +24,7 @@ and cmp_option = {
   cmpo_tstats  : string option;
   cmpo_noeco   : bool;
   cmpo_script  : bool;
+  cmpo_trace   : bool;
 }
 
 and cli_option = {
@@ -341,6 +342,7 @@ let specs = {
       `Spec  ("tstats" , `String, "Save timing statistics to <file>");
       `Spec  ("script" , `Flag  , "Computer-friendly output");
       `Spec  ("no-eco" , `Flag  , "Do not cache verification results");
+      `Spec  ("trace"  , `Flag  , "Save all goals & messages in .eco");
       `Spec  ("compact", `Int   , "<internal>")]);
 
     ("cli", "Run EasyCrypt top-level", [
@@ -506,7 +508,8 @@ let cmp_options_of_values ini values input =
     cmpo_compact = get_int "compact" values;
     cmpo_tstats  = get_string "tstats" values;
     cmpo_noeco   = get_flag "no-eco" values;
-    cmpo_script  = get_flag "script" values; }
+    cmpo_script  = get_flag "script" values;
+    cmpo_trace   = get_flag "trace" values; }
 
 let runtest_options_of_values ini values (input, scenarios) =
   { runo_input     = input;

src/ecOptions.mli

@@ -20,6 +20,7 @@ and cmp_option = {
   cmpo_tstats  : string option;
   cmpo_noeco   : bool;
   cmpo_script  : bool;
+  cmpo_trace   : bool;
 }
 
 and cli_option = {