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
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
|
(* This module provides the functions which handle expansion of symbolic values.
* For now, this file doesn't handle expansion of ⊥ values because they need
* some path utilities for replacement. We might change that in the future (by
* using indices to identify the values for instance). *)
module T = Types
module V = Values
open Scalars
module E = Expressions
open Errors
module C = Contexts
module Subst = Substitute
module A = CfimAst
module L = Logging
open TypesUtils
open ValuesUtils
module Inv = Invariants
module S = Synthesis
open Utils
open InterpreterUtils
open InterpreterProjectors
open InterpreterBorrows
(** Projector kind *)
type proj_kind = LoanProj | BorrowProj
(** Auxiliary function.
Apply a symbolic expansion to avalues in a context, targetting a specific
kind of projectors.
[proj_kind] controls whether we apply the expansion to projectors
on loans or projectors on borrows.
When dealing with reference expansion, it is necessary to first apply the
expansion on loan projectors, then on borrow projectors. The reason is
that reducing the borrow projectors might require to perform some reborrows,
in which case we need to lookup the corresponding loans in the context.
[allow_reborrows] controls whether we allow reborrows or not. It is useful
only if we target borrow projectors.
Also, if this function is called on an expansion for *shared references*,
the proj borrows should already have been expanded.
TODO: the way this function is used is a bit complex, especially because of
the above condition. Maybe we should have:
1. a generic function to expand the loan projectors
2. a function to expand the borrow projectors for non-borrows
3. specialized functions for mut borrows and shared borrows
Note that 2. and 3. may have a little bit of duplicated code, but hopefully
it would make things clearer.
*)
let apply_symbolic_expansion_to_target_avalues (config : C.config)
(allow_reborrows : bool) (proj_kind : proj_kind)
(original_sv : V.symbolic_value) (expansion : symbolic_expansion)
(ctx : C.eval_ctx) : C.eval_ctx =
(* Symbolic values contained in the expansion might contain already ended regions *)
let check_symbolic_no_ended = false in
(* Prepare reborrows registration *)
let fresh_reborrow, apply_registered_reborrows =
prepare_reborrows config allow_reborrows ctx
in
(* Visitor to apply the expansion *)
let obj =
object
inherit [_] C.map_eval_ctx as super
method! visit_abs proj_regions abs =
assert (Option.is_none proj_regions);
let proj_regions = Some abs.V.regions in
super#visit_abs proj_regions abs
(** When visiting an abstraction, we remember the regions it owns to be
able to properly reduce projectors when expanding symbolic values *)
method! visit_ASymbolic proj_regions aproj =
let proj_regions = Option.get proj_regions in
match (aproj, proj_kind) with
| V.AProjLoans sv, LoanProj ->
(* Check if this is the symbolic value we are looking for *)
if same_symbolic_id sv original_sv then
(* Apply the projector *)
let projected_value =
apply_proj_loans_on_symbolic_expansion proj_regions expansion
original_sv.V.sv_ty
in
(* Replace *)
projected_value.V.value
else
(* Not the searched symbolic value: nothing to do *)
super#visit_ASymbolic (Some proj_regions) aproj
| V.AProjBorrows (sv, proj_ty), BorrowProj ->
(* Check if this is the symbolic value we are looking for *)
if same_symbolic_id sv original_sv then
(* Convert the symbolic expansion to a value on which we can
* apply a projector (if the expansion is a reference expansion,
* convert it to a borrow) *)
(* WARNING: we mustn't get there if the expansion is for a shared
* reference. *)
let expansion =
symbolic_expansion_non_shared_borrow_to_value original_sv
expansion
in
(* Apply the projector *)
let projected_value =
apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
proj_regions expansion proj_ty
in
(* Replace *)
projected_value.V.value
else
(* Not the searched symbolic value: nothing to do *)
super#visit_ASymbolic (Some proj_regions) aproj
| V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj ->
(* Nothing to do *)
super#visit_ASymbolic (Some proj_regions) aproj
end
in
(* Apply the expansion *)
let ctx = obj#visit_eval_ctx None ctx in
(* Apply the reborrows *)
apply_registered_reborrows ctx
(** Auxiliary function.
Apply a symbolic expansion to avalues in a context.
*)
let apply_symbolic_expansion_to_avalues (config : C.config)
(allow_reborrows : bool) (original_sv : V.symbolic_value)
(expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx =
let apply_expansion proj_kind ctx =
apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind
original_sv expansion ctx
in
(* First target the loan projectors, then the borrow projectors *)
let ctx = apply_expansion LoanProj ctx in
let ctx = apply_expansion BorrowProj ctx in
ctx
(** Auxiliary function.
Simply replace the symbolic values (*not avalues*) in the context with
a given value. Will break invariants if not used properly.
*)
let replace_symbolic_values (at_most_once : bool)
(original_sv : V.symbolic_value) (nv : V.value) (ctx : C.eval_ctx) :
C.eval_ctx =
(* Count *)
let replaced = ref false in
let replace () =
if at_most_once then assert (not !replaced);
replaced := true;
nv
in
(* Visitor to apply the substitution *)
let obj =
object
inherit [_] C.map_eval_ctx as super
method! visit_Symbolic env spc =
if same_symbolic_id spc.V.svalue original_sv then replace ()
else super#visit_Symbolic env spc
end
in
(* Apply the substitution *)
let ctx = obj#visit_eval_ctx None ctx in
(* Check that we substituted *)
assert !replaced;
(* Return *)
ctx
(** Apply a symbolic expansion to a context, by replacing the original
symbolic value with its expanded value. Is valid only if the expansion
is not a borrow (i.e., an adt...).
*)
let apply_symbolic_expansion_non_borrow (config : C.config)
(original_sv : V.symbolic_value) (expansion : symbolic_expansion)
(ctx : C.eval_ctx) : C.eval_ctx =
(* Apply the expansion to non-abstraction values *)
let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
let at_most_once = false in
let ctx = replace_symbolic_values at_most_once original_sv nv.V.value ctx in
(* Apply the expansion to abstraction values *)
let allow_reborrows = false in
apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
expansion ctx
(** Compute the expansion of an adt value.
The function might return a list of contexts and values if the symbolic
value to expand is an enumeration.
`expand_enumerations` controls the expansion of enumerations: if false, it
doesn't allow the expansion of enumerations *containing several variants*.
*)
let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
(ended_regions : T.RegionId.set_t) (def_id : T.TypeDefId.id)
(regions : T.RegionId.id T.region list) (types : T.rty list)
(ctx : C.eval_ctx) : (C.eval_ctx * symbolic_expansion) list =
(* Lookup the definition and check if it is an enumeration with several
* variants *)
let def = C.ctx_lookup_type_def ctx def_id in
assert (List.length regions = List.length def.T.region_params);
(* Retrieve, for every variant, the list of its instantiated field types *)
let variants_fields_types =
Subst.type_def_get_instantiated_variants_fields_rtypes def regions types
in
(* Check if there is strictly more than one variant *)
if List.length variants_fields_types > 1 && not expand_enumerations then
failwith "Not allowed to expand enumerations with several variants";
(* Initialize the expanded value for a given variant *)
let initialize (ctx : C.eval_ctx)
((variant_id, field_types) : T.VariantId.id option * T.rty list) :
C.eval_ctx * symbolic_expansion =
let ctx, field_values =
List.fold_left_map
(fun ctx (ty : T.rty) ->
mk_fresh_symbolic_proj_comp ended_regions ty ctx)
ctx field_types
in
let see = SeAdt (variant_id, field_values) in
(ctx, see)
in
(* Initialize all the expanded values of all the variants *)
List.map (initialize ctx) variants_fields_types
let compute_expanded_symbolic_tuple_value (ended_regions : T.RegionId.set_t)
(field_types : T.rty list) (ctx : C.eval_ctx) :
C.eval_ctx * symbolic_expansion =
(* Generate the field values *)
let ctx, field_values =
List.fold_left_map
(fun ctx sv_ty -> mk_fresh_symbolic_proj_comp ended_regions sv_ty ctx)
ctx field_types
in
let variant_id = None in
let see = SeAdt (variant_id, field_values) in
(ctx, see)
let compute_expanded_symbolic_box_value (ended_regions : T.RegionId.set_t)
(boxed_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * symbolic_expansion =
(* Introduce a fresh symbolic value *)
let ctx, boxed_value =
mk_fresh_symbolic_proj_comp ended_regions boxed_ty ctx
in
let see = SeAdt (None, [ boxed_value ]) in
(ctx, see)
let expand_symbolic_value_shared_borrow (config : C.config)
(original_sv : V.symbolic_value) (ended_regions : T.RegionId.set_t)
(ref_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx =
(* First, replace the projectors on borrows (AProjBorrow and proj_comp)
* The important point is that the symbolic value to expand may appear
* several times, if it has been copied. In this case, we need to introduce
* one fresh borrow id per instance.
*)
let borrows = ref V.BorrowId.Set.empty in
let borrow_counter = ref ctx.C.borrow_counter in
let fresh_borrow () =
let bid', cnt' = V.BorrowId.fresh !borrow_counter in
borrow_counter := cnt';
borrows := V.BorrowId.Set.add bid' !borrows;
bid'
in
(* Small utility used on shared borrows in abstractions (regular borrow
* projector and asb).
* Returns `Some` if the symbolic value has been expanded to an asb list,
* `None` otherwise *)
let reborrow_ashared proj_regions (sv : V.symbolic_value) (proj_ty : T.rty) :
V.abstract_shared_borrows option =
if same_symbolic_id sv original_sv then
match proj_ty with
| T.Ref (r, ref_ty, T.Shared) ->
(* Projector over the shared value *)
let shared_asb = V.AsbProjReborrows (sv, ref_ty) in
(* Check if the region is in the set of projected regions *)
if region_in_set r proj_regions then
(* In the set: we need to reborrow *)
let bid = fresh_borrow () in
Some [ V.AsbBorrow bid; shared_asb ]
else (* Not in the set: ignore *)
Some [ shared_asb ]
| _ -> failwith "Unexpected"
else None
in
(* Visitor to replace the projectors on borrows *)
let obj =
object
inherit [_] C.map_eval_ctx as super
method! visit_Symbolic env sv =
if same_symbolic_id sv.V.svalue original_sv then
let bid = fresh_borrow () in
V.Borrow (V.SharedBorrow bid)
else super#visit_Symbolic env sv
method! visit_Abs proj_regions abs =
assert (Option.is_none proj_regions);
let proj_regions = Some abs.V.regions in
super#visit_Abs proj_regions abs
method! visit_AProjSharedBorrow proj_regions asb =
let expand_asb (asb : V.abstract_shared_borrow) :
V.abstract_shared_borrows =
match asb with
| V.AsbBorrow _ -> [ asb ]
| V.AsbProjReborrows (sv, proj_ty) -> (
match reborrow_ashared (Option.get proj_regions) sv proj_ty with
| None -> [ asb ]
| Some asb -> asb)
in
let asb = List.concat (List.map expand_asb asb) in
V.AProjSharedBorrow asb
method! visit_ASymbolic proj_regions aproj =
match aproj with
| AProjLoans _ ->
(* Loans are handled later *)
super#visit_ASymbolic proj_regions aproj
| AProjBorrows (sv, proj_ty) -> (
(* Check if we need to reborrow *)
match reborrow_ashared (Option.get proj_regions) sv proj_ty with
| None -> super#visit_ASymbolic proj_regions aproj
| Some asb -> V.ABorrow (V.AProjSharedBorrow asb))
end
in
(* Call the visitor *)
let ctx = obj#visit_eval_ctx None ctx in
let ctx = { ctx with C.borrow_counter = !borrow_counter } in
(* Finally, replace the projectors on loans *)
let bids = !borrows in
assert (not (V.BorrowId.Set.is_empty bids));
let ctx, shared_sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in
let see = SeSharedRef (bids, shared_sv) in
let allow_reborrows = true in
let ctx =
apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see
ctx
in
(* Update the synthesized program *)
S.synthesize_symbolic_expansion_no_branching original_sv see;
(* Return *)
ctx
let expand_symbolic_value_borrow (config : C.config)
(original_sv : V.symbolic_value) (ended_regions : T.RegionId.set_t)
(region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind)
(ctx : C.eval_ctx) : C.eval_ctx =
(* Check that we are allowed to expand the reference *)
assert (not (region_in_set region ended_regions));
(* Match on the reference kind *)
match rkind with
| T.Mut ->
(* Simple case: simply create a fresh symbolic value and a fresh
* borrow id *)
let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in
let ctx, bid = C.fresh_borrow_id ctx in
let see = SeMutRef (bid, sv) in
(* Expand the symbolic values - we simply perform a substitution (and
* check that we perform exactly one substitution) *)
let nv = symbolic_expansion_non_shared_borrow_to_value original_sv see in
let at_most_once = true in
let ctx =
replace_symbolic_values at_most_once original_sv nv.V.value ctx
in
(* Expand the symbolic avalues *)
let allow_reborrows = true in
let ctx =
apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
see ctx
in
(* Update the synthesized program *)
S.synthesize_symbolic_expansion_no_branching original_sv see;
(* Return *)
ctx
| T.Shared ->
expand_symbolic_value_shared_borrow config original_sv ended_regions
ref_ty ctx
(** Expand a symbolic value which is not an enumeration with several variants
(i.e., in a situation where it doesn't lead to branching).
This function is used when exploring paths.
*)
let expand_symbolic_value_no_branching (config : C.config)
(pe : E.projection_elem) (sp : V.symbolic_proj_comp) (ctx : C.eval_ctx) :
C.eval_ctx =
(* Compute the expanded value - note that when doing so, we may introduce
* fresh symbolic values in the context (which thus gets updated) *)
let original_sv = sp.V.svalue in
let rty = original_sv.V.sv_ty in
let ended_regions = sp.V.rset_ended in
let ctx =
match (pe, rty) with
(* "Regular" ADTs *)
| ( Field (ProjAdt (def_id, _opt_variant_id), _),
T.Adt (T.AdtId def_id', regions, types) ) -> (
assert (def_id = def_id');
(* Compute the expanded value - there should be exactly one because we
* don't allow to expand enumerations with strictly more than one variant *)
let expand_enumerations = false in
match
compute_expanded_symbolic_adt_value expand_enumerations ended_regions
def_id regions types ctx
with
| [ (ctx, see) ] ->
(* Apply in the context *)
let ctx =
apply_symbolic_expansion_non_borrow config original_sv see ctx
in
(* Update the synthesized program *)
S.synthesize_symbolic_expansion_no_branching original_sv see;
(* Return *)
ctx
| _ -> failwith "Unexpected")
(* Tuples *)
| Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
assert (arity = List.length tys);
(* Generate the field values *)
let ctx, see =
compute_expanded_symbolic_tuple_value ended_regions tys ctx
in
(* Apply in the context *)
let ctx =
apply_symbolic_expansion_non_borrow config original_sv see ctx
in
(* Update the synthesized program *)
S.synthesize_symbolic_expansion_no_branching original_sv see;
(* Return *)
ctx
(* Boxes *)
| DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
let ctx, see =
compute_expanded_symbolic_box_value ended_regions boxed_ty ctx
in
(* Apply in the context *)
let ctx =
apply_symbolic_expansion_non_borrow config original_sv see ctx
in
(* Update the synthesized program *)
S.synthesize_symbolic_expansion_no_branching original_sv see;
(* Return *)
ctx
(* Borrows *)
| Deref, T.Ref (region, ref_ty, rkind) ->
expand_symbolic_value_borrow config original_sv ended_regions region
ref_ty rkind ctx
| _ ->
failwith
("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
in
(* Sanity check: the symbolic value has disappeared *)
assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx));
(* Return *)
ctx
(** Expand a symbolic enumeration value.
This might lead to branching.
*)
let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_proj_comp)
(ctx : C.eval_ctx) : C.eval_ctx list =
(* Compute the expanded value - note that when doing so, we may introduce
* fresh symbolic values in the context (which thus gets updated) *)
let original_sv = sp.V.svalue in
let rty = original_sv.V.sv_ty in
let ended_regions = sp.V.rset_ended in
match rty with
(* The value should be a "regular" ADTs *)
| T.Adt (T.AdtId def_id, regions, types) ->
(* Compute the expanded value - there should be exactly one because we
* don't allow to expand enumerations with strictly more than one variant *)
let expand_enumerations = true in
let res =
compute_expanded_symbolic_adt_value expand_enumerations ended_regions
def_id regions types ctx
in
(* Update the synthesized program *)
let seel = List.map (fun (_, x) -> x) res in
S.synthesize_symbolic_expansion_enum_branching original_sv seel;
(* Apply in the context *)
let apply (ctx, see) : C.eval_ctx =
let ctx =
apply_symbolic_expansion_non_borrow config original_sv see ctx
in
(* Sanity check: the symbolic value has disappeared *)
assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx));
(* Return *)
ctx
in
List.map apply res
| _ -> failwith "Unexpected"
|