From fc85993092d96f2c51cc80799ad254df3ab486d3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 27 Oct 2022 09:47:14 +0200 Subject: Rename driver.ml to Driver.ml --- compiler/driver.ml | 208 ----------------------------------------------------- 1 file changed, 208 deletions(-) delete mode 100644 compiler/driver.ml (limited to 'compiler/driver.ml') diff --git a/compiler/driver.ml b/compiler/driver.ml deleted file mode 100644 index ae9d238a..00000000 --- a/compiler/driver.ml +++ /dev/null @@ -1,208 +0,0 @@ -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))) -- cgit v1.2.3