From 7a963e0bfc645f750235d07eaa4a6a58438df3cd Mon Sep 17 00:00:00 2001 From: Fengyun Liu Date: Mon, 8 Dec 2025 22:47:44 +0100 Subject: [PATCH 1/5] Default to BestEffort mode --- .../tools/dotc/transform/init/Objects.scala | 33 ++++++++++++++----- 1 file changed, 24 insertions(+), 9 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/transform/init/Objects.scala b/compiler/src/dotty/tools/dotc/transform/init/Objects.scala index b8a213718a19..9d31391580e7 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Objects.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Objects.scala @@ -81,6 +81,19 @@ class Objects(using Context @constructorOnly): val allowList: Set[Symbol] = Set(SetNode_EmptySetNode, HashSet_EmptySet, Vector_EmptyIterator, MapNode_EmptyMapNode, HashMap_EmptyMap, ManifestFactory_ObjectTYPE, ManifestFactory_NothingTYPE, ManifestFactory_NullTYPE) + /** + * Whether the analysis work in best-effort mode in contrast to aggressive mode. + * + * - In best-effort mode, the analysis tries to be fast, useful and unobtrusive. + * - In the aggressive mode, the analysis tries to be sound and verbose by spending more check time. + * + * In both mode, there is a worst-case guarantee based on a quota on the + * number of method calls in initializing a global object. + * + * We use a patch to set `BestEffort` to `false` in testing community projects. + */ + val BestEffort: Boolean = true + // ----------------------------- abstract domain ----------------------------- /** Syntax for the data structure abstraction used in abstract domain: @@ -370,8 +383,14 @@ class Objects(using Context @constructorOnly): val hasError = ctx.reporter.pendingMessages.nonEmpty if cache.hasChanged && !hasError then - cache.prepareForNextIteration() - iterate() + if count <= 3 then + cache.prepareForNextIteration() + iterate() + else + if !BestEffort then + report.warning("Giving up checking initializatino of " + classSym + " due to complex code", classSym.sourcePos) + data.checkedObjects += obj + obj else data.checkedObjects += obj obj @@ -959,15 +978,11 @@ class Objects(using Context @constructorOnly): if !map.contains(sym) then map.updated(sym, value) else map.updated(sym, map(sym).join(value)) - /** Check if the checker option reports warnings about unknown code - */ - val reportUnknown: Boolean = false - def reportWarningForUnknownValue(msg: => String, pos: SrcPos)(using Context): Value = - if reportUnknown then - report.warning(msg, pos) + if BestEffort then Bottom else + report.warning(msg, pos) UnknownValue /** Handle method calls `e.m(args)`. @@ -1122,7 +1137,7 @@ class Objects(using Context @constructorOnly): value else // In future, we will have Tasty for stdlib classes and can abstractly interpret that Tasty. - // For now, return `UnknownValue` to ensure soundness and trigger a warning when reportUnknown = true. + // For now, return `UnknownValue` to ensure soundness and trigger a warning when BestEffort = false. UnknownValue end if end if From 227ac2b06c3b9f245db6bd37d59b9e0eba4d4d4a Mon Sep 17 00:00:00 2001 From: Fengyun Liu Date: Mon, 15 Dec 2025 16:29:56 +0100 Subject: [PATCH 2/5] Refactor handling of isAfterSuperCall --- .../tools/dotc/transform/init/Objects.scala | 26 ++++++++++++++----- 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/transform/init/Objects.scala b/compiler/src/dotty/tools/dotc/transform/init/Objects.scala index 9d31391580e7..719ac2b8611b 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Objects.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Objects.scala @@ -186,18 +186,29 @@ class Objects(using Context @constructorOnly): def outerValue(sym: Symbol)(using Heap.MutableData): Value = Heap.readOuter(this, sym) + def hasOuter(classSymbol: Symbol)(using Heap.MutableData): Boolean = Heap.hasOuter(this, classSymbol) + def outer(using Heap.MutableData): Value = this.outerValue(klass) def outerEnv(using Heap.MutableData): Env.EnvSet = Heap.readOuterEnv(this) end Ref - /** A reference to a static object */ + /** A reference to a static object + * + * Invariant: The reference itself should not contain any state + * + * Rationale: There can be multiple references to the same object. They must + * share the same state. + */ case class ObjectRef private (klass: ClassSymbol)(using Trace) extends Ref: - var afterSuperCall = false - - def isAfterSuperCall = afterSuperCall + /** Use the special outer to denote whether the super constructor of the + * object has been called or not. + */ + def isAfterSuperCall(using Heap.MutableData) = + this.hasOuter(klass.sourceModule) - def setAfterSuperCall(): Unit = afterSuperCall = true + def setAfterSuperCall()(using Heap.MutableData): Unit = + this.initOuter(klass.sourceModule, Bottom) def owner = klass @@ -707,6 +718,9 @@ class Objects(using Context @constructorOnly): def readOuter(ref: Ref, parent: Symbol)(using mutable: MutableData): Value = mutable.heap(ref).outersMap(parent) + def hasOuter(ref: Ref, parent: Symbol)(using mutable: MutableData): Boolean = + mutable.heap(ref).outersMap.contains(parent) + def readOuterEnv(ref: Ref)(using mutable: MutableData): Env.EnvSet = mutable.heap(ref).outerEnvs @@ -1701,7 +1715,7 @@ class Objects(using Context @constructorOnly): val args = evalArgs(elems.map(Arg.apply), thisV, klass) val arr = ArrayRef(State.currentObject, summon[Regions.Data]) arr.writeElement(args.map(_.value).join) - call(ObjectRef(module), meth, List(ArgInfo(arr, summon[Trace], EmptyTree)), module.typeRef, NoType) + call(accessObject(module), meth, List(ArgInfo(arr, summon[Trace], EmptyTree)), module.typeRef, NoType) case Inlined(call, bindings, expansion) => evalExprs(bindings, thisV, klass) From 2abda6eb844cbafb533b26741d3e22645243819a Mon Sep 17 00:00:00 2001 From: Fengyun Liu Date: Tue, 16 Dec 2025 00:33:47 +0100 Subject: [PATCH 3/5] Enforce quota in analysis --- .../tools/dotc/transform/init/Objects.scala | 88 ++++++++++++++++--- 1 file changed, 77 insertions(+), 11 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/transform/init/Objects.scala b/compiler/src/dotty/tools/dotc/transform/init/Objects.scala index 719ac2b8611b..3a2d0506edcd 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Objects.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Objects.scala @@ -94,13 +94,20 @@ class Objects(using Context @constructorOnly): */ val BestEffort: Boolean = true + /** The analysis has run out of quota */ + class OutOfQuotaException(count: Int) extends Exception + + def checkCost(count: Int): Unit = + if count > 500 && BestEffort || count > 2000 && !BestEffort then + throw new OutOfQuotaException(count) + // ----------------------------- abstract domain ----------------------------- /** Syntax for the data structure abstraction used in abstract domain: * * ve ::= ObjectRef(class) // global object - * | InstanceRef(class, ownerObject, ctor, regions) // instance of a class - * | ArrayRef(ownerObject, regions) // represents values of native array class in Array.scala + * | InstanceRef(class, ownerObject, ctor, regions) // instance of a class + * | ArrayRef(ownerObject, regions) // represents values of native array class in Array.scala * | Fun(code, thisV, scope) // value elements that can be contained in ValueSet * | SafeValue // values on which method calls and field accesses won't cause warnings. Int, String, etc. * | UnknownValue // values whose source are unknown at compile time @@ -113,8 +120,8 @@ class Objects(using Context @constructorOnly): * EnvRef(tree, ownerObject) // represents environments for evaluating methods, functions, or lazy/by-name values * EnvSet ::= Set(EnvRef) * InstanceBody ::= (valsMap: Map[Symbol, Value], - outersMap: Map[ClassSymbol, Value], - outerEnv: EnvSet) // represents combined information of all instances represented by a ref + * outersMap: Map[ClassSymbol, Value], + * outerEnv: EnvSet) // represents combined information of all instances represented by a ref * Heap ::= Ref -> InstanceBody // heap is mutable * EnvBody ::= (valsMap: Map[Symbol, Value], * thisV: Value, @@ -364,10 +371,39 @@ class Objects(using Context @constructorOnly): private[State] val checkingObjects = new mutable.ArrayBuffer[ObjectRef] private[State] val checkedObjects = new mutable.ArrayBuffer[ObjectRef] private[State] val pendingTraces = new mutable.ArrayBuffer[Trace] + + /** It records how many calls have being analyzed for the current object under check */ + private[State] val checkingCosts = new mutable.ArrayBuffer[Int] + + private[State] val quotaExhaustedObjects = new mutable.ArrayBuffer[ObjectRef] + + def addChecking(obj: ObjectRef): Unit = + this.checkingObjects += obj + this.checkingCosts += 0 + + def popChecking(): Unit = + val index = this.checkingObjects.size - 1 + checkingObjects.remove(index) + checkingCosts.remove(index) + + def addChecked(obj: ObjectRef): Unit = + this.checkedObjects += obj + + def addQuotaExhausted(obj: ObjectRef): Unit = + this.quotaExhaustedObjects += obj end Data def currentObject(using data: Data): ClassSymbol = data.checkingObjects.last.klass + def recordCall()(using data: Data): Unit = + val lastIndex = data.checkingCosts.size - 1 + val callCount = data.checkingCosts(lastIndex) + 1 + data.checkingCosts(lastIndex) = callCount + checkCost(callCount) + + def isQuotaExhausted(obj: ObjectRef)(using data: Data): Boolean = + data.quotaExhaustedObjects.contains(obj) + private def doCheckObject(classSym: ClassSymbol)(using ctx: Context, data: Data, heap: Heap.MutableData, envMap: EnvMap.EnvMapMutableData) = val tpl = classSym.defTree.asInstanceOf[TypeDef].rhs.asInstanceOf[Template] @@ -386,10 +422,20 @@ class Objects(using Context @constructorOnly): val obj = ObjectRef(classSym) given Scope = obj log("Iteration " + count) { - data.checkingObjects += obj - init(tpl, obj, classSym) + data.addChecking(obj) + + try + init(tpl, obj, classSym) + catch case _: OutOfQuotaException => + if !BestEffort then + report.warning("Giving up checking initializatino of " + classSym + " due to exhausted budget", classSym.sourcePos) + data.addQuotaExhausted(obj) + data.addChecked(obj) + return obj + assert(data.checkingObjects.last.klass == classSym, "Expect = " + classSym.show + ", found = " + data.checkingObjects.last.klass) - data.checkingObjects.remove(data.checkingObjects.size - 1) + + data.popChecking() } val hasError = ctx.reporter.pendingMessages.nonEmpty @@ -400,10 +446,10 @@ class Objects(using Context @constructorOnly): else if !BestEffort then report.warning("Giving up checking initializatino of " + classSym + " due to complex code", classSym.sourcePos) - data.checkedObjects += obj + data.addChecked(obj) obj else - data.checkedObjects += obj + data.addChecked(obj) obj end iterate @@ -1110,6 +1156,7 @@ class Objects(using Context @constructorOnly): val env2 = Env.ofDefDef(ddef, args.map(_.value), thisV, outerEnv) extendTrace(ddef) { + State.recordCall() given Scope = env2 cache.cachedEval(ref, ddef.rhs, cacheResult = true) { expr => Returns.installHandler(meth) @@ -1144,7 +1191,10 @@ class Objects(using Context @constructorOnly): case env: Env.EnvRef => Env.ofDefDef(ddef, args.map(_.value), thisVOfClosure, Env.EnvSet(Set(env))) } given Scope = funEnv - extendTrace(code) { eval(ddef.rhs, thisVOfClosure, klass, cacheResult = true) } + extendTrace(code) { + State.recordCall() + eval(ddef.rhs, thisVOfClosure, klass, cacheResult = true) + } else // The methods defined in `Any` and `AnyRef` are trivial and don't affect initialization. if meth.owner == defn.AnyClass || meth.owner == defn.ObjectClass then @@ -1187,6 +1237,7 @@ class Objects(using Context @constructorOnly): extendTrace(cls.defTree) { eval(tpl, ref, cls, cacheResult = true) } else extendTrace(ddef) { // The return values for secondary constructors can be ignored + State.recordCall() Returns.installHandler(ctor) eval(ddef.rhs, ref, cls, cacheResult = true) Returns.popHandler(ctor) @@ -1241,34 +1292,49 @@ class Objects(using Context @constructorOnly): if target.is(Flags.Lazy) then // select a lazy field if ref.hasVal(target) then ref.valValue(target) + else if target.hasSource then val rhs = target.defTree.asInstanceOf[ValDef].rhs given Scope = Env.ofByName(target, rhs, ref, Env.NoEnv) val result = eval(rhs, ref, target.owner.asClass, cacheResult = true) ref.initVal(target, result) result + else UnknownValue + else if target.exists then def isNextFieldOfColonColon: Boolean = ref.klass == defn.ConsClass && target.name.toString == "next" if target.isMutableVarOrAccessor && !isNextFieldOfColonColon then if ref.hasVar(target) then if ref.owner == State.currentObject then ref.varValue(target) + else errorReadOtherStaticObject(State.currentObject, ref) Bottom + else if ref.isObjectRef && ref.klass.hasSource then - report.warning("Access uninitialized field " + field.show + ". " + Trace.show, Trace.position) + if State.isQuotaExhausted(ref.asObjectRef) then + if !BestEffort then + report.warning("Access uninitialized field of quota exhausted object " + field.show + ". " + Trace.show, Trace.position) + + else + report.warning("Access uninitialized field " + field.show + ". " + Trace.show, Trace.position) + Bottom + else // initialization error, reported by the initialization checker Bottom + else if ref.hasVal(target) then ref.valValue(target) + else if ref.isObjectRef && ref.klass.hasSource then report.warning("Access uninitialized field " + field.show + ". " + Trace.show, Trace.position) Bottom + else // initialization error, reported by the initialization checker Bottom From ceb2517eb75e4e6925b553e4bd122359cbd3156a Mon Sep 17 00:00:00 2001 From: Fengyun Liu Date: Tue, 16 Dec 2025 00:41:21 +0100 Subject: [PATCH 4/5] Refactor error reporting --- .../tools/dotc/transform/init/Objects.scala | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/transform/init/Objects.scala b/compiler/src/dotty/tools/dotc/transform/init/Objects.scala index 3a2d0506edcd..c369e855af63 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Objects.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Objects.scala @@ -1315,13 +1315,7 @@ class Objects(using Context @constructorOnly): Bottom else if ref.isObjectRef && ref.klass.hasSource then - if State.isQuotaExhausted(ref.asObjectRef) then - if !BestEffort then - report.warning("Access uninitialized field of quota exhausted object " + field.show + ". " + Trace.show, Trace.position) - - else - report.warning("Access uninitialized field " + field.show + ". " + Trace.show, Trace.position) - + errorReadUninitializedField(ref.asObjectRef, field) Bottom else @@ -1332,7 +1326,7 @@ class Objects(using Context @constructorOnly): ref.valValue(target) else if ref.isObjectRef && ref.klass.hasSource then - report.warning("Access uninitialized field " + field.show + ". " + Trace.show, Trace.position) + errorReadUninitializedField(ref.asObjectRef, field) Bottom else @@ -2324,3 +2318,10 @@ class Objects(using Context @constructorOnly): printTraceWhenMultiple(scope_trace) report.warning(msg, Trace.position) + + def errorReadUninitializedField(obj: ObjectRef, field: Symbol)(using State.Data, Trace, Context): Unit = + if State.isQuotaExhausted(obj) then + if !BestEffort then + report.warning("Access uninitialized field of quota exhausted object " + field.show + ". " + Trace.show, Trace.position) + else + report.warning("Access uninitialized field " + field.show + ". " + Trace.show, Trace.position) From 7c9a2f2cc942fced1aab6f19f332292ffb5cb727 Mon Sep 17 00:00:00 2001 From: Fengyun Liu Date: Tue, 16 Dec 2025 07:52:26 +0100 Subject: [PATCH 5/5] Add missing data.popChecking() --- compiler/src/dotty/tools/dotc/transform/init/Objects.scala | 1 + 1 file changed, 1 insertion(+) diff --git a/compiler/src/dotty/tools/dotc/transform/init/Objects.scala b/compiler/src/dotty/tools/dotc/transform/init/Objects.scala index c369e855af63..57131fc74316 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Objects.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Objects.scala @@ -431,6 +431,7 @@ class Objects(using Context @constructorOnly): report.warning("Giving up checking initializatino of " + classSym + " due to exhausted budget", classSym.sourcePos) data.addQuotaExhausted(obj) data.addChecked(obj) + data.popChecking() return obj assert(data.checkingObjects.last.klass == classSym, "Expect = " + classSym.show + ", found = " + data.checkingObjects.last.klass)