Fix a bug in convert_value_to_abstractions

src/interp/InterpreterBorrows.ml

@@ -2009,6 +2009,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
           avalues;
         }
       in
+      Invariants.opt_type_check_abs span ctx abs;
       (* Add to the list of abstractions *)
       absl := abs :: !absl
   in
@@ -2083,7 +2084,6 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
             let value = ABorrow (ASharedBorrow (PNone, bid)) in
             ([ { value; ty } ], v)
         | VMutBorrow (bid, bv) ->
-            let r_id = if group then r_id else fresh_region_id () in
             (* We don't support nested borrows for now *)
             cassert __FILE__ __LINE__
               (not (value_has_borrows (Some span) ctx bv.value))
@@ -3507,6 +3507,7 @@ let merge_into_first_abstraction (span : Meta.span) (abs_kind : abs_kind)
   let nabs =
     merge_abstractions span abs_kind can_end merge_funs ctx abs0 abs1
   in
+  Invariants.opt_type_check_abs span ctx nabs;
 
   (* Update the environment: replace the abstraction 0 with the result of the merge,
      remove the abstraction 1 *)

src/interp/InterpreterLoops.ml

@@ -388,7 +388,8 @@ let eval_loop_symbolic (config : config) (span : span)
       log#ldebug
         (lazy
           ("eval_loop_symbolic: compute_abs_given_back_tys:\n- abs:\n"
-         ^ abs_to_string span ctx abs ^ "\n"));
+          ^ abs_to_string span ~with_ended:true ctx abs
+          ^ "\n"));
 
       let is_borrow (av : typed_avalue) : bool =
         match av.value with

src/interp/InterpreterLoopsJoinCtxs.ml

@@ -303,12 +303,13 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option)
            match ee with
            | EAbs _ | EFrame | EBinding (BVar _, _) -> [ ee ]
            | EBinding (BDummy id, v) ->
-               if is_fresh_did id then
+               if is_fresh_did id then (
                  let absl =
                    convert_value_to_abstractions span abs_kind can_end
                      destructure_shared_values ctx0 v
                  in
-                 List.map (fun abs -> EAbs abs) absl
+                 Invariants.opt_type_check_absl span ctx0 absl;
+                 List.map (fun abs -> EAbs abs) absl)
                else [ ee ])
          ctx0.env)
   in
@@ -1171,16 +1172,22 @@ let loop_join_origin_with_continue_ctxs (config : config) (span : Meta.span)
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after destructure:\n"
         ^ eval_ctx_to_string ~span:(Some span) ctx));
+    (* Sanity check *)
+    if !Config.sanity_checks then Invariants.check_invariants span ctx;
 
     (* Reduce the context we want to add to the join *)
     let ctx = reduce_ctx span loop_id fixed_ids ctx in
     log#ldebug
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after reduce:\n"
         ^ eval_ctx_to_string ~span:(Some span) ctx));
+    (* Sanity check *)
+    if !Config.sanity_checks then Invariants.check_invariants span ctx;
 
     (* Refresh the fresh abstractions *)
     let ctx = refresh_abs fixed_ids.aids ctx in
+    (* Sanity check *)
+    if !Config.sanity_checks then Invariants.check_invariants span ctx;
 
     (* Join the two contexts  *)
     let ctx1 = join_one_aux ctx in
@@ -1195,6 +1202,8 @@ let loop_join_origin_with_continue_ctxs (config : config) (span : Meta.span)
       (lazy
         ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n"
         ^ eval_ctx_to_string ~span:(Some span) !joined_ctx));
+    (* Sanity check *)
+    if !Config.sanity_checks then Invariants.check_invariants span !joined_ctx;
 
     (* Reduce again to reach a fixed point *)
     joined_ctx := reduce_ctx span loop_id fixed_ids !joined_ctx;

src/interp/InterpreterUtils.ml

@@ -64,8 +64,8 @@ let env_elem_to_string span ctx =
 let env_to_string span ctx env =
   eval_ctx_to_string ~span:(Some span) { ctx with env }
 
-let abs_to_string span ctx =
-  Print.EvalCtx.abs_to_string ~span:(Some span) ctx "" "  "
+let abs_to_string span ?(with_ended = false) ctx =
+  Print.EvalCtx.abs_to_string ~span:(Some span) ~with_ended ctx "" "  "
 
 let same_symbolic_id (sv0 : symbolic_value) (sv1 : symbolic_value) : bool =
   sv0.sv_id = sv1.sv_id
@@ -255,6 +255,11 @@ let symbolic_value_has_ended_regions (ended_regions : RegionId.Set.t)
   let regions = ty_regions s.sv_ty in
   not (RegionId.Set.disjoint regions ended_regions)
 
+let region_is_owned (abs : abs) (r : region) : bool =
+  match r with
+  | RVar (Free rid) -> RegionId.Set.mem rid abs.regions.owned
+  | _ -> false
+
 let bottom_in_value_visitor (ended_regions : RegionId.Set.t) =
   object
     inherit [_] iter_typed_value