From 897990f24401b217c472b3babe65096ddf51d667 Mon Sep 17 00:00:00 2001 From: Tianhan Lu Date: Fri, 27 Oct 2017 09:49:33 -0600 Subject: [PATCH 1/6] interval analysis for jsy using Apron --- .../cuanto/jsy/numdomain/IntervalDomain.scala | 136 ++++++++++++++++++ .../jsy/numdomain/IntervalDomainTest.scala | 37 +++++ 2 files changed, 173 insertions(+) create mode 100644 src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala create mode 100644 src/test/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomainTest.scala diff --git a/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala b/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala new file mode 100644 index 0000000..7e7f4b6 --- /dev/null +++ b/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala @@ -0,0 +1,136 @@ +package edu.colorado.plv.cuanto.jsy.numdomain + +import apron._ +import edu.colorado.plv.cuanto.jsy._ +import edu.colorado.plv.cuanto.jsy.arithmetic._ +import gmp.Mpfr + +/** + * @author Tianhan Lu + */ +object IntervalDomain { + implicit def convert(d: Double): MpfrScalar = new MpfrScalar(d, Mpfr.RNDU) + val ERROR_VAL = new Texpr1CstNode(-1.0) + + /** + * + * @param num a number + * @return an Apron expression that wraps the number + */ + def Wrap(num: N): Texpr1Node = new Texpr1CstNode(num.n) + + /** + * + * @param uop unary operator + * @param op operand could either be a double or a variable name + * @return an Apron expression that wraps the unary expression + */ + def Wrap(uop: Uop, op: Either[Double, String]): Texpr1BinNode = { + val operand = op match { + case Left(op) => new Texpr1CstNode(op) + case Right(op) => new Texpr1VarNode(op) + } + uop match { + case Neg => new Texpr1BinNode(Texpr0BinNode.OP_SUB, new Texpr1CstNode(0.0), operand) + } + } + + /** + * + * @param uop unary operator + * @param node an Apron expression + * @return an Apron expression that wraps the unary expression + */ + def Wrap(uop: Uop, node: Option[Texpr1Node]): Texpr1Node = { + node match { + case Some(node) => new Texpr1BinNode(Texpr0BinNode.OP_SUB, new Texpr1CstNode(0.0), node) + case None => ERROR_VAL + } + } + + /** + * + * @param bop binary operator + * @param left an Apron expression + * @param right an Apron expression + * @return an Apron expression that wraps the binary expression + */ + def Wrap(bop: Bop, left: Option[Texpr1Node], right: Option[Texpr1Node]): Texpr1Node = { + (left, right) match { + case (Some(left), Some(right)) => + bop match { + case Plus => new Texpr1BinNode(Texpr1BinNode.OP_ADD, left, right) + case Minus => new Texpr1BinNode(Texpr1BinNode.OP_SUB, left, right) + case Times => new Texpr1BinNode(Texpr1BinNode.OP_MUL, left, right) + case Div => new Texpr1BinNode(Texpr1BinNode.OP_DIV, left, right) + case x@_ => throw new Exception("Unsupported operator " + x) + } + case _ => ERROR_VAL + } + } + + /** + * + * @param bop binary operator + * @param op1 operand could either be a double or a variable name + * @param op2 operand could either be a double or a variable name + * @return an Apron expression that wraps the binary expression + */ + def Wrap(bop: Bop, op1: Either[Double, String], op2: Either[Double, String]): Texpr1BinNode = { + val left = op1 match { + case Left(op1) => new Texpr1CstNode(op1) + case Right(op1) => new Texpr1VarNode(op1) + } + val right = op2 match { + case Left(op2) => new Texpr1CstNode(op2) + case Right(op2) => new Texpr1VarNode(op2) + } + bop match { + case Plus => new Texpr1BinNode(Texpr1BinNode.OP_ADD, left, right) + case Minus => new Texpr1BinNode(Texpr1BinNode.OP_SUB, left, right) + case Times => new Texpr1BinNode(Texpr1BinNode.OP_MUL, left, right) + case Div => new Texpr1BinNode(Texpr1BinNode.OP_DIV, left, right) + case x@_ => throw new Exception("Unsupported operator " + x) + } + } + + /** + * + * @param e a jsy expression + * @return an Apron expression that represents the jsy expression + */ + def interpret(e: Expr): Option[Texpr1Node] = { + implicit def some: Texpr1Node => Option[Texpr1Node] = { Some(_) } + + e match { + /* Do rules. */ + case n@N(num) => Wrap(n) + case Unary(op, N(n1)) => Wrap(op, Left(n1)) + case Unary(op, edu.colorado.plv.cuanto.jsy.Var(name)) => Wrap(op, Right(name)) + case Binary(op, N(n1), N(n2)) => Wrap(op, Left(n1), Left(n2)) + case Binary(op, edu.colorado.plv.cuanto.jsy.Var(n1), edu.colorado.plv.cuanto.jsy.Var(n2)) => Wrap(op, Right(n1), Right(n2)) + case Binary(op, edu.colorado.plv.cuanto.jsy.Var(n1), N(n2)) => Wrap(op, Right(n1), Left(n2)) + case Binary(op, N(n1), edu.colorado.plv.cuanto.jsy.Var(n2)) => Wrap(op, Left(n1), Right(n2)) + + /* Search rules. */ + case Unary(op, e1) => + for { + e1p <- interpret(e1) + } yield + Wrap(op, e1p) + case Binary(op, v1 @ N(_), e2) => + for { + e2p <- interpret(e2) + } yield + Wrap(op, Wrap(v1), e2p) + case Binary(op, e1, e2) => + for { + e1p <- interpret(e1) + } yield + Wrap(op, e1p, interpret(e2)) + + /* Otherwise (including values) get stuck. */ + case _ => None + } + } +} diff --git a/src/test/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomainTest.scala b/src/test/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomainTest.scala new file mode 100644 index 0000000..2746483 --- /dev/null +++ b/src/test/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomainTest.scala @@ -0,0 +1,37 @@ +package edu.colorado.plv.cuanto.jsy.numdomain + +import apron._ +import edu.colorado.plv.cuanto.jsy.arithmetic.{Minus, N, Plus, Times} +import edu.colorado.plv.cuanto.jsy.{Binary, Var} +import org.scalatest.{FlatSpec, Matchers} + +/** + * @author Tianhan Lu + */ +class IntervalDomainTest extends FlatSpec with Matchers { + "Interval analysis" should "work on jsy" in { + val manager = new Polka(false) + val box = Array(new Interval(1, 10), new Interval(2, 5)) + val varnames = Array("x1", "x2") + val env = new Environment(varnames, Array[String]()) + /** + * The element is such that vars[i] is in interval box[i]. + * All variables from vars must be exist in the environment e. + * vars and box must have the same length. + */ + val a1 = new Abstract1(manager, env, varnames, box) + + /** + * (x1 + 3) * (x2 - 7) - 10 + */ + val target = Binary(Minus, Binary(Times, Binary(Plus, Var("x1"), N(3)), Binary(Minus, Var("x2"), N(7))), N(10)) + + // interpret the target expression into an Apron constraint + IntervalDomain.interpret(target) match { + case Some(cons) => + val res = a1.getBound(manager, new Texpr1Intern(env, cons)) + assert(res.toString == "[-75,-18]") + case None => throw new IllegalStateException("Cannot interpret a jsy expression into an Apron constraint") + } + } +} From c9fd4e9a3f80528d0f80b15c4e4f85c45ca86426 Mon Sep 17 00:00:00 2001 From: Tianhan Lu Date: Fri, 27 Oct 2017 10:10:20 -0600 Subject: [PATCH 2/6] code refactor --- .../cuanto/jsy/numdomain/IntervalDomain.scala | 61 +++++++++++-------- 1 file changed, 36 insertions(+), 25 deletions(-) diff --git a/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala b/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala index 7e7f4b6..0db5ecc 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala @@ -17,7 +17,7 @@ object IntervalDomain { * @param num a number * @return an Apron expression that wraps the number */ - def Wrap(num: N): Texpr1Node = new Texpr1CstNode(num.n) + def wrap(num: N): Texpr1Node = new Texpr1CstNode(num.n) /** * @@ -25,13 +25,13 @@ object IntervalDomain { * @param op operand could either be a double or a variable name * @return an Apron expression that wraps the unary expression */ - def Wrap(uop: Uop, op: Either[Double, String]): Texpr1BinNode = { + def wrap(uop: Uop, op: Either[Double, String]): Texpr1Node = { val operand = op match { case Left(op) => new Texpr1CstNode(op) case Right(op) => new Texpr1VarNode(op) } uop match { - case Neg => new Texpr1BinNode(Texpr0BinNode.OP_SUB, new Texpr1CstNode(0.0), operand) + case Neg => genNegNode(operand) } } @@ -41,9 +41,9 @@ object IntervalDomain { * @param node an Apron expression * @return an Apron expression that wraps the unary expression */ - def Wrap(uop: Uop, node: Option[Texpr1Node]): Texpr1Node = { + def wrap(uop: Uop, node: Option[Texpr1Node]): Texpr1Node = { node match { - case Some(node) => new Texpr1BinNode(Texpr0BinNode.OP_SUB, new Texpr1CstNode(0.0), node) + case Some(node) => genNegNode(node) case None => ERROR_VAL } } @@ -55,16 +55,9 @@ object IntervalDomain { * @param right an Apron expression * @return an Apron expression that wraps the binary expression */ - def Wrap(bop: Bop, left: Option[Texpr1Node], right: Option[Texpr1Node]): Texpr1Node = { + def wrap(bop: Bop, left: Option[Texpr1Node], right: Option[Texpr1Node]): Texpr1Node = { (left, right) match { - case (Some(left), Some(right)) => - bop match { - case Plus => new Texpr1BinNode(Texpr1BinNode.OP_ADD, left, right) - case Minus => new Texpr1BinNode(Texpr1BinNode.OP_SUB, left, right) - case Times => new Texpr1BinNode(Texpr1BinNode.OP_MUL, left, right) - case Div => new Texpr1BinNode(Texpr1BinNode.OP_DIV, left, right) - case x@_ => throw new Exception("Unsupported operator " + x) - } + case (Some(left), Some(right)) => genBinNode(bop, left, right) case _ => ERROR_VAL } } @@ -76,7 +69,7 @@ object IntervalDomain { * @param op2 operand could either be a double or a variable name * @return an Apron expression that wraps the binary expression */ - def Wrap(bop: Bop, op1: Either[Double, String], op2: Either[Double, String]): Texpr1BinNode = { + def wrap(bop: Bop, op1: Either[Double, String], op2: Either[Double, String]): Texpr1Node = { val left = op1 match { case Left(op1) => new Texpr1CstNode(op1) case Right(op1) => new Texpr1VarNode(op1) @@ -85,6 +78,24 @@ object IntervalDomain { case Left(op2) => new Texpr1CstNode(op2) case Right(op2) => new Texpr1VarNode(op2) } + genBinNode(bop, left, right) + } + + /** + * + * @param node an Apron expression + * @return an Apron expression that represents `0 - node` + */ + def genNegNode(node: Texpr1Node): Texpr1Node = new Texpr1BinNode(Texpr0BinNode.OP_SUB, new Texpr1CstNode(0.0), node) + + /** + * + * @param bop a binary operator + * @param left an Apron expression + * @param right an Apron expression + * @return an Apron expression that represents `left bop right` + */ + def genBinNode(bop: Bop, left: Texpr1Node, right: Texpr1Node): Texpr1Node = { bop match { case Plus => new Texpr1BinNode(Texpr1BinNode.OP_ADD, left, right) case Minus => new Texpr1BinNode(Texpr1BinNode.OP_SUB, left, right) @@ -104,30 +115,30 @@ object IntervalDomain { e match { /* Do rules. */ - case n@N(num) => Wrap(n) - case Unary(op, N(n1)) => Wrap(op, Left(n1)) - case Unary(op, edu.colorado.plv.cuanto.jsy.Var(name)) => Wrap(op, Right(name)) - case Binary(op, N(n1), N(n2)) => Wrap(op, Left(n1), Left(n2)) - case Binary(op, edu.colorado.plv.cuanto.jsy.Var(n1), edu.colorado.plv.cuanto.jsy.Var(n2)) => Wrap(op, Right(n1), Right(n2)) - case Binary(op, edu.colorado.plv.cuanto.jsy.Var(n1), N(n2)) => Wrap(op, Right(n1), Left(n2)) - case Binary(op, N(n1), edu.colorado.plv.cuanto.jsy.Var(n2)) => Wrap(op, Left(n1), Right(n2)) + case n@N(num) => wrap(n) + case Unary(op, N(n1)) => wrap(op, Left(n1)) + case Unary(op, edu.colorado.plv.cuanto.jsy.Var(name)) => wrap(op, Right(name)) + case Binary(op, N(n1), N(n2)) => wrap(op, Left(n1), Left(n2)) + case Binary(op, edu.colorado.plv.cuanto.jsy.Var(n1), edu.colorado.plv.cuanto.jsy.Var(n2)) => wrap(op, Right(n1), Right(n2)) + case Binary(op, edu.colorado.plv.cuanto.jsy.Var(n1), N(n2)) => wrap(op, Right(n1), Left(n2)) + case Binary(op, N(n1), edu.colorado.plv.cuanto.jsy.Var(n2)) => wrap(op, Left(n1), Right(n2)) /* Search rules. */ case Unary(op, e1) => for { e1p <- interpret(e1) } yield - Wrap(op, e1p) + wrap(op, e1p) case Binary(op, v1 @ N(_), e2) => for { e2p <- interpret(e2) } yield - Wrap(op, Wrap(v1), e2p) + wrap(op, wrap(v1), e2p) case Binary(op, e1, e2) => for { e1p <- interpret(e1) } yield - Wrap(op, e1p, interpret(e2)) + wrap(op, e1p, interpret(e2)) /* Otherwise (including values) get stuck. */ case _ => None From 669fa308a6cbd7a258e40e82b6c6db581e415d20 Mon Sep 17 00:00:00 2001 From: Tianhan Lu Date: Fri, 27 Oct 2017 10:30:20 -0600 Subject: [PATCH 3/6] add comments --- .../plv/cuanto/jsy/numdomain/IntervalDomainTest.scala | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/test/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomainTest.scala b/src/test/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomainTest.scala index 2746483..513f878 100644 --- a/src/test/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomainTest.scala +++ b/src/test/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomainTest.scala @@ -12,7 +12,9 @@ class IntervalDomainTest extends FlatSpec with Matchers { "Interval analysis" should "work on jsy" in { val manager = new Polka(false) val box = Array(new Interval(1, 10), new Interval(2, 5)) - val varnames = Array("x1", "x2") + val var1 = "x1" + val var2 = "x2" + val varnames = Array(var1, var2) val env = new Environment(varnames, Array[String]()) /** * The element is such that vars[i] is in interval box[i]. @@ -23,8 +25,10 @@ class IntervalDomainTest extends FlatSpec with Matchers { /** * (x1 + 3) * (x2 - 7) - 10 + * 1 <= x1 <= 10 + * 2 <= x2 <= 5 */ - val target = Binary(Minus, Binary(Times, Binary(Plus, Var("x1"), N(3)), Binary(Minus, Var("x2"), N(7))), N(10)) + val target = Binary(Minus, Binary(Times, Binary(Plus, Var(var1), N(3)), Binary(Minus, Var(var2), N(7))), N(10)) // interpret the target expression into an Apron constraint IntervalDomain.interpret(target) match { From 10146da842b452afe902041cb3367d20faabd891 Mon Sep 17 00:00:00 2001 From: Tianhan Lu Date: Fri, 27 Oct 2017 11:02:35 -0600 Subject: [PATCH 4/6] try to pass codacy --- .../colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala b/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala index 0db5ecc..1fdef24 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala @@ -10,7 +10,7 @@ import gmp.Mpfr */ object IntervalDomain { implicit def convert(d: Double): MpfrScalar = new MpfrScalar(d, Mpfr.RNDU) - val ERROR_VAL = new Texpr1CstNode(-1.0) + val ERROR = new Texpr1CstNode(-1.0) /** * @@ -44,7 +44,7 @@ object IntervalDomain { def wrap(uop: Uop, node: Option[Texpr1Node]): Texpr1Node = { node match { case Some(node) => genNegNode(node) - case None => ERROR_VAL + case None => ERROR } } @@ -58,7 +58,7 @@ object IntervalDomain { def wrap(bop: Bop, left: Option[Texpr1Node], right: Option[Texpr1Node]): Texpr1Node = { (left, right) match { case (Some(left), Some(right)) => genBinNode(bop, left, right) - case _ => ERROR_VAL + case _ => ERROR } } From 24de506c96e3f8fe5b37b8d1d84948690c3dbda3 Mon Sep 17 00:00:00 2001 From: Tianhan Lu Date: Fri, 27 Oct 2017 11:23:24 -0600 Subject: [PATCH 5/6] it does not make sense that renaming variables lead travis-ci to fail --- .../colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala b/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala index 1fdef24..0db5ecc 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala @@ -10,7 +10,7 @@ import gmp.Mpfr */ object IntervalDomain { implicit def convert(d: Double): MpfrScalar = new MpfrScalar(d, Mpfr.RNDU) - val ERROR = new Texpr1CstNode(-1.0) + val ERROR_VAL = new Texpr1CstNode(-1.0) /** * @@ -44,7 +44,7 @@ object IntervalDomain { def wrap(uop: Uop, node: Option[Texpr1Node]): Texpr1Node = { node match { case Some(node) => genNegNode(node) - case None => ERROR + case None => ERROR_VAL } } @@ -58,7 +58,7 @@ object IntervalDomain { def wrap(bop: Bop, left: Option[Texpr1Node], right: Option[Texpr1Node]): Texpr1Node = { (left, right) match { case (Some(left), Some(right)) => genBinNode(bop, left, right) - case _ => ERROR + case _ => ERROR_VAL } } From be4b429365026396a7d4776176221e2da7d8fd15 Mon Sep 17 00:00:00 2001 From: Tianhan Lu Date: Fri, 27 Oct 2017 13:14:29 -0600 Subject: [PATCH 6/6] try to pass codacy --- .../colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala b/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala index 0db5ecc..a5a9f5a 100644 --- a/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala +++ b/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala @@ -10,7 +10,7 @@ import gmp.Mpfr */ object IntervalDomain { implicit def convert(d: Double): MpfrScalar = new MpfrScalar(d, Mpfr.RNDU) - val ERROR_VAL = new Texpr1CstNode(-1.0) + val ERRORNODE = new Texpr1CstNode(-1.0) /** * @@ -44,7 +44,7 @@ object IntervalDomain { def wrap(uop: Uop, node: Option[Texpr1Node]): Texpr1Node = { node match { case Some(node) => genNegNode(node) - case None => ERROR_VAL + case None => ERRORNODE } } @@ -58,7 +58,7 @@ object IntervalDomain { def wrap(bop: Bop, left: Option[Texpr1Node], right: Option[Texpr1Node]): Texpr1Node = { (left, right) match { case (Some(left), Some(right)) => genBinNode(bop, left, right) - case _ => ERROR_VAL + case _ => ERRORNODE } }