diff --git a/src/main/scala/leon/codegen/CodeGenParams.scala b/src/main/scala/leon/codegen/CodeGenParams.scala index ff99627659ddd7ef26b736f245d702d70e0318c2..61dc94719447fab828e5ac22cbade5afdb89aa97 100644 --- a/src/main/scala/leon/codegen/CodeGenParams.scala +++ b/src/main/scala/leon/codegen/CodeGenParams.scala @@ -6,7 +6,7 @@ package codegen case class CodeGenParams ( maxFunctionInvocations: Int, // Monitor calls and abort execution if more than X calls checkContracts: Boolean, // Generate calls that checks pre/postconditions - doInstrument: Boolean // Instrument reads to case classes (mainly for vanuatoo) + doInstrument: Boolean // Instrument reads to case classes ) { val recordInvocations = maxFunctionInvocations > -1 diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala deleted file mode 100644 index 6e13cb030ad7df32b6a5ec1543e6d2c80915903d..0000000000000000000000000000000000000000 --- a/src/main/scala/leon/datagen/VanuatooDataGen.scala +++ /dev/null @@ -1,409 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon -package datagen - -import purescala.Common._ -import purescala.Definitions._ -import purescala.ExprOps._ -import purescala.Expressions._ -import purescala.Types._ -import purescala.Extractors._ -import purescala.Constructors._ - -import codegen.CompilationUnit -import codegen.CodeGenParams -import codegen.runtime.StdMonitor -import vanuatoo.{Pattern => VPattern, _} - -import evaluators._ - -class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator { - val unit = new CompilationUnit(ctx, p, CodeGenParams.default.copy(doInstrument = true)) - - val ints = (for (i <- Set(0, 1, 2, 3)) yield { - i -> Constructor[Expr, TypeTree](List(), Int32Type, s => IntLiteral(i), ""+i) - }).toMap - - val bigInts = (for (i <- Set(0, 1, 2, 3)) yield { - i -> Constructor[Expr, TypeTree](List(), IntegerType, s => InfiniteIntegerLiteral(i), ""+i) - }).toMap - - val booleans = (for (b <- Set(true, false)) yield { - b -> Constructor[Expr, TypeTree](List(), BooleanType, s => BooleanLiteral(b), ""+b) - }).toMap - - val chars = (for (c <- Set('a', 'b', 'c', 'd')) yield { - c -> Constructor[Expr, TypeTree](List(), CharType, s => CharLiteral(c), ""+c) - }).toMap - - val rationals = (for (n <- Set(0, 1, 2, 3); d <- Set(1,2,3,4)) yield { - (n, d) -> Constructor[Expr, TypeTree](List(), RealType, s => FractionalLiteral(n, d), "" + n + "/" + d) - }).toMap - - val strings = (for (b <- Set("", "a", "foo", "bar")) yield { - b -> Constructor[Expr, TypeTree](List(), StringType, s => StringLiteral(b), b) - }).toMap - - - def intConstructor(i: Int) = ints(i) - - def bigIntConstructor(i: Int) = bigInts(i) - - def boolConstructor(b: Boolean) = booleans(b) - - def charConstructor(c: Char) = chars(c) - - def rationalConstructor(n: Int, d: Int) = rationals(n -> d) - - def stringConstructor(s: String) = strings(s) - - lazy val stubValues = ints.values ++ bigInts.values ++ booleans.values ++ chars.values ++ rationals.values ++ strings.values - - def cPattern(c: Constructor[Expr, TypeTree], args: Seq[VPattern[Expr, TypeTree]]) = { - ConstructorPattern[Expr, TypeTree](c, args) - } - - private var constructors = Map[TypeTree, List[Constructor[Expr, TypeTree]]]() - - private def getConstructorFor(t: CaseClassType, act: AbstractClassType): Constructor[Expr, TypeTree] = { - // We "up-cast" the returnType of the specific caseclass generator to match its superclass - getConstructors(t).head.copy(retType = act) - } - - private def getConstructors(t: TypeTree): List[Constructor[Expr, TypeTree]] = t match { - case UnitType => - constructors.getOrElse(t, { - val cs = List(Constructor[Expr, TypeTree](List(), t, s => UnitLiteral(), "()")) - constructors += t -> cs - cs - }) - - case at @ ArrayType(sub) => - constructors.getOrElse(at, { - val cs = for (size <- List(0, 1, 2, 5)) yield { - Constructor[Expr, TypeTree]( - (1 to size).map(i => sub).toList, - at, - s => finiteArray(s, None, sub), - at.asString(ctx)+"@"+size - ) - } - constructors += at -> cs - cs - }) - - case st @ SetType(sub) => - constructors.getOrElse(st, { - val cs = for (size <- List(0, 1, 2, 5)) yield { - Constructor[Expr, TypeTree]( - (1 to size).map(i => sub).toList, - st, - s => FiniteSet(s.toSet, sub), - st.asString(ctx)+"@"+size - ) - } - constructors += st -> cs - cs - }) - - case bt @ BagType(sub) => - constructors.getOrElse(bt, { - val cs = for (size <- List(0, 1, 2, 5)) yield { - val subs = (1 to size).flatMap(i => List(sub, IntegerType)).toList - Constructor[Expr, TypeTree](subs, bt, s => FiniteBag(s.grouped(2).map { - case Seq(k, i @ InfiniteIntegerLiteral(v)) => - k -> (if (v > 0) i else InfiniteIntegerLiteral(-v + 1)) - }.toMap, sub), bt.asString(ctx)+"@"+size) - } - constructors += bt -> cs - cs - }) - - case tt @ TupleType(parts) => - constructors.getOrElse(tt, { - val cs = List(Constructor[Expr, TypeTree](parts, tt, s => tupleWrap(s), tt.asString(ctx))) - constructors += tt -> cs - cs - }) - - case mt @ MapType(from, to) => - constructors.getOrElse(mt, { - val cs = for (size <- List(0, 1, 2, 5)) yield { - val subs = (1 to size).flatMap(i => List(from, to)).toList - Constructor[Expr, TypeTree](subs, mt, s => FiniteMap(s.grouped(2).map(t => (t(0), t(1))).toMap, from, to), mt.asString(ctx)+"@"+size) - } - constructors += mt -> cs - cs - }) - - case ft @ FunctionType(from, to) => - constructors.getOrElse(ft, { - val cs = for (size <- List(1, 2, 3, 5)) yield { - val subs = (1 to size).flatMap(_ => from :+ to).toList - Constructor[Expr, TypeTree](subs, ft, { s => - val grouped = s.grouped(from.size + 1).toSeq - val mapping = grouped.init.map { case args :+ res => (args -> res) } - FiniteLambda(mapping, grouped.last.last, ft) - }, ft.asString(ctx) + "@" + size) - } - constructors += ft -> cs - cs - }) - - case tp: TypeParameter => - constructors.getOrElse(tp, { - val cs = for (i <- List(1, 2)) yield { - Constructor[Expr, TypeTree](List(), tp, s => GenericValue(tp, i), tp.id+"#"+i) - } - constructors += tp -> cs - cs - }) - - case act: AbstractClassType => - constructors.getOrElse(act, { - val cs = act.knownCCDescendants.map { - cct => getConstructorFor(cct, act) - }.toList - - constructors += act -> cs - - cs - }) - - case cct: CaseClassType => - constructors.getOrElse(cct, { - val c = List(Constructor[Expr, TypeTree](cct.fieldsTypes, cct, s => CaseClass(cct, s), cct.id.name)) - constructors += cct -> c - c - }) - - case _ => - ctx.reporter.error("Unknown type to generate constructor for: "+t) - Nil - } - - // Returns the pattern and whether it is fully precise - private def valueToPattern(v: AnyRef, expType: TypeTree): (VPattern[Expr, TypeTree], Boolean) = (v, expType) match { - case (i: Integer, Int32Type) => - (cPattern(intConstructor(i), List()), true) - - case (i: Integer, IntegerType) => - (cPattern(bigIntConstructor(i), List()), true) - - case (b: java.lang.Boolean, BooleanType) => - (cPattern(boolConstructor(b), List()), true) - - case (c: java.lang.Character, CharType) => - (cPattern(charConstructor(c), List()), true) - - case (b: java.lang.String, StringType) => - (cPattern(stringConstructor(b), List()), true) - - case (cc: codegen.runtime.CaseClass, ct: ClassType) => - val r = cc.__getRead() - - unit.jvmClassToLeonClass(cc.getClass.getName) match { - case Some(ccd: CaseClassDef) => - val cct = CaseClassType(ccd, ct.tps) - val c = ct match { - case act : AbstractClassType => - getConstructorFor(cct, act) - case cct : CaseClassType => - getConstructors(cct).head - } - - val fields = cc.productElements() - - val elems = for (i <- 0 until fields.length) yield { - if (((r >> i) & 1) == 1) { - // has been read - valueToPattern(fields(i), cct.fieldsTypes(i)) - } else { - (AnyPattern[Expr, TypeTree](), false) - } - } - - (ConstructorPattern(c, elems.map(_._1)), elems.forall(_._2)) - - case _ => - ctx.reporter.error("Could not retrieve type for :"+cc.getClass.getName) - (AnyPattern[Expr, TypeTree](), false) - } - - case (t: codegen.runtime.Tuple, tpe) => - val r = t.__getRead() - - val parts = unwrapTupleType(tpe, t.getArity) - - val c = getConstructors(tpe).head - - val elems = for (i <- 0 until t.getArity) yield { - if (((r >> i) & 1) == 1) { - // has been read - valueToPattern(t.get(i), parts(i)) - } else { - (AnyPattern[Expr, TypeTree](), false) - } - } - - (ConstructorPattern(c, elems.map(_._1)), elems.forall(_._2)) - - case (gv: GenericValue, t: TypeParameter) => - (cPattern(getConstructors(t)(gv.id-1), List()), true) - - case (v, t) => - ctx.reporter.debug("Unsupported value, can't paternify : "+v+" ("+v.getClass+") : "+t) - (AnyPattern[Expr, TypeTree](), false) - } - - type InstrumentedResult = (EvaluationResults.Result[Expr], Option[vanuatoo.Pattern[Expr, TypeTree]]) - - def compile(expression: Expr, argorder: Seq[Identifier]) : Option[Expr=>InstrumentedResult] = { - import leon.codegen.runtime.LeonCodeGenRuntimeException - import leon.codegen.runtime.LeonCodeGenEvaluationException - - try { - val ttype = tupleTypeWrap(argorder.map(_.getType)) - val tid = FreshIdentifier("tup", ttype) - - val map = argorder.zipWithIndex.map{ case (id, i) => id -> tupleSelect(Variable(tid), i + 1, argorder.size) }.toMap - - val newExpr = replaceFromIDs(map, expression) - - val ce = unit.compileExpression(newExpr, Seq(tid))(ctx) - - Some((args : Expr) => { - try { - val monitor = new StdMonitor(unit, unit.params.maxFunctionInvocations, Map()) - - val jvmArgs = ce.argsToJVM(Seq(args), monitor) - - val result = ce.evalFromJVM(jvmArgs, monitor) - - // jvmArgs is getting updated by evaluating - val pattern = valueToPattern(jvmArgs.head, ttype) - - (EvaluationResults.Successful(result), if (!pattern._2) Some(pattern._1) else None) - } catch { - case e : StackOverflowError => - (EvaluationResults.RuntimeError(e.getMessage), None) - - case e : ClassCastException => - (EvaluationResults.RuntimeError(e.getMessage), None) - - case e : ArithmeticException => - (EvaluationResults.RuntimeError(e.getMessage), None) - - case e : ArrayIndexOutOfBoundsException => - (EvaluationResults.RuntimeError(e.getMessage), None) - - case e : LeonCodeGenRuntimeException => - (EvaluationResults.RuntimeError(e.getMessage), None) - - case e : LeonCodeGenEvaluationException => - (EvaluationResults.EvaluatorError(e.getMessage), None) - } - }) - } catch { - case t: Throwable => - ctx.reporter.warning("Error while compiling expression: "+t.getMessage); t.printStackTrace() - None - } - } - - def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = { - // Split conjunctions - val TopLevelAnds(ands) = satisfying - - val runners = ands.flatMap(a => compile(a, ins) match { - case Some(runner) => Some(runner) - case None => - ctx.reporter.error("Could not compile predicate " + a) - None - }) - - val gen = new StubGenerator[Expr, TypeTree](stubValues.toSeq, - Some(getConstructors _), - treatEmptyStubsAsChildless = true) - - /** - * Gather at most <n> isomoprhic models before skipping them - * - Too little means skipping many excluding patterns - * - Too large means repetitive (and not useful models) before reaching maxEnumerated - */ - - val maxIsomorphicModels = maxValid+1 - - val it = gen.enumerate(tupleTypeWrap(ins.map(_.getType))) - - new Iterator[Seq[Expr]] { - var total = 0 - var found = 0 - - var theNext: Option[Seq[Expr]] = None - - def hasNext = { - if (total == 0) { - theNext = computeNext() - } - - theNext.isDefined - } - - def next() = { - val res = theNext.get - theNext = computeNext() - res - } - - - def computeNext(): Option[Seq[Expr]] = { - //return None - while (total < maxEnumerated && found < maxValid && it.hasNext && !interrupted.get) { - val model = it.next() - it.hasNext // FIXME: required for some reason by StubGenerator or will return false during loop check - - if (model eq null) { - total = maxEnumerated - } else { - total += 1 - - var failed = false - - for (r <- runners) r(model) match { - case (EvaluationResults.Successful(BooleanLiteral(true)), _) => - - case (_, Some(pattern)) => - failed = true - it.exclude(pattern) - - case (_, None) => - failed = true; - } - - if (!failed) { - //println("Got model:") - //for ((i, v) <- (ins zip model.exprs)) { - // println(" - "+i+" -> "+v) - //} - - found += 1 - - if (found % maxIsomorphicModels == 0) { - it.skipIsomorphic() - } - - return Some(unwrapTuple(model, ins.size)) - } - - //if (total % 1000 == 0) { - // println("... "+total+" ...") - //} - } - } - None - } - } - } -} diff --git a/src/main/scala/leon/solvers/EnumerationSolver.scala b/src/main/scala/leon/solvers/EnumerationSolver.scala index 79f53ef9134a07198b8ef2c87f3deff0571e26ad..85966b0363ff8e75bce7169b96cd0ed918157c9c 100644 --- a/src/main/scala/leon/solvers/EnumerationSolver.scala +++ b/src/main/scala/leon/solvers/EnumerationSolver.scala @@ -3,6 +3,7 @@ package leon package solvers +import leon.evaluators.DefaultEvaluator import utils._ import purescala.Common._ import purescala.Definitions._ @@ -52,7 +53,7 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends def check: Option[Boolean] = { val timer = context.timers.solvers.enum.check.start() val res = try { - datagen = Some(new VanuatooDataGen(context, program)) + datagen = Some(new GrammarDataGen(new DefaultEvaluator(context, program))) if (interrupted) { None } else { diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala index 40ffc8b9b749708ded65df9a1fd7e68d6d3dd093..77829376ccdb62fb4f5bd537e1ae5d200db00a50 100644 --- a/src/main/scala/leon/synthesis/SynthesisPhase.scala +++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala @@ -21,7 +21,6 @@ object SynthesisPhase extends UnitPhase[Program] { // CEGIS options val optCEGISOptTimeout = LeonFlagOptionDef("cegis:opttimeout", "Consider a time-out of CE-search as untrusted solution", true ) - val optCEGISVanuatoo = LeonFlagOptionDef("cegis:vanuatoo", "Generate inputs using new korat-style generator", false) val optCEGISNaiveGrammar = LeonFlagOptionDef("cegis:naive", "Use the old naive grammar for CEGIS", false) val optCEGISMaxSize = LeonLongOptionDef("cegis:maxsize", "Maximum size of expressions synthesized by CEGIS", 7L, "N") @@ -29,7 +28,7 @@ object SynthesisPhase extends UnitPhase[Program] { val optSpecifyRecCalls = LeonFlagOptionDef("reccalls", "Use full value as spec for introduced recursive calls", true) override val definedOptions : Set[LeonOptionDef[Any]] = Set( - optManual, optCostModel, optDerivTrees, optCEGISOptTimeout, optCEGISVanuatoo, + optManual, optCostModel, optDerivTrees, optCEGISOptTimeout, optCEGISNaiveGrammar, optCEGISMaxSize, optSpecifyRecCalls, optAllowPartial ) @@ -63,7 +62,6 @@ object SynthesisPhase extends UnitPhase[Program] { manualSearch = ms, functions = ctx.findOption(GlobalOptions.optFunctions) map { _.toSet }, cegisUseOptTimeout = ctx.findOptionOrDefault(optCEGISOptTimeout), - cegisUseVanuatoo = ctx.findOptionOrDefault(optCEGISVanuatoo), cegisMaxSize = ctx.findOptionOrDefault(optCEGISMaxSize).toInt ) } diff --git a/src/main/scala/leon/synthesis/SynthesisSettings.scala b/src/main/scala/leon/synthesis/SynthesisSettings.scala index 5bbff9444ded17b5100b1bc5ba0c3949b7f4dc61..e7cdf0f0e0e1d7a568af599470c3a79b17b18630 100644 --- a/src/main/scala/leon/synthesis/SynthesisSettings.scala +++ b/src/main/scala/leon/synthesis/SynthesisSettings.scala @@ -17,7 +17,5 @@ case class SynthesisSettings( // Cegis related options cegisUseOptTimeout: Boolean = true, - cegisUseVanuatoo : Boolean = false, cegisMaxSize: Int = 7 - ) diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala index 41e82c459b70fa61da686a89a1041433f6a599e4..7ebf27a7d0cbf94068f3b66354d2bf722d8d3a89 100644 --- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala +++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala @@ -49,7 +49,6 @@ abstract class CEGISLike(name: String) extends Rule(name) { // CEGIS Flags to activate or deactivate features val useOptTimeout = hctx.settings.cegisUseOptTimeout - val useVanuatoo = hctx.settings.cegisUseVanuatoo // The factor by which programs need to be reduced by testing before we validate them individually val testReductionRatio = 10 @@ -795,12 +794,8 @@ abstract class CEGISLike(name: String) extends Rule(name) { if (complicated) { Iterator() } else { - if (useVanuatoo) { - new VanuatooDataGen(hctx, hctx.program).generateFor(p.as, p.pc.toClause, nTests, 3000).map(InExample) - } else { - val evaluator = new DualEvaluator(hctx, hctx.program, CodeGenParams.default) - new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc.toClause, nTests, 1000).map(InExample) - } + val evaluator = new DualEvaluator(hctx, hctx.program, CodeGenParams.default) + new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc.toClause, nTests, 1000).map(InExample) } } diff --git a/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala index ee49610d06a4070154df5bfb744925121754f054..1cfe7df1c0db2a4af4ab614f3460ded2830a2570 100644 --- a/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala +++ b/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala @@ -38,11 +38,7 @@ abstract class TEGISLike(name: String) extends Rule(name) { val nTests = if (p.pc.isEmpty) 50 else 20 - val useVanuatoo = hctx.settings.cegisUseVanuatoo - - val inputGenerator: Iterator[Seq[Expr]] = if (useVanuatoo) { - new VanuatooDataGen(hctx, hctx.program).generateFor(p.as, p.pc.toClause, nTests, 3000) - } else { + val inputGenerator: Iterator[Seq[Expr]] = { val evaluator = new DualEvaluator(hctx, hctx.program, CodeGenParams.default) new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc.toClause, nTests, 1000) } diff --git a/src/main/scala/root-doc.txt b/src/main/scala/root-doc.txt index 9f01546cc61ad0c4122a05b89fe16d4cdc3e95e4..096b42bae7200287bad4d45be9fae554b85a94dd 100644 --- a/src/main/scala/root-doc.txt +++ b/src/main/scala/root-doc.txt @@ -13,7 +13,7 @@ assume a Pure Scala only AST. - [[leon.codegen]] provides bytecode generator for Leon programs. Enable the conversion of a [[leon.purescala.Definitions.Program]] to JVM bytecode. - - [[leon.datagen]] provides a generator of expressions (trees), based on vanuatoo. + - [[leon.datagen]] provides generators of expressions (trees). - [[leon.evaluators]] implements different evaluators for Leon programs in Pure Scala. diff --git a/src/sphinx/installation.rst b/src/sphinx/installation.rst index b4deaf194eb4f84eac0b14dabb42221cfb999056..cc71615ca8076264e17a4fa24eb579844353df88 100644 --- a/src/sphinx/installation.rst +++ b/src/sphinx/installation.rst @@ -78,12 +78,11 @@ under Cygwin. *Missing jars* If running leon produces errors because it could not find -some cafebabe*.jar or vanuatoo*.jar, it is probably because +some cafebabe*.jar, it is probably because symlinks have not been resolved. If your architecture is x64, do the following: -1. Copy ``unmanaged/common/cafebabe*.jar`` to ``unmanaged/64/`` -2. Copy ``unmanaged/common/vanuatoo*.jar`` to ``unmanaged/64/`` +Copy ``unmanaged/common/cafebabe*.jar`` to ``unmanaged/64/`` You may be able to obtain additional tips on getting Leon to work on Windows from [Mikael Mayer](http://people.epfl.ch/mikael.mayer) or on [his dedicated web page](http://lara.epfl.ch/~mayer/leon/), diff --git a/src/sphinx/options.rst b/src/sphinx/options.rst index 38f18d0aef81eea7dd1006c92fda59f170b3f25e..b898a4964b08baa533f00916f6579d3aa5001b0f 100644 --- a/src/sphinx/options.rst +++ b/src/sphinx/options.rst @@ -255,10 +255,6 @@ Synthesis Shrink non-deterministic programs when tests pruning works well. -* ``--cegis:vanuatoo`` - - Generate inputs using new korat-style generator. - * ``--costmodel=cm`` Use a specific cost model for this search. diff --git a/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala index 8882238999acebde711027ec6a8b1db152813b20..b9d73779ab5abbe6ee4ba52bace0ebfcadc58dda 100644 --- a/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala +++ b/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala @@ -333,7 +333,7 @@ class CodegenEvaluatorSuite extends LeonTestSuiteWithProgram with helpers.Expres val eval = new CodeGenEvaluator(fix._1, fix._2, CodeGenParams( maxFunctionInvocations = if (requireMonitor) 1000 else -1, // Monitor calls and abort execution if more than X calls checkContracts = true, // Generate calls that checks pre/postconditions - doInstrument = doInstrument // Instrument reads to case classes (mainly for vanuatoo) + doInstrument = doInstrument // Instrument reads to case classes )) (eval.eval(fcall(name + ".test")()).result, exp) match { diff --git a/unmanaged/64/vanuatoo_2.11-0.1.jar b/unmanaged/64/vanuatoo_2.11-0.1.jar deleted file mode 100644 index 9550eb732bb464d91853cb6edc5fcedee9f8f481..0000000000000000000000000000000000000000 Binary files a/unmanaged/64/vanuatoo_2.11-0.1.jar and /dev/null differ