diff options
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | compiler/Config.ml | 192 | ||||
| -rw-r--r-- | compiler/Contexts.ml | 55 | ||||
| -rw-r--r-- | compiler/Driver.ml | 84 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 28 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 18 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.mli | 3 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 48 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.mli | 10 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 18 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 19 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 89 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 158 | ||||
| -rw-r--r-- | compiler/Translate.ml | 151 | ||||
| -rw-r--r-- | compiler/dune | 1 |
17 files changed, 392 insertions, 496 deletions
@@ -17,7 +17,7 @@ CHARON_TESTS_SRC = AENEAS_DRIVER = driver.exe # The user can specify additional translation options for Aeneas: -OPTIONS ?= +OPTIONS += -unfold-monads # Default translation options: # - insert calls to the normalizer in the translated code to test the @@ -75,7 +75,7 @@ AENEAS_CMD = cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DI # Add specific options to some tests trans-no_nested_borrows trans-paper: \ - TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses + TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses trans-no_nested_borrows trans-paper: SUBDIR:=misc trans-hashmap: TRANS_OPTIONS += -template-clauses -no-state @@ -84,10 +84,10 @@ trans-hashmap: SUBDIR:=hashmap trans-hashmap_main: TRANS_OPTIONS += -template-clauses trans-hashmap_main: SUBDIR:=hashmap_on_disk -trans-polonius-betree_polonius: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses +trans-polonius-betree_polonius: TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses trans-polonius-betree_polonius: SUBDIR:=misc -trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses +trans-constants: TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses trans-constants: SUBDIR:=misc trans-external: TRANS_OPTIONS += diff --git a/compiler/Config.ml b/compiler/Config.ml new file mode 100644 index 00000000..f446872c --- /dev/null +++ b/compiler/Config.ml @@ -0,0 +1,192 @@ +(** Define the global configuration options *) + +(** {0 Interpreter} *) + +(** Check that invariants are maintained whenever we execute a statement *) +let check_invariants = ref true + +(** Expand all symbolic values containing borrows upon introduction - allows + to use restrict ourselves to a simpler model for the projectors over + symbolic values. + The interpreter fails if doing this requires to do a branching (because + we need to expand an enumeration with strictly more than one variant) + or if we need to expand a recursive type (because this leads to looping). + *) +let greedy_expand_symbolics_with_borrows = true + +(** Experimental. + + TODO: remove (always true now) + + We sometimes want to temporarily break the invariant that there is no + bottom value below a borrow. If this value is true, we don't check + the invariant, and the rule becomes: we can't end a borrow *if* it contains + a bottom value. The consequence is that it becomes ok to temporarily + have bottom below a borrow, if we put something else inside before ending + the borrow. + + For instance, when evaluating an assignment, we move the value which + will be overwritten then do some administrative tasks with the borrows, + then move the rvalue to its destination. We currently want to be able + to check the invariants every time we end a borrow/an abstraction, + meaning at intermediate steps of the assignment where the invariants + might actually be broken. + *) +let allow_bottom_below_borrow = true + +(** If a function doesn't return any borrows, we can immediately call + its backward functions. If this option is on, whenever we call a + function *and* this function returns unit, we immediately end all the + abstractions which are introduced and don't contain loans. This can be + useful to make the code cleaner (the backward function is introduced + where the function call happened) and make sure all forward functions + with no return value are followed by a backward function. + *) +let return_unit_end_abs_with_no_loans = true + +(** {0 Translation} *) + +(** Controls whether we need to use a state to model the external world + (I/O, for instance). + *) +let use_state = ref true (* TODO *) + +(** Controls whether backward functions update the state, in case we use + a state ({!use_state}). + + If they update the state, we generate code of the following style: + {[ + (st1, y) <-- f_fwd x st0; // st0 is the state upon calling f_fwd + ... + (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back + }] + + Otherwise, we generate code of the following shape: + {[ + (st1, y) <-- f_fwd x st0; + ... + x' <-- f_back x st0 y'; + }] + + The second format is easier to reason about, but the first one is + necessary to properly handle some Rust functions which use internal + mutability such as {{:https://doc.rust-lang.org/std/cell/struct.RefCell.html#method.try_borrow_mut} [RefCell::try_mut_borrow]}: + in order to model this behaviour we would need a state, and calling the backward + function would update the state by reinserting the updated value in it. + *) +let backward_no_state_update = ref false + +(** Controls whether we split the generated definitions between different + files for the types, clauses and functions, or if we group them in + one file. + *) +let split_files = ref true + +(** If true, treat the unit functions (function taking no inputs and returning + no outputs) as unit tests: evaluate them with the interpreter and check that + they don't panic. + *) +let test_unit_functions = ref false + +(** If true, insert tests in the generated files to check that the + unit functions normalize to [Success _]. + + For instance, in F* it generates code like this: + {[ + let _ = assert_norm (FUNCTION () = Success ()) + ]} + *) +let test_trans_unit_functions = ref false + +(** If [true], insert [decreases] clauses for all the recursive definitions. + + The body of such clauses must be defined by the user. + *) +let extract_decreases_clauses = ref true + +(** In order to help the user, we can generate "template" decrease clauses + (i.e., definitions with proper signatures but dummy bodies) in a + dedicated file. + *) +let extract_template_decreases_clauses = ref false + +(** {0 Micro passes} *) + +(** Some provers like F* don't support the decomposition of return values + in monadic let-bindings: + {[ + // NOT supported in F* + let (x, y) <-- f (); + ... + ]} + + In such situations, we might want to introduce an intermediate + assignment: + {[ + let tmp <-- f (); + let (x, y) = tmp in + ... + ]} + *) +let decompose_monadic_let_bindings = ref false + +(** Controls the unfolding of monadic let-bindings to explicit matches: + + [y <-- f x; ...] + + becomes: + + [match f x with | Failure -> Failure | Return y -> ...] + + + This is useful when extracting to F*: the support for monadic + definitions is not super powerful. + Note that when {!field:unfold_monadic_let_bindings} is true, setting + {!field:decompose_monadic_let_bindings} to true and only makes the code + more verbose. + *) +let unfold_monadic_let_bindings = ref false + +(** Controls whether we try to filter the calls to monadic functions + (which can fail) when their outputs are not used. + + The useless calls are calls to backward functions which have no outputs. + This case happens if the original Rust function only takes *shared* borrows + as inputs, and is thus pretty common. + + We are allowed to do this only because in this specific case, + the backward function fails *exactly* when the forward function fails + (they actually do exactly the same thing, the only difference being + that the forward function can potentially return a value), and upon + reaching the place where we should introduce a call to the backward + function, we know we have introduced a call to the forward function. + + Also note that in general, backward functions "do more things" than + forward functions, and have more opportunities to fail (even though + in the generated code, calls to the backward functions should fail + exactly when the corresponding, previous call to the forward functions + failed). + + This optimization is done in {!SymbolicToPure}. We might want to move it to + the micro-passes subsequent to the translation from symbolic to pure, but it + is really super easy to do it when going from symbolic to pure. Note that + we later filter the useless *forward* calls in the micro-passes, where it is + more natural to do. + + See the comments for {!expression_contains_child_call_in_all_paths} + for additional explanations. + *) +let filter_useless_monadic_calls = ref true + +(** If {!filter_useless_monadic_calls} is activated, some functions + become useless: if this option is true, we don't extract them. + + The calls to functions which always get filtered are: + - the forward functions with unit return value + - the backward functions which don't output anything (backward + functions coming from rust functions with no mutable borrows + as input values - note that if a function doesn't take mutable + borrows as inputs, it can't return mutable borrows; we actually + dynamically check for that). + *) +let filter_useless_functions = ref true diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index 0c72392b..96749f07 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -182,63 +182,10 @@ type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show] type config = { mode : interpreter_mode; (** Concrete mode (interpreter) or symbolic mode (for synthesis) **) - check_invariants : bool; - (** Check that invariants are maintained whenever we execute a statement *) - greedy_expand_symbolics_with_borrows : bool; - (** Expand all symbolic values containing borrows upon introduction - allows - to use restrict ourselves to a simpler model for the projectors over - symbolic values. - The interpreter fails if doing this requires to do a branching (because - we need to expand an enumeration with strictly more than one variant) - or if we need to expand a recursive type (because this leads to looping). - *) - allow_bottom_below_borrow : bool; - (** Experimental. - - We sometimes want to temporarily break the invariant that there is no - bottom value below a borrow. If this value is true, we don't check - the invariant, and the rule becomes: we can't end a borrow *if* it contains - a bottom value. The consequence is that it becomes ok to temporarily - have bottom below a borrow, if we put something else inside before ending - the borrow. - - For instance, when evaluating an assignment, we move the value which - will be overwritten then do some administrative tasks with the borrows, - then move the rvalue to its destination. We currently want to be able - to check the invariants every time we end a borrow/an abstraction, - meaning at intermediate steps of the assignment where the invariants - might actually be broken. - *) - return_unit_end_abs_with_no_loans : bool; - (** If a function doesn't return any borrows, we can immediately call - its backward functions. If this option is on, whenever we call a - function *and* this function returns unit, we immediately end all the - abstractions which are introduced and don't contain loans. This can be - useful to make the code cleaner (the backward function is introduced - where the function call happened) and make sure all forward functions - with no return value are followed by a backward function. - *) } [@@deriving show] -(** See {!config} *) -type partial_config = { - check_invariants : bool; - greedy_expand_symbolics_with_borrows : bool; - allow_bottom_below_borrow : bool; - return_unit_end_abs_with_no_loans : bool; -} - -let config_of_partial (mode : interpreter_mode) (config : partial_config) : - config = - { - mode; - check_invariants = config.check_invariants; - greedy_expand_symbolics_with_borrows = - config.greedy_expand_symbolics_with_borrows; - allow_bottom_below_borrow = config.allow_bottom_below_borrow; - return_unit_end_abs_with_no_loans = config.return_unit_end_abs_with_no_loans; - } +let mk_config (mode : interpreter_mode) : config = { mode } type type_context = { type_decls_groups : type_declaration_group TypeDeclId.Map.t; diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 6f0e8074..304d0f2f 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -1,6 +1,5 @@ open Aeneas.LlbcOfJson open Aeneas.Logging -open Aeneas.Print module T = Aeneas.Types module A = Aeneas.LlbcAst module I = Aeneas.Interpreter @@ -10,6 +9,7 @@ module Micro = Aeneas.PureMicroPasses module Print = Aeneas.Print module PrePasses = Aeneas.PrePasses module Translate = Aeneas.Translate +open Aeneas.Config (* This is necessary to have a backtrace when raising exceptions - for some * reason, the -g option doesn't work. @@ -30,25 +30,12 @@ let () = (* 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 - (* [backward_no_state_update]: see the comment for {!Translate.config.backward_no_state_update} *) - let backward_no_state_update = 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, + Arg.Set decompose_monadic_let_bindings, " 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\ @@ -59,49 +46,49 @@ let () = \ `tmp <-- f (); let (x, y) = tmp in ...`\n\ \ " ); ( "-unfold-monads", - Arg.Set unfold_monads, + Arg.Set unfold_monadic_let_bindings, " 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" ); + ( "-no-filter-useless-calls", + Arg.Clear filter_useless_monadic_calls, + " Do not filter the useless function calls, when possible" ); + ( "-no-filter-useless-funs", + Arg.Clear filter_useless_functions, + " Do not filter the useless forward/backward functions" ); ( "-test-units", - Arg.Set test_units, + Arg.Set test_unit_functions, " Test the unit functions with the concrete interpreter" ); ( "-test-trans-units", - Arg.Set test_trans_units, + Arg.Set test_trans_unit_functions, " Test the translated unit functions with the target theorem\n\ \ prover's normalizer" ); ( "-no-decreases-clauses", - Arg.Set no_decreases_clauses, + Arg.Clear extract_decreases_clauses, " Do not add decrease clauses to the recursive definitions" ); ( "-no-state", - Arg.Set no_state, + Arg.Clear use_state, " Do not use state-error monads, simply use error monads" ); ( "-backward-no-state-update", Arg.Set backward_no_state_update, " Forbid backward functions from updating the state" ); ( "-template-clauses", - Arg.Set template_decreases_clauses, + Arg.Set extract_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, + Arg.Clear split_files, " Don't split the definitions between different files for types,\n\ \ functions, etc." ); ( "-no-check-inv", - Arg.Set no_check_inv, + Arg.Clear check_invariants, " 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); + assert (!extract_decreases_clauses || not !extract_template_decreases_clauses); (* Sanity check: -backward-no-state-update ==> not -no-state *) - assert ((not !backward_no_state_update) || not !no_state); + assert ((not !backward_no_state_update) || !use_state); let spec = Arg.align spec in let filenames = ref [] in @@ -169,46 +156,17 @@ let () = 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; + if !test_unit_functions then I.Test.test_unit_functions 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; + I.Test.test_functions_symbolic 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; - backward_no_state_update = !backward_no_state_update; - } - in - Translate.translate_module filename dest_dir trans_config m; + Translate.translate_module filename dest_dir m; (* Print total elapsed time *) log#linfo diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index e752594e..f776c7ff 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -208,7 +208,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return for the synthesis) - the symbolic AST generated by the symbolic execution *) -let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) +let evaluate_function_symbolic (synthesize : bool) (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context) (fdef : A.fun_decl) (back_id : T.RegionGroupId.id option) : @@ -229,7 +229,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) in (* Create the continuation to finish the evaluation *) - let config = C.config_of_partial C.SymbolicMode config in + let config = C.mk_config C.SymbolicMode in let cf_finish res ctx = match res with | Return -> @@ -284,8 +284,7 @@ module Test = struct (** Test a unit function (taking no arguments) by evaluating it in an empty environment. *) - let test_unit_function (config : C.partial_config) (crate : A.crate) - (fid : A.FunDeclId.id) : unit = + let test_unit_function (crate : A.crate) (fid : A.FunDeclId.id) : unit = (* Retrieve the function declaration *) let fdef = A.FunDeclId.nth crate.functions fid in let body = Option.get fdef.body in @@ -311,7 +310,7 @@ module Test = struct let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in (* Create the continuation to check the function's result *) - let config = C.config_of_partial C.ConcreteMode config in + let config = C.mk_config C.ConcreteMode in let cf_check res ctx = match res with | Return -> @@ -340,24 +339,24 @@ module Test = struct && List.length def.A.signature.inputs = 0 (** Test all the unit functions in a list of function definitions *) - let test_unit_functions (config : C.partial_config) (crate : A.crate) : unit = + let test_unit_functions (crate : A.crate) : unit = let unit_funs = List.filter fun_decl_is_transparent_unit crate.functions in let test_unit_fun (def : A.fun_decl) : unit = - test_unit_function config crate def.A.def_id + test_unit_function crate def.A.def_id in List.iter test_unit_fun unit_funs (** Execute the symbolic interpreter on a function. *) - let test_function_symbolic (config : C.partial_config) (synthesize : bool) - (type_context : C.type_context) (fun_context : C.fun_context) - (global_context : C.global_context) (fdef : A.fun_decl) : unit = + let test_function_symbolic (synthesize : bool) (type_context : C.type_context) + (fun_context : C.fun_context) (global_context : C.global_context) + (fdef : A.fun_decl) : unit = (* Debug *) log#ldebug (lazy ("test_function_symbolic: " ^ Print.fun_name_to_string fdef.A.name)); (* Evaluate *) let evaluate = - evaluate_function_symbolic config synthesize type_context fun_context + evaluate_function_symbolic synthesize type_context fun_context global_context fdef in (* Execute the forward function *) @@ -380,8 +379,7 @@ module Test = struct TODO: for now we ignore the functions which contain loops, because they are not supported by the symbolic interpreter. *) - let test_functions_symbolic (config : C.partial_config) (synthesize : bool) - (crate : A.crate) : unit = + let test_functions_symbolic (synthesize : bool) (crate : A.crate) : unit = (* Filter the functions which contain loops *) let no_loop_funs = List.filter @@ -397,8 +395,8 @@ module Test = struct (* Execute the function - note that as the symbolic interpreter explores * all the path, some executions are expected to "panic": we thus don't * check the return value *) - test_function_symbolic config synthesize type_context fun_context - global_context def + test_function_symbolic synthesize type_context fun_context global_context + def in List.iter test_fun no_loop_funs end diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 585db0eb..3d8ca3bf 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -853,7 +853,7 @@ let rec end_borrow_aux (config : C.config) (chain : borrow_or_abs_ids) (* The complete sanity check: also check that after we ended a borrow, * the invariant is preserved *) let cf_check : cm_fun = - comp cf_check_disappeared (Invariants.cf_check_invariants config) + comp cf_check_disappeared Invariants.cf_check_invariants in (* Start by ending the borrow itself (we lookup it up and replace it with [Bottom] *) @@ -1011,7 +1011,7 @@ and end_abstraction_aux (config : C.config) (chain : borrow_or_abs_ids) in (* Sanity check: ending an abstraction must preserve the invariants *) - let cc = comp cc (Invariants.cf_check_invariants config) in + let cc = comp cc Invariants.cf_check_invariants in (* Apply the continuation *) cc cf ctx diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index fe9ccbf4..40c32ccc 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -719,7 +719,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = let greedy_expand_symbolic_values (config : C.config) : cm_fun = fun cf ctx -> - if config.greedy_expand_symbolics_with_borrows then ( + if Config.greedy_expand_symbolics_with_borrows then ( log#ldebug (lazy "greedy_expand_symbolic_values"); greedy_expand_symbolics_with_borrows config cf ctx) else cf ctx diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index a0fb97d1..5bc440e7 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -34,7 +34,7 @@ let expand_primitively_copyable_at_place (config : C.config) (* Small helper *) let rec expand : cm_fun = fun cf ctx -> - let v = read_place config access p ctx in + let v = read_place access p ctx in match find_first_primitively_copyable_sv_with_borrows ctx.type_context.type_infos v @@ -55,10 +55,10 @@ let expand_primitively_copyable_at_place (config : C.config) We also check that the value *doesn't contain bottoms or reserved borrows*. *) -let read_place (config : C.config) (access : access_kind) (p : E.place) +let read_place (access : access_kind) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> - let v = read_place config access p ctx in + let v = read_place access p ctx in (* Check that there are no bottoms in the value *) assert (not (bottom_in_value ctx.ended_regions v)); (* Check that there are no reserved borrows in the value *) @@ -82,7 +82,7 @@ let access_rplace_reorganize_and_read (config : C.config) else cc in (* Read the place - note that this checks that the value doesn't contain bottoms *) - let read_place = read_place config access p in + let read_place = read_place access p in (* Compose *) comp cc read_place cf ctx @@ -263,7 +263,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) | Expressions.Copy p -> (* Access the value *) let access = Read in - let cc = read_place config access p in + let cc = read_place access p in (* Copy the value *) let copy cf v : m_fun = fun ctx -> @@ -284,14 +284,14 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) | Expressions.Move p -> (* Access the value *) let access = Move in - let cc = read_place config access p in + let cc = read_place access p in (* Move the value *) let move cf v : m_fun = fun ctx -> (* Check that there are no bottoms in the value we are about to move *) assert (not (bottom_in_value ctx.ended_regions v)); let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in - let ctx = write_place config access p bottom ctx in + let ctx = write_place access p bottom ctx in cf v ctx in (* Compose and apply *) @@ -575,7 +575,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) ({ v with V.value = v' }, v) in (* Update the borrowed value in the context *) - let ctx = write_place config access p nv ctx in + let ctx = write_place access p nv ctx in (* Compute the rvalue - simply a shared borrow with a the fresh id. * Note that the reference is *mutable* if we do a two-phase borrow *) let rv_ty = @@ -610,7 +610,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) (* Compute the value with which to replace the value at place p *) let nv = { v with V.value = V.Loan (V.MutLoan bid) } in (* Update the value in the context *) - let ctx = write_place config access p nv ctx in + let ctx = write_place access p nv ctx in (* Continue *) cf rv ctx in diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli index 2ea3c6df..a268ed1f 100644 --- a/compiler/InterpreterExpressions.mli +++ b/compiler/InterpreterExpressions.mli @@ -19,8 +19,7 @@ open InterpreterPaths This function doesn't reorganize the context to make sure we can read the place. If needs be, you should call {!update_ctx_along_read_place} first. *) -val read_place : - C.config -> access_kind -> E.place -> (V.typed_value -> m_fun) -> m_fun +val read_place : access_kind -> E.place -> (V.typed_value -> m_fun) -> m_fun (** Auxiliary function. diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 63e03e31..1e1401df 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -310,8 +310,8 @@ let access_kind_to_projection_access (access : access_kind) : projection_access Note that we only access the value at the place, and do not check that the value is "well-formed" (for instance that it doesn't contain bottoms). *) -let try_read_place (config : C.config) (access : access_kind) (p : E.place) - (ctx : C.eval_ctx) : V.typed_value path_access_result = +let try_read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) : + V.typed_value path_access_result = let access = access_kind_to_projection_access access in (* The update function is the identity *) let update v = v in @@ -321,7 +321,7 @@ let try_read_place (config : C.config) (access : access_kind) (p : E.place) (* Note that we ignore the new environment: it should be the same as the original one. *) - if config.check_invariants then + if !Config.check_invariants then if ctx1 <> ctx then ( let msg = "Unexpected environment update:\nNew environment:\n" @@ -332,15 +332,15 @@ let try_read_place (config : C.config) (access : access_kind) (p : E.place) raise (Failure "Unexpected environment update")); Ok read_value -let read_place (config : C.config) (access : access_kind) (p : E.place) - (ctx : C.eval_ctx) : V.typed_value = - match try_read_place config access p ctx with +let read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) : + V.typed_value = + match try_read_place access p ctx with | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e)) | Ok v -> v (** Attempt to update the value at a given place *) -let try_write_place (_config : C.config) (access : access_kind) (p : E.place) - (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx path_access_result = +let try_write_place (access : access_kind) (p : E.place) (nv : V.typed_value) + (ctx : C.eval_ctx) : C.eval_ctx path_access_result = let access = access_kind_to_projection_access access in (* The update function substitutes the value with the new value *) let update _ = nv in @@ -350,9 +350,9 @@ let try_write_place (_config : C.config) (access : access_kind) (p : E.place) (* We ignore the read value *) Ok ctx -let write_place (config : C.config) (access : access_kind) (p : E.place) - (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx = - match try_write_place config access p nv ctx with +let write_place (access : access_kind) (p : E.place) (nv : V.typed_value) + (ctx : C.eval_ctx) : C.eval_ctx = + match try_write_place access p nv ctx with | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e)) | Ok ctx -> ctx @@ -417,9 +417,9 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) : about which variant we should project to, which is why we *can* set the variant index when writing one of its fields). *) -let expand_bottom_value_from_projection (config : C.config) - (access : access_kind) (p : E.place) (remaining_pes : int) - (pe : E.projection_elem) (ty : T.ety) (ctx : C.eval_ctx) : C.eval_ctx = +let expand_bottom_value_from_projection (access : access_kind) (p : E.place) + (remaining_pes : int) (pe : E.projection_elem) (ty : T.ety) + (ctx : C.eval_ctx) : C.eval_ctx = (* Debugging *) log#ldebug (lazy @@ -464,7 +464,7 @@ let expand_bottom_value_from_projection (config : C.config) ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty)) in (* Update the context by inserting the expanded value at the proper place *) - match try_write_place config access p' nv ctx with + match try_write_place access p' nv ctx with | Ok ctx -> ctx | Error _ -> raise (Failure "Unreachable") @@ -472,7 +472,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind) (p : E.place) : cm_fun = fun cf ctx -> (* Attempt to read the place: if it fails, update the environment and retry *) - match try_read_place config access p ctx with + match try_read_place access p ctx with | Ok _ -> cf ctx | Error err -> let cc = @@ -501,7 +501,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind) fun cf ctx -> (* Attempt to *read* (yes, *read*: we check the access to the place, and write to it later) the place: if it fails, update the environment and retry *) - match try_read_place config access p ctx with + match try_read_place access p ctx with | Ok _ -> cf ctx | Error err -> (* Update the context *) @@ -518,8 +518,8 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind) (* Expand the {!V.Bottom} value *) fun cf ctx -> let ctx = - expand_bottom_value_from_projection config access p remaining_pes - pe ty ctx + expand_bottom_value_from_projection access p remaining_pes pe ty + ctx in cf ctx | FailBorrow _ -> raise (Failure "Could not write to a borrow") @@ -569,7 +569,7 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) in (* First, retrieve the value *) - let v = read_place config access p ctx in + let v = read_place access p ctx in (* Inspect the value and update the context while doing so. If the context gets updated: perform a recursive call (many things may have been updated in the context: we need to re-read the value @@ -590,8 +590,8 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun = (* Move the current value in the place outside of this place and into * a dummy variable *) let access = Write in - let v = read_place config access p ctx in - let ctx = write_place config access p (mk_bottom v.V.ty) ctx in + let v = read_place access p ctx in + let ctx = write_place access p (mk_bottom v.V.ty) ctx in let dummy_id = C.fresh_dummy_var_id () in let ctx = C.ctx_push_dummy_var ctx dummy_id v in (* Auxiliary function *) @@ -624,7 +624,7 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun = (* Pop *) let ctx, v = C.ctx_remove_dummy_var ctx dummy_id in (* Reinsert *) - let ctx = write_place config access p v ctx in + let ctx = write_place access p v ctx in (* Sanity check *) assert (not (outer_loans_in_value v)); (* Continue *) @@ -648,7 +648,7 @@ let prepare_lplace (config : C.config) (p : E.place) (* Read the value and check it *) let read_check cf : m_fun = fun ctx -> - let v = read_place config access p ctx in + let v = read_place access p ctx in (* Sanity checks *) assert (not (outer_loans_in_value v)); (* Continue *) diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli index 14baf128..6e9286cd 100644 --- a/compiler/InterpreterPaths.mli +++ b/compiler/InterpreterPaths.mli @@ -33,8 +33,7 @@ val update_ctx_along_write_place : C.config -> access_kind -> E.place -> cm_fun Note that we only access the value at the place, and do not check that the value is "well-formed" (for instance that it doesn't contain bottoms). *) -val read_place : - C.config -> access_kind -> E.place -> C.eval_ctx -> V.typed_value +val read_place : access_kind -> E.place -> C.eval_ctx -> V.typed_value (** Update the value at a given place. @@ -46,12 +45,7 @@ val read_place : overwrite it. *) val write_place : - C.config -> - access_kind -> - E.place -> - V.typed_value -> - C.eval_ctx -> - C.eval_ctx + access_kind -> E.place -> V.typed_value -> C.eval_ctx -> C.eval_ctx (** Compute an expanded tuple ⊥ value. diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 15962ee3..14dd59b1 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -39,12 +39,12 @@ let drop_value (config : C.config) (p : E.place) : cm_fun = let replace cf (v : V.typed_value) ctx = (* Move the value at destination (that we will overwrite) to a dummy variable * to preserve the borrows it may contain *) - let mv = InterpreterPaths.read_place config access p ctx in + let mv = InterpreterPaths.read_place access p ctx in let dummy_id = C.fresh_dummy_var_id () in let ctx = C.ctx_push_dummy_var ctx dummy_id mv in (* Update the destination to ⊥ *) let nv = { v with value = V.Bottom } in - let ctx = write_place config access p nv ctx in + let ctx = write_place access p nv ctx in log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n" @@ -119,14 +119,14 @@ let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) : fun ctx -> (* Move the value at destination (that we will overwrite) to a dummy variable * to preserve the borrows *) - let mv = InterpreterPaths.read_place config Write p ctx in + let mv = InterpreterPaths.read_place Write p ctx in let dest_vid = C.fresh_dummy_var_id () in let ctx = C.ctx_push_dummy_var ctx dest_vid mv in (* Write to the destination *) (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) assert (not (bottom_in_value ctx.ended_regions rv)); (* Update the destination *) - let ctx = write_place config Write p rv ctx in + let ctx = write_place Write p rv ctx in (* Debug *) log#ldebug (lazy @@ -540,9 +540,7 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list) match (region_params, type_params, args) with | [], [ boxed_ty ], [ E.Move input_box_place ] -> (* Required type checking *) - let input_box = - InterpreterPaths.read_place config Write input_box_place ctx - in + let input_box = InterpreterPaths.read_place Write input_box_place ctx in (let input_ty = ty_get_box input_box.V.ty in assert (input_ty = boxed_ty)); @@ -783,7 +781,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = * checking the invariants *) let cc = greedy_expand_symbolic_values config in (* Sanity check *) - let cc = comp cc (Inv.cf_check_invariants config) in + let cc = comp cc Inv.cf_check_invariants in (* Evaluate *) let cf_eval_st cf : m_fun = @@ -1279,7 +1277,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) * (see the documentation of {!config} for more information) *) let cc = - if config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output + if Config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output then comp cc end_abs_with_no_loans else cc in @@ -1382,7 +1380,7 @@ and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun = * checking the invariants *) let cc = greedy_expand_symbolic_values config in (* Sanity check *) - let cc = comp_check_ctx cc (Inv.check_invariants config) in + let cc = comp_check_ctx cc Inv.check_invariants in (* Continue *) cc (cf res) in diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index ead064a4..9bd6b78b 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -301,15 +301,14 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = - borrows/loans can't contain ⊥ or reserved mut borrows - shared loans can't contain mutable loans *) -let check_borrowed_values_invariant (config : C.config) (ctx : C.eval_ctx) : - unit = +let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = let visitor = object inherit [_] C.iter_eval_ctx as super method! visit_Bottom info = (* No ⊥ inside borrowed values *) - assert (config.C.allow_bottom_below_borrow || not info.outer_borrow) + assert (Config.allow_bottom_below_borrow || not info.outer_borrow) method! visit_ABottom _info = (* ⊥ inside an abstraction is not the same as in a regular value *) @@ -672,7 +671,7 @@ type sv_info = { - the union of the aproj_loans contains the aproj_borrows applied on the same symbolic values *) -let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit = +let check_symbolic_values (ctx : C.eval_ctx) : unit = (* Small utility *) let module M = V.SymbolicValueId.Map in let infos : sv_info M.t ref = ref M.empty in @@ -781,17 +780,17 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit = M.iter check_info !infos -let check_invariants (config : C.config) (ctx : C.eval_ctx) : unit = - if config.C.check_invariants then ( +let check_invariants (ctx : C.eval_ctx) : unit = + if !Config.check_invariants then ( log#ldebug (lazy "Checking invariants"); check_loans_borrows_relation_invariant ctx; - check_borrowed_values_invariant config ctx; + check_borrowed_values_invariant ctx; check_typing_invariant ctx; - check_symbolic_values config ctx) + check_symbolic_values ctx) else log#ldebug (lazy "Not checking invariants (check is not activated)") (** Same as {!check_invariants}, but written in CPS *) -let cf_check_invariants (config : C.config) : cm_fun = +let cf_check_invariants : cm_fun = fun cf ctx -> - check_invariants config ctx; + check_invariants ctx; cf ctx diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 9d604626..1bf3b903 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -8,64 +8,6 @@ module V = Values (** The local logger *) let log = L.pure_micro_passes_log -(** A configuration to control the application of the passes *) -type config = { - decompose_monadic_let_bindings : bool; - (** Some provers like F* don't support the decomposition of return values - in monadic let-bindings: - {[ - // NOT supported in F* - let (x, y) <-- f (); - ... - ]} - - In such situations, we might want to introduce an intermediate - assignment: - {[ - let tmp <-- f (); - let (x, y) = tmp in - ... - ]} - *) - unfold_monadic_let_bindings : bool; - (** Controls the unfolding of monadic let-bindings to explicit matches: - - [y <-- f x; ...] - - becomes: - - [match f x with | Failure -> Failure | Return y -> ...] - - - This is useful when extracting to F*: the support for monadic - definitions is not super powerful. - Note that when {!field:unfold_monadic_let_bindings} is true, setting - {!field:decompose_monadic_let_bindings} to true and only makes the code - more verbose. - *) - filter_useless_monadic_calls : bool; - (** Controls whether we try to filter the calls to monadic functions - (which can fail) when their outputs are not used. - - See the comments for {!expression_contains_child_call_in_all_paths} - for additional explanations. - - TODO: rename to {!filter_useless_monadic_calls} - *) - filter_useless_functions : bool; - (** If {!filter_useless_monadic_calls} is activated, some functions - become useless: if this option is true, we don't extract them. - - The calls to functions which always get filtered are: - - the forward functions with unit return value - - the backward functions which don't output anything (backward - functions coming from rust functions with no mutable borrows - as input values - note that if a function doesn't take mutable - borrows as inputs, it can't return mutable borrows; we actually - dynamically check for that). - *) -} - (** Small utility. We sometimes have to insert new fresh variables in a function body, in which @@ -1003,10 +945,10 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl = symbolic to pure. Here, we remove the definitions altogether, because they are now useless *) -let filter_if_backward_with_no_outputs (config : config) (def : fun_decl) : - fun_decl option = +let filter_if_backward_with_no_outputs (def : fun_decl) : fun_decl option = if - config.filter_useless_functions && Option.is_some def.back_id + !Config.filter_useless_functions + && Option.is_some def.back_id && def.signature.output = mk_result_ty mk_unit_ty then None else Some def @@ -1027,12 +969,12 @@ let filter_if_backward_with_no_outputs (config : config) (def : fun_decl) : In such situation, we can remove the forward function definition altogether. *) -let keep_forward (config : config) (trans : pure_fun_translation) : bool = +let keep_forward (trans : pure_fun_translation) : bool = let fwd, backs = trans in (* Note that at this point, the output types are no longer seen as tuples: * they should be lists of length 1. *) if - config.filter_useless_functions + !Config.filter_useless_functions && fwd.signature.output = mk_result_ty mk_unit_ty && backs <> [] then false @@ -1141,7 +1083,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = (** Decompose the monadic let-bindings. - See the explanations in [config]. + See the explanations in {!config.decompose_monadic_let_bindings} *) let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl = @@ -1243,8 +1185,7 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl = [ctx]: used only for printing. *) -let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) : - fun_decl option = +let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl option = (* Debug *) log#ldebug (lazy @@ -1274,7 +1215,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) : * Note that the calls to those functions should already have been removed, * when translating from symbolic to pure. Here, we remove the definitions * altogether, because they are now useless *) - let def = filter_if_backward_with_no_outputs config def in + let def = filter_if_backward_with_no_outputs def in match def with | None -> None @@ -1304,7 +1245,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) : ("eliminate_box_functions:\n\n" ^ fun_decl_to_string ctx def ^ "\n")); (* Filter the useless variables, assignments, function calls, etc. *) - let def = filter_useless config.filter_useless_monadic_calls ctx def in + let def = filter_useless !Config.filter_useless_monadic_calls ctx def in log#ldebug (lazy ("filter_useless:\n\n" ^ fun_decl_to_string ctx def ^ "\n")); @@ -1323,7 +1264,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) : (* Decompose the monadic let-bindings - F* specific * TODO: remove? *) let def = - if config.decompose_monadic_let_bindings then ( + if !Config.decompose_monadic_let_bindings then ( let def = decompose_monadic_let_bindings ctx def in log#ldebug (lazy @@ -1339,7 +1280,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) : (* Unfold the monadic let-bindings *) let def = - if config.unfold_monadic_let_bindings then ( + if !Config.unfold_monadic_let_bindings then ( let def = unfold_monadic_let_bindings ctx def in log#ldebug (lazy @@ -1365,12 +1306,12 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) : because this function contains useful information to extract the backward functions: keeping it is not necessary but more convenient. *) -let apply_passes_to_pure_fun_translation (config : config) (ctx : trans_ctx) +let apply_passes_to_pure_fun_translation (ctx : trans_ctx) (trans : pure_fun_translation) : bool * pure_fun_translation = (* Apply the passes to the individual functions *) let forward, backwards = trans in - let forward = Option.get (apply_passes_to_def config ctx forward) in - let backwards = List.filter_map (apply_passes_to_def config ctx) backwards in + let forward = Option.get (apply_passes_to_def ctx forward) in + let backwards = List.filter_map (apply_passes_to_def ctx) backwards in let trans = (forward, backwards) in (* Compute whether we need to filter the forward function or not *) - (keep_forward config trans, trans) + (keep_forward trans, trans) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 9d249cfb..74bc20ae 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -12,45 +12,6 @@ module FA = FunsAnalysis (** The local logger *) let log = L.symbolic_to_pure_log -(* TODO: carrying configurations everywhere is super annoying. - Group everything in references in a [Config.ml] file (put aside the execution - mode, maybe). -*) -type config = { - filter_useless_back_calls : bool; - (** If [true], filter the useless calls to backward functions. - - The useless calls are calls to backward functions which have no outputs. - This case happens if the original Rust function only takes *shared* borrows - as inputs, and is thus pretty common. - - We are allowed to do this only because in this specific case, - the backward function fails *exactly* when the forward function fails - (they actually do exactly the same thing, the only difference being - that the forward function can potentially return a value), and upon - reaching the place where we should introduce a call to the backward - function, we know we have introduced a call to the forward function. - - Also note that in general, backward functions "do more things" than - forward functions, and have more opportunities to fail (even though - in the generated code, calls to the backward functions should fail - exactly when the corresponding, previous call to the forward functions - failed). - - We might want to move this optimization to the micro-passes subsequent - to the translation from symbolic to pure, but it is really super easy - to do it when going from symbolic to pure. - Note that we later filter the useless *forward* calls in the micro-passes, - where it is more natural to do. - *) - backward_no_state_update : bool; - (** Controls whether backward functions update the state, in case we use - a state ({!use_state}). - - See {!Translate.config.backward_no_state_update}. - *) -} - type type_context = { llbc_type_decls : T.type_decl TypeDeclId.Map.t; type_decls : type_decl TypeDeclId.Map.t; @@ -528,15 +489,14 @@ let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) : [backward_no_state_update]: see {!config} *) -let get_fun_effect_info (backward_no_state_update : bool) - (fun_infos : FA.fun_info A.FunDeclId.Map.t) (fun_id : A.fun_id) - (gid : T.RegionGroupId.id option) : fun_effect_info = +let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t) + (fun_id : A.fun_id) (gid : T.RegionGroupId.id option) : fun_effect_info = match fun_id with | A.Regular fid -> let info = A.FunDeclId.Map.find fid fun_infos in let stateful_group = info.stateful in let stateful = - stateful_group && ((not backward_no_state_update) || gid = None) + stateful_group && ((not !Config.backward_no_state_update) || gid = None) in { can_fail = info.can_fail; stateful_group; stateful } | A.Assumed aid -> @@ -553,9 +513,8 @@ let get_fun_effect_info (backward_no_state_update : bool) name (outputs for backward functions come from borrows in the inputs of the forward function) which we use as hints to generate pretty names. *) -let translate_fun_sig (backward_no_state_update : bool) - (fun_infos : FA.fun_info A.FunDeclId.Map.t) (fun_id : A.fun_id) - (types_infos : TA.type_infos) (sg : A.fun_sig) +let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t) + (fun_id : A.fun_id) (types_infos : TA.type_infos) (sg : A.fun_sig) (input_names : string option list) (bid : T.RegionGroupId.id option) : fun_sig_named_outputs = (* Retrieve the list of parent backward functions *) @@ -606,20 +565,18 @@ let translate_fun_sig (backward_no_state_update : bool) List.filter_map (translate_back_ty_for_gid gid) [ sg.output ] in (* Is the function stateful, and can it fail? *) - let effect_info = - get_fun_effect_info backward_no_state_update fun_infos fun_id bid - in + let effect_info = get_fun_effect_info fun_infos fun_id bid in (* If the function is stateful, the inputs are: - forward: [fwd_ty0, ..., fwd_tyn, state] - backward: - - if config.no_backward_state: [fwd_ty0, ..., fwd_tyn, state, back_ty, state] + - if {!Config.backward_no_state_update}: [fwd_ty0, ..., fwd_tyn, state, back_ty, state] - otherwise: [fwd_ty0, ..., fwd_tyn, state, back_ty] The backward takes the same state as input as the forward function, together with the state at the point where it gets called, if it is stateful. - See the comments for {!Translate.config.backward_no_state_update} + See the comments for {!Config.backward_no_state_update} *) let fwd_state_ty = (* For the forward state, we check if the *whole group* is stateful. @@ -1134,17 +1091,16 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) : let abs_ancestors = list_ancestor_abstractions ctx abs in (call_info.forward, abs_ancestors) -let rec translate_expression (config : config) (e : S.expression) (ctx : bs_ctx) - : texpression = +let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = match e with | S.Return opt_v -> translate_return opt_v ctx | Panic -> translate_panic ctx - | FunCall (call, e) -> translate_function_call config call e ctx - | EndAbstraction (abs, e) -> translate_end_abstraction config abs e ctx - | EvalGlobal (gid, sv, e) -> translate_global_eval config gid sv e ctx - | Assertion (v, e) -> translate_assertion config v e ctx - | Expansion (p, sv, exp) -> translate_expansion config p sv exp ctx - | Meta (meta, e) -> translate_meta config meta e ctx + | FunCall (call, e) -> translate_function_call call e ctx + | EndAbstraction (abs, e) -> translate_end_abstraction abs e ctx + | EvalGlobal (gid, sv, e) -> translate_global_eval gid sv e ctx + | Assertion (v, e) -> translate_assertion v e ctx + | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx + | Meta (meta, e) -> translate_meta meta e ctx | ForwardEnd e -> (* Update the current state with the additional state received by the backward function, if needs be *) @@ -1153,7 +1109,7 @@ let rec translate_expression (config : config) (e : S.expression) (ctx : bs_ctx) | None -> ctx | Some _ -> { ctx with state_var = ctx.back_state_var } in - translate_expression config e ctx + translate_expression e ctx and translate_panic (ctx : bs_ctx) : texpression = (* Here we use the function return type - note that it is ok because @@ -1213,8 +1169,8 @@ and translate_return (opt_v : V.typed_value option) (ctx : bs_ctx) : texpression (* TODO: we should use a [Return] function *) mk_result_return_texpression output -and translate_function_call (config : config) (call : S.call) (e : S.expression) - (ctx : bs_ctx) : texpression = +and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : + texpression = (* Translate the function call *) let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in let args = @@ -1236,8 +1192,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression) (* Retrieve the effect information about this function (can fail, * takes a state as input, etc.) *) let effect_info = - get_fun_effect_info config.backward_no_state_update - ctx.fun_context.fun_infos fid None + get_fun_effect_info ctx.fun_context.fun_infos fid None in (* If the function is stateful: * - add the state input argument @@ -1306,12 +1261,12 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression) let func = { e = Qualif func; ty = func_ty } in let call = mk_apps func args in (* Translate the next expression *) - let next_e = translate_expression config e ctx in + let next_e = translate_expression e ctx in (* Put together *) mk_let effect_info.can_fail dest_v call next_e -and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) - (ctx : bs_ctx) : texpression = +and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : + texpression = log#ldebug (lazy ("translate_end_abstraction: abstraction kind: " @@ -1359,7 +1314,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) (fun (var, v) -> assert ((var : var).ty = (v : texpression).ty)) variables_values; (* Translate the next expression *) - let next_e = translate_expression config e ctx in + let next_e = translate_expression e ctx in (* Generate the assignemnts *) let monadic = false in List.fold_right @@ -1377,8 +1332,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) raise (Failure "Unreachable") in let effect_info = - get_fun_effect_info config.backward_no_state_update - ctx.fun_context.fun_infos fun_id (Some abs.back_id) + get_fun_effect_info ctx.fun_context.fun_infos fun_id (Some abs.back_id) in let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in (* Retrieve the original call and the parent abstractions *) @@ -1459,7 +1413,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) * if necessary *) let ctx, func = bs_ctx_register_backward_call abs back_inputs ctx in (* Translate the next expression *) - let next_e = translate_expression config e ctx in + let next_e = translate_expression e ctx in (* Put everything together *) let args_mplaces = List.map (fun _ -> None) inputs in let args = @@ -1479,14 +1433,15 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) * ================= * We do a small optimization here: if the backward function doesn't * have any output, we don't introduce any function call. - * See the comment in [config]. + * See the comment in {!Config.filter_useless_monadic_calls}. * * TODO: use an option to disallow backward functions from updating the state. * TODO: a backward function which only gives back shared borrows shouldn't * update the state (state updates should only be used for mutable borrows, * with objects like Rc for instance. *) - if config.filter_useless_back_calls && outputs = [] && nstate = None then ( + if !Config.filter_useless_monadic_calls && outputs = [] && nstate = None + then ( (* No outputs - we do a small sanity check: the backward function * should have exactly the same number of inputs as the forward: * this number can be different only if the forward function returned @@ -1549,7 +1504,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) assert (given_back.ty = input.ty)) given_back_inputs; (* Translate the next expression *) - let next_e = translate_expression config e ctx in + let next_e = translate_expression e ctx in (* Generate the assignments *) let monadic = false in List.fold_right @@ -1557,20 +1512,20 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) mk_let monadic given_back (mk_texpression_from_var input_var) e) given_back_inputs next_e -and translate_global_eval (config : config) (gid : A.GlobalDeclId.id) - (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) : texpression = +and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value) + (e : S.expression) (ctx : bs_ctx) : texpression = let ctx, var = fresh_var_for_symbolic_value sval ctx in let decl = A.GlobalDeclId.Map.find gid ctx.global_context.llbc_global_decls in let global_expr = { id = Global gid; type_args = [] } in (* We use translate_fwd_ty to translate the global type *) let ty = ctx_translate_fwd_ty ctx decl.ty in let gval = { e = Qualif global_expr; ty } in - let e = translate_expression config e ctx in + let e = translate_expression e ctx in mk_let false (mk_typed_pattern_from_var var None) gval e -and translate_assertion (config : config) (v : V.typed_value) (e : S.expression) - (ctx : bs_ctx) : texpression = - let next_e = translate_expression config e ctx in +and translate_assertion (v : V.typed_value) (e : S.expression) (ctx : bs_ctx) : + texpression = + let next_e = translate_expression e ctx in let monadic = true in let v = typed_value_to_texpression ctx v in let args = [ v ] in @@ -1580,8 +1535,8 @@ and translate_assertion (config : config) (v : V.typed_value) (e : S.expression) let assertion = mk_apps func args in mk_let monadic (mk_dummy_pattern mk_unit_ty) assertion next_e -and translate_expansion (config : config) (p : S.mplace option) - (sv : V.symbolic_value) (exp : S.expansion) (ctx : bs_ctx) : texpression = +and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) + (exp : S.expansion) (ctx : bs_ctx) : texpression = (* Translate the scrutinee *) let scrutinee_var = lookup_var_for_symbolic_value sv ctx in let scrutinee = mk_texpression_from_var scrutinee_var in @@ -1598,7 +1553,7 @@ and translate_expansion (config : config) (p : S.mplace option) (* The (mut/shared) borrow type is extracted to identity: we thus simply * introduce an reassignment *) let ctx, var = fresh_var_for_symbolic_value nsv ctx in - let next_e = translate_expression config e ctx in + let next_e = translate_expression e ctx in let monadic = false in mk_let monadic (mk_typed_pattern_from_var var None) @@ -1615,7 +1570,7 @@ and translate_expansion (config : config) (p : S.mplace option) (* There is exactly one branch: no branching *) let type_id, _, _ = TypesUtils.ty_as_adt sv.V.sv_ty in let ctx, vars = fresh_vars_for_symbolic_values svl ctx in - let branch = translate_expression config branch ctx in + let branch = translate_expression branch ctx in match type_id with | T.AdtId adt_id -> (* Detect if this is an enumeration or not *) @@ -1706,7 +1661,7 @@ and translate_expansion (config : config) (p : S.mplace option) in let pat_ty = scrutinee.ty in let pat = mk_adt_pattern pat_ty variant_id vars in - let branch = translate_expression config branch ctx in + let branch = translate_expression branch ctx in { pat; branch } in let branches = @@ -1727,8 +1682,8 @@ and translate_expansion (config : config) (p : S.mplace option) | ExpandBool (true_e, false_e) -> (* We don't need to update the context: we don't introduce any * new values/variables *) - let true_e = translate_expression config true_e ctx in - let false_e = translate_expression config false_e ctx in + let true_e = translate_expression true_e ctx in + let false_e = translate_expression false_e ctx in let e = Switch ( mk_opt_mplace_texpression scrutinee_mplace scrutinee, @@ -1742,12 +1697,12 @@ and translate_expansion (config : config) (p : S.mplace option) match_branch = (* We don't need to update the context: we don't introduce any * new values/variables *) - let branch = translate_expression config branch_e ctx in + let branch = translate_expression branch_e ctx in let pat = mk_typed_pattern_from_primitive_value (PV.Scalar v) in { pat; branch } in let branches = List.map translate_branch branches in - let otherwise = translate_expression config otherwise ctx in + let otherwise = translate_expression otherwise ctx in let pat_ty = Integer int_ty in let otherwise_pat : typed_pattern = { value = PatDummy; ty = pat_ty } in let otherwise : match_branch = @@ -1764,9 +1719,9 @@ and translate_expansion (config : config) (p : S.mplace option) List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches); { e; ty } -and translate_meta (config : config) (meta : S.meta) (e : S.expression) - (ctx : bs_ctx) : texpression = - let next_e = translate_expression config e ctx in +and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) : + texpression = + let next_e = translate_expression e ctx in let meta = match meta with | S.Assignment (lp, rv, rp) -> @@ -1779,8 +1734,7 @@ and translate_meta (config : config) (meta : S.meta) (e : S.expression) let ty = next_e.ty in { e; ty } -let translate_fun_decl (config : config) (ctx : bs_ctx) - (body : S.expression option) : fun_decl = +let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = (* Translate *) let def = ctx.fun_decl in let bid = ctx.bid in @@ -1802,10 +1756,9 @@ let translate_fun_decl (config : config) (ctx : bs_ctx) match body with | None -> None | Some body -> - let body = translate_expression config body ctx in + let body = translate_expression body ctx in let effect_info = - get_fun_effect_info config.backward_no_state_update - ctx.fun_context.fun_infos (Regular def_id) bid + get_fun_effect_info ctx.fun_context.fun_infos (Regular def_id) bid in (* Sanity check *) type_check_texpression ctx body; @@ -1902,8 +1855,8 @@ let translate_type_decls (type_decls : T.type_decl list) : type_decl list = - optional names for the outputs values (we derive them for the backward functions) *) -let translate_fun_signatures (backward_no_state_update : bool) - (fun_infos : FA.fun_info A.FunDeclId.Map.t) (types_infos : TA.type_infos) +let translate_fun_signatures (fun_infos : FA.fun_info A.FunDeclId.Map.t) + (types_infos : TA.type_infos) (functions : (A.fun_id * string option list * A.fun_sig) list) : fun_sig_named_outputs RegularFunIdMap.t = (* For every function, translate the signatures of: @@ -1914,8 +1867,7 @@ let translate_fun_signatures (backward_no_state_update : bool) (sg : A.fun_sig) : (regular_fun_id * fun_sig_named_outputs) list = (* The forward function *) let fwd_sg = - translate_fun_sig backward_no_state_update fun_infos fun_id types_infos sg - input_names None + translate_fun_sig fun_infos fun_id types_infos sg input_names None in let fwd_id = (fun_id, None) in (* The backward functions *) @@ -1923,8 +1875,8 @@ let translate_fun_signatures (backward_no_state_update : bool) List.map (fun (rg : T.region_var_group) -> let tsg = - translate_fun_sig backward_no_state_update fun_infos fun_id - types_infos sg input_names (Some rg.id) + translate_fun_sig fun_infos fun_id types_infos sg input_names + (Some rg.id) in let id = (fun_id, Some rg.id) in (id, tsg)) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 72322c73..453e02db 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -11,63 +11,6 @@ open TranslateCore (** The local logger *) let log = TranslateCore.log -type config = { - eval_config : Contexts.partial_config; - mp_config : Micro.config; - use_state : bool; - (** Controls whether we need to use a state to model the external world - (I/O, for instance). - *) - backward_no_state_update : bool; - (** Controls whether backward functions update the state, in case we use - a state ({!use_state}). - - If they update the state, we generate code of the following style: - {[ - (st1, y) <-- f_fwd x st0; // st0 is the state upon calling f_fwd - ... - (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back - }] - - Otherwise, we generate code of the following shape: - {[ - (st1, y) <-- f_fwd x st0; - ... - x' <-- f_back x st0 y'; - }] - - The second format is easier to reason about, but the first one is - necessary to properly handle some Rust functions which use internal - mutability such as {{:https://doc.rust-lang.org/std/cell/struct.RefCell.html#method.try_borrow_mut} [RefCell::try_mut_borrow]}: - in order to model this behaviour we would need a state, and calling the backward - function would update the state by reinserting the updated value in it. - *) - split_files : bool; - (** Controls whether we split the generated definitions between different - files for the types, clauses and functions, or if we group them in - one file. - *) - test_unit_functions : bool; - (** If true, insert tests in the generated files to check that the - unit functions normalize to [Success _]. - - For instance, in F* it generates code like this: - {[ - let _ = assert_norm (FUNCTION () = Success ()) - ]} - *) - extract_decreases_clauses : bool; - (** If [true], insert [decreases] clauses for all the recursive definitions. - - The body of such clauses must be defined by the user. - *) - extract_template_decreases_clauses : bool; - (** In order to help the user, we can generate "template" decrease clauses - (i.e., definitions with proper signatures but dummy bodies) in a - dedicated file. - *) -} - (** The result of running the symbolic interpreter on a function: - the list of symbolic values used for the input values - the generated symbolic AST @@ -77,9 +20,8 @@ type symbolic_fun_translation = V.symbolic_value list * SA.expression (** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs, for the forward function and the backward functions. *) -let translate_function_to_symbolics (config : C.partial_config) - (trans_ctx : trans_ctx) (fdef : A.fun_decl) : - (symbolic_fun_translation * symbolic_fun_translation list) option = +let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl) + : (symbolic_fun_translation * symbolic_fun_translation list) option = (* Debug *) log#ldebug (lazy @@ -96,7 +38,7 @@ let translate_function_to_symbolics (config : C.partial_config) let synthesize = true in let evaluate gid = let inputs, symb = - evaluate_function_symbolic config synthesize type_context fun_context + evaluate_function_symbolic synthesize type_context fun_context global_context fdef gid in (inputs, Option.get symb) @@ -119,9 +61,7 @@ let translate_function_to_symbolics (config : C.partial_config) of backward functions, we also provide names for the outputs. TODO: maybe we should introduce a record for this. *) -let translate_function_to_pure (config : C.partial_config) - (mp_config : Micro.config) (backward_no_state_update : bool) - (trans_ctx : trans_ctx) +let translate_function_to_pure (trans_ctx : trans_ctx) (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t) (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl) : pure_fun_translation = @@ -134,7 +74,7 @@ let translate_function_to_pure (config : C.partial_config) let def_id = fdef.def_id in (* Compute the symbolic ASTs, if the function is transparent *) - let symbolic_trans = translate_function_to_symbolics config trans_ctx fdef in + let symbolic_trans = translate_function_to_symbolics trans_ctx fdef in let symbolic_forward, symbolic_backwards = match symbolic_trans with | None -> (None, None) @@ -210,21 +150,12 @@ let translate_function_to_pure (config : C.partial_config) { ctx with forward_inputs } in - (* The symbolic to pure config *) - let sp_config = - { - SymbolicToPure.filter_useless_back_calls = - mp_config.filter_useless_monadic_calls; - backward_no_state_update; - } - in - (* Translate the forward function *) let pure_forward = match symbolic_forward with - | None -> SymbolicToPure.translate_fun_decl sp_config ctx None + | None -> SymbolicToPure.translate_fun_decl ctx None | Some (fwd_svs, fwd_ast) -> - SymbolicToPure.translate_fun_decl sp_config + SymbolicToPure.translate_fun_decl (add_forward_inputs fwd_svs ctx) (Some fwd_ast) in @@ -247,7 +178,7 @@ let translate_function_to_pure (config : C.partial_config) let ctx = { ctx with bid = Some back_id; sg = backward_sg.sg } in (* Translate *) - SymbolicToPure.translate_fun_decl sp_config ctx None + SymbolicToPure.translate_fun_decl ctx None | Some symbolic_backwards -> let input_svs, symbolic = T.RegionGroupId.nth symbolic_backwards back_id @@ -259,8 +190,8 @@ let translate_function_to_pure (config : C.partial_config) in (* We need to ignore the forward inputs, and the state input (if there is) *) let fun_info = - SymbolicToPure.get_fun_effect_info backward_no_state_update - fun_context.fun_infos (A.Regular def_id) (Some back_id) + SymbolicToPure.get_fun_effect_info fun_context.fun_infos + (A.Regular def_id) (Some back_id) in let backward_inputs = (* We need to ignore the forward state and the backward state *) @@ -313,7 +244,7 @@ let translate_function_to_pure (config : C.partial_config) in (* Translate *) - SymbolicToPure.translate_fun_decl sp_config ctx (Some symbolic) + SymbolicToPure.translate_fun_decl ctx (Some symbolic) in let pure_backwards = List.map translate_backward fdef.signature.regions_hierarchy @@ -322,9 +253,7 @@ let translate_function_to_pure (config : C.partial_config) (* Return *) (pure_forward, pure_backwards) -let translate_module_to_pure (config : C.partial_config) - (mp_config : Micro.config) (use_state : bool) - (backward_no_state_update : bool) (crate : A.crate) : +let translate_module_to_pure (crate : A.crate) : trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list = (* Debug *) log#ldebug (lazy "translate_module_to_pure"); @@ -335,7 +264,7 @@ let translate_module_to_pure (config : C.partial_config) in let fun_infos = FA.analyze_module crate fun_context.C.fun_decls - global_context.C.global_decls use_state + global_context.C.global_decls !Config.use_state in let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in let trans_ctx = { type_context; fun_context; global_context } in @@ -372,22 +301,21 @@ let translate_module_to_pure (config : C.partial_config) in let sigs = List.append assumed_sigs local_sigs in let fun_sigs = - SymbolicToPure.translate_fun_signatures backward_no_state_update - fun_context.fun_infos type_context.type_infos sigs + SymbolicToPure.translate_fun_signatures fun_context.fun_infos + type_context.type_infos sigs in (* Translate all the *transparent* functions *) let pure_translations = List.map - (translate_function_to_pure config mp_config backward_no_state_update - trans_ctx fun_sigs type_decls_map) + (translate_function_to_pure trans_ctx fun_sigs type_decls_map) crate.functions in (* Apply the micro-passes *) let pure_translations = List.map - (Micro.apply_passes_to_pure_fun_translation mp_config trans_ctx) + (Micro.apply_passes_to_pure_fun_translation trans_ctx) pure_translations in @@ -404,8 +332,6 @@ type gen_ctx = { } type gen_config = { - mp_config : Micro.config; - use_state : bool; extract_types : bool; extract_decreases_clauses : bool; extract_template_decreases_clauses : bool; @@ -423,7 +349,7 @@ type gen_config = { declarations in an interface file, together with an implementation file if needed. *) - test_unit_functions : bool; + test_trans_unit_functions : bool; } (** Returns the pair: (has opaque type decls, has opaque fun decls) *) @@ -538,7 +464,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) has_decr_clause def) fls); (* Insert unit tests if necessary *) - if config.test_unit_functions then + if config.test_trans_unit_functions then List.iter (fun (keep_fwd, (fwd, _)) -> if keep_fwd then @@ -665,13 +591,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) (** Translate a module and write the synthesized code to an output file. TODO: rename to translate_crate *) -let translate_module (filename : string) (dest_dir : string) (config : config) - (crate : A.crate) : unit = +let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : + unit = (* Translate the module to the pure AST *) - let trans_ctx, trans_types, trans_funs = - translate_module_to_pure config.eval_config config.mp_config - config.use_state config.backward_no_state_update crate - in + let trans_ctx, trans_types, trans_funs = translate_module_to_pure crate in (* Initialize the extraction context - for now we extract only to F*. * We initialize the names map by registering the keywords used in the @@ -796,30 +719,26 @@ let translate_module (filename : string) (dest_dir : string) (config : config) } in - let use_state = config.use_state in - (* Extract one or several files, depending on the configuration *) - if config.split_files then ( + if !Config.split_files then ( let base_gen_config = { - mp_config = config.mp_config; - use_state; extract_types = false; - extract_decreases_clauses = config.extract_decreases_clauses; + extract_decreases_clauses = !Config.extract_decreases_clauses; extract_template_decreases_clauses = false; extract_fun_decls = false; extract_transparent = true; extract_opaque = false; extract_state_type = false; interface = false; - test_unit_functions = false; + test_trans_unit_functions = false; } in (* Check if there are opaque types and functions - in which case we need * to split *) let has_opaque_types, has_opaque_funs = module_has_opaque_decls gen_ctx in - let has_opaque_types = has_opaque_types || use_state in + let has_opaque_types = has_opaque_types || !Config.use_state in (* Extract the types *) (* If there are opaque types, we extract in an interface *) @@ -831,7 +750,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) base_gen_config with extract_types = true; extract_opaque = true; - extract_state_type = use_state; + extract_state_type = !Config.use_state; interface = has_opaque_types; } in @@ -840,10 +759,10 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (* Extract the template clauses *) let needs_clauses_module = - config.extract_decreases_clauses + !Config.extract_decreases_clauses && not (A.FunDeclId.Set.is_empty rec_functions) in - (if needs_clauses_module && config.extract_template_decreases_clauses then + (if needs_clauses_module && !Config.extract_template_decreases_clauses then let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in let clauses_module = module_name ^ ".Clauses.Template" in let clauses_config = @@ -880,7 +799,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) { base_gen_config with extract_fun_decls = true; - test_unit_functions = config.test_unit_functions; + test_trans_unit_functions = !Config.test_trans_unit_functions; } in let clauses_module = @@ -892,18 +811,16 @@ let translate_module (filename : string) (dest_dir : string) (config : config) else let gen_config = { - mp_config = config.mp_config; - use_state; extract_types = true; - extract_decreases_clauses = config.extract_decreases_clauses; + extract_decreases_clauses = !Config.extract_decreases_clauses; extract_template_decreases_clauses = - config.extract_template_decreases_clauses; + !Config.extract_template_decreases_clauses; extract_fun_decls = true; extract_transparent = true; extract_opaque = true; - extract_state_type = use_state; + extract_state_type = !Config.use_state; interface = false; - test_unit_functions = config.test_unit_functions; + test_trans_unit_functions = !Config.test_trans_unit_functions; } in (* Add the extension for F* *) diff --git a/compiler/dune b/compiler/dune index 0d340d59..85f4b75b 100644 --- a/compiler/dune +++ b/compiler/dune @@ -14,6 +14,7 @@ (modules Assumed Collections + Config ConstStrings Contexts Cps |