diff --git a/build.sbt b/build.sbt index 4d07bbf..4f25781 100644 --- a/build.sbt +++ b/build.sbt @@ -56,6 +56,10 @@ lazy val root = (project in file(".")). scalaCheck % Test ), + // scala-smtlib comes from the "sonatype releases" repository + resolvers += sonatypeResolver, + libraryDependencies += scalaSMTLIB, + // Soot dependency using Paderborn Nexus resolvers ++= sootResolvers, libraryDependencies += soot, diff --git a/project/Dependencies.scala b/project/Dependencies.scala index 3b00053..877cc89 100644 --- a/project/Dependencies.scala +++ b/project/Dependencies.scala @@ -6,6 +6,11 @@ object Dependencies { lazy val scalaCheck = "org.scalacheck" %% "scalacheck" % "1.13.4" lazy val scalaParserCombinators = "org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.5" + + lazy val javaSMT = "org.sosy-lab" % "java-smt" % "1.0.1" + + lazy val sonatypeResolver = "Sonatype OSS Releases" at "https://oss.sonatype.org/content/repositories/releases" + lazy val scalaSMTLIB = "com.regblanc" %% "scala-smtlib" % "0.2.1" lazy val sootResolvers = Seq( "soot snapshot" at "https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/", diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/Abstraction.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/Abstraction.scala deleted file mode 100644 index 5b5ef01..0000000 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/Abstraction.scala +++ /dev/null @@ -1,18 +0,0 @@ -package edu.colorado.plv.cuanto.abstracting - -/** Signature for a generic abstraction. - * - * An abstraction is a join semi-lattice. - * - * @author Bor-Yuh Evan Chang - */ -trait Abstraction { - /** The abstract element type. */ - type A - - val bottom: A - def isBottom(e: A): Boolean - - def implies(e1: A, e2: A): Boolean - def join(e1: A, e2: A): A -} diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/bitvectors/B3.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/bitvectors/B3.scala new file mode 100644 index 0000000..a5f75e7 --- /dev/null +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/bitvectors/B3.scala @@ -0,0 +1,220 @@ +package edu.colorado.plv.cuanto.abstracting + +/** + * @author Nicholas Lewchenko + */ +package bitvectors + +import scala.collection.immutable.{Map => IMap} + +import smtlib._ +import interpreters.Z3Interpreter +import theories.Core._ +import theories.Constructors._ +import parser.Terms._ +import parser.Commands._ +import parser.CommandsResponses._ + +import symbolic._ + +/** The concrete form, a tuple of three booleans */ +case class B3(bool1: Boolean, bool2: Boolean, bool3: Boolean) + +object B3 { + val postHatUpInst = + (t: (SMT3,SMT3) => Term, v: Vote3) => postHatUp( + SMT3.model _, + Vote3.represent _, + SMT3.gammaHat _, + t, + not, + v + ) + + /** The symbolic form, capable of fully representing a B3 as an SMT + * script */ + case class SMT3(bool1: Term, bool2: Term, bool3: Term) + + object SMT3 { + + def model( + s1: (SMT3 => Term), + t: ((SMT3,SMT3) => Term), + s2: (SMT3 => Term) + ): Option[(B3,B3)] = { + val a1 = SSymbol("a1") + val b1 = SSymbol("b1") + val c1 = SSymbol("c1") + val a2 = SSymbol("a2") + val b2 = SSymbol("b2") + val c2 = SSymbol("c2") + + val mkTerm = (s: SSymbol) => QualifiedIdentifier(SimpleIdentifier(s)) + val mkSMT3 = (a: SSymbol,b: SSymbol,c: SSymbol) => + SMT3(mkTerm(a),mkTerm(b),mkTerm(c)) + + val z3 = Z3Interpreter.buildDefault + + val smt1 = mkSMT3(a1,b1,c1) + val smt2 = mkSMT3(a2,b2,c2) + + Seq( + DeclareConst(a1,BoolSort()), + DeclareConst(b1,BoolSort()), + DeclareConst(c1,BoolSort()), + DeclareConst(a2,BoolSort()), + DeclareConst(b2,BoolSort()), + DeclareConst(c2,BoolSort()), + + Assert( + and( + s1(smt1), + s2(smt2), + t(smt1,smt2) + ) + ), + + CheckSat() + ).map(z3.eval) + + z3.eval(GetModel()) match { + case GetModelResponseSuccess(m) => + val res = comprehend(m) + for { + boolA1 <- res get a1 + boolB1 <- res get b1 + boolC1 <- res get c1 + boolA2 <- res get a2 + boolB2 <- res get b2 + boolC2 <- res get c2 + } yield (( + B3(boolA1,boolB1,boolC1), + B3(boolA2,boolB2,boolC2) + )) + case _ => None + } + } + + def comprehend(m: List[SExpr]): IMap[SSymbol,Boolean] = { + val p: (IMap[SSymbol,Boolean],SExpr) => IMap[SSymbol,Boolean] = { + (acc,i) => i match { + case DefineFun(FunDef(id,_,_,v)) => v match { + case True() => acc + (id -> true) + case Not(True()) => acc + (id -> false) + case False() => acc + (id -> false) + case _ => acc + } + case _ => acc + } + } + m.foldLeft[IMap[SSymbol,Boolean]](IMap.empty)(p) + } + + def gammaHat(v: Vote3): SMT3 => Term = { (smt: SMT3) => + def yayFormula(smt: SMT3): Term = smt match { + case SMT3(a,b,c) => Or(and(a,b), Or(and(b,c), and(c,a))) + } + v match { + case Top => True() + case Yay => yayFormula(smt) + case Nay => not(yayFormula(smt)) + case Bot => False() + } + } + + + implicit def represent(b: Boolean): Term => Term = { (t: Term) => + b match { + case true => t + case false => not(t) + } + } + + implicit def represent(b3: B3): SMT3 => Term = { (smt: SMT3) => + and( + b3.bool1(smt.bool1), + b3.bool2(smt.bool2), + b3.bool3(smt.bool3) + ) + } + + /** A single vote changes from Nay to Yay (note that this will fail if + * all votes in the precondition are already Yay; this could maybe + * be defined to also pass in that case?) */ + def voteYay(pre: SMT3, post: SMT3): Term = (pre,post) match { + case (SMT3(a,b,c),SMT3(an,bn,cn)) => + Or( + and(not(a),an,Equals(b,bn),Equals(c,cn)), + and(Equals(a,an),not(b),bn,Equals(c,cn)), + and(Equals(a,an),Equals(b,bn),not(c),cn) + ) + } + + /** Opposite of voteYay */ + def voteNay(pre: SMT3, post: SMT3): Term = (pre,post) match { + case (SMT3(a,b,c),SMT3(an,bn,cn)) => + Or( + and(a,not(an),Equals(b,bn),Equals(c,cn)), + and(Equals(a,an),b,not(bn),Equals(c,cn)), + and(Equals(a,an),Equals(b,bn),c,not(cn)) + ) + } + + } + + /** The abstract form, which loses precision */ + sealed abstract class Vote3 + case object Top extends Vote3 + case object Yay extends Vote3 + case object Nay extends Vote3 + case object Bot extends Vote3 + + object Vote3 { + implicit val abstractVote3: Abstraction[Vote3] = new Abstraction[Vote3] { + + val bottom: Vote3 = Bot + def isBottom(e: Vote3): Boolean = e == bottom + def implies(e1: Vote3, e2: Vote3): Boolean = (e1,e2) match { + case (Bot,_) => true + case (_,Top) => true + case _ => false + } + def join(e1: Vote3, e2: Vote3): Vote3 = (e1, e2) match { + case _ if e1 == e2 => e1 + case (Bot, _) => e2 + case (_, Bot) => e1 + case _ => Top + } + + } + + // def represent(b3: B3): Vote3 = b3 match { + // case B3(a,b,c) => Seq(a,b,c).filter((b: Boolean) => b).size match { + // case s if s >= 2 => Yay + // case _ => Nay + // } + // } + + def represent(b3: B3): Vote3 = b3 match { + case B3(true,true,true) => Yay + case B3(true,true,_ ) => Yay + case B3(_ ,true,true) => Yay + case B3(true,_ ,true) => Yay + case _ => Nay + } + + def voteYay(vs: Vote3): Vote3 = vs match { + case Yay => Yay + case Nay => Top + case v => v + } + + def voteNay(vs: Vote3): Vote3 = vs match { + case Nay => Nay + case Yay => Top + case v => v + } + + } + +} diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/package.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/package.scala index 698cb2c..9296417 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/package.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/package.scala @@ -2,6 +2,7 @@ package edu.colorado.plv.cuanto /** * @author Bor-Yuh Evan Chang + * @author Nicholas Lewchenko */ package abstracting { @@ -22,5 +23,18 @@ package abstracting { @inline final implicit def beta(c: C): A = represent(c) } + trait Abstraction[A] { + val bottom: A + def isBottom(e: A): Boolean + def implies(e1: A, e2: A): Boolean + def join(e1: A, e2: A): A + } + + object Abstraction { + def apply[A : Abstraction]: Abstraction[A] = + implicitly[Abstraction[A]] + } + + } diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/symbolic/package.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/symbolic/package.scala new file mode 100644 index 0000000..df0a22c --- /dev/null +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/symbolic/package.scala @@ -0,0 +1,33 @@ +package edu.colorado.plv.cuanto.abstracting + +/** + * @author Nicholas Lewchenko + */ +package symbolic { + +} + +package object symbolic { + + def postHatUp[C,A : Abstraction,L,T]( + model: ((L => T),((L,L) => T),(L => T)) => Option[(C,C)], + beta: C => A, + gammaHat: A => (L => T), + t: (L,L) => T, + neg: T => T, + v: A + ): A = { + val notGammaHat = (e: A) => (l: L) => neg(gammaHat(e)(l)) + def recur(low: A): A = + model(gammaHat(v),t,notGammaHat(low)) match { + case Some((s,sn)) => { + recur(Abstraction[A].join(low,beta(sn))) + } + case _ => { + low + } + } + recur(Abstraction[A].bottom) + } + +} diff --git a/src/test/scala/edu/colorado/plv/cuanto/abstracting/symbolic/SymbolicAbstractionSpec.scala b/src/test/scala/edu/colorado/plv/cuanto/abstracting/symbolic/SymbolicAbstractionSpec.scala new file mode 100644 index 0000000..739938c --- /dev/null +++ b/src/test/scala/edu/colorado/plv/cuanto/abstracting/symbolic/SymbolicAbstractionSpec.scala @@ -0,0 +1,26 @@ +package edu.colorado.plv.cuanto + +/** + * @author Nicholas Lewchenko + */ +package abstracting.symbolic + +import abstracting.bitvectors.B3._ + +class SymbolicAbstractionSpec extends CuantoSpec { + + val avals = Seq(Top,Yay,Nay,Bot) + + "The postHat funtion" should "correctly model voteYay" in { + avals.map({ + v => postHatUpInst(SMT3.voteYay,v) should equal (Vote3.voteYay(v)) + }) + } + + "The postHat funtion" should "correctly model voteNay" in { + avals.map({ + v => postHatUpInst(SMT3.voteNay,v) should equal (Vote3.voteNay(v)) + }) + } + +} diff --git a/src/test/scala/edu/colorado/plv/cuanto/example/ScalaSmtlibExamples.scala b/src/test/scala/edu/colorado/plv/cuanto/example/ScalaSmtlibExamples.scala new file mode 100644 index 0000000..597b03d --- /dev/null +++ b/src/test/scala/edu/colorado/plv/cuanto/example/ScalaSmtlibExamples.scala @@ -0,0 +1,136 @@ +package edu.colorado.plv.cuanto + +/** + * @author Nicholas Lewchenko + */ +package example + +import org.scalatest.tagobjects.Slow + +import smtlib.{ + Interpreter +} +import smtlib.interpreters.{ + Z3Interpreter +} +import smtlib.parser.Terms.{ + SSymbol, + Term, + QualifiedIdentifier, + SimpleIdentifier +} +import smtlib.parser.Commands.{ + Command, + DeclareConst, + Assert, + CheckSat, + GetModel, + DefineFun, + FunDef, + Push, + Pop +} +import smtlib.parser.CommandsResponses.{ + Success, + CheckSatStatus, + SatStatus, + UnsatStatus, + GetModelResponseSuccess, + Error +} +import smtlib.theories.Core.{ + True, + False, + Or +} +import smtlib.theories.Ints.{ + IntSort, + NumeralLit, + GreaterEquals, + GreaterThan, + LessThan, + Neg +} +import smtlib.theories.Constructors.{ + and, + not => notTerm +} + +/** + * Usage examples based on the scala-smtlib integration tests + * + * [[https://github.com/regb/scala-smtlib/blob/v0.2.1/src/it/scala/smtlib/it/SmtLibRunnerTests.scala]] + * + * @author Nicholas Lewchenko + */ +class ScalaSmtlibExample extends CuantoSpec { + + "Evaluating SMT scripts" should "go like this" taggedAs(Slow) in { + forAll (testCmds) { (cmd,res) => z3.eval(cmd) should equal (res) } + } + + lazy val z3: Interpreter = Z3Interpreter.buildDefault + + val zero: Term = NumeralLit(0) + val one: Term = NumeralLit(1) + val three: Term = NumeralLit(3) + + val mkVar: SSymbol => Term = name => + QualifiedIdentifier(SimpleIdentifier(name)) + + val xs: SSymbol = SSymbol("x") + val ys: SSymbol = SSymbol("y") + val x: Term = mkVar(xs) + val y: Term = mkVar(ys) + + val goodExpr: Term = + and( + GreaterEquals(x,zero), + notTerm(GreaterThan(x,three)), + LessThan(y,x) + ) + + /** Models are returned as sequences of "define-fun" commands */ + val goodModel: List[Command] = List( + DefineFun(FunDef(ys, List.empty, IntSort(), Neg(one))), + DefineFun(FunDef(xs, List.empty, IntSort(), zero)) + ) + + val badExpr: Term = + and( + GreaterEquals(x,three), + LessThan(x,zero) + ) + + /** This is an example SMT script (as a sequence of commands, which + * are given to the interpreter one by one) + * + * On the left is the command, and on the right is the response + * that is received. + */ + val testCmds = Table( + "command" -> "response", + + Push(0) -> Success, + Assert(Or(True(),False())) -> Success, + CheckSat() -> CheckSatStatus(SatStatus), + Pop(0) -> Success, + + DeclareConst(xs,IntSort()) -> Success, + DeclareConst(ys,IntSort()) -> Success, + + Push(0) -> Success, + Assert(goodExpr) -> Success, + CheckSat() -> CheckSatStatus(SatStatus), + GetModel() -> GetModelResponseSuccess(goodModel), + Pop(0) -> Success, + + Push(0) -> Success, + Assert(badExpr) -> Success, + CheckSat() -> CheckSatStatus(UnsatStatus), + GetModel() -> Error("line 31 column 10: model is not available"), + Pop(0) -> Success + + ) + +}