From 1730c4a5dceb6beaba3db4003c3757e93942dc80 Mon Sep 17 00:00:00 2001 From: Ivan Kuraj <ivan.kuraj@epfl.ch> Date: Thu, 28 Mar 2013 08:19:53 +0100 Subject: [PATCH] Changes before the submission - DataGen, benchmarks, timeout checking --- src/main/scala/lesynth/ExampleRunner.scala | 5 +- src/main/scala/lesynth/InputExamples.scala | 236 ++++++++++-------- .../scala/lesynth/SynthesizerExamples.scala | 62 ++++- ...ConditionAbductionSynthesisImmediate.scala | 2 +- .../ConditionAbductionSynthesisTwoPhase.scala | 18 +- 5 files changed, 201 insertions(+), 122 deletions(-) diff --git a/src/main/scala/lesynth/ExampleRunner.scala b/src/main/scala/lesynth/ExampleRunner.scala index f32f5c6a3..111101188 100644 --- a/src/main/scala/lesynth/ExampleRunner.scala +++ b/src/main/scala/lesynth/ExampleRunner.scala @@ -6,6 +6,7 @@ import scala.collection.mutable.{ LinkedList => MutableList } import leon.{ Main => LeonMain, DefaultReporter, Settings, LeonContext } import leon.evaluators._ +import leon.evaluators.EvaluationResults._ import leon.solvers.Solver import leon.solvers.z3.{ FairZ3Solver } import leon.verification.AnalysisPhase @@ -17,6 +18,8 @@ import leon.purescala.TreeOps import insynth.util.logging.HasLogger +import EvaluationResults._ + class ExampleRunner(program: Program, maxSteps: Int = 2000) extends HasLogger { import TreeOps._ @@ -35,7 +38,7 @@ class ExampleRunner(program: Program, maxSteps: Int = 2000) extends HasLogger { def evaluate(expr: Expr, mapping: Map[Identifier, Expr]) = { fine("to evaluate: " + expr + " for mapping: " + mapping) defaultEvaluator.eval(expr, mapping) match { - case EvaluationSuccessful(BooleanLiteral(true)) => + case Successful(BooleanLiteral(true)) => fine("Eval succeded: EvaluationSuccessful(true)") true case m => diff --git a/src/main/scala/lesynth/InputExamples.scala b/src/main/scala/lesynth/InputExamples.scala index 00fa92c27..71c9db244 100755 --- a/src/main/scala/lesynth/InputExamples.scala +++ b/src/main/scala/lesynth/InputExamples.scala @@ -9,12 +9,26 @@ import leon.purescala.TypeTrees.{ ClassType, CaseClassType, Int32Type } import leon.purescala.Trees.{ IntLiteral, CaseClass } import leon.purescala.Definitions.{ FunDef, VarDecls } import leon.purescala.Common.Identifier +import leon.evaluators.Evaluator +import leon.purescala.DataGen.findModels +import leon.synthesis.Problem import insynth.leon.loader.{ HoleExtractor, LeonLoader } object InputExamples { - - def getInputExamples(argumentIds: Seq[Identifier], loader: LeonLoader) = { + + def getDataGenInputExamples(evaluator: Evaluator, p: Problem, + numOfModels: Int, numOfTries: Int, _forcedFreeVars: Option[Seq[Identifier]]) + (argumentIds: Seq[Identifier], loader: LeonLoader) = { + + val models = findModels(p.pc, evaluator, numOfModels, numOfTries, + forcedFreeVars = _forcedFreeVars) + + models.toList + + } + + def getFixedInputExamples(argumentIds: Seq[Identifier], loader: LeonLoader) = { argumentIds match { case singleArgument :: Nil if isList(singleArgument) => introduceOneListArgumentExamples(argumentIds, loader) @@ -24,125 +38,125 @@ object InputExamples { introduceExamplesIntList(argumentIds, loader) case _ => null } - } - + } + def introduceExamplesIntList(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = { - + // list type val ct = argumentIds(1).getType.asInstanceOf[ClassType] - - val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef) - - val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0) - - val nilClass = nilClassSet.head - val consClass = consClassSet.head - - var counter = 10 - def getIntLiteral = { counter+=1; IntLiteral(counter) } - val intLiteral = IntLiteral(5) - - val list0 = CaseClass(nilClass, Nil) - val list1 = CaseClass(consClass, IntLiteral(10) :: list0 :: Nil) - val list32 = CaseClass(consClass, IntLiteral(5) :: CaseClass(consClass, IntLiteral(7) :: list1 :: Nil) :: Nil) - - Map(argumentIds(0) -> IntLiteral(3), argumentIds(1) -> list32) :: - Map(argumentIds(0) -> IntLiteral(2), argumentIds(1) -> list32) :: - Map(argumentIds(0) -> IntLiteral(3), argumentIds(1) -> list0) :: - Map(argumentIds(0) -> IntLiteral(2), argumentIds(1) -> list0) :: - Map(argumentIds(0) -> IntLiteral(6), argumentIds(1) -> list32) :: - Map(argumentIds(0) -> IntLiteral(9), argumentIds(1) -> list32) :: - Nil + + val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef) + + val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0) + + val nilClass = nilClassSet.head + val consClass = consClassSet.head + + var counter = 10 + def getIntLiteral = { counter += 1; IntLiteral(counter) } + val intLiteral = IntLiteral(5) + + val list0 = CaseClass(nilClass, Nil) + val list1 = CaseClass(consClass, IntLiteral(10) :: list0 :: Nil) + val list32 = CaseClass(consClass, IntLiteral(5) :: CaseClass(consClass, IntLiteral(7) :: list1 :: Nil) :: Nil) + + Map(argumentIds(0) -> IntLiteral(3), argumentIds(1) -> list32) :: + Map(argumentIds(0) -> IntLiteral(2), argumentIds(1) -> list32) :: + Map(argumentIds(0) -> IntLiteral(3), argumentIds(1) -> list0) :: + Map(argumentIds(0) -> IntLiteral(2), argumentIds(1) -> list0) :: + Map(argumentIds(0) -> IntLiteral(6), argumentIds(1) -> list32) :: + Map(argumentIds(0) -> IntLiteral(9), argumentIds(1) -> list32) :: + Nil } - + def introduceOneListArgumentExamples(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = { - + // list type val ct = argumentIds(0).getType.asInstanceOf[ClassType] - - val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef) - - val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0) - - val nilClass = nilClassSet.head - val consClass = consClassSet.head - - var counter = 10 - def getIntLiteral = { counter+=1; IntLiteral(counter) } - val intLiteral = IntLiteral(5) - - val list0 = CaseClass(nilClass, Nil) - val list1 = CaseClass(consClass, IntLiteral(10) :: list0 :: Nil) - val list2s = CaseClass(consClass, IntLiteral(5) :: list1 :: Nil) - val list2u = CaseClass(consClass, IntLiteral(5) :: list1 :: Nil) - val list3s = CaseClass(consClass, IntLiteral(5) :: list2s :: Nil) - val list3u1 = CaseClass(consClass, IntLiteral(5) :: list2u :: Nil) - val list3u2 = CaseClass(consClass, IntLiteral(15) :: list2s :: Nil) - val list3u3 = CaseClass(consClass, IntLiteral(15) :: list2u :: Nil) - - for (list <- List(list0, list1, list2s, list2u, list3s, list3u1, list3u2, list3u3)) - yield Map(argumentIds(0) -> list) + + val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef) + + val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0) + + val nilClass = nilClassSet.head + val consClass = consClassSet.head + + var counter = 10 + def getIntLiteral = { counter += 1; IntLiteral(counter) } + val intLiteral = IntLiteral(5) + + val list0 = CaseClass(nilClass, Nil) + val list1 = CaseClass(consClass, IntLiteral(10) :: list0 :: Nil) + val list2s = CaseClass(consClass, IntLiteral(5) :: list1 :: Nil) + val list2u = CaseClass(consClass, IntLiteral(5) :: list1 :: Nil) + val list3s = CaseClass(consClass, IntLiteral(5) :: list2s :: Nil) + val list3u1 = CaseClass(consClass, IntLiteral(5) :: list2u :: Nil) + val list3u2 = CaseClass(consClass, IntLiteral(15) :: list2s :: Nil) + val list3u3 = CaseClass(consClass, IntLiteral(15) :: list2u :: Nil) + + for (list <- List(list0, list1, list2s, list2u, list3s, list3u1, list3u2, list3u3)) + yield Map(argumentIds(0) -> list) } - + def introduceTwoListArgumentsExamples(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = { - - loader.hole.getType match { - case ct: ClassType => - val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef) - - val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0) - - val nilClass = nilClassSet.head - val consClass = consClassSet.head - - var counter = 0 - def getIntLiteral = { counter+=1; IntLiteral(counter) } - - val list0 = () => CaseClass(nilClass, Nil) - val list1 = () => CaseClass(consClass, getIntLiteral :: list0() :: Nil) - val list2 = () => CaseClass(consClass, getIntLiteral :: list1() :: Nil) - val list3 = () => CaseClass(consClass, getIntLiteral :: list2() :: Nil) - val list4 = () => CaseClass(consClass, getIntLiteral :: list3() :: Nil) - - val lists = List(list0, list1, list2, list3/*, list4*/) - - for(l1 <- lists; l2 <- lists) - yield Map(argumentIds(0) -> l1(), argumentIds(1) -> l2()) - - case _ => - null - } + + loader.hole.getType match { + case ct: ClassType => + val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef) + + val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0) + + val nilClass = nilClassSet.head + val consClass = consClassSet.head + + var counter = 0 + def getIntLiteral = { counter += 1; IntLiteral(counter) } + + val list0 = () => CaseClass(nilClass, Nil) + val list1 = () => CaseClass(consClass, getIntLiteral :: list0() :: Nil) + val list2 = () => CaseClass(consClass, getIntLiteral :: list1() :: Nil) + val list3 = () => CaseClass(consClass, getIntLiteral :: list2() :: Nil) + val list4 = () => CaseClass(consClass, getIntLiteral :: list3() :: Nil) + + val lists = List(list0, list1, list2, list3 /*, list4*/ ) + + for (l1 <- lists; l2 <- lists) + yield Map(argumentIds(0) -> l1(), argumentIds(1) -> l2()) + + case _ => + null + } } - + def isList(id: Identifier) = id.getType.toString == "List" def isInt(id: Identifier) = id.getType == Int32Type - -// def introduceOneListArgumentExamples(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = { -// -// // list type -// val ct = argumentIds(0).getType.asInstanceOf[ClassType] -// -// val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef) -// -// val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0) -// -// val nilClass = nilClassSet.head -// val consClass = consClassSet.head -// -// var counter = 10 -// def getIntLiteral = { counter+=1; IntLiteral(counter) } -// val intLiteral = IntLiteral(5) -// -// val list0 = CaseClass(nilClass, Nil) -// val list1 = CaseClass(consClass, IntLiteral(5) :: list0 :: Nil) -// val list2 = CaseClass(consClass, IntLiteral(3) :: list1 :: Nil) -// val list3 = CaseClass(consClass, IntLiteral(1) :: list2 :: Nil) -// val list32 = CaseClass(consClass, IntLiteral(10) :: CaseClass(consClass, IntLiteral(7) :: list1 :: Nil) :: Nil) -// -// val lists = List(list0, list1, list2, list3, list32) -// -// for(l1 <- lists) -// yield Map(argumentIds(0) -> l1) -// -// } + + // def introduceOneListArgumentExamples(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = { + // + // // list type + // val ct = argumentIds(0).getType.asInstanceOf[ClassType] + // + // val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef) + // + // val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0) + // + // val nilClass = nilClassSet.head + // val consClass = consClassSet.head + // + // var counter = 10 + // def getIntLiteral = { counter+=1; IntLiteral(counter) } + // val intLiteral = IntLiteral(5) + // + // val list0 = CaseClass(nilClass, Nil) + // val list1 = CaseClass(consClass, IntLiteral(5) :: list0 :: Nil) + // val list2 = CaseClass(consClass, IntLiteral(3) :: list1 :: Nil) + // val list3 = CaseClass(consClass, IntLiteral(1) :: list2 :: Nil) + // val list32 = CaseClass(consClass, IntLiteral(10) :: CaseClass(consClass, IntLiteral(7) :: list1 :: Nil) :: Nil) + // + // val lists = List(list0, list1, list2, list3, list32) + // + // for(l1 <- lists) + // yield Map(argumentIds(0) -> l1) + // + // } } \ No newline at end of file diff --git a/src/main/scala/lesynth/SynthesizerExamples.scala b/src/main/scala/lesynth/SynthesizerExamples.scala index 39cdcde6c..4c4fd1f73 100755 --- a/src/main/scala/lesynth/SynthesizerExamples.scala +++ b/src/main/scala/lesynth/SynthesizerExamples.scala @@ -25,7 +25,7 @@ import insynth.interfaces.Declaration import insynth.engine.InitialEnvironmentBuilder import insynth.leon.TypeTransformer import insynth.reconstruction.Output -import leon.synthesis.Problem +import leon.synthesis.{ Problem, SynthesisContext } import leon.Main.processOptions import leon.purescala.TypeTrees._ @@ -41,6 +41,7 @@ class SynthesizerForRuleExamples( val desiredType: LeonType, val holeFunDef: FunDef, val problem: Problem, + val synthesisContext: SynthesisContext, val freshResVar: LeonVariable, // number of condition expressions to try before giving up on that branch expression numberOfBooleanSnippets: Int = 5, @@ -99,6 +100,9 @@ class SynthesizerForRuleExamples( private var accumulatingExpression: Expr => Expr = _ //private var accumulatingExpressionMatch: Expr => Expr = _ + var flag1 = false + var flag2 = false + // time var startTime: Long = _ var verTime: Long = 0 @@ -131,6 +135,18 @@ class SynthesizerForRuleExamples( withPrec } + + val reporter = //new DefaultReporter + new SilentReporter + val args = + if (analyzeSynthesizedFunctionOnly) + Array(fileName, "--timeout=" + leonTimeout, "--functions=" + holeFunDef.id.name) + else + Array(fileName, "--timeout=" + leonTimeout) + info("Leon context array: " + args.mkString(",")) + ctx = processOptions(reporter, args.toList) + val solver = new TimeoutSolver(new FairZ3Solver(ctx), 1000L) + solver.setProgram(program) Globals.allSolved = solver.solve(theExpr) fine("solver said " + Globals.allSolved + " for " + theExpr) @@ -187,7 +203,8 @@ class SynthesizerForRuleExamples( // return found counterexamples and the formed precondition (maps, precondition) } - + + def getCurrentBuilder = new InitialEnvironmentBuilder(allDeclarations) def synthesizeBranchExpressions = @@ -338,6 +355,13 @@ class SynthesizerForRuleExamples( case Some(true) => false case _ => true } + // update flag in case of time limit overdue + def checkTimeout = + if (synthesisContext.shouldStop.get) { + keepGoing = false + true + } else + false // initial snippets (will update in the loop) var snippets = synthesizeBranchExpressions @@ -349,10 +373,13 @@ class SynthesizerForRuleExamples( // iterate while the program is not valid import scala.util.control.Breaks._ var iteration = 0 + var noBranchFoundIteration = 0 breakable { while (keepGoing) { + if (checkTimeout) break // next iteration iteration += 1 + noBranchFoundIteration += 1 reporter.info("####################################") reporter.info("######Iteration #" + iteration + " ###############") reporter.info("####################################") @@ -390,6 +417,7 @@ class SynthesizerForRuleExamples( ) { finest("snippetTree is: " + snippetTree) // note that we do not add snippets to the set of seen if enqueued + if (checkTimeout) break // skip avoidable calls if (!refiner.isAvoidable(snippetTree, problem.as)) { @@ -402,6 +430,7 @@ class SynthesizerForRuleExamples( if (tryToSynthesizeBranch(snippetTree)) { // will set found if correct body is found + noBranchFoundIteration = 0 break } } else { @@ -423,7 +452,7 @@ class SynthesizerForRuleExamples( } // if (!refiner.isAvoidable(snippetTree)) { // check if we this makes one test iteration - if (numberOfTested >= numberOfTestsInIteration) { + if (numberOfTested >= numberOfTestsInIteration * noBranchFoundIteration) { reporter.info("Finalizing enumeration/testing phase.") fine("Queue contents: " + pq.toList.take(10).mkString("\n")) fine({ if (pq.isEmpty) "queue is empty" else "head of queue is: " + pq.head }) @@ -436,6 +465,7 @@ class SynthesizerForRuleExamples( //interactivePause if (tryToSynthesizeBranch(nextSnippet)) { + noBranchFoundIteration = 0 break } @@ -443,6 +473,7 @@ class SynthesizerForRuleExamples( //seenBranchExpressions += nextSnippet.toString } + numberOfTested = 0 } else numberOfTested += 1 @@ -497,6 +528,7 @@ class SynthesizerForRuleExamples( // TODO spare one analyzing step // analyze the program fine("analyzing program for funDef:" + holeFunDef) + solver.setProgram(program) analyzeProgram // check if solver could solved this instance @@ -549,10 +581,12 @@ class SynthesizerForRuleExamples( // } //if(maps.isEmpty) throw new RuntimeException("asdasdasd") + + // will modify funDef body and precondition, restore it later try { - if (!maps.isEmpty) { + { //if (!maps.isEmpty) { // proceed with synthesizing boolean expressions //solver.setProgram(program) @@ -607,6 +641,23 @@ class SynthesizerForRuleExamples( } def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr, precondition: Expr): (Boolean, Option[Expr]) = { + + // trying some examples that cannot be verified + if (snippetTree.toString == "Cons(l.head, insert(e, l.tail))" //&& + //innerSnippetTree.toString.contains("aList.head < bList.head") +) { + val endTime = System.currentTimeMillis + reporter.info("We are done, in time: " + (endTime - startTime)) + interactivePause +} + + if (snippetTree.toString == "Cons(aList.head, merge(aList.tail, bList))" //&& + //innerSnippetTree.toString.contains("aList.head < bList.head") +) { + val endTime = System.currentTimeMillis + reporter.info("We are done, in time: " + (endTime - startTime)) + interactivePause +} // new condition together with existing precondition val newCondition = And(Seq(accumulatingPrecondition, innerSnippetTree)) @@ -637,6 +688,7 @@ class SynthesizerForRuleExamples( // if expression implies counterexamples add it to the precondition and try to validate program holeFunDef.precondition = Some(newCondition) // do analysis + solver.setProgram(program) analyzeProgram // program is valid, we have a branch if (Globals.allSolved == Some(true)) { @@ -722,4 +774,4 @@ class SynthesizerForRuleExamples( None } -} \ No newline at end of file +} diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala index bf54519c2..31acfdbb5 100755 --- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala +++ b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala @@ -34,7 +34,7 @@ case object ConditionAbductionSynthesisImmediate extends Rule("Condition abducti holeFunDef.precondition = Some(p.pc) val synthesizer = new SynthesizerForRuleExamples( - solver, program, desiredType, holeFunDef, p, freshResVar, + solver, program, desiredType, holeFunDef, p, sctx, freshResVar, reporter = reporter, introduceExamples = introduceTwoListArgumentsExamples ) diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala index a48556285..ded1a568d 100755 --- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala +++ b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala @@ -7,11 +7,12 @@ import leon.purescala.TypeTrees._ import leon.purescala.TreeOps._ import leon.purescala.Extractors._ import leon.purescala.Definitions._ +import leon.purescala.DataGen.findModels import leon.synthesis._ import leon.solvers.{ Solver, TimeoutSolver } +import leon.evaluators.CodeGenEvaluator import InputExamples._ -import lesynth.SynthesizerForRuleExamples case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abduction synthesis (two phase).") { def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = { @@ -21,7 +22,7 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio List(new RuleInstantiation(p, this, SolutionBuilder.none, "Condition abduction") { def apply(sctx: SynthesisContext): RuleApplicationResult = { try { - val solver = new TimeoutSolver(sctx.solver, 2000L) + val solver = new TimeoutSolver(sctx.solver, 1000L) val program = sctx.program val reporter = sctx.reporter @@ -36,15 +37,24 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio val freshResID = FreshIdentifier("result").setType(holeFunDef.returnType) val freshResVar = Variable(freshResID) + val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program) + def getInputExamples = + getDataGenInputExamples(codeGenEval, p, + 40, 2000, Some(holeFunDef.args.map(_.id)) + ) _ + holeFunDef.postcondition = Some(replace( Map(givenVariable.toVariable -> ResultVariable().setType(holeFunDef.returnType)), p.phi)) holeFunDef.precondition = Some(p.pc) val synthesizer = new SynthesizerForRuleExamples( - solver, program, desiredType, holeFunDef, p, freshResVar, + solver, program, desiredType, holeFunDef, p, sctx, freshResVar, 20, 2, 1, reporter = reporter, - introduceExamples = getInputExamples) + introduceExamples = getInputExamples, + numberOfTestsInIteration = 50, + numberOfCheckInIteration = 5 + ) synthesizer.synthesize match { case EmptyReport => RuleApplicationImpossible -- GitLab