summaryrefslogtreecommitdiff
path: root/compiler/Config.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Config.ml')
-rw-r--r--compiler/Config.ml192
1 files changed, 192 insertions, 0 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