blob: 0fb12180b9b3b5cd3cdcce6effd5954817f049bc (
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
|
open Expressions
open Values
open Contexts
open Cps
open InterpreterPaths
(** Read a place (CPS-style function).
We also check that the value *doesn't contain bottoms or reserved
borrows*.
This function doesn't reorganize the context to make sure we can read
the place. If needs be, you should call {!InterpreterPaths.update_ctx_along_read_place} first.
*)
val read_place :
Meta.meta -> access_kind -> place -> (typed_value -> m_fun) -> m_fun
(** Auxiliary function.
Prepare the access to a place in a right-value (typically an operand) by
reorganizing the environment.
We reorganize the environment so that:
- we can access the place (we prepare *along* the path)
- the value at the place itself doesn't contain loans (the [access_kind]
controls whether we only end mutable loans, or also shared loans).
We also check, after the reorganization, that the value at the place
*doesn't contain any bottom nor reserved borrows*.
[expand_prim_copy]: if [true], expand the symbolic values which are
primitively copyable and contain borrows.
*)
val access_rplace_reorganize_and_read :
config ->
Meta.meta ->
bool ->
access_kind ->
place ->
(typed_value -> m_fun) ->
m_fun
(** Evaluate an operand.
Reorganize the context, then evaluate the operand.
**Warning**: this function shouldn't be used to evaluate a list of
operands (for a function call, for instance): we must do *one* reorganization
of the environment, before evaluating all the operands at once.
Use {!eval_operands} instead.
*)
val eval_operand :
config -> Meta.meta -> operand -> (typed_value -> m_fun) -> m_fun
(** Evaluate several operands at once. *)
val eval_operands :
config -> Meta.meta -> operand list -> (typed_value list -> m_fun) -> m_fun
(** Evaluate an rvalue which is not a global (globals are handled elsewhere).
Transmits the computed rvalue to the received continuation.
Note that this function fails on {!Aeneas.Expressions.rvalue.Discriminant}: discriminant
reads should have been eliminated from the AST.
*)
val eval_rvalue_not_global :
config ->
Meta.meta ->
rvalue ->
((typed_value, eval_error) result -> m_fun) ->
m_fun
(** Evaluate a fake read (update the context so that we can read a place) *)
val eval_fake_read : config -> Meta.meta -> place -> cm_fun
|
