From f204e2a5543257e77a4bc6ed666efa2f3c4ffabf Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jan 2022 10:13:13 +0100 Subject: Add comments about symbolic values --- src/Values.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'src/Values.ml') diff --git a/src/Values.ml b/src/Values.ml index 8ecf8849..a0bd96c5 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -54,10 +54,13 @@ type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty } - 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 + So [symbolic_value] is actually a projector. TODO: rename to [symbolic_proj]. + The kind of projector will then depend on the context. *) -(** TODO: make it clear that complementary projectors are projectors on borrows *) +(** TODO: make it clear that complementary projectors are projectors on borrows. + ** TODO: actually this is useless: the set of ended regions should be global! + ** (and thus stored in the context) *) type symbolic_proj_comp = { svalue : symbolic_value; (** The symbolic value itself *) rset_ended : RegionId.set_t; -- cgit v1.2.3 From d658ff64adc746523568577668ce80034071d963 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jan 2022 10:17:29 +0100 Subject: Update some comments --- src/Values.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/Values.ml') diff --git a/src/Values.ml b/src/Values.ml index a0bd96c5..0239da5e 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -56,6 +56,10 @@ type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty } We need to make this clear and more consistant. So [symbolic_value] is actually a projector. TODO: rename to [symbolic_proj]. The kind of projector will then depend on the context. + Actually, maybe we shouldn't use this type. Or for abstractions we should + use different types. Something like: + - [proj_borrows] for values + - [aproj_loans], [aproj_borrows] for avalues *) (** TODO: make it clear that complementary projectors are projectors on borrows. -- cgit v1.2.3 From b191de7f680e4ae43178fc42ccabc91808e189f8 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jan 2022 18:13:06 +0100 Subject: Make good progress on eval_local_function_call_symbolic --- src/Values.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Values.ml') diff --git a/src/Values.ml b/src/Values.ml index 0239da5e..001c0347 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -544,7 +544,7 @@ type abs = { 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 *) + by the current abstraction. TODO: why do we need those? *) regions : (RegionId.set_t[@opaque]); (** Regions owned by this abstraction *) avalues : typed_avalue list; (** The values in this abstraction *) } -- cgit v1.2.3 From d22f5d1ae5155c53b9cd0daf165dccb5d5563c1f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jan 2022 18:36:47 +0100 Subject: Finish implementing eval_local_function_call_symbolic --- src/Values.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'src/Values.ml') diff --git a/src/Values.ml b/src/Values.ml index 001c0347..ae9eb127 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -542,9 +542,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. TODO: why do we need those? *) regions : (RegionId.set_t[@opaque]); (** Regions owned by this abstraction *) avalues : typed_avalue list; (** The values in this abstraction *) } -- cgit v1.2.3 From 6f25cbb0dd202b53fe850560ddf566c75183af7d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jan 2022 10:07:15 +0100 Subject: Generate iterators for statement --- src/Values.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/Values.ml') diff --git a/src/Values.ml b/src/Values.ml index ae9eb127..ac4145eb 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -77,7 +77,7 @@ type symbolic_proj_comp = { regions *but* the ones which are listed in the projector. *) -(** 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 @@ -92,7 +92,7 @@ class ['self] iter_typed_value_base = 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 @@ -215,7 +215,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 @@ -231,7 +231,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 -- cgit v1.2.3 From 407474a35b7dd80116c8d358873d25e1a9b49048 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jan 2022 16:18:40 +0100 Subject: Fix some bugs --- src/Values.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src/Values.ml') diff --git a/src/Values.ml b/src/Values.ml index ac4145eb..47bdda23 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -518,7 +518,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, -- cgit v1.2.3 From 7137e0733650e0ce37eff4ff805c95543f2c1161 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jan 2022 17:44:17 +0100 Subject: Remove the symbolic_proj_comp def and make the set of ended regions a field in the eval_ctx struct --- src/Values.ml | 45 ++++++++++----------------------------------- 1 file changed, 10 insertions(+), 35 deletions(-) (limited to 'src/Values.ml') diff --git a/src/Values.ml b/src/Values.ml index 47bdda23..b6bb414b 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -47,35 +47,7 @@ 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 to [symbolic_proj]. - The kind of projector will then depend on the context. - Actually, maybe we shouldn't use this type. Or for abstractions we should - use different types. Something like: - - [proj_borrows] for values - - [aproj_loans], [aproj_borrows] for avalues - *) - -(** TODO: make it clear that complementary projectors are projectors on borrows. - ** TODO: actually this is useless: the set of ended regions should be global! - ** (and thus stored in the context) *) -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 [typed_value] iter visitor *) class ['self] iter_typed_value_base = @@ -86,8 +58,7 @@ 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 @@ -103,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 @@ -117,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]); -- cgit v1.2.3