From 93d6dce8f3d78ad6f2f18ca3e2f58fa605d503cd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 22 Apr 2024 10:47:35 +0200
Subject: Fix an issue when joining a symbolic value with bottom

---
 compiler/InterpreterLoopsMatchCtxs.ml | 40 +++++++++++++++++++++++++++--------
 compiler/SymbolicToPure.ml            |  4 ++--
 2 files changed, 33 insertions(+), 11 deletions(-)

(limited to 'compiler')

diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index e710ed2b..3db68f5d 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -714,7 +714,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
          both borrows *)
       raise (ValueMatchFailure (LoanInLeft id0))
 
-  let match_symbolic_values (ctx0 : eval_ctx) (_ : eval_ctx)
+  let match_symbolic_values (ctx0 : eval_ctx) (ctx1 : eval_ctx)
       (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value =
     let id0 = sv0.sv_id in
     let id1 = sv1.sv_id in
@@ -729,11 +729,18 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
       sanity_check __FILE__ __LINE__
         (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty))
         meta;
-      (* We simply introduce a fresh symbolic value *)
+      (* TODO: the symbolic values may contain bottoms: we're being conservatice,
+         and fail (for now) if part of a symbolic value contains a bottom.
+         A more general approach would be to introduce a symbolic value
+         with some ended regions. *)
+      sanity_check __FILE__ __LINE__
+        ((not (symbolic_value_has_ended_regions ctx0.ended_regions sv0))
+        && not (symbolic_value_has_ended_regions ctx1.ended_regions sv1))
+        meta;
       mk_fresh_symbolic_value meta sv0.sv_ty)
 
-  let match_symbolic_with_other (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool)
-      (sv : symbolic_value) (v : typed_value) : typed_value =
+  let match_symbolic_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx)
+      (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value =
     (* Check that:
        - there are no borrows in the symbolic value
        - there are no borrows in the "regular" value
@@ -763,8 +770,16 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
     | Some (VMutLoan id) ->
         if value_is_left then raise (ValueMatchFailure (LoanInLeft id))
         else raise (ValueMatchFailure (LoanInRight id)));
-    (* Return a fresh symbolic value *)
-    mk_fresh_symbolic_typed_value meta sv.sv_ty
+
+    (* There might be a bottom in the other value. We're being conservative:
+       if there is a bottom anywhere (it includes the case where part of the
+       value contains bottom) the result of the join is bottom. Otherwise,
+       we generate a fresh symbolic value. *)
+    if
+      symbolic_value_has_ended_regions ctx0.ended_regions sv
+      || bottom_in_value ctx1.ended_regions v
+    then mk_bottom meta sv.sv_ty
+    else mk_fresh_symbolic_typed_value meta sv.sv_ty
 
   let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool)
       (v : typed_value) : typed_value =
@@ -903,9 +918,16 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
       (sv1 : symbolic_value) : symbolic_value =
     sv1
 
-  let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool)
-      (sv : symbolic_value) (v : typed_value) : typed_value =
-    if left then v else mk_typed_value_from_symbolic_value sv
+  let match_symbolic_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx)
+      (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value =
+    (* We're being conservative for now: if any of the two values contains
+       a bottom, the join is bottom *)
+    if
+      symbolic_value_has_ended_regions ctx0.ended_regions sv
+      || bottom_in_value ctx1.ended_regions v
+    then mk_bottom meta sv.sv_ty
+    else if left then v
+    else mk_typed_value_from_symbolic_value sv
 
   let match_bottom_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool)
       (v : typed_value) : typed_value =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 46135f09..6c925bcd 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -618,7 +618,7 @@ let translate_type_id (meta : Meta.meta) (id : T.type_id) : type_id =
         | T.TBox ->
             (* Boxes have to be eliminated: this type id shouldn't
                be translated *)
-            craise __FILE__ __LINE__ meta "Unreachable"
+            craise __FILE__ __LINE__ meta "Unexpected box type"
       in
       TAssumed aty
   | TTuple -> TTuple
@@ -1626,7 +1626,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
             let cons = { e = cons_e; ty = cons_ty } in
             (* Apply the constructor *)
             mk_apps ctx.meta cons field_values)
-    | VBottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable"
+    | VBottom -> craise __FILE__ __LINE__ ctx.meta "Unexpected bottom value"
     | VLoan lc -> (
         match lc with
         | VSharedLoan (_, v) -> translate v
-- 
cgit v1.2.3