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
|
open Types
open Values
open Contexts
(** Auxiliary function.
Apply a proj_borrows on a shared borrow.
Note that when projecting over shared values, we generate
{!type:Aeneas.Values.abstract_shared_borrows}, not {!type:Aeneas.Values.avalue}s.
Parameters:
[regions]
[ancestor_regions]
[see]
[original_sv_ty]: shouldn't have erased regions
*)
val apply_proj_loans_on_symbolic_expansion :
Meta.meta -> RegionId.Set.t -> RegionId.Set.t -> symbolic_expansion -> rty -> typed_avalue
(** Convert a symbolic expansion *which is not a borrow* to a value *)
val symbolic_expansion_non_borrow_to_value :
Meta.meta -> symbolic_value -> symbolic_expansion -> typed_value
(** Convert a symbolic expansion *which is not a shared borrow* to a value.
If the expansion is a mutable reference expansion, it converts it to a borrow.
This function is meant to be used when reducing projectors over borrows,
during a symbolic expansion.
*)
val symbolic_expansion_non_shared_borrow_to_value :
Meta.meta -> symbolic_value -> symbolic_expansion -> typed_value
(** Auxiliary function to prepare reborrowing operations (used when
applying projectors).
Returns two functions:
- a function to generate fresh re-borrow ids, and register the reborrows
- a function to apply the reborrows in a context
Those functions are of course stateful.
Parameters:
- [config]
- [allow_reborrows]
*)
val prepare_reborrows :
config -> Meta.meta -> bool -> (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx)
(** Apply (and reduce) a projector over borrows to an avalue.
We use this for instance to spread the borrows present in the inputs
of a function into the regions introduced for this function. For instance:
{[
fn f<'a, 'b, T>(x: &'a T, y: &'b T)
]}
If we call `f` with `x -> shared_borrow l0` and `y -> shared_borrow l1`, then
for the region introduced for `'a` we need to project the value for `x` to
a shared aborrow, and we need to ignore the borrow in `y`, because it belongs
to the other region.
Parameters:
- [check_symbolic_no_ended]: controls whether we check or not whether
symbolic values don't contain already ended regions.
This check is activated when applying projectors upon calling a function
(because we need to check that function arguments don't contain ⊥),
but deactivated when expanding symbolic values:
{[
fn f<'a,'b>(x : &'a mut u32, y : &'b mut u32) -> (&'a mut u32, &'b mut u32);
let p = f(&mut x, &mut y); // p -> @s0
assert(x == ...); // end 'a
let z = p.1; // HERE: the symbolic expansion of @s0 contains ended regions
]}
- [ctx]
- [fresh_reborrow]: a function which generates fresh ids for reborrows, and
registers the reborrows (to be applied later to the context).
When applying projections on shared values, we need to apply
reborrows. This is a bit annoying because, with the way we compute
the projection on borrows, we can't update the context immediately.
Instead, we remember the list of borrows we have to insert in the
context *afterwards*.
See {!prepare_reborrows}
- [regions]: the regions to project
- [ancestor_regions]
- [v]: the value on which to apply the projection
- [ty]: the projection type (is used to map borrows to regions, or in other
words to interpret the borrows as belonging to some regions). Remember that
[v] doesn't contain region information.
For instance, if we have:
[v <: ty] where:
- [v = mut_borrow l ...]
- [ty = Ref (r, ...)]
then we interpret the borrow [l] as belonging to region [r]
*)
val apply_proj_borrows :
Meta.meta ->
bool ->
eval_ctx ->
(BorrowId.id -> BorrowId.id) ->
RegionId.Set.t ->
RegionId.Set.t ->
typed_value ->
rty ->
typed_avalue
(** Parameters:
- [config]
- [ctx]
- [regions]: the regions to project
- [ancestors_regions]
- [v]: the value on which to apply the projection
- [ty]: the type (with regions) to use for the projection (shouldn't have
erased regions)
*)
val apply_proj_borrows_on_input_value :
config ->
Meta.meta ->
eval_ctx ->
RegionId.Set.t ->
RegionId.Set.t ->
typed_value ->
rty ->
eval_ctx * typed_avalue
|
