Merge pull request #95 from AeneasVerif/escherichia/errors

Escherichia/errors

2 files changed, 96 insertions, 78 deletions

diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 4dc53586..6e86e6a4 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -6,18 +6,19 @@ module Assoc = AssociatedTypes
 open TypesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
+open Errors
 
 (** The local logger *)
 let log = Logging.projectors_log
 
 (** [ty] shouldn't contain erased regions *)
-let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx)
+let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
     (fresh_reborrow : BorrowId.id -> BorrowId.id) (regions : RegionId.Set.t)
     (v : typed_value) (ty : rty) : abstract_shared_borrows =
   (* Sanity check - TODO: move those elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
   let ety = Subst.erase_regions ty in
-  assert (ty_is_rty ty && ety = v.ty);
+  sanity_check __FILE__ __LINE__ (ty_is_rty ty && ety = v.ty) meta;
   (* Project - if there are no regions from the abstraction in the type, return [_] *)
   if not (ty_has_regions_in_set regions ty) then []
   else
@@ -26,7 +27,8 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx)
     | VAdt adt, TAdt (id, generics) ->
         (* Retrieve the types of the fields *)
         let field_types =
-          Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics
+          Assoc.ctx_adt_value_get_inst_norm_field_rtypes meta ctx adt id
+            generics
         in
 
         (* Project over the field values *)
@@ -34,12 +36,12 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx)
         let proj_fields =
           List.map
             (fun (fv, fty) ->
-              apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions fv
-                fty)
+              apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow
+                regions fv fty)
             fields_types
         in
         List.concat proj_fields
-    | VBottom, _ -> raise (Failure "Unreachable")
+    | VBottom, _ -> craise __FILE__ __LINE__ meta "Unreachable"
     | VBorrow bc, TRef (r, ref_ty, kind) ->
         (* Retrieve the bid of the borrow and the asb of the projected borrowed value *)
         let bid, asb =
@@ -48,28 +50,27 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx)
           | VMutBorrow (bid, bv), RMut ->
               (* Apply the projection on the borrowed value *)
               let asb =
-                apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions
-                  bv ref_ty
+                apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow
+                  regions bv ref_ty
               in
               (bid, asb)
           | VSharedBorrow bid, RShared ->
               (* Lookup the shared value *)
               let ek = ek_all in
-              let sv = lookup_loan ek bid ctx in
+              let sv = lookup_loan meta ek bid ctx in
               let asb =
                 match sv with
                 | _, Concrete (VSharedLoan (_, sv))
                 | _, Abstract (ASharedLoan (_, sv, _)) ->
-                    apply_proj_borrows_on_shared_borrow ctx fresh_reborrow
+                    apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow
                       regions sv ref_ty
-                | _ -> raise (Failure "Unexpected")
+                | _ -> craise __FILE__ __LINE__ meta "Unexpected"
               in
               (bid, asb)
           | VReservedMutBorrow _, _ ->
