diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Values.ml | 55 |
1 files changed, 19 insertions, 36 deletions
diff --git a/src/Values.ml b/src/Values.ml index 8ecf8849..b6bb414b 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -47,30 +47,9 @@ type constant_value = type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty } [@@deriving show] -(** Symbolic value. - - TODO: a symbolic value may not always have the same type!! - For references: - - a projector on loans may see a symbolic value of id `sid` as having type `T` - - a projector on borrows may see it as having type `&mut T` - We need to make this clear and more consistant. - So [symbolic_value] is actually a projector. TODO: rename - *) - -(** TODO: make it clear that complementary projectors are projectors on borrows *) -type symbolic_proj_comp = { - svalue : symbolic_value; (** The symbolic value itself *) - rset_ended : RegionId.set_t; - (** The regions used in the symbolic value which have already ended *) -} -[@@deriving show] -(** A complementary projector over a symbolic value. - - "Complementary" stands for the fact that it is a projector over all the - regions *but* the ones which are listed in the projector. -*) +(** A symbolic value *) -(** Ancestor for iter visitor for [typed_value] *) +(** Ancestor for [typed_value] iter visitor *) class ['self] iter_typed_value_base = object (_self : 'self) inherit [_] VisitorsRuntime.iter @@ -79,13 +58,12 @@ class ['self] iter_typed_value_base = method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> () - method visit_symbolic_proj_comp : 'env -> symbolic_proj_comp -> unit = - fun _ _ -> () + method visit_symbolic_value : 'env -> symbolic_value -> unit = fun _ _ -> () method visit_ety : 'env -> ety -> unit = fun _ _ -> () end -(** Ancestor for map visitor for [typed_value] *) +(** Ancestor for [typed_value] map visitor for *) class ['self] map_typed_value_base = object (_self : 'self) inherit [_] VisitorsRuntime.map @@ -96,8 +74,7 @@ class ['self] map_typed_value_base = method visit_erased_region : 'env -> erased_region -> erased_region = fun _ r -> r - method visit_symbolic_proj_comp - : 'env -> symbolic_proj_comp -> symbolic_proj_comp = + method visit_symbolic_value : 'env -> symbolic_value -> symbolic_value = fun _ sv -> sv method visit_ety : 'env -> ety -> ety = fun _ ty -> ty @@ -110,8 +87,13 @@ type value = | Bottom (** No value (uninitialized or moved value) *) | Borrow of borrow_content (** A borrowed value *) | Loan of loan_content (** A loaned value *) - | Symbolic of symbolic_proj_comp - (** Unknown (symbolic) value. This is a projector on borrows (TODO: make this clearer). *) + | Symbolic of symbolic_value + (** Borrow projector over a symbolic value. + + Note that contrary to the abstraction-values case, symbolic values + appearing in regular values are interpreted as *borrow* projectors, + they can never be *loan* projectors. + *) and adt_value = { variant_id : (VariantId.id option[@opaque]); @@ -208,7 +190,7 @@ type aproj = type region = RegionVarId.id Types.region [@@deriving show] -(** Ancestor for iter visitor for [typed_avalue] *) +(** Ancestor for [typed_avalue] iter visitor *) class ['self] iter_typed_avalue_base = object (_self : 'self) inherit [_] iter_typed_value @@ -224,7 +206,7 @@ class ['self] iter_typed_avalue_base = fun _ _ -> () end -(** Ancestor for MAP visitor for [typed_avalue] *) +(** Ancestor for [typed_avalue] map visitor *) class ['self] map_typed_avalue_base = object (_self : 'self) inherit [_] map_typed_value @@ -511,7 +493,11 @@ and aborrow_content = *) (* TODO: we may want to merge this with typed_value - would prevent some issues - when accessing fields... *) + when accessing fields.... + + TODO: the type of avalues doesn't make sense for loan avalues: they currently + are typed as `& (mut) T` instead of `T`... +*) and typed_avalue = { value : avalue; ty : rty } [@@deriving show, @@ -535,9 +521,6 @@ and typed_avalue = { value : avalue; ty : rty } type abs = { abs_id : (AbstractionId.id[@opaque]); parents : (AbstractionId.set_t[@opaque]); (** The parent abstractions *) - acc_regions : (RegionId.set_t[@opaque]); - (** Union of the regions owned by the (transitive) parent abstractions and - by the current abstraction *) regions : (RegionId.set_t[@opaque]); (** Regions owned by this abstraction *) avalues : typed_avalue list; (** The values in this abstraction *) } |