From e5f29640ce88766ba8c24279e1cb0000064b5645 Mon Sep 17 00:00:00 2001 From: octalsrc Date: Fri, 28 Jul 2017 11:37:06 -0600 Subject: [PATCH 1/8] Begin symbolic abstraction again --- .../abstracting/tc/domains/Interval.scala | 18 +++++++ .../abstracting/tc/symbolic/package.scala | 50 +++++++++++++++++++ 2 files changed, 68 insertions(+) create mode 100644 src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala index 01e1382..9ebee12 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala @@ -2,6 +2,12 @@ package edu.colorado.plv.cuanto package abstracting.tc package domains +import smtlib.parser.Commands._ +import smtlib.parser.Terms._ +import smtlib.theories.Ints._ + +import symbolic._ + /** A domain representing an integer constrained by an upper and/or * lower bound * @@ -45,7 +51,19 @@ package object interval { reduce(Btw(g,l)) } + case class IntSMT(int1: Term) + object instances { + implicit val intSMTSymbol: Symbol[IntSMT] = new Symbol[IntSMT] { + override def draw(name: String): (IntSMT,Traversable[Command]) = { + val s: SSymbol = SSymbol(name) + val q: QualifiedIdentifier = QualifiedIdentifier(SimpleIdentifier(s)) + + (IntSMT(q),Seq(DeclareConst(s,IntSort()))) + } + override val idConstraint: Constraint[IntSMT] = ??? + } + implicit val latticeInterval: Lattice[Interval] = new Lattice[I] { val bot: Interval = Bot val top: Interval = Top diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala new file mode 100644 index 0000000..394722e --- /dev/null +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala @@ -0,0 +1,50 @@ +package edu.colorado.plv.cuanto +package abstracting.tc + +import smtlib.parser.Commands.Command +import smtlib.parser.Terms.Term +import smtlib.theories.Core.Not + +import Semilattice._ +import Abstraction._ + +package object symbolic { + + type Constraint[S] = S => Term + type Transformer[S] = (S,S) => Term + + trait Symbol[S] { + def draw(s: String): (S,Traversable[Command]) + val idConstraint: Constraint[S] + } + + trait Model[C] { + type Schema + def model(s: Constraint[Schema]): Option[C] + } + + trait SymAbstract[A,S] { + def gammaHat(a: A): Constraint[S] + } + + def modelT[C,S]( + t: Transformer[S] + )( + pre: Constraint[S], + post: Constraint[S] + )( + implicit iM: Model[C] {type Schema = S} + ): Option[(C,C)] = ??? + + def postHatUp[C,A : Semilattice,S : Symbol](t: Transformer[S])(v: A)( + implicit iM: Model[C] {type Schema = S}, iS: SymAbstract[A,S], iA: Abstraction[C,A] + ): A = { + val notGammaHat = (e: A) => (l: S) => Not(iS.gammaHat(e)(l)) + def recur(low: A): A = + modelT(t)(iS.gammaHat(v),notGammaHat(low)) match { + case Some((s1,s2)) => recur(join(low,beta(s2))) + case None => low + } + recur(bot[A]) + } +} From 7403bfc838bdf6ba41dbfe4d7784e650bcb8ae1d Mon Sep 17 00:00:00 2001 From: octalsrc Date: Wed, 16 Aug 2017 13:15:47 -0600 Subject: [PATCH 2/8] Implement smt modeling abstractions for Ints --- .../abstracting/tc/domains/Interval.scala | 35 ++++++++++++++- .../abstracting/tc/symbolic/package.scala | 38 ++++++++++++++-- .../tc/domains/SymbolicIntervalSpec.scala | 44 +++++++++++++++++++ 3 files changed, 112 insertions(+), 5 deletions(-) create mode 100644 src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala index 9ebee12..177204a 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala @@ -2,7 +2,9 @@ package edu.colorado.plv.cuanto package abstracting.tc package domains +import smtlib.interpreters.Z3Interpreter import smtlib.parser.Commands._ +import smtlib.parser.CommandsResponses._ import smtlib.parser.Terms._ import smtlib.theories.Ints._ @@ -61,8 +63,39 @@ package object interval { (IntSMT(q),Seq(DeclareConst(s,IntSort()))) } - override val idConstraint: Constraint[IntSMT] = ??? } + + implicit val intSMTVal: SMTVal[Int] = new SMTVal[Int] { + override def interpret(value: Term): Option[Int] = value match { + case NumeralLit(v) => Some(v.intValue()) + case _ => None + } + } + + implicit val intModel: Model[Int] {type Schema = IntSMT} = new Model[Int] { + override type Schema = IntSMT + override def model(name: String, s: Constraint[IntSMT]): Option[Int] = { + val (schemaVal,decl) = Symbol[IntSMT].draw(name) + val z3 = Z3Interpreter.buildDefault + val assertion = Seq(Assert(s(schemaVal))) + + (decl ++ assertion ++ Seq(CheckSat())).map(z3.eval) + + z3.eval(GetModel()) match { + case GetModelResponseSuccess(m) => + val res = comprehend(m) + for { + i <- res get SSymbol(name) + } yield i + case _ => None + } + } + } + + implicit val intervalSym: SymAbstract[Interval,IntSMT] = + new SymAbstract[Interval,IntSMT] { + override def gammaHat(a: Interval): Constraint[IntSMT] = ??? + } implicit val latticeInterval: Lattice[Interval] = new Lattice[I] { val bot: Interval = Bot diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala index 394722e..248b5a8 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala @@ -1,8 +1,8 @@ package edu.colorado.plv.cuanto package abstracting.tc -import smtlib.parser.Commands.Command -import smtlib.parser.Terms.Term +import smtlib.parser.Commands.{Command,DefineFun,FunDef} +import smtlib.parser.Terms.{SExpr,SSymbol,Term} import smtlib.theories.Core.Not import Semilattice._ @@ -15,17 +15,33 @@ package object symbolic { trait Symbol[S] { def draw(s: String): (S,Traversable[Command]) - val idConstraint: Constraint[S] + } + object Symbol { + def apply[A : Symbol]: Symbol[A] = implicitly[Symbol[A]] + } + + trait SMTVal[V] { + def interpret(value: Term): Option[V] + } + object SMTVal { + def apply[A : SMTVal]: SMTVal[A] = implicitly[SMTVal[A]] } trait Model[C] { type Schema - def model(s: Constraint[Schema]): Option[C] + def model(name: String, s: Constraint[Schema]): Option[C] + } + object Model { + def apply[A : Model]: Model[A] = implicitly[Model[A]] } trait SymAbstract[A,S] { def gammaHat(a: A): Constraint[S] } + object SymAbstract { + def apply[A,S](implicit inst: SymAbstract[A,S]): SymAbstract[A,S] = + implicitly[SymAbstract[A,S]] + } def modelT[C,S]( t: Transformer[S] @@ -47,4 +63,18 @@ package object symbolic { } recur(bot[A]) } + + def comprehend[V : SMTVal](m: List[SExpr]): Map[SSymbol,V] = { + val p: (Map[SSymbol,V],SExpr) => Map[SSymbol,V] = { + (acc,i) => i match { + case DefineFun(FunDef(id,_,_,v)) => SMTVal[V].interpret(v) match { + case Some(v) => acc + (id -> v) + case None => acc + } + case _ => acc + } + } + m.foldLeft[Map[SSymbol,V]](Map.empty)(p) + } + } diff --git a/src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala b/src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala new file mode 100644 index 0000000..17df260 --- /dev/null +++ b/src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala @@ -0,0 +1,44 @@ +package edu.colorado.plv.cuanto +package abstracting.tc +package domains.interval + +import smtlib.theories.Core._ +import smtlib.theories.Ints._ + +import symbolic._ + +import instances._ + +/** + * @author Nicholas V. Lewchenko + */ +class SymbolicIntervalSpec extends CuantoSpec { + + val gteSpec: Int => Constraint[IntSMT] = + i => { case IntSMT(t) => GreaterThan(t,NumeralLit(BigInt(i))) } + + val btwSpec: (Int,Int) => Constraint[IntSMT] = { + case (g,l) => { + case IntSMT(t) => And( + GreaterThan(t,NumeralLit(BigInt(g))), + LessThan(t,NumeralLit(BigInt(l))) + ) + } + } + + val modelTests = Table[Constraint[IntSMT],Int => Boolean]( + "SMT constraint" -> "Int predicate", + gteSpec(4) -> { i => i > 4 }, + btwSpec(1,9) -> { i => i > 1 && i < 9 } + ) + + val modelInst: Model[Int] {type Schema = IntSMT} = intModel + + "The Int symbolic representation" should "produce models" in { + forAll (modelTests) { + (smt,p) => modelInst.model("asdf",smt).map(p) should equal (Some(true)) + } + + modelInst.model("asdf",btwSpec(2,1)) should equal (None) + } +} From a5cec78431f3c2bb967b3659690a86da20c33912 Mon Sep 17 00:00:00 2001 From: octalsrc Date: Fri, 18 Aug 2017 10:24:54 -0600 Subject: [PATCH 3/8] partial work --- .../plv/cuanto/abstracting/tc/domains/Interval.scala | 8 ++++++++ .../plv/cuanto/abstracting/tc/symbolic/package.scala | 10 +++++++++- 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala index 177204a..dd39959 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala @@ -2,6 +2,7 @@ package edu.colorado.plv.cuanto package abstracting.tc package domains +import smtlib.Interpreter import smtlib.interpreters.Z3Interpreter import smtlib.parser.Commands._ import smtlib.parser.CommandsResponses._ @@ -90,6 +91,13 @@ package object interval { case _ => None } } + override def getModel(name: String, i: Interpreter): Option[Int] = { + (for { + intResults <- getModelMap(i) + } yield for { + i <- intResults get SSymbol(name) + } yield i).flatten + } } implicit val intervalSym: SymAbstract[Interval,IntSMT] = diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala index 248b5a8..1c63ddb 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala @@ -1,7 +1,9 @@ package edu.colorado.plv.cuanto package abstracting.tc -import smtlib.parser.Commands.{Command,DefineFun,FunDef} +import smtlib.Interpreter +import smtlib.parser.Commands.{Command,DefineFun,FunDef,GetModel} +import smtlib.parser.CommandsResponses.GetModelResponseSuccess import smtlib.parser.Terms.{SExpr,SSymbol,Term} import smtlib.theories.Core.Not @@ -30,6 +32,7 @@ package object symbolic { trait Model[C] { type Schema def model(name: String, s: Constraint[Schema]): Option[C] + def getModel(name: String, interpreter: Interpreter): Option[C] } object Model { def apply[A : Model]: Model[A] = implicitly[Model[A]] @@ -77,4 +80,9 @@ package object symbolic { m.foldLeft[Map[SSymbol,V]](Map.empty)(p) } + def getModelMap[V : SMTVal](i: Interpreter): Option[Map[SSymbol,V]] = + i.eval(GetModel()) match { + case GetModelResponseSuccess(m) => Some(comprehend(m)) + case _ => None + } } From 7d05669b0713a91e4f84b89834de067a9016e6b0 Mon Sep 17 00:00:00 2001 From: octalsrc Date: Fri, 15 Sep 2017 11:08:04 -0600 Subject: [PATCH 4/8] Got more abstract form of `model` to work --- .../abstracting/tc/domains/Interval.scala | 32 ++++--------------- .../abstracting/tc/symbolic/package.scala | 25 +++++++++++++-- .../tc/domains/SymbolicIntervalSpec.scala | 10 +++--- 3 files changed, 33 insertions(+), 34 deletions(-) diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala index dd39959..0c93526 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala @@ -3,9 +3,7 @@ package abstracting.tc package domains import smtlib.Interpreter -import smtlib.interpreters.Z3Interpreter -import smtlib.parser.Commands._ -import smtlib.parser.CommandsResponses._ +import smtlib.parser.Commands.{Command, DeclareConst} import smtlib.parser.Terms._ import smtlib.theories.Ints._ @@ -54,15 +52,14 @@ package object interval { reduce(Btw(g,l)) } - case class IntSMT(int1: Term) + case class IntSMT(int1: SSymbol) object instances { implicit val intSMTSymbol: Symbol[IntSMT] = new Symbol[IntSMT] { override def draw(name: String): (IntSMT,Traversable[Command]) = { val s: SSymbol = SSymbol(name) - val q: QualifiedIdentifier = QualifiedIdentifier(SimpleIdentifier(s)) - (IntSMT(q),Seq(DeclareConst(s,IntSort()))) + (IntSMT(s),Seq(DeclareConst(s,IntSort()))) } } @@ -75,28 +72,11 @@ package object interval { implicit val intModel: Model[Int] {type Schema = IntSMT} = new Model[Int] { override type Schema = IntSMT - override def model(name: String, s: Constraint[IntSMT]): Option[Int] = { - val (schemaVal,decl) = Symbol[IntSMT].draw(name) - val z3 = Z3Interpreter.buildDefault - val assertion = Seq(Assert(s(schemaVal))) - - (decl ++ assertion ++ Seq(CheckSat())).map(z3.eval) - - z3.eval(GetModel()) match { - case GetModelResponseSuccess(m) => - val res = comprehend(m) - for { - i <- res get SSymbol(name) - } yield i - case _ => None - } - } override def getModel(name: String, i: Interpreter): Option[Int] = { - (for { + for { intResults <- getModelMap(i) - } yield for { - i <- intResults get SSymbol(name) - } yield i).flatten + int <- intResults get SSymbol(name) + } yield int } } diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala index 1c63ddb..6e375ef 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala @@ -2,9 +2,10 @@ package edu.colorado.plv.cuanto package abstracting.tc import smtlib.Interpreter -import smtlib.parser.Commands.{Command,DefineFun,FunDef,GetModel} +import smtlib.interpreters.Z3Interpreter +import smtlib.parser.Commands._ import smtlib.parser.CommandsResponses.GetModelResponseSuccess -import smtlib.parser.Terms.{SExpr,SSymbol,Term} +import smtlib.parser.Terms._ import smtlib.theories.Core.Not import Semilattice._ @@ -22,6 +23,11 @@ package object symbolic { def apply[A : Symbol]: Symbol[A] = implicitly[Symbol[A]] } + /** Create a [[smtlib.parser.terms.Term `Term`]] from a + * [[smtlib.parser.terms.SSymbol `SSymbol`]] */ + val sTerm: SSymbol => QualifiedIdentifier = + s => QualifiedIdentifier(SimpleIdentifier(s)) + trait SMTVal[V] { def interpret(value: Term): Option[V] } @@ -31,13 +37,26 @@ package object symbolic { trait Model[C] { type Schema - def model(name: String, s: Constraint[Schema]): Option[C] def getModel(name: String, interpreter: Interpreter): Option[C] } object Model { def apply[A : Model]: Model[A] = implicitly[Model[A]] } + def model[C,S : Symbol]( + name: String, s: Constraint[S] + )( + implicit iM: Model[C] {type Schema = S} + ): Option[C] = { + val (schemaVal,decl) = Symbol[S].draw(name) + val z3 = Z3Interpreter.buildDefault + val assertion = Seq(Assert(s(schemaVal))) + + (decl ++ assertion ++ Seq(CheckSat())).map(z3.eval) + + Model[C].getModel(name, z3) + } + trait SymAbstract[A,S] { def gammaHat(a: A): Constraint[S] } diff --git a/src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala b/src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala index 17df260..ab0df8f 100644 --- a/src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala +++ b/src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala @@ -15,13 +15,13 @@ import instances._ class SymbolicIntervalSpec extends CuantoSpec { val gteSpec: Int => Constraint[IntSMT] = - i => { case IntSMT(t) => GreaterThan(t,NumeralLit(BigInt(i))) } + i => { case IntSMT(t) => GreaterThan(sTerm(t),NumeralLit(BigInt(i))) } val btwSpec: (Int,Int) => Constraint[IntSMT] = { case (g,l) => { case IntSMT(t) => And( - GreaterThan(t,NumeralLit(BigInt(g))), - LessThan(t,NumeralLit(BigInt(l))) + GreaterThan(sTerm(t),NumeralLit(BigInt(g))), + LessThan(sTerm(t),NumeralLit(BigInt(l))) ) } } @@ -36,9 +36,9 @@ class SymbolicIntervalSpec extends CuantoSpec { "The Int symbolic representation" should "produce models" in { forAll (modelTests) { - (smt,p) => modelInst.model("asdf",smt).map(p) should equal (Some(true)) + (smt,p) => model("asdf",smt).map(p) should equal (Some(true)) } - modelInst.model("asdf",btwSpec(2,1)) should equal (None) + model("asdf",btwSpec(2,1)) should equal (None) } } From efd0d505ec484a7e91265b9d3c1398ddbc48cf2e Mon Sep 17 00:00:00 2001 From: octalsrc Date: Fri, 15 Sep 2017 11:25:20 -0600 Subject: [PATCH 5/8] Define `modelT` function --- .../abstracting/tc/symbolic/package.scala | 25 +++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala index 6e375ef..bc47df1 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala @@ -65,14 +65,35 @@ package object symbolic { implicitly[SymAbstract[A,S]] } - def modelT[C,S]( + def modelT[C,S : Symbol]( t: Transformer[S] )( pre: Constraint[S], post: Constraint[S] )( implicit iM: Model[C] {type Schema = S} - ): Option[(C,C)] = ??? + ): Option[(C,C)] = { + val baseName = "modelT" + val preName = baseName + "-pre" + val postName = baseName + "-post" + val (schemaValPre,declPre) = Symbol[S].draw(preName) + val (schemaValPost,declPost) = Symbol[S].draw(postName) + + val z3 = Z3Interpreter.buildDefault + + val assertion = Seq( + Assert(pre(schemaValPre)), + Assert(post(schemaValPost)), + Assert(t(schemaValPre,schemaValPost)) + ) + + (declPre ++ declPost ++ assertion ++ Seq(CheckSat())).map(z3.eval) + + for { + mPre <- Model[C].getModel(preName, z3) + mPost <- Model[C].getModel(postName, z3) + } yield (mPre,mPost) + } def postHatUp[C,A : Semilattice,S : Symbol](t: Transformer[S])(v: A)( implicit iM: Model[C] {type Schema = S}, iS: SymAbstract[A,S], iA: Abstraction[C,A] From 003f431737b9da97dd6b1d9239d6f36a2607e214 Mon Sep 17 00:00:00 2001 From: octalsrc Date: Fri, 22 Sep 2017 11:35:27 -0600 Subject: [PATCH 6/8] Define symbolic transformers --- .../plv/cuanto/abstracting/tc/domains/Interval.scala | 12 ++++++++++++ .../plv/cuanto/abstracting/tc/symbolic/package.scala | 2 +- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala index 0c93526..b320ac5 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala @@ -5,6 +5,7 @@ package domains import smtlib.Interpreter import smtlib.parser.Commands.{Command, DeclareConst} import smtlib.parser.Terms._ +import smtlib.theories.Core._ import smtlib.theories.Ints._ import symbolic._ @@ -149,4 +150,15 @@ package object interval { } + object symbolic { + def add(a: IntSMT): Transformer[IntSMT] = { + case (IntSMT(i1),IntSMT(i2)) => + Equals(Add(sTerm(i1),sTerm(a.int1)), sTerm(i2)) + } + def sub(a: IntSMT): Transformer[IntSMT] = { + case (IntSMT(i1),IntSMT(i2)) => + Equals(Sub(sTerm(i1),sTerm(a.int1)), sTerm(i2)) + } + } + } diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala index bc47df1..4a703f2 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala @@ -107,7 +107,7 @@ package object symbolic { recur(bot[A]) } - def comprehend[V : SMTVal](m: List[SExpr]): Map[SSymbol,V] = { + private[this] def comprehend[V : SMTVal](m: List[SExpr]): Map[SSymbol,V] = { val p: (Map[SSymbol,V],SExpr) => Map[SSymbol,V] = { (acc,i) => i match { case DefineFun(FunDef(id,_,_,v)) => SMTVal[V].interpret(v) match { From cee27d855c24d9002804b7bcebc12d0780e1ea16 Mon Sep 17 00:00:00 2001 From: octalsrc Date: Fri, 6 Oct 2017 08:38:12 -0600 Subject: [PATCH 7/8] Define abstract transformers --- .../abstracting/tc/domains/Interval.scala | 22 +++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala index b320ac5..48ed060 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala @@ -151,14 +151,28 @@ package object interval { } object symbolic { - def add(a: IntSMT): Transformer[IntSMT] = { + def add(a: Int): Transformer[IntSMT] = { case (IntSMT(i1),IntSMT(i2)) => - Equals(Add(sTerm(i1),sTerm(a.int1)), sTerm(i2)) + Equals(Add(sTerm(i1),NumeralLit(BigInt(a))), sTerm(i2)) } - def sub(a: IntSMT): Transformer[IntSMT] = { + def sub(a: Int): Transformer[IntSMT] = { case (IntSMT(i1),IntSMT(i2)) => - Equals(Sub(sTerm(i1),sTerm(a.int1)), sTerm(i2)) + Equals(Sub(sTerm(i1),NumeralLit(BigInt(a))), sTerm(i2)) } } + def add(n: Int)(a: Interval): Interval = a match { + case Btw(g1,l1) => Btw(g1 + n, l1 + n) + case Lte(l) => Lte(l + n) + case Gte(g) => Gte(g + n) + case i => i // Bottom or Top will remain the same + } + + def sub(n: Int)(a: Interval): Interval = a match { + case Btw(g1,l1) => Btw(g1 - n, l1 - n) + case Lte(l) => Lte(l - n) + case Gte(g) => Gte(g - n) + case i => i + } + } From bce71a36aa25ebfe408c5eaea75bff5b910fc4ae Mon Sep 17 00:00:00 2001 From: octalsrc Date: Fri, 6 Oct 2017 11:23:57 -0600 Subject: [PATCH 8/8] Add test for modelT over IntSMT values --- .../tc/domains/SymbolicIntervalSpec.scala | 25 ++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala b/src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala index ab0df8f..f3d3f63 100644 --- a/src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala +++ b/src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala @@ -5,7 +5,7 @@ package domains.interval import smtlib.theories.Core._ import smtlib.theories.Ints._ -import symbolic._ +import abstracting.tc.symbolic._ import instances._ @@ -41,4 +41,27 @@ class SymbolicIntervalSpec extends CuantoSpec { model("asdf",btwSpec(2,1)) should equal (None) } + + + val addSpec: Int => Transformer[IntSMT] = + n => { + case (IntSMT(a1),IntSMT(a2)) => Equals( + Add(sTerm(a1),NumeralLit(BigInt(n))), + sTerm(a2) + ) + } + + val transformerTests = Table[ + (Transformer[IntSMT],Constraint[IntSMT],Constraint[IntSMT]), + ((Int,Int)) => Boolean + ]( + "SMT Transformer and constraints" -> "Int pair predicate", + (addSpec(1),gteSpec(1),gteSpec(5)) -> { case ((i1,i2)) => (i1 + 1) == i2 } + ) + + "The Int symbolic representation" should "produce transformer models" in { + forAll (transformerTests) { + case ((t,pre,post),p) => modelT(t)(pre,post).map(p) should equal (Some(true)) + } + } }