summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-04 18:13:26 +0100
committerSon Ho2022-01-04 18:13:26 +0100
commit4eac971ff729dde4054a4e5473e0de1a156ed6ca (patch)
treee236f66d4a27e0d76a58a01de0b680ab68ece382 /src
parent951d14a7d7ca18a6a05cad58938997f571cd4017 (diff)
Add a sanity check to make sure symbolic values disappear after
expansion
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml114
-rw-r--r--src/Values.ml12
2 files changed, 85 insertions, 41 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index fb98b516..745142b6 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -229,6 +229,36 @@ let loans_in_value (v : V.typed_value) : bool =
false
with Found -> true
+let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
+ bool =
+ let obj =
+ object
+ inherit [_] C.iter_eval_ctx
+
+ method! visit_Symbolic _ sv =
+ if sv.V.svalue.V.sv_id = sv_id then raise Found else ()
+
+ method! visit_ASymbolic _ aproj =
+ match aproj with
+ | AProjLoans sv | AProjBorrows (sv, _) ->
+ if sv.V.sv_id = sv_id then raise Found else ()
+
+ method! visit_abstract_shared_borrows _ asb =
+ let visit (asb : V.abstract_shared_borrow) : unit =
+ match asb with
+ | V.AsbBorrow _ -> ()
+ | V.AsbProjReborrows (sv, _) ->
+ if sv.V.sv_id = sv_id then raise Found else ()
+ in
+ List.iter visit asb
+ end
+ in
+ (* We use exceptions *)
+ try
+ obj#visit_eval_ctx () ctx;
+ false
+ with Found -> true
+
(** Lookup a loan content.
The loan is referred to by a borrow id.
@@ -3150,45 +3180,51 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem)
* fresh symbolic values in the context (which thus gets updated) *)
let rty = sp.V.svalue.V.sv_ty in
let ended_regions = sp.V.rset_ended in
- match (pe, rty) with
- (* "Regular" ADTs *)
- | ( Field (ProjAdt (def_id, _opt_variant_id), _),
- T.Adt (T.AdtId def_id', regions, types) ) -> (
- assert (def_id = def_id');
- (* Compute the expanded value - there should be exactly one because we
- * don't allow to expand enumerations with strictly more than one variant *)
- let expand_enumerations = false in
- match
- compute_expanded_symbolic_adt_value expand_enumerations ended_regions
- def_id regions types ctx
- with
- | [ (ctx, nv) ] ->
- (* Apply in the context *)
- apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx
- | _ -> failwith "Unexpected")
- (* Tuples *)
- | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
- assert (arity = List.length tys);
- (* Generate the field values *)
- let ctx, nv =
- compute_expanded_symbolic_tuple_value ended_regions tys ctx
- in
- (* Apply in the context *)
- apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx
- (* Boxes *)
- | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
- let ctx, nv =
- compute_expanded_symbolic_box_value ended_regions boxed_ty ctx
- in
- (* Apply in the context *)
- apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx
- (* Borrows *)
- | Deref, T.Ref (region, ref_ty, rkind) ->
- expand_symbolic_value_borrow config sp.V.svalue ended_regions region
- ref_ty rkind ctx
- | _ ->
- failwith
- ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
+ let ctx =
+ match (pe, rty) with
+ (* "Regular" ADTs *)
+ | ( Field (ProjAdt (def_id, _opt_variant_id), _),
+ T.Adt (T.AdtId def_id', regions, types) ) -> (
+ assert (def_id = def_id');
+ (* Compute the expanded value - there should be exactly one because we
+ * don't allow to expand enumerations with strictly more than one variant *)
+ let expand_enumerations = false in
+ match
+ compute_expanded_symbolic_adt_value expand_enumerations ended_regions
+ def_id regions types ctx
+ with
+ | [ (ctx, nv) ] ->
+ (* Apply in the context *)
+ apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx
+ | _ -> failwith "Unexpected")
+ (* Tuples *)
+ | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
+ assert (arity = List.length tys);
+ (* Generate the field values *)
+ let ctx, nv =
+ compute_expanded_symbolic_tuple_value ended_regions tys ctx
+ in
+ (* Apply in the context *)
+ apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx
+ (* Boxes *)
+ | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
+ let ctx, nv =
+ compute_expanded_symbolic_box_value ended_regions boxed_ty ctx
+ in
+ (* Apply in the context *)
+ apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx
+ (* Borrows *)
+ | Deref, T.Ref (region, ref_ty, rkind) ->
+ expand_symbolic_value_borrow config sp.V.svalue ended_regions region
+ ref_ty rkind ctx
+ | _ ->
+ failwith
+ ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
+ in
+ (* Sanity check: the symbolic value has disappeared *)
+ assert (not (symbolic_value_id_in_ctx sp.V.svalue.V.sv_id ctx));
+ (* Return *)
+ ctx
(** Update the environment to be able to read a place.
diff --git a/src/Values.ml b/src/Values.ml
index e4eca156..3af287c7 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -196,7 +196,7 @@ type abstract_shared_borrow =
| AsbProjReborrows of (symbolic_value[@opaque]) * (rty[@opaque])
[@@deriving show]
-type abstract_shared_borrows = abstract_shared_borrow list
+type abstract_shared_borrows = abstract_shared_borrow list [@@deriving show]
(** A set of abstract shared borrows *)
type aproj =
@@ -218,6 +218,10 @@ class ['self] iter_typed_avalue_base =
method visit_aproj : 'env -> aproj -> unit = fun _ _ -> ()
method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
+
+ method visit_abstract_shared_borrows
+ : 'env -> abstract_shared_borrows -> unit =
+ fun _ _ -> ()
end
(** Ancestor for MAP visitor for [typed_avalue] *)
@@ -230,6 +234,10 @@ class ['self] map_typed_avalue_base =
method visit_aproj : 'env -> aproj -> aproj = fun _ p -> p
method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
+
+ method visit_abstract_shared_borrows
+ : 'env -> abstract_shared_borrows -> abstract_shared_borrows =
+ fun _ asb -> asb
end
(** Abstraction values are used inside of abstractions to properly model
@@ -470,7 +478,7 @@ and aborrow_content =
abstraction so that we can properly call the backward functions
when generating the pure translation.
*)
- | AProjSharedBorrow of (abstract_shared_borrows[@opaque])
+ | AProjSharedBorrow of abstract_shared_borrows
(** A projected shared borrow.
When giving shared borrows as arguments to function calls, we