summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Config.ml192
-rw-r--r--compiler/Contexts.ml55
-rw-r--r--compiler/Driver.ml84
-rw-r--r--compiler/Interpreter.ml28
-rw-r--r--compiler/InterpreterBorrows.ml4
-rw-r--r--compiler/InterpreterExpansion.ml2
-rw-r--r--compiler/InterpreterExpressions.ml18
-rw-r--r--compiler/InterpreterExpressions.mli3
-rw-r--r--compiler/InterpreterPaths.ml48
-rw-r--r--compiler/InterpreterPaths.mli10
-rw-r--r--compiler/InterpreterStatements.ml18
-rw-r--r--compiler/Invariants.ml19
-rw-r--r--compiler/PureMicroPasses.ml89
-rw-r--r--compiler/SymbolicToPure.ml158
-rw-r--r--compiler/Translate.ml151
-rw-r--r--compiler/dune1
16 files changed, 388 insertions, 492 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 01:52:48 +0000