@@ -69,10 +69,10 @@ object Objects:
69
69
/** Syntax for the data structure abstraction used in abstract domain:
70
70
*
71
71
* ve ::= ObjectRef(class)
72
- * | OfClass(class, vs[outer], ctor, args, env)
73
- * | OfArray(object[owner], regions)
74
- * | Fun(..., env)
75
- * | Cold // abstract values in domain
72
+ * | OfClass(class, vs[outer], ctor, args, env)
73
+ * | OfArray(object[owner], regions)
74
+ * | Fun(..., env)
75
+ * | Cold // abstract values in domain
76
76
* vs ::= Set(ve) // set of abstract values
77
77
*
78
78
* refMap = ( ObjectRef | OfClass ) -> ( valsMap, varsMap, outersMap ) // refMap stores field informations of an object or instance
@@ -87,25 +87,29 @@ object Objects:
87
87
* env = (valsMap, Option[env]) // stores local variables in the residing method, and possibly outer environments
88
88
*
89
89
* addr ::= localVarAddr(regions, valsym, owner)
90
- * | fieldVarAddr(regions, valsym, owner) // independent of OfClass/ObjectRef
91
- * | arrayAddr(regions, owner) // independent of array element type
90
+ * | fieldVarAddr(regions, valsym, owner) // independent of OfClass/ObjectRef
91
+ * | arrayAddr(regions, owner) // independent of array element type
92
92
*
93
93
* regions ::= List(sourcePosition)
94
94
*/
95
95
96
96
sealed abstract class Value :
97
97
def show (using Context ): String
98
98
99
+ /** ValueElement are elements that can be contained in a RefSet */
99
100
sealed abstract class ValueElement extends Value
100
101
102
+ sealed trait ThisValue extends Value :
103
+ def widenThisV (height : Int )(using Context ) : ThisValue = this
104
+
101
105
/**
102
106
* A reference caches the values for outers and immutable fields.
103
107
*/
104
108
sealed abstract class Ref (
105
109
valsMap : mutable.Map [Symbol , Value ],
106
110
varsMap : mutable.Map [Symbol , Heap .Addr ],
107
111
outersMap : mutable.Map [ClassSymbol , Value ])
108
- extends ValueElement :
112
+ extends ValueElement with ThisValue :
109
113
protected val vals : mutable.Map [Symbol , Value ] = valsMap
110
114
protected val vars : mutable.Map [Symbol , Heap .Addr ] = varsMap
111
115
protected val outers : mutable.Map [ClassSymbol , Value ] = outersMap
@@ -162,6 +166,12 @@ object Objects:
162
166
def widenedCopy (outer : Value , args : List [Value ], env : Env .Data ): OfClass =
163
167
new OfClass (klass, outer, ctor, args, env)(this .valsMap, this .varsMap, this .outersMap)
164
168
169
+ override def widenThisV (height : Int )(using Context ): ThisValue =
170
+ val outer2 = outer.widen(height - 1 )
171
+ val args2 = args.map(_.widen(height - 1 ))
172
+ val env2 = env.widen(height - 1 )
173
+ widenedCopy(outer2, args2, env2)
174
+
165
175
def show (using Context ) =
166
176
val valFields = vals.map(_.show + " -> " + _.show)
167
177
" OfClass(" + klass.show + " , outer = " + outer + " , args = " + args.map(_.show) + " , vals = " + valFields + " )"
@@ -198,24 +208,29 @@ object Objects:
198
208
/**
199
209
* Represents a lambda expression
200
210
*/
201
- case class Fun (code : Tree , thisV : ValueElement , klass : ClassSymbol , env : Env .Data ) extends Value :
211
+ case class Fun (code : Tree , thisV : ThisValue , klass : ClassSymbol , env : Env .Data ) extends ValueElement :
202
212
def show (using Context ) = " Fun(" + code.show + " , " + thisV.show + " , " + klass.show + " )"
203
213
204
214
/**
205
215
* Represents a set of values
206
216
*
207
217
* It comes from `if` expressions.
208
218
*/
209
- case class RefSet (refs : ListSet [Value ]) extends Value :
210
- assert(refs.forall(! _.isInstanceOf [RefSet ]))
219
+ case class RefSet (refs : ListSet [ValueElement ]) extends Value :
211
220
def show (using Context ) = refs.map(_.show).mkString(" [" , " ," , " ]" )
212
221
213
- /** A cold alias which should not be used during initialization. */
214
- case object Cold extends ValueElement :
222
+ /** A cold alias which should not be used during initialization.
223
+ *
224
+ * Cold is not ValueElement since RefSet containing Cold is equivalent to Cold
225
+ */
226
+ case object Cold extends Value with ThisValue :
215
227
def show (using Context ) = " Cold"
216
228
217
229
val Bottom = RefSet (ListSet .empty)
218
230
231
+ // type ThisValue = Ref | Cold // used for typing thisV, whose value can only be Ref or Cold
232
+ // type VEOrCold = ValueElement | Cold
233
+
219
234
/** Checking state */
220
235
object State :
221
236
class Data :
@@ -411,7 +426,7 @@ object Objects:
411
426
*
412
427
* @return the environment and value for `this` owned by the given method.
413
428
*/
414
- def resolveEnv (meth : Symbol , thisV : Value , env : Data )(using Context ): Option [(Value , Data )] = log(" Resolving env for " + meth.show + " , this = " + thisV.show + " , env = " + env.show, printer) {
429
+ def resolveEnv (meth : Symbol , thisV : ThisValue , env : Data )(using Context ): Option [(ThisValue , Data )] = log(" Resolving env for " + meth.show + " , this = " + thisV.show + " , env = " + env.show, printer) {
415
430
env match
416
431
case localEnv : LocalEnv =>
417
432
if localEnv.meth == meth then Some (thisV -> env)
@@ -420,7 +435,11 @@ object Objects:
420
435
// TODO: handle RefSet
421
436
thisV match
422
437
case ref : OfClass =>
423
- resolveEnv(meth, ref.outer, ref.env)
438
+ ref.outer match
439
+ case outer : ThisValue =>
440
+ resolveEnv(meth, outer, ref.env)
441
+ case _ => // This is the case for top-level classes and local classes
442
+ None
424
443
case _ =>
425
444
None
426
445
}
@@ -494,7 +513,7 @@ object Objects:
494
513
val config = Config (thisV, summon[Env .Data ], Heap .getHeapData())
495
514
super .get(config, expr).map(_.value)
496
515
497
- def cachedEval (thisV : ValueElement , expr : Tree , cacheResult : Boolean )(fun : Tree => Value )(using Heap .MutableData , Env .Data ): Value =
516
+ def cachedEval (thisV : ThisValue , expr : Tree , cacheResult : Boolean )(fun : Tree => Value )(using Heap .MutableData , Env .Data ): Value =
498
517
val config = Config (thisV, summon[Env .Data ], Heap .getHeapData())
499
518
val result = super .cachedEval(config, expr, cacheResult, default = Res (Bottom , Heap .getHeapData())) { expr =>
500
519
Res (fun(expr), Heap .getHeapData())
@@ -551,14 +570,14 @@ object Objects:
551
570
extension (a : Value )
552
571
def join (b : Value ): Value =
553
572
(a, b) match
554
- case (Cold , b) => Cold
555
- case (a, Cold ) => Cold
556
- case (Bottom , b) => b
557
- case (a, Bottom ) => a
558
- case (RefSet (refs1), RefSet (refs2)) => RefSet (refs1 ++ refs2)
559
- case (a, RefSet (refs)) => RefSet (refs + a)
560
- case (RefSet (refs), b) => RefSet (refs + b)
561
- case (a, b) => RefSet (ListSet (a, b))
573
+ case (Cold , b) => Cold
574
+ case (a, Cold ) => Cold
575
+ case (Bottom , b) => b
576
+ case (a, Bottom ) => a
577
+ case (RefSet (refs1), RefSet (refs2)) => RefSet (refs1 ++ refs2)
578
+ case (a : ValueElement , RefSet (refs)) => RefSet (refs + a)
579
+ case (RefSet (refs), b : ValueElement ) => RefSet (refs + b)
580
+ case (a : ValueElement , b : ValueElement ) => RefSet (ListSet (a, b))
562
581
563
582
def widen (height : Int )(using Context ): Value =
564
583
if height == 0 then Cold
@@ -570,13 +589,10 @@ object Objects:
570
589
refs.map(ref => ref.widen(height)).join
571
590
572
591
case Fun (code, thisV, klass, env) =>
573
- Fun (code, thisV.widen (height). asInstanceOf [ ValueElement ] , klass, env.widen(height))
592
+ Fun (code, thisV.widenThisV (height), klass, env.widen(height))
574
593
575
- case ref @ OfClass (klass, outer, _, args, env) =>
576
- val outer2 = outer.widen(height - 1 )
577
- val args2 = args.map(_.widen(height - 1 ))
578
- val env2 = env.widen(height - 1 )
579
- ref.widenedCopy(outer2, args2, env2)
594
+ case ref : Ref =>
595
+ ref.widenThisV(height)
580
596
581
597
case _ => a
582
598
@@ -641,7 +657,7 @@ object Objects:
641
657
val ddef = target.defTree.asInstanceOf [DefDef ]
642
658
val meth = ddef.symbol
643
659
644
- val (thisV, outerEnv) =
660
+ val (thisV : ThisValue , outerEnv) =
645
661
if meth.owner.isClass then
646
662
(ref, Env .NoEnv )
647
663
else
@@ -653,7 +669,7 @@ object Objects:
653
669
// eval(ddef.rhs, ref, cls, cacheResult = true)
654
670
cache.cachedEval(ref, ddef.rhs, cacheResult = true ) { expr =>
655
671
Returns .installHandler(meth)
656
- val res = cases(expr, thisV. asInstanceOf [ ValueElement ] , cls)
672
+ val res = cases(expr, thisV, cls)
657
673
val returns = Returns .popHandler(meth)
658
674
res.join(returns)
659
675
}
@@ -692,13 +708,13 @@ object Objects:
692
708
693
709
/** Handle constructor calls `<init>(args)`.
694
710
*
695
- * @param thisV The value for the receiver.
711
+ * @param value The value for the receiver.
696
712
* @param ctor The symbol of the target method.
697
713
* @param args Arguments of the constructor call (all parameter blocks flatten to a list).
698
714
*/
699
- def callConstructor (thisV : Value , ctor : Symbol , args : List [ArgInfo ]): Contextual [Value ] = log(" call " + ctor.show + " , args = " + args.map(_.value.show), printer, (_ : Value ).show) {
715
+ def callConstructor (value : Value , ctor : Symbol , args : List [ArgInfo ]): Contextual [Value ] = log(" call " + ctor.show + " , args = " + args.map(_.value.show), printer, (_ : Value ).show) {
700
716
701
- thisV match
717
+ value match
702
718
case ref : Ref =>
703
719
if ctor.hasSource then
704
720
val cls = ctor.owner.enclosingClass.asClass
@@ -720,7 +736,7 @@ object Objects:
720
736
Bottom
721
737
722
738
case _ =>
723
- report.warning(" [Internal error] unexpected constructor call, meth = " + ctor + " , this = " + thisV + Trace .show, Trace .position)
739
+ report.warning(" [Internal error] unexpected constructor call, meth = " + ctor + " , this = " + value + Trace .show, Trace .position)
724
740
Bottom
725
741
}
726
742
@@ -850,7 +866,7 @@ object Objects:
850
866
(outer.widen(1 ), Env .NoEnv )
851
867
else
852
868
// klass.enclosingMethod returns its primary constructor
853
- Env .resolveEnv(klass.owner.enclosingMethod, outer.asInstanceOf [ValueElement ], summon[Env .Data ]).getOrElse(Cold -> Env .NoEnv )
869
+ Env .resolveEnv(klass.owner.enclosingMethod, outer.asInstanceOf [ThisValue ], summon[Env .Data ]).getOrElse(Cold -> Env .NoEnv )
854
870
855
871
val instance = OfClass (klass, outerWidened, ctor, args.map(_.value), envWidened)
856
872
callConstructor(instance, ctor, args)
@@ -880,7 +896,7 @@ object Objects:
880
896
* @param thisV The value for `this` where the variable is used.
881
897
* @param sym The symbol of the variable.
882
898
*/
883
- def readLocal (thisV : ValueElement , sym : Symbol ): Contextual [Value ] = log(" reading local " + sym.show, printer, (_ : Value ).show) {
899
+ def readLocal (thisV : ThisValue , sym : Symbol ): Contextual [Value ] = log(" reading local " + sym.show, printer, (_ : Value ).show) {
884
900
def isByNameParam (sym : Symbol ) = sym.is(Flags .Param ) && sym.info.isInstanceOf [ExprType ]
885
901
Env .resolveEnv(sym.enclosingMethod, thisV, summon[Env .Data ]) match
886
902
case Some (thisV -> env) =>
@@ -934,7 +950,7 @@ object Objects:
934
950
* @param sym The symbol of the variable.
935
951
* @param value The value of the rhs of the assignment.
936
952
*/
937
- def writeLocal (thisV : ValueElement , sym : Symbol , value : Value ): Contextual [Value ] = log(" write local " + sym.show + " with " + value.show, printer, (_ : Value ).show) {
953
+ def writeLocal (thisV : ThisValue , sym : Symbol , value : Value ): Contextual [Value ] = log(" write local " + sym.show + " with " + value.show, printer, (_ : Value ).show) {
938
954
939
955
assert(sym.is(Flags .Mutable ), " Writing to immutable variable " + sym.show)
940
956
Env .resolveEnv(sym.enclosingMethod, thisV, summon[Env .Data ]) match
@@ -955,7 +971,7 @@ object Objects:
955
971
// -------------------------------- algorithm --------------------------------
956
972
957
973
/** Check an individual object */
958
- private def accessObject (classSym : ClassSymbol )(using Context , State .Data , Trace ): Value = log(" accessing " + classSym.show, printer, (_ : Value ).show) {
974
+ private def accessObject (classSym : ClassSymbol )(using Context , State .Data , Trace ): ObjectRef = log(" accessing " + classSym.show, printer, (_ : Value ).show) {
959
975
if classSym.hasSource then
960
976
State .checkObjectAccess(classSym)
961
977
else
@@ -992,13 +1008,13 @@ object Objects:
992
1008
* @param klass The enclosing class where the expression is located.
993
1009
* @param cacheResult It is used to reduce the size of the cache.
994
1010
*/
995
- def eval (expr : Tree , thisV : ValueElement , klass : ClassSymbol , cacheResult : Boolean = false ): Contextual [Value ] = log(" evaluating " + expr.show + " , this = " + thisV.show + " , regions = " + Regions .show + " in " + klass.show, printer, (_ : Value ).show) {
1011
+ def eval (expr : Tree , thisV : ThisValue , klass : ClassSymbol , cacheResult : Boolean = false ): Contextual [Value ] = log(" evaluating " + expr.show + " , this = " + thisV.show + " , regions = " + Regions .show + " in " + klass.show, printer, (_ : Value ).show) {
996
1012
cache.cachedEval(thisV, expr, cacheResult) { expr => cases(expr, thisV, klass) }
997
1013
}
998
1014
999
1015
1000
1016
/** Evaluate a list of expressions */
1001
- def evalExprs (exprs : List [Tree ], thisV : ValueElement , klass : ClassSymbol ): Contextual [List [Value ]] =
1017
+ def evalExprs (exprs : List [Tree ], thisV : ThisValue , klass : ClassSymbol ): Contextual [List [Value ]] =
1002
1018
exprs.map { expr => eval(expr, thisV, klass) }
1003
1019
1004
1020
/** Handles the evaluation of different expressions
@@ -1009,7 +1025,7 @@ object Objects:
1009
1025
* @param thisV The value for `C.this` where `C` is represented by the parameter `klass`.
1010
1026
* @param klass The enclosing class where the expression `expr` is located.
1011
1027
*/
1012
- def cases (expr : Tree , thisV : ValueElement , klass : ClassSymbol ): Contextual [Value ] = log(" evaluating " + expr.show + " , this = " + thisV.show + " in " + klass.show, printer, (_ : Value ).show) {
1028
+ def cases (expr : Tree , thisV : ThisValue , klass : ClassSymbol ): Contextual [Value ] = log(" evaluating " + expr.show + " , this = " + thisV.show + " in " + klass.show, printer, (_ : Value ).show) {
1013
1029
val trace2 = trace.add(expr)
1014
1030
1015
1031
expr match
@@ -1211,7 +1227,7 @@ object Objects:
1211
1227
* Object access elission happens when the object access is used as a prefix
1212
1228
* in `new o.C` and `C` does not need an outer.
1213
1229
*/
1214
- def evalType (tp : Type , thisV : ValueElement , klass : ClassSymbol , elideObjectAccess : Boolean = false ): Contextual [Value ] = log(" evaluating " + tp.show, printer, (_ : Value ).show) {
1230
+ def evalType (tp : Type , thisV : ThisValue , klass : ClassSymbol , elideObjectAccess : Boolean = false ): Contextual [Value ] = log(" evaluating " + tp.show, printer, (_ : Value ).show) {
1215
1231
tp match
1216
1232
case _ : ConstantType =>
1217
1233
Bottom
@@ -1261,7 +1277,7 @@ object Objects:
1261
1277
}
1262
1278
1263
1279
/** Evaluate arguments of methods and constructors */
1264
- def evalArgs (args : List [Arg ], thisV : ValueElement , klass : ClassSymbol ): Contextual [List [ArgInfo ]] =
1280
+ def evalArgs (args : List [Arg ], thisV : ThisValue , klass : ClassSymbol ): Contextual [List [ArgInfo ]] =
1265
1281
val argInfos = new mutable.ArrayBuffer [ArgInfo ]
1266
1282
args.foreach { arg =>
1267
1283
val res =
@@ -1297,7 +1313,7 @@ object Objects:
1297
1313
* @param thisV The value of the current object to be initialized.
1298
1314
* @param klass The class to which the template belongs.
1299
1315
*/
1300
- def init (tpl : Template , thisV : Ref , klass : ClassSymbol ): Contextual [Value ] = log(" init " + klass.show, printer, (_ : Value ).show) {
1316
+ def init (tpl : Template , thisV : Ref , klass : ClassSymbol ): Contextual [Ref ] = log(" init " + klass.show, printer, (_ : Value ).show) {
1301
1317
val paramsMap = tpl.constr.termParamss.flatten.map { vdef =>
1302
1318
vdef.name -> Env .valValue(vdef.symbol)
1303
1319
}.toMap
@@ -1461,7 +1477,7 @@ object Objects:
1461
1477
* @param thisV The value for `C.this` where `C` is represented by the parameter `klass`.
1462
1478
* @param klass The enclosing class where the type `tref` is located.
1463
1479
*/
1464
- def outerValue (tref : TypeRef , thisV : ValueElement , klass : ClassSymbol ): Contextual [Value ] =
1480
+ def outerValue (tref : TypeRef , thisV : ThisValue , klass : ClassSymbol ): Contextual [Value ] =
1465
1481
val cls = tref.classSymbol.asClass
1466
1482
if tref.prefix == NoPrefix then
1467
1483
val enclosing = cls.owner.lexicallyEnclosingClass.asClass
0 commit comments