diff --git a/src/ec.ml b/src/ec.ml index 2207d781bf..948a48ea80 100644 --- a/src/ec.ml +++ b/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) diff --git a/src/ecCommands.ml b/src/ecCommands.ml index a8661e8f16..99a9e675d7 100644 --- a/src/ecCommands.ml +++ b/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 diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 22d0548411..53c233d7ee 100644 --- a/src/ecCommands.mli +++ b/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 -> diff --git a/src/ecEco.ml b/src/ecEco.ml index cd80c80205..2a4ff818c2 100644 --- a/src/ecEco.ml +++ b/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 diff --git a/src/ecOptions.ml b/src/ecOptions.ml index 4056d0205b..c481e817f0 100644 --- a/src/ecOptions.ml +++ b/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 "); `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 , "")]); ("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; diff --git a/src/ecOptions.mli b/src/ecOptions.mli index b779aa44e9..8155576716 100644 --- a/src/ecOptions.mli +++ b/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 = {