diff --git a/.gitignore b/.gitignore
index df8c680efb2df4ec5850d58b035038c36afacf36..bfbd461b232f026844f5d7d6fd2b5fb7647fa941 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,4 @@ project/boot
project/build
project/target
target
+/leon
diff --git a/run-tests.sh b/run-tests.sh
new file mode 100755
index 0000000000000000000000000000000000000000..f1e606a6e76685d6911359614424fe53b01b34d9
--- /dev/null
+++ b/run-tests.sh
@@ -0,0 +1,35 @@
+#!/bin/sh
+
+nbtests=$(ls -l testcases/regression/*valid/*.scala | wc -l)
+nbsuccess=0
+failedtests=""
+
+for f in testcases/regression/valid/*.scala; do
+ echo -n "Running $f, expecting VALID, got: "
+ res=`./leon --timeout=5 --oneline "$f"`
+ echo $res | tr [a-z] [A-Z]
+ if [ $res = valid ]; then
+ nbsuccess=$((nbsuccess + 1))
+ else
+ failedtests="$failedtests $f"
+ fi
+done
+
+for f in testcases/regression/invalid/*.scala; do
+ echo -n "Running $f, expecting INVALID, got: "
+ res=`./leon --timeout=5 --oneline "$f"`
+ echo $res | tr [a-z] [A-Z]
+ if [ $res = invalid ]; then
+ nbsuccess=$((nbsuccess + 1))
+ else
+ failedtests="$failedtests $f"
+ fi
+done
+
+echo "$nbsuccess out of $nbtests tests were successful"
+if [ $nbtests -eq $nbsuccess ]; then
+ echo "PASSED"
+else
+ echo "ERROR. The following test did not run as expected:"
+ for f in $failedtests; do echo $f; done
+fi
diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index 40468a4bef174cd93278452a038cc2b711710328..8c950fd87215da16ebdebc1b13c88dbb78ba66e3 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -7,7 +7,7 @@ import purescala.TypeTrees._
import Extensions._
import scala.collection.mutable.{Set => MutableSet}
-class Analysis(val program: Program, val reporter: Reporter = Settings.reporter) {
+class Analysis(val program : Program, val reporter: Reporter = Settings.reporter) {
Extensions.loadAll(reporter)
val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions
@@ -63,14 +63,17 @@ class Analysis(val program: Program, val reporter: Reporter = Settings.reporter)
defaultTactic
}
- def vcSort(vc1: VerificationCondition, vc2: VerificationCondition) : Boolean = (vc1 < vc2)
-
if(funDef.body.isDefined) {
- allVCs ++= tactic.generatePreconditions(funDef).sortWith(vcSort)
- allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef).sortWith(vcSort)
- allVCs ++= tactic.generatePostconditions(funDef).sortWith(vcSort)
- allVCs ++= tactic.generateMiscCorrectnessConditions(funDef).sortWith(vcSort)
+ allVCs ++= tactic.generatePreconditions(funDef)
+ allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
+ allVCs ++= tactic.generatePostconditions(funDef)
+ allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
}
+ allVCs = allVCs.sortWith((vc1, vc2) => {
+ val id1 = vc1.funDef.id.name
+ val id2 = vc2.funDef.id.name
+ if(id1 != id2) id1 < id2 else vc1 < vc2
+ })
}
val notFound: Set[String] = Settings.functionsToAnalyse -- analysedFunctions
@@ -148,6 +151,14 @@ class Analysis(val program: Program, val reporter: Reporter = Settings.reporter)
)
reporter.info(summaryString)
+ if(Settings.simpleOutput) {
+ val outStr =
+ if(vcs.forall(_.status == "valid")) "valid"
+ else if(vcs.exists(_.status == "invalid")) "invalid"
+ else "unknown"
+ println(outStr)
+ }
+
// Printing summary for the evaluation section of paper:
val writeSummary = false
if (writeSummary) {
diff --git a/src/main/scala/leon/DefaultTactic.scala b/src/main/scala/leon/DefaultTactic.scala
index 6f31b9ff59bc4b4681e7284c4dc3479400585534..a01d025431c2ec3c704a1950410334fd322abae9 100644
--- a/src/main/scala/leon/DefaultTactic.scala
+++ b/src/main/scala/leon/DefaultTactic.scala
@@ -78,7 +78,10 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
expr2
}
}
- Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
+ if(functionDefinition.fromLoop)
+ Seq(new VerificationCondition(theExpr, functionDefinition.parent.get, VCKind.InvariantPost, this.asInstanceOf[DefaultTactic]).setPosInfo(functionDefinition))
+ else
+ Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
}
}
@@ -107,11 +110,18 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
val newBody : Expr = replace(substMap, prec)
val newCall : Expr = (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e))
- new VerificationCondition(
- withPrecIfDefined(path, newCall),
- function,
- VCKind.Precondition,
- this.asInstanceOf[DefaultTactic]).setPosInfo(fi)
+ if(fd.fromLoop)
+ new VerificationCondition(
+ withPrecIfDefined(path, newCall),
+ fd.parent.get,
+ if(fd == function) VCKind.InvariantInd else VCKind.InvariantInit,
+ this.asInstanceOf[DefaultTactic]).setPosInfo(fd)
+ else
+ new VerificationCondition(
+ withPrecIfDefined(path, newCall),
+ function,
+ VCKind.Precondition,
+ this.asInstanceOf[DefaultTactic]).setPosInfo(fi)
}).toSeq
} else {
Seq.empty
@@ -141,7 +151,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
allPathConds.map(pc =>
new VerificationCondition(
withPrecIfDefined(pc._1),
- function,
+ if(function.fromLoop) function.parent.get else function,
VCKind.ExhaustiveMatch,
this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
).toSeq
@@ -173,7 +183,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
allPathConds.map(pc =>
new VerificationCondition(
withPrecIfDefined(pc._1),
- function,
+ if(function.fromLoop) function.parent.get else function,
VCKind.MapAccess,
this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
).toSeq
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..e8409aa317356679938accb064985c284e1e0e23 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 ImpossibleComputation() 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 ImpossibleComputationEx() 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 ImpossibleComputationEx()
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 ImpossibleComputationEx() => ImpossibleComputation()
}
}
}
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 51330a3e37232eb761f74ac594363bd93990c69d..919b5b4f9740768bb6c8aeba5686b19966027df2 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 ImpossibleComputation() => {
+ reporter.info("- Invalid Model: the model could not be verified because of insufficient information.")
+ (false, asMap)
+ }
case other => {
reporter.error("Something went wrong. While evaluating the model, we got this: " + other)
(false, asMap)
@@ -978,6 +1010,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
case errorType => scala.sys.error("Unexpected type for singleton map: " + (ex, errorType))
}
case e @ EmptyMap(fromType, toType) => {
+ typeToSort(e.getType) //had to add this here because the mapRangeNoneConstructors was not yet constructed...
val fromSort = typeToSort(fromType)
val toSort = typeToSort(toType)
z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())
@@ -1226,7 +1259,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
val startingVar : Identifier = FreshIdentifier("start", true).setType(BooleanType)
val result = treatFunctionInvocationSet(startingVar, true, functionCallsOf(formula))
- reporter.info(result)
+ //reporter.info(result)
(Variable(startingVar) +: formula +: result._1, result._2)
}
}
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d9426510ee76f9703514df4219cff8761db26995
--- /dev/null
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -0,0 +1,148 @@
+package leon
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
+
+object FunctionClosure extends Pass {
+
+ val description = "Closing function with its scoping variables"
+
+ private var enclosingPreconditions: List[Expr] = Nil
+
+ private var pathConstraints: List[Expr] = Nil
+ private var newFunDefs: Map[FunDef, FunDef] = Map()
+
+ def apply(program: Program): Program = {
+ newFunDefs = Map()
+ val funDefs = program.definedFunctions
+ funDefs.foreach(fd => {
+ enclosingPreconditions = fd.precondition.toList
+ pathConstraints = fd.precondition.toList
+ 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
+ }
+
+ private def functionClosure(expr: Expr, bindedVars: Set[Identifier]): Expr = expr match {
+ case l @ LetDef(fd, rest) => {
+
+ val id = fd.id
+ val rt = fd.returnType
+ val varDecl = fd.args
+ val precondition = fd.precondition
+ val postcondition = fd.postcondition
+
+ 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
+
+ val freshVars: Map[Identifier, Identifier] = capturedVarsWithConstraints.map(v => (v, FreshIdentifier(v.name).setType(v.getType))).toMap
+ val freshVarsExpr: Map[Expr, Expr] = freshVars.map(p => (p._1.toVariable, p._2.toVariable))
+
+ val extraVarDecls = freshVars.map{ case (_, v2) => VarDecl(v2, v2.getType) }
+ val newVarDecls = varDecl ++ extraVarDecls
+ val newFunId = FreshIdentifier(id.name)
+ val newFunDef = new FunDef(newFunId, rt, newVarDecls).setPosInfo(fd)
+ newFunDef.fromLoop = fd.fromLoop
+ newFunDef.parent = fd.parent
+ newFunDef.addAnnotation(fd.annotations.toSeq:_*)
+
+ 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))
+
+ 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 oldPathConstraints = pathConstraints
+ pathConstraints = (precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints).map(e => replace(freshVarsExpr, e))
+ 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))
+ pathConstraints = oldPathConstraints
+
+ newFunDef.precondition = recPrecondition
+ newFunDef.body = recBody
+ newFunDef.postcondition = freshPostcondition
+
+ 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 = searchAndReplaceDFS(substFunInvocInRest)(functionClosure(rest, bindedVars))
+ LetDef(newFunDef, recRest).setType(l.getType)
+ }
+ case l @ Let(i,e,b) => {
+ val re = functionClosure(e, bindedVars)
+ pathConstraints ::= Equals(Variable(i), re)
+ val rb = functionClosure(b, bindedVars + i)
+ pathConstraints = pathConstraints.tail
+ Let(i, re, rb).setType(l.getType)
+ }
+ case n @ NAryOperator(args, recons) => {
+ var change = false
+ val rargs = args.map(a => functionClosure(a, bindedVars))
+ recons(rargs).setType(n.getType)
+ }
+ case b @ BinaryOperator(t1,t2,recons) => {
+ val r1 = functionClosure(t1, bindedVars)
+ val r2 = functionClosure(t2, bindedVars)
+ recons(r1,r2).setType(b.getType)
+ }
+ case u @ UnaryOperator(t,recons) => {
+ val r = functionClosure(t, bindedVars)
+ recons(r).setType(u.getType)
+ }
+ case i @ IfExpr(cond,then,elze) => {
+ val rCond = functionClosure(cond, bindedVars)
+ pathConstraints ::= rCond
+ val rThen = functionClosure(then, bindedVars)
+ pathConstraints = pathConstraints.tail
+ pathConstraints ::= Not(rCond)
+ val rElze = functionClosure(elze, bindedVars)
+ pathConstraints = pathConstraints.tail
+ IfExpr(rCond, rThen, rElze).setType(i.getType)
+ }
+ case m @ MatchExpr(scrut,cses) => { //TODO: will not work if there are actual nested function in cases
+ //val rScrut = functionClosure(scrut, bindedVars)
+ m
+ }
+ case t if t.isInstanceOf[Terminal] => t
+ case unhandled => scala.sys.error("Non-terminal case should be handled in FunctionClosure: " + unhandled)
+ }
+
+ //filter the list of constraints, only keeping those relevant to the set of variables
+ def filterConstraints(vars: Set[Identifier]): (List[Expr], Set[Identifier]) = {
+ var allVars = vars
+ var newVars: Set[Identifier] = Set()
+ var constraints = pathConstraints
+ var filteredConstraints: List[Expr] = Nil
+ do {
+ allVars ++= newVars
+ newVars = Set()
+ constraints = pathConstraints.filterNot(filteredConstraints.contains(_))
+ constraints.foreach(expr => {
+ val vs = variablesOf(expr)
+ if(!vs.intersect(allVars).isEmpty) {
+ filteredConstraints ::= expr
+ newVars ++= vs.diff(allVars)
+ }
+ })
+ } while(newVars != Set())
+ (filteredConstraints, allVars)
+ }
+
+}
diff --git a/src/main/scala/leon/FunctionHoisting.scala b/src/main/scala/leon/FunctionHoisting.scala
new file mode 100644
index 0000000000000000000000000000000000000000..37bc69c41fa12e41c94b3c8d876631f8e3f47220
--- /dev/null
+++ b/src/main/scala/leon/FunctionHoisting.scala
@@ -0,0 +1,103 @@
+package leon
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
+
+object FunctionHoisting extends Pass {
+
+ val description = "Hoist function at the top level"
+
+ def apply(program: Program): Program = {
+ val funDefs = program.definedFunctions
+ var topLevelFuns: Set[FunDef] = Set()
+ funDefs.foreach(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()
+ }
+ topLevelFuns ++= (s2 ++ s4)
+ })
+ val Program(id, ObjectDef(objId, defs, invariants)) = program
+ Program(id, ObjectDef(objId, defs ++ topLevelFuns, invariants))
+ }
+
+ private def hoist(expr: Expr): (Expr, Set[FunDef]) = expr match {
+ case l @ LetDef(fd, rest) => {
+ val (e, s) = hoist(rest)
+ 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)
+ val (rb, s2) = hoist(b)
+ (Let(i, re, rb), s1 ++ s2)
+ }
+ case n @ NAryOperator(args, recons) => {
+ val rargs = args.map(a => hoist(a))
+ (recons(rargs.map(_._1)).setType(n.getType), rargs.flatMap(_._2).toSet)
+ }
+ case b @ BinaryOperator(t1,t2,recons) => {
+ val (r1, s1) = hoist(t1)
+ val (r2, s2) = hoist(t2)
+ (recons(r1,r2).setType(b.getType), s1 ++ s2)
+ }
+ case u @ UnaryOperator(t,recons) => {
+ val (r, s) = hoist(t)
+ (recons(r).setType(u.getType), s)
+ }
+ case i @ IfExpr(t1,t2,t3) => {
+ val (r1, s1) = hoist(t1)
+ val (r2, s2) = hoist(t2)
+ val (r3, s3) = hoist(t3)
+ (IfExpr(r1, r2, r3).setType(i.getType), s1 ++ s2 ++ s3)
+ }
+ case m @ MatchExpr(scrut,cses) => {
+ val (scrutRes, scrutSet) = hoist(scrut)
+ val (csesRes, csesSets) = cses.map{
+ case SimpleCase(pat, rhs) => {
+ val (r, s) = hoist(rhs)
+ (SimpleCase(pat, r), s)
+ }
+ case GuardedCase(pat, guard, rhs) => {
+ val (r, s) = hoist(rhs)
+ (GuardedCase(pat, guard, r), s)
+ }
+ }.unzip
+ (MatchExpr(scrutRes, csesRes).setType(m.getType).setPosInfo(m), csesSets.toSet.flatten ++ scrutSet)
+ }
+ case t if t.isInstanceOf[Terminal] => (t, Set())
+ case unhandled => scala.sys.error("Non-terminal case should be handled in FunctionHoisting: " + unhandled)
+ }
+
+}
+
+// vim: set ts=4 sw=4 et:
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
new file mode 100644
index 0000000000000000000000000000000000000000..eb139f824166e44feda604bd36976689a3ae7541
--- /dev/null
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -0,0 +1,267 @@
+package leon
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
+
+object ImperativeCodeElimination extends Pass {
+
+ val description = "Transform imperative constructs into purely functional code"
+
+ private var varInScope = Set[Identifier]()
+ private var parent: FunDef = null //the enclosing fundef
+
+ def apply(pgm: Program): Program = {
+ val allFuns = pgm.definedFunctions
+ allFuns.foreach(fd => fd.body.map(body => {
+ Logger.debug("Transforming to functional code the following function:\n" + fd, 5, "imperative")
+ parent = fd
+ val (res, scope, _) = toFunction(body)
+ fd.body = Some(scope(res))
+ Logger.debug("Resulting functional code is:\n" + fd, 5, "imperative")
+ }))
+ pgm
+ }
+
+ //return a "scope" consisting of purely functional code that defines potentially needed
+ //new variables (val, not var) and a mapping for each modified variable (var, not val :) )
+ //to their new name defined in the scope. The first returned valued is the value of the expression
+ //that should be introduced as such in the returned scope (the val already refers to the new names)
+ private def toFunction(expr: Expr): (Expr, Expr => Expr, Map[Identifier, Identifier]) = {
+ val res = expr match {
+ case LetVar(id, e, b) => {
+ val newId = FreshIdentifier(id.name).setType(id.getType)
+ val (rhsVal, rhsScope, rhsFun) = toFunction(e)
+ varInScope += id
+ val (bodyRes, bodyScope, bodyFun) = toFunction(b)
+ varInScope -= id
+ val scope = (body: Expr) => rhsScope(Let(newId, rhsVal, replaceNames(rhsFun + (id -> newId), bodyScope(body))))
+ (bodyRes, scope, (rhsFun + (id -> newId)) ++ bodyFun)
+ }
+ case Assignment(id, e) => {
+ assert(varInScope.contains(id))
+ val newId = FreshIdentifier(id.name).setType(id.getType)
+ val (rhsVal, rhsScope, rhsFun) = toFunction(e)
+ val scope = (body: Expr) => rhsScope(Let(newId, rhsVal, body))
+ (UnitLiteral, scope, rhsFun + (id -> newId))
+ }
+
+ case ite@IfExpr(cond, tExpr, eExpr) => {
+ val (cRes, cScope, cFun) = toFunction(cond)
+ val (tRes, tScope, tFun) = toFunction(tExpr)
+ val (eRes, eScope, eFun) = toFunction(eExpr)
+
+ val modifiedVars: Seq[Identifier] = (tFun.keys ++ eFun.keys).toSet.intersect(varInScope).toSeq
+ val resId = FreshIdentifier("res").setType(ite.getType)
+ val freshIds = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
+ val iteType = if(modifiedVars.isEmpty) resId.getType else TupleType(resId.getType +: freshIds.map(_.getType))
+
+ val thenVal = if(modifiedVars.isEmpty) tRes else Tuple(tRes +: modifiedVars.map(vId => tFun.get(vId) match {
+ case Some(newId) => newId.toVariable
+ case None => vId.toVariable
+ })).setType(iteType)
+
+ val elseVal = if(modifiedVars.isEmpty) eRes else Tuple(eRes +: modifiedVars.map(vId => eFun.get(vId) match {
+ case Some(newId) => newId.toVariable
+ case None => vId.toVariable
+ })).setType(iteType)
+
+ val iteExpr = IfExpr(cRes, replaceNames(cFun, tScope(thenVal)), replaceNames(cFun, eScope(elseVal))).setType(iteType)
+
+ val scope = ((body: Expr) => {
+ val tupleId = FreshIdentifier("t").setType(iteType)
+ cScope(
+ Let(tupleId, iteExpr,
+ if(freshIds.isEmpty)
+ Let(resId, tupleId.toVariable, body)
+ else
+ Let(resId, TupleSelect(tupleId.toVariable, 1),
+ freshIds.zipWithIndex.foldLeft(body)((b, id) =>
+ Let(id._1,
+ TupleSelect(tupleId.toVariable, id._2 + 2).setType(id._1.getType),
+ b)))))
+ })
+
+ (resId.toVariable, scope, cFun ++ modifiedVars.zip(freshIds).toMap)
+ }
+
+ case m @ MatchExpr(scrut, cses) => {
+ val csesRhs = cses.map(_.rhs) //we can ignore pattern, and the guard is required to be pure
+ val (csesRes, csesScope, csesFun) = csesRhs.map(toFunction).unzip3
+ val (scrutRes, scrutScope, scrutFun) = toFunction(scrut)
+
+ val modifiedVars: Seq[Identifier] = csesFun.toSet.flatMap((m: Map[Identifier, Identifier]) => m.keys).intersect(varInScope).toSeq
+ val resId = FreshIdentifier("res").setType(m.getType)
+ val freshIds = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
+ val matchType = if(modifiedVars.isEmpty) resId.getType else TupleType(resId.getType +: freshIds.map(_.getType))
+
+ val csesVals = csesRes.zip(csesFun).map{
+ case (cRes, cFun) => if(modifiedVars.isEmpty) cRes else Tuple(cRes +: modifiedVars.map(vId => cFun.get(vId) match {
+ case Some(newId) => newId.toVariable
+ case None => vId.toVariable
+ })).setType(matchType)
+ }
+
+ val newRhs = csesVals.zip(csesScope).map{
+ case (cVal, cScope) => replaceNames(scrutFun, cScope(cVal))
+ }
+ val matchExpr = MatchExpr(scrutRes, cses.zip(newRhs).map{
+ case (SimpleCase(pat, _), newRhs) => SimpleCase(pat, newRhs)
+ case (GuardedCase(pat, guard, _), newRhs) => GuardedCase(pat, replaceNames(scrutFun, guard), newRhs)
+ }).setType(matchType).setPosInfo(m)
+
+ val scope = ((body: Expr) => {
+ val tupleId = FreshIdentifier("t").setType(matchType)
+ scrutScope(
+ Let(tupleId, matchExpr,
+ if(freshIds.isEmpty)
+ Let(resId, tupleId.toVariable, body)
+ else
+ Let(resId, TupleSelect(tupleId.toVariable, 1),
+ freshIds.zipWithIndex.foldLeft(body)((b, id) =>
+ Let(id._1,
+ TupleSelect(tupleId.toVariable, id._2 + 2).setType(id._1.getType),
+ b)))))
+ })
+
+ (resId.toVariable, scope, scrutFun ++ modifiedVars.zip(freshIds).toMap)
+ }
+ case wh@While(cond, body) => {
+ val (condRes, condScope, condFun) = toFunction(cond)
+ val (_, bodyScope, bodyFun) = toFunction(body)
+ val condBodyFun = condFun ++ bodyFun
+
+ val modifiedVars: Seq[Identifier] = condBodyFun.keys.toSet.intersect(varInScope).toSeq
+
+ if(modifiedVars.isEmpty)
+ (UnitLiteral, (b: Expr) => b, Map())
+ else {
+ val whileFunVars = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
+ val modifiedVars2WhileFunVars = modifiedVars.zip(whileFunVars).toMap
+ val whileFunVarDecls = whileFunVars.map(id => VarDecl(id, id.getType))
+ val whileFunReturnType = if(whileFunVars.size == 1) whileFunVars.head.getType else TupleType(whileFunVars.map(_.getType))
+ val whileFunDef = new FunDef(FreshIdentifier("while"), whileFunReturnType, whileFunVarDecls).setPosInfo(wh)
+ whileFunDef.fromLoop = true
+ whileFunDef.parent = Some(parent)
+
+ val whileFunCond = condRes
+ val whileFunRecursiveCall = replaceNames(condFun,
+ bodyScope(FunctionInvocation(whileFunDef, modifiedVars.map(id => condBodyFun(id).toVariable)).setPosInfo(wh)))
+ val whileFunBaseCase =
+ (if(whileFunVars.size == 1)
+ condFun.get(modifiedVars.head).getOrElse(whileFunVars.head).toVariable
+ else
+ Tuple(modifiedVars.map(id => condFun.get(id).getOrElse(modifiedVars2WhileFunVars(id)).toVariable))
+ ).setType(whileFunReturnType)
+ val whileFunBody = replaceNames(modifiedVars2WhileFunVars,
+ condScope(IfExpr(whileFunCond, whileFunRecursiveCall, whileFunBaseCase).setType(whileFunReturnType)))
+ whileFunDef.body = Some(whileFunBody)
+
+ val resVar = ResultVariable().setType(whileFunReturnType)
+ val whileFunVars2ResultVars: Map[Expr, Expr] =
+ if(whileFunVars.size == 1)
+ Map(whileFunVars.head.toVariable -> resVar)
+ else
+ whileFunVars.zipWithIndex.map{ case (v, i) => (v.toVariable, TupleSelect(resVar, i+1).setType(v.getType)) }.toMap
+ val modifiedVars2ResultVars: Map[Expr, Expr] = modifiedVars.map(id =>
+ (id.toVariable, whileFunVars2ResultVars(modifiedVars2WhileFunVars(id).toVariable))).toMap
+
+ //the mapping of the trivial post condition variables depends on whether the condition has had some side effect
+ val trivialPostcondition: Option[Expr] = Some(Not(replace(
+ modifiedVars.map(id => (condFun.get(id).getOrElse(id).toVariable, modifiedVars2ResultVars(id.toVariable))).toMap,
+ whileFunCond)))
+ val invariantPrecondition: Option[Expr] = wh.invariant.map(expr => replaceNames(modifiedVars2WhileFunVars, expr))
+ val invariantPostcondition: Option[Expr] = wh.invariant.map(expr => replace(modifiedVars2ResultVars, expr))
+ whileFunDef.precondition = invariantPrecondition
+ whileFunDef.postcondition = trivialPostcondition.map(expr =>
+ And(expr, invariantPostcondition match {
+ case Some(e) => e
+ case None => BooleanLiteral(true)
+ }))
+
+ val finalVars = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
+ val finalScope = ((body: Expr) => {
+ val tupleId = FreshIdentifier("t").setType(whileFunReturnType)
+ LetDef(
+ whileFunDef,
+ Let(tupleId,
+ FunctionInvocation(whileFunDef, modifiedVars.map(_.toVariable)).setPosInfo(wh),
+ if(finalVars.size == 1)
+ Let(finalVars.head, tupleId.toVariable, body)
+ else
+ finalVars.zipWithIndex.foldLeft(body)((b, id) =>
+ Let(id._1,
+ TupleSelect(tupleId.toVariable, id._2 + 1).setType(id._1.getType),
+ b))))
+ })
+
+ (UnitLiteral, finalScope, modifiedVars.zip(finalVars).toMap)
+ }
+ }
+
+ case Block(Seq(), expr) => toFunction(expr)
+ case Block(exprs, expr) => {
+ val (scope, fun) = exprs.foldRight((body: Expr) => body, Map[Identifier, Identifier]())((e, acc) => {
+ val (accScope, accFun) = acc
+ val (_, rScope, rFun) = toFunction(e)
+ val scope = (body: Expr) => rScope(replaceNames(rFun, accScope(body)))
+ (scope, rFun ++ accFun)
+ })
+ val (lastRes, lastScope, lastFun) = toFunction(expr)
+ val finalFun = fun ++ lastFun
+ (replaceNames(finalFun, lastRes),
+ (body: Expr) => scope(replaceNames(fun, lastScope(body))),
+ finalFun)
+ }
+
+ //pure expression (that could still contain side effects as a subexpression) (evaluation order is from left to right)
+ case Let(id, e, b) => {
+ val (bindRes, bindScope, bindFun) = toFunction(e)
+ val (bodyRes, bodyScope, bodyFun) = toFunction(b)
+ (bodyRes,
+ (b2: Expr) => bindScope(Let(id, bindRes, replaceNames(bindFun, bodyScope(b2)))),
+ bindFun ++ bodyFun)
+ }
+ case LetDef(fd, b) => {
+ //Recall that here the nested function should not access mutable variables from an outside scope
+ val (bodyRes, bodyScope, bodyFun) = toFunction(b)
+ (bodyRes, (b2: Expr) => LetDef(fd, bodyScope(b2)), bodyFun)
+ }
+ case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
+ case n @ NAryOperator(args, recons) => {
+ val (recArgs, scope, fun) = args.foldRight((Seq[Expr](), (body: Expr) => body, Map[Identifier, Identifier]()))((arg, acc) => {
+ val (accArgs, accScope, accFun) = acc
+ val (argVal, argScope, argFun) = toFunction(arg)
+ val newScope = (body: Expr) => argScope(replaceNames(argFun, accScope(body)))
+ (argVal +: accArgs, newScope, argFun ++ accFun)
+ })
+ (recons(recArgs).setType(n.getType), scope, fun)
+ }
+ case b @ BinaryOperator(a1, a2, recons) => {
+ val (argVal1, argScope1, argFun1) = toFunction(a1)
+ val (argVal2, argScope2, argFun2) = toFunction(a2)
+ val scope = (body: Expr) => {
+ val rhs = argScope2(replaceNames(argFun2, body))
+ val lhs = argScope1(replaceNames(argFun1, rhs))
+ lhs
+ }
+ (recons(argVal1, argVal2).setType(b.getType), scope, argFun1 ++ argFun2)
+ }
+ case u @ UnaryOperator(a, recons) => {
+ val (argVal, argScope, argFun) = toFunction(a)
+ (recons(argVal).setType(u.getType), argScope, argFun)
+ }
+ case (t: Terminal) => (t, (body: Expr) => body, Map())
+
+
+ case _ => sys.error("not supported: " + expr)
+ }
+ //val codeRepresentation = res._2(Block(res._3.map{ case (id1, id2) => Assignment(id1, id2.toVariable)}.toSeq, res._1))
+ //println("res of toFunction on: " + expr + " IS: " + codeRepresentation)
+ res.asInstanceOf[(Expr, (Expr) => Expr, Map[Identifier, Identifier])] //need cast because it seems that res first map type is _ <: Identifier instead of Identifier
+ }
+
+ def replaceNames(fun: Map[Identifier, Identifier], expr: Expr) = replace(fun.map(ids => (ids._1.toVariable, ids._2.toVariable)), expr)
+
+}
diff --git a/src/main/scala/leon/InductionTactic.scala b/src/main/scala/leon/InductionTactic.scala
index 5e14f196318a74a53761f17dd9a8b06bd9c63f78..1d30adddf62825cf8184c9eb42aa8677bb28134f 100644
--- a/src/main/scala/leon/InductionTactic.scala
+++ b/src/main/scala/leon/InductionTactic.scala
@@ -65,8 +65,8 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
new VerificationCondition(Implies(CaseClassInstanceOf(ccd, argAsVar), conditionForChild), funDef, VCKind.Postcondition, this)
case _ => scala.sys.error("Abstract class has non-case class subtype.")
}))
- println("Induction tactic yields the following VCs:")
- println(conditionsForEachChild.map(vc => vc.condition).mkString("\n"))
+ Logger.debug("Induction tactic yields the following VCs:\n" +
+ conditionsForEachChild.map(vc => vc.condition).mkString("\n"), 4, "induction")
conditionsForEachChild
}
case None =>
@@ -131,8 +131,8 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
}
case _ => scala.sys.error("Abstract class has non-case class subtype")
}))
- println("Induction tactic yields the following VCs:")
- println(conditionsForEachChild.map(vc => vc.condition).mkString("\n"))
+ Logger.debug("Induction tactic yields the following VCs:\n" +
+ conditionsForEachChild.map(vc => vc.condition).mkString("\n"), 4, "induction")
conditionsForEachChild
}).toSeq
@@ -140,10 +140,6 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
} else {
Seq.empty
}
-
- // println("PRECS VCs FOR " + function.id.name)
- // println(toRet.toList.map(vc => vc.posInfo + " -- " + vc.condition).mkString("\n\n"))
-
toRet
}
case None => {
diff --git a/src/main/scala/leon/Logger.scala b/src/main/scala/leon/Logger.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fc4942535112af7037660c4e7608ade80d1395dc
--- /dev/null
+++ b/src/main/scala/leon/Logger.scala
@@ -0,0 +1,24 @@
+package leon
+
+object Logger {
+
+ //the debug level to display, from 0 (no debug information) to 5 (very verbose)
+ //var level = 0
+
+ //each debug information is tagged by a string, the tag variable only display the message with a tag in this set
+ //if the set is empty then all tags are displayed
+ //var tags: Set[String] = Set()
+
+ val defaultTag = "main"
+
+ private def output(msg: String, lvl: Int, tag: String) {
+ if(lvl <= Settings.debugLevel) {
+ if(Settings.debugTags.isEmpty || Settings.debugTags.contains(tag)) {
+ println("DEBUG: [" + tag + "] " + msg)
+ }
+ }
+ }
+
+ def debug(msg: String, lvl: Int, tag: String = defaultTag) = output(msg, lvl, tag)
+
+}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index aefcf528a0c83593f806374bdc21688c5d2a15bc..e9818f16debfb19ccdbeaec6f1212f169918990f 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -31,7 +31,10 @@ object Main {
}
private def defaultAction(program: Program, reporter: Reporter) : Unit = {
- val analysis = new Analysis(program, reporter)
+ Logger.debug("Default action on program: " + program, 3, "main")
+ 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/Pass.scala b/src/main/scala/leon/Pass.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4bbc88856c20b96bd5c9c3fd9e1815b57b85d976
--- /dev/null
+++ b/src/main/scala/leon/Pass.scala
@@ -0,0 +1,14 @@
+package leon
+
+import purescala.Definitions._
+
+abstract class Pass {
+
+ def apply(pgm: Program): Program
+
+ val description: String
+
+
+ //Maybe adding some dependency declaration and tree checking methods
+
+}
diff --git a/src/main/scala/leon/PassManager.scala b/src/main/scala/leon/PassManager.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bebd985778beeda1a7995ebb9917712aa7403e25
--- /dev/null
+++ b/src/main/scala/leon/PassManager.scala
@@ -0,0 +1,16 @@
+package leon
+
+import purescala.Definitions._
+
+class PassManager(passes: Seq[Pass]) {
+
+ def run(program: Program): Program = {
+ passes.foldLeft(program)((pgm, pass) => {
+ Logger.debug("Running Pass: " + pass.description, 1, "passman")
+ val newPgm = pass(pgm)
+ Logger.debug("Resulting program: " + newPgm, 3, "passman")
+ newPgm
+ })
+ }
+
+}
diff --git a/src/main/scala/leon/RandomSolver.scala b/src/main/scala/leon/RandomSolver.scala
index f153818924cd47d79f7470b8487767df5f30f7bc..4cee5b06181bbc803cc2061af9f62c33c5d04386 100644
--- a/src/main/scala/leon/RandomSolver.scala
+++ b/src/main/scala/leon/RandomSolver.scala
@@ -10,8 +10,6 @@ import Evaluator._
import scala.util.Random
-import scala.sys.error
-
class RandomSolver(reporter: Reporter, val nbTrial: Option[Int] = None) extends Solver(reporter) {
require(nbTrial.forall(i => i >= 0))
@@ -68,13 +66,14 @@ class RandomSolver(reporter: Reporter, val nbTrial: Option[Int] = None) extends
case AnyType => randomValue(randomType(), size)
case SetType(base) => EmptySet(base)
case MultisetType(base) => EmptyMultiset(base)
- case Untyped => error("I don't know what to do")
- case BottomType => error("I don't know what to do")
- case ListType(base) => error("I don't know what to do")
- case TupleType(bases) => error("I don't know what to do")
- case MapType(from, to) => error("I don't know what to do")
- case OptionType(base) => error("I don't know what to do")
- case f: FunctionType => error("I don't know what to do")
+ case Untyped => sys.error("I don't know what to do")
+ case BottomType => sys.error("I don't know what to do")
+ case ListType(base) => sys.error("I don't know what to do")
+ case TupleType(bases) => sys.error("I don't know what to do")
+ case MapType(from, to) => sys.error("I don't know what to do")
+ case OptionType(base) => sys.error("I don't know what to do")
+ case f: FunctionType => sys.error("I don't know what to do")
+ case _ => sys.error("Unexpected type: " + t)
}
def solve(expression: Expr) : Option[Boolean] = {
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 71f22363a9cc7f62848971617625ac8ee7f7704f..2cdea3d02f99f63c7de31a7f86ca5f4815056c08 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -28,7 +28,8 @@ class DefaultReporter extends Reporter {
protected val fatalPfx = "[ Fatal ] "
def output(msg: String) : Unit = {
- /*Console.err.*/println(msg)
+ if(!Settings.simpleOutput)
+ println(msg)
}
protected def reline(pfx: String, msg: String) : String = {
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 6593e418c28a4f49f5b8a798b527b468e9f3040c..dc88a7cb365f1942aa5bfa5ebdf6841057cb30bd 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -19,8 +19,12 @@ 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
var bitvectorBitwidth : Option[Int] = None
+ var debugLevel: Int = 0
+ var debugTags: Set[String] = Set.empty
+ var simpleOutput: Boolean = false
}
diff --git a/src/main/scala/leon/Simplificator.scala b/src/main/scala/leon/Simplificator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5562c75db5965e7d5f5916aa8923da065b1e3bb6
--- /dev/null
+++ b/src/main/scala/leon/Simplificator.scala
@@ -0,0 +1,21 @@
+package leon
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
+
+object Simplificator extends Pass {
+
+ val description = "Some safe and minimal simplification"
+
+ def apply(pgm: Program): Program = {
+
+ val allFuns = pgm.definedFunctions
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..2c5d4d5a532614873b9b6786481e82f0ebd4a3de
--- /dev/null
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -0,0 +1,150 @@
+package leon
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
+
+object UnitElimination extends Pass {
+
+ val description = "Remove all usage of the Unit type and value"
+
+ private var fun2FreshFun: Map[FunDef, FunDef] = Map()
+ private var id2FreshId: Map[Identifier, Identifier] = Map()
+
+ def apply(pgm: Program): Program = {
+ fun2FreshFun = Map()
+ val allFuns = pgm.definedFunctions
+
+ //first introduce new signatures without Unit parameters
+ allFuns.foreach(fd => {
+ if(fd.returnType != UnitType && fd.args.exists(vd => vd.tpe == UnitType)) {
+ val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
+ freshFunDef.fromLoop = fd.fromLoop
+ freshFunDef.parent = fd.parent
+ 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..
+ freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ fun2FreshFun += (fd -> freshFunDef)
+ } else {
+ fun2FreshFun += (fd -> fd) //this will make the next step simpler
+ }
+ })
+
+ //then apply recursively to the bodies
+ val newFuns = allFuns.flatMap(fd => if(fd.returnType == UnitType) Seq() else {
+ val newBody = fd.body.map(body => removeUnit(body))
+ val newFd = fun2FreshFun(fd)
+ newFd.body = newBody
+ Seq(newFd)
+ })
+
+ val Program(id, ObjectDef(objId, _, invariants)) = pgm
+ val allClasses = pgm.definedClasses
+ Program(id, ObjectDef(objId, allClasses ++ newFuns, invariants))
+ }
+
+ private def simplifyType(tpe: TypeTree): TypeTree = tpe match {
+ case TupleType(tpes) => tpes.map(simplifyType).filterNot{ case UnitType => true case _ => false } match {
+ case Seq() => UnitType
+ case Seq(tpe) => tpe
+ case tpes => TupleType(tpes)
+ }
+ case t => t
+ }
+
+ //remove unit value as soon as possible, so expr should never be equal to a unit
+ private def removeUnit(expr: Expr): Expr = {
+ assert(expr.getType != UnitType)
+ expr match {
+ case fi@FunctionInvocation(fd, args) => {
+ val newArgs = args.filterNot(arg => arg.getType == UnitType)
+ FunctionInvocation(fun2FreshFun(fd), newArgs).setPosInfo(fi)
+ }
+ case t@Tuple(args) => {
+ val TupleType(tpes) = t.getType
+ val (newTpes, newArgs) = tpes.zip(args).filterNot{ case (UnitType, _) => true case _ => false }.unzip
+ Tuple(newArgs.map(removeUnit)).setType(TupleType(newTpes))
+ }
+ case ts@TupleSelect(t, index) => {
+ val TupleType(tpes) = t.getType
+ val selectionType = tpes(index-1)
+ val (_, newIndex) = tpes.zipWithIndex.foldLeft((0,-1)){
+ case ((nbUnit, newIndex), (tpe, i)) =>
+ if(i == index-1) (nbUnit, index - nbUnit) else (if(tpe == UnitType) nbUnit + 1 else nbUnit, newIndex)
+ }
+ TupleSelect(removeUnit(t), newIndex).setType(selectionType)
+ }
+ case Let(id, e, b) => {
+ if(id.getType == UnitType)
+ removeUnit(b)
+ else {
+ id.getType match {
+ case TupleType(tpes) if tpes.exists(_ == UnitType) => {
+ val newTupleType = TupleType(tpes.filterNot(_ == UnitType))
+ val freshId = FreshIdentifier(id.name).setType(newTupleType)
+ id2FreshId += (id -> freshId)
+ val newBody = removeUnit(b)
+ id2FreshId -= id
+ Let(freshId, removeUnit(e), newBody)
+ }
+ case _ => Let(id, removeUnit(e), removeUnit(b))
+ }
+ }
+ }
+ case LetDef(fd, b) => {
+ if(fd.returnType == UnitType)
+ removeUnit(b)
+ else {
+ val (newFd, rest) = if(fd.args.exists(vd => vd.tpe == UnitType)) {
+ val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
+ freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ freshFunDef.parent = fd.parent
+ freshFunDef.fromLoop = fd.fromLoop
+ 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 = fd.body.map(b => removeUnit(b))
+ val restRec = removeUnit(b)
+ fun2FreshFun -= fd
+ (freshFunDef, restRec)
+ } else {
+ fun2FreshFun += (fd -> fd)
+ fd.body = fd.body.map(b => removeUnit(b))
+ val restRec = removeUnit(b)
+ fun2FreshFun -= fd
+ (fd, restRec)
+ }
+ LetDef(newFd, rest)
+ }
+ }
+ case ite@IfExpr(cond, tExpr, eExpr) => {
+ val thenRec = removeUnit(tExpr)
+ val elseRec = removeUnit(eExpr)
+ IfExpr(removeUnit(cond), thenRec, elseRec).setType(thenRec.getType)
+ }
+ case n @ NAryOperator(args, recons) => {
+ recons(args.map(removeUnit(_))).setType(n.getType)
+ }
+ case b @ BinaryOperator(a1, a2, recons) => {
+ recons(removeUnit(a1), removeUnit(a2)).setType(b.getType)
+ }
+ case u @ UnaryOperator(a, recons) => {
+ recons(removeUnit(a)).setType(u.getType)
+ }
+ case v @ Variable(id) => if(id2FreshId.isDefinedAt(id)) Variable(id2FreshId(id)) else v
+ case (t: Terminal) => t
+ case m @ MatchExpr(scrut, cses) => {
+ val scrutRec = removeUnit(scrut)
+ val csesRec = cses.map{
+ case SimpleCase(pat, rhs) => SimpleCase(pat, removeUnit(rhs))
+ case GuardedCase(pat, guard, rhs) => GuardedCase(pat, removeUnit(guard), removeUnit(rhs))
+ }
+ val tpe = csesRec.head.rhs.getType
+ MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
+ }
+ case _ => sys.error("not supported: " + expr)
+ }
+ }
+
+}
diff --git a/src/main/scala/leon/Utils.scala b/src/main/scala/leon/Utils.scala
index 6d7f019ce669a9e81f7da0380048d0071d6713bc..ae60002b693a0b74657fa8640a7eef56a641703f 100644
--- a/src/main/scala/leon/Utils.scala
+++ b/src/main/scala/leon/Utils.scala
@@ -9,4 +9,11 @@ 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 = ()
+ }
+ implicit def while2Invariant(u: Unit) = InvariantFunction
}
diff --git a/src/main/scala/leon/VerificationCondition.scala b/src/main/scala/leon/VerificationCondition.scala
index 4150536fa441352761a7542019caa64d478b0d6a..01545bc3e87bd3606591b464f59098a5b0d8dd8c 100644
--- a/src/main/scala/leon/VerificationCondition.scala
+++ b/src/main/scala/leon/VerificationCondition.scala
@@ -49,4 +49,7 @@ object VCKind extends Enumeration {
val Postcondition = Value("postcond.")
val ExhaustiveMatch = Value("match.")
val MapAccess = Value("map acc.")
+ val InvariantInit = Value("inv init.")
+ val InvariantInd = Value("inv ind.")
+ val InvariantPost = Value("inv post.")
}
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 2006f489bf6adc89578d557c92e1e3f86f17dc24..e54690c36b732ae3b3b3e3924d1f54d8b3fc945a 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -5,7 +5,7 @@ import scala.tools.nsc._
import scala.tools.nsc.plugins._
import purescala.Definitions._
-import purescala.Trees._
+import purescala.Trees.{Block => PBlock, _}
import purescala.TypeTrees._
import purescala.Common._
@@ -53,6 +53,8 @@ trait CodeExtraction extends Extractors {
sym == function1TraitSym
}
+ private val mutableVarSubsts: scala.collection.mutable.Map[Symbol,Function0[Expr]] =
+ scala.collection.mutable.Map.empty[Symbol,Function0[Expr]]
private val varSubsts: scala.collection.mutable.Map[Symbol,Function0[Expr]] =
scala.collection.mutable.Map.empty[Symbol,Function0[Expr]]
private val classesToClasses: scala.collection.mutable.Map[Symbol,ClassTypeDef] =
@@ -60,7 +62,7 @@ trait CodeExtraction extends Extractors {
private val defsToDefs: scala.collection.mutable.Map[Symbol,FunDef] =
scala.collection.mutable.Map.empty[Symbol,FunDef]
- def extractCode(unit: CompilationUnit): Program = {
+ def extractCode(unit: CompilationUnit): Program = {
import scala.collection.mutable.HashMap
def s2ps(tree: Tree): Expr = toPureScala(unit)(tree) match {
@@ -278,11 +280,21 @@ trait CodeExtraction extends Extractors {
}
val bodyAttempt = try {
- Some(scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies)(realBody))
+ Some(flattenBlocks(scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies)(realBody)))
} catch {
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)
+ })
+ ensCont.map(e =>
+ if(containsLetDef(e)) {
+ unit.error(realBody.pos, "Function postcondition should not contain nested function definition")
+ throw ImpureCodeEncounteredException(realBody)
+ })
funDef.body = bodyAttempt
funDef.precondition = reqCont
funDef.postcondition = ensCont
@@ -347,6 +359,22 @@ trait CodeExtraction extends Extractors {
assert(args.size == cd.fields.size)
CaseClassPattern(Some(newID), cd, args.map(pat2pat(_)))
}
+ case a@Apply(fn, args) => {
+ val pst = scalaType2PureScala(unit, silent)(a.tpe)
+ pst match {
+ case TupleType(argsTpes) => TuplePattern(None, args.map(pat2pat))
+ case _ => throw ImpureCodeEncounteredException(p)
+ }
+ }
+ case b @ Bind(name, a @ Apply(fn, args)) => {
+ val newID = FreshIdentifier(name.toString).setType(scalaType2PureScala(unit,silent)(b.symbol.tpe))
+ varSubsts(b.symbol) = (() => Variable(newID))
+ val pst = scalaType2PureScala(unit, silent)(a.tpe)
+ pst match {
+ case TupleType(argsTpes) => TuplePattern(Some(newID), args.map(pat2pat))
+ case _ => throw ImpureCodeEncounteredException(p)
+ }
+ }
case _ => {
if(!silent)
unit.error(p.pos, "Unsupported pattern.")
@@ -357,304 +385,479 @@ trait CodeExtraction extends Extractors {
if(cd.guard == EmptyTree) {
SimpleCase(pat2pat(cd.pat), rec(cd.body))
} else {
- GuardedCase(pat2pat(cd.pat), rec(cd.guard), rec(cd.body))
+ val recPattern = pat2pat(cd.pat)
+ val recGuard = rec(cd.guard)
+ val recBody = rec(cd.body)
+ if(!isPure(recGuard)) {
+ unit.error(cd.guard.pos, "Guard expression must be pure")
+ throw ImpureCodeEncounteredException(cd)
+ }
+ GuardedCase(recPattern, recGuard, recBody)
}
}
- def rec(tr: Tree): Expr = tr match {
- case ExTuple(tpes, exprs) => {
- // println("getting ExTuple with " + tpes + " and " + exprs)
- val tupleType = TupleType(tpes.map(tpe => scalaType2PureScala(unit, silent)(tpe)))
- val tupleExprs = exprs.map(e => rec(e))
- Tuple(tupleExprs).setType(tupleType)
- }
- case ExTupleExtract(tuple, index) => {
- val tupleExpr = rec(tuple)
- val TupleType(tpes) = tupleExpr.getType
- if(tpes.size < index)
- throw ImpureCodeEncounteredException(tree)
- else
- TupleSelect(tupleExpr, index).setType(tpes(index-1))
- }
- case ExValDef(vs, tpt, bdy, rst) => {
- val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
- val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
- val oldSubsts = varSubsts
- val valTree = rec(bdy)
- varSubsts(vs) = (() => Variable(newID))
- val restTree = rec(rst)
- varSubsts.remove(vs)
- Let(newID, valTree, restTree)
+ def extractFunSig(nameStr: String, params: Seq[ValDef], tpt: Tree): FunDef = {
+ val newParams = params.map(p => {
+ val ptpe = scalaType2PureScala(unit, silent) (p.tpt.tpe)
+ val newID = FreshIdentifier(p.name.toString).setType(ptpe)
+ varSubsts(p.symbol) = (() => Variable(newID))
+ VarDecl(newID, ptpe)
+ })
+ new FunDef(FreshIdentifier(nameStr), scalaType2PureScala(unit, silent)(tpt.tpe), newParams)
+ }
+
+ def extractFunDef(funDef: FunDef, body: Tree): FunDef = {
+ var realBody = body
+ var reqCont: Option[Expr] = None
+ var ensCont: Option[Expr] = None
+
+ realBody match {
+ case ExEnsuredExpression(body2, resSym, contract) => {
+ varSubsts(resSym) = (() => ResultVariable().setType(funDef.returnType))
+ val c1 = scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies) (contract)
+ // varSubsts.remove(resSym)
+ realBody = body2
+ ensCont = Some(c1)
+ }
+ case ExHoldsExpression(body2) => {
+ realBody = body2
+ ensCont = Some(ResultVariable().setType(BooleanType))
+ }
+ case _ => ;
}
- case ExInt32Literal(v) => IntLiteral(v).setType(Int32Type)
- case ExBooleanLiteral(v) => BooleanLiteral(v).setType(BooleanType)
- case ExTyped(e,tpt) => rec(e)
- case ExIdentifier(sym,tpt) => varSubsts.get(sym) match {
- case Some(fun) => fun()
- case None => {
- unit.error(tr.pos, "Unidentified variable.")
- throw ImpureCodeEncounteredException(tr)
+
+ realBody match {
+ case ExRequiredExpression(body3, contract) => {
+ realBody = body3
+ reqCont = Some(scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies) (contract))
}
+ case _ => ;
}
- case ExSomeConstruction(tpe, arg) => {
- // println("Got Some !" + tpe + ":" + arg)
- val underlying = scalaType2PureScala(unit, silent)(tpe)
- OptionSome(rec(arg)).setType(OptionType(underlying))
+
+ val bodyAttempt = try {
+ Some(flattenBlocks(scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies)(realBody)))
+ } catch {
+ case e: ImpureCodeEncounteredException => None
}
- case ExCaseClassConstruction(tpt, args) => {
- val cctype = scalaType2PureScala(unit, silent)(tpt.tpe)
- if(!cctype.isInstanceOf[CaseClassType]) {
- if(!silent) {
- unit.error(tr.pos, "Construction of a non-case class.")
+
+ reqCont.map(e =>
+ if(containsLetDef(e)) {
+ unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
+ throw ImpureCodeEncounteredException(realBody)
+ })
+ ensCont.map(e =>
+ if(containsLetDef(e)) {
+ unit.error(realBody.pos, "Function postcondition should not contain nested function definition")
+ throw ImpureCodeEncounteredException(realBody)
+ })
+ funDef.body = bodyAttempt
+ funDef.precondition = reqCont
+ funDef.postcondition = ensCont
+ funDef
+ }
+
+ def rec(tr: Tree): Expr = {
+
+ val (nextExpr, rest) = tr match {
+ case Block(Block(e :: es1, l1) :: es2, l2) => (e, Some(Block(es1 ++ Seq(l1) ++ es2, l2)))
+ case Block(e :: Nil, last) => (e, Some(last))
+ case Block(e :: es, last) => (e, Some(Block(es, last)))
+ case _ => (tr, None)
+ }
+
+ var handleRest = true
+ val psExpr = nextExpr match {
+ case ExTuple(tpes, exprs) => {
+ val tupleType = TupleType(tpes.map(tpe => scalaType2PureScala(unit, silent)(tpe)))
+ val tupleExprs = exprs.map(e => rec(e))
+ Tuple(tupleExprs).setType(tupleType)
+ }
+ case ExTupleExtract(tuple, index) => {
+ val tupleExpr = rec(tuple)
+ val TupleType(tpes) = tupleExpr.getType
+ if(tpes.size < index)
+ throw ImpureCodeEncounteredException(tree)
+ else
+ TupleSelect(tupleExpr, index).setType(tpes(index-1))
+ }
+ case ExValDef(vs, tpt, bdy) => {
+ val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
+ val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
+ val valTree = rec(bdy)
+ val restTree = rest match {
+ case Some(rst) => {
+ varSubsts(vs) = (() => Variable(newID))
+ val res = rec(rst)
+ varSubsts.remove(vs)
+ res
+ }
+ case None => UnitLiteral
}
- throw ImpureCodeEncounteredException(tree)
+ handleRest = false
+ val res = Let(newID, valTree, restTree)
+ res
+ }
+ case dd@ExFunctionDef(n, p, t, b) => {
+ val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
+ defsToDefs += (dd.symbol -> funDef)
+ val oldMutableVarSubst = mutableVarSubsts.toMap //take an immutable snapshot of the map
+ mutableVarSubsts.clear //reseting the visible mutable vars, we do not handle mutable variable closure in nested functions
+ val funDefWithBody = extractFunDef(funDef, b)
+ mutableVarSubsts ++= oldMutableVarSubst
+ val restTree = rest match {
+ case Some(rst) => rec(rst)
+ case None => UnitLiteral
+ }
+ defsToDefs.remove(dd.symbol)
+ handleRest = false
+ LetDef(funDefWithBody, restTree)
+ }
+ case ExVarDef(vs, tpt, bdy) => {
+ val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
+ val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
+ val valTree = rec(bdy)
+ mutableVarSubsts += (vs -> (() => Variable(newID)))
+ val restTree = rest match {
+ case Some(rst) => {
+ varSubsts(vs) = (() => Variable(newID))
+ val res = rec(rst)
+ varSubsts.remove(vs)
+ res
+ }
+ case None => UnitLiteral
+ }
+ handleRest = false
+ val res = LetVar(newID, valTree, restTree)
+ res
}
- val nargs = args.map(rec(_))
- val cct = cctype.asInstanceOf[CaseClassType]
- CaseClass(cct.classDef, nargs).setType(cct)
- }
- case ExAnd(l, r) => And(rec(l), rec(r)).setType(BooleanType)
- case ExOr(l, r) => Or(rec(l), rec(r)).setType(BooleanType)
- case ExNot(e) => Not(rec(e)).setType(BooleanType)
- case ExUMinus(e) => UMinus(rec(e)).setType(Int32Type)
- case ExPlus(l, r) => Plus(rec(l), rec(r)).setType(Int32Type)
- case ExMinus(l, r) => Minus(rec(l), rec(r)).setType(Int32Type)
- case ExTimes(l, r) => Times(rec(l), rec(r)).setType(Int32Type)
- case ExDiv(l, r) => Division(rec(l), rec(r)).setType(Int32Type)
- case ExMod(l, r) => Modulo(rec(l), rec(r)).setType(Int32Type)
- case ExEquals(l, r) => {
- val rl = rec(l)
- val rr = rec(r)
- ((rl.getType,rr.getType) match {
- case (SetType(_), SetType(_)) => SetEquals(rl, rr)
- case (BooleanType, BooleanType) => Iff(rl, rr)
- case (_, _) => Equals(rl, rr)
- }).setType(BooleanType)
- }
- case ExNotEquals(l, r) => Not(Equals(rec(l), rec(r)).setType(BooleanType)).setType(BooleanType)
- case ExGreaterThan(l, r) => GreaterThan(rec(l), rec(r)).setType(BooleanType)
- case ExGreaterEqThan(l, r) => GreaterEquals(rec(l), rec(r)).setType(BooleanType)
- case ExLessThan(l, r) => LessThan(rec(l), rec(r)).setType(BooleanType)
- case ExLessEqThan(l, r) => LessEquals(rec(l), rec(r)).setType(BooleanType)
- case ExFiniteSet(tt, args) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- FiniteSet(args.map(rec(_))).setType(SetType(underlying))
- }
- case ExFiniteMultiset(tt, args) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- FiniteMultiset(args.map(rec(_))).setType(MultisetType(underlying))
- }
- case ExEmptySet(tt) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- EmptySet(underlying).setType(SetType(underlying))
- }
- case ExEmptyMultiset(tt) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- EmptyMultiset(underlying).setType(MultisetType(underlying))
- }
- case ExEmptyMap(ft, tt) => {
- val fromUnderlying = scalaType2PureScala(unit, silent)(ft.tpe)
- val toUnderlying = scalaType2PureScala(unit, silent)(tt.tpe)
- EmptyMap(fromUnderlying, toUnderlying).setType(MapType(fromUnderlying, toUnderlying))
- }
- case ExSetMin(t) => {
- val set = rec(t)
- if(!set.getType.isInstanceOf[SetType]) {
- if(!silent) unit.error(t.pos, "Min should be computed on a set.")
- throw ImpureCodeEncounteredException(tree)
+
+ case ExAssign(sym, rhs) => mutableVarSubsts.get(sym) match {
+ case Some(fun) => {
+ val Variable(id) = fun()
+ val rhsTree = rec(rhs)
+ Assignment(id, rhsTree)
+ }
+ case None => {
+ unit.error(tr.pos, "Undeclared variable.")
+ throw ImpureCodeEncounteredException(tr)
+ }
}
- SetMin(set).setType(set.getType.asInstanceOf[SetType].base)
- }
- case ExSetMax(t) => {
- val set = rec(t)
- if(!set.getType.isInstanceOf[SetType]) {
- if(!silent) unit.error(t.pos, "Max should be computed on a set.")
- throw ImpureCodeEncounteredException(tree)
+ case wh@ExWhile(cond, body) => {
+ val condTree = rec(cond)
+ val bodyTree = rec(body)
+ While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
+ }
+ case wh@ExWhileWithInvariant(cond, body, inv) => {
+ val condTree = rec(cond)
+ val bodyTree = rec(body)
+ val invTree = rec(inv)
+ val w = While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
+ w.invariant = Some(invTree)
+ w
+ }
+
+ case ExInt32Literal(v) => IntLiteral(v).setType(Int32Type)
+ case ExBooleanLiteral(v) => BooleanLiteral(v).setType(BooleanType)
+ case ExUnitLiteral() => UnitLiteral
+
+ case ExTyped(e,tpt) => rec(e)
+ case ExIdentifier(sym,tpt) => varSubsts.get(sym) match {
+ case Some(fun) => fun()
+ case None => mutableVarSubsts.get(sym) match {
+ case Some(fun) => fun()
+ case None => {
+ unit.error(tr.pos, "Unidentified variable.")
+ throw ImpureCodeEncounteredException(tr)
+ }
+ }
}
- SetMax(set).setType(set.getType.asInstanceOf[SetType].base)
- }
- case ExUnion(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SetUnion(rl, rr).setType(s)
- case m @ MultisetType(_) => MultisetUnion(rl, rr).setType(m)
- case _ => {
- if(!silent) unit.error(tree.pos, "Union of non set/multiset expressions.")
+ 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)
+ }
+ if(containsEpsilon(c1)) {
+ unit.error(epsi.pos, "Usage of nested epsilon is not allowed.")
+ throw ImpureCodeEncounteredException(epsi)
+ }
+ 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)
+ OptionSome(rec(arg)).setType(OptionType(underlying))
+ }
+ case ExCaseClassConstruction(tpt, args) => {
+ val cctype = scalaType2PureScala(unit, silent)(tpt.tpe)
+ if(!cctype.isInstanceOf[CaseClassType]) {
+ if(!silent) {
+ unit.error(tr.pos, "Construction of a non-case class.")
+ }
throw ImpureCodeEncounteredException(tree)
}
- }
- }
- case ExIntersection(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SetIntersection(rl, rr).setType(s)
- case m @ MultisetType(_) => MultisetIntersection(rl, rr).setType(m)
- case _ => {
- if(!silent) unit.error(tree.pos, "Intersection of non set/multiset expressions.")
+ val nargs = args.map(rec(_))
+ val cct = cctype.asInstanceOf[CaseClassType]
+ CaseClass(cct.classDef, nargs).setType(cct)
+ }
+ case ExAnd(l, r) => And(rec(l), rec(r)).setType(BooleanType)
+ case ExOr(l, r) => Or(rec(l), rec(r)).setType(BooleanType)
+ case ExNot(e) => Not(rec(e)).setType(BooleanType)
+ case ExUMinus(e) => UMinus(rec(e)).setType(Int32Type)
+ case ExPlus(l, r) => Plus(rec(l), rec(r)).setType(Int32Type)
+ case ExMinus(l, r) => Minus(rec(l), rec(r)).setType(Int32Type)
+ case ExTimes(l, r) => Times(rec(l), rec(r)).setType(Int32Type)
+ case ExDiv(l, r) => Division(rec(l), rec(r)).setType(Int32Type)
+ case ExMod(l, r) => Modulo(rec(l), rec(r)).setType(Int32Type)
+ case ExEquals(l, r) => {
+ val rl = rec(l)
+ val rr = rec(r)
+ ((rl.getType,rr.getType) match {
+ case (SetType(_), SetType(_)) => SetEquals(rl, rr)
+ case (BooleanType, BooleanType) => Iff(rl, rr)
+ case (_, _) => Equals(rl, rr)
+ }).setType(BooleanType)
+ }
+ case ExNotEquals(l, r) => Not(Equals(rec(l), rec(r)).setType(BooleanType)).setType(BooleanType)
+ case ExGreaterThan(l, r) => GreaterThan(rec(l), rec(r)).setType(BooleanType)
+ case ExGreaterEqThan(l, r) => GreaterEquals(rec(l), rec(r)).setType(BooleanType)
+ case ExLessThan(l, r) => LessThan(rec(l), rec(r)).setType(BooleanType)
+ case ExLessEqThan(l, r) => LessEquals(rec(l), rec(r)).setType(BooleanType)
+ case ExFiniteSet(tt, args) => {
+ val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ FiniteSet(args.map(rec(_))).setType(SetType(underlying))
+ }
+ case ExFiniteMultiset(tt, args) => {
+ val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ FiniteMultiset(args.map(rec(_))).setType(MultisetType(underlying))
+ }
+ case ExEmptySet(tt) => {
+ val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ EmptySet(underlying).setType(SetType(underlying))
+ }
+ case ExEmptyMultiset(tt) => {
+ val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ EmptyMultiset(underlying).setType(MultisetType(underlying))
+ }
+ case ExEmptyMap(ft, tt) => {
+ val fromUnderlying = scalaType2PureScala(unit, silent)(ft.tpe)
+ val toUnderlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ EmptyMap(fromUnderlying, toUnderlying).setType(MapType(fromUnderlying, toUnderlying))
+ }
+ case ExSetMin(t) => {
+ val set = rec(t)
+ if(!set.getType.isInstanceOf[SetType]) {
+ if(!silent) unit.error(t.pos, "Min should be computed on a set.")
throw ImpureCodeEncounteredException(tree)
}
+ SetMin(set).setType(set.getType.asInstanceOf[SetType].base)
}
- }
- case ExSetContains(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => ElementOfSet(rr, rl)
- case _ => {
- if(!silent) unit.error(tree.pos, ".contains on non set expression.")
+ case ExSetMax(t) => {
+ val set = rec(t)
+ if(!set.getType.isInstanceOf[SetType]) {
+ if(!silent) unit.error(t.pos, "Max should be computed on a set.")
throw ImpureCodeEncounteredException(tree)
}
+ SetMax(set).setType(set.getType.asInstanceOf[SetType].base)
+ }
+ case ExUnion(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SetUnion(rl, rr).setType(s)
+ case m @ MultisetType(_) => MultisetUnion(rl, rr).setType(m)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Union of non set/multiset expressions.")
+ throw ImpureCodeEncounteredException(tree)
+ }
+ }
}
- }
- case ExSetSubset(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SubsetOf(rl, rr)
- case _ => {
- if(!silent) unit.error(tree.pos, "Subset on non set expression.")
- throw ImpureCodeEncounteredException(tree)
+ case ExIntersection(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SetIntersection(rl, rr).setType(s)
+ case m @ MultisetType(_) => MultisetIntersection(rl, rr).setType(m)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Intersection of non set/multiset expressions.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExSetMinus(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SetDifference(rl, rr).setType(s)
- case m @ MultisetType(_) => MultisetDifference(rl, rr).setType(m)
- case _ => {
- if(!silent) unit.error(tree.pos, "Difference of non set/multiset expressions.")
- throw ImpureCodeEncounteredException(tree)
+ case ExSetContains(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => ElementOfSet(rr, rl)
+ case _ => {
+ if(!silent) unit.error(tree.pos, ".contains on non set expression.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExSetCard(t) => {
- val rt = rec(t)
- rt.getType match {
- case s @ SetType(_) => SetCardinality(rt)
- case m @ MultisetType(_) => MultisetCardinality(rt)
- case _ => {
- if(!silent) unit.error(tree.pos, "Cardinality of non set/multiset expressions.")
- throw ImpureCodeEncounteredException(tree)
+ case ExSetSubset(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SubsetOf(rl, rr)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Subset on non set expression.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExMultisetToSet(t) => {
- val rt = rec(t)
- rt.getType match {
- case m @ MultisetType(u) => MultisetToSet(rt).setType(SetType(u))
- case _ => {
- if(!silent) unit.error(tree.pos, "toSet can only be applied to multisets.")
- throw ImpureCodeEncounteredException(tree)
+ case ExSetMinus(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SetDifference(rl, rr).setType(s)
+ case m @ MultisetType(_) => MultisetDifference(rl, rr).setType(m)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Difference of non set/multiset expressions.")
+ throw ImpureCodeEncounteredException(tree)
+ }
+ }
+ }
+ case ExSetCard(t) => {
+ val rt = rec(t)
+ rt.getType match {
+ case s @ SetType(_) => SetCardinality(rt)
+ case m @ MultisetType(_) => MultisetCardinality(rt)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Cardinality of non set/multiset expressions.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExMapUpdated(m,f,t) => {
- val rm = rec(m)
- val rf = rec(f)
- val rt = rec(t)
- val newSingleton = SingletonMap(rf, rt).setType(rm.getType)
- rm.getType match {
- case MapType(ft, tt) =>
- MapUnion(rm, FiniteMap(Seq(newSingleton)).setType(rm.getType)).setType(rm.getType)
- case _ => {
- if (!silent) unit.error(tree.pos, "updated can only be applied to maps.")
- throw ImpureCodeEncounteredException(tree)
+ case ExMultisetToSet(t) => {
+ val rt = rec(t)
+ rt.getType match {
+ case m @ MultisetType(u) => MultisetToSet(rt).setType(SetType(u))
+ case _ => {
+ if(!silent) unit.error(tree.pos, "toSet can only be applied to multisets.")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExMapIsDefinedAt(m,k) => {
- val rm = rec(m)
- val rk = rec(k)
- MapIsDefinedAt(rm, rk)
- }
-
- case ExPlusPlusPlus(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- MultisetPlus(rl, rr).setType(rl.getType)
- }
- case ExApply(lhs,args) => {
- val rlhs = rec(lhs)
- val rargs = args map rec
- rlhs.getType match {
- case MapType(_,tt) =>
- assert(rargs.size == 1)
- MapGet(rlhs, rargs.head).setType(tt)
- case FunctionType(fts, tt) => {
- rlhs match {
- case Variable(id) =>
- AnonymousFunctionInvocation(id, rargs).setType(tt)
- case _ => {
- if (!silent) unit.error(tree.pos, "apply on non-variable or non-map expression")
- throw ImpureCodeEncounteredException(tree)
- }
+ case ExMapUpdated(m,f,t) => {
+ val rm = rec(m)
+ val rf = rec(f)
+ val rt = rec(t)
+ val newSingleton = SingletonMap(rf, rt).setType(rm.getType)
+ rm.getType match {
+ case MapType(ft, tt) =>
+ MapUnion(rm, FiniteMap(Seq(newSingleton)).setType(rm.getType)).setType(rm.getType)
+ case _ => {
+ if (!silent) unit.error(tree.pos, "updated can only be applied to maps.")
+ throw ImpureCodeEncounteredException(tree)
}
}
- case _ => {
- if (!silent) unit.error(tree.pos, "apply on unexpected type")
- throw ImpureCodeEncounteredException(tree)
+ }
+ case ExMapIsDefinedAt(m,k) => {
+ val rm = rec(m)
+ val rk = rec(k)
+ MapIsDefinedAt(rm, rk)
+ }
+
+ case ExPlusPlusPlus(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ MultisetPlus(rl, rr).setType(rl.getType)
+ }
+ case app@ExApply(lhs,args) => {
+ val rlhs = rec(lhs)
+ val rargs = args map rec
+ rlhs.getType match {
+ case MapType(_,tt) =>
+ assert(rargs.size == 1)
+ MapGet(rlhs, rargs.head).setType(tt).setPosInfo(app.pos.line, app.pos.column)
+ case FunctionType(fts, tt) => {
+ rlhs match {
+ case Variable(id) =>
+ AnonymousFunctionInvocation(id, rargs).setType(tt)
+ case _ => {
+ if (!silent) unit.error(tree.pos, "apply on non-variable or non-map expression")
+ throw ImpureCodeEncounteredException(tree)
+ }
+ }
+ }
+ case _ => {
+ if (!silent) unit.error(tree.pos, "apply on unexpected type")
+ throw ImpureCodeEncounteredException(tree)
+ }
}
}
- }
- case ExIfThenElse(t1,t2,t3) => {
- val r1 = rec(t1)
- val r2 = rec(t2)
- val r3 = rec(t3)
- IfExpr(r1, r2, r3).setType(leastUpperBound(r2.getType, r3.getType))
- }
- case lc @ ExLocalCall(sy,nm,ar) => {
- if(defsToDefs.keysIterator.find(_ == sy).isEmpty) {
- if(!silent)
- unit.error(tr.pos, "Invoking an invalid function.")
- throw ImpureCodeEncounteredException(tr)
+ case ExIfThenElse(t1,t2,t3) => {
+ val r1 = rec(t1)
+ val r2 = rec(t2)
+ val r3 = rec(t3)
+ IfExpr(r1, r2, r3).setType(leastUpperBound(r2.getType, r3.getType))
}
- val fd = defsToDefs(sy)
- FunctionInvocation(fd, ar.map(rec(_))).setType(fd.returnType).setPosInfo(lc.pos.line,lc.pos.column)
- }
- case pm @ ExPatternMatching(sel, cses) => {
- val rs = rec(sel)
- val rc = cses.map(rewriteCaseDef(_))
- val rt: purescala.TypeTrees.TypeTree = rc.map(_.rhs.getType).reduceLeft(leastUpperBound(_,_))
- MatchExpr(rs, rc).setType(rt).setPosInfo(pm.pos.line,pm.pos.column)
- }
-
- // this one should stay after all others, cause it also catches UMinus
- // and Not, for instance.
- case ExParameterlessMethodCall(t,n) => {
- val selector = rec(t)
- val selType = selector.getType
-
- if(!selType.isInstanceOf[CaseClassType]) {
- if(!silent)
- unit.error(tr.pos, "Invalid method or field invocation (not purescala?)")
- throw ImpureCodeEncounteredException(tr)
+ case lc @ ExLocalCall(sy,nm,ar) => {
+ if(defsToDefs.keysIterator.find(_ == sy).isEmpty) {
+ if(!silent)
+ unit.error(tr.pos, "Invoking an invalid function.")
+ throw ImpureCodeEncounteredException(tr)
+ }
+ val fd = defsToDefs(sy)
+ FunctionInvocation(fd, ar.map(rec(_))).setType(fd.returnType).setPosInfo(lc.pos.line,lc.pos.column)
+ }
+ case pm @ ExPatternMatching(sel, cses) => {
+ val rs = rec(sel)
+ val rc = cses.map(rewriteCaseDef(_))
+ val rt: purescala.TypeTrees.TypeTree = rc.map(_.rhs.getType).reduceLeft(leastUpperBound(_,_))
+ MatchExpr(rs, rc).setType(rt).setPosInfo(pm.pos.line,pm.pos.column)
}
- val selDef: CaseClassDef = selType.asInstanceOf[CaseClassType].classDef
+ // this one should stay after all others, cause it also catches UMinus
+ // and Not, for instance.
+ case ExParameterlessMethodCall(t,n) => {
+ val selector = rec(t)
+ val selType = selector.getType
- val fieldID = selDef.fields.find(_.id.name == n.toString) match {
- case None => {
+ if(!selType.isInstanceOf[CaseClassType]) {
if(!silent)
- unit.error(tr.pos, "Invalid method or field invocation (not a case class arg?)")
+ unit.error(tr.pos, "Invalid method or field invocation (not purescala?)")
throw ImpureCodeEncounteredException(tr)
}
- case Some(vd) => vd.id
- }
- CaseClassSelector(selDef, selector, fieldID).setType(fieldID.getType)
+ val selDef: CaseClassDef = selType.asInstanceOf[CaseClassType].classDef
+
+ val fieldID = selDef.fields.find(_.id.name == n.toString) match {
+ case None => {
+ if(!silent)
+ unit.error(tr.pos, "Invalid method or field invocation (not a case class arg?)")
+ throw ImpureCodeEncounteredException(tr)
+ }
+ case Some(vd) => vd.id
+ }
+
+ CaseClassSelector(selDef, selector, fieldID).setType(fieldID.getType)
+ }
+
+ // default behaviour is to complain :)
+ case _ => {
+ if(!silent) {
+ println(tr)
+ reporter.info(tr.pos, "Could not extract as PureScala.", true)
+ }
+ throw ImpureCodeEncounteredException(tree)
+ }
}
-
- // default behaviour is to complain :)
- case _ => {
- if(!silent) {
- println(tr)
- reporter.info(tr.pos, "Could not extract as PureScala.", true)
+
+ if(handleRest) {
+ rest match {
+ case Some(rst) => {
+ val recRst = rec(rst)
+ PBlock(Seq(psExpr), recRst).setType(recRst.getType)
+ }
+ case None => psExpr
}
- throw ImpureCodeEncounteredException(tree)
+ } else {
+ psExpr
}
}
rec(tree)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 08cdfe37973e3fc2ac9e641a4bf6344f63fcb91d..78e66bf6c9ef5a2a8a1e0f23a2a3c4e30a85d19c 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -31,61 +31,6 @@ trait Extractors {
}
}
- object ExTuple {
- def unapply(tree: Apply): Option[(Seq[Type], Seq[Tree])] = tree match {
- case Apply(
- Select(New(tupleType), _),
- List(e1, e2)
- ) if tupleType.symbol == tuple2Sym => tupleType.tpe match {
- case TypeRef(_, sym, List(t1, t2)) => Some((Seq(t1, t2), Seq(e1, e2)))
- case _ => None
- }
-
- case Apply(
- Select(New(tupleType), _),
- List(e1, e2, e3)
- ) if tupleType.symbol == tuple3Sym => tupleType.tpe match {
- case TypeRef(_, sym, List(t1, t2, t3)) => Some((Seq(t1, t2, t3), Seq(e1, e2, e3)))
- case _ => None
- }
- case Apply(
- Select(New(tupleType), _),
- List(e1, e2, e3, e4)
- ) if tupleType.symbol == tuple4Sym => tupleType.tpe match {
- case TypeRef(_, sym, List(t1, t2, t3, t4)) => Some((Seq(t1, t2, t3, t4), Seq(e1, e2, e3, e4)))
- case _ => None
- }
- case Apply(
- Select(New(tupleType), _),
- List(e1, e2, e3, e4, e5)
- ) if tupleType.symbol == tuple5Sym => tupleType.tpe match {
- case TypeRef(_, sym, List(t1, t2, t3, t4, t5)) => Some((Seq(t1, t2, t3, t4, t5), Seq(e1, e2, e3, e4, e5)))
- case _ => None
- }
- case _ => None
- }
- }
-
- object ExTupleExtract {
- def unapply(tree: Select) : Option[(Tree,Int)] = tree match {
- case Select(lhs, n) => {
- val methodName = n.toString
- if(methodName.head == '_') {
- val indexString = methodName.tail
- try {
- val index = indexString.toInt
- if(index > 0) {
- Some((lhs, index))
- } else None
- } catch {
- case _ => None
- }
- } else None
- }
- case _ => None
- }
- }
-
object ExEnsuredExpression {
/** Extracts the 'ensuring' contract from an expression. */
def unapply(tree: Apply): Option[(Tree,Symbol,Tree)] = tree match {
@@ -126,17 +71,6 @@ trait Extractors {
}
}
- object ExValDef {
- /** Extracts val's in the head of blocks. */
- def unapply(tree: Block): Option[(Symbol,Tree,Tree,Tree)] = tree match {
- case Block((vd @ ValDef(_, _, tpt, rhs)) :: rest, expr) =>
- if(rest.isEmpty)
- Some((vd.symbol, tpt, rhs, expr))
- else
- Some((vd.symbol, tpt, rhs, Block(rest, expr)))
- case _ => None
- }
- }
object ExObjectDef {
/** Matches an object with no type parameters, and regardless of its
@@ -209,9 +143,134 @@ trait Extractors {
case _ => None
}
}
+
}
object ExpressionExtractors {
+
+ //object ExLocalFunctionDef {
+ // def unapply(tree: Block): Option[(DefDef,String,Seq[ValDef],Tree,Tree,Tree)] = tree match {
+ // case Block((dd @ DefDef(_, name, tparams, vparamss, tpt, rhs)) :: rest, expr) if(tparams.isEmpty && vparamss.size == 1 && name != nme.CONSTRUCTOR) => {
+ // if(rest.isEmpty)
+ // Some((dd,name.toString, vparamss(0), tpt, rhs, expr))
+ // else
+ // Some((dd,name.toString, vparamss(0), tpt, rhs, Block(rest, expr)))
+ // }
+ // case _ => None
+ // }
+ //}
+
+
+ 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 {
+ case vd @ ValDef(mods, _, tpt, rhs) if !mods.isMutable => Some((vd.symbol, tpt, rhs))
+ case _ => None
+ }
+ }
+ object ExVarDef {
+ /** Extracts var's in the head of blocks. */
+ def unapply(tree: ValDef): Option[(Symbol,Tree,Tree)] = tree match {
+ case vd @ ValDef(mods, _, tpt, rhs) if mods.isMutable => Some((vd.symbol, tpt, rhs))
+ case _ => None
+ }
+ }
+
+ object ExAssign {
+ def unapply(tree: Assign): Option[(Symbol,Tree)] = tree match {
+ case Assign(id@Ident(_), rhs) => Some((id.symbol, rhs))
+ case _ => None
+ }
+ }
+
+ object ExWhile {
+ def unapply(tree: LabelDef): Option[(Tree,Tree)] = tree match {
+ case (label@LabelDef(
+ _, _, If(cond, Block(body, jump@Apply(_, _)), unit@ExUnitLiteral())))
+ if label.symbol == jump.symbol && unit.symbol == null => Some((cond, Block(body, unit)))
+ case _ => None
+ }
+ }
+ object ExWhileWithInvariant {
+ def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
+ case Apply(
+ Select(
+ Apply(while2invariant, List(ExWhile(cond, body))),
+ invariantSym),
+ List(invariant)) if invariantSym.toString == "invariant" => Some((cond, body, invariant))
+ case _ => None
+ }
+ }
+ object ExTuple {
+ def unapply(tree: Apply): Option[(Seq[Type], Seq[Tree])] = tree match {
+ case Apply(
+ Select(New(tupleType), _),
+ List(e1, e2)
+ ) if tupleType.symbol == tuple2Sym => tupleType.tpe match {
+ case TypeRef(_, sym, List(t1, t2)) => Some((Seq(t1, t2), Seq(e1, e2)))
+ case _ => None
+ }
+
+ case Apply(
+ Select(New(tupleType), _),
+ List(e1, e2, e3)
+ ) if tupleType.symbol == tuple3Sym => tupleType.tpe match {
+ case TypeRef(_, sym, List(t1, t2, t3)) => Some((Seq(t1, t2, t3), Seq(e1, e2, e3)))
+ case _ => None
+ }
+ case Apply(
+ Select(New(tupleType), _),
+ List(e1, e2, e3, e4)
+ ) if tupleType.symbol == tuple4Sym => tupleType.tpe match {
+ case TypeRef(_, sym, List(t1, t2, t3, t4)) => Some((Seq(t1, t2, t3, t4), Seq(e1, e2, e3, e4)))
+ case _ => None
+ }
+ case Apply(
+ Select(New(tupleType), _),
+ List(e1, e2, e3, e4, e5)
+ ) if tupleType.symbol == tuple5Sym => tupleType.tpe match {
+ case TypeRef(_, sym, List(t1, t2, t3, t4, t5)) => Some((Seq(t1, t2, t3, t4, t5), Seq(e1, e2, e3, e4, e5)))
+ case _ => None
+ }
+ case _ => None
+ }
+ }
+
+ object ExTupleExtract {
+ def unapply(tree: Select) : Option[(Tree,Int)] = tree match {
+ case Select(lhs, n) => {
+ val methodName = n.toString
+ if(methodName.head == '_') {
+ val indexString = methodName.tail
+ try {
+ val index = indexString.toInt
+ if(index > 0) {
+ Some((lhs, index))
+ } else None
+ } catch {
+ case _ => None
+ }
+ } else None
+ }
+ case _ => None
+ }
+ }
+
object ExIfThenElse {
def unapply(tree: If): Option[(Tree,Tree,Tree)] = tree match {
case If(t1,t2,t3) => Some((t1,t2,t3))
@@ -234,6 +293,13 @@ trait Extractors {
}
}
+ object ExUnitLiteral {
+ def unapply(tree: Literal): Boolean = tree match {
+ case Literal(c @ Constant(_)) if c.tpe == UnitClass.tpe => true
+ case _ => false
+ }
+ }
+
object ExSomeConstruction {
def unapply(tree: Apply) : Option[(Type,Tree)] = tree match {
case Apply(s @ Select(New(tpt), n), arg) if (arg.size == 1 && n == nme.CONSTRUCTOR && tpt.symbol.name.toString == "Some") => tpt.tpe match {
@@ -384,6 +450,7 @@ trait Extractors {
object ExLocalCall {
def unapply(tree: Apply): Option[(Symbol,String,List[Tree])] = tree match {
case a @ Apply(Select(This(_), nme), args) => Some((a.symbol, nme.toString, args))
+ case a @ Apply(Ident(nme), args) => Some((a.symbol, nme.toString, args))
case _ => None
}
}
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index b059ad59dbf218ea9042eb6923484778c3ae5c46..e37b5b1a8c047cc5b7af6ab26d5cdabb03731287 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -39,7 +39,11 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
" --cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
" --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"
+ " --noLuckyTests Do not perform additional tests to potentially find models early" + "\n" +
+ " --noverifymodel Do not verify the correctness of models returned by Z3" + "\n" +
+ " --debug=[1-5] Debug level" + "\n" +
+ " --tags=t1:... Filter out debug information that are not of one of the given tags" + "\n" +
+ " --oneline Reduce the output to a single line: valid if all properties were valid, invalid if at least one is invalid, unknown else"
)
/** Processes the command-line options. */
@@ -47,21 +51,26 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
override def processOptions(options: List[String], error: String => Unit) {
for(option <- options) {
option match {
- case "with-code" => stopAfterAnalysis = false
- case "uniqid" => leon.Settings.showIDs = true
- case "parse" => stopAfterExtraction = true
- case "tolerant" => silentlyTolerateNonPureBodies = true
- case "nodefaults" => leon.Settings.runDefaultExtensions = false
- case "axioms" => leon.Settings.noForallAxioms = false
- case "bapa" => leon.Settings.useBAPA = true
- case "impure" => leon.Settings.impureTestcases = true
- case "XP" => leon.Settings.experimental = true
- case "BV" => leon.Settings.bitvectorBitwidth = Some(32)
- case "prune" => leon.Settings.pruneBranches = true
- case "cores" => leon.Settings.useCores = true
- case "quickcheck" => leon.Settings.useQuickCheck = true
- case "parallel" => leon.Settings.useParallel = true
- case "noLuckyTests" => leon.Settings.luckyTest = false
+ case "with-code" => stopAfterAnalysis = false
+ case "uniqid" => leon.Settings.showIDs = true
+ case "parse" => stopAfterExtraction = true
+ case "tolerant" => silentlyTolerateNonPureBodies = true
+ case "nodefaults" => leon.Settings.runDefaultExtensions = false
+ case "axioms" => leon.Settings.noForallAxioms = false
+ case "bapa" => leon.Settings.useBAPA = true
+ case "impure" => leon.Settings.impureTestcases = true
+ case "XP" => leon.Settings.experimental = true
+ case "BV" => leon.Settings.bitvectorBitwidth = Some(32)
+ case "prune" => leon.Settings.pruneBranches = true
+ case "cores" => leon.Settings.useCores = true
+ case "quickcheck" => leon.Settings.useQuickCheck = true
+ case "parallel" => leon.Settings.useParallel = true
+ case "oneline" => leon.Settings.simpleOutput = true
+ case "noLuckyTests" => leon.Settings.luckyTest = false
+ case "noverifymodel" => leon.Settings.verifyModel = false
+
+ case s if s.startsWith("debug=") => leon.Settings.debugLevel = try { s.substring("debug=".length, s.length).toInt } catch { case _ => 0 }
+ case s if s.startsWith("tags=") => leon.Settings.debugTags = Set(splitList(s.substring("tags=".length, s.length)): _*)
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)): _*)
case s if s.startsWith("extensions=") => leon.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index efd8b52fb31e7cd4d61ff868bba3c836ca1f0e2e..f2da8a7cef1f1f3b0290a35a260f40ceefbf6705 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -283,6 +283,11 @@ object Definitions {
var precondition: Option[Expr] = None
var postcondition: Option[Expr] = None
+ //true if this function has been generated from a while loop
+ var fromLoop = false
+ //the fundef where the loop was defined (if applies)
+ var parent: Option[FunDef] = None
+
def hasImplementation : Boolean = body.isDefined
def hasBody = hasImplementation
def hasPrecondition : Boolean = precondition.isDefined
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 9ed2e564646559bb0b62bfc6078c20fae7e028b9..d1a39f7172fafb612c2201b2c4322615a0aabdef 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -69,7 +69,32 @@ object PrettyPrinter {
case Variable(id) => sb.append(id)
case DeBruijnIndex(idx) => sb.append("_" + idx)
case Let(b,d,e) => {
- pp(e, pp(d, sb.append("(let (" + b + " := "), lvl).append(") in "), lvl).append(")")
+ //pp(e, pp(d, sb.append("(let (" + b + " := "), lvl).append(") in "), lvl).append(")")
+ sb.append("(let (" + b + " := ");
+ pp(d, sb, lvl)
+ sb.append(") in\n")
+ ind(sb, lvl+1)
+ pp(e, sb, lvl+1)
+ sb.append(")")
+ sb
+ }
+ case LetVar(b,d,e) => {
+ sb.append("(letvar (" + b + " := ");
+ pp(d, sb, lvl)
+ sb.append(") in\n")
+ ind(sb, lvl+1)
+ pp(e, sb, lvl+1)
+ sb.append(")")
+ sb
+ }
+ case LetDef(fd,e) => {
+ sb.append("\n")
+ pp(fd, sb, lvl+1)
+ sb.append("\n")
+ sb.append("\n")
+ ind(sb, lvl)
+ pp(e, sb, lvl)
+ sb
}
case And(exprs) => ppNary(sb, exprs, "(", " \u2227 ", ")", lvl) // \land
case Or(exprs) => ppNary(sb, exprs, "(", " \u2228 ", ")", lvl) // \lor
@@ -81,12 +106,54 @@ object PrettyPrinter {
case IntLiteral(v) => sb.append(v)
case BooleanLiteral(v) => sb.append(v)
case StringLiteral(s) => sb.append("\"" + s + "\"")
+ case UnitLiteral => sb.append("()")
+ case Block(exprs, last) => {
+ sb.append("{\n")
+ (exprs :+ last).foreach(e => {
+ ind(sb, lvl+1)
+ pp(e, sb, lvl+1)
+ sb.append("\n")
+ })
+ ind(sb, lvl)
+ sb.append("}\n")
+ sb
+ }
+ case Assignment(lhs, rhs) => ppBinary(sb, lhs.toVariable, rhs, " = ", lvl)
+ case wh@While(cond, body) => {
+ wh.invariant match {
+ case Some(inv) => {
+ sb.append("\n")
+ ind(sb, lvl)
+ sb.append("@invariant: ")
+ pp(inv, sb, lvl)
+ sb.append("\n")
+ ind(sb, lvl)
+ }
+ case None =>
+ }
+ sb.append("while(")
+ pp(cond, sb, lvl)
+ sb.append(")\n")
+ ind(sb, lvl+1)
+ pp(body, sb, lvl+1)
+ sb.append("\n")
+ }
+
case Tuple(exprs) => ppNary(sb, exprs, "(", ", ", ")", lvl)
case TupleSelect(t, i) => {
pp(t, sb, lvl)
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(")
@@ -194,18 +261,27 @@ object PrettyPrinter {
var nsb = sb
nsb.append("if (")
nsb = pp(c, nsb, lvl)
- nsb.append(") {\n")
+ nsb.append(")\n")
ind(nsb, lvl+1)
nsb = pp(t, nsb, lvl+1)
nsb.append("\n")
ind(nsb, lvl)
- nsb.append("} else {\n")
+ nsb.append("else\n")
ind(nsb, lvl+1)
nsb = pp(e, nsb, lvl+1)
- nsb.append("\n")
- ind(nsb, lvl)
- nsb.append("}")
nsb
+ //nsb.append(") {\n")
+ //ind(nsb, lvl+1)
+ //nsb = pp(t, nsb, lvl+1)
+ //nsb.append("\n")
+ //ind(nsb, lvl)
+ //nsb.append("} else {\n")
+ //ind(nsb, lvl+1)
+ //nsb = pp(e, nsb, lvl+1)
+ //nsb.append("\n")
+ //ind(nsb, lvl)
+ //nsb.append("}")
+ //nsb
}
case mex @ MatchExpr(s, csc) => {
@@ -228,6 +304,16 @@ object PrettyPrinter {
}
case WildcardPattern(None) => sb.append("_")
case WildcardPattern(Some(id)) => sb.append(id)
+ case TuplePattern(bndr, subPatterns) => {
+ bndr.foreach(b => sb.append(b + " @ "))
+ sb.append("(")
+ subPatterns.init.foreach(p => {
+ ppc(sb, p)
+ sb.append(", ")
+ })
+ ppc(sb, subPatterns.last)
+ sb.append(")")
+ }
case _ => sb.append("Pattern?")
}
@@ -256,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) => {
@@ -287,6 +374,7 @@ object PrettyPrinter {
private def pp(tpe: TypeTree, sb: StringBuffer, lvl: Int): StringBuffer = tpe match {
case Untyped => sb.append("???")
+ case UnitType => sb.append("Unit")
case Int32Type => sb.append("Int")
case BooleanType => sb.append("Boolean")
case SetType(bt) => pp(bt, sb.append("Set["), lvl).append("]")
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 6ca7d660eb8b1ac5d0888bd4e5d10658822c90ab..638db0c2024152c46b9f735263b11e9ce01b5ca2 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -17,11 +17,31 @@ object Trees {
self: Expr =>
}
+ case class Block(exprs: Seq[Expr], last: Expr) extends Expr {
+ //val t = last.getType
+ //if(t != Untyped)
+ // setType(t)
+ }
+
+ case class Assignment(varId: Identifier, expr: Expr) extends Expr with FixedType {
+ val fixedType = UnitType
+ }
+ case class While(cond: Expr, body: Expr) extends Expr with FixedType with ScalacPositional {
+ val fixedType = UnitType
+ var invariant: Option[Expr] = None
+
+ def getInvariant: Expr = invariant.get
+ def setInvariant(inv: Expr) = { invariant = Some(inv); this }
+ def setInvariant(inv: Option[Expr]) = { invariant = inv; this }
+ }
+
/* This describes computational errors (unmatched case, taking min of an
* empty set, division by zero, etc.). It should always be typed according to
* 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
@@ -29,6 +49,26 @@ object Trees {
if(et != Untyped)
setType(et)
}
+ //same as let, buf for mutable variable declaration
+ case class LetVar(binder: Identifier, value: Expr, body: Expr) extends Expr {
+ binder.markAsLetBinder
+ val et = body.getType
+ if(et != Untyped)
+ setType(et)
+ }
+
+ //case class LetTuple(binders: Seq[Identifier], value: Expr, body: Expr) extends Expr {
+ // binders.foreach(_.markAsLetBinder)
+ // val et = body.getType
+ // if(et != Untyped)
+ // setType(et)
+ //}
+
+ case class LetDef(value: FunDef, body: Expr) extends Expr {
+ val et = body.getType
+ if(et != Untyped)
+ setType(et)
+ }
/* Control flow */
case class FunctionInvocation(funDef: FunDef, args: Seq[Expr]) extends Expr with FixedType with ScalacPositional {
@@ -47,6 +87,7 @@ object Trees {
case CaseClassPattern(_, ccd, _) if ccd != c.classDef => false
case _ => true
}))
+ case t: TupleType => new MatchExpr(scrutinee, cases)
case _ => scala.sys.error("Constructing match expression on non-class type.")
}
}
@@ -105,6 +146,8 @@ object Trees {
// subPatterns: Seq[Pattern]) extends Pattern // c @ Extractor(...,...)
// We don't handle Seq stars for now.
+ case class TuplePattern(binder: Option[Identifier], subPatterns: Seq[Pattern]) extends Pattern
+
/* Propositional logic */
object And {
def apply(l: Expr, r: Expr) : Expr = (l,r) match {
@@ -225,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
@@ -237,6 +282,10 @@ object Trees {
val fixedType = BooleanType
}
case class StringLiteral(value: String) extends Literal[String]
+ case object UnitLiteral extends Literal[Unit] with FixedType {
+ val fixedType = UnitType
+ val value = ()
+ }
case class CaseClass(classDef: CaseClassDef, args: Seq[Expr]) extends Expr with FixedType {
val fixedType = CaseClassType(classDef)
@@ -323,7 +372,7 @@ object Trees {
case class SingletonMap(from: Expr, to: Expr) extends Expr
case class FiniteMap(singletons: Seq[SingletonMap]) extends Expr
- case class MapGet(map: Expr, key: Expr) extends Expr
+ case class MapGet(map: Expr, key: Expr) extends Expr with ScalacPositional
case class MapUnion(map1: Expr, map2: Expr) extends Expr
case class MapDifference(map: Expr, keys: Expr) extends Expr
case class MapIsDefinedAt(map: Expr, key: Expr) extends Expr with FixedType {
@@ -360,7 +409,9 @@ object Trees {
case SetMax(s) => Some((s,SetMax))
case CaseClassSelector(cd, e, sel) => Some((e, CaseClassSelector(cd, _, sel)))
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
}
}
@@ -391,12 +442,13 @@ object Trees {
case MultisetPlus(t1,t2) => Some((t1,t2,MultisetPlus))
case MultisetDifference(t1,t2) => Some((t1,t2,MultisetDifference))
case SingletonMap(t1,t2) => Some((t1,t2,SingletonMap))
- case MapGet(t1,t2) => Some((t1,t2,MapGet))
+ case mg@MapGet(t1,t2) => Some((t1,t2, (t1, t2) => MapGet(t1, t2).setPosInfo(mg)))
case MapUnion(t1,t2) => Some((t1,t2,MapUnion))
case MapDifference(t1,t2) => Some((t1,t2,MapDifference))
case MapIsDefinedAt(t1,t2) => Some((t1,t2, MapIsDefinedAt))
case Concat(t1,t2) => Some((t1,t2,Concat))
case ListAt(t1,t2) => Some((t1,t2,ListAt))
+ case wh@While(t1, t2) => Some((t1,t2, (t1, t2) => While(t1, t2).setInvariant(wh.invariant).setPosInfo(wh)))
case _ => None
}
}
@@ -412,6 +464,7 @@ object Trees {
case FiniteMap(args) => Some((args, (as : Seq[Expr]) => FiniteMap(as.asInstanceOf[Seq[SingletonMap]])))
case FiniteMultiset(args) => Some((args, FiniteMultiset))
case Distinct(args) => Some((args, Distinct))
+ case Block(args, rest) => Some((args :+ rest, exprs => Block(exprs.init, exprs.last)))
case Tuple(args) => Some((args, Tuple))
case _ => None
}
@@ -464,6 +517,21 @@ object Trees {
else
l
}
+ case l @ LetVar(i,e,b) => {
+ val re = rec(e)
+ val rb = rec(b)
+ if(re != e || rb != b)
+ LetVar(i, re, rb).setType(l.getType)
+ else
+ l
+ }
+ case l @ LetDef(fd, b) => {
+ //TODO, not sure, see comment for the next LetDef
+ fd.body = fd.body.map(rec(_))
+ fd.precondition = fd.precondition.map(rec(_))
+ fd.postcondition = fd.postcondition.map(rec(_))
+ LetDef(fd, rec(b)).setType(l.getType)
+ }
case n @ NAryOperator(args, recons) => {
var change = false
val rargs = args.map(a => {
@@ -547,6 +615,23 @@ object Trees {
l
})
}
+ case l @ LetVar(i,e,b) => {
+ val re = rec(e)
+ val rb = rec(b)
+ applySubst(if(re != e || rb != b) {
+ LetVar(i,re,rb).setType(l.getType)
+ } else {
+ l
+ })
+ }
+ case l @ LetDef(fd,b) => {
+ //TODO: Not sure: I actually need the replace to occurs even in the pre/post condition, hope this is correct
+ fd.body = fd.body.map(rec(_))
+ fd.precondition = fd.precondition.map(rec(_))
+ fd.postcondition = fd.postcondition.map(rec(_))
+ val rl = LetDef(fd, rec(b)).setType(l.getType)
+ applySubst(rl)
+ }
case n @ NAryOperator(args, recons) => {
var change = false
val rargs = args.map(a => {
@@ -670,6 +755,11 @@ object Trees {
def treeCatamorphism[A](convert: Expr=>A, combine: (A,A)=>A, compute: (Expr,A)=>A, expression: Expr) : A = {
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) => {//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))
@@ -688,6 +778,71 @@ object Trees {
rec(expression)
}
+ def flattenBlocks(expr: Expr): Expr = {
+ def applyToTree(expr: Expr): Option[Expr] = expr match {
+ case Block(exprs, last) => {
+ val nexprs = (exprs :+ last).flatMap{
+ case Block(es2, el) => es2 :+ el
+ case UnitLiteral => Seq()
+ case e2 => Seq(e2)
+ }
+ val fexpr = nexprs match {
+ case Seq() => UnitLiteral
+ case Seq(e) => e
+ case es => Block(es.init, es.last).setType(es.last.getType)
+ }
+ Some(fexpr)
+ }
+ case _ => None
+ }
+ searchAndReplaceDFS(applyToTree)(expr)
+ }
+
+ //checking whether the expr is pure, that is do not contains any non-pure construct: assign, while and blocks
+ def isPure(expr: Expr): Boolean = {
+ def convert(t: Expr) : Boolean = t match {
+ case Block(_, _) => false
+ case Assignment(_, _) => false
+ case While(_, _) => false
+ case LetVar(_, _, _) => false
+ case _ => true
+ }
+ def combine(b1: Boolean, b2: Boolean) = b1 && b2
+ def compute(e: Expr, b: Boolean) = e match {
+ case Block(_, _) => false
+ case Assignment(_, _) => false
+ case While(_, _) => false
+ case LetVar(_, _, _) => false
+ case _ => b
+ }
+ treeCatamorphism(convert, combine, compute, expr)
+ }
+
+ def containsEpsilon(expr: Expr): Boolean = {
+ def convert(t : Expr) : Boolean = t match {
+ case (l : Epsilon) => true
+ case _ => false
+ }
+ def combine(c1 : Boolean, c2 : Boolean) : Boolean = c1 || c2
+ def compute(t : Expr, c : Boolean) = t match {
+ case (l : Epsilon) => true
+ case _ => c
+ }
+ 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)
@@ -767,6 +922,8 @@ object Trees {
def allIdentifiers(expr: Expr) : Set[Identifier] = expr match {
case l @ Let(binder, e, b) => allIdentifiers(e) ++ allIdentifiers(b) + binder
+ case l @ LetVar(binder, e, b) => allIdentifiers(e) ++ allIdentifiers(b) + binder
+ case l @ LetDef(fd, b) => allIdentifiers(fd.getBody) ++ allIdentifiers(b) + fd.id
case n @ NAryOperator(args, _) =>
(args map (Trees.allIdentifiers(_))).foldLeft(Set[Identifier]())((a, b) => a ++ b)
case b @ BinaryOperator(a1,a2,_) => allIdentifiers(a1) ++ allIdentifiers(a2)
@@ -940,7 +1097,9 @@ object Trees {
val MatchExpr(scrutinee, cases) = e
val sType = scrutinee.getType
- if(sType.isInstanceOf[AbstractClassType]) {
+ if(sType.isInstanceOf[TupleType]) {
+ None
+ } else if(sType.isInstanceOf[AbstractClassType]) {
val cCD = sType.asInstanceOf[AbstractClassType].classDef
if(cases.size == cCD.knownChildren.size && cases.forall(!_.hasGuard)) {
var seen = Set.empty[ClassTypeDef]
@@ -1086,6 +1245,17 @@ object Trees {
case None => together
}
}
+ case TuplePattern(b, subps) => {
+ val TupleType(tpes) = in.getType
+ assert(tpes.size == subps.size)
+
+ val maps = subps.zipWithIndex.map{case (p, i) => mapForPattern(TupleSelect(in, i+1).setType(tpes(i)), p)}
+ val map = maps.foldLeft(Map.empty[Identifier,Expr])(_ ++ _)
+ b match {
+ case Some(id) => map + (id -> in)
+ case None => map
+ }
+ }
}
def conditionForPattern(in: Expr, pattern: Pattern) : Expr = pattern match {
@@ -1098,6 +1268,12 @@ object Trees {
val together = And(subTests)
And(CaseClassInstanceOf(ccd, in), together)
}
+ case TuplePattern(_, subps) => {
+ val TupleType(tpes) = in.getType
+ assert(tpes.size == subps.size)
+ val subTests = subps.zipWithIndex.map{case (p, i) => conditionForPattern(TupleSelect(in, i+1).setType(tpes(i)), p)}
+ And(subTests)
+ }
}
def rewritePM(e: Expr) : Option[Expr] = e match {
@@ -1158,7 +1334,7 @@ object Trees {
def rewriteMapGet(e: Expr) : Option[Expr] = e match {
case mg @ MapGet(m,k) =>
val ida = MapIsDefinedAt(m, k)
- Some(IfExpr(ida, mg, Error("key not found for map access").setType(mg.getType)).setType(mg.getType))
+ Some(IfExpr(ida, mg, Error("key not found for map access").setType(mg.getType).setPosInfo(mg)).setType(mg.getType))
case _ => None
}
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index e948a433f42e58cb452877414fada6fae5f8da5d..31947bf28177682e1376f0fd013944ef9dc37c05 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -97,6 +97,7 @@ object TypeTrees {
case AnyType => InfiniteSize
case BottomType => FiniteSize(0)
case BooleanType => FiniteSize(2)
+ case UnitType => FiniteSize(1)
case Int32Type => InfiniteSize
case ListType(_) => InfiniteSize
case TupleType(bases) => {
@@ -138,6 +139,7 @@ object TypeTrees {
case object BottomType extends TypeTree // This type is useful when we need an underlying type for None, Set.empty, etc. It should always be removed after parsing, though.
case object BooleanType extends TypeTree
case object Int32Type extends TypeTree
+ case object UnitType extends TypeTree
case class ListType(base: TypeTree) extends TypeTree
case class TupleType(bases: Seq[TypeTree]) extends TypeTree { lazy val dimension: Int = bases.length }
diff --git a/testcases/Abs.scala b/testcases/Abs.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5efb41797b5dc4401407c5fea7c3fc6a7591f4f2
--- /dev/null
+++ b/testcases/Abs.scala
@@ -0,0 +1,51 @@
+import leon.Utils._
+
+object Abs {
+
+
+ def abs(tab: Map[Int, Int], size: Int): Map[Int, Int] = ({
+ require(size <= 5 && isArray(tab, size))
+ var k = 0
+ var tabres = Map.empty[Int, Int]
+ (while(k < size) {
+ if(tab(k) < 0)
+ tabres = tabres.updated(k, -tab(k))
+ else
+ tabres = tabres.updated(k, tab(k))
+ k = k + 1
+ }) invariant(isArray(tabres, k) && k >= 0 && k <= size && isPositive(tabres, k))
+ tabres
+ }) ensuring(res => isArray(res, size) && isPositive(res, size))
+
+ def isPositive(a: Map[Int, Int], size: Int): Boolean = {
+ require(size <= 10 && isArray(a, size))
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size)
+ true
+ else {
+ if(a(i) < 0)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ }
+
+ if(size < 0)
+ false
+ else
+ rec(0)
+ }
+
+}
diff --git a/testcases/Add.scala b/testcases/Add.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5d125e3c72f29d96fdaa7176756efe11ca36b98a
--- /dev/null
+++ b/testcases/Add.scala
@@ -0,0 +1,25 @@
+import leon.Utils._
+
+/* VSTTE 2008 - Dafny paper */
+
+object Add {
+
+ def add(x : Int, y : Int): Int = ({
+ var r = x
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - 1
+ n = n + 1
+ }) invariant(r == x + y - n && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + 1
+ n = n - 1
+ }) invariant(r == x + y - n && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x+y)
+
+}
diff --git a/testcases/BinarySearch.scala b/testcases/BinarySearch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..92d4cf0667fe0175b80ae0da34679e991efcc633
--- /dev/null
+++ b/testcases/BinarySearch.scala
@@ -0,0 +1,73 @@
+import leon.Utils._
+
+/* VSTTE 2008 - Dafny paper */
+
+object BinarySearch {
+
+ def binarySearch(a: Map[Int, Int], size: Int, key: Int): Int = ({
+ require(isArray(a, size) && size < 5 && sorted(a, size, 0, size - 1))
+ var low = 0
+ var high = size - 1
+ var res = -1
+
+ (while(low <= high && res == -1) {
+ val i = (high + low) / 2
+ val v = a(i)
+
+ if(v == key)
+ res = i
+
+ if(v > key)
+ high = i - 1
+ else if(v < key)
+ low = i + 1
+ }) invariant(0 <= low && low <= high + 1 && high < size && (if(res >= 0) a(res) == key else (!occurs(a, 0, low, key) && !occurs(a, high + 1, size, key))))
+ res
+ }) ensuring(res => res >= -1 && res < size && (if(res >= 0) a(res) == key else !occurs(a, 0, size, key)))
+
+
+ def occurs(a: Map[Int, Int], from: Int, to: Int, key: Int): Boolean = {
+ require(isArray(a, to) && to < 5 && from >= 0)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= to)
+ false
+ else {
+ if(a(i) == key) true else rec(i+1)
+ }
+ }
+ if(from >= to)
+ false
+ else
+ rec(from)
+ }
+
+
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ }
+
+ if(size < 0)
+ false
+ else
+ rec(0)
+ }
+
+ def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
+ val t = sortedWhile(true, l, l, u, a, size)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
+ } else (isSorted, k)
+ }
+}
diff --git a/testcases/BubbleFun.scala b/testcases/BubbleFun.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5962eea28e93cbd3d496ae9c7dd92af3a1297d15
--- /dev/null
+++ b/testcases/BubbleFun.scala
@@ -0,0 +1,153 @@
+object BubbleFun {
+
+ // --------------------- sort ----------------------
+
+ def sort(a: Map[Int,Int], size: Int): Map[Int,Int] = ({
+ require(isArray(a, size) && size < 5)
+
+ val i = size - 1
+ val t = sortWhile(0, a, i, size)
+ t._2
+ }) ensuring(res => isArray(res, size) && sorted(res, size, 0, size-1) /*&& content(res, size) == content(a, size)*/)
+
+ def sortWhile(j: Int, sortedArray: Map[Int,Int], i: Int, size: Int) : (Int, Map[Int,Int], Int) = ({
+ require(i >= 0 && i < size && isArray(sortedArray, size) && size < 5 &&
+ sorted(sortedArray, size, i, size - 1) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1))
+
+ if (i > 0) {
+ val t = sortNestedWhile(sortedArray, 0, i, size)
+ sortWhile(t._2, t._1, i - 1, size)
+ } else (j, sortedArray, i)
+ }) ensuring(res => isArray(res._2, size) &&
+ sorted(res._2, size, res._3, size - 1) &&
+ partitioned(res._2, size, 0, res._3, res._3+1, size-1) &&
+ res._3 >= 0 && res._3 <= 0 /*&& content(res._2, size) == content(sortedArray, size)*/
+ )
+
+
+ def sortNestedWhile(sortedArray: Map[Int,Int], j: Int, i: Int, size: Int) : (Map[Int,Int], Int) = ({
+ require(j >= 0 && j <= i && i < size && isArray(sortedArray, size) && size < 5 &&
+ sorted(sortedArray, size, i, size - 1) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+ partitioned(sortedArray, size, 0, j-1, j, j))
+ if(j < i) {
+ val newSortedArray =
+ if(sortedArray(j) > sortedArray(j + 1))
+ sortedArray.updated(j, sortedArray(j + 1)).updated(j+1, sortedArray(j))
+ else
+ sortedArray
+ sortNestedWhile(newSortedArray, j + 1, i, size)
+ } else (sortedArray, j)
+ }) ensuring(res => isArray(res._1, size) &&
+ sorted(res._1, size, i, size - 1) &&
+ partitioned(res._1, size, 0, i, i+1, size-1) &&
+ partitioned(res._1, size, 0, res._2-1, res._2, res._2) &&
+ res._2 >= i && res._2 >= 0 && res._2 <= i /*&& content(res._1, size) == content(sortedArray, size)*/)
+
+
+ //some intermediate results
+ def lemma1(a: Map[Int, Int], size: Int, i: Int): Boolean = ({
+ require(isArray(a, size) && size < 5 && sorted(a, size, i, size-1) && partitioned(a, size, 0, i, i+1, size-1) && i >= 0 && i < size)
+ val t = sortNestedWhile(a, 0, i, size)
+ val newJ = t._2
+ i == newJ
+ }) ensuring(_ == true)
+ def lemma2(a: Map[Int, Int], size: Int, i: Int): Boolean = ({
+ require(isArray(a, size) && size < 5 && sorted(a, size, i, size-1) && partitioned(a, size, 0, i, i+1, size-1) && i >= 0 && i < size)
+ val t = sortNestedWhile(a, 0, i, size)
+ val newA = t._1
+ val newJ = t._2
+ partitioned(newA, size, 0, i-1, i, i)
+ }) ensuring(_ == true)
+ def lemma3(a: Map[Int, Int], size: Int, i: Int): Boolean = ({
+ require(partitioned(a, size, 0, i, i+1, size-1) && partitioned(a, size, 0, i-1, i, i) && isArray(a, size) && size < 5 && i >= 0 && i < size)
+ partitioned(a, size, 0, i-1, i, size-1)
+ }) ensuring(_ == true)
+ def lemma4(a: Map[Int, Int], size: Int, i: Int): Boolean = ({
+ require(isArray(a, size) && size < 5 && sorted(a, size, i, size-1) && partitioned(a, size, 0, i, i+1, size-1) && i >= 0 && i < size)
+ val t = sortNestedWhile(a, 0, i, size)
+ val newA = t._1
+ partitioned(newA, size, 0, i-1, i, size-1)
+ }) ensuring(_ == true)
+
+
+ // --------------------- sorted --------------------
+ def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
+ val t = sortedWhile(true, l, l, u, a, size)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
+ } else (isSorted, k)
+ }
+
+
+
+ // ------------- partitioned ------------------
+ def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
+ t._2
+ }
+ }
+ def partitionedWhile(j: Int, isPartitionned: Boolean, i: Int, l1: Int, size: Int, u2: Int, l2: Int, u1: Int, a: Map[Int,Int]) : (Int, Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && i >= l1)
+
+ if(i <= u1) {
+ val t = partitionedNestedWhile(isPartitionned, l2, i, l1, u1, size, u2, a, l2)
+ partitionedWhile(t._2, t._1, i + 1, l1, size, u2, l2, u1, a)
+ } else (j, isPartitionned, i)
+ }
+ def partitionedNestedWhile(isPartitionned: Boolean, j: Int, i: Int, l1: Int, u1: Int, size: Int, u2: Int, a: Map[Int,Int], l2: Int): (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && j >= l2 && i >= l1 && i <= u1)
+
+ if (j <= u2) {
+ partitionedNestedWhile(
+ (if (a(i) > a(j))
+ false
+ else
+ isPartitionned),
+ j + 1, i, l1, u1, size, u2, a, l2)
+ } else (isPartitionned, j)
+ }
+
+
+ //------------ isArray -------------------
+ def isArray(a: Map[Int,Int], size: Int): Boolean =
+ if(size <= 0)
+ false
+ else
+ isArrayRec(0, size, a)
+
+ def isArrayRec(i: Int, size: Int, a: Map[Int,Int]): Boolean =
+ if (i >= size)
+ true
+ else {
+ if(a.isDefinedAt(i))
+ isArrayRec(i + 1, size, a)
+ else
+ false
+ }
+
+
+ // ----------------- content ------------------
+ def content(a: Map[Int, Int], size: Int): Set[Int] = {
+ require(isArray(a, size) && size < 5)
+ var i = 0
+ var s = Set.empty[Int]
+ while(i < size) {
+ s = s ++ Set(a(i))
+ i = i + 1
+ }
+ s
+ }
+
+}
diff --git a/testcases/BubbleSort.scala b/testcases/BubbleSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4e274e2707b0cff262e712ab4b78b53eee0db990
--- /dev/null
+++ b/testcases/BubbleSort.scala
@@ -0,0 +1,132 @@
+import leon.Utils._
+
+/* The calculus of Computation textbook */
+
+object Bubble {
+
+ def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = ({
+ require(size < 5 && isArray(a, size))
+ var i = size - 1
+ var j = 0
+ var sortedArray = a
+ (while(i > 0) {
+ j = 0
+ (while(j < i) {
+ if(sortedArray(j) > sortedArray(j+1)) {
+ val tmp = sortedArray(j)
+ sortedArray = sortedArray.updated(j, sortedArray(j+1))
+ sortedArray = sortedArray.updated(j+1, tmp)
+ }
+ j = j + 1
+ }) invariant(
+ j >= 0 &&
+ j <= i &&
+ i < size &&
+ isArray(sortedArray, size) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+ sorted(sortedArray, size, i, size-1) &&
+ partitioned(sortedArray, size, 0, j-1, j, j)
+ )
+ i = i - 1
+ }) invariant(
+ i >= 0 &&
+ i < size &&
+ isArray(sortedArray, size) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+ sorted(sortedArray, size, i, size-1)
+ )
+ sortedArray
+ }) ensuring(res => sorted(res, size, 0, size-1))
+
+ def sorted(a: Map[Int, Int], size: Int, l: Int, u: Int): Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && u < size && l <= u)
+ var k = l
+ var isSorted = true
+ (while(k < u) {
+ if(a(k) > a(k+1))
+ isSorted = false
+ k = k + 1
+ }) invariant(k <= u && k >= l)
+ isSorted
+ }
+ /*
+ // --------------------- sorted --------------------
+ def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
+ val t = sortedWhile(true, l, l, u, a, size)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
+ } else (isSorted, k)
+ }
+ */
+
+ /*
+ // ------------- partitioned ------------------
+ def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
+ t._2
+ }
+ }
+ def partitionedWhile(j: Int, isPartitionned: Boolean, i: Int, l1: Int, size: Int, u2: Int, l2: Int, u1: Int, a: Map[Int,Int]) : (Int, Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && i >= l1)
+
+ if(i <= u1) {
+ val t = partitionedNestedWhile(isPartitionned, l2, i, l1, u1, size, u2, a, l2)
+ partitionedWhile(t._2, t._1, i + 1, l1, size, u2, l2, u1, a)
+ } else (j, isPartitionned, i)
+ }
+ def partitionedNestedWhile(isPartitionned: Boolean, j: Int, i: Int, l1: Int, u1: Int, size: Int, u2: Int, a: Map[Int,Int], l2: Int): (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && j >= l2 && i >= l1 && i <= u1)
+
+ if (j <= u2) {
+ partitionedNestedWhile(
+ (if (a(i) > a(j))
+ false
+ else
+ isPartitionned),
+ j + 1, i, l1, u1, size, u2, a, l2)
+ } else (isPartitionned, j)
+ }
+ */
+
+ def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(l1 >= 0 && u1 < l2 && u2 < size && isArray(a, size) && size < 5)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
+ }
+
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+ def rec(i: Int): Boolean = if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ if(size <= 0)
+ false
+ else
+ rec(0)
+ }
+
+}
diff --git a/testcases/BubbleWeakInvariant.scala b/testcases/BubbleWeakInvariant.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d335cb81ffce8831f0dc1c203ab47c227d761e7f
--- /dev/null
+++ b/testcases/BubbleWeakInvariant.scala
@@ -0,0 +1,132 @@
+import leon.Utils._
+
+/* The calculus of Computation textbook */
+
+object Bubble {
+
+ def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = ({
+ require(size < 5 && isArray(a, size))
+ var i = size - 1
+ var j = 0
+ var sortedArray = a
+ (while(i > 0) {
+ j = 0
+ (while(j < i) {
+ if(sortedArray(j) > sortedArray(j+1)) {
+ val tmp = sortedArray(j)
+ sortedArray = sortedArray.updated(j, sortedArray(j+1))
+ sortedArray = sortedArray.updated(j+1, tmp)
+ }
+ j = j + 1
+ }) invariant(
+ j >= 0 &&
+ j <= i &&
+ i < size &&
+ isArray(sortedArray, size) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+ //partitioned(sortedArray, size, 0, j-1, j, j) &&
+ sorted(sortedArray, size, i, size-1)
+ )
+ i = i - 1
+ }) invariant(
+ i >= 0 &&
+ i < size &&
+ isArray(sortedArray, size) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+ sorted(sortedArray, size, i, size-1)
+ )
+ sortedArray
+ }) ensuring(res => sorted(res, size, 0, size-1))
+
+ def sorted(a: Map[Int, Int], size: Int, l: Int, u: Int): Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && u < size && l <= u)
+ var k = l
+ var isSorted = true
+ (while(k < u) {
+ if(a(k) > a(k+1))
+ isSorted = false
+ k = k + 1
+ }) invariant(k <= u && k >= l)
+ isSorted
+ }
+ /*
+ // --------------------- sorted --------------------
+ def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
+ val t = sortedWhile(true, l, l, u, a, size)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
+ } else (isSorted, k)
+ }
+ */
+
+ /*
+ // ------------- partitioned ------------------
+ def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
+ t._2
+ }
+ }
+ def partitionedWhile(j: Int, isPartitionned: Boolean, i: Int, l1: Int, size: Int, u2: Int, l2: Int, u1: Int, a: Map[Int,Int]) : (Int, Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && i >= l1)
+
+ if(i <= u1) {
+ val t = partitionedNestedWhile(isPartitionned, l2, i, l1, u1, size, u2, a, l2)
+ partitionedWhile(t._2, t._1, i + 1, l1, size, u2, l2, u1, a)
+ } else (j, isPartitionned, i)
+ }
+ def partitionedNestedWhile(isPartitionned: Boolean, j: Int, i: Int, l1: Int, u1: Int, size: Int, u2: Int, a: Map[Int,Int], l2: Int): (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && j >= l2 && i >= l1 && i <= u1)
+
+ if (j <= u2) {
+ partitionedNestedWhile(
+ (if (a(i) > a(j))
+ false
+ else
+ isPartitionned),
+ j + 1, i, l1, u1, size, u2, a, l2)
+ } else (isPartitionned, j)
+ }
+ */
+
+ def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(l1 >= 0 && u1 < l2 && u2 < size && isArray(a, size) && size < 5)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
+ }
+
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+ def rec(i: Int): Boolean = if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ if(size <= 0)
+ false
+ else
+ rec(0)
+ }
+
+}
diff --git a/testcases/LinearSearch.scala b/testcases/LinearSearch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e91a3f2679b33b8b35e7d64989db1b7ade451d14
--- /dev/null
+++ b/testcases/LinearSearch.scala
@@ -0,0 +1,53 @@
+import leon.Utils._
+
+/* The calculus of Computation textbook */
+
+object LinearSearch {
+
+ def linearSearch(a: Map[Int, Int], size: Int, c: Int): Boolean = ({
+ require(size <= 5 && isArray(a, size))
+ var i = 0
+ var found = false
+ (while(i < size) {
+ if(a(i) == c)
+ found = true
+ i = i + 1
+ }) invariant(i <= size &&
+ i >= 0 &&
+ (if(found) contains(a, i, c) else !contains(a, i, c))
+ )
+ found
+ }) ensuring(res => if(res) contains(a, size, c) else !contains(a, size, c))
+
+ def contains(a: Map[Int, Int], size: Int, c: Int): Boolean = {
+ require(isArray(a, size) && size <= 5)
+ content(a, size).contains(c)
+ }
+
+
+ def content(a: Map[Int, Int], size: Int): Set[Int] = {
+ require(isArray(a, size) && size <= 5)
+ var set = Set.empty[Int]
+ var i = 0
+ (while(i < size) {
+ set = set ++ Set(a(i))
+ i = i + 1
+ }) invariant(i >= 0 && i <= size)
+ set
+ }
+
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ }
+
+ if(size < 0)
+ false
+ else
+ rec(0)
+ }
+}
diff --git a/testcases/MaxSum.scala b/testcases/MaxSum.scala
new file mode 100644
index 0000000000000000000000000000000000000000..07c5d12ab2450cc95af964c7078759a13fe8f0cb
--- /dev/null
+++ b/testcases/MaxSum.scala
@@ -0,0 +1,70 @@
+import leon.Utils._
+
+/* VSTTE 2010 challenge 1 */
+
+object MaxSum {
+
+
+ def maxSum(a: Map[Int, Int], size: Int): (Int, Int) = ({
+ require(isArray(a, size) && size < 5 && isPositive(a, size))
+ var sum = 0
+ var max = 0
+ var i = 0
+ (while(i < size) {
+ if(max < a(i))
+ max = a(i)
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant (sum <= i * max && /*isGreaterEq(a, i, max) &&*/ /*(if(i == 0) max == 0 else true) &&*/ i >= 0 && i <= size)
+ (sum, max)
+ }) ensuring(res => res._1 <= size * res._2)
+
+/*
+ def isGreaterEq(a: Map[Int, Int], size: Int, n: Int): Boolean = {
+ require(size <= 5 && isArray(a, size))
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size)
+ true
+ else {
+ if(a(i) > n)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+ */
+
+ def isPositive(a: Map[Int, Int], size: Int): Boolean = {
+ require(size <= 5 && isArray(a, size))
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size)
+ true
+ else {
+ if(a(i) < 0)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ }
+
+ if(size < 0)
+ false
+ else
+ rec(0)
+ }
+}
diff --git a/testcases/Mult.scala b/testcases/Mult.scala
new file mode 100644
index 0000000000000000000000000000000000000000..417e9e9cdc74440ccac679b2d55bac33a6381e4a
--- /dev/null
+++ b/testcases/Mult.scala
@@ -0,0 +1,26 @@
+import leon.Utils._
+
+/* VSTTE 2008 - Dafny paper */
+
+object Mult {
+
+ def mult(x : Int, y : Int): Int = ({
+ var r = 0
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - x
+ n = n + 1
+ }) invariant(r == x * (y - n) && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + x
+ n = n - 1
+ }) invariant(r == x * (y - n) && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x*y)
+
+}
+
diff --git a/testcases/regression/invalid/Epsilon1.scala b/testcases/regression/invalid/Epsilon1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..859ced1c19b0c3688ad8eef433fbc290c672fbe9
--- /dev/null
+++ b/testcases/regression/invalid/Epsilon1.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def greaterWrong(x: Int): Int = {
+ epsilon((y: Int) => y >= x)
+ } ensuring(_ > x)
+
+}
diff --git a/testcases/regression/invalid/Epsilon2.scala b/testcases/regression/invalid/Epsilon2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..20699fc427e7dce9025e578767f5364ae19aaf88
--- /dev/null
+++ b/testcases/regression/invalid/Epsilon2.scala
@@ -0,0 +1,11 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def rand3(x: Int): Int = epsilon((y: Int) => x == x)
+
+ //this should not hold
+ def property3(x: Int): Boolean = {
+ rand3(x) == rand3(x+1)
+ } holds
+}
diff --git a/testcases/regression/invalid/Epsilon3.scala b/testcases/regression/invalid/Epsilon3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5ff47b6d638cc7270640f0bba95f4cd572f8201a
--- /dev/null
+++ b/testcases/regression/invalid/Epsilon3.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon3 {
+
+ def posWrong(): Int = {
+ epsilon((y: Int) => y >= 0)
+ } ensuring(_ > 0)
+
+}
diff --git a/testcases/regression/invalid/Epsilon4.scala b/testcases/regression/invalid/Epsilon4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..52ee6dbe66c2d5b3517d5d84f90f35f8f10aa38d
--- /dev/null
+++ b/testcases/regression/invalid/Epsilon4.scala
@@ -0,0 +1,27 @@
+import leon.Utils._
+
+object Epsilon4 {
+
+ 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)))
+ }
+
+
+ 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/testcases/regression/invalid/Epsilon5.scala b/testcases/regression/invalid/Epsilon5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b96fa7564e5dba8a44aeb9d750034153b362ebfe
--- /dev/null
+++ b/testcases/regression/invalid/Epsilon5.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon5 {
+
+ def fooWrong(x: Int, y: Int): Int = {
+ epsilon((z: Int) => z >= x && z <= y)
+ } ensuring(_ > x)
+
+}
diff --git a/testcases/regression/invalid/IfExpr1.scala b/testcases/regression/invalid/IfExpr1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..25ae2a2103b1e2cfd8bf886442adeabf12bb6dc3
--- /dev/null
+++ b/testcases/regression/invalid/IfExpr1.scala
@@ -0,0 +1,13 @@
+object IfExpr1 {
+
+ def foo(): Int = {
+ var a = 1
+ var b = 2
+ if({a = a + 1; a != b})
+ a = a + 3
+ else
+ b = a + b
+ a
+ } ensuring(_ == 3)
+
+}
diff --git a/testcases/regression/invalid/IfExpr2.scala b/testcases/regression/invalid/IfExpr2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1284904b5c7dfda8f601e130b6346680538aa99a
--- /dev/null
+++ b/testcases/regression/invalid/IfExpr2.scala
@@ -0,0 +1,14 @@
+object IfExpr2 {
+
+ def foo(): Int = {
+ var a = 1
+ var b = 2
+ if(a < b) {
+ a = a + 3
+ b = b + 2
+ a = a + b
+ }
+ a
+ } ensuring(_ == 0)
+
+}
diff --git a/testcases/regression/invalid/MyTuple1.scala b/testcases/regression/invalid/MyTuple1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f2b06b5b28e405bfb2487875c8e964b8f212792c
--- /dev/null
+++ b/testcases/regression/invalid/MyTuple1.scala
@@ -0,0 +1,11 @@
+object MyTuple1 {
+
+ def foo(): Int = {
+ val t = (1, true, 3)
+ val a1 = t._1
+ val a2 = t._2
+ val a3 = t._3
+ a3
+ } ensuring( _ == 1)
+
+}
diff --git a/testcases/regression/invalid/MyTuple2.scala b/testcases/regression/invalid/MyTuple2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..22b62dc75b75b3193cb2f304118a89afbc90eb91
--- /dev/null
+++ b/testcases/regression/invalid/MyTuple2.scala
@@ -0,0 +1,14 @@
+object MyTuple2 {
+
+ abstract class A
+ case class B(i: Int) extends A
+ case class C(a: A) extends A
+
+ def foo(): Int = {
+ val t = (B(2), C(B(3)))
+ t match {
+ case (B(x), C(y)) => x
+ }
+ } ensuring( _ == 3)
+
+}
diff --git a/testcases/regression/valid/Assign1.scala b/testcases/regression/valid/Assign1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0506c6afb39b49ac5a15c77dc10ab60f54de9ee6
--- /dev/null
+++ b/testcases/regression/valid/Assign1.scala
@@ -0,0 +1,12 @@
+object Assign1 {
+
+ def foo(): Int = {
+ var a = 0
+ val tmp = a + 1
+ a = a + 2
+ a = a + tmp
+ a = a + 4
+ a
+ } ensuring(_ == 7)
+
+}
diff --git a/testcases/regression/valid/Epsilon1.scala b/testcases/regression/valid/Epsilon1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2ae7201dd933e345fa71a6218b48599a61110f44
--- /dev/null
+++ b/testcases/regression/valid/Epsilon1.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def greater(x: Int): Int = {
+ epsilon((y: Int) => y > x)
+ } ensuring(_ >= x)
+
+}
diff --git a/testcases/regression/valid/Epsilon2.scala b/testcases/regression/valid/Epsilon2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b4f53f36bf3b5c76a7c2fad5a4f1cdfed12587a9
--- /dev/null
+++ b/testcases/regression/valid/Epsilon2.scala
@@ -0,0 +1,18 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def rand(): Int = epsilon((x: Int) => true)
+ def rand2(x: Int): Int = epsilon((y: Int) => true)
+
+ //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
+
+}
diff --git a/testcases/regression/valid/Epsilon3.scala b/testcases/regression/valid/Epsilon3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f652016d28976d0b7e110b009a0802a7aac10c99
--- /dev/null
+++ b/testcases/regression/valid/Epsilon3.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon3 {
+
+ def pos(): Int = {
+ epsilon((y: Int) => y > 0)
+ } ensuring(_ >= 0)
+
+}
diff --git a/testcases/regression/valid/Epsilon4.scala b/testcases/regression/valid/Epsilon4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..174042863a690067fae5a2fd4aaf55f95bf29129
--- /dev/null
+++ b/testcases/regression/valid/Epsilon4.scala
@@ -0,0 +1,32 @@
+import leon.Utils._
+
+object Epsilon4 {
+
+ 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)))
+ }
+
+ //timeout, but this probably means that it is valid as expected
+ //def property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds
+
+ def propertyBase(lst: MyList): Boolean = ({
+ require(lst match { case MyNil() => true case _ => false})
+ size(toList(toSet(lst))) <= size(lst)
+ }) holds
+
+}
diff --git a/testcases/regression/valid/Epsilon5.scala b/testcases/regression/valid/Epsilon5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0427cf086ba1050226ae8a3e28d6177a9904b460
--- /dev/null
+++ b/testcases/regression/valid/Epsilon5.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon5 {
+
+ def foo(x: Int, y: Int): Int = {
+ epsilon((z: Int) => z > x && z < y)
+ } ensuring(_ >= x)
+
+}
diff --git a/testcases/regression/valid/IfExpr1.scala b/testcases/regression/valid/IfExpr1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..82db13d5285bc3c779010fd3e62b6e9e68e84e84
--- /dev/null
+++ b/testcases/regression/valid/IfExpr1.scala
@@ -0,0 +1,13 @@
+object IfExpr1 {
+
+ def foo(): Int = {
+ var a = 1
+ var b = 2
+ if({a = a + 1; a != b})
+ a = a + 3
+ else
+ b = a + b
+ a
+ } ensuring(_ == 2)
+
+}
diff --git a/testcases/regression/valid/IfExpr2.scala b/testcases/regression/valid/IfExpr2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7a681bc7276d07e41884147342dc0874d0bbf93d
--- /dev/null
+++ b/testcases/regression/valid/IfExpr2.scala
@@ -0,0 +1,14 @@
+object IfExpr2 {
+
+ def foo(): Int = {
+ var a = 1
+ var b = 2
+ if(a < b) {
+ a = a + 3
+ b = b + 2
+ a = a + b
+ }
+ a
+ } ensuring(_ == 8)
+
+}
diff --git a/testcases/regression/valid/MyTuple1.scala b/testcases/regression/valid/MyTuple1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..48383898e203c723751a7a53869ac6c8c69ae3b5
--- /dev/null
+++ b/testcases/regression/valid/MyTuple1.scala
@@ -0,0 +1,11 @@
+object MyTuple1 {
+
+ def foo(): Int = {
+ val t = (1, true, 3)
+ val a1 = t._1
+ val a2 = t._2
+ val a3 = t._3
+ a3
+ } ensuring( _ == 3)
+
+}
diff --git a/testcases/regression/valid/MyTuple2.scala b/testcases/regression/valid/MyTuple2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9fd21eb20b14350d86d06071800ec3b86acc1a84
--- /dev/null
+++ b/testcases/regression/valid/MyTuple2.scala
@@ -0,0 +1,14 @@
+object MyTuple2 {
+
+ abstract class A
+ case class B(i: Int) extends A
+ case class C(a: A) extends A
+
+ def foo(): Int = {
+ val t = (B(2), C(B(3)))
+ t match {
+ case (B(x), C(y)) => x
+ }
+ } ensuring(_ == 2)
+
+}
diff --git a/testcases/regression/valid/MyTuple3.scala b/testcases/regression/valid/MyTuple3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2e14c067b78d86d4d915eb72178169d641e9755a
--- /dev/null
+++ b/testcases/regression/valid/MyTuple3.scala
@@ -0,0 +1,8 @@
+object MyTuple3 {
+
+ def foo(): Int = {
+ val t = ((2, 3), true)
+ t._1._2
+ } ensuring( _ == 3)
+
+}
diff --git a/testcases/regression/valid/MyTuple4.scala b/testcases/regression/valid/MyTuple4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4b87272e23f7d9f2a3c33c29b5d455b88f234ddb
--- /dev/null
+++ b/testcases/regression/valid/MyTuple4.scala
@@ -0,0 +1,14 @@
+
+object MyTuple1 {
+
+ abstract class A
+ case class B(i: Int) extends A
+ case class C(a: A) extends A
+
+ def foo(): Int = {
+ val t = (1, (C(B(4)), 2), 3)
+ val (a1, (C(B(x)), a2), a3) = t
+ x
+ } ensuring( _ == 4)
+
+}
diff --git a/testcases/regression/valid/MyTuple5.scala b/testcases/regression/valid/MyTuple5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6a55bc8c9cdbc4f70be7a6b79c8d11137ecb0d71
--- /dev/null
+++ b/testcases/regression/valid/MyTuple5.scala
@@ -0,0 +1,16 @@
+object MyTuple1 {
+
+ abstract class A
+ case class B(t: (Int, Int)) extends A
+ case class C(a: A) extends A
+
+ def foo(): Int = {
+ val t: (Int, (A, Int), Int) = (1, (C(B((4, 5))), 2), 3)
+ t match {
+ case (_, (B((x, y)), _), _) => x
+ case (_, (C(B((_, x))), _), y) => x
+ case (_, _, x) => x
+ }
+ } ensuring( _ == 5)
+
+}
diff --git a/testcases/regression/valid/Nested1.scala b/testcases/regression/valid/Nested1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7745f794f369cf59b529133fa6c73383466acec8
--- /dev/null
+++ b/testcases/regression/valid/Nested1.scala
@@ -0,0 +1,15 @@
+object Nested1 {
+
+ def foo(i: Int): Int = {
+ val n = 2
+ def rec1(j: Int) = i + j + n
+ def rec2(j: Int) = {
+ def rec3(k: Int) = k + j + i
+ rec3(5)
+ }
+ rec2(2)
+ } ensuring(i + 7 == _)
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/regression/valid/While1.scala b/testcases/regression/valid/While1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0d868b399330c91342bd4ed26f7166f6b40dae5f
--- /dev/null
+++ b/testcases/regression/valid/While1.scala
@@ -0,0 +1,13 @@
+object While1 {
+
+ def foo(): Int = {
+ var a = 0
+ var i = 0
+ while(i < 10) {
+ a = a + 1
+ i = i + 1
+ }
+ a
+ } ensuring(_ == 10)
+
+}
diff --git a/testcases/regression/valid/While2.scala b/testcases/regression/valid/While2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e841ed40ebf045e5545b584b5c16e80bfc11396a
--- /dev/null
+++ b/testcases/regression/valid/While2.scala
@@ -0,0 +1,13 @@
+object While1 {
+
+ def foo(): Int = {
+ var a = 0
+ var i = 0
+ while(i < 10) {
+ a = a + i
+ i = i + 1
+ }
+ a
+ } ensuring(_ == 45)
+
+}
diff --git a/testcases/regression/valid/While3.scala b/testcases/regression/valid/While3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..da85d5dfab90410eb4d2ee23cea90627d1d40c93
--- /dev/null
+++ b/testcases/regression/valid/While3.scala
@@ -0,0 +1,13 @@
+object While3 {
+
+ def foo(): Int = {
+ var a = 0
+ var i = 0
+ while({i = i+2; i <= 10}) {
+ a = a + i
+ i = i - 1
+ }
+ a
+ } ensuring(_ == 54)
+
+}