blob: f0873aa3b9ec548899ec38ce5815dab75824e643 (
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
|
(** 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
[@@deriving show, ord]
type call = {
call_id : call_id;
abstractions : V.AbstractionId.id list;
type_params : T.ety list;
args : V.typed_value list;
dest : V.symbolic_value;
}
(** **Rk.:** here, [expression] is not at all equivalent to the expressions
used in CFIM: they are a first step towards lambda-calculus expressions.
*)
type expression =
| Return of V.typed_value option
(** There are two cases:
- the AST is for a forward function: the typed value should contain
the value which was in the return variable
- the AST is for a backward function: the typed value should be `None`
*)
| 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:
- concrete expansion
- borrow expansion
*Doesn't* include:
- expansion of ADTs with one variant
*)
| ExpandAdt of
(T.VariantId.id option * V.symbolic_value list * expression) list
(** ADT expansion *)
| 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 *)
|
