Skip to content

Commit 2aa7329

Browse files
strubstrub
committed
[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.
1 parent f8fab1d commit 2aa7329

File tree

8 files changed

+195
-25
lines changed

8 files changed

+195
-25
lines changed

‎src/ec.ml‎

Lines changed: 77 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -407,15 +407,36 @@ let main () =
407407
(* Initialize I/O + interaction module *)
408408
let module State = struct
409409
type t = {
410-
prvopts : prv_options;
411-
input : string option;
412-
terminal : T.terminal lazy_t;
413-
interactive : bool;
414-
eco : bool;
415-
gccompact : int option;
416-
docgen : bool;
417-
outdirp : string option;
410+
(*---*) prvopts : prv_options;
411+
(*---*) input : string option;
412+
(*---*) terminal : T.terminal lazy_t;
413+
(*---*) interactive : bool;
414+
(*---*) eco : bool;
415+
(*---*) gccompact : int option;
416+
(*---*) docgen : bool;
417+
(*---*) outdirp : string option;
418+
mutable trace : trace1 list option;
418419
}
420+
421+
and trace1 =
422+
{ position : int
423+
; goals : string list option
424+
; messages : (EcGState.loglevel * string) list }
425+
426+
module Trace = struct
427+
let trace0 : trace1 =
428+
{ position = 0; goals = None; messages = []; }
429+
430+
let push1_message (trace1 : trace1) (msg, lvl) : trace1 =
431+
{ trace1 with messages = (msg, lvl) :: trace1.messages }
432+
433+
let push_message (trace : trace1 list) msg =
434+
match trace with
435+
| [] ->
436+
[push1_message trace0 msg]
437+
| trace1 :: trace ->
438+
push1_message trace1 msg :: trace
439+
end
419440
end in
420441

421442
let state : State.t =
@@ -471,7 +492,8 @@ let main () =
471492
; eco = false
472493
; gccompact = None
473494
; docgen = false
474-
; outdirp = None }
495+
; outdirp = None
496+
; trace = None }
475497

476498
end
477499

@@ -493,14 +515,17 @@ let main () =
493515
lazy (T.from_channel ~name ~gcstats ~progress (open_in name))
494516
in
495517

518+
let trace0 = State.{ position = 0; goals = None; messages = [] } in
519+
496520
{ prvopts = {cmpopts.cmpo_provers with prvo_iterate = true}
497521
; input = Some name
498522
; terminal = terminal
499523
; interactive = false
500524
; eco = cmpopts.cmpo_noeco
501525
; gccompact = cmpopts.cmpo_compact
502526
; docgen = false
503-
; outdirp = None }
527+
; outdirp = None
528+
; trace = Some [trace0] }
504529

505530
end
506531

@@ -543,7 +568,8 @@ let main () =
543568
; eco = true
544569
; gccompact = None
545570
; docgen = true
546-
; outdirp = docopts.doco_outdirp }
571+
; outdirp = docopts.doco_outdirp
572+
; trace = None }
547573
end
548574

549575
in
@@ -571,7 +597,20 @@ let main () =
571597

572598
assert (nameo <> input);
573599

574-
let eco = EcEco.{
600+
let eco =
601+
let mktrace (trace : State.trace1 list) : EcEco.ecotrace =
602+
let mktrace1 (trace1 : State.trace1) : int * EcEco.ecotrace1 =
603+
let goals = Option.value ~default:[] trace1.goals in
604+
let messages =
605+
let for1 (lvl, msg) =
606+
Format.sprintf "%s: %s"
607+
(EcGState.string_of_loglevel lvl)
608+
msg in
609+
String.concat "\n" (List.rev_map for1 trace1.messages) in
610+
(trace1.position, EcEco.{ goals; messages; })
611+
in List.rev_map mktrace1 trace in
612+
613+
EcEco.{
575614
eco_root = EcEco.{
576615
eco_digest = Digest.file input;
577616
eco_kind = kind;
@@ -584,6 +623,7 @@ let main () =
584623
eco_kind = x.rqd_kind;
585624
} in (x.rqd_name, (ecr, x.rqd_direct)))
586625
(EcScope.Theory.required scope));
626+
eco_trace = Option.map mktrace state.trace;
587627
} in
588628

