1 files changed, 208 insertions, 0 deletions
diff --git a/compiler/driver.ml b/compiler/driver.ml
new file mode 100644
index 00000000..ae9d238a
--- /dev/null
+++ b/compiler/driver.ml
@@ -0,0 +1,208 @@
+open Aeneas.LlbcOfJson
+open Aeneas.Logging
+open Aeneas.Print
+module T = Aeneas.Types
+module A = Aeneas.LlbcAst
+module I = Aeneas.Interpreter
+module EL = Easy_logging.Logging
+module TA = Aeneas.TypesAnalysis
+module Micro = Aeneas.PureMicroPasses
+module Print = Aeneas.Print
+module PrePasses = Aeneas.PrePasses
+module Translate = Aeneas.Translate
+
+(* This is necessary to have a backtrace when raising exceptions - for some
+ * reason, the -g option doesn't work.
+ * TODO: run with OCAMLRUNPARAM=b=1? *)
+let () = Printexc.record_backtrace true
+
+let usage =
+  Printf.sprintf
+    {|Aeneas: verification of Rust programs by translation to pure lambda calculus
+
+Usage: %s [OPTIONS] FILE
+|}
+    Sys.argv.(0)
+
+let () =
+  (* Measure start time *)
+  let start_time = Unix.gettimeofday () in
+
+  (* Read the command line arguments *)
+  let dest_dir = ref "" in
+  let decompose_monads = ref false in
+  let unfold_monads = ref true in
+  let filter_useless_calls = ref true in
+  let filter_useless_functions = ref true in
+  let test_units = ref false in
+  let test_trans_units = ref false in
+  let no_decreases_clauses = ref false in
+  let no_state = ref false in
+  let template_decreases_clauses = ref false in
+  let no_split_files = ref false in
+  let no_check_inv = ref false in
+
+  let spec =
+    [
+      ("-dest", Arg.Set_string dest_dir, " Specify the output directory");
+      ( "-decompose-monads",
+        Arg.Set decompose_monads,
+        " Decompose the monadic let-bindings.\n\n\
+        \         Introduces a temporary variable which is later decomposed,\n\
+        \         when the pattern on the left of the monadic let is not a \n\
+        \         variable.\n\
+        \         \n\
+        \         Example:\n\
+        \         `(x, y) <-- f (); ...` ~~>\n\
+        \         `tmp <-- f (); let (x, y) = tmp in ...`\n\
+        \        " );
+      ( "-unfold-monads",
+        Arg.Set unfold_monads,
+        " Unfold the monadic let-bindings to matches" );
+      ( "-filter-useless-calls",
+        Arg.Set filter_useless_calls,
+        " Filter the useless function calls, when possible" );
+      ( "-filter-useless-funs",
+        Arg.Set filter_useless_functions,
+        " Filter the useless forward/backward functions" );
+      ( "-test-units",
+        Arg.Set test_units,
+        " Test the unit functions with the concrete interpreter" );
+      ( "-test-trans-units",
+        Arg.Set test_trans_units,
+        " Test the translated unit functions with the target theorem\n\
+        \                         prover's normalizer" );
+      ( "-no-decreases-clauses",
+        Arg.Set no_decreases_clauses,
+        " Do not add decrease clauses to the recursive definitions" );
+      ( "-no-state",
+        Arg.Set no_state,
+        " Do not use state-error monads, simply use error monads" );
+      ( "-template-clauses",
+        Arg.Set template_decreases_clauses,
+        " Generate templates for the required decreases clauses, in a\n\
+        \                         dedicated file. Incompatible with \
+         -no-decreases-clauses" );
+      ( "-no-split-files",
+        Arg.Set no_split_files,
+        " Don't split the definitions between different files for types,\n\
+        \                         functions, etc." );
+      ( "-no-check-inv",
+        Arg.Set no_check_inv,
+        " Deactivate the invariant sanity checks performed at every step of\n\
+        \                         evaluation. Dramatically saves speed." );
+    ]
+  in
+  (* Sanity check: -template-clauses ==> not -no-decrease-clauses *)
+  assert ((not !no_decreases_clauses) || not !template_decreases_clauses);
+
+  let spec = Arg.align spec in
+  let filenames = ref [] in
+  let add_filename f = filenames := f :: !filenames in
+  Arg.parse spec add_filename usage;
+  let fail () =
+    print_string usage;
+    exit 1
+  in
+  (* Retrieve and check the filename *)
+  let filename =
+    match !filenames with
+    | [ f ] ->
+        (* TODO: update the extension *)
+        if not (Filename.check_suffix f ".llbc") then (
+          print_string "Unrecognized file extension";
+          fail ())
+        else if not (Sys.file_exists f) then (
+          print_string "File not found";
+          fail ())
+        else f
+    | _ ->
+        (* For now, we only process one file at a time *)
+        print_string usage;
+        exit 1
+  in
+  (* Check the destination directory *)
+  let dest_dir =
+    if !dest_dir = "" then Filename.dirname filename else !dest_dir
+  in
+
+  (* Set up the logging - for now we use default values - TODO: use the
+   * command-line arguments *)
+  (* By setting a level for the main_logger_handler, we filter everything *)
+  Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
+  main_log#set_level EL.Info;
+  llbc_of_json_logger#set_level EL.Info;
+  pre_passes_log#set_level EL.Info;
+  interpreter_log#set_level EL.Info;
+  statements_log#set_level EL.Info;
+  paths_log#set_level EL.Info;
+  expressions_log#set_level EL.Info;
+  expansion_log#set_level EL.Info;
+  borrows_log#set_level EL.Info;
+  invariants_log#set_level EL.Info;
+  pure_utils_log#set_level EL.Info;
+  symbolic_to_pure_log#set_level EL.Info;
+  pure_micro_passes_log#set_level EL.Info;
+  pure_to_extract_log#set_level EL.Info;
+  translate_log#set_level EL.Info;
+
+  (* Load the module *)
+  let json = Yojson.Basic.from_file filename in
+  match llbc_crate_of_json json with
+  | Error s ->
+      main_log#error "error: %s\n" s;
+      exit 1
+  | Ok m ->
+      (* Logging *)
+      main_log#linfo (lazy ("Imported: " ^ filename));
+      main_log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
+
+      (* Apply the pre-passes *)
+      let m = PrePasses.apply_passes m in
+
+      (* Some options for the execution *)
+      let eval_config =
+        {
+          C.check_invariants = not !no_check_inv;
+          greedy_expand_symbolics_with_borrows = true;
+          allow_bottom_below_borrow = true;
+          return_unit_end_abs_with_no_loans = true;
+        }
+      in
+
+      (* Test the unit functions with the concrete interpreter *)
+      if !test_units then I.Test.test_unit_functions eval_config m;
+
+      (* Evaluate the symbolic interpreter on the functions, ignoring the
+       * functions which contain loops - TODO: remove *)
+      let synthesize = true in
+      I.Test.test_functions_symbolic eval_config synthesize m;
+
+      (* Translate the functions *)
+      let test_unit_functions = !test_trans_units in
+      let micro_passes_config =
+        {
+          Micro.decompose_monadic_let_bindings = !decompose_monads;
+          unfold_monadic_let_bindings = !unfold_monads;
+          filter_useless_monadic_calls = !filter_useless_calls;
+          filter_useless_functions = !filter_useless_functions;
+        }
+      in
+      let trans_config =
+        {
+          Translate.eval_config;
+          mp_config = micro_passes_config;
+          split_files = not !no_split_files;
+          test_unit_functions;
+          extract_decreases_clauses = not !no_decreases_clauses;
+          extract_template_decreases_clauses = !template_decreases_clauses;
+          use_state = not !no_state;
+        }
+      in
+      Translate.translate_module filename dest_dir trans_config m;
+
+      (* Print total elapsed time *)
+      log#linfo
+        (lazy
+          (Printf.sprintf "Total execution time: %f seconds"
+             (Unix.gettimeofday () -. start_time)))