-              raise
-                (Failure
-                   "Can't apply a proj_borrow over a reserved mutable borrow")
-          | _ -> raise (Failure "Unreachable")
+              craise __FILE__ __LINE__ meta
+                "Can't apply a proj_borrow over a reserved mutable borrow"
+          | _ -> craise __FILE__ __LINE__ meta "Unreachable"
         in
         let asb =
           (* Check if the region is in the set of projected regions (note that
@@ -80,21 +81,24 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx)
           else asb
         in
         asb
-    | VLoan _, _ -> raise (Failure "Unreachable")
+    | VLoan _, _ -> craise __FILE__ __LINE__ meta "Unreachable"
     | VSymbolic s, _ ->
         (* Check that the projection doesn't contain ended regions *)
-        assert (not (projections_intersect s.sv_ty ctx.ended_regions ty regions));
+        sanity_check __FILE__ __LINE__
+          (not
+             (projections_intersect meta s.sv_ty ctx.ended_regions ty regions))
+          meta;
         [ AsbProjReborrows (s, ty) ]
-    | _ -> raise (Failure "Unreachable")
+    | _ -> craise __FILE__ __LINE__ meta "Unreachable"
 
-let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
-    (fresh_reborrow : BorrowId.id -> BorrowId.id) (regions : RegionId.Set.t)
-    (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) :
-    typed_avalue =
+let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
+    (ctx : eval_ctx) (fresh_reborrow : BorrowId.id -> BorrowId.id)
+    (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t)
+    (v : typed_value) (ty : rty) : typed_avalue =
   (* Sanity check - TODO: move this elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
   let ety = Substitute.erase_regions ty in
-  assert (ty_is_rty ty && ety = v.ty);
+  sanity_check __FILE__ __LINE__ (ty_is_rty ty && ety = v.ty) meta;
   (* Project - if there are no regions from the abstraction in the type, return [_] *)
   if not (ty_has_regions_in_set regions ty) then { value = AIgnored; ty }
   else
@@ -104,19 +108,20 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
       | VAdt adt, TAdt (id, generics) ->
           (* Retrieve the types of the fields *)
           let field_types =
-            Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics
+            Assoc.ctx_adt_value_get_inst_norm_field_rtypes meta ctx adt id
+              generics
           in
           (* Project over the field values *)
           let fields_types = List.combine adt.field_values field_types in
           let proj_fields =
             List.map
               (fun (fv, fty) ->
-                apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                  regions ancestors_regions fv fty)
+                apply_proj_borrows meta check_symbolic_no_ended ctx
+                  fresh_reborrow regions ancestors_regions fv fty)
               fields_types
           in
           AAdt { variant_id = adt.variant_id; field_values = proj_fields }
-      | VBottom, _ -> raise (Failure "Unreachable")
+      | VBottom, _ -> craise __FILE__ __LINE__ meta "Unreachable"
       | VBorrow bc, TRef (r, ref_ty, kind) ->
           if
             (* Check if the region is in the set of projected regions (note that
@@ -129,7 +134,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
               | VMutBorrow (bid, bv), RMut ->
                   (* Apply the projection on the borrowed value *)
                   let bv =
-                    apply_proj_borrows check_symbolic_no_ended ctx
+                    apply_proj_borrows meta check_symbolic_no_ended ctx
                       fresh_reborrow regions ancestors_regions bv ref_ty
                   in
                   AMutBorrow (bid, bv)
@@ -147,11 +152,9 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
                   *)
                   ASharedBorrow bid
               | VReservedMutBorrow _, _ ->
-                  raise
-                    (Failure
-                       "Can't apply a proj_borrow over a reserved mutable \
-                        borrow")
-              | _ -> raise (Failure "Unreachable")
+                  craise __FILE__ __LINE__ meta
+                    "Can't apply a proj_borrow over a reserved mutable borrow"
+              | _ -> craise __FILE__ __LINE__ meta "Unreachable"
             in
             ABorrow bc
           else
@@ -163,7 +166,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
               | VMutBorrow (bid, bv), RMut ->
                   (* Apply the projection on the borrowed value *)
                   let bv =
-                    apply_proj_borrows check_symbolic_no_ended ctx
+                    apply_proj_borrows meta check_symbolic_no_ended ctx
                       fresh_reborrow regions ancestors_regions bv ref_ty
                   in
                   (* If the borrow id is in the ancestor's regions, we still need
@@ -176,25 +179,23 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
               | VSharedBorrow bid, RShared ->
                   (* Lookup the shared value *)
                   let ek = ek_all in
-                  let sv = lookup_loan ek bid ctx in
+                  let sv = lookup_loan meta ek bid ctx in
                   let asb =
                     match sv with
                     | _, Concrete (VSharedLoan (_, sv))
                     | _, Abstract (ASharedLoan (_, sv, _)) ->
-                        apply_proj_borrows_on_shared_borrow ctx fresh_reborrow
-                          regions sv ref_ty
-                    | _ -> raise (Failure "Unexpected")
+                        apply_proj_borrows_on_shared_borrow meta ctx
+                          fresh_reborrow regions sv ref_ty
+                    | _ -> craise __FILE__ __LINE__ meta "Unexpected"
                   in
                   AProjSharedBorrow asb
               | VReservedMutBorrow _, _ ->
-                  raise
-                    (Failure
-                       "Can't apply a proj_borrow over a reserved mutable \
-                        borrow")
-              | _ -> raise (Failure "Unreachable")
+                  craise __FILE__ __LINE__ meta
+                    "Can't apply a proj_borrow over a reserved mutable borrow"
+              | _ -> craise __FILE__ __LINE__ meta "Unreachable"
             in
             ABorrow bc
-      | VLoan _, _ -> raise (Failure "Unreachable")
+      | VLoan _, _ -> craise __FILE__ __LINE__ meta "Unreachable"
       | VSymbolic s, _ ->
           (* Check that the projection doesn't contain already ended regions,
            * if necessary *)
@@ -211,20 +212,22 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx)
                 ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
                 ^ RegionId.Set.to_string None rset2
                 ^ "\n"));
-            assert (not (projections_intersect ty1 rset1 ty2 rset2)));
+            sanity_check __FILE__ __LINE__
+              (not (projections_intersect meta ty1 rset1 ty2 rset2))
+              meta);
           ASymbolic (AProjBorrows (s, ty))
       | _ ->
           log#lerror
             (lazy
               ("apply_proj_borrows: unexpected inputs:\n- input value: "
-              ^ typed_value_to_string ctx v
+              ^ typed_value_to_string ~meta:(Some meta) ctx v
               ^ "\n- proj rty: " ^ ty_to_string ctx ty));
