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 +++++++++++++++++++++++++++++++++++++++++++++++++++++ compiler/driver.ml | 208 ----------------------------------------------------- compiler/dune | 2 +- 3 files changed, 209 insertions(+), 209 deletions(-) create mode 100644 compiler/Driver.ml delete mode 100644 compiler/driver.ml (limited to 'compiler') 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))) 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))) diff --git a/compiler/dune b/compiler/dune index e8b53fc5..0968b2be 100644 --- a/compiler/dune +++ b/compiler/dune @@ -7,7 +7,7 @@ (preprocess (pps ppx_deriving.show ppx_deriving.ord visitors.ppx)) (libraries ppx_deriving yojson zarith easy_logging core_unix aeneas) - (modules driver)) + (modules Driver)) (library (name aeneas) ;; The name as used in the project -- cgit v1.2.3