@@ -81,13 +81,33 @@ class Objects(using Context @constructorOnly):
8181 val allowList : Set [Symbol ] = Set (SetNode_EmptySetNode , HashSet_EmptySet , Vector_EmptyIterator , MapNode_EmptyMapNode , HashMap_EmptyMap ,
8282 ManifestFactory_ObjectTYPE , ManifestFactory_NothingTYPE , ManifestFactory_NullTYPE )
8383
84+ /**
85+ * Whether the analysis work in best-effort mode in contrast to aggressive mode.
86+ *
87+ * - In best-effort mode, the analysis tries to be fast, useful and unobtrusive.
88+ * - In the aggressive mode, the analysis tries to be sound and verbose by spending more check time.
89+ *
90+ * In both mode, there is a worst-case guarantee based on a quota on the
91+ * number of method calls in initializing a global object.
92+ *
93+ * We use a patch to set `BestEffort` to `false` in testing community projects.
94+ */
95+ val BestEffort : Boolean = true
96+
97+ /** The analysis has run out of quota */
98+ class OutOfQuotaException (count : Int ) extends Exception
99+
100+ def checkCost (count : Int ): Unit =
101+ if count > 500 && BestEffort || count > 2000 && ! BestEffort then
102+ throw new OutOfQuotaException (count)
103+
84104 // ----------------------------- abstract domain -----------------------------
85105
86106 /** Syntax for the data structure abstraction used in abstract domain:
87107 *
88108 * ve ::= ObjectRef(class) // global object
89- * | InstanceRef(class, ownerObject, ctor, regions) // instance of a class
90- * | ArrayRef(ownerObject, regions) // represents values of native array class in Array.scala
109+ * | InstanceRef(class, ownerObject, ctor, regions) // instance of a class
110+ * | ArrayRef(ownerObject, regions) // represents values of native array class in Array.scala
91111 * | Fun(code, thisV, scope) // value elements that can be contained in ValueSet
92112 * | SafeValue // values on which method calls and field accesses won't cause warnings. Int, String, etc.
93113 * | UnknownValue // values whose source are unknown at compile time
@@ -100,8 +120,8 @@ class Objects(using Context @constructorOnly):
100120 * EnvRef(tree, ownerObject) // represents environments for evaluating methods, functions, or lazy/by-name values
101121 * EnvSet ::= Set(EnvRef)
102122 * InstanceBody ::= (valsMap: Map[Symbol, Value],
103- outersMap: Map[ClassSymbol, Value],
104- outerEnv: EnvSet) // represents combined information of all instances represented by a ref
123+ * outersMap: Map[ClassSymbol, Value],
124+ * outerEnv: EnvSet) // represents combined information of all instances represented by a ref
105125 * Heap ::= Ref -> InstanceBody // heap is mutable
106126 * EnvBody ::= (valsMap: Map[Symbol, Value],
107127 * thisV: Value,
@@ -173,18 +193,29 @@ class Objects(using Context @constructorOnly):
173193
174194 def outerValue (sym : Symbol )(using Heap .MutableData ): Value = Heap .readOuter(this , sym)
175195
196+ def hasOuter (classSymbol : Symbol )(using Heap .MutableData ): Boolean = Heap .hasOuter(this , classSymbol)
197+
176198 def outer (using Heap .MutableData ): Value = this .outerValue(klass)
177199
178200 def outerEnv (using Heap .MutableData ): Env .EnvSet = Heap .readOuterEnv(this )
179201 end Ref
180202
181- /** A reference to a static object */
203+ /** A reference to a static object
204+ *
205+ * Invariant: The reference itself should not contain any state
206+ *
207+ * Rationale: There can be multiple references to the same object. They must
208+ * share the same state.
209+ */
182210 case class ObjectRef private (klass : ClassSymbol )(using Trace ) extends Ref :
183- var afterSuperCall = false
184-
185- def isAfterSuperCall = afterSuperCall
211+ /** Use the special outer to denote whether the super constructor of the
212+ * object has been called or not.
213+ */
214+ def isAfterSuperCall (using Heap .MutableData ) =
215+ this .hasOuter(klass.sourceModule)
186216
187- def setAfterSuperCall (): Unit = afterSuperCall = true
217+ def setAfterSuperCall ()(using Heap .MutableData ): Unit =
218+ this .initOuter(klass.sourceModule, Bottom )
188219
189220 def owner = klass
190221
@@ -340,10 +371,39 @@ class Objects(using Context @constructorOnly):
340371 private [State ] val checkingObjects = new mutable.ArrayBuffer [ObjectRef ]
341372 private [State ] val checkedObjects = new mutable.ArrayBuffer [ObjectRef ]
342373 private [State ] val pendingTraces = new mutable.ArrayBuffer [Trace ]
374+
375+ /** It records how many calls have being analyzed for the current object under check */
376+ private [State ] val checkingCosts = new mutable.ArrayBuffer [Int ]
377+
378+ private [State ] val quotaExhaustedObjects = new mutable.ArrayBuffer [ObjectRef ]
379+
380+ def addChecking (obj : ObjectRef ): Unit =
381+ this .checkingObjects += obj
382+ this .checkingCosts += 0
383+
384+ def popChecking (): Unit =
385+ val index = this .checkingObjects.size - 1
386+ checkingObjects.remove(index)
387+ checkingCosts.remove(index)
388+
389+ def addChecked (obj : ObjectRef ): Unit =
390+ this .checkedObjects += obj
391+
392+ def addQuotaExhausted (obj : ObjectRef ): Unit =
393+ this .quotaExhaustedObjects += obj
343394 end Data
344395
345396 def currentObject (using data : Data ): ClassSymbol = data.checkingObjects.last.klass
346397
398+ def recordCall ()(using data : Data ): Unit =
399+ val lastIndex = data.checkingCosts.size - 1
400+ val callCount = data.checkingCosts(lastIndex) + 1
401+ data.checkingCosts(lastIndex) = callCount
402+ checkCost(callCount)
403+
404+ def isQuotaExhausted (obj : ObjectRef )(using data : Data ): Boolean =
405+ data.quotaExhaustedObjects.contains(obj)
406+
347407 private def doCheckObject (classSym : ClassSymbol )(using ctx : Context , data : Data , heap : Heap .MutableData , envMap : EnvMap .EnvMapMutableData ) =
348408 val tpl = classSym.defTree.asInstanceOf [TypeDef ].rhs.asInstanceOf [Template ]
349409
@@ -362,18 +422,34 @@ class Objects(using Context @constructorOnly):
362422 val obj = ObjectRef (classSym)
363423 given Scope = obj
364424 log(" Iteration " + count) {
365- data.checkingObjects += obj
366- init(tpl, obj, classSym)
425+ data.addChecking(obj)
426+
427+ try
428+ init(tpl, obj, classSym)
429+ catch case _ : OutOfQuotaException =>
430+ report.warning(" Giving up checking initialization of " + classSym + " due to exhausted budget" , classSym.sourcePos)
431+ data.addQuotaExhausted(obj)
432+ data.addChecked(obj)
433+ data.popChecking()
434+ return obj
435+
367436 assert(data.checkingObjects.last.klass == classSym, " Expect = " + classSym.show + " , found = " + data.checkingObjects.last.klass)
368- data.checkingObjects.remove(data.checkingObjects.size - 1 )
437+
438+ data.popChecking()
369439 }
370440
371441 val hasError = ctx.reporter.pendingMessages.nonEmpty
372442 if cache.hasChanged && ! hasError then
373- cache.prepareForNextIteration()
374- iterate()
443+ if count <= 3 then
444+ cache.prepareForNextIteration()
445+ iterate()
446+ else
447+ if ! BestEffort then
448+ report.warning(" Giving up checking initialization of " + classSym + " due to iteration > = " + count, classSym.sourcePos)
449+ data.addChecked(obj)
450+ obj
375451 else
376- data.checkedObjects += obj
452+ data.addChecked( obj)
377453 obj
378454 end iterate
379455
@@ -688,6 +764,9 @@ class Objects(using Context @constructorOnly):
688764 def readOuter (ref : Ref , parent : Symbol )(using mutable : MutableData ): Value =
689765 mutable.heap(ref).outersMap(parent)
690766
767+ def hasOuter (ref : Ref , parent : Symbol )(using mutable : MutableData ): Boolean =
768+ mutable.heap(ref).outersMap.contains(parent)
769+
691770 def readOuterEnv (ref : Ref )(using mutable : MutableData ): Env .EnvSet =
692771 mutable.heap(ref).outerEnvs
693772
@@ -959,15 +1038,11 @@ class Objects(using Context @constructorOnly):
9591038 if ! map.contains(sym) then map.updated(sym, value)
9601039 else map.updated(sym, map(sym).join(value))
9611040
962- /** Check if the checker option reports warnings about unknown code
963- */
964- val reportUnknown : Boolean = false
965-
9661041 def reportWarningForUnknownValue (msg : => String , pos : SrcPos )(using Context ): Value =
967- if reportUnknown then
968- report.warning(msg, pos)
1042+ if BestEffort then
9691043 Bottom
9701044 else
1045+ report.warning(msg, pos)
9711046 UnknownValue
9721047
9731048 /** Handle method calls `e.m(args)`.
@@ -1081,6 +1156,7 @@ class Objects(using Context @constructorOnly):
10811156
10821157 val env2 = Env .ofDefDef(ddef, args.map(_.value), thisV, outerEnv)
10831158 extendTrace(ddef) {
1159+ State .recordCall()
10841160 given Scope = env2
10851161 cache.cachedEval(ref, ddef.rhs, cacheResult = true ) { expr =>
10861162 Returns .installHandler(meth)
@@ -1115,14 +1191,17 @@ class Objects(using Context @constructorOnly):
11151191 case env : Env .EnvRef => Env .ofDefDef(ddef, args.map(_.value), thisVOfClosure, Env .EnvSet (Set (env)))
11161192 }
11171193 given Scope = funEnv
1118- extendTrace(code) { eval(ddef.rhs, thisVOfClosure, klass, cacheResult = true ) }
1194+ extendTrace(code) {
1195+ State .recordCall()
1196+ eval(ddef.rhs, thisVOfClosure, klass, cacheResult = true )
1197+ }
11191198 else
11201199 // The methods defined in `Any` and `AnyRef` are trivial and don't affect initialization.
11211200 if meth.owner == defn.AnyClass || meth.owner == defn.ObjectClass then
11221201 value
11231202 else
11241203 // In future, we will have Tasty for stdlib classes and can abstractly interpret that Tasty.
1125- // For now, return `UnknownValue` to ensure soundness and trigger a warning when reportUnknown = true .
1204+ // For now, return `UnknownValue` to ensure soundness and trigger a warning when BestEffort = false .
11261205 UnknownValue
11271206 end if
11281207 end if
@@ -1158,6 +1237,7 @@ class Objects(using Context @constructorOnly):
11581237 extendTrace(cls.defTree) { eval(tpl, ref, cls, cacheResult = true ) }
11591238 else
11601239 extendTrace(ddef) { // The return values for secondary constructors can be ignored
1240+ State .recordCall()
11611241 Returns .installHandler(ctor)
11621242 eval(ddef.rhs, ref, cls, cacheResult = true )
11631243 Returns .popHandler(ctor)
@@ -1212,34 +1292,43 @@ class Objects(using Context @constructorOnly):
12121292 if target.is(Flags .Lazy ) then // select a lazy field
12131293 if ref.hasVal(target) then
12141294 ref.valValue(target)
1295+
12151296 else if target.hasSource then
12161297 val rhs = target.defTree.asInstanceOf [ValDef ].rhs
12171298 given Scope = Env .ofByName(target, rhs, ref, Env .NoEnv )
12181299 val result = eval(rhs, ref, target.owner.asClass, cacheResult = true )
12191300 ref.initVal(target, result)
12201301 result
1302+
12211303 else
12221304 UnknownValue
1305+
12231306 else if target.exists then
12241307 def isNextFieldOfColonColon : Boolean = ref.klass == defn.ConsClass && target.name.toString == " next"
12251308 if target.isMutableVarOrAccessor && ! isNextFieldOfColonColon then
12261309 if ref.hasVar(target) then
12271310 if ref.owner == State .currentObject then
12281311 ref.varValue(target)
1312+
12291313 else
12301314 errorReadOtherStaticObject(State .currentObject, ref)
12311315 Bottom
1316+
12321317 else if ref.isObjectRef && ref.klass.hasSource then
1233- report.warning( " Access uninitialized field " + field.show + " . " + Trace .show, Trace .position )
1318+ errorReadUninitializedField(ref.asObjectRef, field )
12341319 Bottom
1320+
12351321 else
12361322 // initialization error, reported by the initialization checker
12371323 Bottom
1324+
12381325 else if ref.hasVal(target) then
12391326 ref.valValue(target)
1327+
12401328 else if ref.isObjectRef && ref.klass.hasSource then
1241- report.warning( " Access uninitialized field " + field.show + " . " + Trace .show, Trace .position )
1329+ errorReadUninitializedField(ref.asObjectRef, field )
12421330 Bottom
1331+
12431332 else
12441333 // initialization error, reported by the initialization checker
12451334 Bottom
@@ -1686,7 +1775,7 @@ class Objects(using Context @constructorOnly):
16861775 val args = evalArgs(elems.map(Arg .apply), thisV, klass)
16871776 val arr = ArrayRef (State .currentObject, summon[Regions .Data ])
16881777 arr.writeElement(args.map(_.value).join)
1689- call(ObjectRef (module), meth, List (ArgInfo (arr, summon[Trace ], EmptyTree )), module.typeRef, NoType )
1778+ call(accessObject (module), meth, List (ArgInfo (arr, summon[Trace ], EmptyTree )), module.typeRef, NoType )
16901779
16911780 case Inlined (call, bindings, expansion) =>
16921781 evalExprs(bindings, thisV, klass)
@@ -2229,3 +2318,10 @@ class Objects(using Context @constructorOnly):
22292318 printTraceWhenMultiple(scope_trace)
22302319
22312320 report.warning(msg, Trace .position)
2321+
2322+ def errorReadUninitializedField (obj : ObjectRef , field : Symbol )(using State .Data , Trace , Context ): Unit =
2323+ if State .isQuotaExhausted(obj) then
2324+ if ! BestEffort then
2325+ report.warning(" Access uninitialized field of quota exhausted object " + field.show + " . " + Trace .show, Trace .position)
2326+ else
2327+ report.warning(" Access uninitialized field " + field.show + " . " + Trace .show, Trace .position)
0 commit comments