Save init data when compiling + sorted outputs (#304)

* Save init data when compiling files * Sort output in `act` command * Sort specs in command --------- Co-authored-by: Nat Karmios <[email protected]>
GillianPlatform · Aug 3, 2024 · 8f15618 · 8f15618
1 parent c6cc0e4
commit 8f15618
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 8 deletions.
diff --git a/Gillian-C/lib/global_env.ml b/Gillian-C/lib/global_env.ml
@@ -89,6 +89,11 @@ module Serialization = struct
 end
 
 let of_yojson json =
+  let json =
+    match json with
+    | `Null -> `List []
+    | _ -> json
+  in
   Result.map Serialization.of_definition_list
     ([%of_yojson: Serialization.entry list] json)
 

diff --git a/GillianCore/command_line/command_line.ml b/GillianCore/command_line/command_line.ml
@@ -55,7 +55,7 @@ struct
 
     let consoles : (module Console.S) list =
       [
-        (module Compiler_console.Make (PC));
+        (module Compiler_console.Make (ID) (PC));
         (module C_interpreter_console.Make (ID) (PC) (CState) (C_interpreter)
                   (Gil_parsing));
         (module S_interpreter_console.Make (ID) (PC) (SState) (S_interpreter)

diff --git a/GillianCore/command_line/compiler_console.ml b/GillianCore/command_line/compiler_console.ml
@@ -1,6 +1,9 @@
 open Cmdliner
+open Command_line_utils
 
-module Make (PC : ParserAndCompiler.S) : Console.S = struct
+module Make
+    (ID : Init_data.S)
+    (PC : ParserAndCompiler.S with type init_data = ID.t) : Console.S = struct
   open Common_args.Make (PC)
 
   let mode =
@@ -24,8 +27,10 @@ module Make (PC : ParserAndCompiler.S) : Console.S = struct
       ParserAndCompiler.get_progs_or_fail ~pp_err:PC.pp_err
         (PC.parse_and_compile_files files)
     in
-    List.iter
-      (fun (path, prog) -> Io_utils.save_file_pp path Prog.pp_labeled prog)
+    List.iteri
+      (fun i (path, prog) ->
+        let init_data = if i = 0 then ID.to_yojson progs.init_data else `Null in
+        burn_gil ~init_data ~pp_prog:Prog.pp_labeled prog (Some path))
       progs.gil_progs
 
   let compile files mode runtime_path ci tl_opts =

diff --git a/GillianCore/engine/BiAbduction/Abductor.ml b/GillianCore/engine/BiAbduction/Abductor.ml
@@ -324,7 +324,8 @@ module Make
     in
     let result = run_tests_aux tests [] [] [] 1 in
     Fmt.pr "\nTest results:\nProc, GIL Commands, Tests, Succs, Bugs, Time\n";
-    !stats |> List.rev
+    !stats
+    |> List.sort (fun (name1, _) (name2, _) -> String.compare name1 name2)
     |> List.iter (fun (name, stats) ->
            Fmt.pr "%s, %a\n" name pp_proc_stats stats);
     Fmt.pr "@?";
@@ -335,20 +336,25 @@ module Make
       (succ_specs : Spec.t list)
       (error_specs : Spec.t list)
       (bug_specs : Spec.t list) =
+    let sort_specs =
+      List.sort
+        (fun Spec.{ spec_name = name1; _ } Spec.{ spec_name = name2; _ } ->
+          String.compare name1 name2)
+    in
     let bug_specs_txt =
       Format.asprintf "@[<v 2>BUG SPECS:@\n%a@]@\n"
         Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds))
-        bug_specs
+        (sort_specs bug_specs)
     in
     let error_specs_txt =
       Format.asprintf "@[<v 2>ERROR SPECS:@\n%a@]@\n"
         Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds))
-        error_specs
+        (sort_specs error_specs)
     in
     let normal_specs_txt =
       Format.asprintf "@[<v 2>SUCCESSFUL SPECS:@\n%a@]@\n"
         Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds))
-        succ_specs
+        (sort_specs succ_specs)
     in
 
     if !Config.specs_to_stdout then (