diff options
Diffstat (limited to 'src/CfimAst.ml')
| -rw-r--r-- | src/CfimAst.ml | 188 |
1 files changed, 0 insertions, 188 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml deleted file mode 100644 index f597cd27..00000000 --- a/src/CfimAst.ml +++ /dev/null @@ -1,188 +0,0 @@ -open Identifiers -open Names -open Types -open Values -open Expressions - -module FunDeclId = IdGen () - -type var = { - index : VarId.id; (** Unique variable identifier *) - name : string option; - var_ty : ety; - (** The variable type - erased type, because variables are not used - ** in function signatures: they are only used to declare the list of - ** variables manipulated by a function body *) -} -[@@deriving show] -(** A variable, as used in a function definition *) - -type assumed_fun_id = - | Replace (** `core::mem::replace` *) - | BoxNew - | BoxDeref (** `core::ops::deref::Deref::<alloc::boxed::Box<T>>::deref` *) - | BoxDerefMut - (** `core::ops::deref::DerefMut::<alloc::boxed::Box<T>>::deref_mut` *) - | BoxFree - | VecNew - | VecPush - | VecInsert - | VecLen - | VecIndex (** `core::ops::index::Index::index<alloc::vec::Vec<T>, usize>` *) - | VecIndexMut - (** `core::ops::index::IndexMut::index_mut<alloc::vec::Vec<T>, usize>` *) -[@@deriving show, ord] - -type fun_id = Local of FunDeclId.id | Assumed of assumed_fun_id -[@@deriving show, ord] - -type assertion = { cond : operand; expected : bool } [@@deriving show] - -type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group -[@@deriving show] - -type abs_region_groups = (AbstractionId.id, RegionId.id) g_region_groups -[@@deriving show] - -type fun_sig = { - region_params : region_var list; - num_early_bound_regions : int; - regions_hierarchy : region_var_groups; - type_params : type_var list; - inputs : sty list; - output : sty; -} -[@@deriving show] -(** A function signature, as used when declaring functions *) - -type inst_fun_sig = { - regions_hierarchy : abs_region_groups; - inputs : rty list; - output : rty; -} -[@@deriving show] -(** A function signature, after instantiation *) - -type call = { - func : fun_id; - region_params : erased_region list; - type_params : ety list; - args : operand list; - dest : place; -} -[@@deriving show] - -(** Ancestor for [typed_value] iter visitor *) -class ['self] iter_statement_base = - object (_self : 'self) - inherit [_] VisitorsRuntime.iter - - method visit_place : 'env -> place -> unit = fun _ _ -> () - - method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> () - - method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> () - - method visit_assertion : 'env -> assertion -> unit = fun _ _ -> () - - method visit_operand : 'env -> operand -> unit = fun _ _ -> () - - method visit_call : 'env -> call -> unit = fun _ _ -> () - - method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> () - - method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> () - end - -(** Ancestor for [typed_value] map visitor *) -class ['self] map_statement_base = - object (_self : 'self) - inherit [_] VisitorsRuntime.map - - method visit_place : 'env -> place -> place = fun _ x -> x - - method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x - - method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x - - method visit_assertion : 'env -> assertion -> assertion = fun _ x -> x - - method visit_operand : 'env -> operand -> operand = fun _ x -> x - - method visit_call : 'env -> call -> call = fun _ x -> x - - method visit_integer_type : 'env -> integer_type -> integer_type = - fun _ x -> x - - method visit_scalar_value : 'env -> scalar_value -> scalar_value = - fun _ x -> x - end - -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 - | Sequence of statement * statement - | Switch of operand * switch_targets - | Loop of statement - -and switch_targets = - | If of statement * statement (** Gives the "if" and "else" blocks *) - | SwitchInt of integer_type * (scalar_value list * statement) list * statement - (** The targets for a switch over an integer are: - - the list `(matched values, statement to execute)` - We need a list for the matched values in case we do something like this: - `switch n { 0 | 1 => ..., _ => ... } - - the "otherwise" statement - Also note that we precise the type of the integer (uint32, int64, etc.) - which we switch on. *) -[@@deriving - show, - visitors - { - name = "iter_statement"; - variety = "iter"; - ancestors = [ "iter_statement_base" ]; - nude = true (* Don't inherit [VisitorsRuntime.iter] *); - concrete = true; - }, - visitors - { - name = "map_statement"; - variety = "map"; - ancestors = [ "map_statement_base" ]; - nude = true (* Don't inherit [VisitorsRuntime.iter] *); - concrete = true; - }] - -type fun_decl = { - def_id : FunDeclId.id; - name : fun_name; - signature : fun_sig; - arg_count : int; - locals : var list; - body : statement; -} -[@@deriving show] -(** TODO: function definitions (and maybe type definitions in the future) - * contain information like `divergent`. I wonder if this information should - * be stored directly inside the definitions or inside separate maps/sets. - * Of course, if everything is stored in separate maps/sets, nothing - * prevents us from computing this info in Charon (and thus exporting directly - * it with the type/function defs), in which case we just have to implement special - * treatment when deserializing, to move the info to a separate map. *) |