-          raise (Failure "Unreachable")
+          craise __FILE__ __LINE__ meta "Unreachable"
     in
     { value; ty }
 
-let symbolic_expansion_non_borrow_to_value (sv : symbolic_value)
-    (see : symbolic_expansion) : typed_value =
+let symbolic_expansion_non_borrow_to_value (meta : Meta.meta)
+    (sv : symbolic_value) (see : symbolic_expansion) : typed_value =
   let ty = Subst.erase_regions sv.sv_ty in
   let value =
     match see with
@@ -235,12 +238,12 @@ let symbolic_expansion_non_borrow_to_value (sv : symbolic_value)
         in
         VAdt { variant_id; field_values }
     | SeMutRef (_, _) | SeSharedRef (_, _) ->
-        raise (Failure "Unexpected symbolic reference expansion")
+        craise __FILE__ __LINE__ meta "Unexpected symbolic reference expansion"
   in
   { value; ty }
 
-let symbolic_expansion_non_shared_borrow_to_value (sv : symbolic_value)
-    (see : symbolic_expansion) : typed_value =
+let symbolic_expansion_non_shared_borrow_to_value (meta : Meta.meta)
+    (sv : symbolic_value) (see : symbolic_expansion) : typed_value =
   match see with
   | SeMutRef (bid, bv) ->
       let ty = Subst.erase_regions sv.sv_ty in
@@ -248,19 +251,22 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : symbolic_value)
       let value = VBorrow (VMutBorrow (bid, bv)) in
       { value; ty }
   | SeSharedRef (_, _) ->
-      raise (Failure "Unexpected symbolic shared reference expansion")
-  | _ -> symbolic_expansion_non_borrow_to_value sv see
+      craise __FILE__ __LINE__ meta
+        "Unexpected symbolic shared reference expansion"
+  | _ -> symbolic_expansion_non_borrow_to_value meta sv see
 
 (** Apply (and reduce) a projector over loans to a value.
 
     TODO: detailed comments. See [apply_proj_borrows]
 *)
