diff --git a/build.xml b/build.xml
index 36a4dbc404c1892df434c4ec60151e729dcd8d8e..9d8f971443070bf2469c6faf788309d8eec99da3 100644
--- a/build.xml
+++ b/build.xml
@@ -60,8 +60,9 @@
<path id="build.path">
<path refid="scalac.class.path"/>
- <path refid="funcheck.lib.path"/>
- <pathelement location="${build.plugin.funcheck.dir}" />
+ <!-- <path refid="funcheck.lib.path"/> -->
+ <pathelement location="${lib.dir}/z3.jar"/>
+ <!-- <pathelement location="${build.plugin.funcheck.dir}" /> -->
</path>
<!--
@@ -105,7 +106,7 @@
<mkdir dir="${build.plugin.funcheck.dir}" />
<scalac srcdir="${sources.dir}" destdir="${build.plugin.funcheck.dir}" force="changed" addparams="${scalac.default.params}">
<classpath>
- <path refid="scalac.class.path" />
+ <path refid="build.path" />
</classpath>
<exclude name="scala/collection/**/*"/>
<exclude name="funcheck/lib/**/*"/>
@@ -127,7 +128,7 @@
<fileset file="./scalac-plugin.xml" />
</jar>
- <echo file="${script.file}" message="#!/bin/sh${line.separator}scalac -Xplugin:${dist.jar} $@${line.separator}" />
+ <echo file="${script.file}" message="#!/bin/sh${line.separator}scalac -cp ./lib/z3.jar -Xplugin:${dist.jar} $@${line.separator}" />
<chmod file="${script.file}" perm="u+x" />
</target>
diff --git a/lib/z3.jar b/lib/z3.jar
new file mode 100644
index 0000000000000000000000000000000000000000..2fd797b68a3ae3d5a17bad12f77b857b7e2b4ef3
Binary files /dev/null and b/lib/z3.jar differ
diff --git a/s-f b/s-f
new file mode 100755
index 0000000000000000000000000000000000000000..0e04980aa1736203249654a48f26a1ca5dd54a08
--- /dev/null
+++ b/s-f
@@ -0,0 +1,6 @@
+#!/bin/sh
+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 $@
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index e889f1f3f97ef736a8cbfdfb3861b5ae5691c689..f01145dae44bf5317dfdb24210130dd78f7a387e 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -1,7 +1,10 @@
package purescala
+import Common._
import Definitions._
import Trees._
+import TypeTrees._
+import z3.scala._
object Analysis {
// Analysis should check that:
@@ -13,12 +16,19 @@ object Analysis {
// - injective functions are injective
// - all global invariants are satisfied
def analyze(program: Program) : Unit = {
+ val z3cfg = new Z3Config()
+ //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(vc)
+ val (z3f,stupidMap) = toZ3Formula(z3, vc)
+ z3.assertCnstr(z3.mkNot(z3f))
+ println("Valid? " + z3.check())
}
})
}
@@ -30,7 +40,7 @@ object Analysis {
if(post.isEmpty) {
BooleanLiteral(true)
} else {
- BooleanLiteral(false)
+ replaceInExpr(Map(ResultVariable() -> functionDefinition.body), post.get)
}
}
@@ -41,6 +51,60 @@ object Analysis {
case _ => throw new Exception("ah ha !")
}
+ (expr, Nil)
+ }
+
+ def replaceInExpr(substs: Map[Expr,Expr], expr: Expr) : Expr = {
+ def rec(ex: Expr) : Expr = ex match {
+ case _ if (substs.get(ex).isDefined) => substs(ex)
+ case FunctionInvocation(fd, args) => FunctionInvocation(fd, args.map(rec(_)))
+ case IfExpr(t1,t2,t3) => IfExpr(rec(t1),rec(t2),rec(t3))
+ case MatchExpr(_,_) => ex
+ 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 _ => ex
+ }
+
+ rec(expr)
}
+ def toZ3Formula(z3: Z3Context, expr: Expr) : (Z3AST,Map[Identifier,Z3AST]) = {
+ val intSort = z3.mkIntSort()
+ var varMap: Map[Identifier,Z3AST] = Map.empty
+
+ def rec(ex: Expr) : Z3AST = ex match {
+ case v @ Variable(id) => varMap.get(id) match {
+ case Some(ast) => ast
+ case None => {
+ assert(v.getType == Int32Type)
+ val newAST = z3.mkConst(z3.mkStringSymbol(id.name), intSort)
+ varMap = varMap + (id -> newAST)
+ newAST
+ }
+ }
+ case IfExpr(c,t,e) => z3.mkITE(rec(c), rec(t), rec(e))
+ case And(exs) => z3.mkAnd(exs.map(rec(_)) : _*)
+ 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 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))
+ case Plus(l,r) => z3.mkAdd(rec(l), rec(r))
+ case Minus(l,r) => z3.mkSub(rec(l), rec(r))
+ case Times(l,r) => z3.mkMul(rec(l), rec(r))
+ case Division(l,r) => z3.mkDiv(rec(l), rec(r))
+ case UMinus(e) => z3.mkUnaryMinus(rec(e))
+ case LessThan(l,r) => z3.mkLT(rec(l), rec(r))
+ case LessEquals(l,r) => z3.mkLE(rec(l), rec(r))
+ case GreaterThan(l,r) => z3.mkGT(rec(l), rec(r))
+ case GreaterEquals(l,r) => z3.mkGE(rec(l), rec(r))
+ case _ => scala.Predef.error("Can't handle this in translation to Z3: " + ex)
+ }
+
+ val res = rec(expr)
+ (res,varMap)
+ }
}
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index 17883d57b8e43da5c970f61f148ec2eb51440ec3..e6bbcaf74cda077edf521b91e7de37918e4a8105 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -40,26 +40,36 @@ object Trees {
// We don't handle Seq stars for now.
/* Propositional logic */
- case object And {
+ object And {
+ def apply(exprs: Seq[Expr]) : And = new And(exprs)
+
def apply(l: Expr, r: Expr): Expr = (l,r) match {
case (And(exs1), And(exs2)) => And(exs1 ++ exs2)
case (And(exs1), ex2) => And(exs1 :+ ex2)
case (ex1, And(exs2)) => And(exs2 :+ ex1)
case (ex1, ex2) => And(List(ex1, ex2))
}
+
+ def unapply(and: And) : Option[Seq[Expr]] =
+ if(and == null) None else Some(and.exprs)
}
- case object Or {
+ object Or {
+ def apply(exprs: Seq[Expr]) : Or = new Or(exprs)
+
def apply(l: Expr, r: Expr): Expr = (l,r) match {
case (Or(exs1), Or(exs2)) => Or(exs1 ++ exs2)
case (Or(exs1), ex2) => Or(exs1 :+ ex2)
case (ex1, Or(exs2)) => Or(exs2 :+ ex1)
case (ex1, ex2) => Or(List(ex1, ex2))
}
+
+ def unapply(or: Or) : Option[Seq[Expr]] =
+ if(or == null) None else Some(or.exprs)
}
- case class And(exprs: Seq[Expr]) extends Expr
- case class Or(exprs: Seq[Expr]) extends Expr
+ class And(val exprs: Seq[Expr]) extends Expr
+ class Or(val exprs: Seq[Expr]) extends Expr
case class Not(expr: Expr) extends Expr
/* Maybe we should split this one depending on types? */
@@ -141,4 +151,25 @@ object Trees {
case class Cdr(list: Expr) extends Expr
case class Concat(list1: Expr, list2: Expr) extends Expr
case class ListAt(list: Expr, index: Expr) extends Expr
+
+ 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
+ }
+ }
}
diff --git a/testcases/IntOperations.scala b/testcases/IntOperations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..03256597c78dc64b191e21b30c4f80d48e36557e
--- /dev/null
+++ b/testcases/IntOperations.scala
@@ -0,0 +1,6 @@
+object IntOperations {
+ def sum(a: Int, b: Int) : Int = {
+ a + (if(b < 0) -b else b)
+ } ensuring(_ >= a)
+
+}