Merge pull request #85 from AeneasVerif/son/fix_loops3

Fix some issues with the loops

2 files changed, 71 insertions, 21 deletions

diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 4624a1e9..dd7bd7a7 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -11,6 +11,7 @@ open TypesUtils
 open ValuesUtils
 open Cps
 open InterpreterUtils
+open InterpreterBorrowsCore
 open InterpreterBorrows
 open InterpreterLoopsCore
 module S = SynthesizeSymbolic
@@ -450,8 +451,14 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
       (* No borrows, no loans, no bottoms: we can introduce a symbolic value *)
       mk_fresh_symbolic_typed_value_from_no_regions_ty ty
 
-  let match_shared_borrows (_ : eval_ctx) (_ : eval_ctx) _ (ty : ety)
-      (bid0 : borrow_id) (bid1 : borrow_id) : borrow_id =
+  let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) match_rec
+      (ty : ety) (bid0 : borrow_id) (bid1 : borrow_id) : borrow_id =
+    (* Lookup the shared values and match them - we do this mostly
+       to make sure we end loans which might appear on one side
+       and not on the other. *)
+    let sv0 = lookup_shared_value ctx0 bid0 in
+    let sv1 = lookup_shared_value ctx1 bid1 in
+    let sv = match_rec sv0 sv1 in
     if bid0 = bid1 then bid0
     else
       (* We replace bid0 and bid1 with a fresh borrow id, and introduce
@@ -463,10 +470,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
       let rid = fresh_region_id () in
       let bid2 = fresh_borrow_id () in
 
-      (* Generate a fresh symbolic value for the shared value *)
+      (* Update the type of the shared loan to use the fresh region *)
       let _, bv_ty, kind = ty_as_ref ty in
-      let sv = mk_fresh_symbolic_typed_value_from_no_regions_ty bv_ty in
-
       let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
 
       (* Generate the avalues for the abstraction *)
@@ -1376,9 +1381,16 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets)
       }
     in
     Some maps
-  with Distinct msg ->
-    log#ldebug (lazy ("match_ctxs: distinct: " ^ msg));
-    None
+  with
+  | Distinct msg ->
+      log#ldebug (lazy ("match_ctxs: distinct: " ^ msg ^ "\n"));
+      None
+  | ValueMatchFailure k ->
+      log#ldebug
+        (lazy
+          ("match_ctxs: distinct: ValueMatchFailure" ^ show_updt_env_kind k
+         ^ "\n"));
+      None
 
 let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : eval_ctx)
     (ctx1 : eval_ctx) : bool =
@@ -1388,23 +1400,16 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : eval_ctx)
     (match_ctxs check_equivalent fixed_ids lookup_shared_value
        lookup_shared_value ctx0 ctx1)
 
-let match_ctx_with_target (config : config) (loop_id : LoopId.id)
-    (is_loop_entry : bool) (fp_bl_maps : borrow_loan_corresp)
-    (fp_input_svalues : SymbolicValueId.id list) (fixed_ids : ids_sets)
-    (src_ctx : eval_ctx) : st_cm_fun =
+let prepare_match_ctx_with_target (config : config) (loop_id : LoopId.id)
+    (fixed_ids : ids_sets) (src_ctx : eval_ctx) : cm_fun =
  fun cf tgt_ctx ->
   (* Debug *)
   log#ldebug
     (lazy
-      ("match_ctx_with_target:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids
-     ^ "\n" ^ "\n- src_ctx: " ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: "
-     ^ eval_ctx_to_string tgt_ctx));
-
-  (* We first reorganize [tgt_ctx] so that we can match [src_ctx] with it (by
-     ending loans for instance - remember that the [src_ctx] is the fixed point
-     context, which results from joins during which we ended the loans which
-     were introduced during the loop iterations)
-  *)
+      ("prepare_match_ctx_with_target:\n" ^ "\n- fixed_ids: "
+     ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: "
+     ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string tgt_ctx
+      ));
   (* End the loans which lead to mismatches when joining *)
   let rec cf_reorganize_join_tgt : cm_fun =
    fun cf tgt_ctx ->
@@ -1530,6 +1535,29 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
       in
       comp cc cf_reorganize_join_tgt cf tgt_ctx
   in
+  (* Apply the reorganization *)
+  cf_reorganize_join_tgt cf tgt_ctx
+
+let match_ctx_with_target (config : config) (loop_id : LoopId.id)
+    (is_loop_entry : bool) (fp_bl_maps : borrow_loan_corresp)
+    (fp_input_svalues : SymbolicValueId.id list) (fixed_ids : ids_sets)
+    (src_ctx : eval_ctx) : st_cm_fun =
+ fun cf tgt_ctx ->
+  (* Debug *)
+  log#ldebug
+    (lazy
+      ("match_ctx_with_target:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids
+     ^ "\n" ^ "\n- src_ctx: " ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: "
+     ^ eval_ctx_to_string tgt_ctx));
+
+  (* We first reorganize [tgt_ctx] so that we can match [src_ctx] with it (by
+     ending loans for instance - remember that the [src_ctx] is the fixed point
+     context, which results from joins during which we ended the loans which
+     were introduced during the loop iterations)
+  *)
+  let cf_reorganize_join_tgt =
+    prepare_match_ctx_with_target config loop_id fixed_ids src_ctx
+  in
 
   (* Introduce the "identity" abstractions for the loop re-entry.
 
@@ -1551,6 +1579,13 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
   let cf_introduce_loop_fp_abs : m_fun =
    fun tgt_ctx ->
     (* Match the source and target contexts *)
+    log#ldebug
+      (lazy
+        ("cf_introduce_loop_fp_abs:\n" ^ "\n- fixed_ids: "
+       ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: "
+       ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: "
+       ^ eval_ctx_to_string tgt_ctx));
+
     let filt_tgt_env, _, _ = ctx_split_fixed_new fixed_ids tgt_ctx in
     let filt_src_env, new_absl, new_dummyl =
       ctx_split_fixed_new fixed_ids src_ctx
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index 5f69b8d3..d6f89ed6 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -137,6 +137,21 @@ val match_ctxs :
  *)
 val ctxs_are_equivalent : ids_sets -> eval_ctx -> eval_ctx -> bool
 
+(** Reorganize a target context so that we can match it with a source context
+    (remember that the source context is generally the fixed point context,
+    which results from joins during which we ended the loans which
+    were introduced during the loop iterations).
+
+   **Parameters**:
+   - [config]
+   - [loop_id]
+   - [fixed_ids]
+   - [src_ctx]
+
+ *)
+val prepare_match_ctx_with_target :
+  config -> LoopId.id -> ids_sets -> eval_ctx -> cm_fun
+
 (** Match a context with a target context.
 
     This is used to compute application of loop translations: we use this