From 56b4329b2a3af966d72b3cfdf92fdd1325950c2f Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Wed, 13 Nov 2019 16:51:27 +0100 Subject: [PATCH 1/7] Only unfold once when solving partial evaluator's queries --- build.sbt | 2 +- .../transformers/SimplifierWithSolver.scala | 8 +++++--- .../verification/PartialEvaluation.scala | 17 +++-------------- .../verification/ComponentTestSuite.scala | 3 ++- 4 files changed, 11 insertions(+), 19 deletions(-) diff --git a/build.sbt b/build.sbt index 3eef83d1ac..334b33e0b3 100644 --- a/build.sbt +++ b/build.sbt @@ -14,7 +14,7 @@ val isMac = osInf.indexOf("Mac") >= 0 val osName = if (isWindows) "win" else if (isMac) "mac" else "unix" val osArch = System.getProperty("sun.arch.data.model") -val inoxVersion = "1.1.0-332-ga6cbf8e" +val inoxVersion = "1.1.0-340-gdcf84f2" val dottyLibrary = "dotty-compiler_2.12" val dottyVersion = "0.12.0-RC1-nonbootstrapped" val circeVersion = "0.10.0-M2" diff --git a/core/src/main/scala/stainless/transformers/SimplifierWithSolver.scala b/core/src/main/scala/stainless/transformers/SimplifierWithSolver.scala index 1c100b362f..5f8c21e305 100644 --- a/core/src/main/scala/stainless/transformers/SimplifierWithSolver.scala +++ b/core/src/main/scala/stainless/transformers/SimplifierWithSolver.scala @@ -7,6 +7,7 @@ import scala.language.existentials import scala.concurrent.duration._ import inox.solvers.optCheckModels +import inox.solvers.unrolling.optMaxUnfoldSteps trait SimplifierWithSolver extends inox.transformers.SimplifierWithPC { self => import trees._ @@ -23,14 +24,15 @@ trait SimplifierWithSolver extends inox.transformers.SimplifierWithPC { self => val symbols: self.symbols.type } = inox.Program(trees)(symbols) - protected val solver = + protected val solver = { + val solverContext = context.withOpts(optCheckModels(false), optMaxUnfoldSteps(1)) semantics.getSemantics(program) - .getSolver(context.withOpts(optCheckModels(false))) - .withTimeout(150.millis) + .getSolver(solverContext) .toAPI .asInstanceOf[inox.solvers.SimpleSolverAPI { val program: self.program.type }] + } class Env private (val path: Path) extends PathLike[Env] with SolvingPath { override def implies(cond: Expr): Boolean = { diff --git a/core/src/main/scala/stainless/verification/PartialEvaluation.scala b/core/src/main/scala/stainless/verification/PartialEvaluation.scala index d95a1ad140..af8abf1e79 100644 --- a/core/src/main/scala/stainless/verification/PartialEvaluation.scala +++ b/core/src/main/scala/stainless/verification/PartialEvaluation.scala @@ -31,14 +31,6 @@ trait PartialEvaluation protected class TransformerContext(val symbols: s.Symbols) { self0 => import symbols._ - private[this] val simpleSimplifier = new { - override val trees: s.type = s - override val symbols: self0.symbols.type = self0.symbols - override val opts = inox.solvers.PurityOptions.assumeChecked - } with transformers.PartialEvaluator with inox.transformers.SimplifierWithPath { - override val pp = Env - } - private[this] val solvingSimplifier = new { override val trees: s.type = s override val symbols: self0.symbols.type = self0.symbols @@ -61,11 +53,8 @@ trait PartialEvaluation def shouldPartialEval(fd: FunDef): Boolean = invocationsToEval(fd.id).nonEmpty && !(fd.flags contains Synthetic) - private[this] def partialEval(fi: FunctionInvocation, path: Path, simple: Boolean = false): Expr = { - if (simple) - simpleSimplifier.transform(fi, simpleSimplifier.Env(path)) - else - solvingSimplifier.transform(fi, solvingSimplifier.Env(path)) + private[this] def partialEval(fi: FunctionInvocation, path: Path): Expr = { + solvingSimplifier.transform(fi, solvingSimplifier.Env(path)) } final def transform(fd: FunDef): FunDef = { @@ -78,7 +67,7 @@ trait PartialEvaluation reporter.debug(s" Before: $fi") val (elapsed, res) = timers.partialeval.runAndGetTime { - partialEval(fi, path, simple = isSynthetic(fi.id)) + partialEval(fi, path) } reporter.debug(s" After: ${res.get}") diff --git a/frontends/common/src/it/scala/stainless/verification/ComponentTestSuite.scala b/frontends/common/src/it/scala/stainless/verification/ComponentTestSuite.scala index 5191f338c7..d29e49aa29 100644 --- a/frontends/common/src/it/scala/stainless/verification/ComponentTestSuite.scala +++ b/frontends/common/src/it/scala/stainless/verification/ComponentTestSuite.scala @@ -11,8 +11,9 @@ trait ComponentTestSuite extends inox.TestSuite with inox.ResourceUtils with Inp override def configurations: Seq[Seq[inox.OptionValue[_]]] = Seq( Seq( - inox.optSelectedSolvers(Set("smt-z3")), inox.optTimeout(300.seconds), + inox.optSelectedSolvers(Set("smt-z3")), + inox.solvers.unrolling.optMaxUnfoldSteps(1), verification.optStrictArithmetic(false), ) ) From fb9b3e5621732dd82481afcf2a2a43ecdaeb6525 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Wed, 20 Nov 2019 15:39:21 +0100 Subject: [PATCH 2/7] Take measures into account when unfolding in partial evaluator --- .../transformers/PartialEvaluator.scala | 29 ++++++++++++++++++- .../transformers/SimplifierWithSolver.scala | 4 +-- 2 files changed, 30 insertions(+), 3 deletions(-) diff --git a/core/src/main/scala/stainless/transformers/PartialEvaluator.scala b/core/src/main/scala/stainless/transformers/PartialEvaluator.scala index d0600153b4..30fe886361 100644 --- a/core/src/main/scala/stainless/transformers/PartialEvaluator.scala +++ b/core/src/main/scala/stainless/transformers/PartialEvaluator.scala @@ -10,7 +10,17 @@ trait PartialEvaluator extends SimplifierWithPC { self => import symbols._ import exprOps._ + protected def strictlyPositive(tpe: Type, e: Expr): Expr = (tpe match { + case IntegerType() => GreaterThan(e, IntegerLiteral(0)) + case BVType(signed, size) => GreaterThan(e, BVLiteral(signed, 0, size)) + case TupleType(tps) => and((1 to tps.length).map(i => strictlyPositive(tps(i-1), TupleSelect(e,i))): _*) + case _ => sys.error(s"Type $tpe is not supported for measures") + }).setPos(e) + override protected def simplify(e: Expr, path: Env): (Expr, Boolean) = e match { + // case Annotated(e, Seq(Unchecked)) => + // simplify(e, path) + case fi @ FunctionInvocation(id, tps, args) => val tfd = fi.tfd val (rargs, pargs) = args.map(simplify(_, path)).unzip @@ -20,6 +30,23 @@ trait PartialEvaluator extends SimplifierWithPC { self => case _ => false } (expr) + def validMeasure: Boolean = { + println("measure: " + measureOf(tfd.fullBody)) + measureOf(tfd.fullBody) match { + case Some(measure) => + val nextMeasure = exprOps.replaceFromSymbols(tfd.params.zip(args).toMap, measure) + println("next: " + nextMeasure) + val query = strictlyPositive(nextMeasure.getType, nextMeasure) + println("query: " + query) + val result = path.implies(query) + + println("result: " + result) + result + + case None => false + } + } + def isProductiveUnfolding(inlined: Expr): Boolean = { def isKnown(expr: Expr): Boolean = expr match { case BooleanLiteral(_) => true @@ -74,7 +101,7 @@ trait PartialEvaluator extends SimplifierWithPC { self => inlined .filterNot(containsChoose) - .filter(isProductiveUnfolding) + .filter(expr => validMeasure || isProductiveUnfolding(expr)) .map(unfold) .getOrElse(( FunctionInvocation(id, tps, rargs).copiedFrom(fi), diff --git a/core/src/main/scala/stainless/transformers/SimplifierWithSolver.scala b/core/src/main/scala/stainless/transformers/SimplifierWithSolver.scala index 5f8c21e305..42fea7532f 100644 --- a/core/src/main/scala/stainless/transformers/SimplifierWithSolver.scala +++ b/core/src/main/scala/stainless/transformers/SimplifierWithSolver.scala @@ -7,7 +7,7 @@ import scala.language.existentials import scala.concurrent.duration._ import inox.solvers.optCheckModels -import inox.solvers.unrolling.optMaxUnfoldSteps +import inox.solvers.unrolling.{optUnrollBound, optUnrollFactor} trait SimplifierWithSolver extends inox.transformers.SimplifierWithPC { self => import trees._ @@ -25,7 +25,7 @@ trait SimplifierWithSolver extends inox.transformers.SimplifierWithPC { self => } = inox.Program(trees)(symbols) protected val solver = { - val solverContext = context.withOpts(optCheckModels(false), optMaxUnfoldSteps(1)) + val solverContext = context.withOpts(optCheckModels(false), optUnrollBound(1), optUnrollFactor(2)) semantics.getSemantics(program) .getSolver(solverContext) .toAPI From e4c5d75729727d184bff242af7808a268e4785e9 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Thu, 21 Nov 2019 16:43:29 +0100 Subject: [PATCH 3/7] Update local Inox version --- build.sbt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.sbt b/build.sbt index 334b33e0b3..f8ed8710d4 100644 --- a/build.sbt +++ b/build.sbt @@ -14,7 +14,7 @@ val isMac = osInf.indexOf("Mac") >= 0 val osName = if (isWindows) "win" else if (isMac) "mac" else "unix" val osArch = System.getProperty("sun.arch.data.model") -val inoxVersion = "1.1.0-340-gdcf84f2" +val inoxVersion = "1.1.0-341-gb70895c" val dottyLibrary = "dotty-compiler_2.12" val dottyVersion = "0.12.0-RC1-nonbootstrapped" val circeVersion = "0.10.0-M2" From c37c2dc6cef805c0baf9cf1957cf2b4a06a810a8 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Fri, 22 Nov 2019 15:32:41 +0100 Subject: [PATCH 4/7] Re-enable unfolding in test suite --- .../src/it/scala/stainless/verification/ComponentTestSuite.scala | 1 - 1 file changed, 1 deletion(-) diff --git a/frontends/common/src/it/scala/stainless/verification/ComponentTestSuite.scala b/frontends/common/src/it/scala/stainless/verification/ComponentTestSuite.scala index d29e49aa29..153fe1ed31 100644 --- a/frontends/common/src/it/scala/stainless/verification/ComponentTestSuite.scala +++ b/frontends/common/src/it/scala/stainless/verification/ComponentTestSuite.scala @@ -13,7 +13,6 @@ trait ComponentTestSuite extends inox.TestSuite with inox.ResourceUtils with Inp Seq( inox.optTimeout(300.seconds), inox.optSelectedSolvers(Set("smt-z3")), - inox.solvers.unrolling.optMaxUnfoldSteps(1), verification.optStrictArithmetic(false), ) ) From f8da857f197e5309a50ffb4f583476f810b52de6 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Fri, 22 Nov 2019 16:04:32 +0100 Subject: [PATCH 5/7] Add simple test suite for bounded unfolding --- .larabot.conf | 3 +-- .../stainless/verification/VerificationSuite.scala | 14 ++++++++++++++ 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/.larabot.conf b/.larabot.conf index ce806393f8..bd70e1e6e9 100644 --- a/.larabot.conf +++ b/.larabot.conf @@ -1,6 +1,5 @@ commands = [ - "sbt -batch -Dparallel=5 test" - "sbt -batch -Dparallel=5 it:test" + "sbt -batch -Dparallel=1 it:testOnly *SMTZ3Unroll*" ] nightly { diff --git a/frontends/scalac/src/it/scala/stainless/verification/VerificationSuite.scala b/frontends/scalac/src/it/scala/stainless/verification/VerificationSuite.scala index 1940aa3994..652c92398e 100644 --- a/frontends/scalac/src/it/scala/stainless/verification/VerificationSuite.scala +++ b/frontends/scalac/src/it/scala/stainless/verification/VerificationSuite.scala @@ -64,6 +64,20 @@ class SMTZ3VerificationSuite extends VerificationSuite { } } +class SMTZ3UnrollBoundVerificationSuite(unrollBound: Int, unrollFactor: Int) extends SMTZ3VerificationSuite { + override def configurations = super.configurations.map { + seq => Seq( + inox.solvers.unrolling.optUnrollBound(unrollBound), + inox.solvers.unrolling.optUnrollFactor(unrollFactor), + ) ++ seq + } +} + +class SMTZ3UnrollBoundOneOneSuite extends SMTZ3UnrollBoundVerificationSuite(1, 1) +class SMTZ3UnrollBoundOneTwoSuite extends SMTZ3UnrollBoundVerificationSuite(1, 2) +class SMTZ3UnrollBoundTwoOneSuite extends SMTZ3UnrollBoundVerificationSuite(2, 1) +class SMTZ3UnrollBoundTwoTwoSuite extends SMTZ3UnrollBoundVerificationSuite(2, 2) + class CodeGenVerificationSuite extends SMTZ3VerificationSuite { override def configurations = super.configurations.map { seq => Seq( From f79e4ca57a4ebabf0fb403c08f325385f1567929 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Fri, 22 Nov 2019 16:26:13 +0100 Subject: [PATCH 6/7] Remove printlns --- .../scala/stainless/transformers/PartialEvaluator.scala | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/core/src/main/scala/stainless/transformers/PartialEvaluator.scala b/core/src/main/scala/stainless/transformers/PartialEvaluator.scala index 30fe886361..b691d31df4 100644 --- a/core/src/main/scala/stainless/transformers/PartialEvaluator.scala +++ b/core/src/main/scala/stainless/transformers/PartialEvaluator.scala @@ -31,17 +31,11 @@ trait PartialEvaluator extends SimplifierWithPC { self => } (expr) def validMeasure: Boolean = { - println("measure: " + measureOf(tfd.fullBody)) measureOf(tfd.fullBody) match { case Some(measure) => val nextMeasure = exprOps.replaceFromSymbols(tfd.params.zip(args).toMap, measure) - println("next: " + nextMeasure) val query = strictlyPositive(nextMeasure.getType, nextMeasure) - println("query: " + query) - val result = path.implies(query) - - println("result: " + result) - result + path.implies(query) case None => false } From 7278f8a73e6568c045cda20e1d62c899362d0d06 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Wed, 22 Jan 2020 11:46:01 +0100 Subject: [PATCH 7/7] Trust measures --- .../stainless/transformers/PartialEvaluator.scala | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/core/src/main/scala/stainless/transformers/PartialEvaluator.scala b/core/src/main/scala/stainless/transformers/PartialEvaluator.scala index b691d31df4..1afb1076ea 100644 --- a/core/src/main/scala/stainless/transformers/PartialEvaluator.scala +++ b/core/src/main/scala/stainless/transformers/PartialEvaluator.scala @@ -30,14 +30,11 @@ trait PartialEvaluator extends SimplifierWithPC { self => case _ => false } (expr) - def validMeasure: Boolean = { - measureOf(tfd.fullBody) match { - case Some(measure) => - val nextMeasure = exprOps.replaceFromSymbols(tfd.params.zip(args).toMap, measure) - val query = strictlyPositive(nextMeasure.getType, nextMeasure) - path.implies(query) - - case None => false + def validMeasure: Option[Boolean] = { + measureOf(tfd.fullBody) map { measure => + val nextMeasure = exprOps.replaceFromSymbols(tfd.params.zip(args).toMap, measure) + val query = strictlyPositive(nextMeasure.getType, nextMeasure) + path.implies(query) } } @@ -95,7 +92,7 @@ trait PartialEvaluator extends SimplifierWithPC { self => inlined .filterNot(containsChoose) - .filter(expr => validMeasure || isProductiveUnfolding(expr)) + .filter(expr => validMeasure.getOrElse(isProductiveUnfolding(expr))) .map(unfold) .getOrElse(( FunctionInvocation(id, tps, rargs).copiedFrom(fi),