diff options
| -rw-r--r-- | src/Interpreter.ml | 114 | ||||
| -rw-r--r-- | src/Values.ml | 12 |
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 |