summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2024-04-22 10:47:35 +0200
committerSon Ho2024-04-22 10:47:35 +0200
commit93d6dce8f3d78ad6f2f18ca3e2f58fa605d503cd (patch)
tree756865684bdfefd3fd1eb6be482e5fd816aac898 /compiler
parent4deb6ac44c615bbe3594c18ddbf880bf89f07d9e (diff)
Fix an issue when joining a symbolic value with bottom
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml40
-rw-r--r--compiler/SymbolicToPure.ml4
2 files changed, 33 insertions, 11 deletions
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