blob: 29234ea98ecf87897107bdb47f186a9339740436 (
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
|
open Expressions
open Values
open Contexts
open Cps
open InterpreterPaths
(** Auxiliary function.
Prepare the access to a place in a right-value (typically an operand) by reorganizing
the environment to end outer loans, then read the value and check that this value
*doesn't contain any bottom nor reserved borrows*.
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).
[expand_prim_copy]: if [true], expand the symbolic values which are
primitively copyable and contain borrows.
*)
val access_rplace_reorganize_and_read :
config ->
Meta.span ->
bool ->
access_kind ->
place ->
eval_ctx ->
typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
(** 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.span ->
operand ->
eval_ctx ->
typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
(** Evaluate several operands at once. *)
val eval_operands :
config ->
Meta.span ->
operand list ->
eval_ctx ->
typed_value list
* eval_ctx
* (SymbolicAst.expression -> SymbolicAst.expression)
(** 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.span ->
rvalue ->
eval_ctx ->
(typed_value, eval_error) result
* eval_ctx
* (SymbolicAst.expression -> SymbolicAst.expression)
(** Evaluate a fake read (update the context so that we can read a place) *)
val eval_fake_read : config -> Meta.span -> place -> cm_fun
|
