diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Expressions.ml | 11 | ||||
| -rw-r--r-- | src/Identifiers.ml | 21 | ||||
| -rw-r--r-- | src/Interpreter.ml | 30 | ||||
| -rw-r--r-- | src/Print.ml | 77 | ||||
| -rw-r--r-- | src/Types.ml | 20 | ||||
| -rw-r--r-- | src/Values.ml | 1 | ||||
| -rw-r--r-- | src/dune | 3 | ||||
| -rw-r--r-- | src/main.ml | 4 |
8 files changed, 143 insertions, 24 deletions
diff --git a/src/Expressions.ml b/src/Expressions.ml index 7ae6ab01..20431f18 100644 --- a/src/Expressions.ml +++ b/src/Expressions.ml @@ -6,20 +6,22 @@ open Values type field_proj_kind = | ProjAdt of TypeDefId.id * VariantId.id option | ProjTuple of int +[@@deriving show] (* arity of the tuple *) type projection_elem = | Deref | DerefBox | Field of field_proj_kind * FieldId.id +[@@deriving show] -type projection = projection_elem list +type projection = projection_elem list [@@deriving show] -type place = { var_id : VarId.id; projection : projection } +type place = { var_id : VarId.id; projection : projection } [@@deriving show] -type borrow_kind = Shared | Mut | TwoPhaseMut +type borrow_kind = Shared | Mut | TwoPhaseMut [@@deriving show] -type unop = Not | Neg +type unop = Not | Neg [@@deriving show] (** A binary operation @@ -45,6 +47,7 @@ type binop = | Mul | Shl | Shr +[@@deriving show] (** Constant value for an operand diff --git a/src/Identifiers.ml b/src/Identifiers.ml index b858360d..e1684f2c 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -20,10 +20,23 @@ module type Id = sig val to_string : id -> string + val pp_id : Format.formatter -> id -> unit + + val show_id : id -> string + + val pp_generator : Format.formatter -> generator -> unit + + val show_generator : generator -> string + val to_int : id -> int val of_int : id -> int + val pp_vector : + (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a vector -> unit + + val show_vector : (Format.formatter -> 'a -> unit) -> 'a vector -> string + val empty_vector : 'a vector val vector_to_list : 'a vector -> 'a list @@ -77,11 +90,11 @@ end *) module IdGen () : Id = struct (* TODO: use Z.t *) - type id = int + type id = int [@@deriving show] - type generator = id + type generator = id [@@deriving show] - type 'a vector = 'a list + type 'a vector = 'a list [@@deriving show] let zero = 0 @@ -159,6 +172,6 @@ module IdGen () : Id = struct (OfJsonBasic.list_of_json a_of_json js) end -type name = string list [@@deriving yojson] +type name = string list [@@deriving show] (** A name such as: `std::collections::vector` (which would be represented as [["std"; "collections"; "vector"]]) *) diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 00adf68a..5278cfdd 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -16,6 +16,8 @@ module L = Logging let ctx2 = ... ctx1 in ... *) +(* TODO: for debugging purposes, we might want to put use eval_ctx everywhere + (rather than only env) *) (** Some utilities *) @@ -980,7 +982,9 @@ let rec access_projection (access : projection_access) (env : C.env) Ok (env1, { res with updated }) (* If we reach Bottom, it may mean we need to expand an uninitialized * enumeration value *)) - | Field (ProjAdt (_, Some _variant_id), _), V.Bottom -> + | Field (ProjAdt (_, _), _), V.Bottom -> + Error (FailBottom (1 + List.length p', pe, v.ty)) + | Field (ProjTuple _, _), V.Bottom -> Error (FailBottom (1 + List.length p', pe, v.ty)) (* Symbolic value: needs to be expanded *) | _, Symbolic sp -> @@ -1240,7 +1244,12 @@ let expand_bottom_value (config : C.config) (access : access_kind) assert (arity = List.length tys); (* Generate the field values *) compute_expanded_bottom_tuple_value tys - | _ -> failwith "Unreachable" + | _ -> + failwith + ("Unreachable: " + ^ Print.CfimAst.projection_elem_variant_name pe + ^ ", " + ^ Print.Types.ty_variant_name ty) in (* Update the environment by inserting the expanded value at the proper place *) match write_place config access p' nv env with @@ -1282,11 +1291,12 @@ let rec update_env_along_read_place (config : C.config) (access : access_kind) See [update_env_alond_read_place]. *) let rec update_env_along_write_place (config : C.config) (access : access_kind) - (tyctx : T.type_def T.TypeDefId.vector) (p : E.place) (nv : V.typed_value) - (env : C.env) : C.env = - (* Attempt to write the place: if it fails, update the environment and retry *) - match write_place config access p nv env with - | Ok env' -> env' + (tyctx : T.type_def T.TypeDefId.vector) (p : E.place) (env : C.env) : C.env + = + (* Attempt to *read* (yes, "read": we check the access to the place, and + write to it later) the place: if it fails, update the environment and retry *) + match read_place config access p env with + | Ok _ -> env | Error err -> let env' = match err with @@ -1302,7 +1312,7 @@ let rec update_env_along_write_place (config : C.config) (access : access_kind) expand_bottom_value config access tyctx p remaining_pes pe ty env | FailBorrow _ -> failwith "Could not write to a borrow" in - update_env_along_write_place config access tyctx p nv env' + update_env_along_write_place config access tyctx p env' exception UpdateEnv of C.env (** Small utility used to break control-flow *) @@ -1830,7 +1840,9 @@ type statement_eval_res = Unit | Break of int | Continue of int | Return let prepare_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = let access = Write in - let env1 = update_env_along_read_place config access p ctx.env in + let env1 = + update_env_along_write_place config access ctx.type_context p ctx.env + in let env2 = collect_borrows_at_place config access p env1 in let env3 = drop_borrows_at_place config p env2 in let v = read_place_unwrap config access p env3 in diff --git a/src/Print.ml b/src/Print.ml index 9cdde188..4b8ad30a 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -55,6 +55,21 @@ module Types = struct | T.U64 -> "u64" | T.U128 -> "u128" + let ty_variant_name (ty : 'r T.ty) : string = + match ty with + | T.Adt (_, _, _) -> "Adt" + | T.TypeVar _ -> "TypeVar" + | T.Bool -> "Bool" + | T.Char -> "Char" + | T.Never -> "Never" + | T.Integer _ -> "Integer" + | T.Str -> "Str" + | T.Array _ -> "Array" + | T.Slice _ -> "Slice" + | T.Ref (_, _, _) -> "Ref" + | T.Tuple _ -> "Tuple" + | T.Assumed (_, _, _) -> "Assumed" + let rec ty_to_string (fmt : 'r type_formatter) (ty : 'r T.ty) : string = match ty with | T.Adt (id, regions, tys) -> @@ -569,6 +584,12 @@ module CfimAst = struct fun_def_id_to_string; } + let projection_elem_variant_name (pe : E.projection_elem) : string = + match pe with + | E.Deref -> "Deref" + | E.DerefBox -> "DerefBox" + | E.Field (_, _) -> "Field" + let rec projection_to_string (fmt : ast_formatter) (inside : string) (p : E.projection) : string = match p with @@ -917,3 +938,59 @@ module EvalCtxCfimAst = struct let fmt = PA.eval_ctx_to_ast_formatter ctx in PA.expression_to_string fmt indent indent_incr e end + +(* +(** Debugging facilities, for when there is missing context *) +module Debug = struct + let erased_region_to_string = PT.erased_region_to_string + + let region_var_id_to_string (id : T.RegionVarId.id) = + "@" ^ T.RegionVarId.to_string id + + let type_var_id_to_string (id : T.TypeVarId.id) = + "@" ^ T.TypeVarId.to_string id + + let type_def_id_to_string (id : T.TypeDefId.id) = + "@" ^ T.TypeDefId.to_string id + + let adt_variant_to_string (_def_id : T.TypeDefId.id) + (variant_id : T.VariantId.id) : string = + T.VariantId.to_string variant_id + + let var_id_to_string (id : V.VarId.id) = "@" ^ V.VarId.to_string id + + let adt_field_names (_def_id : T.TypeDefId.id) + (opt_variant_idt : T.VariantId.id option) : string list option = + None + + let dummy_etype_fmt : PT.etype_formatter = + let r_to_string = erased_region_to_string in + { r_to_string; type_var_id_to_string; type_def_id_to_string } + + let dummy_rtype_fmt : PT.rtype_formatter = + let r_to_string r = PT.region_to_string region_var_id_to_string r in + { r_to_string; type_var_id_to_string; type_def_id_to_string } + + let dummy_value_fmt : PV.value_formatter = + let r_to_string = region_var_id_to_string in + { + r_to_string; + type_var_id_to_string; + type_def_id_to_string; + adt_variant_to_string; + var_id_to_string; + adt_field_names; + } + + let field_proj_kind_to_string (pe : E.projection_elem) : string = + match pe with + | E.Deref -> "Deref" + | E.DerefBox -> "DerefBox" + | Field + + let projection_elem_to_string (pe : E.projection_elem) : string = + match pe with + | E.Deref -> "Deref" + | E.DerefBox -> "DerefBox" + | Field +end*) diff --git a/src/Types.ml b/src/Types.ml index 6f00f799..77296ac1 100644 --- a/src/Types.ml +++ b/src/Types.ml @@ -16,12 +16,14 @@ type type_var = { using indexed vectors *) tv_name : string; (** Variable name *) } +[@@deriving show] type region_var = { rv_index : RegionVarId.id; (** Unique index identifying the region - TODO: may be redundant *) rv_name : string option; (** Region name *) } +[@@deriving show] (** A region. @@ -32,12 +34,13 @@ type region_var = { type 'rid region = | Static (** Static region *) | Var of 'rid (** Non-static region *) +[@@deriving show] (** The type of erased regions. We could use unit, but having a dedicated type makes things more explicit. *) -type erased_region = Erased +type erased_region = Erased [@@deriving show] type integer_type = | Isize @@ -52,10 +55,11 @@ type integer_type = | U32 | U64 | U128 +[@@deriving show] -type ref_kind = Mut | Shared +type ref_kind = Mut | Shared [@@deriving show] -type assumed_ty = Box +type assumed_ty = Box [@@deriving show] type 'r ty = | Adt of TypeDefId.id * 'r list * 'r ty list @@ -70,26 +74,29 @@ type 'r ty = | Slice of 'r ty | Ref of 'r * 'r ty * ref_kind | Assumed of assumed_ty * 'r list * 'r ty list +[@@deriving show] -type rty = RegionVarId.id region ty +type rty = RegionVarId.id region ty [@@deriving show] (** Type with *R*egions. Used in function signatures and type definitions. *) -type ety = erased_region ty +type ety = erased_region ty [@@deriving show] (** Type with *E*rased regions. Used in function bodies, "general" value types, etc. *) -type field = { field_name : string; field_ty : rty } +type field = { field_name : string; field_ty : rty } [@@deriving show] type variant = { variant_name : string; fields : field FieldId.vector } +[@@deriving show] type type_def_kind = | Struct of field FieldId.vector | Enum of variant VariantId.vector +[@@deriving show] type type_def = { def_id : TypeDefId.id; @@ -98,6 +105,7 @@ type type_def = { type_params : type_var TypeVarId.vector; kind : type_def_kind; } +[@@deriving show] (** Convert an [rty] to an [ety] by erasing the region variables diff --git a/src/Values.ml b/src/Values.ml index 1346c7f7..e549846d 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -21,6 +21,7 @@ type var = { (** The variable type - erased type, because variables are not used ** in function signatures *) } +[@@deriving show] (** A variable *) @@ -1,6 +1,7 @@ (executable (name main) - (libraries yojson zarith easy_logging)) + (preprocess (pps ppx_deriving.show ppx_deriving.ord)) + (libraries ppx_deriving yojson zarith easy_logging)) (env (dev (flags diff --git a/src/main.ml b/src/main.ml index 36b5dd71..52fd8ea4 100644 --- a/src/main.ml +++ b/src/main.ml @@ -5,6 +5,10 @@ module T = Types module A = CfimAst module I = Interpreter +type test = Test [@@deriving show] + +let _ = show_test Test + (* This is necessary to have a backtrace when raising exceptions - for some * reason, the -g option doesn't work *) let () = Printexc.record_backtrace true |