blob: 3beba61010f8b5a0cd5c93565e9a777d6a48b722 (
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
|
module T = Types
module PV = PrimitiveValues
module V = Values
module LA = LlbcAst
module E = Expressions
module C = Contexts
module Subst = Substitute
module L = Logging
module Inv = Invariants
module S = SynthesizeSymbolic
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 : access_kind -> E.place -> (V.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 :
C.config ->
bool ->
access_kind ->
E.place ->
(V.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 : C.config -> E.operand -> (V.typed_value -> m_fun) -> m_fun
(** Evaluate several operands at once. *)
val eval_operands :
C.config -> E.operand list -> (V.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 {!constructor:Aeneas.Expressions.rvalue.Discriminant}: discriminant
reads should have been eliminated from the AST.
*)
val eval_rvalue_not_global :
C.config -> E.rvalue -> ((V.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 : C.config -> E.place -> cm_fun
|
