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..a5a9f5a --- /dev/null +++ b/src/main/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomain.scala @@ -0,0 +1,147 @@ +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 ERRORNODE = 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]): Texpr1Node = { + val operand = op match { + case Left(op) => new Texpr1CstNode(op) + case Right(op) => new Texpr1VarNode(op) + } + uop match { + case Neg => genNegNode(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) => genNegNode(node) + case None => ERRORNODE + } + } + + /** + * + * @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)) => genBinNode(bop, left, right) + case _ => ERRORNODE + } + } + + /** + * + * @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]): Texpr1Node = { + 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) + } + 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) + 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..513f878 --- /dev/null +++ b/src/test/scala/edu/colorado/plv/cuanto/jsy/numdomain/IntervalDomainTest.scala @@ -0,0 +1,41 @@ +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 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]. + * 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 + * 1 <= x1 <= 10 + * 2 <= x2 <= 5 + */ + 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 { + 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") + } + } +}