refactor: analysis framework

es-meta · Feb 9, 2025 · 10b078d · 10b078d
1 parent 895606b
commit 10b078d
Show file tree

Hide file tree

Showing 31 changed files with 314 additions and 279 deletions.
diff --git a/src/main/scala/esmeta/analyzer/Analyzer.scala b/src/main/scala/esmeta/analyzer/Analyzer.scala
@@ -39,15 +39,6 @@ abstract class Analyzer
   /** check reachability of return points */
   def reachable(rp: ReturnPoint): Boolean
 
-  /** abstract states */
-  type AbsState <: AbsStateLike
-
-  /** abstract return values */
-  type AbsRet <: AbsRetLike
-
-  /** abstract values */
-  type AbsValue <: AbsValueLike
-
   /** lookup for node points */
   def getResult(np: NodePoint[Node]): AbsState =
     npMap.getOrElse(np, AbsState.Bot)
@@ -63,6 +54,7 @@ abstract class Analyzer
     detail: Boolean = false,
   ): String
 
+  /** logging mode */
   val log: Boolean
 
   /** logging the current analysis result */

diff --git a/src/main/scala/esmeta/analyzer/Domain.scala b/src/main/scala/esmeta/analyzer/Domain.scala
@@ -5,11 +5,8 @@ import esmeta.util.BaseUtils.*
 
 trait DomainDecl { self: Analyzer =>
 
-  /** abstract domain */
-  trait DomainLike[Elem] {
-
-    /** top element */
-    def Top: Elem
+  /** analysis domains */
+  trait AnalysisDomain[Elem <: AnalysisElem[Elem]] {
 
     /** bottom element */
     def Bot: Elem
@@ -18,45 +15,58 @@ trait DomainDecl { self: Analyzer =>
     given rule: Rule[Elem]
   }
 
-  trait DomainElemLike[Elem] { self: Elem =>
+  /** analysis elements */
+  trait AnalysisElem[Elem <: AnalysisElem[Elem]] { self: Elem =>
 
     /** abstract domain */
-    def domain: DomainLike[Elem]
+    def domain: AnalysisDomain[Elem]
 
     /** conversion to string */
     override def toString: String = stringify(this)(using domain.rule)
   }
 
+  /** value domains */
+  trait ValueDomain extends AnalysisDomain[AbsValue]
+  val AbsValue: ValueDomain
+
   /** abstract values */
-  trait AbsValueLike extends DomainElemLike[AbsValue] { self: AbsValue =>
+  trait AbsValueElem extends AnalysisElem[AbsValue] { self: AbsValue =>
 
     /** abstract domain */
     def domain = AbsValue
 
     /** get string of abstract value with an abstract state */
     def getString(state: AbsState): String
   }
-  val AbsValue: DomainLike[AbsValue]
+  type AbsValue <: AbsValueElem
+
+  /** state domains */
+  trait StateDomain extends AnalysisDomain[AbsState]
+  val AbsState: StateDomain
 
   /** abstract states */
-  trait AbsStateLike extends DomainElemLike[AbsState] { self: AbsState =>
+  trait AbsStateElem extends AnalysisElem[AbsState] { self: AbsState =>
 
     /** abstract domain */
     def domain = AbsState
 
     /** has imprecise elements */
     def hasImprec: Boolean
   }
-  val AbsState: DomainLike[AbsState]
+  type AbsState <: AbsStateElem
+
+  /** return value domains */
+  trait RetDomain extends AnalysisDomain[AbsRet]
+  val AbsRet: RetDomain
 
   /** abstract return values */
-  trait AbsRetLike extends DomainElemLike[AbsRet] { self: AbsRet =>
+  trait AbsRetElem extends AnalysisElem[AbsRet] { self: AbsRet =>
 
     /** abstract domain */
     def domain = AbsRet
 
     /** return value */
     def value: AbsValue
   }
-  val AbsRet: DomainLike[AbsRet]
+  type AbsRet <: AbsRetElem
 }
diff --git a/src/main/scala/esmeta/analyzer/es/AbsAddr.scala b/src/main/scala/esmeta/analyzer/es/AbsAddr.scala
@@ -9,7 +9,7 @@ import esmeta.util.domain.{*, given}, BSet.*, Flat.*
 /** abstract primitive values */
 trait AbsAddrDecl { self: ESAnalyzer =>
 
-  case class AbsAddr(set: BSet[Addr]) extends DomainElemLike[AbsAddr] {
+  case class AbsAddr(set: BSet[Addr]) extends AnalysisElem[AbsAddr] {
 
     /** abstract domain */
     def domain = AbsAddr
@@ -29,7 +29,7 @@ trait AbsAddrDecl { self: ESAnalyzer =>
     /** meet operator */
     def ⊓(that: AbsAddr): AbsAddr = ???
   }
-  object AbsAddr extends DomainLike[AbsAddr] {
+  object AbsAddr extends AnalysisDomain[AbsAddr] {
 
     /** top element */
     lazy val Top: AbsAddr = ???

diff --git a/src/main/scala/esmeta/analyzer/es/AbsClo.scala b/src/main/scala/esmeta/analyzer/es/AbsClo.scala
@@ -9,7 +9,7 @@ import esmeta.util.Appender.*
 trait AbsCloDecl { self: ESAnalyzer =>
 
   // TODO more precise abstraction
-  case class AbsClo(exist: Boolean) extends DomainElemLike[AbsClo] {
+  case class AbsClo(exist: Boolean) extends AnalysisElem[AbsClo] {
 
     /** abstract domain */
     def domain = AbsClo
@@ -32,7 +32,7 @@ trait AbsCloDecl { self: ESAnalyzer =>
     /** meet operator */
     def ⊓(that: AbsClo): AbsClo = AbsClo(exist && that.exist)
   }
-  object AbsClo extends DomainLike[AbsClo] {
+  object AbsClo extends AnalysisDomain[AbsClo] {
 
     /** top element */
     lazy val Top: AbsClo = AbsClo(true)

diff --git a/src/main/scala/esmeta/analyzer/es/AbsCont.scala b/src/main/scala/esmeta/analyzer/es/AbsCont.scala
@@ -9,7 +9,7 @@ import esmeta.util.Appender.*
 trait AbsContDecl { self: ESAnalyzer =>
 
   // TODO more precise abstraction
-  case class AbsCont(exist: Boolean) extends DomainElemLike[AbsCont] {
+  case class AbsCont(exist: Boolean) extends AnalysisElem[AbsCont] {
 
     /** abstract domain */
     def domain = AbsCont
@@ -32,7 +32,7 @@ trait AbsContDecl { self: ESAnalyzer =>
     /** meet operator */
     def ⊓(that: AbsCont): AbsCont = AbsCont(exist && that.exist)
   }
-  object AbsCont extends DomainLike[AbsCont] {
+  object AbsCont extends AnalysisDomain[AbsCont] {
 
     /** top element */
     lazy val Top: AbsCont = AbsCont(true)

diff --git a/src/main/scala/esmeta/analyzer/es/AbsPrimValue.scala b/src/main/scala/esmeta/analyzer/es/AbsPrimValue.scala
@@ -12,7 +12,7 @@ trait AbsPrimValueDecl { self: ESAnalyzer =>
   // TODO more precise abstraction
   case class AbsPrimValue(
     set: BSet[PrimValue],
-  ) extends DomainElemLike[AbsPrimValue] {
+  ) extends AnalysisElem[AbsPrimValue] {
 
     /** abstract domain */
     def domain = AbsPrimValue
@@ -32,7 +32,7 @@ trait AbsPrimValueDecl { self: ESAnalyzer =>
     /** meet operator */
     def ⊓(that: AbsPrimValue): AbsPrimValue = ???
   }
-  object AbsPrimValue extends DomainLike[AbsPrimValue] {
+  object AbsPrimValue extends AnalysisDomain[AbsPrimValue] {
 
     /** top element */
     lazy val Top: AbsPrimValue = ???

diff --git a/src/main/scala/esmeta/analyzer/es/AbsRet.scala b/src/main/scala/esmeta/analyzer/es/AbsRet.scala
@@ -5,7 +5,7 @@ import esmeta.util.Appender.*
 /** abstract return values */
 trait AbsRetDecl { self: ESAnalyzer =>
 
-  case class AbsRet() extends AbsRetLike {
+  case class AbsRet() extends AbsRetElem {
     import AbsRet.*
 
     /** return value */
@@ -26,7 +26,7 @@ trait AbsRetDecl { self: ESAnalyzer =>
     /** meet operator */
     def ⊓(that: AbsRet): AbsRet = ???
   }
-  object AbsRet extends DomainLike[AbsRet] {
+  object AbsRet extends RetDomain {
 
     /** top element */
     lazy val Top: AbsRet = ???

diff --git a/src/main/scala/esmeta/analyzer/es/AbsState.scala b/src/main/scala/esmeta/analyzer/es/AbsState.scala
@@ -10,7 +10,7 @@ import esmeta.util.BaseUtils.*
 
 /** abstract states */
 trait AbsStateDecl { self: ESAnalyzer =>
-  case class AbsState() extends AbsStateLike {
+  case class AbsState() extends AbsStateElem {
     import AbsState.*
 
     given AbsState = this
@@ -82,7 +82,7 @@ trait AbsStateDecl { self: ESAnalyzer =>
     /** allocate a list object */
     def allocList(vs: Iterable[AbsValue]): (AbsValue, AbsState) = ???
   }
-  object AbsState extends DomainLike[AbsState] {
+  object AbsState extends StateDomain {
 
     /** bases */
     private val globals: Map[Global, AbsValue] =

diff --git a/src/main/scala/esmeta/analyzer/es/AbsValue.scala b/src/main/scala/esmeta/analyzer/es/AbsValue.scala
@@ -19,7 +19,7 @@ trait AbsValueDecl { self: ESAnalyzer =>
     clo: AbsClo = AbsClo.Bot,
     cont: AbsCont = AbsCont.Bot,
     prim: AbsPrimValue = AbsPrimValue.Bot,
-  ) extends AbsValueLike {
+  ) extends AbsValueElem {
     import AbsValue.*
 
     /** bottom check */
@@ -113,7 +113,7 @@ trait AbsValueDecl { self: ESAnalyzer =>
     def getString(state: AbsState): String = ???
 
   }
-  object AbsValue extends DomainLike[AbsValue] {
+  object AbsValue extends ValueDomain {
 
     /** top element */
     lazy val Top: AbsValue = ???

diff --git a/src/main/scala/esmeta/analyzer/tychecker/AbsRet.scala b/src/main/scala/esmeta/analyzer/tychecker/AbsRet.scala
@@ -5,7 +5,7 @@ import esmeta.util.Appender.*
 /** abstract return values */
 trait AbsRetDecl { self: TyChecker =>
 
-  case class AbsRet(value: AbsValue) extends AbsRetLike {
+  case class AbsRet(value: AbsValue) extends AbsRetElem {
     import AbsRet.*
 
     /** bottom check */
@@ -25,7 +25,7 @@ trait AbsRetDecl { self: TyChecker =>
     def ⊓(that: AbsRet)(using AbsState): AbsRet =
       AbsRet(this.value ⊓ that.value)
   }
-  object AbsRet extends DomainLike[AbsRet] {
+  object AbsRet extends RetDomain {
 
     /** top element */
     lazy val Top: AbsRet = AbsRet(AbsValue.Top)

diff --git a/src/main/scala/esmeta/analyzer/tychecker/AbsState.scala b/src/main/scala/esmeta/analyzer/tychecker/AbsState.scala
@@ -18,7 +18,7 @@ trait AbsStateDecl { self: TyChecker =>
     locals: Map[Local, AbsValue],
     symEnv: Map[Sym, ValueTy],
     pred: SymPred,
-  ) extends AbsStateLike {
+  ) extends AbsStateElem {
     import AbsState.*
 
     given AbsState = this
@@ -155,7 +155,7 @@ trait AbsStateDecl { self: TyChecker =>
     def get(base: AbsValue, field: AbsValue)(using AbsState): AbsValue = {
       import SymExpr.*, SymRef.*, SymTy.*
       val guard = lookupGuard(base.guard, field)
-      (base.symty, field.ty.getSingle) match
+      (base.symty, field.ty.toFlat) match
         case (SRef(ref), One(Str(f))) =>
           AbsValue(SRef(SField(ref, STy(StrT(f)))), guard)
         case _ =>
@@ -184,7 +184,7 @@ trait AbsStateDecl { self: TyChecker =>
     private def lookupAstIdxField(
       name: String,
       idx: Int,
-    )(field: ValueTy): ValueTy = field.math.getSingle match
+    )(field: ValueTy): ValueTy = field.math.toFlat match
       case Zero => BotT
       case One(k) =>
         (for {
@@ -197,7 +197,7 @@ trait AbsStateDecl { self: TyChecker =>
     // lookup string fields of ASTs
     private def lookupAstStrField(field: ValueTy): ValueTy =
       val nameMap = cfg.grammar.nameMap
-      field.str.getSingle match
+      field.str.toFlat match
         case Zero                               => BotT
         case One(name) if nameMap contains name => AstT(name)
         case _ => AstT // TODO warning(s"invalid access: $name of $ast")
@@ -243,7 +243,7 @@ trait AbsStateDecl { self: TyChecker =>
       field: AbsValue,
     )(using AbsState): TypeGuard = {
       import RefinementKind.*
-      field.ty.str.getSingle match
+      field.ty.str.toFlat match
         case One("Value") =>
           TypeGuard(guard.map.collect {
             case (RefinementKind(ty), map) if ty == NormalT(TrueT) =>
@@ -327,7 +327,7 @@ trait AbsStateDecl { self: TyChecker =>
     ): (AbsValue, AbsState) =
       (AbsValue(ListT(vs.foldLeft(BotT)(_ || _.ty))), this)
   }
-  object AbsState extends DomainLike[AbsState] {
+  object AbsState extends StateDomain {
 
     /** top element */
     lazy val Top: AbsState = exploded("top abstract state")

diff --git a/src/main/scala/esmeta/analyzer/tychecker/AbsTransfer.scala b/src/main/scala/esmeta/analyzer/tychecker/AbsTransfer.scala
@@ -752,7 +752,7 @@ trait AbsTransferDecl { analyzer: TyChecker =>
               var math = lty.math
               val infinity = lty.infinity --
                 (if (!(isLt ^ pos)) InfinityTy.Pos else InfinityTy.Neg)
-              if (lty.math <= MathTy.Int) rty.getSingle match
+              if (lty.math <= MathTy.Int) rty.toFlat match
                 case One(Math(0)) =>
                   math = (isLt, pos) match
                     case (true, true)   => /* x < 0 */ MathTy.NegInt
@@ -960,7 +960,7 @@ trait AbsTransferDecl { analyzer: TyChecker =>
           } yield {
             val lty = lv.ty
             val rty = rv.ty
-            def aux(positive: Boolean): ValueTy = rty.str.getSingle match
+            def aux(positive: Boolean): ValueTy = rty.str.toFlat match
               case One(tname) =>
                 val vty = ValueTy.fromTypeOf(tname)
                 if (positive) lty && vty else lty -- vty
@@ -1543,7 +1543,7 @@ trait AbsTransferDecl { analyzer: TyChecker =>
           if (ty <= givenTy) None else Some(x -> givenTy)
         case SField(base, STy(x)) if x <= StrT && x.isSingle =>
           val bty = st.getTy(base)
-          val field = x.str.getSingle match
+          val field = x.str.toFlat match
             case One(elem) => elem
             case _         => return None
           val refinedTy = ValueTy(
@@ -1621,7 +1621,7 @@ trait AbsTransferDecl { analyzer: TyChecker =>
       given AbsState <- get
       lty = lv.ty
       rty = rv.ty
-      refinedV = rty.str.getSingle match
+      refinedV = rty.str.toFlat match
         case One(tname) =>
           val value = AbsValue(ValueTy.fromTypeOf(tname))
           if (positive) lv ⊓ value else lv -- value
@@ -1724,7 +1724,7 @@ trait AbsTransferDecl { analyzer: TyChecker =>
         },
         "RequireInternalSlot" -> { (func, vs, retTy, st) =>
           given AbsState = st
-          val refined = vs(1).ty.str.getSingle match
+          val refined = vs(1).ty.str.toFlat match
             case One(f) =>
               ValueTy(
                 record = ObjectT.record.update(f, Binding.Exist, refine = true),

diff --git a/src/main/scala/esmeta/analyzer/tychecker/AbsValue.scala b/src/main/scala/esmeta/analyzer/tychecker/AbsValue.scala
@@ -19,7 +19,7 @@ trait AbsValueDecl { self: TyChecker =>
   case class AbsValue(
     symty: SymTy,
     guard: TypeGuard = TypeGuard.Empty,
-  ) extends AbsValueLike {
+  ) extends AbsValueElem {
     import AbsValue.*
 
     /** bottom check */
@@ -406,7 +406,7 @@ trait AbsValueDecl { self: TyChecker =>
       s"$this (${ty})"
 
   }
-  object AbsValue extends DomainLike[AbsValue] {
+  object AbsValue extends ValueDomain {
 
     def apply(ty: ValueTy): AbsValue = AbsValue(STy(ty), TypeGuard.Empty)