From 0dfdf87f6b9146833d186c0768c54077453662b0 Mon Sep 17 00:00:00 2001 From: Jun Gyeom Kim Date: Thu, 21 Nov 2024 11:24:27 +0900 Subject: [PATCH] Add Provenance feature for Type guards (#265) Co-authored-by: Jihyeok Park --- .../analyzer/tychecker/AbsTransfer.scala | 53 ++++++++++++++++--- .../esmeta/analyzer/tychecker/TyChecker.scala | 34 ++++++++++++ .../esmeta/analyzer/tychecker/TypeGuard.scala | 31 ++++++++++- 3 files changed, 110 insertions(+), 8 deletions(-) diff --git a/src/main/scala/esmeta/analyzer/tychecker/AbsTransfer.scala b/src/main/scala/esmeta/analyzer/tychecker/AbsTransfer.scala index d9683abc4b..ba73b517b2 100644 --- a/src/main/scala/esmeta/analyzer/tychecker/AbsTransfer.scala +++ b/src/main/scala/esmeta/analyzer/tychecker/AbsTransfer.scala @@ -34,9 +34,9 @@ trait AbsTransferDecl { analyzer: TyChecker => val NodePoint(func, node, view) = np node match case Block(_, insts, next) => - val newSt = insts.foldLeft(st) { + val newSt = insts.zipWithIndex.foldLeft(st) { case (nextSt, _) if nextSt.isBottom => nextSt - case (nextSt, inst) => transfer(inst)(nextSt) + case (nextSt, (inst, idx)) => transfer(inst, idx)(nextSt) } next.foreach(to => analyzer += getNextNp(np, to) -> newSt) case call: Call => @@ -48,15 +48,36 @@ trait AbsTransferDecl { analyzer: TyChecker => } yield ())(st) call.next.foreach(to => analyzer += getNextNp(np, to) -> newSt) case br @ Branch(_, kind, c, thenNode, elseNode) => + import RefinementTarget.* + import RefinementKind.* (for { v <- transfer(c); newSt <- get } yield { if (v.ty.bool.contains(true)) - val refinedSt = refine(c, v, true)(newSt) - thenNode.map(analyzer += getNextNp(np, _) -> refinedSt) + val rst = refine(c, v, true)(newSt) + val pred = v.guard.get(True) + if (detail) logRefined(BranchTarget(br, true), pred, newSt, rst) + thenNode.map(analyzer += getNextNp(np, _) -> rst) if (v.ty.bool.contains(false)) - val refinedSt = refine(c, v, false)(newSt) - elseNode.map(analyzer += getNextNp(np, _) -> refinedSt) + val rst = refine(c, v, false)(newSt) + val pred = v.guard.get(False) + if (detail) logRefined(BranchTarget(br, false), pred, newSt, rst) + elseNode.map(analyzer += getNextNp(np, _) -> rst) })(st) + def logRefined( + target: RefinementTarget, + pred: Option[SymPred], + st: AbsState, + refinedSt: AbsState, + ): Unit = + val xs = for { + (x, v) <- st.locals + ty = v.ty(using st) + refinedTy = refinedSt.get(x).ty(using refinedSt) + if refinedTy != ty + } yield x + if (xs.isEmpty) refined -= target + else refined += target -> (xs.toSet, pred.fold(0)(_.depth)) + /** refine with an expression and its abstract value */ def refine( expr: Expr, @@ -332,6 +353,12 @@ trait AbsTransferDecl { analyzer: TyChecker => /** transfer function for normal instructions */ def transfer( inst: NormalInst, + )(using np: NodePoint[_]): Updater = transfer(inst, -1) + + /** transfer function for normal instructions */ + def transfer( + inst: NormalInst, + idx: Int, )(using np: NodePoint[_]): Updater = inst match { case IExpr(expr) => for { @@ -389,8 +416,20 @@ trait AbsTransferDecl { analyzer: TyChecker => case IAssert(expr) => for { v <- transfer(expr) + st <- get + pred = v.guard.get(RefinementKind.True) _ <- modify(refine(expr, v, true)) - given AbsState <- get + refinedSt <- get + given AbsState = refinedSt + _ = if (detail) np.node match + case block: Block => + logRefined( + RefinementTarget.AssertTarget(block, idx), + pred, + st, + refinedSt, + ) + case _ => _ <- if (v ⊑ False) put(AbsState.Bot) else pure(()) } yield () case IPrint(expr) => st => st /* skip */ diff --git a/src/main/scala/esmeta/analyzer/tychecker/TyChecker.scala b/src/main/scala/esmeta/analyzer/tychecker/TyChecker.scala index 84a7216317..d8fba2d51b 100644 --- a/src/main/scala/esmeta/analyzer/tychecker/TyChecker.scala +++ b/src/main/scala/esmeta/analyzer/tychecker/TyChecker.scala @@ -110,6 +110,12 @@ class TyChecker( "returns" -> ratioSimpleString(analyzedReturns.size, cfg.funcs.size), ), ) + if (detail) + info :+= "refined" -> Map( + "targets" -> refinedTargets, + "locals" -> refinedLocals, + "avg. depth" -> refinedAvgDepth, + ) if (inferTypeGuard) info :+= "guards" -> typeGuards.size Yaml(info: _*) }, @@ -149,6 +155,9 @@ class TyChecker( cfg.funcs.size, // total funcs this.analyzedNodes.size, // analyzed nodes cfg.nodes.size, // total nodes + if (detail) refinedTargets else 0, // refined targets + if (detail) refinedLocals else 0, // refined locals + if (detail) refinedAvgDepth else 0, // refined avg. depth if (inferTypeGuard) typeGuards.size else 0, // guards ).mkString("\t"), filename = s"$ANALYZE_LOG_DIR/summary", @@ -204,6 +213,12 @@ class TyChecker( filename = s"$ANALYZE_LOG_DIR/detailed-types", silent = silent, ) + dumpFile( + name = "refined targets", + data = refinedString, + filename = s"$ANALYZE_LOG_DIR/refined", + silent = silent, + ) if (inferTypeGuard) val names = typeGuards.map(_._1.name).toSet dumpFile( @@ -217,6 +232,25 @@ class TyChecker( ) } + /** refined targets */ + var refined: Map[RefinementTarget, (Set[Local], Int)] = Map() + def refinedTargets: Int = refined.size + def refinedLocals: Int = refined.values.map(_._1.size).sum + def refinedAvgDepth: Double = + refined.values.map(_._2).sum.toDouble / refined.size + def refinedString: String = + given Rule[Map[RefinementTarget, (Set[Local], Int)]] = + (app, refined) => + val sorted = refined.toList.sortBy { (t, _) => t } + for ((target, (xs, depth)) <- sorted) + app >> target >> " -> " + app >> xs.toList.sorted.mkString("[locals: ", ", ", "]") + app >> " [depth: " >> depth >> "]" + app >> LINE_SEP + app + (new Appender >> refined).toString + + /** inferred type guards */ def getTypeGuards: List[(Func, AbsValue)] = for { func <- cfg.funcs entrySt = getResult(NodePoint(func, func.entry, emptyView)) diff --git a/src/main/scala/esmeta/analyzer/tychecker/TypeGuard.scala b/src/main/scala/esmeta/analyzer/tychecker/TypeGuard.scala index 7b410a43fa..d3f2c7178c 100644 --- a/src/main/scala/esmeta/analyzer/tychecker/TypeGuard.scala +++ b/src/main/scala/esmeta/analyzer/tychecker/TypeGuard.scala @@ -1,6 +1,6 @@ package esmeta.analyzer.tychecker -import esmeta.cfg.{Func, Call} +import esmeta.cfg.* import esmeta.ir.{Func => _, *} import esmeta.ty.* import esmeta.ty.util.{Stringifier => TyStringifier} @@ -63,6 +63,15 @@ trait TypeGuardDecl { self: TyChecker => def apply(ps: (RefinementKind, SymPred)*): TypeGuard = TypeGuard(ps.toMap) } + /** type refinement target */ + enum RefinementTarget: + case BranchTarget(branch: Branch, isTrue: Boolean) + case AssertTarget(block: Block, idx: Int) + def node: Node = this match + case BranchTarget(branch, _) => branch + case AssertTarget(block, _) => block + def func: Func = cfg.funcOf(node) + /** type refinement kinds */ enum RefinementKind { case True, False, Normal, Abrupt, NormalTrue, NormalFalse @@ -97,6 +106,7 @@ trait TypeGuardDecl { self: TyChecker => /** Symbol */ type Sym = Int case class Provenance(map: Map[Func, List[Call]] = Map()) { + def depth: Int = map.values.map(_.length).max def join(that: Provenance): Provenance = Provenance((for { key <- (this.map.keySet union that.map.keySet).toList calls <- (this.map.get(key), that.map.get(key)) match @@ -165,6 +175,9 @@ trait TypeGuardDecl { self: TyChecker => } yield x -> (origTy && ty, prov), sexpr = None, ) + def depth: Int = + val provs = map.values.map(_._2).toList + sexpr.fold(provs)(_._2 :: provs).map(_.depth).max override def toString: String = (new Appender >> this).toString } object SymPred { @@ -356,6 +369,22 @@ trait TypeGuardDecl { self: TyChecker => given Rule[TypeGuard] = (app, guard) => given Rule[Map[RefinementKind, SymPred]] = sortedMapRule("{", "}", " => ") app >> guard.map + given Rule[RefinementTarget] = (app, target) => + import RefinementTarget.* + val node = target.node + val func = target.func + app >> func.nameWithId >> ":" >> node.name >> ":" + target match + case BranchTarget(branch, isTrue) => + app >> (if (isTrue) "T" else "F") + case AssertTarget(block, idx) => + app >> idx + given Ordering[RefinementTarget] = Ordering.by { target => + import RefinementTarget.* + target match + case BranchTarget(branch, isTrue) => (branch.id, if (isTrue) 1 else 0) + case AssertTarget(block, idx) => (block.id, idx) + } given Rule[RefinementKind] = (app, kind) => import RefinementKind.* kind match