Implement CfimAst.ml

4 files changed, 92 insertions, 2 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;
+}
diff --git a/src/Expressions.ml b/src/Expressions.ml
index f890f9c4..6eb5531b 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -9,7 +9,7 @@ type projection_elem =
   | Deref
   | DerefBox
   | Field of field_proj_kind * FieldId.id
-  | Downcast of VariandId.id
+  | Downcast of VariantId.id
 
 type projection = projection_elem list
 
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index b46b00ee..abbca35c 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -16,6 +16,9 @@ module type Id = sig
   val incr : id -> id
 
   val to_string : id -> string
+
+  (* TODO: remove *)
+  (* module Map : Map.S with type key = id *)
 end
 
 (** Generative functor for identifiers.
@@ -25,7 +28,7 @@ end
 module IdGen () : Id = struct
   type id = int
 
-  type 'a vector = 'a list (* TODO: use a map *)
+  type 'a vector = 'a list
 
   let zero = 0
 
@@ -36,6 +39,21 @@ module IdGen () : Id = struct
     if x == max_int then raise (IntegerOverflow ()) else x + 1
 
   let to_string = string_of_int
+
+  (* TODO: how to make this work? *)
+  (* (module Ord : Map.OrderedType = struct
+       type t = id
+
+       let compare t1 t2 = t2 - t1
+     end)
+
+     module IdMap = Map.Make (Ord) *)
+
+  (* module Map = Map.Make (struct
+       type t = id
+
+       let compare = Stdlib.compare
+     end) *)
 end
 
 type name = string list
diff --git a/src/main.ml b/src/main.ml
index 2248506a..03522106 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,4 +1,5 @@
 open Identifiers
+open CfimAst
 
 module Id0 = IdGen ()