Skip to content

Commit 59c52f5

Browse files
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 ddcc091 commit 59c52f5

File tree

6 files changed

+154
-22
lines changed

6 files changed

+154
-22
lines changed

src/ec.ml

Lines changed: 78 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -382,13 +382,34 @@ let main () =
382382
(* Initialize I/O + interaction module *)
383383
let module State = struct
384384
type t = {
385-
prvopts : prv_options;
386-
input : string option;
387-
terminal : T.terminal lazy_t;
388-
interactive : bool;
389-
eco : bool;
390-
gccompact : int option;
385+
(*---*) prvopts : prv_options;
386+
(*---*) input : string option;
387+
(*---*) terminal : T.terminal lazy_t;
388+
(*---*) interactive : bool;
389+
(*---*) eco : bool;
390+
(*---*) gccompact : int option;
391+
mutable trace : trace1 list option;
391392
}
393+
394+
and trace1 =
395+
{ position : int
396+
; goal : string option
397+
; messages : (EcGState.loglevel * string) list }
398+
399+
module Trace = struct
400+
let trace0 : trace1 =
401+
{ position = 0; goal = None; messages = []; }
402+
403+
let push1_message (trace1 : trace1) (msg, lvl) : trace1 =
404+
{ trace1 with messages = (msg, lvl) :: trace1.messages }
405+
406+
let push_message (trace : trace1 list) msg =
407+
match trace with
408+
| [] ->
409+
[push1_message trace0 msg]
410+
| trace1 :: trace ->
411+
push1_message trace1 msg :: trace
412+
end
392413
end in
393414

394415
let state : State.t =
@@ -442,7 +463,8 @@ let main () =
442463
; terminal = terminal
443464
; interactive = true
444465
; eco = false
445-
; gccompact = None }
466+
; gccompact = None
467+
; trace = None }
446468

447469
end
448470

@@ -464,12 +486,15 @@ let main () =
464486
lazy (T.from_channel ~name ~gcstats ~progress (open_in name))
465487
in
466488

489+
let trace0 = State.{ position = 0; goal = None; messages = [] } in
490+
467491
{ prvopts = {cmpopts.cmpo_provers with prvo_iterate = true}
468492
; input = Some name
469493
; terminal = terminal
470494
; interactive = false
471495
; eco = cmpopts.cmpo_noeco
472-
; gccompact = cmpopts.cmpo_compact }
496+
; gccompact = cmpopts.cmpo_compact
497+
; trace = Some [trace0] }
473498

474499
end
475500

@@ -500,7 +525,20 @@ let main () =
500525

501526
assert (nameo <> input);
502527

503-
let eco = EcEco.{
528+
let eco =
529+
let mktrace (trace : State.trace1 list) : EcEco.ecotrace =
530+
let mktrace1 (trace1 : State.trace1) : int * EcEco.ecotrace1 =
531+
let goal = Option.value ~default:"" trace1.goal in
532+
let messages =
533+
let for1 (lvl, msg) =
534+
Format.sprintf "%s: %s"
535+
(EcGState.string_of_loglevel lvl)
536+
msg in
537+
String.concat "\n" (List.rev_map for1 trace1.messages) in
538+
(trace1.position, EcEco.{ goal; messages; })
539+
in List.rev_map mktrace1 trace in
540+
541+
EcEco.{
504542
eco_root = EcEco.{
505543
eco_digest = Digest.file input;
506544
eco_kind = kind;
@@ -513,6 +551,7 @@ let main () =
513551
eco_kind = x.rqd_kind;
514552
} in (x.rqd_name, (ecr, x.rqd_direct)))
515553
(EcScope.Theory.required scope));
554+
eco_trace = Option.map mktrace state.trace;
516555
} in
517556

518557
let out = open_out nameo in
@@ -589,7 +628,10 @@ let main () =
589628
EcScope.hierror "invalid pragma: `%s'\n%!" x);
590629

