summaryrefslogtreecommitdiff
path: root/compiler/Values.ml
blob: f6f4d1b6a0f569bc8c9523f578081ea0e55fa8b7 (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
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
open Identifiers
open Types
module PrimitiveValues = PrimitiveValues

(* TODO(SH): I often write "abstract" (value, borrow content, etc.) while I should
 * write "abstraction" (because those values are not abstract, they simply are
 * inside abstractions) *)

module BorrowId = IdGen ()
module SymbolicValueId = IdGen ()
module AbstractionId = IdGen ()
module FunCallId = IdGen ()
module LoopId = IdGen ()

type big_int = PrimitiveValues.big_int [@@deriving show, ord]
type scalar_value = PrimitiveValues.scalar_value [@@deriving show, ord]
type primitive_value = PrimitiveValues.primitive_value [@@deriving show, ord]
type symbolic_value_id = SymbolicValueId.id [@@deriving show, ord]

(** The kind of a symbolic value, which precises how the value was generated.

    TODO: remove? This is not useful anymore.
  *)
type sv_kind =
  | FunCallRet  (** The value is the return value of a function call *)
  | FunCallGivenBack
      (** The value is a borrowed value given back by an abstraction
          (happens when giving a borrow to a function: when the abstraction
          introduced to model the function call ends we reintroduce a symbolic
          value in the context for the value modified by the abstraction through
          the borrow).
       *)
  | SynthInput
      (** The value is an input value of the function whose body we are
          currently synthesizing.
       *)
  | SynthRetGivenBack
      (** The value is a borrowed value that the function whose body we are
          synthesizing returned, and which was given back because we ended
          one of the lifetimes of this function (we do this to synthesize
          the backward functions).
       *)
  | SynthInputGivenBack
      (** The value was given back upon ending one of the input abstractions *)
  | Global  (** The value is a global *)
  | LoopOutput  (** The output of a loop (seen as a forward computation) *)
  | LoopGivenBack
      (** A value given back by a loop (when ending abstractions while going backwards) *)
  | LoopJoin
      (** The result of a loop join (when computing loop fixed points) *)
[@@deriving show, ord]

(** Ancestor for {!symbolic_value} iter visitor *)
class ['self] iter_symbolic_value_base =
  object (_self : 'self)
    inherit [_] VisitorsRuntime.iter
    method visit_sv_kind : 'env -> sv_kind -> unit = fun _ _ -> ()
    method visit_rty : 'env -> rty -> unit = fun _ _ -> ()

    method visit_symbolic_value_id : 'env -> symbolic_value_id -> unit =
      fun _ _ -> ()
  end

(** Ancestor for {!symbolic_value} map visitor for *)
class ['self] map_symbolic_value_base =
  object (_self : 'self)
    inherit [_] VisitorsRuntime.map
    method visit_sv_kind : 'env -> sv_kind -> sv_kind = fun _ x -> x
    method visit_rty : 'env -> rty -> rty = fun _ x -> x

    method visit_symbolic_value_id
        : 'env -> symbolic_value_id -> symbolic_value_id =
      fun _ x -> x
  end

(** A symbolic value *)
type symbolic_value = {
  sv_kind : sv_kind;
  sv_id : symbolic_value_id;
  sv_ty : rty;
}
[@@deriving
  show,
    ord,
    visitors
      {
        name = "iter_symbolic_value";
        variety = "iter";
        ancestors = [ "iter_symbolic_value_base" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      },
    visitors
      {
        name = "map_symbolic_value";
        variety = "map";
        ancestors = [ "map_symbolic_value_base" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      }]

type borrow_id = BorrowId.id [@@deriving show, ord]
type borrow_id_set = BorrowId.Set.t [@@deriving show, ord]
type loan_id = BorrowId.id [@@deriving show, ord]
type loan_id_set = BorrowId.Set.t [@@deriving show, ord]

(** Ancestor for {!typed_value} iter visitor *)
class ['self] iter_typed_value_base =
  object (self : 'self)
    inherit [_] iter_symbolic_value

    method visit_primitive_value : 'env -> primitive_value -> unit =
      fun _ _ -> ()

    method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
    method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
    method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
    method visit_borrow_id : 'env -> borrow_id -> unit = fun _ _ -> ()
    method visit_loan_id : 'env -> loan_id -> unit = fun _ _ -> ()

    method visit_borrow_id_set : 'env -> borrow_id_set -> unit =
      fun env ids -> BorrowId.Set.iter (self#visit_borrow_id env) ids

    method visit_loan_id_set : 'env -> loan_id_set -> unit =
      fun env ids -> BorrowId.Set.iter (self#visit_loan_id env) ids
  end

(** Ancestor for {!typed_value} map visitor for *)
class ['self] map_typed_value_base =
  object (self : 'self)
    inherit [_] map_symbolic_value

    method visit_primitive_value : 'env -> primitive_value -> primitive_value =
      fun _ cv -> cv

    method visit_erased_region : 'env -> erased_region -> erased_region =
      fun _ r -> r

    method visit_ety : 'env -> ety -> ety = fun _ ty -> ty
    method visit_variant_id : 'env -> variant_id -> variant_id = fun _ x -> x
    method visit_borrow_id : 'env -> borrow_id -> borrow_id = fun _ id -> id
    method visit_loan_id : 'env -> loan_id -> loan_id = fun _ id -> id

    method visit_borrow_id_set : 'env -> borrow_id_set -> borrow_id_set =
      fun env ids -> BorrowId.Set.map (self#visit_borrow_id env) ids

    method visit_loan_id_set : 'env -> loan_id_set -> loan_id_set =
      fun env ids -> BorrowId.Set.map (self#visit_loan_id env) ids
  end

(** An untyped value, used in the environments *)
type value =
  | Primitive of primitive_value  (** Non-symbolic primitive value *)
  | Adt of adt_value  (** Enumerations and structures *)
  | Bottom  (** No value (uninitialized or moved value) *)
  | Borrow of borrow_content  (** A borrowed value *)
  | Loan of loan_content  (** A loaned value *)
  | Symbolic of symbolic_value
      (** Borrow projector over a symbolic value.
      
          Note that contrary to the abstraction-values case, symbolic values
          appearing in regular values are interpreted as *borrow* projectors,
          they can never be *loan* projectors.
       *)

and adt_value = {
  variant_id : variant_id option;
  field_values : typed_value list;
}

and borrow_content =
  | SharedBorrow of mvalue * borrow_id
      (** A shared borrow.
      
          We remember the shared value which was borrowed as a meta value.
          This is necessary for synthesis: upon translating to "pure" values,
          we can't perform any lookup because we don't have an environment
          anymore. Note that it is ok to keep the shared value and copy
          the shared value this way, because shared values are immutable
          for as long as they are shared (i.e., as long as we can use the
          shared borrow).
       *)
  | MutBorrow of borrow_id * typed_value  (** A mutably borrowed value. *)
  | ReservedMutBorrow of mvalue * borrow_id
      (** A reserved mut borrow.

          This is used to model {{: https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html} two-phase borrows}.
          When evaluating a two-phase mutable borrow, we first introduce a reserved
          borrow which behaves like a shared borrow, until the moment we actually *use*
          the borrow: at this point, we end all the other shared borrows (or reserved
          borrows - though there shouldn't be any other reserved borrows) of this value
          and replace the reserved borrow with a mutable borrow (as well as the shared
          loan with a mutable loan).
          
          A simple use case of two-phase borrows:
          {[
            let mut v = Vec::new();
            v.push(v.len());
          ]}
          
          This gets desugared to (something similar to) the following MIR:
          {[
            v = Vec::new();
            v1 = &mut v;
            v2 = &v; // We need this borrow, but v has already been mutably borrowed!
            l = Vec::len(move v2); // We need v2 here, and v1 *below*
            Vec::push(move v1, move l); // In practice, v1 gets promoted only here
          ]}
          
          The meta-value is used for the same purposes as with shared borrows,
          at the exception that in the case of reserved borrows it is not
          *necessary* for the synthesis: we keep it only as meta-information.
          To be more precise:
          - when generating the synthesized program, we may need to convert
            shared borrows to pure values
          - we never need to do so for reserved borrows: such borrows must
            be promoted at the moment we use them (meaning in the synthesis we
            convert a *mutable* borrow to a pure value). However, we save
            meta-data about the assignments, which is used to make the code
            cleaner: when generating this meta-data, we may need to convert
            reserved borrows to pure values, in which situation we convert
            the meta-value we stored in the reserved borrow.
       *)

and loan_content =
  | SharedLoan of loan_id_set * typed_value
  | MutLoan of loan_id
      (** TODO: we might want to add a set of borrow ids (useful for reserved
          borrows, and extremely useful when giving shared values to abstractions).
       *)

(** "Meta"-value: information we store for the synthesis.

     Note that we never automatically visit the meta-values with the
     visitors: they really are meta information, and shouldn't be considered
     as part of the environment during a symbolic execution.
     
     TODO: we may want to create wrappers, to prevent accidently mixing meta
     values and regular values.
 *)
and mvalue = typed_value

(** "Regular" typed value (we map variables to typed values) *)
and typed_value = { value : value; ty : ety }
[@@deriving
  show,
    ord,
    visitors
      {
        name = "iter_typed_value_visit_mvalue";
        variety = "iter";
        ancestors = [ "iter_typed_value_base" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      },
    visitors
      {
        name = "map_typed_value_visit_mvalue";
        variety = "map";
        ancestors = [ "map_typed_value_base" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      }]

(** "Meta"-symbolic value.

     See the explanations for {!mvalue}

     TODO: we may want to create wrappers, to prevent mixing meta values
     and regular values.
 *)
type msymbolic_value = symbolic_value [@@deriving show, ord]

class ['self] iter_typed_value =
  object (_self : 'self)
    inherit [_] iter_typed_value_visit_mvalue

    (** We have to override the {!iter_typed_value_visit_mvalue.visit_mvalue} method,
        to ignore meta-values *)
    method! visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> ()

    method visit_msymbolic_value : 'env -> msymbolic_value -> unit =
      fun _ _ -> ()
  end

class ['self] map_typed_value =
  object (_self : 'self)
    inherit [_] map_typed_value_visit_mvalue

    (** We have to override the {!iter_typed_value_visit_mvalue.visit_mvalue} method,
        to ignore meta-values *)
    method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x

    method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value =
      fun _ m -> m
  end

(** When giving shared borrows to functions (i.e., inserting shared borrows inside
    abstractions) we need to reborrow the shared values. When doing so, we lookup
    the shared values and apply some special projections to the shared value
    (until we can't go further, i.e., we find symbolic values which may get
    expanded upon reading them later), which don't generate avalues but
    sets of borrow ids and symbolic values.
    
    Note that as shared values can't get modified it is ok to forget the
    structure of the values we projected, and only keep the set of borrows
    (and symbolic values).
    
    TODO: we may actually need to remember the structure, in order to know
    which borrows are inside which other borrows...
*)
type abstract_shared_borrow =
  | AsbBorrow of borrow_id
  | AsbProjReborrows of symbolic_value * rty
[@@deriving
  show,
    ord,
    visitors
      {
        name = "iter_abstract_shared_borrow";
        variety = "iter";
        ancestors = [ "iter_typed_value" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      },
    visitors
      {
        name = "map_abstract_shared_borrow";
        variety = "map";
        ancestors = [ "map_typed_value" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      }]

(** A set of abstract shared borrows *)
type abstract_shared_borrows = abstract_shared_borrow list
[@@deriving
  show,
    ord,
    visitors
      {
        name = "iter_abstract_shared_borrows";
        variety = "iter";
        ancestors = [ "iter_abstract_shared_borrow" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      },
    visitors
      {
        name = "map_abstract_shared_borrows";
        variety = "map";
        ancestors = [ "map_abstract_shared_borrow" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      }]

(** Ancestor for {!aproj} iter visitor *)
class ['self] iter_aproj_base =
  object (_self : 'self)
    inherit [_] iter_abstract_shared_borrows
  end

(** Ancestor for {!aproj} map visitor *)
class ['self] map_aproj_base =
  object (_self : 'self)
    inherit [_] map_abstract_shared_borrows
  end

type aproj =
  | AProjLoans of symbolic_value * (msymbolic_value * aproj) list
      (** A projector of loans over a symbolic value.
      
          Note that the borrows of a symbolic value may be spread between
          different abstractions, meaning that the projector of loans might
          receive *several* (symbolic) given back values.
          
          This is the case in the following example:
          {[
            fn f<'a> (...) -> (&'a mut u32, &'a mut u32);
            fn g<'b, 'c>(p : (&'b mut u32, &'c mut u32));

            let p = f(...);
            g(move p);

            // Symbolic context after the call to g:
            // abs'a {'a} { [s@0 <: (&'a mut u32, &'a mut u32)] }
            //
            // abs'b {'b} { (s@0 <: (&'b mut u32, &'c mut u32)) }
            // abs'c {'c} { (s@0 <: (&'b mut u32, &'c mut u32)) }
          ]}
          
          Upon evaluating the call to [f], we introduce a symbolic value [s@0]
          and a projector of loans (projector loans from the region 'c).
          This projector will later receive two given back values: one for
          'a and one for 'b.
          
          We accumulate those values in the list of projections (note that
          the meta value stores the value which was given back).
          
          We can later end the projector of loans if [s@0] is not referenced
          anywhere in the context below a projector of borrows which intersects
          this projector of loans.
       *)
  | AProjBorrows of symbolic_value * rty
      (** Note that an AProjBorrows only operates on a value which is not below
          a shared loan: under a shared loan, we use {!abstract_shared_borrow}.
          
          Also note that once given to a borrow projection, a symbolic value
          can't get updated/expanded: this means that we don't need to save
          any meta-value here.
       *)
  | AEndedProjLoans of msymbolic_value * (msymbolic_value * aproj) list
      (** An ended projector of loans over a symbolic value.
      
          See the explanations for {!AProjLoans}
          
          Note that we keep the original symbolic value as a meta-value.
       *)
  | AEndedProjBorrows of msymbolic_value
      (** The only purpose of {!AEndedProjBorrows} is to store, for synthesis
          purposes, the symbolic value which was generated and given back upon
          ending the borrow.
       *)
  | AIgnoredProjBorrows
[@@deriving
  show,
    ord,
    visitors
      {
        name = "iter_aproj";
        variety = "iter";
        ancestors = [ "iter_aproj_base" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      },
    visitors
      {
        name = "map_aproj";
        variety = "map";
        ancestors = [ "map_aproj_base" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      }]

type region = RegionVarId.id Types.region [@@deriving show, ord]
type region_var_id = RegionVarId.id [@@deriving show, ord]
type region_id = RegionId.id [@@deriving show, ord]
type region_id_set = RegionId.Set.t [@@deriving show, ord]
type abstraction_id = AbstractionId.id [@@deriving show, ord]
type abstraction_id_set = AbstractionId.Set.t [@@deriving show, ord]

(** Ancestor for {!typed_avalue} iter visitor *)
class ['self] iter_typed_avalue_base =
  object (self : 'self)
    inherit [_] iter_aproj
    method visit_region_var_id : 'env -> region_var_id -> unit = fun _ _ -> ()

    method visit_region : 'env -> region -> unit =
      fun env r ->
        match r with
        | Static -> ()
        | Var rid -> self#visit_region_var_id env rid

    method visit_region_id : 'env -> region_id -> unit = fun _ _ -> ()

    method visit_region_id_set : 'env -> region_id_set -> unit =
      fun env ids -> RegionId.Set.iter (self#visit_region_id env) ids

    method visit_abstraction_id : 'env -> abstraction_id -> unit = fun _ _ -> ()

    method visit_abstraction_id_set : 'env -> abstraction_id_set -> unit =
      fun env ids -> AbstractionId.Set.iter (self#visit_abstraction_id env) ids
  end

(** Ancestor for {!typed_avalue} map visitor *)
class ['self] map_typed_avalue_base =
  object (self : 'self)
    inherit [_] map_aproj

    method visit_region_var_id : 'env -> region_var_id -> region_var_id =
      fun _ x -> x

    method visit_region : 'env -> region -> region =
      fun env r ->
        match r with
        | Static -> Static
        | Var rid -> Var (self#visit_region_var_id env rid)

    method visit_region_id : 'env -> region_id -> region_id = fun _ x -> x

    method visit_region_id_set : 'env -> region_id_set -> region_id_set =
      fun env ids -> RegionId.Set.map (self#visit_region_id env) ids

    method visit_abstraction_id : 'env -> abstraction_id -> abstraction_id =
      fun _ x -> x

    method visit_abstraction_id_set
        : 'env -> abstraction_id_set -> abstraction_id_set =
      fun env ids -> AbstractionId.Set.map (self#visit_abstraction_id env) ids
  end

(** Abstraction values are used inside of abstractions to properly model
    borrowing relations introduced by function calls.

    When calling a function, we lose information about the borrow graph:
    part of it is thus "abstracted" away.
*)
type avalue =
  | APrimitive of primitive_value
      (** TODO: remove. We actually don't use that for the synthesis, but the
          meta-values.
       
          Note that this case is not used in the projections to keep track of the
          borrow graph (because there are no borrows in "concrete" values!) but
          to correctly instantiate the backward functions (we may give back some
          values at different moments: we need to remember what those values were
          precisely). Also note that even though avalues and values are not the
          same, once values are projected to avalues, those avalues still have
          the structure of the original values (this is necessary, again, to
          correctly instantiate the backward functions)
       *)
  | AAdt of adt_avalue
  | ABottom
  | ALoan of aloan_content
  | ABorrow of aborrow_content
  | ASymbolic of aproj
  | AIgnored
      (** A value which doesn't contain borrows, or which borrows we
          don't own and thus ignore *)

and adt_avalue = {
  variant_id : (VariantId.id option[@opaque]);
  field_values : typed_avalue list;
}

(** A loan content as stored in an abstraction.

    Note that the children avalues are independent of the parent avalues.
    For instance, the child avalue contained in an {!AMutLoan} will likely
    contain other, independent loans.
    Keeping track of the hierarchy is not necessary to maintain the borrow graph
    (which is the primary role of the abstractions), but it is necessary
    to properly instantiate the backward functions when generating the pure
    translation.
*)
and aloan_content =
  | AMutLoan of loan_id * typed_avalue
      (** A mutable loan owned by an abstraction.
         
          Example:
          ========
          {[
            fn f<'a>(...) -> &'a mut &'a mut u32;

            let px = f(...);
          ]}
          
          We get (after some symbolic exansion):
          {[
            abs0 {
              a_mut_loan l0 (a_mut_loan l1 _)
            }
            px -> mut_borrow l0 (mut_borrow @s1)
          ]}
       *)
  | ASharedLoan of loan_id_set * typed_value * typed_avalue
      (** A shared loan owned by an abstraction.

          Example:
          ========
          {[
            fn f<'a>(...) -> &'a u32;

            let px = f(...);
          ]}
          
          We get:
          {[
            abs0 { a_shared_loan {l0} @s0 _ }
            px -> shared_loan l0
          ]}
     *)
  | AEndedMutLoan of {
      child : typed_avalue;
      given_back : typed_avalue;
      given_back_meta : mvalue;
    }
      (** An ended mutable loan in an abstraction.
          We need it because abstractions must keep track of the values
          we gave back to them, so that we can correctly instantiate
          backward functions.
          
          Rk.: *DO NOT* use [visit_AEndedMutLoan]. If we update the order of
          the arguments and you forget to swap them at the level of
          [visit_AEndedMutLoan], you will not notice it.          
      
          Example:
          ========
          {[
            abs0 { a_mut_loan l0 ⊥ }
            x -> mut_borrow l0 (U32 3)
          ]}
          
          After ending [l0]:
          
          {[
            abs0 { a_ended_mut_loan { given_back = U32 3; child = ⊥; }
            x -> ⊥
          ]}
       *)
  | AEndedSharedLoan of typed_value * typed_avalue
      (** Similar to {!AEndedMutLoan} but in this case there are no avalues to
          give back. We keep the shared value because it now behaves as a
          "regular" value (which contains borrows we might want to end...).
       *)
  | AIgnoredMutLoan of loan_id option * typed_avalue
      (** An ignored mutable loan.
      
          We need to keep track of ignored mutable loans, because we may have
          to apply projections on the values given back to those loans (say
          you have a borrow of type [&'a mut &'b mut], in the abstraction 'b,
          the outer loan is ignored, however you need to keep track of it so
          that when ending the borrow corresponding to 'a you can correctly
          project on the inner value).

          Note that we need to do so only for borrows consumed by parent
          abstractions, hence the optional loan id.
       
          Example:
          ========
          {[
            fn f<'a,'b>(...) -> &'a mut &'b mut u32;
            let x = f(...);

            > abs'a { a_mut_loan l0 (a_ignored_mut_loan l1 ⊥) }
            > abs'b { a_ignored_mut_loan l0 (a_mut_loan l1 ⊥) }
            > x -> mut_borrow l0 (mut_borrow l1 @s1)
          ]}
       *)
  | AEndedIgnoredMutLoan of {
      child : typed_avalue;
      given_back : typed_avalue;
      given_back_meta : mvalue;
    }
      (** Similar to {!AEndedMutLoan}, for ignored loans.

           Rk.: *DO NOT* use [visit_AEndedIgnoredMutLoan].
           See the comment for {!AEndedMutLoan}.
       *)
  | AIgnoredSharedLoan of typed_avalue
      (** An ignored shared loan.
            
          Example:
          ========
          {[
            fn f<'a,'b>(...) -> &'a &'b u32;
            let x = f(...);

            > abs'a { a_shared_loan {l0} (shared_borrow l1) (a_ignored_shared_loan ⊥) }
            > abs'b { a_ignored_shared_loan (a_shared_loan {l1} @s1 ⊥) }
            > x -> shared_borrow l0
          ]}
       *)

(** Note that when a borrow content is ended, it is replaced by ⊥ (while
    we need to track ended loans more precisely, especially because of their
    children values).

    Note that contrary to {!aloan_content}, here the children avalues are
    not independent of the parent avalues. For instance, a value
    [AMutBorrow (_, AMutBorrow (_, ...)] (ignoring the types) really is
    to be seen like a [mut_borrow ... (mut_borrow ...)].
    
    TODO: be more precise about the ignored borrows (keep track of the borrow
    ids)?
*)
and aborrow_content =
  | AMutBorrow of mvalue * borrow_id * typed_avalue
      (** A mutable borrow owned by an abstraction.
      
          Is used when an abstraction "consumes" borrows, when giving borrows
          as arguments to a function.

          Example:
          ========
          {[
            fn f<'a>(px : &'a mut u32);

            > x -> mut_loan l0
            > px -> mut_borrow l0 (U32 0)

            f(move px);

            > x -> mut_loan l0
            > px -> ⊥
            > abs0 { a_mut_borrow l0 (U32 0) }
          ]}
          
          The meta-value stores the initial value on which the projector was
          applied, which reduced to this mut borrow. This meta-information
          is only used for the synthesis.
          TODO: do we really use it actually?
     *)
  | ASharedBorrow of borrow_id
      (** A shared borrow owned by an abstraction.
    
          Example:
          ========
          {[
            fn f<'a>(px : &'a u32);

            > x -> shared_loan {l0} (U32 0)
            > px -> shared_borrow l0

            f(move px);

            > x -> shared_loan {l0} (U32 0)
            > px -> ⊥
            > abs0 { a_shared_borrow l0 }
          ]}
     *)
  | AIgnoredMutBorrow of borrow_id option * typed_avalue
      (** An ignored mutable borrow.
      
          We need to keep track of ignored mut borrows because when ending such
          borrows, we need to project the loans of the given back value to
          insert them in the proper abstractions.
          
          Note that we need to do so only for borrows consumed by parent
          abstractions (hence the optional borrow id).
          
          Rem.: we don't have an equivalent for shared borrows because if
          we ignore a shared borrow we don't need keep track it (we directly
          use {!AProjSharedBorrow} to project the shared value).

          TODO: the explanations below are obsolete

          Example:
          ========
          {[
            fn f<'a,'b>(ppx : &'a mut &'b mut u32);

            > x -> mut_loan l0
            > px -> mut_loan l1
            > ppx -> mut_borrow l1 (mut_borrow l0 (U32 0))

            f(move ppx);

            > x -> mut_loan l0
            > px -> mut_loan l1
            > ppx -> ⊥
            > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow None (U32 0)) } // TODO: duplication
            > abs'b {parents={abs'a}} { a_ignored_mut_borrow (Some l1) (a_mut_borrow l0 (U32 0)) }

            ... // abs'a ends

            > x -> mut_loan l0
            > px -> @s0
            > ppx -> ⊥
            > abs'b {
            >   a_ended_ignored_mut_borrow (a_proj_loans (@s0 <: &'b mut u32)) // <-- loan projector
            >                              (a_mut_borrow l0 (U32 0))
            > }

            ... // [@s0] gets expanded to [&mut l2 @s1]

            > x -> mut_loan l0
            > px -> &mut l2 @s1
            > ppx -> ⊥
            > abs'b {
            >   a_ended_ignored_mut_borrow (a_mut_loan l2) // <-- loan l2 is here
            >                              (a_mut_borrow l0 (U32 0))
            > }

          ]}

          Note that we could use AIgnoredMutLoan in the case the borrow id is not
          None, which would allow us to simplify the rules (to not have rules
          to specifically handle the case of AIgnoredMutBorrow with Some borrow
          id) and also remove the AEndedIgnoredMutBorrow variant.
          For now, the rules are implemented and it allows us to make the avalues
          more precise and clearer, so we will keep it that way.
   
          TODO: this is annoying, we are duplicating information. Maybe we
          could introduce an "Ignored" value? We have to pay attention to
          two things:
          - introducing ⊥ when ignoring a value is not always possible, because
            we check whether the borrowed value contains ⊥ when giving back a
            borrowed value (if it is the case we give back ⊥, otherwise we
            introduce a symbolic value). This is necessary when ending nested
            borrows with the same lifetime: when ending the inner borrow we
            actually give back a value, however when ending the outer borrow
            we need to give back ⊥.
            TODO: actually we don't do that anymore, we check if the borrowed
            avalue contains ended regions (which is cleaner and more robust).
          - we may need to remember the precise values given to the
            abstraction so that we can properly call the backward functions
            when generating the pure translation.
       *)
  | AEndedMutBorrow of msymbolic_value * typed_avalue
      (** The sole purpose of {!AEndedMutBorrow} is to store the (symbolic) value
          that we gave back as a meta-value, to help with the synthesis.

          We also remember the child {!avalue} because this structural information
          is useful for the synthesis (but not for the symbolic execution):
          in practice the child value should only contain ended borrows, ignored
          values, bottom values, etc.
       *)
  | AEndedSharedBorrow
      (** We don't really need {!AEndedSharedBorrow}: we simply want to be
          precise, and not insert ⊥ when ending borrows.
       *)
  | AEndedIgnoredMutBorrow of {
      child : typed_avalue;
      given_back_loans_proj : typed_avalue;
      given_back_meta : msymbolic_value;
          (** [given_back_meta] is used to store the (symbolic) value we gave back
              upon ending the borrow.

              Rk.: *DO NOT* use [visit_AEndedIgnoredMutLoan].
              See the comment for {!AEndedMutLoan}.
          *)
    }  (** See the explanations for {!AIgnoredMutBorrow} *)
  | AProjSharedBorrow of abstract_shared_borrows
      (** A projected shared borrow.

          When giving shared borrows as arguments to function calls, we
          introduce new borrows to keep track of the fact that the function
          might reborrow values inside. Note that as shared values are immutable,
          we don't really need to remember the structure of the shared values.

          Example:
          ========
          Below, when calling [f], we need to introduce one shared borrow per
          borrow in the argument.
          {[
            fn f<'a,'b>(pppx : &'a &'b &'c mut u32);

            > x    -> mut_loan l0
            > px   -> shared_loan {l1} (mut_borrow l0 (U32 0))
            > ppx  -> shared_loan {l2} (shared_borrow l1)
            > pppx -> shared_borrow l2

            f(move pppx);

            > x    -> mut_loan l0
            > px   -> shared_loan {l1, l3, l4} (mut_borrow l0 (U32 0))
            > ppx  -> shared_loan {l2} (shared_borrow l1)
            > pppx -> ⊥
            > abs'a { a_shared_borrow {l2} }
            > abs'b { a_proj_shared_borrow {l3} } // l3 reborrows l1
            > abs'c { a_proj_shared_borrow {l4} } // l4 reborrows l0
          ]}

          Rem.: we introduce {!AProjSharedBorrow} only when we project a shared
          borrow *which is ignored* (i.e., the shared borrow doesn't belong to
          the current abstraction). The reason is that if the shared borrow
          belongs to the abstraction, then by introducing a shared borrow inside
          the abstraction we make sure the whole value is shared (and thus immutable)
          for as long as the abstraction lives, meaning reborrowing subvalues
          is redundant. However, if the borrow doesn't belong to the abstraction,
          we need to project the shared values because it may contain some
          borrows which *do* belong to the current abstraction.

          TODO: maybe we should factorized [ASharedBorrow] and [AProjSharedBorrow].
       *)

(* TODO: the type of avalues doesn't make sense for loan avalues: they currently
   are typed as [& (mut) T] instead of [T]...
*)
and typed_avalue = { value : avalue; ty : rty }
[@@deriving
  show,
    ord,
    visitors
      {
        name = "iter_typed_avalue";
        variety = "iter";
        ancestors = [ "iter_typed_avalue_base" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      },
    visitors
      {
        name = "map_typed_avalue";
        variety = "map";
        ancestors = [ "map_typed_avalue_base" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      }]

(** The kind of an abstraction, which keeps track of its origin *)
type abs_kind =
  | FunCall of (FunCallId.id * RegionGroupId.id)
      (** The abstraction was introduced because of a function call.

          It contains he identifier of the function call which introduced this
          abstraction, as well as the id of the backward function this
          abstraction stands for (backward functions are identified by the group
          of regions to which they are associated). This is not used by the
          symbolic execution: this is only used for pretty-printing and
          debugging in the symbolic AST, generated by the symbolic
          execution.
       *)
  | SynthInput of RegionGroupId.id
      (** The abstraction keeps track of the input values of the function
          we are currently synthesizing.

          We introduce one abstraction per (group of) region(s) in the function
          signature, the region group id identifies this group. Similarly to
          the [FunCall] case, this is not used by the symbolic execution.
       *)
  | SynthRet of RegionGroupId.id
      (** The abstraction "absorbed" the value returned by the function we
          are currently synthesizing

          See the explanations for [SynthInput].
       *)
  | Loop of LoopId.id  (** The abstraction corresponds to a loop *)
[@@deriving show, ord]

(** Abstractions model the parts in the borrow graph where the borrowing relations
    have been abstracted because of a function call.
    
    In order to model the relations between the borrows, we use "abstraction values",
    which are a special kind of value.
*)
type abs = {
  abs_id : abstraction_id;
  kind : (abs_kind[@opaque]);
  can_end : (bool[@opaque]);
      (** Controls whether the region can be ended or not.
          
          This allows to "pin" some regions, and is useful when generating
          backward functions.
          
          For instance, if we have: [fn f<'a, 'b>(...) -> (&'a mut T, &'b mut T)],
          when generating the backward function for 'a, we have to make sure we
          don't need to end the return region for 'b (if it is the case, it means
          the function doesn't borrow check).
       *)
  parents : abstraction_id_set;  (** The parent abstractions *)
  original_parents : abstraction_id list;
      (** The original list of parents, ordered. This is used for synthesis. TODO: remove? *)
  regions : region_id_set;  (** Regions owned by this abstraction *)
  ancestors_regions : region_id_set;
      (** Union of the regions owned by this abstraction's ancestors (not
          including the regions of this abstraction itself) *)
  avalues : typed_avalue list;  (** The values in this abstraction *)
}
[@@deriving
  show,
    ord,
    visitors
      {
        name = "iter_abs";
        variety = "iter";
        ancestors = [ "iter_typed_avalue" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      },
    visitors
      {
        name = "map_abs";
        variety = "map";
        ancestors = [ "map_typed_avalue" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      }]

(** A symbolic expansion
    
    A symbolic expansion doesn't represent a value, but rather an operation
    that we apply to values.
    
    TODO: this should rather be name "expanded_symbolic"
 *)
type symbolic_expansion =
  | SePrimitive of primitive_value
  | SeAdt of (VariantId.id option * symbolic_value list)
  | SeMutRef of BorrowId.id * symbolic_value
  | SeSharedRef of BorrowId.Set.t * symbolic_value
[@@deriving show]