summaryrefslogtreecommitdiff
path: root/src/SymbolicAst.ml
blob: fc2b2fc4e3e23639dd502c80527c434e7bfad38e (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
(** 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;
  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 *)