diff options
Diffstat (limited to 'src/LlbcAst.ml')
| -rw-r--r-- | src/LlbcAst.ml | 188 |
1 files changed, 188 insertions, 0 deletions
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml new file mode 100644 index 00000000..f597cd27 --- /dev/null +++ b/src/LlbcAst.ml @@ -0,0 +1,188 @@ +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. *) |