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
|
module T = Types
module V = Values
module E = Expressions
module C = Contexts
module Subst = Substitute
module L = Logging
open Cps
open InterpreterExpansion
module Synth = SynthesizeSymbolic
type access_kind = Read | Write | Move
(** Update the environment to be able to read a place.
When reading a place, we may be stuck along the way because some value
is borrowed, we reach a symbolic value, etc. This function repeatedly
updates the environment (by ending borrows, expanding symbolic values, etc.)
until it manages to fully access the provided place.
*)
val update_ctx_along_read_place : C.config -> access_kind -> E.place -> cm_fun
(** Update the environment to be able to write to a place.
See {!update_ctx_along_read_place}.
*)
val update_ctx_along_write_place : C.config -> access_kind -> E.place -> cm_fun
(** Read the value at a given place.
This function doesn't update the environment to make sure the value is
accessible: if needs be, you should call {!update_ctx_along_read_place} first.
Note that we only access the value at the place, and do not check that
the value is "well-formed" (for instance that it doesn't contain bottoms).
*)
val read_place : access_kind -> E.place -> C.eval_ctx -> V.typed_value
(** Update the value at a given place.
This function doesn't update the environment to make sure the value is
accessible: if needs be, you should call {!update_ctx_along_write_place} first.
This function is a helper function and is **not safe**: it will not check if
the overwritten value contains borrows, loans, etc. and will simply
overwrite it.
*)
val write_place :
access_kind -> E.place -> V.typed_value -> C.eval_ctx -> C.eval_ctx
(** Compute an expanded tuple ⊥ value.
[compute_expanded_bottom_tuple_value [ty0, ..., tyn]] returns
[(⊥:ty0, ..., ⊥:tyn)]
*)
val compute_expanded_bottom_tuple_value : T.ety list -> V.typed_value
(** Compute an expanded ADT ⊥ value *)
val compute_expanded_bottom_adt_value :
T.type_decl T.TypeDeclId.Map.t ->
T.TypeDeclId.id ->
T.VariantId.id option ->
T.erased_region list ->
T.ety list ->
V.typed_value
(** Compute an expanded [Option] ⊥ value *)
val compute_expanded_bottom_option_value :
T.VariantId.id -> T.ety -> V.typed_value
(** Drop (end) outer loans at a given place, which should be seen as an l-value
(we will write to it later, but need to drop the loans before writing).
This is used to drop values when evaluating the drop statement or before
writing to a place.
Note that we don't do what is defined in the formalization: we move the
value to a temporary dummy value, then explore this value and end the outer
loans which are inside as long as we find some, then move the resulting
value back to where it was. This shouldn't make any difference, really (note
that the place is *inside* a borrow, if we end the borrow, we won't be able
to reinsert the value back).
*)
val drop_outer_loans_at_lplace : C.config -> E.place -> cm_fun
(** End the loans at a given place: read the value, if it contains a loan,
end this loan, repeat.
This is used when reading or borrowing values. We typically
first call {!update_ctx_along_read_place} or {!update_ctx_along_write_place}
to get access to the value, then call this function to "prepare" the value:
when moving values, we can't move a value which contains loans and thus need
to end them, etc.
*)
val end_loans_at_place : C.config -> access_kind -> E.place -> cm_fun
(** Small utility.
Prepare a place which is to be used as the destination of an assignment:
update the environment along the paths, end the outer loans at this place, etc.
Return the updated context and the (updated) value at the end of the
place. This value should not contain any outer loan (and we check it is the
case). Note that this value is very likely to contain ⊥ subvalues.
*)
val prepare_lplace : C.config -> E.place -> (V.typed_value -> m_fun) -> m_fun
|