591630
let notifier (lvl : EcGState.loglevel) (lazy msg) =
592-
T.notice ~immediate:true lvl msg terminal
631+
state.trace <- state.trace |> Option.map (fun trace ->
632+
State.Trace.push_message trace (lvl, msg)
633+
);
634+
T.notice ~immediate:true lvl msg terminal;
593635
in
594636

595637
EcCommands.addnotifier notifier;
@@ -617,8 +659,30 @@ let main () =
617659
let timed = p.EP.gl_debug = Some `Timed in
618660
let break = p.EP.gl_debug = Some `Break in
619661
let ignore_fail = ref false in
662+
663+
state.trace <- state.trace |> Option.map (fun trace ->
664+
{ State.Trace.trace0 with position = loc.loc_echar } :: trace
665+
);
666+
620667
try
621668
let tdelta = EcCommands.process ~timed ~break p.EP.gl_action in
669+
670+
state.trace <- state.trace |> Option.map (fun trace ->
671+
match trace with
672+
| [] -> assert false
673+
| trace1 :: trace ->
674+
assert (Option.is_none trace1.State.goal);
675+
let goal =
676+
let buffer = Buffer.create 0 in
677+
Format.fprintf
678+
(Format.formatter_of_buffer buffer)
679+
"%t@?" (EcCommands.pp_current_goal ~all:false);
680+
Buffer.contents buffer in
681+
let goal = if String.is_empty goal then None else Some goal in
682+
let trace1 = { trace1 with goal } in
683+
trace1 :: trace
684+
);
685+
622686
if p.EP.gl_fail then begin
623687
ignore_fail := true;
624688
raise (EcScope.HiScopeError (None, "this command is expected to fail"))
@@ -636,10 +700,10 @@ let main () =
636700
raise (EcScope.toperror_of_exn ~gloc:loc e)
637701
end;
638702
if T.interactive terminal then begin
639-
let error =
640-
Format.asprintf
641-
"The following error has been ignored:@.@.@%a"
642-
EcPException.exn_printer e in
703+
let error =
704+
Format.asprintf
705+
"The following error has been ignored:@.@.@%a"
706+
EcPException.exn_printer e in
643707
T.notice ~immediate:true `Info error terminal
644708
end
645709
end)

src/ecCommands.ml

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -773,6 +773,11 @@ let addnotifier (notifier : notifier) =
773773
let gstate = EcScope.gstate (oget !context).ct_root in
774774
ignore (EcGState.add_notifier notifier gstate)
775775

776+
(* -------------------------------------------------------------------- *)
777+
let notify (level : EcGState.loglevel) fmt =
778+
assert (EcUtils.is_some !context);
779+
EcScope.notify (oget !context).ct_root level fmt
780+
776781
(* -------------------------------------------------------------------- *)
777782
let current () =
778783
(oget !context).ct_current

src/ecCommands.mli

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,7 @@ val initialize :
3030

3131
val current : unit -> EcScope.scope
3232
val addnotifier : notifier -> unit
33+
val notify : EcGState.loglevel -> ('a, Format.formatter, unit, unit) format4 -> 'a
3334

3435
(* -------------------------------------------------------------------- *)
3536
val process : ?timed:bool -> ?break:bool ->

src/ecEco.ml

Lines changed: 65 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 = { goal: string; 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 =
@@ -37,6 +44,18 @@ let flag_to_json (flag : bool) : Json.t =
3744
`Bool flag
3845

3946
(* -------------------------------------------------------------------- *)
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+
(* -------------------------------------------------------------------- *)
4059
let kind_to_json (k : EcLoader.kind) =
4160
match k with
4261
| `Ec -> `String "ec"
@@ -71,9 +90,9 @@ let ecoroot_to_map (ecor : ecoroot) : (string * Json.t) list =
7190
"digest", digest_to_json ecor.eco_digest ]
7291

7392
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; }
93+
let eco_kind = kind_of_json (Mstr.find_exn InvalidEco "kind" data) in
94+
let eco_digest = digest_of_json (Mstr.find_exn InvalidEco "digest" data) in
95+
{ eco_kind; eco_digest; }
7796

7897
(* -------------------------------------------------------------------- *)
7998
let ecoroot_to_json (ecor : ecoroot) : Json.t =
@@ -86,6 +105,43 @@ let ecoroot_of_json (data : Json.t) : ecoroot =
86105

