Start working on the generation of the symbolic AST

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. *)