Share stats printing, improve Soteria.Terminal

soteria-c/bin/soteria_c.ml

@@ -40,6 +40,7 @@ module Exec_main = struct
       $ Soteria.Logs.Cli.term
       $ Soteria.Terminal.Config.cmdliner_term ()
       $ Soteria.Solvers.Config.cmdliner_term ()
+      $ Soteria.Stats.Config.cmdliner_term ()
       $ Soteria_c_lib.Config.cmdliner_term ()
       $ Soteria.Symex.Fuel_gauge.Cli.term ~default:Driver.default_wpst_fuel ()
       $ includes_arg
@@ -98,6 +99,7 @@ module Generate_summaries = struct
       $ Soteria.Logs.Cli.term
       $ Soteria.Terminal.Config.cmdliner_term ()
       $ Soteria.Solvers.Config.cmdliner_term ()
+      $ Soteria.Stats.Config.cmdliner_term ()
       $ Soteria_c_lib.Config.cmdliner_term ()
       $ includes_arg
       $ functions_arg
@@ -127,6 +129,7 @@ module Capture_db = struct
       $ Soteria.Logs.Cli.term
       $ Soteria.Terminal.Config.cmdliner_term ()
       $ Soteria.Solvers.Config.cmdliner_term ()
+      $ Soteria.Stats.Config.cmdliner_term ()
       $ Soteria_c_lib.Config.cmdliner_term ()
       $ compilation_db_arg
       $ functions_arg)

soteria-c/lib/config.ml

