summaryrefslogtreecommitdiff
path: root/compiler/InterpreterExpansion.ml
blob: 167e3d581a79e591d18d37c1894aa0fa52ee28f3 (plain)
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
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
(* 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 PV = PrimitiveValues
module V = Values
module E = Expressions
module C = Contexts
module Subst = Substitute
module Assoc = AssociatedTypes
module L = Logging
open TypesUtils
module Inv = Invariants
module S = SynthesizeSymbolic
module SA = SymbolicAst
open Cps
open ValuesUtils
open InterpreterUtils
open InterpreterProjectors
open InterpreterBorrows

(** The local logger *)
let log = L.expansion_log

(** 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 : V.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
  in
  (* Visitor to apply the expansion *)
  let obj =
    object (self)
      inherit [_] C.map_eval_ctx as super

      (** When visiting an abstraction, we remember the regions it owns to be
          able to properly reduce projectors when expanding symbolic values *)
      method! visit_abs current_abs abs =
        assert (Option.is_none current_abs);
        let current_abs = Some abs in
        super#visit_abs current_abs abs

      (** We carefully updated {!visit_ASymbolic} so that {!visit_aproj} is called
          only on child projections (i.e., projections which appear in {!AEndedProjLoans}).
          The role of visit_aproj is then to check we don't have to expand symbolic
          values in child projections, because it should never happen
        *)
      method! visit_aproj current_abs aproj =
        (match aproj with
        | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
            assert (not (same_symbolic_id sv original_sv))
        | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
        super#visit_aproj current_abs aproj

      method! visit_ASymbolic current_abs aproj =
        let current_abs = Option.get current_abs in
        let proj_regions = current_abs.regions in
        let ancestors_regions = current_abs.ancestors_regions in
        (* Explore in depth first - we won't update anything: we simply
         * want to check we don't have to expand inner symbolic value *)
        match (aproj, proj_kind) with
        | V.AEndedProjBorrows _, _ -> V.ASymbolic aproj
        | V.AEndedProjLoans _, _ ->
            (* Explore the given back values to make sure we don't have to expand
             * anything in there *)
            V.ASymbolic (self#visit_aproj (Some current_abs) aproj)
        | V.AProjLoans (sv, given_back), LoanProj ->
            (* Check if this is the symbolic value we are looking for *)
            if same_symbolic_id sv original_sv then (
              (* There mustn't be any given back values *)
              assert (given_back = []);
              (* Apply the projector *)
              let projected_value =
                apply_proj_loans_on_symbolic_expansion proj_regions
                  ancestors_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 current_abs) 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 ancestors_regions expansion proj_ty
              in
              (* Replace *)
              projected_value.V.value
            else
              (* Not the searched symbolic value: nothing to do *)
              super#visit_ASymbolic (Some current_abs) aproj
        | V.AProjLoans _, BorrowProj
        | V.AProjBorrows (_, _), LoanProj
        | V.AIgnoredProjBorrows, _ ->
            (* Nothing to do *)
            V.ASymbolic 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 : V.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 original_sv then replace ()
        else super#visit_Symbolic env spc
    end
  in
  (* Apply the substitution *)
  let ctx = obj#visit_eval_ctx None ctx in
  (* Return *)
  ctx

let apply_symbolic_expansion_non_borrow (config : C.config)
    (original_sv : V.symbolic_value) (expansion : V.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 a non-assumed (i.e.: not [Box], etc.)
    adt value.

    The function might return a list of 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_non_assumed_adt_value (expand_enumerations : bool)
    (kind : V.sv_kind) (def_id : T.TypeDeclId.id) (generics : T.rgeneric_args)
    (ctx : C.eval_ctx) : V.symbolic_expansion list =
  (* Lookup the definition and check if it is an enumeration with several
   * variants *)
  let def = C.ctx_lookup_type_decl ctx def_id in
  assert (List.length generics.regions = List.length def.T.generics.regions);
  (* Retrieve, for every variant, the list of its instantiated field types *)
  let variants_fields_types =
    Assoc.type_decl_get_inst_norm_variants_fields_rtypes ctx def generics
  in
  (* Check if there is strictly more than one variant *)
  if List.length variants_fields_types > 1 && not expand_enumerations then
    raise (Failure "Not allowed to expand enumerations with several variants");
  (* Initialize the expanded value for a given variant *)
  let initialize
      ((variant_id, field_types) : T.VariantId.id option * T.rty list) :
      V.symbolic_expansion =
    let field_values =
      List.map (fun (ty : T.rty) -> mk_fresh_symbolic_value kind ty) field_types
    in
    let see = V.SeAdt (variant_id, field_values) in
    see
  in
  (* Initialize all the expanded values of all the variants *)
  List.map initialize variants_fields_types

let compute_expanded_symbolic_tuple_value (kind : V.sv_kind)
    (field_types : T.rty list) : V.symbolic_expansion =
  (* Generate the field values *)
  let field_values =
    List.map (fun sv_ty -> mk_fresh_symbolic_value kind sv_ty) field_types
  in
  let variant_id = None in
  let see = V.SeAdt (variant_id, field_values) in
  see

let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) :
    V.symbolic_expansion =
  (* Introduce a fresh symbolic value *)
  let boxed_value = mk_fresh_symbolic_value kind boxed_ty in
  let see = V.SeAdt (None, [ boxed_value ]) in
  see

(** Compute the expansion of an adt value.

    The function might return a list of 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)
    (kind : V.sv_kind) (adt_id : T.type_id) (generics : T.rgeneric_args)
    (ctx : C.eval_ctx) : V.symbolic_expansion list =
  match (adt_id, generics.regions, generics.types) with
  | T.AdtId def_id, _, _ ->
      compute_expanded_symbolic_non_assumed_adt_value expand_enumerations kind
        def_id generics ctx
  | T.Tuple, [], _ ->
      [ compute_expanded_symbolic_tuple_value kind generics.types ]
  | T.Assumed T.Box, [], [ boxed_ty ] ->
      [ compute_expanded_symbolic_box_value kind boxed_ty ]
  | _ ->
      raise
        (Failure "compute_expanded_symbolic_adt_value: unexpected combination")

let expand_symbolic_value_shared_borrow (config : C.config)
    (original_sv : V.symbolic_value) (original_sv_place : SA.mplace option)
    (ref_ty : T.rty) : cm_fun =
 fun cf ctx ->
  (* First, replace the projectors on borrows.
   * 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 fresh_borrow () =
    let bid' = C.fresh_borrow_id () in
    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 ]
      | _ -> raise (Failure "Unexpected")
    else None
  in
  (* The fresh symbolic value for the shared value *)
  let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
  (* Visitor to replace the projectors on borrows *)
  let obj =
    object (self)
      inherit [_] C.map_eval_ctx as super

      method! visit_Symbolic env sv =
        if same_symbolic_id sv 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

      (** We carefully updated {!visit_ASymbolic} so that {!visit_aproj} is called
          only on child projections (i.e., projections which appear in {!AEndedProjLoans}).
          The role of visit_aproj is then to check we don't have to expand symbolic
          values in child projections, because it should never happen
        *)
      method! visit_aproj proj_regions aproj =
        (match aproj with
        | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
            assert (not (same_symbolic_id sv original_sv))
        | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
        super#visit_aproj proj_regions aproj

      method! visit_ASymbolic proj_regions aproj =
        match aproj with
        | AEndedProjBorrows _ | AIgnoredProjBorrows ->
            (* We ignore borrows *) V.ASymbolic aproj
        | AProjLoans _ ->
            (* Loans are handled later *)
            V.ASymbolic 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))
        | AEndedProjLoans _ ->
            (* Sanity check: make sure there is nothing to expand inside the
             * children projections *)
            V.ASymbolic (self#visit_aproj proj_regions aproj)
    end
  in
  (* Call the visitor *)
  let ctx = obj#visit_eval_ctx None ctx in
  (* Finally, replace the projectors on loans *)
  let bids = !borrows in
  assert (not (V.BorrowId.Set.is_empty bids));
  let see = V.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
  (* Call the continuation *)
  let expr = cf ctx in
  (* Update the synthesized program *)
  S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place see
    expr

(** TODO: simplify and merge with the other expansion function *)
let expand_symbolic_value_borrow (config : C.config)
    (original_sv : V.symbolic_value) (original_sv_place : SA.mplace option)
    (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) :
    cm_fun =
 fun cf ctx ->
  (* Check that we are allowed to expand the reference *)
  assert (not (region_in_set region ctx.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 sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
      let bid = C.fresh_borrow_id () in
      let see = V.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
      (* Apply the continuation *)
      let expr = cf ctx in
      (* Update the synthesized program *)
      S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place
        see expr
  | T.Shared ->
      expand_symbolic_value_shared_borrow config original_sv original_sv_place
        ref_ty cf ctx

(** A small helper.

    Apply a branching symbolic expansion to a context and execute all the
    branches. Note that the expansion is optional for every branch (this is
    used for integer expansion: see {!expand_symbolic_int}).
    
    [see_cf_l]: list of pairs (optional symbolic expansion, continuation).
    We use [None] for the symbolic expansion for the [_] (default) case of the
    integer expansions.
    The continuation are used to execute the content of the branches, but not
    what comes after.

    [cf_after_join]: this continuation is called *after* the branches have been evaluated.
    We need this continuation separately (i.e., we can't compose it with the
    continuations in [see_cf_l]) because we perform a join *before* calling it.
*)
let apply_branching_symbolic_expansions_non_borrow (config : C.config)
    (sv : V.symbolic_value) (sv_place : SA.mplace option)
    (see_cf_l : (V.symbolic_expansion option * st_cm_fun) list)
    (cf_after_join : st_m_fun) : m_fun =
 fun ctx ->
  assert (see_cf_l <> []);
  (* Apply the symbolic expansion in the context and call the continuation *)
  let resl =
    List.map
      (fun (see_opt, cf_br) ->
        (* Remember the initial context for printing purposes *)
        let ctx0 = ctx in
        (* Expansion *)
        let ctx =
          match see_opt with
          | None -> ctx
          | Some see -> apply_symbolic_expansion_non_borrow config sv see ctx
        in
        (* Debug *)
        log#ldebug
          (lazy
            ("apply_branching_symbolic_expansions_non_borrow: "
            ^ symbolic_value_to_string ctx0 sv
            ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
            ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
        (* Continuation *)
        cf_br cf_after_join ctx)
      see_cf_l
  in
  (* Collect the result: either we computed no subterm, or we computed all
   * of them *)
  let subterms =
    match resl with
    | Some _ :: _ -> Some (List.map Option.get resl)
    | None :: _ ->
        List.iter (fun res -> assert (res = None)) resl;
        None
    | _ -> raise (Failure "Unreachable")
  in
  (* Synthesize and return *)
  let seel = List.map fst see_cf_l in
  S.synthesize_symbolic_expansion sv sv_place seel subterms

let expand_symbolic_bool (config : C.config) (sv : V.symbolic_value)
    (sv_place : SA.mplace option) (cf_true : st_cm_fun) (cf_false : st_cm_fun)
    (cf_after_join : st_m_fun) : m_fun =
 fun ctx ->
  (* Compute the expanded value *)
  let original_sv = sv in
  let original_sv_place = sv_place in
  let rty = original_sv.V.sv_ty in
  assert (rty = T.Literal PV.Bool);
  (* Expand the symbolic value to true or false and continue execution *)
  let see_true = V.SeLiteral (PV.Bool true) in
  let see_false = V.SeLiteral (PV.Bool false) in
  let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in
  (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
  apply_branching_symbolic_expansions_non_borrow config original_sv
    original_sv_place seel cf_after_join ctx

let expand_symbolic_value_no_branching (config : C.config)
    (sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun =
 fun cf ctx ->
  (* Debug *)
  log#ldebug
    (lazy
      ("expand_symbolic_value_no_branching:" ^ symbolic_value_to_string ctx sv));
  (* Remember the initial context for printing purposes *)
  let ctx0 = ctx in
  (* 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 = sv in
  let original_sv_place = sv_place in
  let rty = original_sv.V.sv_ty in
  let cc : cm_fun =
   fun cf ctx ->
    match rty with
    (* ADTs *)
    | T.Adt (adt_id, generics) ->
        (* Compute the expanded value *)
        let allow_branching = false in
        let seel =
          compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id
            generics ctx
        in
        (* There should be exacly one branch *)
        let see = Collections.List.to_cons_nil seel in
        (* Apply in the context *)
        let ctx =
          apply_symbolic_expansion_non_borrow config original_sv see ctx
        in
        (* Call the continuation *)
        let expr = cf ctx in
        (* Update the synthesized program *)
        S.synthesize_symbolic_expansion_no_branching original_sv
          original_sv_place see expr
    (* Borrows *)
    | T.Ref (region, ref_ty, rkind) ->
        expand_symbolic_value_borrow config original_sv original_sv_place region
          ref_ty rkind cf ctx
    | _ ->
        raise
          (Failure
             ("expand_symbolic_value_no_branching: unexpected type: "
            ^ T.show_rty rty))
  in
  (* Debug *)
  let cc =
    comp_unit cc (fun ctx ->
        log#ldebug
          (lazy
            ("expand_symbolic_value_no_branching: "
            ^ symbolic_value_to_string ctx0 sv
            ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
            ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
        (* Sanity check: the symbolic value has disappeared *)
        assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx)))
  in
  (* Continue *)
  cc cf ctx

let expand_symbolic_adt (config : C.config) (sv : V.symbolic_value)
    (sv_place : SA.mplace option) (cf_branches : st_cm_fun)
    (cf_after_join : st_m_fun) : m_fun =
 fun ctx ->
  (* Debug *)
  log#ldebug (lazy ("expand_symbolic_adt:" ^ symbolic_value_to_string ctx sv));
  (* 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 = sv in
  let original_sv_place = sv_place in
  let rty = original_sv.V.sv_ty in
  (* Execute *)
  match rty with
  (* ADTs *)
  | T.Adt (adt_id, generics) ->
      let allow_branching = true in
      (* Compute the expanded value *)
      let seel =
        compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id
          generics ctx
      in
      (* Apply *)
      let seel = List.map (fun see -> (Some see, cf_branches)) seel in
      apply_branching_symbolic_expansions_non_borrow config original_sv
        original_sv_place seel cf_after_join ctx
  | _ ->
      raise
        (Failure ("expand_symbolic_adt: unexpected type: " ^ T.show_rty rty))

let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
    (sv_place : SA.mplace option) (int_type : T.integer_type)
    (tgts : (V.scalar_value * st_cm_fun) list) (otherwise : st_cm_fun)
    (cf_after_join : st_m_fun) : m_fun =
  (* Sanity check *)
  assert (sv.V.sv_ty = T.Literal (PV.Integer int_type));
  (* For all the branches of the switch, we expand the symbolic value
   * to the value given by the branch and execute the branch statement.
   * For the otherwise branch, we leave the symbolic value as it is
   * (because this branch doesn't precisely define which should be the
   * value of the scrutinee...) and simply execute the otherwise statement.
   *
   * First, generate the list of pairs:
   * (optional expansion, statement to execute)
   *)
  let seel =
    List.map (fun (v, cf) -> (Some (V.SeLiteral (PV.Scalar v)), cf)) tgts
  in
  let seel = List.append seel [ (None, otherwise) ] in
  (* Then expand and evaluate - this generates the proper symbolic AST *)
  apply_branching_symbolic_expansions_non_borrow config sv sv_place seel
    cf_after_join

(** Expand all the symbolic values which contain borrows.
    Allows us to restrict ourselves to a simpler model for the projectors over
    symbolic values.
    
    Fails if doing this requires to do a branching (because we need to expand
    an enumeration with strictly more than one variant, a slice, etc.) or if
    we need to expand a recursive type (because this leads to looping).
 *)
let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
 fun cf ctx ->
  (* The visitor object, to look for symbolic values in the concrete environment *)
  let obj =
    object
      inherit [_] C.iter_eval_ctx

      method! visit_Symbolic _ sv =
        if ty_has_borrows ctx.type_context.type_infos sv.V.sv_ty then
          raise (FoundSymbolicValue sv)
        else ()

      (** Don't enter abstractions *)
      method! visit_abs _ _ = ()
    end
  in

  let rec expand : cm_fun =
   fun cf ctx ->
    try
      (* We reverse the environment before exploring it - this way the values
         get expanded in a more "logical" order (this is only for convenience) *)
      obj#visit_env () (List.rev ctx.env);
      (* Nothing to expand: continue *)
      cf ctx
    with FoundSymbolicValue sv ->
      (* Expand and recheck the environment *)
      log#ldebug
        (lazy
          ("greedy_expand_symbolics_with_borrows: about to expand: "
          ^ symbolic_value_to_string ctx sv));
      let cc : cm_fun =
        match sv.V.sv_ty with
        | T.Adt (AdtId def_id, _) ->
            (* {!expand_symbolic_value_no_branching} checks if there are branchings,
             * but we prefer to also check it here - this leads to cleaner messages
             * and debugging *)
            let def = C.ctx_lookup_type_decl ctx def_id in
            (match def.kind with
            | T.Struct _ | T.Enum ([] | [ _ ]) -> ()
            | T.Enum (_ :: _) ->
                raise
                  (Failure
                     ("Attempted to greedily expand a symbolic enumeration \
                       with > 1 variants (option \
                       [greedy_expand_symbolics_with_borrows] of [config]): "
                     ^ Print.name_to_string def.name))
            | T.Opaque ->
                raise (Failure "Attempted to greedily expand an opaque type"));
            (* Also, we need to check if the definition is recursive *)
            if C.ctx_type_decl_is_rec ctx def_id then
              raise
                (Failure
                   ("Attempted to greedily expand a recursive definition \
                     (option [greedy_expand_symbolics_with_borrows] of \
                     [config]): "
                   ^ Print.name_to_string def.name))
            else expand_symbolic_value_no_branching config sv None
        | T.Adt ((Tuple | Assumed Box), _) | T.Ref (_, _, _) ->
            (* Ok *)
            expand_symbolic_value_no_branching config sv None
        | T.Adt (Assumed (Array | Slice | Str), _) ->
            (* We can't expand those *)
            raise
              (Failure
                 "Attempted to greedily expand an ADT which can't be expanded ")
        | T.TypeVar _ | T.Literal _ | Never | T.TraitType _ | T.Arrow _ ->
            raise (Failure "Unreachable")
      in
      (* Compose and continue *)
      comp cc expand cf ctx
  in
  (* Apply *)
  expand cf ctx

let greedy_expand_symbolic_values (config : C.config) : cm_fun =
 fun cf ctx ->
  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