From 7687b79788b4514cb3c9dfdb00317382de3eb4cd Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 9 Jan 2013 15:49:52 +0100
Subject: [PATCH] CEGIS: Implement enumerate&test given known valid inputs
CE-Testing allows CEGIS to compile the program at the current unrolling
level and test with provided Bs (the determinized program) on previously
discovered inputs. This allows us to skip a SAT query in case one of
them fails.
Given a series of known valid inputs, it can prune program candidates by
enumerating them and testing against these inputs. This should
dramatically reduce the number of SAT queries. Currently we have no
heuristic to disable enumarting when branching factor becomes too big.
We might want to do random sampling.
We start by figuring out one basic examples that we can use for pruning.
In the presence of a path-condition, we need to perform a simple SAT
query
Also, B-Paths enforces sub-branches to use a fixed value if the parent
branch is closed. This should prune the program exploration behind
closed branches. We have observed no clear benefits in terms of
performance yet.
CEGIS will only use fully determined functions as candidates for
gencalls. (e.g. no functions containing 'choose')
---
.../scala/leon/codegen/CodeGeneration.scala | 33 +-
.../scala/leon/codegen/CompilationUnit.scala | 12 +-
.../leon/evaluators/CodeGenEvaluator.scala | 41 +-
.../leon/evaluators/DefaultEvaluator.scala | 7 +-
.../scala/leon/solvers/z3/FairZ3Solver.scala | 140 ++++-
.../leon/solvers/z3/FunctionTemplate.scala | 52 ++
.../leon/synthesis/SynthesisContext.scala | 2 +
.../leon/synthesis/SynthesizerOptions.scala | 19 +-
.../scala/leon/synthesis/rules/Cegis.scala | 537 ++++++++++++++----
.../leon/synthesis/utils/Benchmarks.scala | 1 +
.../test/evaluators/EvaluatorsTests.scala | 31 +-
.../leon/test/synthesis/SynthesisSuite.scala | 2 +-
.../XLangVerificationRegression.scala | 2 -
13 files changed, 710 insertions(+), 169 deletions(-)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index c495ccb5d..0afef05bf 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -45,6 +45,9 @@ object CodeGeneration {
case _ : MapType =>
"L" + MapClass + ";"
+ case ArrayType(base) =>
+ "[" + typeToJVM(base)
+
case _ => throw CompilationException("Unsupported type : " + tpe)
}
@@ -61,7 +64,7 @@ object CodeGeneration {
case Int32Type | BooleanType | UnitType =>
ch << IRETURN
- case _ : ClassType | _ : TupleType | _ : SetType | _ : MapType =>
+ case _ : ClassType | _ : TupleType | _ : SetType | _ : MapType | _ : ArrayType =>
ch << ARETURN
case other =>
@@ -282,6 +285,34 @@ object CodeGeneration {
mkExpr(e, ch)
ch << INEG
+ case ArrayLength(a) =>
+ mkExpr(a, ch)
+ ch << ARRAYLENGTH
+
+ case as @ ArraySelect(a,i) =>
+ mkExpr(a, ch)
+ mkExpr(i, ch)
+ ch << (as.getType match {
+ case Untyped => throw CompilationException("Cannot compile untyped array access.")
+ case Int32Type => IALOAD
+ case BooleanType => BALOAD
+ case _ => AALOAD
+ })
+
+ case a @ FiniteArray(es) =>
+ ch << Ldc(es.size)
+ val storeInstr = a.getType match {
+ case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
+ case ArrayType(BooleanType) => ch << NewArray.primitive("T_BOOLEAN"); BASTORE
+ case ArrayType(other) => ch << NewArray(typeToJVM(other)); AASTORE
+ case other => throw CompilationException("Cannot compile finite array expression whose type is %s.".format(other))
+ }
+ for((e,i) <- es.zipWithIndex) {
+ ch << DUP << Ldc(i)
+ mkExpr(e, ch)
+ ch << storeInstr
+ }
+
// Misc and boolean tests
case Error(desc) =>
ch << New(ErrorClass) << DUP
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 799241c5c..0d547d27a 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -67,7 +67,12 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
val cons = caseClassConstructors(ccd)
cons.newInstance(args.map(valueToJVM).toArray : _*).asInstanceOf[AnyRef]
- // just slightly overkill...
+ // For now, we only treat boolean arrays separately.
+ // We have a use for these, mind you.
+ case f @ FiniteArray(exprs) if f.getType == ArrayType(BooleanType) =>
+ exprs.map(e => valueToJVM(e).asInstanceOf[java.lang.Boolean].booleanValue).toArray
+
+ // Just slightly overkill...
case _ =>
compileExpression(e, Seq()).evalToJVM(Seq())
}
@@ -112,6 +117,9 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
}
def compileExpression(e: Expr, args: Seq[Identifier]): CompiledExpression = {
+ if(e.getType == Untyped) {
+ throw new IllegalArgumentException("Cannot compile untyped expression [%s].".format(e))
+ }
val id = nextExprId
@@ -149,7 +157,7 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
case Int32Type | BooleanType =>
ch << IRETURN
- case UnitType | TupleType(_) | SetType(_) | MapType(_, _) | AbstractClassType(_) | CaseClassType(_) =>
+ case UnitType | TupleType(_) | SetType(_) | MapType(_, _) | AbstractClassType(_) | CaseClassType(_) | ArrayType(_) =>
ch << ARETURN
case other =>
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index 7202c4ff1..f45372327 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -30,21 +30,30 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
import leon.codegen.runtime.LeonCodeGenRuntimeException
import leon.codegen.runtime.LeonCodeGenEvaluationException
- val ce = unit.compileExpression(expression, argorder)
-
- Some((args : Seq[Expr]) => {
- try {
- EvaluationSuccessful(ce.eval(args))
- } catch {
- case e : ArithmeticException =>
- EvaluationFailure(e.getMessage)
-
- case e : LeonCodeGenRuntimeException =>
- EvaluationFailure(e.getMessage)
-
- case e : LeonCodeGenEvaluationException =>
- EvaluationError(e.getMessage)
- }
- })
+ try {
+ val ce = unit.compileExpression(expression, argorder)
+
+ Some((args : Seq[Expr]) => {
+ try {
+ EvaluationSuccessful(ce.eval(args))
+ } catch {
+ case e : ArithmeticException =>
+ EvaluationFailure(e.getMessage)
+
+ case e : ArrayIndexOutOfBoundsException =>
+ EvaluationFailure(e.getMessage)
+
+ case e : LeonCodeGenRuntimeException =>
+ EvaluationFailure(e.getMessage)
+
+ case e : LeonCodeGenEvaluationException =>
+ EvaluationError(e.getMessage)
+ }
+ })
+ } catch {
+ case t: Throwable =>
+ ctx.reporter.warning("Error while compiling expression: "+t.getMessage)
+ None
+ }
}
}
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index 9b0bbdc2e..47d86be95 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -253,7 +253,11 @@ class DefaultEvaluator(ctx : LeonContext, prog : Program) extends Evaluator(ctx,
case ArraySelect(a, i) => {
val IntLiteral(index) = rec(ctx, i)
val FiniteArray(exprs) = rec(ctx, a)
- exprs(index)
+ try {
+ exprs(index)
+ } catch {
+ case e : IndexOutOfBoundsException => throw RuntimeError(e.getMessage)
+ }
}
case FiniteArray(exprs) => {
FiniteArray(exprs.map(e => rec(ctx, e)))
@@ -297,6 +301,7 @@ class DefaultEvaluator(ctx : LeonContext, prog : Program) extends Evaluator(ctx,
try {
EvaluationSuccessful(rec(mapping, expression))
} catch {
+ case so: StackOverflowError => EvaluationError("Stack overflow")
case EvalError(msg) => EvaluationError(msg)
case RuntimeError(msg) => EvaluationFailure(msg)
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 641b86c81..0b79871ba 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -36,11 +36,13 @@ class FairZ3Solver(context : LeonContext)
)
// What wouldn't we do to avoid defining vars?
- val (feelingLucky, checkModels, useCodeGen, evalGroundApps) = locally {
- var lucky = false
- var check = false
- var codegen = false
- var evalground = false
+ val (feelingLucky, checkModels, useCodeGen, evalGroundApps, unrollUnsatCores, pruneUnsatCores) = locally {
+ var lucky = true
+ var check = false
+ var codegen = false
+ var evalground = false
+ var unrollUnsatCores = true
+ var pruneUnsatCores = true
for(opt <- context.options) opt match {
case LeonFlagOption("checkmodels") => check = true
@@ -50,7 +52,7 @@ class FairZ3Solver(context : LeonContext)
case _ =>
}
- (lucky,check,codegen,evalground)
+ (lucky, check, codegen, evalground, unrollUnsatCores, pruneUnsatCores)
}
private var evaluator : Evaluator = null
@@ -175,7 +177,7 @@ class FairZ3Solver(context : LeonContext)
(false, asMap)
case EvaluationError(msg) =>
- reporter.error("Something went wrong. While evaluating the model, we got this : " + msg)
+ reporter.warning("Something went wrong. While evaluating the model, we got this : " + msg)
(false, asMap)
}
@@ -210,7 +212,7 @@ class FairZ3Solver(context : LeonContext)
// Keep which function invocation is guarded by which guard with polarity,
// also specify the generation of the blocker
- private var blockersInfoStack : List[MutableMap[(Z3AST,Boolean), (Int, Z3AST, Set[Z3FunctionInvocation])]] = List(MutableMap())
+ private var blockersInfoStack : List[MutableMap[(Z3AST,Boolean), (Int, Int, Z3AST, Set[Z3FunctionInvocation])]] = List(MutableMap())
def blockersInfo = blockersInfoStack.head
@@ -222,14 +224,28 @@ class FairZ3Solver(context : LeonContext)
blockersInfoStack = blockersInfoStack.drop(lvl)
}
- def z3CurrentZ3Blockers = blockersInfo.map(_._2._2)
+ def z3CurrentZ3Blockers = blockersInfo.map(_._2._3)
+
+ def dumpBlockers = {
+ blockersInfo.groupBy(_._2._1).toSeq.sortBy(_._1).foreach { case (gen, entries) =>
+ reporter.info("--- "+gen)
+
+ for (((bast, bpol), (gen, origGen, ast, fis)) <- entries) {
+ reporter.info(". "+(if(!bpol) "¬" else "")+bast +" ~> "+fis.map(_.funDef.id))
+ }
+ }
+ }
def canUnroll = !blockersInfo.isEmpty
def getZ3BlockersToUnlock: Seq[(Z3AST, Boolean)] = {
- val minGeneration = blockersInfo.values.map(_._1).min
+ if (!blockersInfo.isEmpty) {
+ val minGeneration = blockersInfo.values.map(_._1).min
- blockersInfo.filter(_._2._1 == minGeneration).toSeq.map(_._1)
+ blockersInfo.filter(_._2._1 == minGeneration).toSeq.map(_._1)
+ } else {
+ Seq()
+ }
}
private def registerBlocker(gen: Int, id: Z3AST, pol: Boolean, fis: Set[Z3FunctionInvocation]) {
@@ -238,12 +254,12 @@ class FairZ3Solver(context : LeonContext)
val z3ast = if (pol) z3.mkNot(id) else id
blockersInfo.get(pair) match {
- case Some((exGen, _, exFis)) =>
+ case Some((exGen, origGen, _, exFis)) =>
assert(exGen == gen, "Mixing the same pair "+pair+" with various generations "+ exGen+" and "+gen)
- blockersInfo(pair) = ((gen, z3ast, fis++exFis))
+ blockersInfo(pair) = ((gen, origGen, z3ast, fis++exFis))
case None =>
- blockersInfo(pair) = ((gen, z3ast, fis))
+ blockersInfo(pair) = ((gen, gen, z3ast, fis))
}
}
@@ -264,18 +280,42 @@ class FairZ3Solver(context : LeonContext)
val (newClauses, newBlocks) = template.instantiate(template.z3ActivatingBool, true, z3args)
- for(((i, p), fis) <- newBlocks) {
- registerBlocker(1, i, p, fis)
+ val extraClauses = for(((i, p), fis) <- newBlocks) yield {
+ registerBlocker(nextGeneration(0), i, p, fis)
+ //unlock(i, p)
+ Nil
+ }
+
+ newClauses ++ extraClauses.flatten
+ }
+
+ def nextGeneration(gen: Int) = gen + 3
+
+ def decreaseAllGenerations() = {
+ for ((block, (gen, origGen, ast, finvs)) <- blockersInfo) {
+ // We also decrease the original generation here
+ blockersInfo(block) = (math.max(1,gen-1), math.max(1,origGen-1), ast, finvs)
+ }
+ }
+
+ def prune(ast: Z3AST, pol: Boolean) = {
+ val b = (ast, pol)
+ blockersInfo -= b
+ }
+
+ def promoteBlocker(bast: Z3AST, pol: Boolean) = {
+ val b = (bast, pol)
+ if (blockersInfo contains b) {
+ val (gen, origGen, ast, finvs) = blockersInfo(b)
+ blockersInfo(b) = (1, origGen, ast, finvs)
}
-
- newClauses
}
def unlock(id: Z3AST, pol: Boolean) : Seq[Z3AST] = {
val pair = (id, pol)
assert(blockersInfo contains pair)
- val (gen, _, fis) = blockersInfo(pair)
+ val (gen, origGen, _, fis) = blockersInfo(pair)
blockersInfo -= pair
var newClauses : Seq[Z3AST] = Seq.empty
@@ -285,7 +325,8 @@ class FairZ3Solver(context : LeonContext)
val (newExprs, newBlocks) = template.instantiate(id, pol, fi.args)
for(((i, p), fis) <- newBlocks) {
- registerBlocker(gen+1, i, p, fis)
+ // We use origGen here
+ registerBlocker(nextGeneration(origGen), i, p, fis)
}
newClauses ++= newExprs
@@ -405,9 +446,9 @@ class FairZ3Solver(context : LeonContext)
reporter.info(" - Running Z3 search...")
- //reporter.info("Searching in:\n"+solver.getAssertions.toSeq.mkString("\nAND\n"))
- //reporter.info("Unroll. Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString(" && "))
- //reporter.info("Userland Assumptions:\n"+assumptionsAsZ3.mkString(" && "))
+ reporter.info("Searching in:\n"+solver.getAssertions.toSeq.mkString("\nAND\n"))
+ reporter.info("Unroll. Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString(" && "))
+ reporter.info("Userland Assumptions:\n"+assumptionsAsZ3.mkString(" && "))
z3Time.start
solver.push() // FIXME: remove when z3 bug is fixed
@@ -459,9 +500,47 @@ class FairZ3Solver(context : LeonContext)
// distinction is made inside.
case Some(false) =>
- //val core = z3CoreToCore(solver.getUnsatCore)
+ val z3Core = solver.getUnsatCore
- //reporter.info("UNSAT BECAUSE: "+solver.getUnsatCore.mkString(" AND "))
+ def coreElemToBlocker(c: Z3AST): (Z3AST, Boolean) = {
+ z3.getASTKind(c) match {
+ case Z3AppAST(decl, args) =>
+ z3.getDeclKind(decl) match {
+ case Z3DeclKind.OpNot =>
+ (args(0), true)
+ case Z3DeclKind.OpUninterpreted =>
+ (c, false)
+ }
+
+ case ast =>
+ (c, false)
+ }
+ }
+
+ if (unrollUnsatCores) {
+ unrollingBank.decreaseAllGenerations()
+
+ for (c <- solver.getUnsatCore) {
+ val (z3ast, pol) = coreElemToBlocker(c)
+
+ unrollingBank.promoteBlocker(z3ast, pol)
+ }
+
+ }
+
+ if (pruneUnsatCores) {
+ z3Core.toSeq match {
+ case Seq(c) =>
+ // If there is only one element in the Seq, we can prune
+ val (z3ast, pol) = coreElemToBlocker(c)
+
+ unrollingBank.prune(z3ast, !pol)
+ solver.assertCnstr(if (pol) z3ast else z3.mkNot(z3ast))
+ case _ =>
+ }
+ }
+
+ reporter.info("UNSAT BECAUSE: "+solver.getUnsatCore.mkString("\n AND \n"))
//reporter.info("UNSAT BECAUSE: "+core.mkString(" AND "))
if (!forceStop) {
@@ -480,10 +559,10 @@ class FairZ3Solver(context : LeonContext)
res2 match {
case Some(false) =>
- //reporter.info("UNSAT WITHOUT Blockers")
+ reporter.info("UNSAT WITHOUT Blockers")
foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore))
case Some(true) =>
- //reporter.info("SAT WITHOUT Blockers")
+ reporter.info("SAT WITHOUT Blockers")
if (this.feelingLucky && !forceStop) {
// we might have been lucky :D
luckyTime.start
@@ -507,15 +586,18 @@ class FairZ3Solver(context : LeonContext)
reporter.info("- We need to keep going.")
//val toReleaseAsPairs = unrollingBank.getBlockersToUnlock
+ // unrollingBank.dumpBlockers
val toReleaseAsPairs = unrollingBank.getZ3BlockersToUnlock
reporter.info(" - more unrollings")
+ unrollingBank.dumpBlockers
+
for((id, polarity) <- toReleaseAsPairs) {
unlockingTime.start
val newClauses = unrollingBank.unlock(id, polarity)
unlockingTime.stop
- //reporter.info(" - - Unrolling behind "+(if(!polarity) "¬" else "")+id)
+ reporter.info(" - - Unrolling behind "+(if(!polarity) "¬" else "")+id)
//for (cl <- newClauses) {
// reporter.info(" - - - "+cl)
//}
@@ -540,6 +622,8 @@ class FairZ3Solver(context : LeonContext)
StopwatchCollections.get("FairZ3 Unlocking") += unlockingTime
StopwatchCollections.get("FairZ3 ScalaTime") += scalaTime
+ reporter.info(" !! DONE !! ")
+
if(forceStop) {
None
} else {
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index 66cb6af25..da4de6471 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -142,6 +142,29 @@ object FunctionTemplate {
}
}
+ // Group elements that satisfy p toghether
+ // List(a, a, a, b, c, a, a), with p = _ == a will produce:
+ // List(List(a,a,a), List(b), List(c), List(a, a))
+ def groupWhile[T](p: T => Boolean, l: Seq[T]): Seq[Seq[T]] = {
+ var res: Seq[Seq[T]] = Nil
+
+ var c = l
+
+ while(!c.isEmpty) {
+ val (span, rest) = c.span(p)
+
+ if (span.isEmpty) {
+ res = res :+ Seq(rest.head)
+ c = rest.tail
+ } else {
+ res = res :+ span
+ c = rest
+ }
+ }
+
+ res
+ }
+
def rec(pathVar : Identifier, pathPol : Boolean, expr : Expr) : Expr = {
expr match {
case l @ Let(i, e, b) =>
@@ -154,6 +177,35 @@ object FunctionTemplate {
case m : MatchExpr => sys.error("MatchExpr's should have been eliminated.")
+ case i @ Implies(lhs, rhs) =>
+ if (containsFunctionCalls(i)) {
+ rec(pathVar, pathPol, IfExpr(lhs, rhs, BooleanLiteral(true)))
+ } else {
+ i
+ }
+
+ case a @ And(parts) =>
+ if (containsFunctionCalls(a)) {
+ val partitions = groupWhile((e: Expr) => !containsFunctionCalls(e), parts)
+
+ val ifExpr = partitions.map(And(_)).reduceRight{ (a: Expr, b: Expr) => IfExpr(a, b, BooleanLiteral(false)) }
+
+ rec(pathVar, pathPol, ifExpr)
+ } else {
+ a
+ }
+
+ case o @ Or(parts) =>
+ if (containsFunctionCalls(o)) {
+ val partitions = groupWhile((e: Expr) => !containsFunctionCalls(e), parts)
+
+ val ifExpr = partitions.map(Or(_)).reduceRight{ (a: Expr, b: Expr) => IfExpr(a, BooleanLiteral(true), b) }
+
+ rec(pathVar, pathPol, ifExpr)
+ } else {
+ o
+ }
+
case i @ IfExpr(cond, then, elze) => {
if(!containsFunctionCalls(cond) && !containsFunctionCalls(then) && !containsFunctionCalls(elze)) {
i
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 1245490fd..92ae31535 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -9,6 +9,7 @@ import purescala.Common.Identifier
import java.util.concurrent.atomic.AtomicBoolean
case class SynthesisContext(
+ context: LeonContext,
options: SynthesizerOptions,
functionContext: Option[FunDef],
program: Program,
@@ -20,6 +21,7 @@ case class SynthesisContext(
object SynthesisContext {
def fromSynthesizer(synth: Synthesizer) = {
SynthesisContext(
+ synth.context,
synth.options,
synth.functionContext,
synth.program,
diff --git a/src/main/scala/leon/synthesis/SynthesizerOptions.scala b/src/main/scala/leon/synthesis/SynthesizerOptions.scala
index e9d2f4c94..647e4049d 100644
--- a/src/main/scala/leon/synthesis/SynthesizerOptions.scala
+++ b/src/main/scala/leon/synthesis/SynthesizerOptions.scala
@@ -2,11 +2,16 @@ package leon
package synthesis
case class SynthesizerOptions(
- generateDerivationTrees: Boolean = false,
- filterFuns: Option[Set[String]] = None,
- searchWorkers: Int = 1,
- firstOnly: Boolean = false,
- timeoutMs: Option[Long] = None,
- costModel: CostModel = CostModel.default,
- cegisGenerateFunCalls: Boolean = false
+ generateDerivationTrees: Boolean = false,
+ filterFuns: Option[Set[String]] = None,
+ searchWorkers: Int = 1,
+ firstOnly: Boolean = false,
+ timeoutMs: Option[Long] = None,
+ costModel: CostModel = CostModel.default,
+
+ // Cegis related options
+ cegisGenerateFunCalls: Boolean = false,
+ cegisUseCETests: Boolean = true,
+ cegisUseCEPruning: Boolean = true,
+ cegisUseBPaths: Boolean = true
)
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 0be347929..2cb41ef38 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -8,6 +8,9 @@ import purescala.Definitions._
import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
+import purescala.ScalaPrinter
+
+import evaluators._
import solvers.z3.FairZ3Solver
@@ -15,10 +18,14 @@ case object CEGIS extends Rule("CEGIS") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
// CEGIS Flags to actiave or de-activate features
- val useCounterExamples = false
+ val useCEAsserts = false
val useUninterpretedProbe = false
val useUnsatCores = true
val useFunGenerators = sctx.options.cegisGenerateFunCalls
+ val useBPaths = sctx.options.cegisUseBPaths
+ val useCETests = sctx.options.cegisUseCETests
+ val useCEPruning = sctx.options.cegisUseCEPruning
+ val evaluator = new CodeGenEvaluator(sctx.context, sctx.program)
case class Generator(tpe: TypeTree, altBuilder: () => List[(Expr, Set[Identifier])]);
@@ -83,7 +90,17 @@ case object CEGIS extends Rule("CEGIS") {
false
}
- isSubtypeOf(fd.returnType, t) && !isRecursiveCall
+ val isNotSynthesizable = fd.body match {
+ case Some(b) =>
+ collectChooses(b).isEmpty
+
+ case None =>
+ false
+ }
+
+
+
+ isSubtypeOf(fd.returnType, t) && !isRecursiveCall && isNotSynthesizable
}
sctx.program.definedFunctions.filter(isCandidate).map{ fd =>
@@ -96,58 +113,255 @@ case object CEGIS extends Rule("CEGIS") {
}
}
- class TentativeFormula(val pathcond: Expr,
- val phi: Expr,
- var program: Expr,
- var mappings: Map[Identifier, (Identifier, Expr)],
- var recTerms: Map[Identifier, Set[Identifier]]) {
+ class NonDeterministicProgram(val p: Problem,
+ val initGuard: Identifier) {
+
+ //var program: Expr = BooleanLiteral(true)
+
+ // b -> (c, ex) means the clause b => c == ex
+ var mappings: Map[Identifier, (Identifier, Expr)] = Map()
+
+ // b -> Set(c1, c2) means c1 and c2 are uninterpreted behing b, requires b to be closed
+ private var guardedTerms: Map[Identifier, Set[Identifier]] = Map(initGuard -> p.xs.toSet)
+
+
+ def isBClosed(b: Identifier) = guardedTerms.contains(b)
+
+ // b -> Map(c1 -> Set(b2, b3), c2 -> Set(b4, b5)) means b protects c1 (with sub alternatives b2/b3), and c2 (with sub b4/b5)
+ private var bTree = Map[Identifier, Map[Identifier, Set[Identifier]]]( initGuard -> p.xs.map(_ -> Set[Identifier]()).toMap)
+
+ // Returns all possible assignments to Bs in order to enumerate all possible programs
+ def allPrograms(): Set[Set[Identifier]] = {
+ def allChildPaths(b: Identifier): Stream[Set[Identifier]] = {
+ if (isBClosed(b)) {
+ Stream.empty
+ } else {
+ bTree.get(b) match {
+ case Some(cToBs) =>
+ val streams = cToBs.values.map { children =>
+ children.toStream.flatMap(c => allChildPaths(c).map(l => l + b))
+ }
+
+ streams.reduceLeft{ (s1: Stream[Set[Identifier]], s2: Stream[Set[Identifier]]) => for(p1 <- s1; p2 <- s2) yield { p1 ++ p2 } }
+ case None =>
+ Stream.cons(Set(b), Stream.empty)
+ }
+ }
+ }
+
+ allChildPaths(initGuard).toSet
+ }
+
+ /*
+ * Compilation/Execution of programs
+ */
+
+ // b1 => c == F(c2, c3) OR b2 => c == F(c4, c5) is represented here as c -> Set(c2, c3, c4, c5)
+ private var cChildren: Map[Identifier, Set[Identifier]] = Map().withDefaultValue(Set())
+
+
+ private var triedCompilation = false
+ private var progEvaluator: Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = None
+
+ def canTest() = {
+ if (!triedCompilation) {
+ progEvaluator = compile()
+ }
+
+ progEvaluator.isDefined
+ }
+
+ private var bssOrdered: Seq[Identifier] = Seq()
+
+ def testForProgram(bss: Set[Identifier])(ins: Seq[Expr]): Boolean = {
+ if (canTest()) {
+ val bssValues : Seq[Expr] = bssOrdered.map(i => BooleanLiteral(bss(i)))
+
+ val evalResult = progEvaluator.get.apply(bssValues, ins)
+
+ evalResult match {
+ case EvaluationSuccessful(res) =>
+ res == BooleanLiteral(true)
+
+ case EvaluationError(err) =>
+ sctx.reporter.error("Error testing CE: "+err)
+ true
+
+ case EvaluationFailure(err) =>
+ sctx.reporter.error("Error testing CE: "+err)
+ true
+ }
+ } else {
+ true
+ }
+ }
+
+ def compile(): Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = {
+ var unreachableCs: Set[Identifier] = guardedTerms.flatMap(_._2).toSet
+
+ val cToExprs = mappings.groupBy(_._2._1).map {
+ case (c, maps) =>
+ // We only keep cases within the current unrolling closedBs
+ val cases = maps.flatMap{ case (b, (_, ex)) => if (isBClosed(b)) None else Some(b -> ex) }
+
+ // We compute the IF expression corresponding to each c
+ val ifExpr = if (cases.isEmpty) {
+ // This can happen with ADTs with only cases with arguments
+ Error("No valid clause available").setType(c.getType)
+ } else {
+ cases.tail.foldLeft(cases.head._2) {
+ case (elze, (b, then)) => IfExpr(Variable(b), then, elze)
+ }
+ }
+
+ c -> ifExpr
+ } toMap
+
+ // Map each x generated by the program to fresh xs passed as argument
+ val newXs = p.xs.map(x => x -> FreshIdentifier(x.name, true).setType(x.getType))
+
+ val baseExpr = p.phi
+
+ bssOrdered = bss.toSeq.sortBy(_.id)
+
+ var res = baseExpr
+
+ def composeWith(c: Identifier) {
+ cToExprs.get(c) match {
+ case Some(value) =>
+ res = Let(c, cToExprs(c), res)
+ case None =>
+ res = Let(c, Error("No value available").setType(c.getType), res)
+ }
+
+ for (dep <- cChildren(c) if !unreachableCs(dep)) {
+ composeWith(dep)
+ }
+
+ }
+
+ for (c <- p.xs) {
+ composeWith(c)
+ }
+
+ val simplerRes = simplifyLets(res)
+
+ // println("COMPILATION RESULT: ")
+ // println(ScalaPrinter(simplerRes))
+ // println("BSS: "+bssOrdered)
+ // println("FREE: "+variablesOf(simplerRes))
+
+ def compileWithArray(): Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = {
+ val ba = FreshIdentifier("bssArray").setType(ArrayType(BooleanType))
+ val bav = Variable(ba)
+ val substMap : Map[Expr,Expr] = (bssOrdered.zipWithIndex.map {
+ case (b,i) => Variable(b) -> ArraySelect(bav, IntLiteral(i)).setType(BooleanType)
+ }).toMap
+ val forArray = replace(substMap, simplerRes)
+
+ // println("FORARRAY RESULT: ")
+ // println(ScalaPrinter(forArray))
+ // println("FREE: "+variablesOf(simplerRes))
+
+ // We trust arrays to be fast...
+ // val simple = evaluator.compile(simplerRes, bssOrdered ++ p.as)
+ val eval = evaluator.compile(forArray, ba +: p.as)
+
+ eval.map{e => { case (bss, ins) =>
+ e(FiniteArray(bss).setType(ArrayType(BooleanType)) +: ins)
+ }}
+ }
+
+ def compileWithArgs(): Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = {
+ val eval = evaluator.compile(simplerRes, bssOrdered ++ p.as)
+
+ eval.map{e => { case (bss, ins) =>
+ e(bss ++ ins)
+ }}
+ }
+
+ triedCompilation = true
+
+ val localVariables = bss.size + cToExprs.size + p.as.size
+
+ if (localVariables < 128) {
+ compileWithArgs().orElse(compileWithArray())
+ } else {
+ compileWithArray()
+ }
+ }
+
+ def determinize(bss: Set[Identifier]): Expr = {
+ val cClauses = mappings.filterKeys(bss).map(_._2).toMap
+
+ def getCValue(c: Identifier): Expr = {
+ val map = for (dep <- cChildren(c) if cClauses contains dep) yield {
+ dep -> getCValue(dep)
+ }
+
+ substAll(map.toMap, cClauses(c))
+ }
+
+ Tuple(p.xs.map(c => getCValue(c))).setType(TupleType(p.xs.map(_.getType)))
+
+ }
def unroll: (List[Expr], Set[Identifier]) = {
- var newClauses = List[Expr]()
- var newRecTerms = Map[Identifier, Set[Identifier]]()
- var newMappings = Map[Identifier, (Identifier, Expr)]()
+ var newClauses = List[Expr]()
+ var newGuardedTerms = Map[Identifier, Set[Identifier]]()
+ var newMappings = Map[Identifier, (Identifier, Expr)]()
+
+ for ((parentGuard, recIds) <- guardedTerms; recId <- recIds) {
- for ((_, recIds) <- recTerms; recId <- recIds) {
val gen = getGenerator(recId.getType)
+
val alts = gen.altBuilder() ::: inputAlternatives(recId.getType) ::: funcAlternatives(recId.getType)
- val altsWithBranches = alts.map(alt => FreshIdentifier("b", true).setType(BooleanType) -> alt)
+ val altsWithBranches = alts.map(alt => FreshIdentifier("B", true).setType(BooleanType) -> alt)
- val bvs = altsWithBranches.map(alt => Variable(alt._1))
- val distinct = if (bvs.size > 1) {
- (for (i <- (1 to bvs.size-1); j <- 0 to i-1) yield {
- Or(Not(bvs(i)), Not(bvs(j)))
- }).toList
- } else {
- List(BooleanLiteral(true))
+ val bvs = altsWithBranches.map(alt => Variable(alt._1))
+
+ val failedPath = Not(Variable(parentGuard))
+
+ val distinct = bvs.combinations(2).collect {
+ case List(a, b) =>
+ Or(Not(a) :: Not(b) :: Nil)
}
- val pre = And(Or(bvs) :: distinct) // (b1 OR b2) AND (Not(b1) OR Not(b2))
+
+ val pre = And(Seq(Or(failedPath :: bvs), Implies(failedPath, And(bvs.map(Not(_))))) ++ distinct)
+
val cases = for((bid, (ex, rec)) <- altsWithBranches.toList) yield { // b1 => E(gen1, gen2) [b1 -> {gen1, gen2}]
if (!rec.isEmpty) {
- newRecTerms += bid -> rec
+ newGuardedTerms += bid -> rec
+ cChildren += recId -> (cChildren(recId) ++ rec)
}
- newMappings += bid -> (recId -> ex)
+
+ newMappings += bid -> (recId -> ex)
Implies(Variable(bid), Equals(Variable(recId), ex))
}
+ val newBIds = altsWithBranches.map(_._1).toSet
+ bTree += parentGuard -> (bTree.getOrElse(parentGuard, Map()) + (recId -> newBIds))
+
newClauses = newClauses ::: pre :: cases
}
- program = And(program :: newClauses)
+ //program = And(program :: newClauses)
mappings = mappings ++ newMappings
- recTerms = newRecTerms
+ guardedTerms = newGuardedTerms
+
+ // Finally, we reset the state of the evalautor
+ triedCompilation = false
+ progEvaluator = None
- (newClauses, newRecTerms.keySet)
+ (newClauses, newGuardedTerms.keySet)
}
- def bounds = recTerms.keySet.map(id => Not(Variable(id))).toList
def bss = mappings.keySet
- def css : Set[Identifier] = mappings.values.map(_._1).toSet ++ recTerms.flatMap(_._2)
-
- def entireFormula = And(pathcond :: phi :: program :: bounds)
+ def css : Set[Identifier] = mappings.values.map(_._1).toSet ++ guardedTerms.flatMap(_._2)
}
val TopLevelAnds(ands) = p.phi
@@ -158,51 +372,121 @@ case object CEGIS extends Rule("CEGIS") {
val (exprsA, others) = ands.partition(e => (variablesOf(e) & xsSet).isEmpty)
if (exprsA.isEmpty) {
val res = new RuleInstantiation(p, this, SolutionBuilder.none) {
- def apply(sctx: SynthesisContext) = {
+ def apply(sctx: SynthesisContext): RuleApplicationResult = {
var result: Option[RuleApplicationResult] = None
var ass = p.as.toSet
var xss = p.xs.toSet
- val unrolling = new TentativeFormula(p.pc, p.phi, BooleanLiteral(true), Map(), Map() ++ p.xs.map(x => x -> Set(x)))
+ val initGuard = FreshIdentifier("START", true).setType(BooleanType)
+
+ val ndProgram = new NonDeterministicProgram(p, initGuard)
var unrolings = 0
val maxUnrolings = 3
- var predicates: Seq[Expr] = Seq()
-
val mainSolver: FairZ3Solver = sctx.solver.asInstanceOf[FairZ3Solver]
+ var exampleInputs = Set[Seq[Expr]]()
+
+ // We populate the list of examples with a predefined one
+ if (p.pc == BooleanLiteral(true)) {
+ exampleInputs += p.as.map(a => simplestValue(a.getType))
+ } else {
+ val solver = mainSolver.getNewSolver
+
+ solver.assertCnstr(p.pc)
+
+ solver.check match {
+ case Some(true) =>
+ val model = solver.getModel
+ exampleInputs += p.as.map(a => model.getOrElse(a, simplestValue(a.getType)))
+
+ case Some(false) =>
+ return RuleApplicationImpossible
+
+ case None =>
+ sctx.reporter.warning("Solver could not solve path-condition")
+ return RuleApplicationImpossible // This is not necessary though, but probably wanted
+ }
+ }
+
+ // Keep track of collected cores to filter programs to test
+ var collectedCores = Set[Set[Identifier]]()
+
// solver1 is used for the initial SAT queries
- val solver1 = mainSolver.getNewSolver
- solver1.assertCnstr(And(p.pc, p.phi))
+ var solver1 = mainSolver.getNewSolver
+ solver1.assertCnstr(And(p.pc :: p.phi :: Variable(initGuard) :: Nil))
- // solver2 is used for the CE search
+ // solver2 is used for validating a candidate program, or finding new inputs
val solver2 = mainSolver.getNewSolver
- solver2.assertCnstr(And(p.pc :: Not(p.phi) :: Nil))
+ solver2.assertCnstr(And(p.pc :: Not(p.phi) :: Variable(initGuard) :: Nil))
+
+
+ var allClauses = List[Expr]()
try {
do {
- val (clauses, bounds) = unrolling.unroll
+ var needMoreUnrolling = false
+
+ // Compute all programs that have not been excluded yet
+ var allPrograms: Set[Set[Identifier]] = if (useCEPruning) {
+ ndProgram.allPrograms.filterNot(p => collectedCores.exists(c => c.subsetOf(p)))
+ } else {
+ Set()
+ }
+
+ //println("Programs: "+allPrograms.size)
+ //println("CEs: "+exampleInputs.size)
+
+ // We further filter the set of working programs to remove those that fail on known examples
+ if (useCEPruning && !exampleInputs.isEmpty && ndProgram.canTest()) {
+ //for (ce <- exampleInputs) {
+ // println("CE: "+ce)
+ //}
+
+ for (p <- allPrograms) {
+ if (!exampleInputs.forall(ndProgram.testForProgram(p))) {
+ // This program failed on at least one example
+ solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
+ allPrograms -= p
+ }
+ }
+
+ if (allPrograms.isEmpty) {
+ needMoreUnrolling = true
+ }
+
+ //println("Passing tests: "+allPrograms.size)
+ }
+
+ //allPrograms.foreach { p =>
+ // println("PATH: "+p)
+ // println("CLAUSES: "+p.flatMap( b => ndProgram.mappings.get(b).map{ case (c, ex) => c+" = "+ex}).mkString(" && "))
+ //}
+
+ val (clauses, closedBs) = ndProgram.unroll
//println("UNROLLING: ")
//for (c <- clauses) {
// println(" - " + c)
//}
- //println("BOUNDS "+bounds)
+ //println("CLOSED Bs "+closedBs)
val clause = And(clauses)
+ allClauses = clause :: allClauses
+
solver1.assertCnstr(clause)
solver2.assertCnstr(clause)
val tpe = TupleType(p.xs.map(_.getType))
- val bss = unrolling.bss
+ val bss = ndProgram.bss
- var continue = !clauses.isEmpty
+ if (clauses.isEmpty) {
+ needMoreUnrolling = true
+ }
- while (result.isEmpty && continue && !sctx.shouldStop.get) {
- //println("Looking for CE...")
- //println("-"*80)
+ while (result.isEmpty && !needMoreUnrolling && !sctx.shouldStop.get) {
- solver1.checkAssumptions(bounds.map(id => Not(Variable(id)))) match {
+ solver1.checkAssumptions(closedBs.map(id => Not(Variable(id)))) match {
case Some(true) =>
val satModel = solver1.getModel
@@ -211,80 +495,120 @@ case object CEGIS extends Rule("CEGIS") {
case BooleanLiteral(false) => Not(Variable(b))
})
+ //println("CEGIS OUT!")
//println("Found solution: "+bssAssumptions)
- //println("#"*80)
- solver2.checkAssumptions(bssAssumptions) match {
- case Some(true) =>
- //println("#"*80)
- val invalidModel = solver2.getModel
-
- val fixedAss = And(ass.collect {
- case a if invalidModel contains a => Equals(Variable(a), invalidModel(a))
- }.toSeq)
-
- solver1.push()
- solver1.assertCnstr(fixedAss)
- //println("Found counter example: "+fixedAss)
-
- val unsatCore = if (useUnsatCores) {
- solver1.checkAssumptions(bssAssumptions) match {
- case Some(false) =>
- // Core might be empty if unrolling level is
- // insufficient, it becomes unsat no matter what
- // the assumptions are.
- solver1.getUnsatCore
- case _ =>
- bssAssumptions
+ //bssAssumptions.collect { case Variable(b) => ndProgram.mappings(b) }.foreach {
+ // case (c, ex) =>
+ // println(". "+c+" = "+ex)
+ //}
+
+ val validateWithZ3 = if (useCETests && !exampleInputs.isEmpty && ndProgram.canTest()) {
+
+ val p = bssAssumptions.collect { case Variable(b) => b }
+
+ if (exampleInputs.forall(ndProgram.testForProgram(p))) {
+ // All valid inputs also work with this, we need to
+ // make sure by validating this candidate with z3
+ true
+ } else {
+ // One valid input failed with this candidate, we can skip
+ solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
+ false
+ }
+ } else {
+ // No inputs or capability to test, we need to ask Z3
+ true
+ }
+
+ if (validateWithZ3) {
+ solver2.checkAssumptions(bssAssumptions) match {
+ case Some(true) =>
+ //println("#"*80)
+ val invalidModel = solver2.getModel
+
+ val fixedAss = And(ass.collect {
+ case a if invalidModel contains a => Equals(Variable(a), invalidModel(a))
+ }.toSeq)
+
+ val newCE = p.as.map(valuateWithModel(invalidModel))
+
+ exampleInputs += newCE
+
+ //println("Found counter example: "+fixedAss)
+
+ // Retest whether the newly found C-E invalidates all programs
+ if (useCEPruning && ndProgram.canTest) {
+ if (allPrograms.forall(p => !ndProgram.testForProgram(p)(newCE))) {
+ // println("I found a killer example!")
+ needMoreUnrolling = true
+ }
}
- } else {
- bssAssumptions
- }
-
- solver1.pop()
-
- if (unsatCore.isEmpty) {
- continue = false
- } else {
- if (useCounterExamples) {
- val freshCss = unrolling.css.map(c => c -> Variable(FreshIdentifier(c.name, true).setType(c.getType))).toMap
- val ceIn = ass.collect {
- case id if invalidModel contains id => id -> invalidModel(id)
+
+ val unsatCore = if (useUnsatCores) {
+ solver1.push()
+ solver1.assertCnstr(fixedAss)
+
+ val core = solver1.checkAssumptions(bssAssumptions) match {
+ case Some(false) =>
+ // Core might be empty if unrolling level is
+ // insufficient, it becomes unsat no matter what
+ // the assumptions are.
+ solver1.getUnsatCore
+
+ case _ =>
+ bssAssumptions
}
- val ceMap = (freshCss ++ ceIn)
+ solver1.pop()
+
+ collectedCores += core.collect{ case Variable(id) => id }
+
+ core
+ } else {
+ bssAssumptions
+ }
+
+ if (unsatCore.isEmpty) {
+ needMoreUnrolling = true
+ } else {
+ //if (useCEAsserts) {
+ // val freshCss = ndProgram.css.map(c => c -> Variable(FreshIdentifier(c.name, true).setType(c.getType))).toMap
+ // val ceIn = ass.collect {
+ // case id if invalidModel contains id => id -> invalidModel(id)
+ // }
- val counterexample = substAll(ceMap, And(Seq(unrolling.program, unrolling.phi)))
+ // val ceMap = (freshCss ++ ceIn)
- //val And(ands) = counterexample
- //println("CE:")
- //for (a <- ands) {
- // println(" - "+a)
+ // val counterexample = substAll(ceMap, And(Seq(ndProgram.program, p.phi)))
+
+ // //val And(ands) = counterexample
+ // //println("CE:")
+ // //for (a <- ands) {
+ // // println(" - "+a)
+ // //}
+
+ // solver1.assertCnstr(counterexample)
//}
- solver1.assertCnstr(counterexample)
+ solver1.assertCnstr(Not(And(unsatCore.toSeq)))
}
- solver1.assertCnstr(Not(And(unsatCore.toSeq)))
- }
-
- case Some(false) =>
- var mapping = unrolling.mappings.filterKeys(satModel.mapValues(_ == BooleanLiteral(true))).values.toMap
+ case Some(false) =>
- // Resolve mapping
- for ((c, e) <- mapping) {
- mapping += c -> substAll(mapping, e)
- }
+ val expr = ndProgram.determinize(satModel.filter(_._2 == BooleanLiteral(true)).keySet)
- result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(mapping))).setType(tpe))))
+ result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), expr)))
- case _ =>
- if (!sctx.shouldStop.get) {
- sctx.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
- }
- continue = false
+ case _ =>
+ if (!sctx.shouldStop.get) {
+ sctx.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
+ }
+ needMoreUnrolling = true
+ }
}
+
case Some(false) =>
//println("%%%% UNSAT")
@@ -298,11 +622,14 @@ case object CEGIS extends Rule("CEGIS") {
}
}
- continue = false
+ needMoreUnrolling = true
case _ =>
+ if (!sctx.shouldStop.get) {
+ sctx.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
+ }
//println("%%%% WOOPS")
- continue = false
+ needMoreUnrolling = true
}
}
diff --git a/src/main/scala/leon/synthesis/utils/Benchmarks.scala b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
index 15ebc81e6..8cb4c5fa7 100644
--- a/src/main/scala/leon/synthesis/utils/Benchmarks.scala
+++ b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
@@ -87,6 +87,7 @@ object Benchmarks extends App {
for ((f, ps) <- results.toSeq.sortBy(_._1.id.toString); p <- ps) {
val sctx = SynthesisContext(
+ context = ctx,
options = opts,
functionContext = Some(f),
program = program,
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 36edcf9f0..4fe7228d1 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -175,7 +175,6 @@ class EvaluatorsTests extends FunSuite {
|""".stripMargin
implicit val prog = parseString(p)
-
val evaluators = prepareEvaluators
for(e <- evaluators) {
@@ -211,7 +210,6 @@ class EvaluatorsTests extends FunSuite {
|}""".stripMargin
implicit val prog = parseString(p)
-
val evaluators = prepareEvaluators
for(e <- evaluators) {
@@ -274,7 +272,6 @@ class EvaluatorsTests extends FunSuite {
|}""".stripMargin
implicit val prog = parseString(p)
-
val evaluators = prepareEvaluators
val nil = mkCaseClass("Nil")
@@ -316,7 +313,6 @@ class EvaluatorsTests extends FunSuite {
|}""".stripMargin
implicit val prog = parseString(p)
-
val evaluators = prepareEvaluators
val nil = mkCaseClass("Nil")
@@ -362,7 +358,6 @@ class EvaluatorsTests extends FunSuite {
|}""".stripMargin
implicit val prog = parseString(p)
-
val evaluators = prepareEvaluators
val cons1223 = mkCaseClass("PCons", IL(1), IL(2), mkCaseClass("PCons", IL(2), IL(3), mkCaseClass("PNil")))
@@ -379,6 +374,31 @@ class EvaluatorsTests extends FunSuite {
}
}
+ test("Arrays") {
+ val p = """|object Program {
+ | def boolArrayRead(bools : Array[Boolean], index : Int) : Boolean = bools(index)
+ |
+ | def intArrayRead(bools : Array[Int], index : Int) : Int = bools(index)
+ |}
+ |""".stripMargin
+
+ implicit val progs = parseString(p)
+ val evaluators = prepareEvaluators
+
+ val ba = FiniteArray(Seq(T, F)).setType(ArrayType(BooleanType))
+ val ia = FiniteArray(Seq(IL(41), IL(42), IL(43))).setType(ArrayType(Int32Type))
+
+ for(e <- evaluators) {
+ checkComp(e, mkCall("boolArrayRead", ba, IL(0)), T)
+ checkComp(e, mkCall("boolArrayRead", ba, IL(1)), F)
+ checkComp(e, mkCall("intArrayRead", ia, IL(0)), IL(41))
+ checkComp(e, mkCall("intArrayRead", ia, IL(1)), IL(42))
+ checkComp(e, ArrayLength(ia), IL(3))
+
+ checkError(e, mkCall("boolArrayRead", ba, IL(2)))
+ }
+ }
+
test("Misc") {
val p = """|object Program {
| import leon.Utils._
@@ -388,7 +408,6 @@ class EvaluatorsTests extends FunSuite {
|""".stripMargin
implicit val prog = parseString(p)
-
val evaluators = prepareEvaluators
for(e <- evaluators) {
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 96d7104d7..567d30abb 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -44,7 +44,7 @@ class SynthesisSuite extends FunSuite {
for ((f, ps) <- results; p <- ps) {
test("Synthesizing %3d: %-20s [%s]".format(nextInt(), f.id.toString, title)) {
- val sctx = SynthesisContext(opts, Some(f), program, solver, new DefaultReporter, new java.util.concurrent.atomic.AtomicBoolean)
+ val sctx = SynthesisContext(ctx, opts, Some(f), program, solver, new DefaultReporter, new java.util.concurrent.atomic.AtomicBoolean)
block(sctx, f, p)
}
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index f5b33c3e2..e590093cc 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -79,7 +79,6 @@ class XLangVerificationRegression extends FunSuite {
assert(report.totalConditions === report.totalValid,
"All verification conditions ("+report.totalConditions+") should be valid.")
assert(reporter.errorCount === 0)
- assert(reporter.warningCount === 0)
}
forEachFileIn("invalid") { output =>
@@ -89,7 +88,6 @@ class XLangVerificationRegression extends FunSuite {
assert(report.totalUnknown === 0,
"There should not be unknown verification conditions.")
assert(reporter.errorCount >= report.totalInvalid)
- assert(reporter.warningCount === 0)
}
forEachFileIn("error", true) { output => () }
--
GitLab