Implement CfimAst.ml

1 files changed, 71 insertions, 0 deletions

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
new file mode 100644
index 00000000..90eb41cb
--- /dev/null
+++ b/src/CfimAst.ml
@@ -0,0 +1,71 @@
+open Identifiers
+open Types
+open Values
+open Expressions
+
+type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree
+
+type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id
+
+type assertion = { cond : operand; expected : bool }
+
+type fun_sig = {
+  region_params : region_var RegionVarId.vector;
+  num_early_bound_regions : int;
+  type_params : type_var TypeVarId.vector;
+  inputs : rty VarId.vector;
+  output : rty;
+}
+
+type call = {
+  func : fun_id;
+  region_params : erased_region list;
+  type_params : ety list;
+  args : operand list;
+  dest : place;
+}
+
+type statement =
+  | Assign of place * rvalue
+  | FakeRead of place
+  | SetDiscriminant of place * VariantId.id
+  | Drop of place
+  | Assert of assertion
+  | Call of call
+  | Panic
+  | Return
+  | Break of int
+      (** Break to (outer) loop. The [int] identifies the loop to break to:
+          * 0: break to the first outer loop (the current loop)
+          * 1: break to the second outer loop
+          * ...
+          *)
+  | Continue of int
+      (** Continue to (outer) loop. The loop identifier works
+          the same way as for [Break] *)
+  | Nop
+
+type expression =
+  | Statement of statement
+  | Sequence of expression * expression
+  | Switch of operand * switch_targets
+  | Loop of expression
+
+and switch_targets =
+  | If of expression * expression  (** Gives the "if" and "else" blocks *)
+  | SwitchInt of integer_type * (scalar_value * expression) list * expression
+      (** The targets for a switch over an integer are:
+          - the list `(matched value, expression to execute)`
+          - the "otherwise" expression.
+          Also note that we precise the type of the integer (uint32, int64, etc.)
+          which we switch on. *)
+
+type fun_def = {
+  def_id : FunDefId.id;
+  name : name;
+  signature : fun_sig;
+  divergent : bool;
+  arg_count : int;
+  locals : var VarId.vector;
+  body : expression;
+}