@@ -9,10 +9,6 @@ type t = {
       [@names [ "auto-include-path" ]]
       [@env "SOTERIA_AUTO_INCLUDE_PATH"]
       (** Path to the directory that contains the soteria-c.h *)
-  dump_stats_file : string option;
-      [@docv "FILE"] [@names [ "dump-stats" ]] [@env "SOTERIA_DUMP_STATS"]
-      (** Dump a json file with unsupported features and their number of
-          occurences *)
   no_ignore_parse_failures : bool;
       [@make.default false]
       [@names [ "no-ignore-parse-failures" ]]

soteria-c/lib/driver.ml

@@ -13,11 +13,6 @@ let tool_error msg =
 let with_tool_errors_caught () f =
   try f () with Tool_error -> Error.Exit_code.Tool_error
 
-let dump_stats stats =
-  match (Config.current ()).dump_stats_file with
-  | None -> ()
-  | Some file -> Csymex.Stats.dump stats file
-
 let default_wpst_fuel =
   Soteria.Symex.Fuel_gauge.{ steps = Finite 150; branching = Finite 4 }
 
@@ -292,10 +287,11 @@ let generate_errors content =
 (** {2 Entry points} *)
 
 (* Helper for all main entry points *)
-let initialise ?log_config ?term_config ?solver_config config f =
+let initialise ?log_config ?term_config ?solver_config ?stats_config config f =
   Option.iter Soteria.Logs.Config.check_set_and_lock log_config;
   Option.iter Soteria.Terminal.Config.set_and_lock term_config;
   Option.iter Soteria.Solvers.Config.set solver_config;
+  Option.iter Soteria.Stats.Config.set_and_lock stats_config;
   Config.with_config ~config f
 
 let print_states result =
@@ -312,15 +308,17 @@ let print_states result =
     result.res
 
 (* Entry point function *)
-let exec_and_print log_config term_config solver_config config fuel includes
-    file_names entry_point : Error.Exit_code.t =
+let exec_and_print log_config term_config solver_config stats_config config fuel
+    includes file_names entry_point : Error.Exit_code.t =
   (* The following line is not set as an initialiser so that it is executed before initialising z3 *)
   let fuel = Soteria.Symex.Fuel_gauge.Cli.validate_or_exit fuel in
-  let@ () = initialise ~log_config ~term_config ~solver_config config in
+  let@ () =
+    initialise ~log_config ~term_config ~solver_config ~stats_config config
+  in
   let result = exec_function ~includes ~fuel file_names entry_point in
   if (Config.current ()).parse_only then Error.Exit_code.Success
   else (
-    dump_stats result.stats;
+    Csymex.Stats.output result.stats;
     if (Config.current ()).print_states then print_states result;
     let errors_to_signal =
       List.filter_map
@@ -402,7 +400,7 @@ let generate_summaries ~functions_to_analyse prog =
   let { Soteria.Stats.res; stats } =
     Abductor.generate_all_summaries ~functions_to_analyse prog
   in
-  dump_stats stats;
+  Csymex.Stats.output stats;
   let results = analyse_summaries res in
   dump_summaries results;
   Fmt.pr "@\n@?";
@@ -447,12 +445,14 @@ let show_ail log_config term_config config (includes : string list)
       Error.Exit_code.Tool_error
 
 (* Entry point function *)
-let generate_all_summaries log_config term_config solver_config config includes
-    functions_to_analyse file_names =
+let generate_all_summaries log_config term_config solver_config stats_config
+    config includes functions_to_analyse file_names =
   (* TODO: generate a compilation database directly, to simplify the interface in this file. *)
   let@ () = with_tool_errors_caught () in
   let functions_to_analyse = as_nonempty_list functions_to_analyse in
-  let@ () = initialise ~log_config ~term_config ~solver_config config in
+  let@ () =
+    initialise ~log_config ~term_config ~solver_config ~stats_config config
+  in
   let prog =
     let@ () = L.with_section "Parsing and Linking" in
     parse_and_link_ail ~includes file_names
@@ -464,12 +464,14 @@ let generate_all_summaries log_config term_config solver_config config includes
   else generate_summaries ~functions_to_analyse prog
 
 (* Entry point function *)
-let capture_db log_config term_config solver_config config json_file
-    functions_to_analyse =
+let capture_db log_config term_config solver_config stats_config config
+    json_file functions_to_analyse =
   let open Syntaxes.Result in
   let@ () = with_tool_errors_caught () in
   let functions_to_analyse = as_nonempty_list functions_to_analyse in
-  let@ () = initialise ~log_config ~term_config ~solver_config config in
+  let@ () =
+    initialise ~log_config ~term_config ~solver_config ~stats_config config
+  in
   let linked_prog =
     let@ () = L.with_section "Parsing and Linking from database" in
     let db = Compilation_database.from_file json_file in

soteria-linear/parser/lexer.mll

@@ -16,11 +16,11 @@ rule read = parse
   | "if" { IF }
   | "then" { THEN }
   | "else" { ELSE }
-  | "take" { TAKE }
-  | "requires" { REQUIRES }
-  | "ensures" { ENSURES }
-  | "RW" { RW }
-  | "Freed" { FREED }
+  (* | "take" { TAKE } *)
+  (* | "requires" { REQUIRES } *)
+  (* | "ensures" { ENSURES } *)
+  (* | "RW" { RW } *)
+  (* | "Freed" { FREED } *)
   | "true" { TRUE }
   | "false" { FALSE }
   | "nondet" { NONDET }

soteria-linear/parser/parser.mly

@@ -8,8 +8,9 @@
 %token PLUS MINUS TIMES DIV AND OR EQ EQEQ LT
 %token LBRACK RBRACK ASSIGN SEMI LPAREN RPAREN COMMA
 %token LET IN IF THEN ELSE
-%token TAKE RW FREED TRUE FALSE NONDET ALLOC FREE
-%token REQUIRES ENSURES
+// %token TAKE RW FREED
+%token TRUE FALSE NONDET ALLOC FREE
+// %token REQUIRES ENSURES
 %token EOF
 
 %start <Program.t> program

soteria-rust/lib/charon_util.ml

@@ -173,9 +173,11 @@ let pp_span_data ft ({ file; beg_loc; end_loc } : Meta.span_data) =
     | Local name -> Fmt.string ft (clean_filename name)
     | Virtual name -> Fmt.pf ft "%s (virtual)" (clean_filename name)
   in
-  if beg_loc.line = end_loc.line then
-    Fmt.pf ft "%a:%d:%d-%d" pp_filename file beg_loc.line beg_loc.col
-      end_loc.col
-  else
-    Fmt.pf ft "%a:%d:%d-%d:%d" pp_filename file beg_loc.line beg_loc.col
-      end_loc.line end_loc.col
+  let pp_range ft ((start, stop) : Meta.loc * Meta.loc) =
+    if start.line = stop.line then
+      Fmt.pf ft "%d:%d-%d" start.line start.col stop.col
+    else Fmt.pf ft "%d:%d-%d:%d" start.line start.col stop.line stop.col
+  in
+  Fmt.pf ft "%a:%a" pp_filename file
+    (Soteria.Terminal.Printers.pp_unstable ~name:"range" pp_range)
+    (beg_loc, end_loc)

soteria-rust/lib/config.ml

@@ -11,7 +11,8 @@ type t = {
   (*
      Compilation flags
    *)
-  cleanup : bool; [@make.default false] [@names [ "clean" ]]
+  cleanup : bool;
+      [@make.default false] [@names [ "clean" ]] [@env "SOTERIA_RUST_CLEANUP"]
       (** Clean up compiled files after execution *)
   log_compilation : bool; [@make.default false] [@names [ "log-compilation" ]]
       (** Log the compilation process *)
@@ -20,6 +21,10 @@ type t = {
   no_compile_plugins : bool;
       [@make.default false] [@names [ "no-compile-plugins" ]]
       (** Do not compile the plugins, as they are already compiled *)
+  plugin_directory : string option;
+      [@names [ "plugins" ]] [@env "SOTERIA_RUST_PLUGINS"]
+      (** The directory in which plugins are and should be compiled; defaults to
+          the current dune-managed site. *)
   target : string option; [@names [ "target" ]] [@env "TARGET"]
       (** The compilation target triple to use, e.g. x86_64-unknown-linux-gnu.
           If not provided, the default target for the current machine is used.
@@ -49,14 +54,9 @@ type t = {
       (** Filter the entrypoints to run, by name. If empty, all entrypoints are
           run. Multiple filters can be provided; tests matching any will be
           selected. The filters are treated as regexes. *)
-  no_timing : bool; [@make.default false] [@names [ "no-timing" ]]
-      (** Do not display execution times *)
   print_summary : bool; [@make.default false] [@names [ "summary" ]]
       (** If a summary of all test cases should be printed at the end of
           execution *)
-  print_stats : bool; [@make.default false] [@names [ "stats" ]]
-      (** If statistics about the execution should be printed at the end of each
-          test *)
   (*
      Symbolic execution behaviour
    *)
@@ -86,7 +86,8 @@ type global = {
       [@term Soteria.Terminal.Config.cmdliner_term ()]
   solver : Soteria.Solvers.Config.t;
       [@term Soteria.Solvers.Config.cmdliner_term ()]
-  rusteria : t; [@term term]
+  stats : Soteria.Stats.Config.t; [@term Soteria.Stats.Config.cmdliner_term ()]
+  soteria_rust : t; [@term term]
 }
 [@@deriving make, subliner]
 
@@ -98,4 +99,5 @@ let set (config : global) =
   Soteria.Solvers.Config.set config.solver;
   Soteria.Logs.Config.check_set_and_lock config.logs;
   Soteria.Terminal.Config.set_and_lock config.terminal;
-  current := config.rusteria
+  Soteria.Stats.Config.set_and_lock config.stats;
+  current := config.soteria_rust

soteria-rust/lib/driver.ml

@@ -31,12 +31,7 @@ module Outcome = struct
     | Fatal -> Color.pp_clr `Yellow ft "unknown"
 end
 
-let pp_branches ft n = Fmt.pf ft "%i branch%s" n (if n = 1 then "" else "es")
-
-let pp_time ft t =
-  if !Config.current.no_timing then Fmt.pf ft "<time>"
-  else if t < 0.05 then Fmt.pf ft "%ams" (Fmt.float_dfrac 2) (t *. 1000.)
-  else Fmt.pf ft "%as" (Fmt.float_dfrac 2) t
+let pp_branches = Printers.pp_plural ~sing:"branch" ~plur:"branches"
 
 let print_pcs pcs =
   let open Fmt in
@@ -58,7 +53,8 @@ let print_outcomes entry_name f =
       let time = Unix.gettimeofday () -. time in
       Fmt.kstr
         (Diagnostic.print_diagnostic_simple ~severity:Note)
-        "%s: done in %a, ran %a" entry_name pp_time time pp_branches ntotal;
+        "%s: done in %a, ran %a" entry_name Printers.pp_time time pp_branches
+        ntotal;
       print_pcs pcs;
       Fmt.pr "@.@.";
       (entry_name, Outcome.Ok)
@@ -70,8 +66,8 @@ let print_outcomes entry_name f =
       in
       Fmt.kstr
         (Diagnostic.print_diagnostic_simple ~severity:Error)
-        "%s: found issues in %a, errors in %a (out of %d)" entry_name pp_time
-        time pp_branches err_branches ntotal;
+        "%s: found issues in %a, errors in %a (out of %d)" entry_name
+        Printers.pp_time time pp_branches err_branches ntotal;
       Fmt.pr "@.";
       let () =
         let@ error, call_trace, pcs = Fun.flip List.iter errs in
@@ -93,7 +89,7 @@ let print_outcomes entry_name f =
       in
       Fmt.kstr
         (Diagnostic.print_diagnostic_simple ~severity:Warning)
-        "%s (%a): %s, %s@.@." entry_name pp_time time error msg;
+        "%s (%a): %s, %s@.@." entry_name Printers.pp_time time error msg;
       (entry_name, Outcome.Fatal)
 
 let print_outcomes_summary outcomes =
@@ -103,31 +99,6 @@ let print_outcomes_summary outcomes =
     (list ~sep:(any "@\n") pp_outcome)
     outcomes
 
-let print_stats (stats : 'a Stats.stats) =
-  let open Fmt in
-  let entries =
-    [
-      ("Steps", fun ft () -> int ft stats.steps_number);
-      ("Branches", fun ft () -> int ft stats.branch_number);
-      ("Total time", fun ft () -> pp_time ft stats.exec_time);
-      ( "Execution time",
-        fun ft () ->
-          Fmt.pf ft "%a (%a%%)" pp_time
-            (stats.exec_time -. stats.sat_time)
-            (float_dfrac 2)
-            (100. *. (stats.exec_time -. stats.sat_time) /. stats.exec_time) );
-      ( "Solver time",
-        fun ft () ->
-          Fmt.pf ft "%a (%a%%)" pp_time stats.sat_time (float_dfrac 2)
-            (100. *. stats.sat_time /. stats.exec_time) );
-      ("SAT checks", fun ft () -> int ft stats.sat_checks);
-    ]
-  in
-  let pp_entry ft (name, pp_value) = Fmt.pf ft " • %s: %a" name pp_value () in
-  pr "%a:@\n%a@\n" (pp_style `Bold) "Statistics"
-    (list ~sep:(any "@\n") pp_entry)
-    entries
-
 let exec_crate
     ( (crate : Charon.UllbcAst.crate),
       (entry_points : 'fuel Frontend.entry_point list) ) =
@@ -151,7 +122,7 @@ let exec_crate
     @@ exec_fun entry.fun_decl
   in
 
-  if !Config.current.print_stats then print_stats stats;
+  Rustsymex.Stats.output stats;
 
   (* inverse ok and errors if we expect a failure *)
   let nbranches = List.length branches in
@@ -209,7 +180,7 @@ let wrap_step name f =
     let time = Unix.gettimeofday () in
     let res = f () in
     let time = Unix.gettimeofday () -. time in
-    Fmt.pr " done in %a@." pp_time time;
+    Fmt.pr " done in %a@." Printers.pp_time time;
     res
   with e ->
     let bt = Printexc.get_raw_backtrace () in

soteria-rust/lib/frontend.ml

@@ -187,7 +187,7 @@ module Lib = struct
 
   let root =
     lazy
-      (match Sys.getenv_opt "RUSTERIA_PLUGINS" with
+      (match !Config.current.plugin_directory with
       | Some root -> root
       | None -> List.hd Runtime_sites.Sites.plugins)
 

soteria-rust/test/cram/cargo.t/run.t

@@ -1,5 +1,5 @@
 Test running Rusteria on a crate
-  $ soteria-rust cargo . --clean --no-timing
+  $ soteria-rust cargo .
   Compiling... done in <time>
   note: tests::tests::my_test: done in <time>, ran 2 branches
   PC 1: (V|1| == 0x01) /\ (V|1| == 0x01)

soteria-rust/test/cram/dune

@@ -1,3 +1,9 @@
+(env
+ (_
+  (env-vars
+   (HIDE_UNSTABLE 1)
+   (SOTERIA_RUST_CLEANUP 1))))
+
 (cram
  (deps ../../bin/soteria_rust.exe)
  (applies_to :whole_subtree))