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
|
module T = Types
module PV = PrimitiveValues
module V = Values
module E = Expressions
module C = Contexts
module Subst = Substitute
module L = Logging
module Inv = Invariants
module S = SynthesizeSymbolic
module SA = SymbolicAst
open Cps
open InterpreterBorrows
type proj_kind = LoanProj | BorrowProj
(** Apply a symbolic expansion to a context, by replacing the original
symbolic value with its expanded value. Is valid only if the expansion
is *not a borrow* (i.e., an adt...).
This function does *not* update the synthesis.
*)
val apply_symbolic_expansion_non_borrow :
C.config ->
V.symbolic_value ->
V.symbolic_expansion ->
C.eval_ctx ->
C.eval_ctx
(** Expand a symhbolic value, without branching *)
val expand_symbolic_value_no_branching :
C.config -> V.symbolic_value -> SA.mplace option -> cm_fun
(** Expand a symbolic enumeration (leads to branching if the enumeration has
more than one variant).
Parameters:
- [config]
- [sv]
- [sv_place]
- [cf_branches]: the continuation to evaluate the branches. This continuation
typically evaluates a [match] statement *after* we have performed the symbolic
expansion (in particular, we can have one continuation for all the branches).
- [cf_after_join]: the continuation for *after* the match (we perform a join
then call it).
*)
val expand_symbolic_adt :
C.config ->
V.symbolic_value ->
SA.mplace option ->
st_cm_fun ->
st_m_fun ->
m_fun
(** Expand a symbolic boolean.
Parameters: see {!expand_symbolic_adt}.
The two parameters of type [st_cm_fun] correspond to the [cf_branches]
parameter (here, there are exactly two branches).
*)
val expand_symbolic_bool :
C.config ->
V.symbolic_value ->
SA.mplace option ->
st_cm_fun ->
st_cm_fun ->
st_m_fun ->
m_fun
(** Symbolic integers are expanded upon evaluating a [SwitchInt].
When expanding a boolean upon evaluating an [if ... then ... else ...],
or an enumeration just before matching over it, we can simply expand the
boolean/enumeration (generating a list of contexts from which to execute)
then retry evaluating the [if ... then ... else ...] or the [match]: as
the scrutinee will then have a concrete value, the interpreter will switch
to the proper branch.
However, when expanding a "regular" integer for a switch, there is always an
*otherwise* branch that we can take, for which the integer must remain symbolic
(because in this branch the scrutinee can take a range of values). We thus
can't simply expand then retry to evaluate the [switch], because then we
would loop...
For this reason, we take the list of branches to execute as parameters, and
directly jump to those branches after the expansion, without reevaluating the
switch. The continuation is thus for the execution *after* the switch.
*)
val expand_symbolic_int :
C.config ->
V.symbolic_value ->
SA.mplace option ->
T.integer_type ->
(V.scalar_value * st_cm_fun) list ->
st_cm_fun ->
st_m_fun ->
m_fun
(** If this mode is activated through the [config], greedily expand the symbolic
values which need to be expanded. See {!C.config} for more information.
*)
val greedy_expand_symbolic_values : C.config -> cm_fun
|
