summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-29 23:20:02 +0100
committerSon Ho2021-11-29 23:20:02 +0100
commit3952c51d7e63b754642ef2e1ea8b64d4aceccdc6 (patch)
tree1e1b01516a5a2f44a09fac6ba37526efe6810a70
parent46c0648948caa9f57cdd7e8561470e598eb814ab (diff)
Start deriving formatters for debugging
-rw-r--r--src/Expressions.ml11
-rw-r--r--src/Identifiers.ml21
-rw-r--r--src/Interpreter.ml30
-rw-r--r--src/Print.ml77
-rw-r--r--src/Types.ml20
-rw-r--r--src/Values.ml1
-rw-r--r--src/dune3
-rw-r--r--src/main.ml4
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 *)
diff --git a/src/dune b/src/dune
index c565d9fa..ec9f2d2b 100644
--- a/src/dune
+++ b/src/dune
@@ -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