From b6bf313fb03061e7a02405556f2e8c139f24a20e Mon Sep 17 00:00:00 2001 From: Jihyeok Park Date: Fri, 4 Oct 2024 11:21:02 +0900 Subject: [PATCH] Use SymBase type for keys of SymPred.map --- .../esmeta/analyzer/tychecker/AbsState.scala | 22 +-- .../analyzer/tychecker/AbsTransfer.scala | 174 +++++++++--------- .../esmeta/analyzer/tychecker/TyChecker.scala | 2 +- src/main/scala/esmeta/ty/package.scala | 43 +++-- 4 files changed, 123 insertions(+), 118 deletions(-) diff --git a/src/main/scala/esmeta/analyzer/tychecker/AbsState.scala b/src/main/scala/esmeta/analyzer/tychecker/AbsState.scala index bdffe1b9b7..93d63a35e2 100644 --- a/src/main/scala/esmeta/analyzer/tychecker/AbsState.scala +++ b/src/main/scala/esmeta/analyzer/tychecker/AbsState.scala @@ -1,5 +1,5 @@ package esmeta.analyzer.tychecker -import esmeta.ir.{*, given} +import esmeta.ir.* import esmeta.ty.{*, given} import esmeta.ty.util.Stringifier.{*, given} import esmeta.state.* @@ -90,9 +90,6 @@ trait AbsStateDecl { self: TyChecker => case x: Global => base.getOrElse(x, AbsValue.Bot) case x: Local => locals.getOrElse(x, AbsValue.Bot) - /** getter for symbols */ - def getTy(sym: Sym): ValueTy = symEnv.getOrElse(sym, BotT) - /** getter for symbolic expressions */ def getTy(expr: SymExpr): ValueTy = { import SymExpr.* @@ -109,11 +106,15 @@ trait AbsStateDecl { self: TyChecker => def getTy(ref: SymRef): ValueTy = { import SymRef.* ref match - case SSym(sym) => getTy(sym) - case SLocal(x) => get(x).ty + case SBase(x) => getTy(x) case SField(base, field) => get(getTy(base), getTy(field)) } + /** getter for symbolic bases */ + def getTy(x: SymBase): ValueTy = x match + case x: Sym => symEnv.getOrElse(x, BotT) + case x: Local => get(x).ty + /** getter */ def get(base: AbsValue, field: AbsValue)(using AbsState): AbsValue = { import SymExpr.*, SymRef.* @@ -319,13 +320,10 @@ trait AbsStateDecl { self: TyChecker => private def mkRule(detail: Boolean): Rule[AbsState] = (app, elem) => if (!elem.isBottom) { val AbsState(reachable, locals, symEnv, pred) = elem - val irStringifier = IRElem.getStringifier(detail, false) - import irStringifier.given given localsRule: Rule[Map[Local, AbsValue]] = sortedMapRule(sep = ": ") - given symEnvRule: Rule[Map[Sym, ValueTy]] = sortedMapRule(sep = ": ")( - using kRule = (app, sym) => app >> "#" >> sym, - ) - given predRule: Rule[Map[SymRef, ValueTy]] = sortedMapRule(sep = " <: ") + given symEnvRule: Rule[Map[Sym, ValueTy]] = sortedMapRule(sep = ": ") + given predRule: Rule[Map[SymBase, ValueTy]] = + sortedMapRule(sep = " <: ") app >> locals if (symEnv.nonEmpty) app >> symEnv app >> pred diff --git a/src/main/scala/esmeta/analyzer/tychecker/AbsTransfer.scala b/src/main/scala/esmeta/analyzer/tychecker/AbsTransfer.scala index 21e86839d7..262dddd2b9 100644 --- a/src/main/scala/esmeta/analyzer/tychecker/AbsTransfer.scala +++ b/src/main/scala/esmeta/analyzer/tychecker/AbsTransfer.scala @@ -68,7 +68,8 @@ trait AbsTransferDecl { analyzer: TyChecker => val newSt = (for { ref <- toSymRef(expr, v) if useTypeGuard - } yield refine(SymPred(Map(ref -> TrueT)), positive)(st)) + pair <- getRefiner(ref -> TrueT)(using st) + } yield refine(SymPred(Map(pair)), positive)(st)) .getOrElse(st) v.guard.get(kind) match case Some(pred) => refine(pred, true)(newSt) @@ -235,7 +236,7 @@ trait AbsTransferDecl { analyzer: TyChecker => /** conversion to symbolic references */ def toSymRef(ref: Ref): Option[SymRef] = ref match - case s: Local => Some(SLocal(s)) + case x: Local => Some(SBase(x)) case Field(base, EStr(field)) => for { b <- toSymRef(base) @@ -595,13 +596,22 @@ trait AbsTransferDecl { analyzer: TyChecker => val thenTy = aux(binding) val elseTy = aux(lty.record(field) -- binding) var guard: TypeGuard = Map() + var bools = Set(true, false) toSymRef(x, lv).map { ref => if (lty != thenTy) - guard += True -> withPred(SymPred(Map(ref -> thenTy))) + if (thenTy.isBottom) bools -= true + else + getRefiner(ref -> thenTy).map { pair => + guard += True -> withPred(SymPred(Map(pair))) + } if (lty != elseTy) - guard += False -> withPred(SymPred(Map(ref -> elseTy))) + if (elseTy.isBottom) bools -= false + else + getRefiner(ref -> elseTy).map { pair => + guard += False -> withPred(SymPred(Map(pair))) + } } - AbsValue(BoolT, Many, guard) + AbsValue(BoolT(bools), Many, guard) } if (!useTypeGuard) None else @@ -765,13 +775,22 @@ trait AbsTransferDecl { analyzer: TyChecker => val thenTy = aux(true) val elseTy = aux(false) var guard: TypeGuard = Map() + var bools = Set(true, false) toSymRef(ref, lv).map { ref => if (lty != thenTy) - guard += True -> withPred(SymPred(Map(ref -> thenTy))) + if (thenTy.isBottom) bools -= true + else + getRefiner(ref -> thenTy).map { pair => + guard += True -> withPred(SymPred(Map(pair))) + } if (lty != elseTy) - guard += False -> withPred(SymPred(Map(ref -> elseTy))) + if (elseTy.isBottom) bools -= false + else + getRefiner(ref -> elseTy).map { pair => + guard += False -> withPred(SymPred(Map(pair))) + } } - AbsValue(BoolT, Many, guard) + AbsValue(BoolT(bools), Many, guard) }) case EUnary(UOp.Not, e) => Some(for { @@ -1021,14 +1040,19 @@ trait AbsTransferDecl { analyzer: TyChecker => /** instantiation of symbolic references */ def instantiate(sref: SymRef, map: Map[Sym, SymRef]): Option[SymRef] = sref match - case SSym(sym) => map.get(sym) - case SLocal(x) => None + case SBase(x) => instantiate(x, map) case SField(base, field) => for { b <- instantiate(base, map) f <- instantiate(field, map) } yield SField(b, f) + /** instantiation of symbolic bases */ + def instantiate(x: SymBase, map: Map[Sym, SymRef]): Option[SymRef] = + x match + case x: Sym => map.get(x) + case x => None + // ------------------------------------------------------------------------- // Type Refinement // ------------------------------------------------------------------------- @@ -1101,7 +1125,7 @@ trait AbsTransferDecl { analyzer: TyChecker => )(using np: NodePoint[_]): Updater = val SymPred(map, expr) = pred for { - _ <- join(map.map { case (ref, ty) => refine(ref, ty, positive) }) + _ <- join(map.map { case (x, ty) => refine(x, ty, positive) }) _ <- expr.fold(pure(()))(e => modify(refine(e, positive))) _ <- modify(st => st.copy(pred = st.pred && pred)) } yield () @@ -1113,27 +1137,27 @@ trait AbsTransferDecl { analyzer: TyChecker => )(using np: NodePoint[_]): Updater = for { _ <- modify(expr match { - // refine boolean local variables - case SERef(x: Local) => - refineBool(x, positive) - // refine type checks - case SETypeCheck(SERef(ref), ty) => - refine(ref, ty, positive) - // refine logical negation - case SEUnary(UOp.Not, e) => - refine(e, !positive) - // refine logical disjunction - case SEBinary(BOp.Or, l, r) => - st => - if (positive) refine(l, true)(st) ⊔ refine(r, true)(st) - // TODO short circuiting - else refine(r, false)(refine(l, false)(st)) - // refine logical conjunction - case SEBinary(BOp.And, l, r) => - st => - if (positive) refine(r, true)(refine(l, true)(st)) - // TODO short circuiting - else refine(l, false)(st) ⊔ refine(r, false)(st) + // // refine boolean local variables + // case SERef(x: Local) => + // refineBool(x, positive) + // // refine type checks + // case SETypeCheck(SERef(ref), ty) => + // refine(ref, ty, positive) + // // refine logical negation + // case SEUnary(UOp.Not, e) => + // refine(e, !positive) + // // refine logical disjunction + // case SEBinary(BOp.Or, l, r) => + // st => + // if (positive) refine(l, true)(st) ⊔ refine(r, true)(st) + // // TODO short circuiting + // else refine(r, false)(refine(l, false)(st)) + // // refine logical conjunction + // case SEBinary(BOp.And, l, r) => + // st => + // if (positive) refine(r, true)(refine(l, true)(st)) + // // TODO short circuiting + // else refine(l, false)(st) ⊔ refine(r, false)(st) // no pruning case _ => st => st }) @@ -1141,15 +1165,15 @@ trait AbsTransferDecl { analyzer: TyChecker => /** refine references using types */ def refine( - ref: SymRef, + ref: SymBase, ty: ValueTy, positive: Boolean, )(using np: NodePoint[_]): Updater = ref match - case SSym(sym) => + case sym: Sym => st => val refinedTy = st.symEnv.get(sym).fold(ty)(_ && ty) st.copy(symEnv = st.symEnv + (sym -> refinedTy)) - case SLocal(x) => + case x: Local => for { v <- transfer(x) given AbsState <- get @@ -1161,30 +1185,15 @@ trait AbsTransferDecl { analyzer: TyChecker => _ <- modify(_.update(x, refinedV, refine = true)) _ <- refine(v, refinedV) // propagate type guard } yield () - case SField(base, SEStr(field)) => - println(s"[${np.node.id}] refine field: $base.$field") - for { - bty <- get(_.getTy(base)) - rbinding = Binding(ty) - binding = if (positive) rbinding else bty.record(field) -- rbinding - refinedTy = ValueTy( - ast = bty.ast, - record = bty.record.update(field, binding, refine = true), - ) - _ <- refine(base, refinedTy, positive) - } yield () - case _ => st => st def getRefiner( pair: (SymRef, ValueTy), - )(using st: AbsState): Option[(SymRef, ValueTy)] = { + )(using st: AbsState): Option[(SymBase, ValueTy)] = { val (ref, givenTy) = pair - val ty = st.getTy(ref) - val res = ref match - case SSym(sym) => - if (ty <= givenTy) None else Some(ref -> (ty && givenTy)) - case SLocal(x) => - if (ty <= givenTy) None else Some(ref -> (ty && givenTy)) + ref match + case SBase(x) => + val ty = st.getTy(x) + if (ty <= givenTy) None else Some(x -> (ty && givenTy)) case SField(base, SEStr(field)) => val bty = st.getTy(base) val refinedTy = ValueTy( @@ -1193,7 +1202,6 @@ trait AbsTransferDecl { analyzer: TyChecker => ) getRefiner(base -> refinedTy) case _ => None - res } /** refine types for boolean local variables */ @@ -1461,14 +1469,14 @@ trait AbsTransferDecl { analyzer: TyChecker => "IsCallable" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - True -> SymPred(Map(SSym(0) -> FunctionT)), + True -> SymPred(Map(0 -> FunctionT)), ) AbsValue(retTy, Zero, guard) }, "IsConstructor" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - True -> SymPred(Map(SSym(0) -> ConstructorT)), + True -> SymPred(Map(0 -> ConstructorT)), ) AbsValue(retTy, Zero, guard) }, @@ -1481,28 +1489,28 @@ trait AbsTransferDecl { analyzer: TyChecker => ) case _ => ObjectT val guard: TypeGuard = Map( - Normal -> SymPred(Map(SSym(0) -> refined)), + Normal -> SymPred(Map(0 -> refined)), ) AbsValue(retTy, Zero, guard) }, "ValidateTypedArray" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - Normal -> SymPred(Map(SSym(0) -> TypedArrayT)), + Normal -> SymPred(Map(0 -> TypedArrayT)), ) AbsValue(retTy, Zero, guard) }, "ValidateIntegerTypedArray" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - Normal -> SymPred(Map(SSym(0) -> TypedArrayT)), + Normal -> SymPred(Map(0 -> TypedArrayT)), ) AbsValue(retTy, Zero, guard) }, "ValidateAtomicAccessOnIntegerTypedArray" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - Normal -> SymPred(Map(SSym(0) -> TypedArrayT)), + Normal -> SymPred(Map(0 -> TypedArrayT)), ) AbsValue(retTy, Zero, guard) }, @@ -1511,7 +1519,7 @@ trait AbsTransferDecl { analyzer: TyChecker => val guard: TypeGuard = Map( Normal -> SymPred( Map( - SSym(0) -> ValueTy.from( + 0 -> ValueTy.from( "Record[ProxyExoticObject { ProxyHandler : Record[Object], ProxyTarget : Record[Object] }]", ), ), @@ -1522,22 +1530,22 @@ trait AbsTransferDecl { analyzer: TyChecker => "IsPromise" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - True -> SymPred(Map(SSym(0) -> RecordT("Promise"))), + True -> SymPred(Map(0 -> RecordT("Promise"))), ) AbsValue(retTy, Zero, guard) }, "IsRegExp" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - NormalTrue -> SymPred(Map(SSym(0) -> ObjectT)), - Abrupt -> SymPred(Map(SSym(0) -> ObjectT)), + NormalTrue -> SymPred(Map(0 -> ObjectT)), + Abrupt -> SymPred(Map(0 -> ObjectT)), ) AbsValue(retTy, Zero, guard) }, "NewPromiseCapability" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - Normal -> SymPred(Map(SSym(0) -> ConstructorT)), + Normal -> SymPred(Map(0 -> ConstructorT)), ) AbsValue(retTy, Zero, guard) }, @@ -1562,7 +1570,7 @@ trait AbsTransferDecl { analyzer: TyChecker => var guard: TypeGuard = Map( True -> SymPred( Map( - SSym(0) -> + 0 -> RecordT( "ReferenceRecord", Map("Base" -> EnumT("unresolvable")), @@ -1571,7 +1579,7 @@ trait AbsTransferDecl { analyzer: TyChecker => ), False -> SymPred( Map( - SSym(0) -> + 0 -> RecordT( "ReferenceRecord", Map("Base" -> (ESValueT || RecordT("EnvironmentRecord"))), @@ -1587,12 +1595,12 @@ trait AbsTransferDecl { analyzer: TyChecker => True -> SymPred( Map( - SSym(0) -> RecordT("ReferenceRecord", Map("Base" -> ESValueT)), + 0 -> RecordT("ReferenceRecord", Map("Base" -> ESValueT)), ), ), False -> SymPred( Map( - SSym(0) -> + 0 -> RecordT( "ReferenceRecord", Map( @@ -1608,7 +1616,7 @@ trait AbsTransferDecl { analyzer: TyChecker => "IsSuperReference" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - True -> SymPred(Map(SSym(0) -> RecordT("SuperReferenceRecord"))), + True -> SymPred(Map(0 -> RecordT("SuperReferenceRecord"))), ) AbsValue(retTy, Zero, guard) }, @@ -1617,7 +1625,7 @@ trait AbsTransferDecl { analyzer: TyChecker => val guard: TypeGuard = Map( True -> SymPred( Map( - SSym(0) -> + 0 -> RecordT( "ReferenceRecord", Map("ReferencedName" -> RecordT("PrivateName")), @@ -1626,7 +1634,7 @@ trait AbsTransferDecl { analyzer: TyChecker => ), False -> SymPred( Map( - SSym(0) -> + 0 -> RecordT( "ReferenceRecord", Map( @@ -1641,8 +1649,8 @@ trait AbsTransferDecl { analyzer: TyChecker => "IsArray" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - NormalTrue -> SymPred(Map(SSym(0) -> ObjectT)), - Abrupt -> SymPred(Map(SSym(0) -> ObjectT)), + NormalTrue -> SymPred(Map(0 -> ObjectT)), + Abrupt -> SymPred(Map(0 -> ObjectT)), ) AbsValue(retTy, Zero, guard) }, @@ -1651,7 +1659,7 @@ trait AbsTransferDecl { analyzer: TyChecker => val guard: TypeGuard = Map( True -> SymPred( Map( - SSym(0) -> + 0 -> RecordT( "SharedArrayBuffer", Map("ArrayBufferData" -> RecordT("SharedDataBlock")), @@ -1664,8 +1672,8 @@ trait AbsTransferDecl { analyzer: TyChecker => "IsConcatSpreadable" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - NormalTrue -> SymPred(Map(SSym(0) -> ObjectT)), - Abrupt -> SymPred(Map(SSym(0) -> ObjectT)), + NormalTrue -> SymPred(Map(0 -> ObjectT)), + Abrupt -> SymPred(Map(0 -> ObjectT)), ) AbsValue(retTy, Zero, guard) }, @@ -1678,10 +1686,10 @@ trait AbsTransferDecl { analyzer: TyChecker => ), ) val guard: TypeGuard = Map( - True -> SymPred(Map(SSym(0) -> getTy(NullT, NullT))), + True -> SymPred(Map(0 -> getTy(NullT, NullT))), False -> SymPred( Map( - SSym(0) -> getTy( + 0 -> getTy( RecordT("DataBlock"), RecordT("SharedDataBlock"), ), @@ -1721,14 +1729,14 @@ trait AbsTransferDecl { analyzer: TyChecker => "CanBeHeldWeakly" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - True -> SymPred(Map(SSym(0) -> (ObjectT || SymbolT))), + True -> SymPred(Map(0 -> (ObjectT || SymbolT))), ) AbsValue(retTy, Zero, guard) }, "AsyncGeneratorValidate" -> { (vs, retTy, st) => given AbsState = st val guard: TypeGuard = Map( - Normal -> SymPred(Map(SSym(0) -> RecordT("AsyncGenerator"))), + Normal -> SymPred(Map(0 -> RecordT("AsyncGenerator"))), ) AbsValue(retTy, Zero, guard) }, diff --git a/src/main/scala/esmeta/analyzer/tychecker/TyChecker.scala b/src/main/scala/esmeta/analyzer/tychecker/TyChecker.scala index 9089a65c3d..7228b7c8a3 100644 --- a/src/main/scala/esmeta/analyzer/tychecker/TyChecker.scala +++ b/src/main/scala/esmeta/analyzer/tychecker/TyChecker.scala @@ -219,7 +219,7 @@ class TyChecker( val (newLocals, symEnv) = (for { ((x, value), sym) <- idxLocals } yield ( - x -> AbsValue(BotT, One(SERef(SSym(sym))), Map()), + x -> AbsValue(BotT, One(SERef(SBase(sym))), Map()), sym -> value.ty, )).unzip callerSt.copy(locals = newLocals.toMap, symEnv = symEnv.toMap) diff --git a/src/main/scala/esmeta/ty/package.scala b/src/main/scala/esmeta/ty/package.scala index 965f393987..0845ca80f0 100644 --- a/src/main/scala/esmeta/ty/package.scala +++ b/src/main/scala/esmeta/ty/package.scala @@ -80,20 +80,16 @@ type SymBase = Sym | Local /** symbolic references */ enum SymRef: - case SSym(sym: Sym) - case SLocal(local: Local) + case SBase(base: SymBase) case SField(base: SymRef, field: SymExpr) def getBase: SymBase = this match - case SSym(s) => s - case SLocal(x) => x + case SBase(s) => s case SField(base, f) => base.getBase def has(sym: Sym): Boolean = this match - case SSym(s) => s == sym - case SLocal(x) => false + case SBase(s) => s == sym case SField(base, f) => base.has(sym) || f.has(sym) def kill(x: Local): Option[SymRef] = this match - case SSym(s) => Some(this) - case SLocal(y) => if (x == y) None else Some(this) + case SBase(y) => if (x == y) None else Some(this) case SField(base, f) => for { b <- base.kill(x) @@ -103,30 +99,30 @@ enum SymRef: /** symbolic predicates */ case class SymPred( - map: Map[SymRef, ValueTy] = Map(), + map: Map[SymBase, ValueTy] = Map(), expr: Option[SymExpr] = None, ) { def isTop: Boolean = map.isEmpty && expr.isEmpty def nonTop: Boolean = !isTop def ||(that: SymPred): SymPred = SymPred( (for { - ref <- (this.map.keySet intersect that.map.keySet).toList - ty = this.map(ref) || that.map(ref) - } yield ref -> ty).toMap, + x <- (this.map.keySet intersect that.map.keySet).toList + ty = this.map(x) || that.map(x) + } yield x -> ty).toMap, this.expr || that.expr, ) def &&(that: SymPred): SymPred = SymPred( (for { - ref <- (this.map.keySet ++ that.map.keySet).toList - ty = this.map.getOrElse(ref, AnyT) && that.map.getOrElse(ref, AnyT) - } yield ref -> ty).toMap, + x <- (this.map.keySet ++ that.map.keySet).toList + ty = this.map.getOrElse(x, AnyT) && that.map.getOrElse(x, AnyT) + } yield x -> ty).toMap, this.expr && that.expr, ) def kill(x: Local): SymPred = SymPred( for { - (ref, ty) <- map - newRef <- ref.kill(x) - } yield newRef -> ty, + (y, ty) <- map + if y != x + } yield y -> ty, expr.flatMap(_.kill(x)), ) override def toString: String = (new Appender >> this).toString @@ -299,7 +295,11 @@ extension (elem: Boolean) { import TyStringifier.given val irStringifier = IRElem.getStringifier(true, false) import irStringifier.given -given Ordering[SymRef] = Ordering.by(_.toString) +given Rule[SymBase] = (app, base) => + base match + case sym: Sym => app >> "#" >> sym.toString + case local: Local => app >> local.toString +given Ordering[SymBase] = Ordering.by(_.toString) given Rule[SymExpr] = (app, expr) => import SymExpr.* expr match @@ -317,12 +317,11 @@ given Rule[SymRef] = (app, ref) => lazy val inlineField = "([_a-zA-Z][_a-zA-Z0-9]*)".r import SymRef.* ref match - case SSym(sym) => app >> "#" >> sym - case SLocal(x) => app >> x + case SBase(x) => app >> x case SField(base, SEStr(inlineField(f))) => app >> base >> "." >> f case SField(base, field) => app >> base >> "[" >> field >> "]" given Rule[SymPred] = (app, pred) => import SymPred.* - given Rule[Map[SymRef, ValueTy]] = sortedMapRule(sep = " <: ") + given Rule[Map[SymBase, ValueTy]] = sortedMapRule(sep = " <: ") if (pred.map.nonEmpty) app >> pred.map pred.expr.fold(app)(app >> "[" >> _ >> "]")