@@ -56,16 +56,9 @@ import dotty.tools.dotc.util.SrcPos
5656 * This principle not only put initialization of static objects on a solid foundation, but also
5757 * avoids whole-program analysis.
5858 *
59- * 2. The design is based on the concept of "Top" --- a Top value may not be actively
60- * used during initialization, i.e., it's forbidden to call methods or access fields of a Top.
61- * Method arguments are widened to Top by default unless specified to be sensitive.
62- * Method parameters captured in lambdas or inner classes are always widened to Top.
59+ * 2. It is inter-procedural and flow-sensitive.
6360 *
64- * 3. It is inter-procedural and flow-sensitive.
65- *
66- * 4. It is object-sensitive by default and parameter-sensitive on-demand.
67- *
68- * 5. The check is modular in the sense that each object is checked separately and there is no
61+ * 3. The check is modular in the sense that each object is checked separately and there is no
6962 * whole-program analysis. However, the check is not modular in terms of project boundaries.
7063 *
7164 */
@@ -91,30 +84,24 @@ class Objects(using Context @constructorOnly):
9184 /** Syntax for the data structure abstraction used in abstract domain:
9285 *
9386 * ve ::= ObjectRef(class) // global object
94- * | OfClass(class, vs[outer] , ctor, args, env) // instance of a class
95- * | OfArray(object[owner] , regions)
96- * | Fun(... , env) // value elements that can be contained in ValueSet
87+ * | OfClass(class, ownerObject , ctor) // instance of a class
88+ * | OfArray(ownerObject , regions) // represents values of native array class in Array.scala
89+ * | Fun(code , env) // value elements that can be contained in ValueSet
9790 * | SafeValue // values on which method calls and field accesses won't cause warnings. Int, String, etc.
91+ * | UnknownValue // values whose source are unknown at compile time
92+ * | Package // represets a package
9893 * vs ::= ValueSet(ve) // set of abstract values
9994 * Bottom ::= ValueSet(Empty)
100- * val ::= ve | Top | UnknownValue | vs | Package // all possible abstract values in domain
101- * Ref ::= ObjectRef | OfClass // values that represent a reference to some (global or instance) object
102- * ThisValue ::= Ref | Top // possible values for 'this'
103- *
104- * refMap = Ref -> ( valsMap, varsMap, outersMap ) // refMap stores field informations of an object or instance
105- * valsMap = valsym -> val // maps immutable fields to their values
106- * varsMap = valsym -> addr // each mutable field has an abstract address
107- * outersMap = class -> val // maps outer objects to their values
108- *
109- * arrayMap = OfArray -> addr // an array has one address that stores the join value of every element
95+ * val ::= ve | vs
96+ * Ref ::= ObjectRef | OfClass | OfArray // values that represent a reference to some (global or instance) object
97+ * ThisValue ::= Ref | vs // possible values for 'this'
98+ * LocalEnv(meth, ownerObject) // represents environments for methods or functions
99+ * Scope ::= Ref | LocalEnv
100+ * ScopeSet ::= Set(Scope)
110101 *
111- * heap = addr -> val // heap is mutable
112- *
113- * env = (valsMap, Option[env]) // stores local variables in the residing method, and possibly outer environments
114- *
115- * addr ::= localVarAddr(regions, valsym, owner)
116- * | fieldVarAddr(regions, valsym, owner) // independent of OfClass/ObjectRef
117- * | arrayAddr(regions, owner) // independent of array element type
102+ * valsMap = sym -> val // maps variables to their values
103+ * outersMap = classSym -> ScopeSEt // maps the possible outer scopes for a corresponding (parent) class
104+ * heap.MutableData = Scope -> (valsMap, outersMap) // heap is mutable
118105 *
119106 * regions ::= List(sourcePosition)
120107 */
@@ -289,6 +276,13 @@ class Objects(using Context @constructorOnly):
289276 assert(typeSymbol.isDefined, " Invalid creation of SafeValue with type " + tpe)
290277 new SafeValue (typeSymbol.get)
291278
279+ /** Represents values unknown to the checker, such as values loaded without source
280+ * UnknownValue is not ValueElement since RefSet containing UnknownValue
281+ * is equivalent to UnknownValue
282+ */
283+ case object UnknownValue extends ValueElement :
284+ def show (using Context ): String = " UnknownValue"
285+
292286 /**
293287 * Represents a set of values
294288 *
@@ -310,29 +304,10 @@ class Objects(using Context @constructorOnly):
310304 assert(packageSym.is(Flags .Package ), " Invalid symbol to create Package!" )
311305 Package (packageSym.moduleClass.asClass)
312306
313- /** Represents values unknown to the checker, such as values loaded without source
314- * UnknownValue is not ValueElement since RefSet containing UnknownValue
315- * is equivalent to UnknownValue
316- */
317- case object UnknownValue extends Value :
318- def show (using Context ): String = " UnknownValue"
319-
320- /** Represents values lost due to widening
321- *
322- * This is the top of the abstract domain lattice, which should not
323- * be used during initialization.
324- *
325- * Top is not ValueElement since RefSet containing Top
326- * is equivalent to Top
327- */
328-
329- case object Top extends Value :
330- def show (using Context ): String = " Top"
331-
332307 val Bottom = ValueSet (ListSet .empty)
333308
334309 /** Possible types for 'this' */
335- type ThisValue = Ref | Top . type | ValueSet
310+ type ThisValue = Ref | ValueSet
336311
337312 /** Checking state */
338313 object State :
@@ -572,18 +547,6 @@ class Objects(using Context @constructorOnly):
572547 /** Abstract heap for mutable fields
573548 */
574549 object Heap :
575- abstract class Addr :
576- /** The static object which owns the mutable slot */
577- def owner : ClassSymbol
578- def getTrace : Trace = Trace .empty
579-
580- /** The address for mutable fields of objects. */
581- private case class FieldAddr (regions : Regions .Data , field : Symbol , owner : ClassSymbol )(trace : Trace ) extends Addr :
582- override def getTrace : Trace = trace
583-
584- /** The address for mutable local variables . */
585- private case class LocalVarAddr (regions : Regions .Data , sym : Symbol , owner : ClassSymbol ) extends Addr
586-
587550 private case class ScopeBody (
588551 paramsMap : Map [Symbol , Value ],
589552 valsMap : Map [Symbol , Value ],
@@ -690,15 +653,6 @@ class Objects(using Context @constructorOnly):
690653 def writeJoinOuter (scope : Scope , outer : Symbol , outerScope : ScopeSet )(using mutable : MutableData ): Unit =
691654 mutable.writeJoinOuter(scope, outer, outerScope)
692655
693- def localVarAddr (regions : Regions .Data , sym : Symbol , owner : ClassSymbol ): Addr =
694- LocalVarAddr (regions, sym, owner)
695-
696- def fieldVarAddr (regions : Regions .Data , sym : Symbol , owner : ClassSymbol )(using Trace ): Addr =
697- FieldAddr (regions, sym, owner)(summon[Trace ])
698-
699- def arrayAddr (regions : Regions .Data , owner : ClassSymbol )(using Trace , Context ): Addr =
700- FieldAddr (regions, defn.ArrayClass , owner)(summon[Trace ])
701-
702656 def getHeapData ()(using mutable : MutableData ): Data = mutable.heap
703657
704658 def setHeap (newHeap : Data )(using mutable : MutableData ): Unit = mutable.heap = newHeap
@@ -777,10 +731,6 @@ class Objects(using Context @constructorOnly):
777731 def join (b : Value ): Value =
778732 assert(! a.isInstanceOf [Package ] && ! b.isInstanceOf [Package ], " Unexpected join between " + a + " and " + b)
779733 (a, b) match
780- case (Top , _) => Top
781- case (_, Top ) => Top
782- case (UnknownValue , _) => UnknownValue
783- case (_, UnknownValue ) => UnknownValue
784734 case (Bottom , b) => b
785735 case (a, Bottom ) => a
786736 case (ValueSet (values1), ValueSet (values2)) => ValueSet (values1 ++ values2)
@@ -813,7 +763,7 @@ class Objects(using Context @constructorOnly):
813763 else
814764 val klass = sym.asClass
815765 a match
816- case UnknownValue | Top => a
766+ case UnknownValue => a
817767 case Package (packageModuleClass) =>
818768 // the typer might mistakenly set the receiver to be a package instead of package object.
819769 // See pos/packageObjectStringInterpolator.scala
@@ -844,8 +794,6 @@ class Objects(using Context @constructorOnly):
844794 else
845795 scopes.reduce { (s1, s2) => s1.join(s2) }
846796
847- // def widen(height: Int): Contextual[List[V]] = values.map(_.widen(height)).toList
848-
849797 extension [V : Join ](map : Map [Symbol , V ])
850798 def join (sym : Symbol , value : V ): Map [Symbol , V ] =
851799 if ! map.contains(sym) then map.updated(sym, value)
@@ -873,9 +821,6 @@ class Objects(using Context @constructorOnly):
873821 */
874822 def call (value : Value , meth : Symbol , args : List [ArgInfo ], receiver : Type , superType : Type , needResolve : Boolean = true ): Contextual [Value ] = log(" call " + meth.show + " , this = " + value.show + " , args = " + args.map(_.value.show), printer, (_ : Value ).show) {
875823 value.filterClass(meth.owner) match
876- case Top =>
877- report.warning(" Value is unknown to the checker due to widening. " + Trace .show, Trace .position)
878- Bottom
879824 case UnknownValue =>
880825 reportWarningForUnknownValue(" Using unknown value. " + Trace .show, Trace .position)
881826
@@ -1084,9 +1029,6 @@ class Objects(using Context @constructorOnly):
10841029 */
10851030 def select (value : Value , field : Symbol , receiver : Type , needResolve : Boolean = true ): Contextual [Value ] = log(" select " + field.show + " , this = " + value.show, printer, (_ : Value ).show) {
10861031 value.filterClass(field.owner) match
1087- case Top =>
1088- report.warning(" Value is unknown to the checker due to widening. " + Trace .show, Trace .position)
1089- Bottom
10901032 case UnknownValue =>
10911033 reportWarningForUnknownValue(" Using unknown value. " + Trace .show, Trace .position)
10921034
@@ -1171,8 +1113,6 @@ class Objects(using Context @constructorOnly):
11711113 */
11721114 def assign (lhs : Value , field : Symbol , rhs : Value , rhsTyp : Type ): Contextual [Value ] = log(" Assign" + field.show + " of " + lhs.show + " , rhs = " + rhs.show, printer, (_ : Value ).show) {
11731115 lhs.filterClass(field.owner) match
1174- case Top =>
1175- report.warning(" Value is unknown to the checker due to widening. " + Trace .show, Trace .position)
11761116 case UnknownValue =>
11771117 val _ = reportWarningForUnknownValue(" Assigning to unknown value. " + Trace .show, Trace .position)
11781118 case p : Package =>
@@ -1220,7 +1160,7 @@ class Objects(using Context @constructorOnly):
12201160 case UnknownValue =>
12211161 reportWarningForUnknownValue(" Instantiating when outer is unknown. " + Trace .show, Trace .position)
12221162
1223- case outer : (Ref | Top . type | Package ) =>
1163+ case outer : (Ref | Package ) =>
12241164 if klass == defn.ArrayClass then
12251165 args.head.tree.tpe match
12261166 case ConstantType (Constants .Constant (0 )) =>
@@ -1246,7 +1186,7 @@ class Objects(using Context @constructorOnly):
12461186 if enclosingMethod == outerCls.primaryConstructor then
12471187 ScopeSet (Set (thisV.asInstanceOf [Ref ]))
12481188 else
1249- Env .resolveEnvByMethod(klass.owner.enclosingMethod, thisV, summon[Scope ]).getOrElse(Top -> Env .NoEnv )._2
1189+ Env .resolveEnvByMethod(klass.owner.enclosingMethod, thisV, summon[Scope ]).getOrElse(UnknownValue -> Env .NoEnv )._2
12501190
12511191 val instance = OfClass (klass, envWidened, ctor)
12521192 callConstructor(instance, ctor, args)
@@ -1280,9 +1220,6 @@ class Objects(using Context @constructorOnly):
12801220 eval(fun.code, fun.thisV, fun.klass)
12811221 case UnknownValue =>
12821222 reportWarningForUnknownValue(" Calling on unknown value. " + Trace .show, Trace .position)
1283- case Top =>
1284- report.warning(" Calling on value lost due to widening. " + Trace .show, Trace .position)
1285- Bottom
12861223 case Bottom => Bottom
12871224 case ValueSet (values) if values.size == 1 =>
12881225 evalByNameParam(values.head)
@@ -2073,7 +2010,6 @@ class Objects(using Context @constructorOnly):
20732010 else accessObject(target)
20742011 else
20752012 thisV match
2076- case Top => Top
20772013 case Bottom => Bottom
20782014 case ref : Ref =>
20792015 recur(ScopeSet (Set (ref)))
0 commit comments