Merge pull request #95 from AeneasVerif/escherichia/errors

Escherichia/errors

1 files changed, 44 insertions, 30 deletions

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 243cf67b..4ee11cbd 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -6,6 +6,7 @@ open LlbcAst
 open Utils
 open TypesUtils
 open Cps
+open Errors
 
 (* TODO: we should probably rename the file to ContextsUtils *)
 
@@ -16,10 +17,11 @@ let log = Logging.interpreter_log
 
 (** Auxiliary function - call a function which requires a continuation,
     and return the let context given to the continuation *)
-let get_cf_ctx_no_synth (f : cm_fun) (ctx : eval_ctx) : eval_ctx =
+let get_cf_ctx_no_synth (meta : Meta.meta) (f : cm_fun) (ctx : eval_ctx) :
+    eval_ctx =
   let nctx = ref None in
   let cf ctx =
-    assert (!nctx = None);
+    sanity_check __FILE__ __LINE__ (!nctx = None) meta;
     nctx := Some ctx;
     None
   in
@@ -61,9 +63,14 @@ let statement_to_string ctx = Print.EvalCtx.statement_to_string ctx "" "  "
 let statement_to_string_with_tab ctx =
   Print.EvalCtx.statement_to_string ctx "  " "  "
 
-let env_elem_to_string ctx = Print.EvalCtx.env_elem_to_string ctx "" "  "
-let env_to_string ctx env = eval_ctx_to_string { ctx with env }
-let abs_to_string ctx = Print.EvalCtx.abs_to_string ctx "" "  "
+let env_elem_to_string meta ctx =
+  Print.EvalCtx.env_elem_to_string ~meta:(Some meta) ctx "" "  "
+
+let env_to_string meta ctx env =
+  eval_ctx_to_string ~meta:(Some meta) { ctx with env }
+
+let abs_to_string meta ctx =
+  Print.EvalCtx.abs_to_string ~meta:(Some meta) ctx "" "  "
 
 let same_symbolic_id (sv0 : symbolic_value) (sv1 : symbolic_value) : bool =
   sv0.sv_id = sv1.sv_id
@@ -76,29 +83,31 @@ let mk_place_from_var_id (var_id : VarId.id) : place =
   { var_id; projection = [] }
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_value (ty : ty) : symbolic_value =
+let mk_fresh_symbolic_value (meta : Meta.meta) (ty : ty) : symbolic_value =
   (* Sanity check *)
-  assert (ty_is_rty ty);
+  sanity_check __FILE__ __LINE__ (ty_is_rty ty) meta;
   let sv_id = fresh_symbolic_value_id () in
   let svalue = { sv_id; sv_ty = ty } in
   svalue
 
-let mk_fresh_symbolic_value_from_no_regions_ty (ty : ty) : symbolic_value =
-  assert (ty_no_regions ty);
-  mk_fresh_symbolic_value ty
+let mk_fresh_symbolic_value_from_no_regions_ty (meta : Meta.meta) (ty : ty) :
+    symbolic_value =
+  sanity_check __FILE__ __LINE__ (ty_no_regions ty) meta;
+  mk_fresh_symbolic_value meta ty
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_typed_value (rty : ty) : typed_value =
-  assert (ty_is_rty rty);
+let mk_fresh_symbolic_typed_value (meta : Meta.meta) (rty : ty) : typed_value =
+  sanity_check __FILE__ __LINE__ (ty_is_rty rty) meta;
   let ty = Substitute.erase_regions rty in
   (* Generate the fresh a symbolic value *)
-  let value = mk_fresh_symbolic_value rty in
+  let value = mk_fresh_symbolic_value meta rty in
   let value = VSymbolic value in
   { value; ty }
 
-let mk_fresh_symbolic_typed_value_from_no_regions_ty (ty : ty) : typed_value =
-  assert (ty_no_regions ty);
-  mk_fresh_symbolic_typed_value ty
+let mk_fresh_symbolic_typed_value_from_no_regions_ty (meta : Meta.meta)
+    (ty : ty) : typed_value =
+  sanity_check __FILE__ __LINE__ (ty_no_regions ty) meta;
+  mk_fresh_symbolic_typed_value meta ty
 
 (** Create a typed value from a symbolic value. *)
 let mk_typed_value_from_symbolic_value (svalue : symbolic_value) : typed_value =
@@ -124,9 +133,10 @@ let mk_aproj_loans_value_from_symbolic_value (regions : RegionId.Set.t)
   else { value = AIgnored; ty = svalue.sv_ty }
 
 (** Create a borrows projector from a symbolic value *)