589629
let out = open_out nameo in
@@ -665,7 +705,10 @@ let main () =
665705
EcScope.hierror "invalid pragma: `%s'\n%!" x);
666706

667707
let notifier (lvl : EcGState.loglevel) (lazy msg) =
668-
T.notice ~immediate:true lvl msg terminal
708+
state.trace <- state.trace |> Option.map (fun trace ->
709+
State.Trace.push_message trace (lvl, msg)
710+
);
711+
T.notice ~immediate:true lvl msg terminal;
669712
in
670713

671714
EcCommands.addnotifier notifier;
@@ -694,8 +737,25 @@ let main () =
694737
let timed = p.EP.gl_debug = Some `Timed in
695738
let break = p.EP.gl_debug = Some `Break in
696739
let ignore_fail = ref false in
740+
741+
state.trace <- state.trace |> Option.map (fun trace ->
742+
{ State.Trace.trace0 with position = loc.loc_echar } :: trace
743+
);
744+
697745
try
698746
let tdelta = EcCommands.process ~src ~timed ~break p.EP.gl_action in
747+
748+
state.trace <- state.trace |> Option.map (fun trace ->
749+
match trace with
750+
| [] -> assert false
751+
| trace1 :: trace ->
752+
assert (Option.is_none trace1.State.goals);
753+
let goals = EcCommands.pp_all_goals () in
754+
let goals = if List.is_empty goals then None else Some goals in
755+
let trace1 = { trace1 with goals } in
756+
trace1 :: trace
757+
);
758+
699759
if p.EP.gl_fail then begin
700760
ignore_fail := true;
701761
raise (EcScope.HiScopeError (None, "this command is expected to fail"))
@@ -713,10 +773,10 @@ let main () =
713773
raise (EcScope.toperror_of_exn ~gloc:loc e)
714774
end;
715775
if T.interactive terminal then begin
716-
let error =
717-
Format.asprintf
718-
"The following error has been ignored:@.@.@%a"
719-
EcPException.exn_printer e in
776+
let error =
777+
Format.asprintf
778+
"The following error has been ignored:@.@.@%a"
779+
EcPException.exn_printer e in
720780
T.notice ~immediate:true `Info error terminal
721781
end
722782
end)

‎src/ecCommands.ml‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -912,6 +912,11 @@ let addnotifier (notifier : notifier) =
912912
let gstate = EcScope.gstate (oget !context).ct_root in
913913
ignore (EcGState.add_notifier notifier gstate)
914914

915+
(* -------------------------------------------------------------------- *)
916+
let notify (level : EcGState.loglevel) fmt =
917+
assert (EcUtils.is_some !context);
918+
EcScope.notify (oget !context).ct_root level fmt
919+
915920
(* -------------------------------------------------------------------- *)
916921
let current () =
917922
(oget !context).ct_current
@@ -1017,7 +1022,36 @@ let pp_current_goal ?(all = false) stream =
10171022
end
10181023
end
10191024

1025+
(* -------------------------------------------------------------------- *)
10201026
let pp_maybe_current_goal stream =
10211027
match (Pragma.get ()).pm_verbose with
10221028
| true -> pp_current_goal ~all:(Pragma.get ()).pm_g_prall stream
10231029
| false -> ()
1030+
1031+
(* -------------------------------------------------------------------- *)
1032+
let pp_all_goals () =
1033+
let scope = current () in
1034+
1035+
match S.xgoal scope with
1036+
| Some { S.puc_active = Some ({ puc_jdg = S.PSCheck pf }, _) } -> begin
1037+
match EcCoreGoal.opened pf with
1038+
| None ->
1039+
[]
1040+
1041+
| Some _ ->
1042+
let get_hc { EcCoreGoal.g_hyps; EcCoreGoal.g_concl } =
1043+
(EcEnv.LDecl.tohyps g_hyps, g_concl)
1044+
in
1045+
1046+
let ppe = EcPrinting.PPEnv.ofenv (S.env scope) in
1047+
let goals = List.map get_hc (EcCoreGoal.all_opened pf) in
1048+
1049+
List.map (fun goal ->
1050+
let buffer = Buffer.create 0 in
1051+
Format.fprintf
1052+
(Format.formatter_of_buffer buffer)
1053+
"%a@?" (EcPrinting.pp_goal1 ppe) goal;
1054+
Buffer.contents buffer) goals
1055+
end
1056+
1057+
| _ -> []

‎src/ecCommands.mli‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ val initialize :
3636

3737
val current : unit -> EcScope.scope
3838
val addnotifier : notifier -> unit
39+
val notify : EcGState.loglevel -> ('a, Format.formatter, unit, unit) format4 -> 'a
3940

4041
(* -------------------------------------------------------------------- *)
4142
val process_internal :
@@ -60,6 +61,7 @@ val doc_comment : [`Global | `Item] * string -> unit
6061
(* -------------------------------------------------------------------- *)
6162
val pp_current_goal : ?all:bool -> Format.formatter -> unit
6263
val pp_maybe_current_goal : Format.formatter -> unit
64+
val pp_all_goals : unit -> string list
6365

6466
(* -------------------------------------------------------------------- *)
6567
val pragma_verbose : bool -> unit

‎src/ecCorePrinting.ml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -112,6 +112,8 @@ module type PrinterAPI = sig
112112
val pp_hyps : PPEnv.t -> EcEnv.LDecl.hyps pp
113113
val pp_goal : PPEnv.t -> prpo_display -> ppgoal pp
114114

115+
val pp_goal1 : PPEnv.t -> (EcBaseLogic.hyps * form) pp
116+
115117
(* ------------------------------------------------------------------ *)
116118
val pp_by_theory : PPEnv.t -> (PPEnv.t -> (EcPath.path * 'a) pp) -> ((EcPath.path * 'a) list) pp
117119

‎src/ecEco.ml‎

Lines changed: 71 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ module Json = Yojson
55

66
(* -------------------------------------------------------------------- *)
77
module Version = struct
8-
let current : int = 3
8+
let current : int = 4
99
end
1010

1111
(* -------------------------------------------------------------------- *)
@@ -16,9 +16,16 @@ type ecoroot = {
1616
eco_digest : digest;
1717
}
1818

19+
type ecorange = int
20+
21+
type ecotrace1 = { goals: string list; messages: string; }
22+
23+
type ecotrace = (ecorange * ecotrace1) list
24+
1925
type eco = {
2026
eco_root : ecoroot;
2127
eco_depends : ecodepend Mstr.t;
28+
eco_trace : ecotrace option;
2229
}
2330

2431
and ecodepend =
@@ -36,6 +43,24 @@ let flag_of_json (data : Json.t) : bool =
3643
let flag_to_json (flag : bool) : Json.t =
3744
`Bool flag
3845

