From 965264c32ced7a8154670a7590bcada1ae5e6e8b Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 7 Jan 2013 18:57:03 +0100
Subject: [PATCH] Allow onSuccess to fail. This is necessary to prevent
soundness issues.
The synthesizer used to generate wrong programs by generating inductive
programs with an impossible base-case. onSuccess on inductive rules now
prevents this by checking that sufficiently many cases have precondition
== true. Otherwise, onSuccess fails. This last-moment failure is now
handled correctly.
Strenghten precondition
---
.../scala/leon/synthesis/Heuristics.scala | 4 +-
src/main/scala/leon/synthesis/Rules.scala | 16 ++++----
src/main/scala/leon/synthesis/Solution.scala | 5 ---
.../synthesis/heuristics/ADTInduction.scala | 24 +++++++----
.../synthesis/heuristics/IntInduction.scala | 40 +++++++++++--------
.../scala/leon/synthesis/rules/ADTSplit.scala | 4 +-
.../scala/leon/synthesis/rules/Assert.scala | 4 +-
.../leon/synthesis/rules/CaseSplit.scala | 6 +--
.../leon/synthesis/rules/EqualitySplit.scala | 6 +--
.../synthesis/rules/IntegerEquation.scala | 18 +++++----
.../synthesis/rules/IntegerInequalities.scala | 11 ++---
.../scala/leon/synthesis/rules/OnePoint.scala | 10 +++--
.../synthesis/rules/UnconstrainedOutput.scala | 6 +--
.../leon/synthesis/search/AndOrGraph.scala | 14 +++++--
14 files changed, 97 insertions(+), 71 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index a80831ec4..837c08d3b 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -37,10 +37,10 @@ object HeuristicInstantiation {
Some(s)
}
- def apply(problem: Problem, rule: Rule, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
+ def apply(problem: Problem, rule: Rule, subProblems: List[Problem], onSuccess: List[Solution] => Option[Solution]): RuleInstantiation = {
val builder = new SolutionBuilder(subProblems.size) {
def apply(sols: List[Solution]) = {
- Some(onSuccess(sols))
+ onSuccess(sols)
}
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 0ea37eac2..548d8fb30 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -31,10 +31,10 @@ abstract class SolutionBuilder(val arity: Int) {
def apply(sols: List[Solution]): Option[Solution]
}
-class SolutionCombiner(arity: Int, f: List[Solution] => Solution) extends SolutionBuilder(arity) {
+class SolutionCombiner(arity: Int, f: List[Solution] => Option[Solution]) extends SolutionBuilder(arity) {
def apply(sols: List[Solution]) = {
assert(sols.size == arity)
- Some(f(sols))
+ f(sols)
}
}
@@ -62,14 +62,14 @@ case class RuleDecomposed(sub: List[Problem]) extends RuleApplicationResult
case object RuleApplicationImpossible extends RuleApplicationResult
object RuleInstantiation {
- def immediateDecomp(problem: Problem, rule: Rule, sub: List[Problem], onSuccess: List[Solution] => Solution) = {
+ def immediateDecomp(problem: Problem, rule: Rule, sub: List[Problem], onSuccess: List[Solution] => Option[Solution]) = {
new RuleInstantiation(problem, rule, new SolutionCombiner(sub.size, onSuccess)) {
def apply(sctx: SynthesisContext) = RuleDecomposed(sub)
}
}
def immediateSuccess(problem: Problem, rule: Rule, solution: Solution) = {
- new RuleInstantiation(problem, rule, new SolutionCombiner(0, ls => solution)) {
+ new RuleInstantiation(problem, rule, new SolutionCombiner(0, ls => Some(solution))) {
def apply(sctx: SynthesisContext) = RuleSuccess(solution)
}
}
@@ -81,9 +81,11 @@ abstract class Rule(val name: String) {
def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replace(what.map(w => Variable(w._1) -> w._2), in)
- val forward: List[Solution] => Solution = {
- case List(s) => Solution(s.pre, s.defs, s.term)
- case _ => Solution.none
+ val forward: List[Solution] => Option[Solution] = {
+ case List(s) =>
+ Some(Solution(s.pre, s.defs, s.term))
+ case _ =>
+ None
}
override def toString = "R: "+name
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 945e9796b..07c37915b 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -28,7 +28,6 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr) {
}
object Solution {
-
def simplify(e: Expr) = simplifyLets(e)
def apply(pre: Expr, defs: Set[FunDef], term: Expr) = {
@@ -49,8 +48,4 @@ object Solution {
def simplest: Solution = {
new Solution(BooleanLiteral(true), Set(), BooleanLiteral(true))
}
-
- def none: Solution = {
- throw new Exception("Unexpected failure to construct solution")
- }
}
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index c9e5af133..b1f95c726 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -73,7 +73,7 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
sys.error("Woops, non case-class as descendent")
}
- val onSuccess: List[Solution] => Solution = {
+ val onSuccess: List[Solution] => Option[Solution] = {
case sols =>
var globalPre = List[Expr]()
@@ -86,15 +86,25 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
SimpleCase(caze, calls.foldLeft(sol.term){ case (t, (binders, callargs)) => LetTuple(binders, FunctionInvocation(newFun, callargs), t) })
}
- val funPre = subst(origId -> Variable(inductOn), Or(globalPre))
- val outerPre = Or(globalPre)
+ if (sols.exists(_.pre != BooleanLiteral(true))) {
+ // Required to avoid an impossible cases, which suffices to
+ // allow invalid programs. This might be too strong though: we
+ // might only have to enforce it on solutions of base cases.
+ None
+ } else {
+ val funPre = subst(origId -> Variable(inductOn), Or(globalPre))
+ val outerPre = Or(globalPre)
- newFun.precondition = Some(funPre)
- newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable().setType(resType), p.phi))
+ newFun.precondition = Some(funPre)
+ newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable().setType(resType), p.phi))
- newFun.body = Some(MatchExpr(Variable(inductOn), cases))
+ newFun.body = Some(MatchExpr(Variable(inductOn), cases))
- Solution(Or(globalPre), sols.flatMap(_.defs).toSet+newFun, FunctionInvocation(newFun, Variable(origId) :: oas.map(Variable(_))))
+ Some(Solution(Or(globalPre),
+ sols.flatMap(_.defs).toSet+newFun,
+ FunctionInvocation(newFun, Variable(origId) :: oas.map(Variable(_)))
+ ))
+ }
}
Some(HeuristicInstantiation(p, this, subProblemsInfo.map(_._1).toList, onSuccess))
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index 8151341a3..e59150394 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -29,29 +29,35 @@ case object IntInduction extends Rule("Int Induction") with Heuristic {
val subGT = Problem(inductOn :: postXs, And(Seq(GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT, p.pc)), newPhi, p.xs)
val subLT = Problem(inductOn :: postXs, And(Seq(LessThan(Variable(inductOn), IntLiteral(0)), postCondLT, p.pc)), newPhi, p.xs)
- val onSuccess: List[Solution] => Solution = {
+ val onSuccess: List[Solution] => Option[Solution] = {
case List(base, gt, lt) =>
- val preIn = Or(Seq(And(Equals(Variable(inductOn), IntLiteral(0)), base.pre),
- And(GreaterThan(Variable(inductOn), IntLiteral(0)), gt.pre),
- And(LessThan(Variable(inductOn), IntLiteral(0)), lt.pre)))
- val preOut = subst(inductOn -> Variable(origId), preIn)
+ if (base.pre != BooleanLiteral(true) || (gt.pre != BooleanLiteral(true) && lt.pre != BooleanLiteral(true))) {
+ // Required to avoid an impossible base-case, which suffices to
+ // allow invalid programs.
+ None
+ } else {
+ val preIn = Or(Seq(And(Equals(Variable(inductOn), IntLiteral(0)), base.pre),
+ And(GreaterThan(Variable(inductOn), IntLiteral(0)), gt.pre),
+ And(LessThan(Variable(inductOn), IntLiteral(0)), lt.pre)))
+ val preOut = subst(inductOn -> Variable(origId), preIn)
- val newFun = new FunDef(FreshIdentifier("rec", true), tpe, Seq(VarDecl(inductOn, inductOn.getType)))
- newFun.precondition = Some(preIn)
- newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable().setType(tpe), p.phi))
+ val newFun = new FunDef(FreshIdentifier("rec", true), tpe, Seq(VarDecl(inductOn, inductOn.getType)))
+ newFun.precondition = Some(preIn)
+ newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable().setType(tpe), p.phi))
- newFun.body = Some(
- IfExpr(Equals(Variable(inductOn), IntLiteral(0)),
- base.toExpr,
- IfExpr(GreaterThan(Variable(inductOn), IntLiteral(0)),
- LetTuple(postXs, FunctionInvocation(newFun, Seq(Minus(Variable(inductOn), IntLiteral(1)))), gt.toExpr)
- , LetTuple(postXs, FunctionInvocation(newFun, Seq(Plus(Variable(inductOn), IntLiteral(1)))), lt.toExpr)))
- )
+ newFun.body = Some(
+ IfExpr(Equals(Variable(inductOn), IntLiteral(0)),
+ base.toExpr,
+ IfExpr(GreaterThan(Variable(inductOn), IntLiteral(0)),
+ LetTuple(postXs, FunctionInvocation(newFun, Seq(Minus(Variable(inductOn), IntLiteral(1)))), gt.toExpr)
+ , LetTuple(postXs, FunctionInvocation(newFun, Seq(Plus(Variable(inductOn), IntLiteral(1)))), lt.toExpr)))
+ )
- Solution(preOut, base.defs++gt.defs++lt.defs+newFun, FunctionInvocation(newFun, Seq(Variable(origId))))
+ Some(Solution(preOut, base.defs++gt.defs++lt.defs+newFun, FunctionInvocation(newFun, Seq(Variable(origId)))))
+ }
case _ =>
- Solution.none
+ None
}
Some(HeuristicInstantiation(p, this, List(subBase, subGT, subLT), onSuccess))
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 7235f9bb4..07347e95b 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -56,7 +56,7 @@ case object ADTSplit extends Rule("ADT Split.") {
}
- val onSuccess: List[Solution] => Solution = {
+ val onSuccess: List[Solution] => Option[Solution] = {
case sols =>
var globalPre = List[Expr]()
@@ -66,7 +66,7 @@ case object ADTSplit extends Rule("ADT Split.") {
SimpleCase(pattern, sol.term)
}
- Solution(Or(globalPre), sols.flatMap(_.defs).toSet, MatchExpr(Variable(id), cases))
+ Some(Solution(Or(globalPre), sols.flatMap(_.defs).toSet, MatchExpr(Variable(id), cases)))
}
Some(RuleInstantiation.immediateDecomp(p, this, subInfo.map(_._2).toList, onSuccess))
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index d45d08903..898f1ea05 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -21,8 +21,8 @@ case object Assert extends Rule("Assert") {
val sub = p.copy(pc = And(p.pc +: exprsA), phi = And(others))
List(RuleInstantiation.immediateDecomp(p, this, List(sub), {
- case Solution(pre, defs, term) :: Nil => Solution(And(exprsA :+ pre), defs, term)
- case _ => Solution.none
+ case Solution(pre, defs, term) :: Nil => Some(Solution(And(exprsA :+ pre), defs, term))
+ case _ => None
}))
}
} else {
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 9b3e56315..1e1ac7940 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -19,7 +19,7 @@ case object CaseSplit extends Rule("Case-Split") {
def split(alts: Seq[Expr], p: Problem): RuleInstantiation = {
val subs = alts.map(a => Problem(p.as, p.pc, a, p.xs)).toList
- val onSuccess: List[Solution] => Solution = {
+ val onSuccess: List[Solution] => Option[Solution] = {
case sols if sols.size == subs.size =>
val pre = Or(sols.map(_.pre))
val defs = sols.map(_.defs).reduceLeft(_ ++ _)
@@ -28,10 +28,10 @@ case object CaseSplit extends Rule("Case-Split") {
val term = prefix.foldRight(last.term) { (s, t) => IfExpr(s.pre, s.term, t) }
- Solution(pre, defs, term)
+ Some(Solution(pre, defs, term))
case _ =>
- Solution.none
+ None
}
RuleInstantiation.immediateDecomp(p, this, subs, onSuccess)
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index 603a48a08..205440cf3 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -41,11 +41,11 @@ case object EqualitySplit extends Rule("Eq. Split.") {
val sub1 = p.copy(pc = And(Equals(Variable(a1), Variable(a2)), p.pc))
val sub2 = p.copy(pc = And(Not(Equals(Variable(a1), Variable(a2))), p.pc))
- val onSuccess: List[Solution] => Solution = {
+ val onSuccess: List[Solution] => Option[Solution] = {
case List(s1, s2) =>
- Solution(Or(s1.pre, s2.pre), s1.defs++s2.defs, IfExpr(Equals(Variable(a1), Variable(a2)), s1.term, s2.term))
+ Some(Solution(Or(s1.pre, s2.pre), s1.defs++s2.defs, IfExpr(Equals(Variable(a1), Variable(a2)), s1.term, s2.term)))
case _ =>
- Solution.none
+ None
}
Some(RuleInstantiation.immediateDecomp(p, this, List(sub1, sub2), onSuccess))
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index f74e4478e..1d3579907 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -53,11 +53,11 @@ case object IntegerEquation extends Rule("Integer Equation") {
val eqPre = Equals(normalizedEq.head, IntLiteral(0))
val newProblem = Problem(problem.as, And(eqPre, problem.pc), And(allOthers), problem.xs)
- val onSuccess: List[Solution] => Solution = {
- case List(Solution(pre, defs, term)) => {
- Solution(And(eqPre, pre), defs, term)
- }
- case _ => Solution.none
+ val onSuccess: List[Solution] => Option[Solution] = {
+ case List(Solution(pre, defs, term)) =>
+ Some(Solution(And(eqPre, pre), defs, term))
+ case _ =>
+ None
}
List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess))
@@ -90,7 +90,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
val newProblem = Problem(problem.as ++ freshInputVariables, And(eqPre, problem.pc), freshFormula, subproblemxs)
- val onSuccess: List[Solution] => Solution = {
+ val onSuccess: List[Solution] => Option[Solution] = {
case List(Solution(pre, defs, term)) => {
val freshPre = replace(equivalenceConstraints, pre)
val freshTerm = replace(equivalenceConstraints, term)
@@ -98,9 +98,11 @@ case object IntegerEquation extends Rule("Integer Equation") {
val id2res: Map[Expr, Expr] =
freshsubxs.zip(subproblemxs).map{case (id1, id2) => (Variable(id1), Variable(id2))}.toMap ++
neqxs.map(id => (Variable(id), eqSubstMap(Variable(id)))).toMap
- Solution(And(eqPre, freshPre), defs, simplifyArithmetic(simplifyLets(LetTuple(subproblemxs, freshTerm, replace(id2res, Tuple(problem.xs.map(Variable(_))))))))
+ Some(Solution(And(eqPre, freshPre), defs, simplifyArithmetic(simplifyLets(LetTuple(subproblemxs, freshTerm, replace(id2res, Tuple(problem.xs.map(Variable(_)))))))))
}
- case _ => Solution.none
+
+ case _ =>
+ None
}
List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess))
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 7fbc67fd6..540dd6b94 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -163,13 +163,13 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
val subProblem = Problem(problem.as ++ remainderIds, problem.pc, subProblemFormula, subProblemxs)
- def onSuccess(sols: List[Solution]): Solution = sols match {
+ def onSuccess(sols: List[Solution]): Option[Solution] = sols match {
case List(Solution(pre, defs, term)) => {
if(remainderIds.isEmpty) {
- Solution(And(newPre, pre), defs,
+ Some(Solution(And(newPre, pre), defs,
LetTuple(subProblemxs, term,
Let(processedVar, witness,
- Tuple(problem.xs.map(Variable(_))))))
+ Tuple(problem.xs.map(Variable(_)))))))
} else if(remainderIds.size > 1) {
sys.error("TODO")
} else {
@@ -194,10 +194,11 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
))
funDef.body = Some(funBody)
- Solution(And(newPre, pre), defs + funDef, FunctionInvocation(funDef, Seq(IntLiteral(L-1))))
+ Some(Solution(And(newPre, pre), defs + funDef, FunctionInvocation(funDef, Seq(IntLiteral(L-1)))))
}
}
- case _ => Solution.none
+ case _ =>
+ None
}
List(RuleInstantiation.immediateDecomp(problem, this, List(subProblem), onSuccess))
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 7f4fae9da..42c931f59 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -25,14 +25,16 @@ case object OnePoint extends Rule("One-point") {
val newProblem = Problem(p.as, p.pc, subst(x -> e, And(others)), oxs)
- val onSuccess: List[Solution] => Solution = {
+ val onSuccess: List[Solution] => Option[Solution] = {
case List(Solution(pre, defs, term)) =>
if (oxs.isEmpty) {
- Solution(pre, defs, Tuple(e :: Nil))
+ Some(Solution(pre, defs, Tuple(e :: Nil)))
} else {
- Solution(pre, defs, LetTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_))))))
+ Some(Solution(pre, defs, LetTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_)))))))
}
- case _ => Solution.none
+
+ case _ =>
+ None
}
List(RuleInstantiation.immediateDecomp(p, this, List(newProblem), onSuccess))
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 381f73f6b..c5ddd02ef 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -13,11 +13,11 @@ case object UnconstrainedOutput extends Rule("Unconstr.Output") {
if (!unconstr.isEmpty) {
val sub = p.copy(xs = p.xs.filterNot(unconstr))
- val onSuccess: List[Solution] => Solution = {
+ val onSuccess: List[Solution] => Option[Solution] = {
case List(s) =>
- Solution(s.pre, s.defs, LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(Variable(id)) else Variable(id)))))
+ Some(Solution(s.pre, s.defs, LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(Variable(id)) else Variable(id))))))
case _ =>
- Solution.none
+ None
}
List(RuleInstantiation.immediateDecomp(p, this, List(sub), onSuccess))
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraph.scala b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
index 251734160..8227a0e9f 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
@@ -84,10 +84,18 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S](val root: OT, val cos
subSolutions += sub.task -> sol
if (subSolutions.size == subProblems.size) {
- solution = task.composeSolution(subTasks.map(subSolutions))
- updateMin()
+ task.composeSolution(subTasks.map(subSolutions)) match {
+ case Some(sol) =>
+ solution = Some(sol)
+ updateMin()
+
+ notifyParent(sol)
- notifyParent(solution.get)
+ case None =>
+ if (solution.isEmpty) {
+ unsolvable(sub)
+ }
+ }
} else {
updateMin()
}
--
GitLab