From c6bf974ff2c7d2da8968c644b079ff000e409db6 Mon Sep 17 00:00:00 2001 From: Georg Stefan Schmid Date: Fri, 3 Sep 2021 16:13:57 +0200 Subject: [PATCH] Add debug option to dump blocker graph --- src/main/scala/inox/Main.scala | 1 + src/main/scala/inox/ast/SymbolOps.scala | 14 +++++----- .../solvers/unrolling/FunctionTemplates.scala | 7 ++--- .../solvers/unrolling/TemplateGenerator.scala | 6 ++--- .../inox/solvers/unrolling/Templates.scala | 19 ++++++++++--- .../solvers/unrolling/UnrollingSolver.scala | 27 +++++++++++++++++++ 6 files changed, 58 insertions(+), 16 deletions(-) diff --git a/src/main/scala/inox/Main.scala b/src/main/scala/inox/Main.scala index 41a7404dd..f4f4b7d67 100644 --- a/src/main/scala/inox/Main.scala +++ b/src/main/scala/inox/Main.scala @@ -12,6 +12,7 @@ trait MainHelpers { utils.DebugSectionTimers, solvers.DebugSectionSolver, solvers.smtlib.DebugSectionSMT, + solvers.unrolling.DebugSectionBlockerGraph, tip.DebugSectionTip ) diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala index ae66e0f2f..1001cc3a5 100644 --- a/src/main/scala/inox/ast/SymbolOps.scala +++ b/src/main/scala/inox/ast/SymbolOps.scala @@ -63,7 +63,7 @@ trait SymbolOps { self: TypeOps => /** Override point for transformer with PC creation - * + * * Note that we don't actually need the `PathProvider[P]` here but it will * become useful in the Stainless overrides. */ protected def transformerWithPC[P <: PathLike[P]]( @@ -247,7 +247,7 @@ trait SymbolOps { self: TypeOps => } def evalChildren(e: Expr)(implicit opts: PurityOptions): Expr = e match { - case Operator(es, recons) => recons(es.map(rec)) + case Operator(es, recons) => recons(es.map(rec)).copiedFrom(e) } // TODO: Should we run this within a fixpoint with simplifyByConstructor? @@ -398,7 +398,7 @@ trait SymbolOps { self: TypeOps => class Liftable(path: Path) { def unapply(e: Expr): Option[Seq[Expr]] = { // The set of minimal conditions that must be met for an expression to be liftable - val minimal = + val minimal = (isSimple(e) || !onlySimple) && // check whether we want only simple expression !containsChoose(e) && // expressions containing chooses can't be lifted (!inFunction || !containsRecursive(e)) // recursive functions can't be lifted from lambdas @@ -438,7 +438,7 @@ trait SymbolOps { self: TypeOps => preserveApps ) => val Operator(es, recons) = e - recons(es.map(op(_, env))) + recons(es.map(op(_, env))).copiedFrom(e) case Let(vd, e @ liftable(conditions), b) => subst(vd.toVariable) = (e, conditions) @@ -501,7 +501,7 @@ trait SymbolOps { self: TypeOps => val lambda = Lambda(params, recons(esWithParams.map { case (_, Some(vd)) => vd.toVariable case (e, _) => e - })) + }).copiedFrom(e)) Application( getVariable(lambda, lambda.getType, conditions = conditions), @@ -511,7 +511,7 @@ trait SymbolOps { self: TypeOps => case _ => val (ids, vs, es, tps, flags, recons) = deconstructor.deconstruct(e) val newVs = vs map transformVar - op.sup(recons(ids, newVs, es, tps, flags), env) + op.sup(recons(ids, newVs, es, tps, flags).copiedFrom(e), env) } }, (tpe, env, op) => transformType(vars, tpe, inFunction, env) @@ -695,7 +695,7 @@ trait SymbolOps { self: TypeOps => case Forall(args, body) => Forall(args, rec(body, lambdas, true)) case Operator(es, recons) => - recons(es.map(rec(_, lambdas, inForall))) + recons(es.map(rec(_, lambdas, inForall))).copiedFrom(e) } rec(e, Map.empty, false) diff --git a/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala b/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala index 63ccd51df..d2b02747a 100644 --- a/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala +++ b/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala @@ -33,12 +33,13 @@ trait FunctionTemplates { self: Templates => object FunctionTemplate { private val cache: MutableMap[TypedFunDef, FunctionTemplate] = MutableMap.empty - def apply(tfd: TypedFunDef): FunctionTemplate = cache.getOrElse(tfd, { + def apply(tfd: TypedFunDef, pos: utils.Position): FunctionTemplate = cache.getOrElse(tfd, { val body: Expr = timers.solvers.simplify.run { simplifyFormula(tfd.fullBody) } val tpVars = tfd.tps.flatMap(variableSeq).distinct val fdArgs: Seq[Variable] = tfd.params.map(_.toVariable) - val call: Expr = tfd.applied(fdArgs) + // Note: This position is best-effort, since function templates are cached. + val call: Expr = tfd.applied(fdArgs).setPos(pos) val start = Variable.fresh("start", BooleanType(), true) val pathVar = start -> encodeSymbol(start) @@ -237,7 +238,7 @@ trait FunctionTemplates { self: Templates => val templateClauses = Template.instantiate(clauses, calls, apps, matchers, equalities, substMap) substClauses ++ templateClauses } getOrElse { - FunctionTemplate(tfd).instantiate(defBlocker, args ++ tpSubst) + FunctionTemplate(tfd, call.getPos).instantiate(defBlocker, args ++ tpSubst) } } diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala index 4adb701fc..7779e4b28 100644 --- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala +++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala @@ -141,7 +141,7 @@ trait TemplateGenerator { self: Templates => newArg } - val newCall = thenCall.tfd.applied(newArgs) + val newCall = thenCall.tfd.applied(newArgs).copiedFrom(thenCall) builder.storeGuarded(newBlocker, Equals(newExpr, newCall)) } @@ -514,7 +514,7 @@ trait TemplateGenerator { self: Templates => storeEquality(pathVar, re1, re2) Application(v, Seq(re1, re2)) - case Operator(as, r) => r(as.map(a => rec(pathVar, a, None))) + case Operator(as, recons) => recons(as.map(a => rec(pathVar, a, None))).copiedFrom(expr) } val p = rec(pathVar, expr, polarity) @@ -578,7 +578,7 @@ trait TemplateGenerator { self: Templates => and( sort.invariant .filter(_ => generator == FreeGenerator) - .map(_.applied(Seq(expr))) + .map(tfd => tfd.applied(Seq(expr)).copiedFrom(tfd)) .getOrElse(BooleanLiteral(true)), if (sort.definition.isInductive && !state.recurseAdt) { storeType(pathVar, tpe, expr) diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala index 015ab5c37..e9845db58 100644 --- a/src/main/scala/inox/solvers/unrolling/Templates.scala +++ b/src/main/scala/inox/solvers/unrolling/Templates.scala @@ -177,6 +177,18 @@ trait Templates if (equal.nonEmpty) equal else (condImplied(b) + b) })(bs).filter(_ != trueT) + def blockerGraph(strict: Boolean = true): Graphs.DiGraph[Encoded, Graphs.SimpleEdge[Encoded]] = { + var implies = condImplies.toSeq.toMap + if (!strict) + implies = implies merge potImplies.toSeq.toMap + val nodes = implies.keySet ++ implies.values.flatten + val edges = implies.iterator + .flatMap(imp => imp._2.map(imp._1 -> _)) + .map(e => Graphs.SimpleEdge(e._1, e._2)) + .toSet + Graphs.DiGraph(nodes, edges) + } + def promoteBlocker(b: Encoded, force: Boolean = false): Boolean = { var seen: Set[Encoded] = Set.empty var promoted: Boolean = false @@ -226,7 +238,7 @@ trait Templates } /** Represents a named function call in the unfolding procedure */ - case class Call(tfd: TypedFunDef, args: Seq[Arg], tpSubst: Seq[Arg]) { + case class Call(tfd: TypedFunDef, args: Seq[Arg], tpSubst: Seq[Arg]) extends utils.Positioned { override def toString: String = { def pArgs(args: Seq[Arg]): String = args.map { case Right(m) => m.toString @@ -246,7 +258,7 @@ trait Templates def substitute(substituter: Encoded => Encoded, msubst: Map[Encoded, Matcher]): Call = copy( args = args.map(_.substitute(substituter, msubst)), tpSubst = tpSubst.map(_.substitute(substituter, msubst)) - ) + ).setPos(this.getPos) } /** Represents an application of a first-class function in the unfolding procedure */ @@ -594,9 +606,10 @@ trait Templates val calls = exprOps.collect[FunctionInvocation] { case fi: FunctionInvocation => Set(fi) case _ => Set.empty - } (expr).map { case FunctionInvocation(id, tps, args) => + } (expr).map { case fi @ FunctionInvocation(id, tps, args) => val tpVars = tps.flatMap(variableSeq).distinct Call(getFunction(id, tps), args.map(encodeArg), tpVars.map(encodeArg)) + .setPos(fi.getPos) }.filter { case Call(tfd, args, _) => !optCall.exists(p => p._1 == tfd && p._2 == args) } diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala index ba8c32700..3ea6561b1 100644 --- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala +++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala @@ -23,6 +23,10 @@ object optModelFinding extends IntOptionDef("model-finding", 0, " | }) } +object DebugSectionBlockerGraph extends inox.DebugSection("blocker-graph") + +private[unrolling] object DebugBlockerGraphFileNumbers extends UniqueCounter[String] + trait AbstractUnrollingSolver extends Solver { self => import context._ @@ -826,6 +830,29 @@ trait AbstractUnrollingSolver extends Solver { self => } } + reporter.whenDebug(DebugSectionBlockerGraph) { debug => + val file = options.findOptionOrDefault(Main.optFiles).headOption.map(_.getName).getOrElse("NA") + val n = DebugBlockerGraphFileNumbers.next(file) + val fileName = s"blocker-graphs/$file-$n.dot" + + val javaFile = new java.io.File(fileName) + javaFile.getParentFile.mkdirs() + + debug(s"Outputting blocker graph into $fileName") + + val calls = templates.getCalls + val callsMap = calls.toMap + assert(calls.size == callsMap.size) + + type Graph = Graphs.DiGraph[Encoded, Graphs.SimpleEdge[Encoded]] + val printer = new GraphPrinters.DotPrinter[Encoded, Graphs.SimpleEdge[Encoded], Graph]() + printer.setNodeLabel { n => + val callStr = callsMap.get(n).map(call => s"\n(${call.tfd.id} @ ${call.getPos})").getOrElse("") + s"$n$callStr" + } + printer.asFile(templates.blockerGraph(strict = false), fileName) + } + val CheckResult(res) = currentState res }).recover {