blob: 7f8c3a0a28291e7f3dc21e51efb5837204507371 (
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
75
76
77
78
79
80
81
82
83
84
85
|
open Values
open Contexts
open Cps
module SA = SymbolicAst
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 :
config ->
Meta.span ->
symbolic_value ->
eval_ctx ->
symbolic_expansion ->
eval_ctx
(** Expand a symhbolic value, without branching *)
val expand_symbolic_value_no_branching :
config -> Meta.span -> symbolic_value -> SA.mplace option -> cm_fun
(** Expand a symbolic enumeration (leads to branching if the enumeration has
more than one variant).
Parameters:
- [config]
- [span]
- [sv]
- [sv_place]
*)
val expand_symbolic_adt :
config ->
Meta.span ->
symbolic_value ->
SA.mplace option ->
eval_ctx ->
eval_ctx list * (SymbolicAst.expression list option -> eval_result)
(** Expand a symbolic boolean.
Parameters: see {!expand_symbolic_adt}.
*)
val expand_symbolic_bool :
config ->
Meta.span ->
symbolic_value ->
SA.mplace option ->
eval_ctx ->
(eval_ctx * eval_ctx)
* ((SymbolicAst.expression * SymbolicAst.expression) option -> eval_result)
(** 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.
When expanding a "regular" integer for a switch there is always an *otherwise*
branch. We treat it separately: for this reason we return a pair of a list
of evaluation contexts (for the branches which are not the otherwise branch)
and an additional evaluation context for the otherwise branch.
*)
val expand_symbolic_int :
config ->
Meta.span ->
symbolic_value ->
SA.mplace option ->
integer_type ->
scalar_value list ->
eval_ctx ->
(eval_ctx list * eval_ctx)
* ((SymbolicAst.expression list * SymbolicAst.expression) option ->
eval_result)
(** If this mode is activated through the [config], greedily expand the symbolic
values which need to be expanded. See {!type:Contexts.config} for more information.
*)
val greedy_expand_symbolic_values : config -> Meta.span -> cm_fun
|
