diff --git a/mytest/Epsilon1.scala b/mytest/Epsilon1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..827c1e6e5a1de4363b7fc61bf7ceeba07c85ac2e
--- /dev/null
+++ b/mytest/Epsilon1.scala
@@ -0,0 +1,13 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def greater(x: Int): Int = {
+ epsilon((y: Int) => y > x)
+ } ensuring(_ >= x)
+
+ def greaterWrong(x: Int): Int = {
+ epsilon((y: Int) => y >= x)
+ } ensuring(_ > x)
+
+}
diff --git a/mytest/Epsilon2.scala b/mytest/Epsilon2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1bf56bdd7b517c1c895ffe478046f4443856ea1e
--- /dev/null
+++ b/mytest/Epsilon2.scala
@@ -0,0 +1,23 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def rand(): Int = epsilon((x: Int) => true)
+ def rand2(x: Int): Int = epsilon((y: Int) => true)
+ def rand3(x: Int): Int = epsilon((y: Int) => x == x)
+
+ //this should hold, that is the expected semantic of our epsilon
+ def property1(): Boolean = {
+ rand() == rand()
+ } holds
+
+ //this should hold, that is the expected semantic of our epsilon
+ def property2(x: Int): Boolean = {
+ rand2(x) == rand2(x+1)
+ } holds
+
+ //this should NOT hold
+ def property3(x: Int): Boolean = {
+ rand3(x) == rand3(x+1)
+ } holds
+}
diff --git a/mytest/Sets2.scala b/mytest/Sets2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..14e636924d9c44a660a6d168b0a7a6badc5c8307
--- /dev/null
+++ b/mytest/Sets2.scala
@@ -0,0 +1,29 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Sets2 {
+ sealed abstract class MyList
+ case class MyCons(head: Int, tail: MyList) extends MyList
+ case class MyNil() extends MyList
+
+ def size(lst: MyList): Int = (lst match {
+ case MyNil() => 0
+ case MyCons(_, xs) => 1 + size(xs)
+ })
+
+ def toSet(lst: MyList): Set[Int] = lst match {
+ case MyCons(x, xs) => toSet(xs) ++ Set(x)
+ case MyNil() => Set[Int]()
+ }
+
+ def toList(set: Set[Int]): MyList = if(set == Set.empty[Int]) MyNil() else {
+ val elem = epsilon((x : Int) => set contains x)
+ MyCons(elem, toList(set -- Set[Int](elem)))
+ }
+
+ @induct
+ def property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds
+
+ def wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds
+ def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
+}
diff --git a/src/main/scala/leon/EpsilonElimination.scala b/src/main/scala/leon/EpsilonElimination.scala
new file mode 100644
index 0000000000000000000000000000000000000000..585888f4c771ea6354df64f8792d0becd90dea52
--- /dev/null
+++ b/src/main/scala/leon/EpsilonElimination.scala
@@ -0,0 +1,33 @@
+package leon
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
+
+object EpsilonElimination extends Pass {
+
+ val description = "Remove all epsilons from the program"
+
+ def apply(pgm: Program): Program = {
+
+ val allFuns = pgm.definedFunctions
+ allFuns.foreach(fd => fd.body.map(body => {
+ val newBody = searchAndReplaceDFS{
+ case eps@Epsilon(pred) => {
+ val freshName = FreshIdentifier("epsilon")
+ val newFunDef = new FunDef(freshName, eps.getType, Seq())
+ val epsilonVar = EpsilonVariable(eps.posIntInfo)
+ val resultVar = ResultVariable().setType(eps.getType)
+ val postcondition = replace(Map(epsilonVar -> resultVar), pred)
+ newFunDef.postcondition = Some(postcondition)
+ Some(LetDef(newFunDef, FunctionInvocation(newFunDef, Seq())))
+ }
+ case _ => None
+ }(body)
+ fd.body = Some(newBody)
+ }))
+ pgm
+ }
+
+}
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index 72c62ef152b58b54a563ceb9e238c129af5a565c..6bb9ef1b3f4bc7fcfbcb9e719c36325a7759bd85 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -24,11 +24,16 @@ object Evaluator {
case class InfiniteComputation() extends EvaluationResult {
val finalResult = None
}
+ case class PostconditionViolationFunctionFromModel() extends EvaluationResult {
+ val finalResult = None
+ }
+
def eval(context: EvaluationContext, expression: Expr, evaluator: Option[(EvaluationContext)=>Boolean], maxSteps: Int=500000) : EvaluationResult = {
case class RuntimeErrorEx(msg: String) extends Exception
case class InfiniteComputationEx() extends Exception
case class TypeErrorEx(typeError: TypeError) extends Exception
+ case class PostconditionViolationFunctionFromModelEx() extends Exception
var left: Int = maxSteps
@@ -85,16 +90,18 @@ object Evaluator {
}
}
- if(!fd.hasBody) {
+ if(!fd.hasBody && !context.isDefinedAt(fd.id)) {
throw RuntimeErrorEx("Evaluation of function with unknown implementation.")
}
- val callResult = rec(frame, matchToIfThenElse(fd.body.get))
+ val body = fd.body.getOrElse(context(fd.id))
+ val callResult = rec(frame, matchToIfThenElse(body))
if(fd.hasPostcondition) {
val freshResID = FreshIdentifier("result").setType(fd.returnType)
val postBody = replace(Map(ResultVariable() -> Variable(freshResID)), matchToIfThenElse(fd.postcondition.get))
rec(frame + ((freshResID -> callResult)), postBody) match {
case BooleanLiteral(true) => ;
+ case BooleanLiteral(false) if !fd.hasImplementation => throw PostconditionViolationFunctionFromModelEx()
case BooleanLiteral(false) => throw RuntimeErrorEx("Postcondition violation for " + fd.id.name + " reached in evaluation.")
case other => throw TypeErrorEx(TypeError(other, BooleanType))
}
@@ -306,6 +313,7 @@ object Evaluator {
case RuntimeErrorEx(msg) => RuntimeError(msg)
case InfiniteComputationEx() => InfiniteComputation()
case TypeErrorEx(te) => te
+ case PostconditionViolationFunctionFromModelEx() => PostconditionViolationFunctionFromModel()
}
}
}
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index d70d665fdb4e1281e490ab7640794c9b36360373..ebca10ab29caa0c40c4742dc0a37c3c1bcc655d3 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -581,9 +581,11 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
}
case (Some(true), m) => { // SAT
- //println("MODEL IS: " + m)
validatingStopwatch.start
- val (trueModel, model) = validateAndDeleteModel(m, toCheckAgainstModels, varsInVC, evaluator)
+ val (trueModel, model) = if(Settings.verifyModel)
+ validateAndDeleteModel(m, toCheckAgainstModels, varsInVC, evaluator)
+ else
+ (true, modelToMap(m, varsInVC))
validatingStopwatch.stop
if (trueModel) {
@@ -779,7 +781,33 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
import Evaluator._
if(!forceStop) {
- val asMap = modelToMap(model, variables)
+
+ val functionsModel: Map[Z3FuncDecl, (Seq[(Seq[Z3AST], Z3AST)], Z3AST)] = model.getModelFuncInterpretations.map(i => (i._1, (i._2, i._3))).toMap
+ val functionsAsMap: Map[Identifier, Expr] = functionsModel.flatMap(p => {
+ if(isKnownDecl(p._1)) {
+ val fd = functionDeclToDef(p._1)
+ if(!fd.hasImplementation) {
+ val (cses, default) = p._2
+ val ite = cses.foldLeft(fromZ3Formula(model, default, Some(fd.returnType)))((expr, q) => IfExpr(
+ And(
+ q._1.zip(fd.args).map(a12 => Equals(fromZ3Formula(model, a12._1, Some(a12._2.tpe)), Variable(a12._2.id)))
+ ),
+ fromZ3Formula(model, q._2, Some(fd.returnType)),
+ expr))
+ Seq((fd.id, ite))
+ } else Seq()
+ } else Seq()
+ }).toMap
+ val constantFunctionsAsMap: Map[Identifier, Expr] = model.getModelConstantInterpretations.flatMap(p => {
+ if(isKnownDecl(p._1)) {
+ val fd = functionDeclToDef(p._1)
+ if(!fd.hasImplementation) {
+ Seq((fd.id, fromZ3Formula(model, p._2, Some(fd.returnType))))
+ } else Seq()
+ } else Seq()
+ }).toMap
+
+ val asMap = modelToMap(model, variables) ++ functionsAsMap ++ constantFunctionsAsMap
model.delete
lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
val evalResult = eval(asMap, formula, evaluator)
@@ -799,6 +827,10 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
reporter.info("- Invalid model.")
(false, asMap)
}
+ case PostconditionViolationFunctionFromModel() => {
+ reporter.info("- Invalid Model: postcondition violation of a function that whose implementation was specified by the model")
+ (false, asMap)
+ }
case other => {
reporter.error("Something went wrong. While evaluating the model, we got this: " + other)
(false, asMap)
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index 0bcfa566e996e4f8d9ebe572bce0979ab37c565c..172281235e2c40aef6583c64156f991d90a6c6d3 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -13,7 +13,6 @@ object FunctionClosure extends Pass {
private var pathConstraints: List[Expr] = Nil
private var newFunDefs: Map[FunDef, FunDef] = Map()
- //private var
def apply(program: Program): Program = {
newFunDefs = Map()
@@ -21,7 +20,8 @@ object FunctionClosure extends Pass {
funDefs.foreach(fd => {
enclosingPreconditions = fd.precondition.toList
pathConstraints = fd.precondition.toList
- fd.body = Some(functionClosure(fd.getBody, fd.args.map(_.id).toSet))
+ fd.body = fd.body.map(b => functionClosure(b, fd.args.map(_.id).toSet))
+ fd.postcondition = fd.postcondition.map(b => functionClosure(b, fd.args.map(_.id).toSet))
})
program
}
@@ -32,11 +32,13 @@ object FunctionClosure extends Pass {
val id = fd.id
val rt = fd.returnType
val varDecl = fd.args
- val funBody = fd.getBody
val precondition = fd.precondition
val postcondition = fd.postcondition
- val bodyVars: Set[Identifier] = variablesOf(funBody) ++ variablesOf(precondition.getOrElse(BooleanLiteral(true)))
+ val bodyVars: Set[Identifier] = variablesOf(fd.body.getOrElse(BooleanLiteral(true))) ++
+ variablesOf(precondition.getOrElse(BooleanLiteral(true))) ++
+ variablesOf(postcondition.getOrElse(BooleanLiteral(true)))
+
val capturedVars = bodyVars.intersect(bindedVars)// this should be the variable used that are in the scope
val (constraints, allCapturedVars) = filterConstraints(capturedVars) //all relevant path constraints
val capturedVarsWithConstraints = allCapturedVars.toSeq
@@ -52,32 +54,38 @@ object FunctionClosure extends Pass {
newFunDef.parent = fd.parent
val freshPrecondition = precondition.map(expr => replace(freshVarsExpr, expr))
+ val freshPostcondition = postcondition.map(expr => replace(freshVarsExpr, expr))
+ val freshBody = fd.body.map(b => replace(freshVarsExpr, b))
val freshConstraints = constraints.map(expr => replace(freshVarsExpr, expr))
- newFunDef.precondition = freshConstraints match {
- case List() => freshPrecondition
- case precs => Some(And(freshPrecondition.getOrElse(BooleanLiteral(true)) +: precs))
- }
- newFunDef.postcondition = postcondition.map(expr => replace(freshVarsExpr, expr))
def substFunInvocInDef(expr: Expr): Option[Expr] = expr match {
case fi@FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ extraVarDecls.map(_.id.toVariable)).setPosInfo(fi))
case _ => None
}
- val freshBody = replace(freshVarsExpr, funBody)
val oldPathConstraints = pathConstraints
pathConstraints = (precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints).map(e => replace(freshVarsExpr, e))
- val recBody = functionClosure(freshBody, bindedVars ++ newVarDecls.map(_.id))
+ val recPrecondition = freshConstraints match { //Actually, we do not allow nested fundef in precondition
+ case List() => freshPrecondition
+ case precs => Some(And(freshPrecondition.getOrElse(BooleanLiteral(true)) +: precs))
+ }
+ val recBody = freshBody.map(b =>
+ functionClosure(b, bindedVars ++ newVarDecls.map(_.id))
+ ).map(b => searchAndReplaceDFS(substFunInvocInDef)(b))
+ val recPostcondition = freshPostcondition.map(expr =>
+ functionClosure(expr, bindedVars ++ newVarDecls.map(_.id))
+ ).map(expr => searchAndReplaceDFS(substFunInvocInDef)(expr))
pathConstraints = oldPathConstraints
- val recBody2 = searchAndReplaceDFS(substFunInvocInDef)(recBody)
- newFunDef.body = Some(recBody2)
+
+ newFunDef.precondition = recPrecondition
+ newFunDef.body = recBody
+ newFunDef.postcondition = recPostcondition
def substFunInvocInRest(expr: Expr): Option[Expr] = expr match {
case fi@FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVarsWithConstraints.map(_.toVariable)).setPosInfo(fi))
case _ => None
}
- val recRest = functionClosure(rest, bindedVars)
- val recRest2 = searchAndReplaceDFS(substFunInvocInRest)(recRest)
- LetDef(newFunDef, recRest2).setType(l.getType)
+ val recRest = searchAndReplaceDFS(substFunInvocInRest)(functionClosure(rest, bindedVars))
+ LetDef(newFunDef, recRest).setType(l.getType)
}
case l @ Let(i,e,b) => {
val re = functionClosure(e, bindedVars)
diff --git a/src/main/scala/leon/FunctionHoisting.scala b/src/main/scala/leon/FunctionHoisting.scala
index c8ad9268dc3b571be1a812d35317f7bc4562b6a7..37bc69c41fa12e41c94b3c8d876631f8e3f47220 100644
--- a/src/main/scala/leon/FunctionHoisting.scala
+++ b/src/main/scala/leon/FunctionHoisting.scala
@@ -13,9 +13,23 @@ object FunctionHoisting extends Pass {
val funDefs = program.definedFunctions
var topLevelFuns: Set[FunDef] = Set()
funDefs.foreach(fd => {
- val (newBody, additionalTopLevelFun) = hoist(fd.getBody)
- fd.body = Some(newBody)
- topLevelFuns ++= additionalTopLevelFun
+ val s2 = fd.body match {
+ case Some(body) => {
+ val (e2, s2) = hoist(body)
+ fd.body = Some(e2)
+ s2
+ }
+ case None => Set()
+ }
+ val s4 = fd.postcondition match {
+ case Some(expr) => {
+ val (e4, s4) = hoist(expr)
+ fd.postcondition = Some(e4)
+ s4
+ }
+ case None => Set()
+ }
+ topLevelFuns ++= (s2 ++ s4)
})
val Program(id, ObjectDef(objId, defs, invariants)) = program
Program(id, ObjectDef(objId, defs ++ topLevelFuns, invariants))
@@ -24,10 +38,23 @@ object FunctionHoisting extends Pass {
private def hoist(expr: Expr): (Expr, Set[FunDef]) = expr match {
case l @ LetDef(fd, rest) => {
val (e, s) = hoist(rest)
- val (e2, s2) = hoist(fd.getBody)
- fd.body = Some(e2)
-
- (e, (s ++ s2) + fd)
+ val s2 = fd.body match {
+ case Some(body) => {
+ val (e2, s2) = hoist(body)
+ fd.body = Some(e2)
+ s2
+ }
+ case None => Set()
+ }
+ val s4 = fd.postcondition match {
+ case Some(expr) => {
+ val (e4, s4) = hoist(expr)
+ fd.postcondition = Some(e4)
+ s4
+ }
+ case None => Set()
+ }
+ (e, (s ++ s2 ++ s4) + fd)
}
case l @ Let(i,e,b) => {
val (re, s1) = hoist(e)
diff --git a/src/main/scala/leon/FunctionTemplate.scala b/src/main/scala/leon/FunctionTemplate.scala
index 6a4395f188bf19d7b636c3cb3ec646d921ed38b1..be4189b4283b2d79eefd63c94726ea7f6d683000 100644
--- a/src/main/scala/leon/FunctionTemplate.scala
+++ b/src/main/scala/leon/FunctionTemplate.scala
@@ -90,9 +90,11 @@ object FunctionTemplate {
cache(funDef)
} else {
val result = {
+ /*
if(!funDef.hasImplementation) {
sys.error("Cannot create a FunctionTemplate out of a function with no body.")
}
+ */
val condVars : MutableSet[Identifier] = MutableSet.empty
val exprVars : MutableSet[Identifier] = MutableSet.empty
@@ -165,14 +167,22 @@ object FunctionTemplate {
}
// Treating the body first.
+ /*
val body : Expr = if(KEEPLETS) {
matchToIfThenElse(funDef.getImplementation)
} else {
matchToIfThenElse(expandLets(funDef.getImplementation))
}
+ */
+ val body : Option[Expr] = if(KEEPLETS) {
+ funDef.body.map(b => matchToIfThenElse(b))
+ } else {
+ funDef.body.map(b => matchToIfThenElse(expandLets(b)))
+ }
val invocation : Expr = FunctionInvocation(funDef, funDef.args.map(_.toVariable))
+ /*
val invocationEqualsBody : Expr = {
val b : Expr = Equals(invocation, body)
if(PREPENDPRECONDS && funDef.hasPrecondition) {
@@ -181,11 +191,22 @@ object FunctionTemplate {
b
}
}
+ */
+ val invocationEqualsBody : Option[Expr] = body.map(body => {
+ val b : Expr = Equals(invocation, body)
+ if(PREPENDPRECONDS && funDef.hasPrecondition) {
+ Implies(prec.get, b)
+ } else {
+ b
+ }
+ })
val activatingBool : Identifier = FreshIdentifier("a", true).setType(BooleanType)
- val finalPred : Expr = rec(activatingBool, true, invocationEqualsBody)
- storeGuarded(activatingBool, true, finalPred)
+ //val finalPred : Expr = rec(activatingBool, true, invocationEqualsBody)
+ val finalPred : Option[Expr] = invocationEqualsBody.map(expr => rec(activatingBool, true, expr))
+ //storeGuarded(activatingBool, true, finalPred)
+ finalPred.foreach(p => storeGuarded(activatingBool, true, p))
// Now the postcondition.
if(funDef.hasPostcondition) {
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index b006520ebd0eee5b1d49861534d5dc686f8dea57..662ed9cc9e8ce207b004ecba81f83af41ea1446c 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -14,11 +14,11 @@ object ImperativeCodeElimination extends Pass {
def apply(pgm: Program): Program = {
val allFuns = pgm.definedFunctions
- allFuns.foreach(fd => {
+ allFuns.foreach(fd => fd.body.map(body => {
parent = fd
- val (res, scope, _) = toFunction(fd.getBody)
+ val (res, scope, _) = toFunction(body)
fd.body = Some(scope(res))
- })
+ }))
pgm
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 72623c96a2c732b4dac1995392545474c7f3f9c7..3d93d5972f95729d872c022ef418e760f6a61e1f 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -31,7 +31,7 @@ object Main {
}
private def defaultAction(program: Program, reporter: Reporter) : Unit = {
- val passManager = new PassManager(Seq(ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator))
+ val passManager = new PassManager(Seq(EpsilonElimination, ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator))
val program2 = passManager.run(program)
val analysis = new Analysis(program2, reporter)
analysis.analyse
diff --git a/src/main/scala/leon/PassManager.scala b/src/main/scala/leon/PassManager.scala
index f2830df79bfa129ce93d58157110a2107453595a..5381b7bee6a389ac120477c8316fcf1e97ccdc62 100644
--- a/src/main/scala/leon/PassManager.scala
+++ b/src/main/scala/leon/PassManager.scala
@@ -6,9 +6,9 @@ class PassManager(passes: Seq[Pass]) {
def run(program: Program): Program = {
passes.foldLeft(program)((pgm, pass) => {
- //println("Running Pass: " + pass.description)
+ println("Running Pass: " + pass.description)
val newPgm = pass(pgm)
- //println("Resulting program: " + newPgm)
+ println("Resulting program: " + newPgm)
newPgm
})
}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 797a209e57d08d863f24dcd5f97008d4fc875bf7..9e7055638b46d401a55d9a49866ad8bc0e7751e3 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -19,6 +19,7 @@ object Settings {
var pruneBranches : Boolean = false
var solverTimeout : Option[Int] = None
var luckyTest : Boolean = true
+ var verifyModel : Boolean = true
var useQuickCheck : Boolean = false
var useParallel : Boolean = false
// When this is None, use real integers
diff --git a/src/main/scala/leon/Simplificator.scala b/src/main/scala/leon/Simplificator.scala
index e8a7e2e005b68ce54a6482cb4a06f942d54ba58f..5562c75db5965e7d5f5916aa8923da065b1e3bb6 100644
--- a/src/main/scala/leon/Simplificator.scala
+++ b/src/main/scala/leon/Simplificator.scala
@@ -12,11 +12,10 @@ object Simplificator extends Pass {
def apply(pgm: Program): Program = {
val allFuns = pgm.definedFunctions
- allFuns.foreach(fd => {
- fd.body = Some(simplifyLets(fd.getBody))
- })
+ allFuns.foreach(fd => fd.body.map(body => {
+ fd.body = Some(simplifyLets(body))
+ }))
pgm
}
}
-
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index 7fe181fba57f7c80d0aa878896641b8195742485..2f5f1bc53fc000242758f19aee766cf175dadf84 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -32,9 +32,9 @@ object UnitElimination extends Pass {
//then apply recursively to the bodies
val newFuns = allFuns.flatMap(fd => if(fd.returnType == UnitType) Seq() else {
- val body = fd.getBody
+ val newBody = fd.body.map(body => removeUnit(body))
val newFd = fun2FreshFun(fd)
- newFd.body = Some(removeUnit(body))
+ newFd.body = newBody
Seq(newFd)
})
@@ -100,13 +100,13 @@ object UnitElimination extends Pass {
freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
fun2FreshFun += (fd -> freshFunDef)
- freshFunDef.body = Some(removeUnit(fd.getBody))
+ freshFunDef.body = fd.body.map(b => removeUnit(b))
val restRec = removeUnit(b)
fun2FreshFun -= fd
(freshFunDef, restRec)
} else {
fun2FreshFun += (fd -> fd)
- fd.body = Some(removeUnit(fd.getBody))
+ fd.body = fd.body.map(b => removeUnit(b))
val restRec = removeUnit(b)
fun2FreshFun -= fd
(fd, restRec)
diff --git a/src/main/scala/leon/Utils.scala b/src/main/scala/leon/Utils.scala
index 9ed8ef400ea0f143af078149c0d3b3034394c3a4..ae60002b693a0b74657fa8640a7eef56a641703f 100644
--- a/src/main/scala/leon/Utils.scala
+++ b/src/main/scala/leon/Utils.scala
@@ -10,6 +10,7 @@ object Utils {
implicit def any2IsValid(x: Boolean) : IsValid = new IsValid(x)
+ def epsilon[A](pred: (A) => Boolean): A = throw new RuntimeException("Implementation not supported")
object InvariantFunction {
def invariant(x: Boolean): Unit = ()
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index c418cdf4e4bb1f7fce36a2c8cce7ea1984855201..a0c7579410e87dfea059495303eadc5c555920ae 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -285,6 +285,11 @@ trait CodeExtraction extends Extractors {
case e: ImpureCodeEncounteredException => None
}
+ reqCont.map(e =>
+ if(containsLetDef(e)) {
+ unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
+ throw ImpureCodeEncounteredException(realBody)
+ })
funDef.body = bodyAttempt
funDef.precondition = reqCont
funDef.postcondition = ensCont
@@ -430,6 +435,11 @@ trait CodeExtraction extends Extractors {
case e: ImpureCodeEncounteredException => None
}
+ reqCont.map(e =>
+ if(containsLetDef(e)) {
+ unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
+ throw ImpureCodeEncounteredException(realBody)
+ })
funDef.body = bodyAttempt
funDef.precondition = reqCont
funDef.postcondition = ensCont
@@ -551,6 +561,17 @@ trait CodeExtraction extends Extractors {
}
}
}
+ case epsi@ExEpsilonExpression(tpe, varSym, predBody) => {
+ val pstpe = scalaType2PureScala(unit, silent)(tpe)
+ val previousVarSubst: Option[Function0[Expr]] = varSubsts.get(varSym) //save the previous in case of nested epsilon
+ varSubsts(varSym) = (() => EpsilonVariable((epsi.pos.line, epsi.pos.column)).setType(pstpe))
+ val c1 = rec(predBody)
+ previousVarSubst match {
+ case Some(f) => varSubsts(varSym) = f
+ case None => varSubsts.remove(varSym)
+ }
+ Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
+ }
case ExSomeConstruction(tpe, arg) => {
// println("Got Some !" + tpe + ":" + arg)
val underlying = scalaType2PureScala(unit, silent)(tpe)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 4bd9f9bf3bb34940a0bf0ea552a89df60b177ec3..78e66bf6c9ef5a2a8a1e0f23a2a3c4e30a85d19c 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -160,6 +160,22 @@ trait Extractors {
// }
//}
+
+ object ExEpsilonExpression {
+ def unapply(tree: Apply) : Option[(Type, Symbol, Tree)] = tree match {
+ case Apply(
+ TypeApply(Select(Select(funcheckIdent, utilsName), epsilonName), typeTree :: Nil),
+ Function((vd @ ValDef(_, _, _, EmptyTree)) :: Nil, predicateBody) :: Nil) => {
+ if (utilsName.toString == "Utils" && epsilonName.toString == "epsilon")
+ Some((typeTree.tpe, vd.symbol, predicateBody))
+ else
+ None
+ }
+ case _ => None
+ }
+ }
+
+
object ExValDef {
/** Extracts val's in the head of blocks. */
def unapply(tree: ValDef): Option[(Symbol,Tree,Tree)] = tree match {
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index 5de24fa44bbf489350371d2bce9775231ebf3e1d..3654de04ad807d2fd55a7470ce5c3fd97a131327 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -40,6 +40,7 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
" --quickcheck Use QuickCheck-like random search" + "\n" +
" --parallel Run all solvers in parallel" + "\n" +
" --noLuckyTests Do not perform additional tests to potentially find models early" + "\n" +
+ " --noverifymodel Do not verify the correctness of models returned by Z3" + "\n" +
" --verbose Print debugging informations"
)
@@ -63,6 +64,7 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
case "quickcheck" => leon.Settings.useQuickCheck = true
case "parallel" => leon.Settings.useParallel = true
case "noLuckyTests" => leon.Settings.luckyTest = false
+ case "noverifymodel" => leon.Settings.verifyModel = false
case "verbose" => leon.Settings.verbose = true
case s if s.startsWith("unrolling=") => leon.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("functions=") => leon.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 6f2038edeab63f6a2dcc0809d4b912429f55b5eb..d1a39f7172fafb612c2201b2c4322615a0aabdef 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -145,6 +145,15 @@ object PrettyPrinter {
sb.append("._" + i)
sb
}
+
+ case e@Epsilon(pred) => {
+ var nsb = sb
+ nsb.append("epsilon(x" + e.posIntInfo._1 + "_" + e.posIntInfo._2 + ". ")
+ nsb = pp(pred, nsb, lvl)
+ nsb.append(")")
+ nsb
+ }
+
case OptionSome(a) => {
var nsb = sb
nsb.append("Some(")
@@ -333,6 +342,7 @@ object PrettyPrinter {
}
case ResultVariable() => sb.append("#res")
+ case EpsilonVariable((row, col)) => sb.append("x" + row + "_" + col)
case Not(expr) => ppUnary(sb, expr, "\u00AC(", ")", lvl) // \neg
case e @ Error(desc) => {
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index ff0eeea21289861dffc5bcd4f24efefad73d0eb1..f9d0498f0fd46c867817778fb6ba9a845498755f 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -40,6 +40,8 @@ object Trees {
* the expected type. */
case class Error(description: String) extends Expr with Terminal with ScalacPositional
+ case class Epsilon(pred: Expr) extends Expr with ScalacPositional
+
/* Like vals */
case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr {
binder.markAsLetBinder
@@ -266,6 +268,8 @@ object Trees {
// represents the result in post-conditions
case class ResultVariable() extends Expr with Terminal
+ case class EpsilonVariable(pos: (Int, Int)) extends Expr with Terminal
+
/* Literals */
sealed abstract class Literal[T] extends Expr with Terminal {
val value: T
@@ -407,6 +411,7 @@ object Trees {
case CaseClassInstanceOf(cd, e) => Some((e, CaseClassInstanceOf(cd, _)))
case Assignment(id, e) => Some((e, Assignment(id, _)))
case TupleSelect(t, i) => Some((t, TupleSelect(_, i)))
+ case e@Epsilon(t) => Some((t, (expr: Expr) => Epsilon(expr).setType(e.getType).setPosInfo(e)))
case _ => None
}
}
@@ -751,7 +756,10 @@ object Trees {
def rec(expr: Expr) : A = expr match {
case l @ Let(_, e, b) => compute(l, combine(rec(e), rec(b)))
case l @ LetVar(_, e, b) => compute(l, combine(rec(e), rec(b)))
- case l @ LetDef(fd, b) => compute(l, combine(rec(fd.getBody), rec(b))) //TODO, still not sure about the semantic
+ case l @ LetDef(fd, b) => {//TODO, still not sure about the semantic
+ val exprs: Seq[Expr] = fd.precondition.toSeq ++ fd.body.toSeq ++ fd.postcondition.toSeq ++ Seq(b)
+ compute(l, exprs.map(rec(_)).reduceLeft(combine))
+ }
case n @ NAryOperator(args, _) => {
if(args.size == 0)
compute(n, convert(n))
@@ -810,6 +818,19 @@ object Trees {
treeCatamorphism(convert, combine, compute, expr)
}
+ def containsLetDef(expr: Expr): Boolean = {
+ def convert(t : Expr) : Boolean = t match {
+ case (l : LetDef) => true
+ case _ => false
+ }
+ def combine(c1 : Boolean, c2 : Boolean) : Boolean = c1 || c2
+ def compute(t : Expr, c : Boolean) = t match {
+ case (l : LetDef) => true
+ case _ => c
+ }
+ treeCatamorphism(convert, combine, compute, expr)
+ }
+
def variablesOf(expr: Expr) : Set[Identifier] = {
def convert(t: Expr) : Set[Identifier] = t match {
case Variable(i) => Set(i)