diff --git a/lib/z3.jar b/lib/z3.jar
deleted file mode 100644
index 2fd797b68a3ae3d5a17bad12f77b857b7e2b4ef3..0000000000000000000000000000000000000000
Binary files a/lib/z3.jar and /dev/null differ
diff --git a/s-f b/s-f
index 0e04980aa1736203249654a48f26a1ca5dd54a08..5ac3f3d27a2b992290944f8cb26b752568384507 100755
--- a/s-f
+++ b/s-f
@@ -3,4 +3,4 @@ SCALALIBDIR=/home/psuter/scala/current/lib
DISTDIR=/home/psuter/guru-svn/funcheck/dist
LIBDIR=/home/psuter/guru-svn/funcheck/lib
SCALAHOME=/home/psuter/scala/current
-java -Dscala.home=${SCALAHOME} -classpath ${SCALALIBDIR}/scala-compiler.jar:${SCALALIBDIR}/scala-library.jar:${DISTDIR}/funcheck-plugin.jar:${LIBDIR}/z3.jar scala.tools.nsc.Main -Xplugin:${DISTDIR}/funcheck-plugin.jar $@
+LD_LIBRARY_PATH=/home/psuter/software/z3/lib java -Dscala.home=${SCALAHOME} -classpath ${SCALALIBDIR}/scala-compiler.jar:${SCALALIBDIR}/scala-library.jar:${DISTDIR}/funcheck-plugin.jar:${LIBDIR}/z3.jar scala.tools.nsc.Main -Xplugin:${DISTDIR}/funcheck-plugin.jar $@
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index f01145dae44bf5317dfdb24210130dd78f7a387e..220d46a057206db75b5ec992b3b5ded5ff86839d 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -17,18 +17,26 @@ object Analysis {
// - all global invariants are satisfied
def analyze(program: Program) : Unit = {
val z3cfg = new Z3Config()
- //z3cfg.setParamValue("MODEL", "TRUE")
+ z3cfg.setParamValue("MODEL", "true")
val z3 = new Z3Context(z3cfg)
program.mainObject.defs.filter(_.isInstanceOf[FunDef]).foreach(df => {
val funDef = df.asInstanceOf[FunDef]
val vc = postconditionVC(funDef)
if(vc != BooleanLiteral(true)) {
- println("Verification condition for " + funDef.id + ":")
+ println("Verification condition (post) for " + funDef.id + ":")
println(vc)
val (z3f,stupidMap) = toZ3Formula(z3, vc)
z3.assertCnstr(z3.mkNot(z3f))
- println("Valid? " + z3.check())
+ //z3.print
+ z3.checkAndGetModel() match {
+ case (Some(true),m) => {
+ println("There's a bug! Here's a model for a counter-example:")
+ m.print
+ }
+ case (Some(false),_) => println("Contract satisfied!")
+ case (None,_) => println("Z3 couldn't run properly or does not know the answer :(")
+ }
}
})
}
@@ -40,7 +48,10 @@ object Analysis {
if(post.isEmpty) {
BooleanLiteral(true)
} else {
- replaceInExpr(Map(ResultVariable() -> functionDefinition.body), post.get)
+ if(prec.isEmpty)
+ replaceInExpr(Map(ResultVariable() -> functionDefinition.body), post.get)
+ else
+ Implies(prec.get, replaceInExpr(Map(ResultVariable() -> functionDefinition.body), post.get))
}
}
@@ -63,7 +74,21 @@ object Analysis {
case And(exs) => And(exs.map(rec(_)))
case Or(exs) => Or(exs.map(rec(_)))
case Not(e) => Not(rec(e))
- case BinaryOperator(t1,t2,recons) => recons(rec(t1),rec(t2))
+ case u @ UnaryOperator(t,recons) => {
+ val r = rec(t)
+ if(r != t)
+ recons(r).setType(u.getType)
+ else
+ u
+ }
+ case b @ BinaryOperator(t1,t2,recons) => {
+ val r1 = rec(t1)
+ val r2 = rec(t2)
+ if(r1 != t1 || r2 != t2)
+ recons(r1,r2).setType(b.getType)
+ else
+ b
+ }
case _ => ex
}
@@ -89,6 +114,7 @@ object Analysis {
case Or(exs) => z3.mkOr(exs.map(rec(_)) : _*)
case Not(Equals(l,r)) => z3.mkDistinct(rec(l),rec(r))
case Not(e) => z3.mkNot(rec(e))
+ case Implies(l,r) => z3.mkImplies(rec(l), rec(r))
case IntLiteral(v) => z3.mkInt(v, intSort)
case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
case Equals(l,r) => z3.mkEq(rec(l),rec(r))
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index c96723707f278ed8a0b0aec944a71a993231e7df..99a6074b5010b82d1b1f05e7c59b8c241fadb027 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/src/purescala/PrettyPrinter.scala
@@ -72,6 +72,7 @@ object PrettyPrinter {
case Or(exprs) => ppNary(sb, exprs, " \u2228 ", lvl) // \lor
case Not(Equals(l, r)) => ppBinary(sb, l, r, " \u2260 ", lvl) // \neq
case Not(expr) => ppUnary(sb, expr, "\u00AC", lvl) // \neg
+ case Implies(l,r) => ppBinary(sb, l, r, "==>", lvl)
case UMinus(expr) => ppUnary(sb, expr, "-", lvl)
case Equals(l,r) => ppBinary(sb, l, r, " == ", lvl)
case IntLiteral(v) => sb.append(v)
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index e6bbcaf74cda077edf521b91e7de37918e4a8105..8d617a834b0eab57a5a4e871d2468335dfccc447 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -54,6 +54,10 @@ object Trees {
if(and == null) None else Some(and.exprs)
}
+ class And(val exprs: Seq[Expr]) extends Expr with FixedType {
+ val fixedType = BooleanType
+ }
+
object Or {
def apply(exprs: Seq[Expr]) : Or = new Or(exprs)
@@ -68,12 +72,22 @@ object Trees {
if(or == null) None else Some(or.exprs)
}
- class And(val exprs: Seq[Expr]) extends Expr
- class Or(val exprs: Seq[Expr]) extends Expr
- case class Not(expr: Expr) extends Expr
+ class Or(val exprs: Seq[Expr]) extends Expr with FixedType {
+ val fixedType = BooleanType
+ }
+
+ case class Implies(left: Expr, right: Expr) extends Expr with FixedType {
+ val fixedType = BooleanType
+ }
+
+ case class Not(expr: Expr) extends Expr with FixedType {
+ val fixedType = BooleanType
+ }
/* Maybe we should split this one depending on types? */
- case class Equals(left: Expr, right: Expr) extends Expr
+ case class Equals(left: Expr, right: Expr) extends Expr with FixedType {
+ val fixedType = BooleanType
+ }
/* Literals */
case class Variable(id: Identifier) extends Expr {
@@ -88,8 +102,12 @@ object Trees {
val value: T
}
- case class IntLiteral(value: Int) extends Literal[Int]
- case class BooleanLiteral(value: Boolean) extends Literal[Boolean]
+ case class IntLiteral(value: Int) extends Literal[Int] with FixedType {
+ val fixedType = Int32Type
+ }
+ case class BooleanLiteral(value: Boolean) extends Literal[Boolean] with FixedType {
+ val fixedType = BooleanType
+ }
case class StringLiteral(value: String) extends Literal[String]
case class CaseClass(classDef: CaseClassDef, args: Seq[Expr]) extends Expr
@@ -142,7 +160,7 @@ object Trees {
case class MapGet(map: Expr, key: Expr) extends Expr
case class MapUnion(map1: Expr, map2: Expr) extends Expr
- case class MapDiffrence(map: Expr, keys: Expr) extends Expr
+ case class MapDifference(map: Expr, keys: Expr) extends Expr
/* List operations */
case class NilList(baseType: TypeTree) extends Expr
@@ -152,24 +170,41 @@ object Trees {
case class Concat(list1: Expr, list2: Expr) extends Expr
case class ListAt(list: Expr, index: Expr) extends Expr
+ object UnaryOperator {
+ def unapply(expr: Expr) : Option[(Expr,(Expr)=>Expr)] = expr match {
+ case IsEmptySet(t) => Some((t,IsEmptySet))
+ case SetCardinality(t) => Some((t,SetCardinality))
+ case Car(t) => Some((t,Car))
+ case Cdr(t) => Some((t,Cdr))
+ case _ => None
+ }
+ }
+
object BinaryOperator {
def unapply(expr: Expr) : Option[(Expr,Expr,(Expr,Expr)=>Expr)] = expr match {
- case Equals(t1,t2) => Some((t1,t2,Equals))
- case Plus(t1,t2) => Some((t1,t2,Plus))
- case Minus(t1,t2) => Some((t1,t2,Minus))
- case Times(t1,t2) => Some((t1,t2,Times))
- case Division(t1,t2) => Some((t1,t2,Division))
- case LessThan(t1,t2) => Some((t1,t2,LessThan))
- case GreaterThan(t1,t2) => Some((t1,t2,GreaterThan))
- case LessEquals(t1,t2) => Some((t1,t2,LessEquals))
- case GreaterEquals(t1,t2) => Some((t1,t2,GreaterEquals))
- case ElementOfSet(t1,t2) => Some((t1,t2,ElementOfSet))
- case SetEquals(t1,t2) => Some((t1,t2,SetEquals))
- case SubsetOf(t1,t2) => Some((t1,t2,SubsetOf))
- case SetIntersection(t1,t2) => Some((t1,t2,SetIntersection))
- case SetUnion(t1,t2) => Some((t1,t2,SetUnion))
- case SetDifference(t1,t2) => Some((t1,t2,SetDifference))
- case _ => None
+ case Equals(t1,t2) => Some((t1,t2,Equals))
+ case Implies(t1,t2) => Some((t1,t2,Implies))
+ case Plus(t1,t2) => Some((t1,t2,Plus))
+ case Minus(t1,t2) => Some((t1,t2,Minus))
+ case Times(t1,t2) => Some((t1,t2,Times))
+ case Division(t1,t2) => Some((t1,t2,Division))
+ case LessThan(t1,t2) => Some((t1,t2,LessThan))
+ case GreaterThan(t1,t2) => Some((t1,t2,GreaterThan))
+ case LessEquals(t1,t2) => Some((t1,t2,LessEquals))
+ case GreaterEquals(t1,t2) => Some((t1,t2,GreaterEquals))
+ case ElementOfSet(t1,t2) => Some((t1,t2,ElementOfSet))
+ case SetEquals(t1,t2) => Some((t1,t2,SetEquals))
+ case SubsetOf(t1,t2) => Some((t1,t2,SubsetOf))
+ case SetIntersection(t1,t2) => Some((t1,t2,SetIntersection))
+ case SetUnion(t1,t2) => Some((t1,t2,SetUnion))
+ case SetDifference(t1,t2) => Some((t1,t2,SetDifference))
+ case SingletonMap(t1,t2) => Some((t1,t2,SingletonMap))
+ case MapGet(t1,t2) => Some((t1,t2,MapGet))
+ case MapUnion(t1,t2) => Some((t1,t2,MapUnion))
+ case MapDifference(t1,t2) => Some((t1,t2,MapDifference))
+ case Concat(t1,t2) => Some((t1,t2,Concat))
+ case ListAt(t1,t2) => Some((t1,t2,ListAt))
+ case _ => None
}
}
}
diff --git a/src/purescala/TypeTrees.scala b/src/purescala/TypeTrees.scala
index 1e7c115bdec57567f6a0c0f9ff660216b4e363f3..caadcd2f8b30d08c48bd774252a84ca5865e4cfa 100644
--- a/src/purescala/TypeTrees.scala
+++ b/src/purescala/TypeTrees.scala
@@ -8,7 +8,7 @@ object TypeTrees {
trait Typed {
self =>
- var _type: Option[TypeTree] = None
+ private var _type: Option[TypeTree] = None
def getType: TypeTree = _type match {
case None => NoType
@@ -21,6 +21,15 @@ object TypeTrees {
}
}
+ trait FixedType extends Typed {
+ self =>
+
+ val fixedType: TypeTree
+ override def getType: TypeTree = fixedType
+ override def setType(tt2: TypeTree) : self.type = this
+ }
+
+
sealed abstract class TypeTree {
override def toString: String = PrettyPrinter(this)
}
diff --git a/testcases/IntOperations.scala b/testcases/IntOperations.scala
index 03256597c78dc64b191e21b30c4f80d48e36557e..0c79ac4cc66d38ac35a5aacba1d00e68f5dec1cc 100644
--- a/testcases/IntOperations.scala
+++ b/testcases/IntOperations.scala
@@ -1,6 +1,6 @@
object IntOperations {
def sum(a: Int, b: Int) : Int = {
- a + (if(b < 0) -b else b)
+ require(b >= 0)
+ a + b
} ensuring(_ >= a)
-
}