-let mk_aproj_borrows_from_symbolic_value (proj_regions : RegionId.Set.t)
-    (svalue : symbolic_value) (proj_ty : ty) : aproj =
-  assert (ty_is_rty proj_ty);
+let mk_aproj_borrows_from_symbolic_value (meta : Meta.meta)
+    (proj_regions : RegionId.Set.t) (svalue : symbolic_value) (proj_ty : ty) :
+    aproj =
+  sanity_check __FILE__ __LINE__ (ty_is_rty proj_ty) meta;
   if ty_has_regions_in_set proj_regions proj_ty then
     AProjBorrows (svalue, proj_ty)
   else AIgnoredProjBorrows
@@ -140,8 +150,8 @@ let borrow_in_asb (bid : BorrowId.id) (asb : abstract_shared_borrows) : bool =
   List.exists (borrow_is_asb bid) asb
 
 (** TODO: move *)
-let remove_borrow_from_asb (bid : BorrowId.id) (asb : abstract_shared_borrows) :
-    abstract_shared_borrows =
+let remove_borrow_from_asb (meta : Meta.meta) (bid : BorrowId.id)
+    (asb : abstract_shared_borrows) : abstract_shared_borrows =
   let removed = ref 0 in
   let asb =
     List.filter
@@ -152,7 +162,7 @@ let remove_borrow_from_asb (bid : BorrowId.id) (asb : abstract_shared_borrows) :
           false))
       asb
   in
-  assert (!removed = 1);
+  sanity_check __FILE__ __LINE__ (!removed = 1) meta;
   asb
 
 (** We sometimes need to return a value whose type may vary depending on
@@ -427,7 +437,7 @@ let empty_ids_set = fst (compute_ctxs_ids [])
 (** **WARNING**: this function doesn't compute the normalized types
     (for the trait type aliases). This should be computed afterwards.
  *)
-let initialize_eval_ctx (ctx : decls_ctx)
+let initialize_eval_ctx (meta : Meta.meta) (ctx : decls_ctx)
     (region_groups : RegionGroupId.id list) (type_vars : type_var list)
     (const_generic_vars : const_generic_var list) : eval_ctx =
   reset_global_counters ();
@@ -436,7 +446,7 @@ let initialize_eval_ctx (ctx : decls_ctx)
       (List.map
          (fun (cg : const_generic_var) ->
            let ty = TLiteral cg.ty in
-           let cv = mk_fresh_symbolic_typed_value ty in
+           let cv = mk_fresh_symbolic_typed_value meta ty in
            (cg.index, cv))
          const_generic_vars)
   in
@@ -459,8 +469,8 @@ let initialize_eval_ctx (ctx : decls_ctx)
     region ids. This is mostly used in preparation of function calls (when
     evaluating in symbolic mode).
  *)
-let instantiate_fun_sig (ctx : eval_ctx) (generics : generic_args)
-    (tr_self : trait_instance_id) (sg : fun_sig)
+let instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx)
+    (generics : generic_args) (tr_self : trait_instance_id) (sg : fun_sig)
     (regions_hierarchy : region_var_groups) : inst_fun_sig =
   log#ldebug
     (lazy
@@ -498,8 +508,12 @@ let instantiate_fun_sig (ctx : eval_ctx) (generics : generic_args)
   (* Generate the type substitution
      Note that for now we don't support instantiating the type parameters with
      types containing regions. *)
-  assert (List.for_all TypesUtils.ty_no_regions generics.types);
-  assert (TypesUtils.trait_instance_id_no_regions tr_self);
+  sanity_check __FILE__ __LINE__
+    (List.for_all TypesUtils.ty_no_regions generics.types)
+    meta;
+  sanity_check __FILE__ __LINE__
+    (TypesUtils.trait_instance_id_no_regions tr_self)
+    meta;
   let tsubst =
     Substitute.make_type_subst_from_vars sg.generics.types generics.types
   in
@@ -513,8 +527,8 @@ let instantiate_fun_sig (ctx : eval_ctx) (generics : generic_args)
   in
   (* Substitute the signature *)
   let inst_sig =
-    AssociatedTypes.ctx_subst_norm_signature ctx asubst rsubst tsubst cgsubst
-      tr_subst tr_self sg regions_hierarchy
+    AssociatedTypes.ctx_subst_norm_signature meta ctx asubst rsubst tsubst
+      cgsubst tr_subst tr_self sg regions_hierarchy
   in
   (* Return *)
   inst_sig