From e1f79b07440f35e5e6296b61819cf50e6f60f090 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 26 Oct 2022 17:31:24 +0200 Subject: Start generating documentation --- Makefile | 17 +++- aeneas.opam | 29 +++++++ dune-project | 23 ++++++ src/PrintSymbolicAst.ml | 59 -------------- src/driver.ml | 208 ++++++++++++++++++++++++++++++++++++++++++++++++ src/dune | 27 ++++++- src/main.ml | 205 ----------------------------------------------- 7 files changed, 298 insertions(+), 270 deletions(-) create mode 100644 aeneas.opam delete mode 100644 src/PrintSymbolicAst.ml create mode 100644 src/driver.ml delete mode 100644 src/main.ml diff --git a/Makefile b/Makefile index c59aec01..3b822802 100644 --- a/Makefile +++ b/Makefile @@ -14,6 +14,8 @@ CHARON_TESTS_DIR = CHARON_OPTIONS = CHARON_TESTS_SRC = +AENEAS_DRIVER = src/driver.exe + # The user can specify additional translation options for Aeneas: OPTIONS ?= @@ -29,8 +31,15 @@ build-tests-verify: build tests verify # Build the project .PHONY: build -build: - dune build src/main.exe +build: build-driver build-lib + +.PHONY: build-driver +build-driver: + dune build $(AENEAS_DRIVER) + +.PHONY: build-lib +build-lib: + dune build src/aeneas.cmxs # Test the project by translating test files to F* .PHONY: tests @@ -91,10 +100,10 @@ trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc trans-polonius-%: gen-llbc-polonius-% - dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) + dune exec -- $(AENEAS_DRIVER) $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) trans-%: gen-llbc-% - dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) + dune exec -- $(AENEAS_DRIVER) $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) .PHONY: doc doc: diff --git a/aeneas.opam b/aeneas.opam new file mode 100644 index 00000000..4048f9a0 --- /dev/null +++ b/aeneas.opam @@ -0,0 +1,29 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "0.1" +synopsis: "" +description: "" +maintainer: ["son.ho@inria.fr"] +authors: ["Son Ho" "Jonathan Protzenko" "Aymeric Fromherz" "Sidney Congard"] +license: "Apache-2.0" +homepage: "https://github.com/AeneasVerif/aeneas" +bug-reports: "https://github.com/AeneasVerif/aeneas/issues" +depends: [ + "dune" {>= "2.8"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/AeneasVerif/aeneas.git" diff --git a/dune-project b/dune-project index c2e46604..f8b418f2 100644 --- a/dune-project +++ b/dune-project @@ -1 +1,24 @@ (lang dune 2.8) + +(name aeneas) + +(version 0.1) + +(generate_opam_files true) + +(formatting) + +(source + (uri git+https://github.com/AeneasVerif/aeneas.git)) + +(homepage "https://github.com/AeneasVerif/aeneas") + +(bug_reports "https://github.com/AeneasVerif/aeneas/issues") + +(authors + "Son Ho" + "Jonathan Protzenko" + "Aymeric Fromherz" + "Sidney Congard") + +(license Apache-2.0) \ No newline at end of file diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml deleted file mode 100644 index 37b7555e..00000000 --- a/src/PrintSymbolicAst.ml +++ /dev/null @@ -1,59 +0,0 @@ -(** Printing utilities for symbolic AST. - - We don't put this in [Print] because: - - [Print] is getting quite big - - if we do so we have a dependency cycle... - *) - -open Errors -open Identifiers -open FunIdentifier -module T = Types -module TU = TypesUtils -module V = Values -module E = Expressions -module A = LlbcAst -module C = Contexts -open SymbolicAst -module P = Print -module PT = Print.Types - -type formatting_ctx = { - type_context : C.type_context; - fun_context : A.fun_decl FunDeclId.Map.t; - type_vars : T.type_var list; -} - -type formatter = P.Values.value_formatter - -let formatting_ctx_to_formatter (ctx : formatting_ctx) : formatter = - (* We shouldn't use [rvar_to_string] *) - let rvar_to_string _ = failwith "Unexpected use of rvar_to_string" in - let r_to_string r = PT.region_id_to_string r in - - let type_var_id_to_string vid = - let v = T.TypeVarId.nth ctx.type_vars vid in - v.name - in - let type_decl_id_to_string def_id = - let def = T.TypeDeclId.Map.find def_id ctx.type_context.type_decls in - P.name_to_string def.name - in - let adt_variant_to_string = - P.Contexts.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls - in - (* We shouldn't use [var_id_to_string] *) - let var_id_to_string _ = failwith "Unexpected use of var_id_to_string" in - - let adt_field_names = - P.Contexts.type_ctx_to_adt_field_names_fun ctx.type_context.type_decls - in - { - rvar_to_string; - r_to_string; - type_var_id_to_string; - type_decl_id_to_string; - adt_variant_to_string; - var_id_to_string; - adt_field_names; - } diff --git a/src/driver.ml b/src/driver.ml new file mode 100644 index 00000000..ae9d238a --- /dev/null +++ b/src/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/src/dune b/src/dune index ccf726c9..e8b53fc5 100644 --- a/src/dune +++ b/src/dune @@ -1,10 +1,33 @@ ;; core: for Core.Unix.mkdir_p (executable - (name main) + (name driver) + (public_name aeneas_driver) + (package aeneas) (preprocess (pps ppx_deriving.show ppx_deriving.ord visitors.ppx)) - (libraries ppx_deriving yojson zarith easy_logging core_unix)) + (libraries ppx_deriving yojson zarith easy_logging core_unix aeneas) + (modules driver)) + +(library + (name aeneas) ;; The name as used in the project + (public_name aeneas) ;; The name as revealed to the projects importing this library + (preprocess + (pps ppx_deriving.show ppx_deriving.ord visitors.ppx)) + (libraries ppx_deriving yojson zarith easy_logging core_unix) + (modules Assumed Collections ConstStrings Contexts Cps Crates Errors + Expressions ExpressionsUtils ExtractToFStar FunsAnalysis Identifiers + InterpreterBorrowsCore InterpreterBorrows InterpreterExpansion + InterpreterExpressions Interpreter InterpreterPaths InterpreterProjectors + InterpreterStatements InterpreterUtils Invariants LlbcAst LlbcAstUtils + LlbcOfJson Logging Meta Names OfJsonBasic PrePasses Print PrintPure + PureMicroPasses Pure PureToExtract PureTypeCheck PureUtils Scalars + StringUtils Substitute SymbolicAst SymbolicToPure SynthesizeSymbolic + TranslateCore Translate TypesAnalysis Types TypesUtils Utils Values + ValuesUtils)) + +(documentation + (package aeneas)) (env (dev diff --git a/src/main.ml b/src/main.ml deleted file mode 100644 index 05e96af9..00000000 --- a/src/main.ml +++ /dev/null @@ -1,205 +0,0 @@ -open LlbcOfJson -open Logging -open Print -module T = Types -module A = LlbcAst -module I = Interpreter -module EL = Easy_logging.Logging -module TA = TypesAnalysis -module Micro = PureMicroPasses - -(* 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