diff options
Diffstat (limited to 'src/SymbolicAst.ml')
-rw-r--r-- | src/SymbolicAst.ml | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml new file mode 100644 index 00000000..6b66ada7 --- /dev/null +++ b/src/SymbolicAst.ml @@ -0,0 +1,47 @@ +(** 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 fun_id = + | Fun of A.fun_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 : V.FunCallId.id; + func : A.fun_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 + +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. *) |