Start deriving formatters for debugging

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