87106
| _ -> raise InvalidEco
88107

108+
(* -------------------------------------------------------------------- *)
109+
let trace_to_json (trace : ecotrace option) : Json.t =
110+
match trace with
111+
| None ->
112+
`Null
113+
114+
| Some trace ->
115+
let for1 ((position, { goal; messages; })) =
116+
`Assoc [
117+
("position", `Int position);
118+
("goal" , `String goal);
119+
("messages", `String messages);
120+
]
121+
in `List (List.map for1 trace)
122+
123+
let trace_of_json (data : Json.t) : ecotrace option =
124+
match data with
125+
| `Null ->
126+
None
127+
128+
| `List data ->
129+
let for1 (data : Json.t) =
130+
match data with
131+
| `Assoc data ->
132+
let data = Mstr.of_list data in
133+
let position = Mstr.find_exn InvalidEco "position" data |> int_of_json in
134+
let goal = Mstr.find_exn InvalidEco "goal" data |> string_of_json in
135+
let messages = Mstr.find_exn InvalidEco "messages" data |> string_of_json in
136+
(position, { goal; messages; })
137+
| _ ->
138+
raise InvalidEco
139+
140+
in Some (List.map for1 data)
141+
142+
| _ ->
143+
raise InvalidEco
144+
89145
(* -------------------------------------------------------------------- *)
90146
let ecodepend_to_json ((ecor, direct) : ecodepend) : Json.t =
91147
`Assoc ([ "direct", flag_to_json direct] @ (ecoroot_to_map ecor))
@@ -119,6 +175,7 @@ let to_json (eco : eco) : Json.t =
119175
[ "version", `Int Version.current;
120176
"echash" , `String EcVersion.hash;
121177
"root" , ecoroot_to_json eco.eco_root;
178+
"trace" , trace_to_json eco.eco_trace;
122179
"depends", `Assoc depends ]
123180

124181
(* -------------------------------------------------------------------- *)
@@ -135,10 +192,11 @@ let of_json (data : Json.t) : eco =
135192
if echash <> `String EcVersion.hash then
136193
raise InvalidEco;
137194

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
195+
let eco_root = ecoroot_of_json (Mstr.find_exn InvalidEco "root" data) in
196+
let eco_depends = depends_of_json (Mstr.find_exn InvalidEco "depends" data) in
197+
let eco_trace = trace_of_json (Mstr.find_exn InvalidEco "trace" data) in
140198

141-
{ eco_root = root; eco_depends = depends; }
199+
{ eco_root; eco_depends; eco_trace; }
142200

143201
| _ -> raise InvalidEco
144202

src/ecOptions.ml

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

2930
and cli_option = {
@@ -341,6 +342,7 @@ let specs = {
341342
`Spec ("tstats" , `String, "Save timing statistics to <file>");
342343
`Spec ("script" , `Flag , "Computer-friendly output");
343344
`Spec ("no-eco" , `Flag , "Do not cache verification results");
345+
`Spec ("trace" , `Flag , "Save all goals & messages in .eco");
344346
`Spec ("compact", `Int , "<internal>")]);
345347

346348
("cli", "Run EasyCrypt top-level", [
@@ -506,7 +508,8 @@ let cmp_options_of_values ini values input =
506508
cmpo_compact = get_int "compact" values;
507509
cmpo_tstats = get_string "tstats" values;
508510
cmpo_noeco = get_flag "no-eco" values;
509-
cmpo_script = get_flag "script" values; }
511+
cmpo_script = get_flag "script" values;
512+
cmpo_trace = get_flag "trace" values; }
510513

511514
let runtest_options_of_values ini values (input, scenarios) =
512515
{ runo_input = input;

src/ecOptions.mli

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ and cmp_option = {
2020
cmpo_tstats : string option;
2121
cmpo_noeco : bool;
2222
cmpo_script : bool;
23+
cmpo_trace : bool;
2324
}
2425

2526
and cli_option = {

0 commit comments

Comments
 (0)