1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
|
(** Define the global configuration options *)
(** {1 Backend choice} *)
(** The choice of backend *)
type backend = FStar | Coq | Lean | HOL4
let backend_names = [ "fstar"; "coq"; "lean"; "hol4" ]
(** Utility to compute the backend from an input parameter *)
let backend_of_string (b : string) : backend option =
match b with
| "fstar" -> Some FStar
| "coq" -> Some Coq
| "lean" -> Some Lean
| "hol4" -> Some HOL4
| _ -> None
let opt_backend : backend option ref = ref None
let set_backend (b : string) : unit =
match backend_of_string b with
| Some b -> opt_backend := Some b
| None ->
(* We shouldn't get there: the string should have been checked as
belonging to the proper set *)
raise (Failure "Unexpected")
(** The backend to which to extract.
We initialize it with a default value, but it always gets overwritten:
we check that the user provides a backend argument.
*)
let backend = ref FStar
(** {1 Interpreter} *)
(** Check that invariants are maintained whenever we execute a statement
TODO: rename to sanity_checks.
*)
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
(** The maximum number of iterations we can do to find a loop fixed point.
This is mostly for sanity: we should always find a fixed point in a
reasonable number of iterations. If we fail to do so, it is likely a bug: we
thus use this bound to detect a loop, fail and report the case to the
user.
*)
let loop_fixed_point_max_num_iters = 2
(** {1 Translation} *)
(** Forbids using field projectors for structures.
If we don't use field projectors, whenever we symbolically expand a structure
value (note that accessing a structure field in the symbolic execution triggers
its expansion), then instead of generating code like this:
{[
let x1 = s.f1 in
let x2 = s.f2 in
...
]}
we generate code like this:
{[
let Mkstruct x1 x2 ... = s in
...
]}
Rem.: this used to be useful for Coq, because in Coq we can't define groups
of mutually recursive records and inductives. In such cases, we extract
the structures as inductives, which means that field projectors are not
always available. As of today, we generate field projectors definitions
(together with the appropriate notations).
*)
let dont_use_field_projectors = ref false
(** Deconstructing ADTs which have only one variant with let-bindings is not always
supported: this parameter controls whether we use let-bindings in such situations or not.
*)
let always_deconstruct_adts_with_matches = ref false
(** Controls whether we need to use a state to model the external world
(I/O, for instance).
*)
let use_state = ref true
(** Controls whether we use fuel to control termination.
*)
let use_fuel = ref false
(** 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
(** Generate the library entry point, if the crate is split between different files.
Sometimes we want to skip this: the library entry points just includes all the
files in the project, and the user may want to write their own entry point, to
add custom includes (to include the files containing the proofs, for instance).
*)
let generate_lib_entry_point = ref true
(** For Lean, controls whether we generate a lakefile or not.
*)
let lean_gen_lakefile = ref false
(** 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], use decreases clauses/termination measures for all the recursive definitions.
More precisely:
- for F*, we generate definitions which use decreases clauses
- for Lean, we generate definitions which use termination measures and
decreases proofs
The body of such clauses/proofs must be defined by the user.
*)
let extract_decreases_clauses = ref false
(** In order to help the user, we can generate "template" decrease clauses/ termination
measures (i.e., definitions with proper signatures but dummy bodies) in a dedicated
file.
*)
let extract_template_decreases_clauses = ref false
(** {1 Micro passes} *)
(** Some provers like F* and Coq don't support the decomposition of return values
in monadic let-bindings:
{[
(* NOT supported in F*/Coq *)
(x, y) <-- f ();
...
]}
In such situations, we might want to introduce an intermediate
assignment:
{[
tmp <-- f ();
let (x, y) = tmp in
...
]}
*)
let decompose_monadic_let_bindings = ref false
(** Some provers like Coq don't support nested patterns in let-bindings:
{[
(* NOT supported in Coq *)
(st, (x1, x2)) <-- f ();
...
]}
In such situations, we might want to introduce intermediate
assignments:
{[
(st, tmp) <-- f ();
let (x1, x2) = tmp in
...
]}
*)
let decompose_nested_let_patterns = 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 {!unfold_monadic_let_bindings} is true, setting
{!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 {!val:PureMicroPasses.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
(** Use short names for the record fields.
Some backends can't disambiguate records when their field names have collisions.
When this happens, we use long names, by which we concatenate the record
names with the field names, and check whether there are name collisions.
For backends which can disambiguate records (typically by using the typing
information), we use short names (i.e., the original field names).
*)
let record_fields_short_names = ref false
(** Parameterize the traits with their associated types, so as not to use
types as first class objects.
This is useful for some backends with limited expressiveness like HOL4,
and to account for type constraints (like [fn f<T : Foo>(...) where T::bar = usize]).
*)
let parameterize_trait_types = ref false
(** For sanity check: type check the generated pure code (activates checks in
several places).
TODO: deactivated for now because we need to implement the normalization of
trait associated types in the pure code.
*)
let type_check_pure_code = ref false
(** Shall we fail hard if we encounter an issue, or should we attempt to go
as far as possible while leaving "holes" in the generated code? *)
let fail_hard = ref true
|