-let apply_proj_loans_on_symbolic_expansion (regions : RegionId.Set.t)
-    (ancestors_regions : RegionId.Set.t) (see : symbolic_expansion)
-    (original_sv_ty : rty) : typed_avalue =
+let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta)
+    (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t)
+    (see : symbolic_expansion) (original_sv_ty : rty) : typed_avalue =
   (* Sanity check: if we have a proj_loans over a symbolic value, it should
    * contain regions which we will project *)
-  assert (ty_has_regions_in_set regions original_sv_ty);
+  sanity_check __FILE__ __LINE__
+    (ty_has_regions_in_set regions original_sv_ty)
+    meta;
   (* Match *)
   let (value, ty) : avalue * ty =
     match (see, original_sv_ty) with
@@ -275,7 +281,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : RegionId.Set.t)
         (AAdt { variant_id; field_values }, original_sv_ty)
     | SeMutRef (bid, spc), TRef (r, ref_ty, RMut) ->
         (* Sanity check *)
-        assert (spc.sv_ty = ref_ty);
+        sanity_check __FILE__ __LINE__ (spc.sv_ty = ref_ty) meta;
         (* Apply the projector to the borrowed value *)
         let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in
         (* Check if the region is in the set of projected regions (note that
@@ -293,7 +299,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : RegionId.Set.t)
           (ALoan (AIgnoredMutLoan (opt_bid, child_av)), ref_ty)
     | SeSharedRef (bids, spc), TRef (r, ref_ty, RShared) ->
         (* Sanity check *)
-        assert (spc.sv_ty = ref_ty);
+        sanity_check __FILE__ __LINE__ (spc.sv_ty = ref_ty) meta;
         (* Apply the projector to the borrowed value *)
         let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in
         (* Check if the region is in the set of projected regions (note that
@@ -305,7 +311,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : RegionId.Set.t)
         else
           (* Not in the set: ignore *)
           (ALoan (AIgnoredSharedLoan child_av), ref_ty)
-    | _ -> raise (Failure "Unreachable")
+    | _ -> craise __FILE__ __LINE__ meta "Unreachable"
   in
   { value; ty }
 
@@ -331,8 +337,8 @@ let apply_proj_loans_on_symbolic_expansion (regions : RegionId.Set.t)
     borrows - easy - and mutable borrows - in this case, we reborrow the whole
     borrow: [mut_borrow ... ~~> shared_loan {...} (mut_borrow ...)]).
 *)