46+
(* -------------------------------------------------------------------- *)
47+
let int_of_json (data : Json.t) : int =
48+
match data with
49+
| `Int i -> i
50+
| _ -> raise InvalidEco
51+
52+
(* -------------------------------------------------------------------- *)
53+
let string_of_json (data : Json.t) : string =
54+
match data with
55+
| `String s -> s
56+
| _ -> raise InvalidEco
57+
58+
(* -------------------------------------------------------------------- *)
59+
let list_of_json (tx : Json.t -> 'a) (data : Json.t) : 'a list =
60+
match data with
61+
| `List data -> List.map tx data
62+
| _ -> raise InvalidEco
63+
3964
(* -------------------------------------------------------------------- *)
4065
let kind_to_json (k : EcLoader.kind) =
4166
match k with
@@ -71,9 +96,9 @@ let ecoroot_to_map (ecor : ecoroot) : (string * Json.t) list =
7196
"digest", digest_to_json ecor.eco_digest ]
7297

7398
let ecoroot_of_map (data : Json.t Mstr.t) : ecoroot =
74-
let kd = kind_of_json (Mstr.find_exn InvalidEco "kind" data) in
75-
let dg = digest_of_json (Mstr.find_exn InvalidEco "digest" data) in
76-
{ eco_kind = kd; eco_digest = dg; }
99+
let eco_kind = kind_of_json (Mstr.find_exn InvalidEco "kind" data) in
100+
let eco_digest = digest_of_json (Mstr.find_exn InvalidEco "digest" data) in
101+
{ eco_kind; eco_digest; }
77102

78103
(* -------------------------------------------------------------------- *)
79104
let ecoroot_to_json (ecor : ecoroot) : Json.t =
@@ -86,6 +111,43 @@ let ecoroot_of_json (data : Json.t) : ecoroot =
86111

87112
| _ -> raise InvalidEco
88113

114+
(* -------------------------------------------------------------------- *)
115+
let trace_to_json (trace : ecotrace option) : Json.t =
116+
match trace with
117+
| None ->
118+
`Null
119+
120+
| Some trace ->
121+
let for1 ((position, { goals; messages; })) =
122+
`Assoc [
123+
("position", `Int position);
124+
("goals" , `List (List.map (fun goal -> `String goal) goals));
125+
("messages", `String messages);
126+
]
127+
in `List (List.map for1 trace)
128+
129+
let trace_of_json (data : Json.t) : ecotrace option =
130+
match data with
131+
| `Null ->
132+
None
133+
134+
| `List data ->
135+
let for1 (data : Json.t) =
136+
match data with
137+
| `Assoc data ->
138+
let data = Mstr.of_list data in
139+
let position = Mstr.find_exn InvalidEco "position" data |> int_of_json in
140+
let goals = Mstr.find_exn InvalidEco "goals" data |> list_of_json string_of_json in
141+
let messages = Mstr.find_exn InvalidEco "messages" data |> string_of_json in
142+
(position, { goals; messages; })
143+
| _ ->
144+
raise InvalidEco
145+
146+
in Some (List.map for1 data)
147+
148+
| _ ->
149+
raise InvalidEco
150+
89151
(* -------------------------------------------------------------------- *)
90152
let ecodepend_to_json ((ecor, direct) : ecodepend) : Json.t =
91153
`Assoc ([ "direct", flag_to_json direct] @ (ecoroot_to_map ecor))
@@ -119,6 +181,7 @@ let to_json (eco : eco) : Json.t =
119181
[ "version", `Int Version.current;
120182
"echash" , `String EcVersion.hash;
121183
"root" , ecoroot_to_json eco.eco_root;
184+
"trace" , trace_to_json eco.eco_trace;
122185
"depends", `Assoc depends ]
123186

124187
(* -------------------------------------------------------------------- *)
@@ -135,10 +198,11 @@ let of_json (data : Json.t) : eco =
135198
if echash <> `String EcVersion.hash then
136199
raise InvalidEco;
137200

138-
let root = ecoroot_of_json (Mstr.find_exn InvalidEco "root" data) in
139-
let depends = depends_of_json (Mstr.find_exn InvalidEco "depends" data) in
201+
let eco_root = ecoroot_of_json (Mstr.find_exn InvalidEco "root" data) in
202+
let eco_depends = depends_of_json (Mstr.find_exn InvalidEco "depends" data) in
203+
let eco_trace = trace_of_json (Mstr.find_exn InvalidEco "trace" data) in
140204

141-
{ eco_root = root; eco_depends = depends; }
205+
{ eco_root; eco_depends; eco_trace; }
142206

143207
| _ -> raise InvalidEco
144208

‎src/ecOptions.ml‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ and cmp_option = {
2525
cmpo_tstats : string option;
2626
cmpo_noeco : bool;
2727
cmpo_script : bool;
28+
cmpo_trace : bool;
2829
}
2930

3031
and cli_option = {
@@ -347,6 +348,7 @@ let specs = {
347348
`Spec ("tstats" , `String, "Save timing statistics to <file>");
348349
`Spec ("script" , `Flag , "Computer-friendly output");
349350
`Spec ("no-eco" , `Flag , "Do not cache verification results");
351+
`Spec ("trace" , `Flag , "Save all goals & messages in .eco");
350352
`Spec ("compact", `Int , "<internal>")]);
351353

352354
("cli", "Run EasyCrypt top-level", [
@@ -516,7 +518,8 @@ let cmp_options_of_values ini values input =
516518
cmpo_compact = get_int "compact" values;
517519
cmpo_tstats = get_string "tstats" values;
518520
cmpo_noeco = get_flag "no-eco" values;
519-
cmpo_script = get_flag "script" values; }
521+
cmpo_script = get_flag "script" values;
522+
cmpo_trace = get_flag "trace" values; }
520523

521524
let runtest_options_of_values ini values (input, scenarios) =
522525
{ runo_input = input;

0 commit comments

Comments
 (0)