blob: 00431ebd389dedcbef7c6ba6e9e50b17ccb162c8 (
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
|
(** The "symbolic" AST is the AST directly generated by the symbolic execution.
It is very rough and meant to be extremely straightforward to build during
the symbolic execution: we later apply transformations to generate the
pure AST that we export. *)
open Identifiers
module T = Types
module V = Values
module E = Expressions
module A = CfimAst
type call_id =
| Fun of A.fun_id * V.FunCallId.id
(** A "regular" function (i.e., a function which is not a primitive operation) *)
| Unop of E.unop
| Binop of E.binop
type call = {
call_id : call_id;
type_params : T.ety list;
args : V.typed_value list;
dest : V.symbolic_value;
}
type expression =
| Return
| Panic
| FunCall of call * expression
| EndAbstraction of V.abs * expression
| Expansion of V.symbolic_value * expansion
| Meta of meta * expression (** Meta information *)
and expansion =
| ExpandNoBranch of V.symbolic_expansion * expression
(** A symbolic expansion which doesn't generate a branching.
Includes: expansion of borrows, structures, enumerations with one
variants... *)
| ExpandEnum of
(T.VariantId.id option * V.symbolic_value list * expression) list
(** A symbolic expansion of an ADT value which leads to branching (i.e.,
a match over an enumeration with strictly more than one variant *)
| ExpandBool of expression * expression
(** A boolean expansion (i.e, an `if ... then ... else ...`) *)
| ExpandInt of
T.integer_type * (V.scalar_value * expression) list * expression
(** An integer expansion (i.e, a switch over an integer). The last
expression is for the "otherwise" branch. *)
(** Meta information, not necessary for synthesis but useful to guide it to
generate a pretty output.
*)
and meta = Aggregate of V.typed_value (** We generated an aggregate value *)
|