-let apply_reborrows (reborrows : (BorrowId.id * BorrowId.id) list)
-    (ctx : eval_ctx) : eval_ctx =
+let apply_reborrows (meta : Meta.meta)
+    (reborrows : (BorrowId.id * BorrowId.id) list) (ctx : eval_ctx) : eval_ctx =
   (* This is a bit brutal, but whenever we insert a reborrow, we remove
    * it from the list. This allows us to check that all the reborrows were
    * applied before returning.
@@ -463,11 +469,12 @@ let apply_reborrows (reborrows : (BorrowId.id * BorrowId.id) list)
   (* Visit *)
   let ctx = obj#visit_eval_ctx () ctx in
   (* Check that there are no reborrows remaining *)
-  assert (!reborrows = []);
+  sanity_check __FILE__ __LINE__ (!reborrows = []) meta;
   (* Return *)
   ctx
 
-let prepare_reborrows (config : config) (allow_reborrows : bool) :
+let prepare_reborrows (config : config) (meta : Meta.meta)
+    (allow_reborrows : bool) :
     (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx) =
   let reborrows : (BorrowId.id * BorrowId.id) list ref = ref [] in
   (* The function to generate and register fresh reborrows *)
@@ -476,34 +483,35 @@ let prepare_reborrows (config : config) (allow_reborrows : bool) :
       let bid' = fresh_borrow_id () in
       reborrows := (bid, bid') :: !reborrows;
       bid')
-    else raise (Failure "Unexpected reborrow")
+    else craise __FILE__ __LINE__ meta "Unexpected reborrow"
   in
   (* The function to apply the reborrows in a context *)
   let apply_registered_reborrows (ctx : eval_ctx) : eval_ctx =
     match config.mode with
     | ConcreteMode ->
-        assert (!reborrows = []);
+        sanity_check __FILE__ __LINE__ (!reborrows = []) meta;
         ctx
     | SymbolicMode ->
         (* Apply the reborrows *)
-        apply_reborrows !reborrows ctx
+        apply_reborrows meta !reborrows ctx
   in
   (fresh_reborrow, apply_registered_reborrows)
 
 (** [ty] shouldn't have erased regions *)
-let apply_proj_borrows_on_input_value (config : config) (ctx : eval_ctx)
-    (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t)
-    (v : typed_value) (ty : rty) : eval_ctx * typed_avalue =
-  assert (ty_is_rty ty);
+let apply_proj_borrows_on_input_value (config : config) (meta : Meta.meta)
+    (ctx : eval_ctx) (regions : RegionId.Set.t)
+    (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) :
+    eval_ctx * typed_avalue =
+  sanity_check __FILE__ __LINE__ (ty_is_rty ty) meta;
   let check_symbolic_no_ended = true in
   let allow_reborrows = true in
   (* Prepare the reborrows *)
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows config allow_reborrows
+    prepare_reborrows config meta allow_reborrows
   in
   (* Apply the projector *)
   let av =
-    apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions
+    apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow regions
       ancestors_regions v ty
   in
   (* Apply the reborrows *)
diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
index 9e4ebc20..17569ac8 100644
--- a/compiler/InterpreterProjectors.mli
+++ b/compiler/InterpreterProjectors.mli
@@ -15,11 +15,16 @@ open Contexts
     [original_sv_ty]: shouldn't have erased regions
 *)
 val apply_proj_loans_on_symbolic_expansion :
-  RegionId.Set.t -> RegionId.Set.t -> symbolic_expansion -> rty -> typed_avalue
+  Meta.meta ->
+  RegionId.Set.t ->
+  RegionId.Set.t ->
+  symbolic_expansion ->
+  rty ->
+  typed_avalue
 
 (** Convert a symbolic expansion *which is not a borrow* to a value *)
 val symbolic_expansion_non_borrow_to_value :
-  symbolic_value -> symbolic_expansion -> typed_value
+  Meta.meta -> symbolic_value -> symbolic_expansion -> typed_value
 
 (** Convert a symbolic expansion *which is not a shared borrow* to a value.
 
@@ -28,7 +33,7 @@ val symbolic_expansion_non_borrow_to_value :
     during a symbolic expansion.
   *)
 val symbolic_expansion_non_shared_borrow_to_value :
-  symbolic_value -> symbolic_expansion -> typed_value
+  Meta.meta -> symbolic_value -> symbolic_expansion -> typed_value
 
 (** Auxiliary function to prepare reborrowing operations (used when
     applying projectors).
@@ -43,7 +48,10 @@ val symbolic_expansion_non_shared_borrow_to_value :
     - [allow_reborrows]
  *)
 val prepare_reborrows :
-  config -> bool -> (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx)
+  config ->
+  Meta.meta ->
+  bool ->
+  (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx)
 
 (** Apply (and reduce) a projector over borrows to an avalue.
     We use this for instance to spread the borrows present in the inputs
@@ -96,6 +104,7 @@ val prepare_reborrows :
       then we interpret the borrow [l] as belonging to region [r]
 *)
 val apply_proj_borrows :
+  Meta.meta ->
   bool ->
   eval_ctx ->
   (BorrowId.id -> BorrowId.id) ->
@@ -116,6 +125,7 @@ val apply_proj_borrows :
  *)
 val apply_proj_borrows_on_input_value :
   config ->
+  Meta.meta ->
   eval_ctx ->
   RegionId.Set.t ->
   RegionId.Set.t ->