Enforce quota in analysis

Author: liufengyun

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