diff options
| -rw-r--r-- | src/CfimAst.ml | 71 | ||||
| -rw-r--r-- | src/Expressions.ml | 2 | ||||
| -rw-r--r-- | src/Identifiers.ml | 20 | ||||
| -rw-r--r-- | src/main.ml | 1 |
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 () |