diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 0000000..87efca9 --- /dev/null +++ b/Dockerfile @@ -0,0 +1,54 @@ +#FROM ubuntu:18.04 # note: trying 20.04 because of glibc 2.29 req for infer + +FROM ubuntu:20.04 +RUN apt-get update +RUN apt-get install -y gcc make sudo cmake apt-transport-https software-properties-common binutils g++ curl +RUN apt-get install -y wget apt-transport-https gnupg python +#RUN wget -qO - https://adoptopenjdk.jfrog.io/adoptopenjdk/api/gpg/key/public | sudo apt-key add - +#RUN echo "deb https://adoptopenjdk.jfrog.io/adoptopenjdk/deb bionic main" | sudo tee /etc/apt/sources.list.d/adoptopenjdk.list +RUN apt-get update +#RUN apt-get -y install adoptopenjdk-11-hotspot +# Install OpenJDK-11 +RUN apt-get update && \ + apt-get install -y openjdk-11-jdk && \ + apt-get clean; +ENV JAVA_HOME "/usr/lib/jvm/java-11-openjdk-amd64/" +RUN mkdir /home/bounder + +## 3. sbt +#RUN echo "deb https://dl.bintray.com/sbt/debian /" | sudo tee -a /etc/apt/sources.list.d/sbt.list +#RUN sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv 2EE0EA64E40A89B84B2DF73499E82A75642AC823 +#RUN sudo apt-get update +#RUN sudo apt-get install -y sbt + +# SBT +RUN echo "deb https://repo.scala-sbt.org/scalasbt/debian all main" | sudo tee /etc/apt/sources.list.d/sbt.list +RUN echo "deb https://repo.scala-sbt.org/scalasbt/debian /" | sudo tee /etc/apt/sources.list.d/sbt_old.list +RUN curl -sL "https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x2EE0EA64E40A89B84B2DF73499E82A75642AC823" | sudo -H gpg --no-default-keyring --keyring gnupg-ring:/etc/apt/trusted.gpg.d/scalasbt-release.gpg --import +RUN sudo chmod 644 /etc/apt/trusted.gpg.d/scalasbt-release.gpg +RUN sudo apt-get update +RUN sudo apt-get install -y sbt + +## Microsoft z3 +ENV Z3_VERSION "4.12.5" +# install debian packages +RUN apt-get update -qq -y +RUN apt-get install binutils g++ make ant -y +RUN apt-get clean +RUN rm -rf /var/lib/apt/lists/* +# +# download, compile and install Z3 +RUN Z3_DIR="$(mktemp -d)" +RUN cd "$Z3_DIR" +RUN wget -qO- https://github.com/Z3Prover/z3/archive/z3-${Z3_VERSION}.tar.gz | tar xz --strip-components=1 +RUN python scripts/mk_make.py --java +RUN cd /build && make && sudo make install +# RUN ls -a +#failing here +# RUN make -j +# RUN +# RUN cd / +# RUN rm -rf "$Z3_DIR" + +RUN apt-get update +RUN apt-get install -y zip unzip \ No newline at end of file diff --git a/README.md b/README.md index 2a7a564..1396759 100644 --- a/README.md +++ b/README.md @@ -48,3 +48,24 @@ Week 5(analysis branch): - Added in `IncrementVar` as a sublass of `Executable` - Created `Conditional` class to hold comparisons - Changed `Rand` to have a max value to create more specific ranges + +Week 6(combine branch): + +- Worked in [dual_evaluate.worksheet.scala](src/main/scala/dual_evaluate.worksheet.sc) to try to find a awy to call the same evaluate function for any domain(concrete, abstract, etc.) + +Week 7 and 8(combine branch): + +- Researched Types and Classes, polymorphism(ad hoc and parametric), and Type Classes. +- Started trying to implement a version of `evaluate` thats approximates the following: `evaluate[T]` => `T`, or in words you can pass the domain type to the evalute function, and each domain will implement each type of expression in its own way. In theory you would be able to call `.evaluate[Domain]` on any expression for whichever domain you wanted at the time. +- Changed to have a type class instead of `Evaluator[T]`, where each T would be a domain like `Int`, `Interval`, etc. All evaluates were outsourced to the `implicit object` of each domain type like `IntEvaluator` or `IntervalEvaluator`. +- Added the `Statement` trait which is for anything that changes state (while loops, executables, etc.). to evaluate a `Statement` you call `Statement.execute[T]`, which returns `State[T]` + +Week 9(combine branch): + +- Started learning docker and how to use a docker file in an attempt to integrate z3 as an smt for my interval analysis. +- Added a simple `Program` class that accepts a list of statements to execute, really just to make the language a bit more cohesive and look nicer. + +Week 10(combine branch): + +- Researched Octagonal Domain and strated adding into project +- [Source](https://arxiv.org/pdf/cs/0703084.pdf) diff --git a/build.sbt b/build.sbt index c22bc61..6660f48 100644 --- a/build.sbt +++ b/build.sbt @@ -6,6 +6,9 @@ lazy val root = project name := "taylor-fall", version := "0.1.0-SNAPSHOT", scalaVersion := scala3Version, - libraryDependencies += "org.scalameta" %% "munit" % "0.7.29" % Test + libraryDependencies += "org.scalameta" %% "munit" % "0.7.29" % Test, // libraryDependencies += "io.github.pityka" %% "nspl-awt" % "0.10.0" + // libraryDependencies += "org.scalacheck" %% "scalacheck" % "1.14.1" % Test + // libraryDependencies += "org.scalacheck" % "scalacheck" % "2.13.13" % Test + unmanagedJars in Compile += baseDirectory.value / "lib/com.microsoft.z3.jar" ) diff --git a/src/main/scala/Adddition.scala b/src/main/scala/Adddition.scala deleted file mode 100644 index b66cdcd..0000000 --- a/src/main/scala/Adddition.scala +++ /dev/null @@ -1,61 +0,0 @@ -class Addition(var a: Expression, var b: Expression, val sub: Boolean = false) - extends Expression: - override def evaluate(state: State): Int | String | scala.Boolean | Point = - - if (a.isInstanceOf[Point] && b.isInstanceOf[Point]) { - if (sub) then - return (a.asInstanceOf[Point] - b.asInstanceOf[Point]).evaluate(state) - else - return (a.asInstanceOf[Point] + b.asInstanceOf[Point]).evaluate(state) - } - val aval = a.evaluate(state) - val bval = b.evaluate(state) - - (aval, bval, sub) match { - case (a: Int, b: Int, false) => a + b - case (a: Int, b: Int, true) => a - b - case (a: String, b: String, _) => a + b - case (a: Boolean, b: Boolean, _) => a || b - case (a: Point, b: Point, true) => (a - b).evaluate(state) - case (a: Point, b: Point, false) => (a + b).evaluate(state) - case _ => - throw new Exception( - "Cannot add " + a.toString() + " and " + b.toString() - ) - } - /* if aval.isInstanceOf[Int] && bval.isInstanceOf[Int] then - if sub then - aval.asInstanceOf[Int] - bval.asInstanceOf[Int] - else - aval.asInstanceOf[Int] + bval.asInstanceOf[Int] - - else if aval.isInstanceOf[String] && bval.isInstanceOf[String] then - aval.asInstanceOf[String] + bval.asInstanceOf[String] - else if aval.isInstanceOf[scala.Boolean] && bval.isInstanceOf[scala.Boolean] then - aval.asInstanceOf[scala.Boolean] || bval.asInstanceOf[scala.Boolean] - else - throw new Exception( - "Cannot add " + aval.toString() + " and " + bval.toString() - ) */ - - end evaluate - - override def abstract_evaluate(state: State): Interval | TwoDInterval = - val aval = a.abstract_evaluate(state) - val bval = b.abstract_evaluate(state) - (aval, bval) match { - case (a: Interval, b: Interval) => if sub then a - b else a + b - case (a: TwoDInterval, b: TwoDInterval) => if sub then a - b else a + b - case _ => - throw new Exception( - "Cannot add " + aval.toString() + " and " + bval.toString() - ) - } - - override def toString: String = { - "Addition(" + a.toString() + ", " + b.toString() + (if !sub then ")" - else - (", sub: " + sub - .toString() + ")" - )) - } diff --git a/src/main/scala/Bool.scala b/src/main/scala/Bool.scala deleted file mode 100644 index 70733ee..0000000 --- a/src/main/scala/Bool.scala +++ /dev/null @@ -1,8 +0,0 @@ -case class Bool(value: scala.Boolean) extends Expression { - override def evaluate(state: State): scala.Boolean = value - override def abstract_evaluate(state: State): Interval = - val as_int = if value then 1 else 0 - Interval(as_int, true, as_int, true) - - override def toString: String = "Boolean(" + value.toString + ")"; -} diff --git a/src/main/scala/Executable.scala b/src/main/scala/Executable.scala deleted file mode 100644 index 17e1967..0000000 --- a/src/main/scala/Executable.scala +++ /dev/null @@ -1,21 +0,0 @@ -class Executable(body: Function1[State, Unit]) extends Expression { - override def evaluate(state: State): Int | String | scala.Boolean = - body(state) - return 0; - override def abstract_evaluate(state: State): Interval = - // somehow "run" the code abstractly, storing new intervals in the state - Interval(0, true, 0, true) - - def executeInterval(interval: Interval): Interval = { - return interval - } - override def toString(): String = "Executable" -} - -case class IncrementVar(x: Variable, c: Int) - extends Executable((state: State) => { - x.addAssign(Number(c), state) - }) { - - override def executeInterval(interval: Interval): Interval = interval + c -} diff --git a/src/main/scala/Expression.scala b/src/main/scala/Expression.scala deleted file mode 100644 index 7d7ac54..0000000 --- a/src/main/scala/Expression.scala +++ /dev/null @@ -1,222 +0,0 @@ -trait Expression: - def evaluate(state: State): Int | String | scala.Boolean | Point - def abstract_evaluate(state: State): Interval | TwoDInterval -end Expression - -case class Infinity(neg: Boolean): - override def toString(): String = if neg then "-Infinity" else "Infinity" - def *(num: Int): Infinity = if num < 0 then Infinity(!neg) else this - def <(num: Int): Boolean = if neg then true else false - def >(num: Int): Boolean = if neg then false else true - def >(num: Infinity): Boolean = if neg then false else true - def <(num: Infinity): Boolean = if neg then true else false - def ==(num: Infinity): Boolean = neg == num.neg - def ==(num: Int): Boolean = false - -case class Interval( - low: Int | Infinity, - lowInc: Boolean, - high: Int | Infinity, - highInc: Boolean -): - override def toString(): String = - (if lowInc then "[" else "(") + low.toString() + ", " + high - .toString() + (if highInc then "]" else ")") - - def *(num: Int): Interval = - if (num == 0) { - throw new Exception("Multiplying Interval by 0 is not allowed") - } - Interval( - high match { - case h: Int => h * num - case h: Infinity => h * (num / (num.abs)) - }, - highInc, - low match { - case l: Int => l * num - case l: Infinity => l * (num / (num.abs)) - }, - lowInc - ) - - def *(other: Interval): Interval = - var low = this.low - var high = this.high - var lowInc = this.lowInc - var highInc = this.highInc - // lower bound - if (this.low.isInstanceOf[Infinity] || other.low.isInstanceOf[Infinity]) { - low = Infinity(true) - lowInc = false - } else { - low = this.low.asInstanceOf[Int] * other.low.asInstanceOf[Int] - lowInc = this.lowInc && other.lowInc - } - - // upper bound - if (this.high.isInstanceOf[Infinity] || other.high.isInstanceOf[Infinity]) { - high = Infinity(false) - highInc = false - } else { - high = this.high.asInstanceOf[Int] * other.high.asInstanceOf[Int] - highInc = this.highInc && other.highInc - } - - Interval(low, lowInc, high, highInc) - - def union(other: Interval): Interval = - var min = this.low - var max = this.high - var minInc, maxInc = true - if (this.low.isInstanceOf[Infinity] || other.low.isInstanceOf[Infinity]) - then - min = Infinity(true) - minInc = false - else - if (this.low.asInstanceOf[Int] < other.low.asInstanceOf[Int]) - then - min = this.low - minInc = this.lowInc - else if (this.low.asInstanceOf[Int] > other.low.asInstanceOf[Int]) - min = other.low - minInc = other.lowInc - else - min = this.low - minInc = this.lowInc && other.lowInc - end if - end if - - if (this.high.isInstanceOf[Infinity] || other.high.isInstanceOf[Infinity]) - then - max = Infinity(false) - maxInc = false - else - if (this.high.asInstanceOf[Int] > other.high.asInstanceOf[Int]) - then - max = this.high - maxInc = this.highInc - else if (this.high.asInstanceOf[Int] < other.high.asInstanceOf[Int]) - max = other.high - maxInc = other.highInc - else - max = this.high - maxInc = this.highInc && other.highInc - end if - end if - - Interval(min, minInc, max, maxInc) - - def +(other: Interval): Interval = - var min = this.low - var max = this.high - var minInc, maxInc = true - if (this.low.isInstanceOf[Infinity] || other.low.isInstanceOf[Infinity]) - then - min = Infinity(true) - minInc = false - else - min = this.low.asInstanceOf[Int] + other.low.asInstanceOf[Int] - minInc = this.lowInc && other.lowInc - end if - - if (this.high.isInstanceOf[Infinity] || other.high.isInstanceOf[Infinity]) - then - max = Infinity(false) - maxInc = false - else - max = this.high.asInstanceOf[Int] + other.high.asInstanceOf[Int] - maxInc = this.highInc && other.highInc - end if - - Interval(min, minInc, max, maxInc) - def +(other: Int): Interval = - this + Interval(other, true, other, true) - def -(other: Interval): Interval = - this + other * -1 - -class Bottom() extends Interval(0, false, 0, false): - override def toString(): String = "\u22A5" - override def *(num: Int): Interval = this - override def *(other: Interval): Interval = this - override def union(other: Interval): Interval = other - override def +(other: Interval): Interval = this - override def -(other: Interval): Interval = this - -case class TwoDInterval(x: Interval, y: Interval): - override def toString(): String = - "(" + x.toString() + ", " + y.toString() + ")" - def union(other: TwoDInterval): TwoDInterval = - TwoDInterval(x union other.x, y union other.y) - def +(other: TwoDInterval): TwoDInterval = - TwoDInterval(x + other.x, y + other.y) - def -(other: TwoDInterval): TwoDInterval = - TwoDInterval(x - other.x, y - other.y) - def *(other: Interval): TwoDInterval = TwoDInterval(x * other, y * other) - def *(num: Int): TwoDInterval = TwoDInterval(x * num, y * num) - - // TODO allow input for rand so it can be within a range -case class Rand(max: Int = Int.MaxValue) extends Expression: - override def evaluate(state: State): Int = - scala.util.Random.nextInt(max) - override def abstract_evaluate(state: State): Interval = - Interval( - 0, - true, - if max == Int.MaxValue then Infinity(false) else max, - if max == Int.MaxValue then false else true - ) - override def toString(): String = "Rand()" - -//think about potential uses/extensions - -//could you integrate abstract analyiss to gps/mapping? perhaps making sure someone stays inside a certain area/range no matter what path they take? -//i feel like theres something with gps we could do here -//look into r3 and algabraic analysis as well - -//models? -//2d visualizations for non-deterministic steps -//states in xy plane - give it increasing number of possible moves -//chance of if in certain interval new behaviour is introduced -//interaction of two states? - -//should add in more operations/expressions like if, while. these should help with non determinism - -// type IntOrInfinity = Int | Infinity -//extension to allow comparison operators on Int | Infinity -extension (x: Int | Infinity) - def <(y: Int | Infinity): Boolean = (x, y) match { - case (x: Infinity, y: Infinity) => x < y - case (x: Int, y: Int) => x < y - case (x: Infinity, y: Int) => x < y - case (x: Int, y: Infinity) => x < y - case _ => false // should be unreachable - } - def >(y: Int | Infinity): Boolean = (x, y) match { - case (x: Infinity, y: Infinity) => x > y - case (x: Int, y: Int) => x > y - case (x: Infinity, y: Int) => x > y - case (x: Int, y: Infinity) => x > y - case _ => false // should be unreachable - } - def ==(y: Int | Infinity): Boolean = (x, y) match { - case (x: Infinity, y: Infinity) => x == y - case (x: Int, y: Int) => x == y - case (x: Infinity, y: Int) => false - case (x: Int, y: Infinity) => false - case _ => false // should be unreachable - } - def <=(y: Int | Infinity): Boolean = (x, y) match { - case (x: Infinity, y: Infinity) => x < y - case (x: Int, y: Int) => x <= y - case (x: Infinity, y: Int) => x < y - case (x: Int, y: Infinity) => x < y - case _ => false // should be unreachable - } - def >=(y: Int | Infinity): Boolean = (x, y) match { - case (x: Infinity, y: Infinity) => x > y - case (x: Int, y: Int) => x >= y - case (x: Infinity, y: Int) => x > y - case (x: Int, y: Infinity) => x > y - case _ => false // should be unreachable - } diff --git a/src/main/scala/Multiplication.scala b/src/main/scala/Multiplication.scala deleted file mode 100644 index 5e79675..0000000 --- a/src/main/scala/Multiplication.scala +++ /dev/null @@ -1,25 +0,0 @@ -case class Multiplication(a: Expression, b: Expression) extends Expression: - override def evaluate(state: State): Int | Point = - val aval = a.evaluate(state) - val bval = b.evaluate(state) - (aval, bval) match { - case (aval: Int, bval: Int) => aval * bval - case (aval: Point, bval: Int) => - (a.asInstanceOf[Point] * bval).evaluate(state) - case _ => - throw new Exception( - "Cannot multipy " + aval.toString() + " and " + bval.toString() - ) - } - override def abstract_evaluate(state: State): Interval | TwoDInterval = - (a.abstract_evaluate(state), b.abstract_evaluate(state)) match { - case (a: Interval, b: Interval) => a * b - case (a: TwoDInterval, b: Interval) => a * b - case _ => - throw new Exception( - "Invalid multiplication: " + this.toString() - ) - - } - override def toString: String = - "Multiplication(" + a.toString() + ", " + b.toString() + ")" diff --git a/src/main/scala/MyString.scala b/src/main/scala/MyString.scala deleted file mode 100644 index a0ad80f..0000000 --- a/src/main/scala/MyString.scala +++ /dev/null @@ -1,6 +0,0 @@ -case class MyString(str: String) extends Expression: - override def evaluate(state: State): String = str - // TODO: implement this - override def abstract_evaluate(state: State): Interval = - Interval(0, true, 0, true) - override def toString: String = "MyString(\"" + str.toString() + "\")" diff --git a/src/main/scala/Number.scala b/src/main/scala/Number.scala deleted file mode 100644 index b0383a4..0000000 --- a/src/main/scala/Number.scala +++ /dev/null @@ -1,5 +0,0 @@ -case class Number(num: Int) extends Expression: - override def evaluate(sttae: State): Int = num - override def abstract_evaluate(state: State): Interval = - Interval(num, true, num, true) - override def toString: String = "Number(" + num.toString() + ")" diff --git a/src/main/scala/Point.scala b/src/main/scala/Point.scala deleted file mode 100644 index 409271b..0000000 --- a/src/main/scala/Point.scala +++ /dev/null @@ -1,67 +0,0 @@ -case class Point(x: Expression | Int, y: Expression | Int) extends Expression: - override def evaluate(state: State): Point = (x, y) match { - case (x: Expression, y: Expression) => - (x.evaluate(state), y.evaluate(state)) match { - case (x: Int, y: Int) => Point(x, y) - case _ => - throw new Exception( - "Invalid type for Point: " + this.toString() - ) - } - case (x: Int, y: Int) => Point(x, y) - case _ => - throw new Exception( - "Invalid form of Point: " + this.toString() - ) - } - override def abstract_evaluate(state: State): TwoDInterval = (x, y) match { - case (x: Expression, y: Expression) => - (x.abstract_evaluate(state), y.abstract_evaluate(state)) match { - case (x: Interval, y: Interval) => TwoDInterval(x, y) - case _ => - throw new Exception( - "Invalid form of Interval: " + x.toString() + ", " + y.toString() - ) - } - case (x: Int, y: Int) => - TwoDInterval( - Interval(x, true, x, true), - Interval(y, true, y, true) - ) // this is basically a concrete interval, hopefully would never get called - case _ => - throw new Exception( - "Invalid form of Point: " + this.toString() - ) - } - - override def toString: String = - "Point(" + x.toString() + ", " + y.toString() + ")" - - def +(other: Point): Point = (x, y, other.x, other.y) match { - case (x: Expression, y: Expression, ox: Expression, oy: Expression) => - Point(Addition(x, ox), Addition(y, oy)) - case (x: Int, y: Int, ox: Int, oy: Int) => Point(x + ox, y + oy) - case _ => - throw new Exception( - "Cannot perfom operation(+) on this form of Point: " + this.toString() - ) - } - - def -(other: Point): Point = (x, y, other.x, other.y) match { - case (x: Expression, y: Expression, ox: Expression, oy: Expression) => - Point(Addition(x, ox, sub = true), Addition(y, oy, sub = true)) - case (x: Int, y: Int, ox: Int, oy: Int) => Point(x - ox, y - oy) - case _ => - throw new Exception( - "Cannot perfom operation(-) on this form of Point: " + this.toString() - ) - } - - def *(num: Int): Point = (x, y) match { - case (x: Expression, y: Expression) => - Point(Multiplication(x, Number(num)), Multiplication(y, Number(num))) - case _ => - throw new Exception( - "Cannot perfom operation(*) on this form of Point: " + this.toString() - ) - } diff --git a/src/main/scala/State.scala b/src/main/scala/State.scala deleted file mode 100644 index 7995686..0000000 --- a/src/main/scala/State.scala +++ /dev/null @@ -1,6 +0,0 @@ -class State(): - var variables = collection.mutable.Map[String, Expression]() - - var intervals = collection.mutable.Map[String, Interval | TwoDInterval]() - -//perhaps have state hold the total interval of each variable across the whole program? diff --git a/src/main/scala/Variable.scala b/src/main/scala/Variable.scala deleted file mode 100644 index 09d489d..0000000 --- a/src/main/scala/Variable.scala +++ /dev/null @@ -1,48 +0,0 @@ -case class Variable(identifier: String) extends Expression { - override def evaluate(state: State): Int | String | scala.Boolean | Point = - state.variables.get(identifier).get.evaluate(state) - override def abstract_evaluate(state: State): Interval | TwoDInterval = - state.variables.get(identifier).get.abstract_evaluate(state) - - // choose not to statically type variable types - // assignment will be the way to update scope's intervals - - def assign(newValue: Expression, state: State): Unit = - if (state.variables.contains(identifier)) then - state.variables(identifier) = newValue - // every time a variable is updated, the state will pick up the new interval - state.intervals(identifier) = - (state.intervals(identifier), newValue.abstract_evaluate(state)) match { - case (o: Interval, n: Interval) => o union n - case (o: TwoDInterval, n: TwoDInterval) => o union n - case _ => - throw new Exception( - "Invalid interval type" - ) // should be impossible to reach - } - else { - state.variables += (identifier -> newValue) - state.intervals += (identifier -> newValue.abstract_evaluate(state)) - } - - def addAssign(value: Expression, state: State): Unit = - if (state.variables.contains(identifier)) then - state.variables(identifier) = Addition(state.variables(identifier), value) - // every time a variable is updated, the state will pick up the new interval - state.intervals(identifier) = - (state.intervals(identifier), value.abstract_evaluate(state)) match { - case (o: Interval, n: Interval) => o union (o + n) - case (o: TwoDInterval, n: TwoDInterval) => o union (o + n) - case _ => - throw new Exception( - "Invalid interval type" - ) // should be impossible to reach - } - else throw new Exception("Variable not intialized") - - override def toString: String = "Variable(" + identifier.toString + ")"; - -} - -//assignment currently can't handle holding itself, would need -//to evalute before storing but that defeats whole purpose of abstract evaluation diff --git a/src/main/scala/domains/Concrete.scala b/src/main/scala/domains/Concrete.scala new file mode 100644 index 0000000..f9ad77c --- /dev/null +++ b/src/main/scala/domains/Concrete.scala @@ -0,0 +1,92 @@ +import scala.util.Random + +/* case class Concrete(value: Int) extends Domain: + def +(other: Domain): Domain = other match { + case other: Concrete => Concrete(other.value + value) + case _ => + throw new Exception("Cannot add Concrete int and " + other.toString()) + } + def -(other: Domain): Domain = other match { + case other: Concrete => Concrete(value - other.value) + case _ => + throw new Exception( + "Cannot subtract Concrete int and " + other.toString() + ) + } + def *(other: Domain): Domain = other match { + case other: Concrete => Concrete(other.value * value) + case _ => + throw new Exception( + "Cannot multiply Concrete int and " + other.toString() + ) + } + def <(other: Domain): Domain = other match { + case other: Concrete => Concrete(if (value < other.value) 1 else 0) + case _ => + throw new Exception("Cannot compare Concrete int and " + other.toString()) + } + def >(other: Domain): Domain = other match { + case other: Concrete => Concrete(if (value > other.value) 1 else 0) + case _ => + throw new Exception("Cannot compare Concrete int and " + other.toString()) + } + + def rand(max: Int): Domain = Concrete(Random.nextInt(max)) + override def toString(): String = "Int" */ + +implicit object IntEvaluator extends Evaluator[Int] { + def evaluate(expr: Expression, state: State[Int]): Int = expr match { + case Addition(left, right, sub) => + if (sub) left.evaluate[Int](state) - right.evaluate[Int](state) + else + left.evaluate[Int](state) + right.evaluate[Int](state) + case Rand(max) => Random.nextInt(max) + case Number(num) => num + case Conditional(a, comp, b) => + if comp match { + case LessThan => + (a.evaluate[Int](state) < b.evaluate[Int](state)) + case GreaterThan => + (a.evaluate[Int](state) > b.evaluate[Int](state)) + case Equals => + (a.evaluate[Int](state) == b.evaluate[Int](state)) + + } + then 1 + else 0 + case Variable(identifier) => state.variables(identifier) + case _ => null.asInstanceOf[Int] + } + + def execute(stmt: Statement, state: State[Int]): State[Int] = stmt match { + case IncrementVar(x, c) => + state.variables(x.identifier) += c.evaluate[Int](state) + state + case stmt: While_Statement => { + while (stmt.evalConditional[Int](state) != 0) { + stmt.execBody[Int](state) + } + state + } + case _ => null + } +} + +/* implicit object BooleanEvaluator extends Evaluator[Boolean] { + def evaluate(expr: Expression, state: State[Boolean]): Boolean = expr match { + case Conditional(a, comp, b) => + if comp match { + case LessThan => + (a.evaluate[Boolean](state) < b.evaluate[Boolean](state)) + case GreaterThan => + (a.evaluate[Boolean](state) > b.evaluate[Boolean](state)) + case Equals => + (a.evaluate[Boolean](state) == b.evaluate[Boolean](state)) + + } + then true + else false + case _ => null.asInstanceOf[Boolean] + } +} + */ diff --git a/src/main/scala/domains/Interval.scala b/src/main/scala/domains/Interval.scala new file mode 100644 index 0000000..1f5a674 --- /dev/null +++ b/src/main/scala/domains/Interval.scala @@ -0,0 +1,467 @@ +case class Interval( + low: Int | Infinity, + lowInc: Boolean, + high: Int | Infinity, + highInc: Boolean +) extends Operable: + override def toString(): String = + (if lowInc then "[" else "(") + low.toString() + ", " + high + .toString() + (if highInc then "]" else ")") + + def *(num: Int): Interval = + if (num == 0) { + throw new Exception("Multiplying Interval by 0 is not allowed") + } + Interval( + high match { + case h: Int => h * num + case h: Infinity => h * (num / (num.abs)) + }, + highInc, + low match { + case l: Int => l * num + case l: Infinity => l * (num / (num.abs)) + }, + lowInc + ) + + def *(other: Interval): Interval = + var low = this.low + var high = this.high + var lowInc = this.lowInc + var highInc = this.highInc + // lower bound + if (this.low.isInstanceOf[Infinity] || other.low.isInstanceOf[Infinity]) { + low = Infinity(true) + lowInc = false + } else { + low = this.low.asInstanceOf[Int] * other.low.asInstanceOf[Int] + lowInc = this.lowInc && other.lowInc + } + + // upper bound + if (this.high.isInstanceOf[Infinity] || other.high.isInstanceOf[Infinity]) { + high = Infinity(false) + highInc = false + } else { + high = this.high.asInstanceOf[Int] * other.high.asInstanceOf[Int] + highInc = this.highInc && other.highInc + } + + Interval(low, lowInc, high, highInc) + + def union(other: Interval): Interval = + var min = this.low + var max = this.high + var minInc, maxInc = true + if (this.low.isInstanceOf[Infinity] || other.low.isInstanceOf[Infinity]) + then + min = Infinity(true) + minInc = false + else + if (this.low.asInstanceOf[Int] < other.low.asInstanceOf[Int]) + then + min = this.low + minInc = this.lowInc + else if (this.low.asInstanceOf[Int] > other.low.asInstanceOf[Int]) + min = other.low + minInc = other.lowInc + else + min = this.low + minInc = this.lowInc && other.lowInc + end if + end if + + if (this.high.isInstanceOf[Infinity] || other.high.isInstanceOf[Infinity]) + then + max = Infinity(false) + maxInc = false + else + if (this.high.asInstanceOf[Int] > other.high.asInstanceOf[Int]) + then + max = this.high + maxInc = this.highInc + else if (this.high.asInstanceOf[Int] < other.high.asInstanceOf[Int]) + max = other.high + maxInc = other.highInc + else + max = this.high + maxInc = this.highInc && other.highInc + end if + end if + + Interval(min, minInc, max, maxInc) + def negate(other: Interval): Interval = { + // returns the stuff left over after a union + if (this.low == other.low && this.high == other.high) then Bottom() + else if (this.low == other.low) then + Interval(other.high, !other.highInc, this.high, this.highInc) + else if (this.high == other.high) then + Interval(this.low, this.lowInc, other.low, !other.lowInc) + else if (this.low < other.low) then + Interval(this.low, this.lowInc, other.low - 1, true) + else if (this.high > other.high) then + Interval(other.high - -1, true, this.high, this.highInc) + else Bottom() + } + def +(other: Interval): Interval = + var min = this.low + var max = this.high + var minInc, maxInc = true + if (this.low.isInstanceOf[Infinity] || other.low.isInstanceOf[Infinity]) + then + min = Infinity(true) + minInc = false + else + min = this.low.asInstanceOf[Int] + other.low.asInstanceOf[Int] + minInc = this.lowInc && other.lowInc + end if + + if (this.high.isInstanceOf[Infinity] || other.high.isInstanceOf[Infinity]) + then + max = Infinity(false) + maxInc = false + else + max = this.high.asInstanceOf[Int] + other.high.asInstanceOf[Int] + maxInc = this.highInc && other.highInc + end if + + Interval(min, minInc, max, maxInc) + def +(other: Int): Interval = + this + Interval(other, true, other, true) + def -(other: Interval): Interval = + this + other * -1 + def rand(max: Int): Interval = + Interval(0, true, max, true) + // returns the interval that is less than the other interval + def <(other: Int): Interval = + if (this.high < other) then this + else if (this.low > other) then Bottom() + else Interval(this.low, this.lowInc, other - 1, true) + def >(other: Int): Interval = + if (this.low > other) then this + else if (this.high < other) then Bottom() + else Interval(other + 1, true, this.high, this.highInc) + def <(other: Interval): Interval = + // returns the part of the interval that is true for the given operator + if (this.high < other.low) then this + else if (this.low > other.high) then Bottom() + else Interval(this.low, this.lowInc, other.low - 1, true) + def >(other: Interval): Interval = + if (this.low > other.high) then this + else if (this.high < other.low) then Bottom() + else Interval(other.high - -1, true, this.high, this.highInc) + // not sure if i am doing this that well + def ==(other: Interval): Interval = { + if (this.low == other.low && this.high == other.high) then this + else Bottom() + } + + def +(other: Operable): Operable = other match { + case other: Interval => this + other + } + def *(other: Operable): Operable = other match { + case other: Interval => this * other + } + def -(other: Operable): Operable = other match { + case other: Interval => this - other + } +class Bottom() extends Interval(0, false, 0, false): + + override def toString(): String = "\u22A5" // ⊥ + override def *(num: Int): Interval = this + override def *(other: Interval): Interval = this + override def union(other: Interval): Interval = other + override def +(other: Interval): Interval = this + override def -(other: Interval): Interval = this + def +(other: Bottom): Interval = this + +class Top() extends Interval(Infinity(true), true, Infinity(false), true): + override def toString(): String = "\u22A4" // ⊤(not T) + override def *(num: Int): Interval = this + override def *(other: Interval): Interval = this + override def union(other: Interval): Interval = this + override def +(other: Interval): Interval = this + override def -(other: Interval): Interval = this + +class Identity() extends Interval(0, true, 0, true) { + override def toString(): String = "Identity" + override def *(other: Interval): Interval = other + override def union(other: Interval): Interval = other + override def +(other: Interval): Interval = other + override def -(other: Interval): Interval = other + +} + +case class Infinity(neg: Boolean): + override def toString(): String = if neg then "-Infinity" else "Infinity" + def *(num: Int): Infinity = if num < 0 then Infinity(!neg) else this + def <(num: Int): Boolean = if neg then true else false + def >(num: Int): Boolean = if neg then false else true + def >(num: Infinity): Boolean = if neg then false else true + def <(num: Infinity): Boolean = if neg then true else false + def ==(num: Infinity): Boolean = neg == num.neg + def ==(num: Int): Boolean = false + +//Two D Interval(removed because useless) +/* case class TwoDInterval(x: Interval, y: Interval) extends Domain: +override def toString(): String = + "(" + x.toString() + ", " + y.toString() + ")" +def union(other: TwoDInterval): TwoDInterval = + TwoDInterval(x union other.x, y union other.y) +def +(other: TwoDInterval): TwoDInterval = + TwoDInterval(x + other.x, y + other.y) +def -(other: TwoDInterval): TwoDInterval = + TwoDInterval(x - other.x, y - other.y) +def *(other: Interval): TwoDInterval = TwoDInterval(x * other, y * other) +def *(num: Concrete): TwoDInterval = TwoDInterval(x * num, y * num) + */ + +extension (x: Int | Infinity) + def <(y: Int | Infinity): Boolean = (x, y) match { + case (x: Infinity, y: Infinity) => x < y + case (x: Int, y: Int) => x < y + case (x: Infinity, y: Int) => x < y + case (x: Int, y: Infinity) => x < y + case _ => false // should be unreachable + } + def >(y: Int | Infinity): Boolean = (x, y) match { + case (x: Infinity, y: Infinity) => x > y + case (x: Int, y: Int) => x > y + case (x: Infinity, y: Int) => x > y + case (x: Int, y: Infinity) => x > y + case _ => false // should be unreachable + } + def ==(y: Int | Infinity): Boolean = (x, y) match { + case (x: Infinity, y: Infinity) => x == y + case (x: Int, y: Int) => x == y + case (x: Infinity, y: Int) => false + case (x: Int, y: Infinity) => false + case _ => false // should be unreachable + } + def <=(y: Int | Infinity): Boolean = (x, y) match { + case (x: Infinity, y: Infinity) => x < y + case (x: Int, y: Int) => x <= y + case (x: Infinity, y: Int) => x < y + case (x: Int, y: Infinity) => x < y + case _ => false // should be unreachable + } + def >=(y: Int | Infinity): Boolean = (x, y) match { + case (x: Infinity, y: Infinity) => x > y + case (x: Int, y: Int) => x >= y + case (x: Infinity, y: Int) => x > y + case (x: Int, y: Infinity) => x > y + case _ => false // should be unreachable + } + def -(y: Int | Infinity): Int | Infinity = (x, y) match { + case (x: Infinity, y: Infinity) => null // how tf does one know? + case (x: Int, y: Int) => x - y + case (x: Infinity, y: Int) => Infinity(x.neg) + case (x: Int, y: Infinity) => Infinity(!y.neg) + case _ => 0 // should be unreachable + } + /* + couldn't get scala to like this because of type erasure. + def +(y: Int | Infinity): Int | Infinity = (x, y) match { + case (x: Infinity, y: Infinity) => null // how tf does one know? + case (x: Int, y: Int) => x + y + case (x: Infinity, y: Int) => Infinity(x.neg) + case (x: Int, y: Infinity) => Infinity(y.neg) + case _ => 0 // should be unreachable + } */ +implicit object IntervalEvaluator extends Evaluator[Interval] { + def evaluate(expr: Expression, state: State[Interval]): Interval = + expr match { + case Number(value) => Interval(value, true, value, true) + case Rand(max) => Interval(0, true, max, true) + case Variable(identifier) => state.variables(identifier) + case Addition(left, right, sub) => + if (sub) + left.evaluate[Interval](state) - right.evaluate[Interval](state) + else left.evaluate[Interval](state) + right.evaluate[Interval](state) + case Conditional(a, comp, b) => { + val aEval = a.evaluate[Interval](state) + val bEval = b.evaluate[Interval](state) + comp match { + case LessThan => aEval < bEval + case GreaterThan => aEval > bEval + case Equals => aEval == bEval + } + } + case stmt: While_Statement => Bottom() // while_interval(state, stmt) + case _ => Bottom() + } + + // doesn't mean run the program, it means evaluate but for a Statement + def execute(stmt: Statement, state: State[Interval]): State[Interval] = + stmt match { + case IncrementVar(x, c) => { + state.variables(x.identifier) += c.evaluate[Interval](state); + state + } + case stmt: While_Statement => while_interval(state, stmt) + case _ => null.asInstanceOf[State[Interval]] + } + + def while_interval( + state: State[Interval], + stmt: While_Statement + ): State[Interval] = { + // this maps each position to the next possible ones + val topologicalMap = Map( + 0 -> List(1), + 1 -> List(3, 2), + 2 -> List(0, 3), + 3 -> List() // No outgoing transitions from position 4 + ) + + // maps each position to the state there + var intervals = collection.mutable.Map( + 0 -> state, + 1 -> State[Interval](), + 2 -> State[Interval](), + 3 -> State[Interval]() + ) + // need some way to keep track of what was changed + var oldIntervals = intervals.clone() + + // what happens at each position + val transfers = + Map( + 0 -> (() => { + var together = intervals(0) union intervals(2) + for ((k, v) <- together.variables) { + var high = v.high + var low = v.low + var highInc = v.highInc + var lowInc = v.lowInc + // for now just if it has increased, then assume it will always increase + if (v.high > intervals(1).variables.getOrElse(k, v).high) { + high = Infinity(false) + highInc = false + } + // same with decrease + if (v.low < intervals(1).variables.getOrElse(k, v).low) { + low = Infinity(true) + lowInc = false + } + together.variables(k) = Interval(low, lowInc, high, highInc) + } + intervals(0) = together + }), // merges 0 and 2 if possible(with fake wideing operator) + 1 -> (() => { + intervals(1) = + stmt.splitInterval(intervals(0))._2 // 2 is the true branch + }), // splits 0 at b, 1 holds true branch + 2 -> (() => + intervals(2) = stmt.execBody[Interval](intervals(1)) + ), // call the executable with 1 + 3 -> (() => { + intervals(3) = + stmt.splitInterval(intervals(0))._1 // 1 is false branch + + }) // holds false branch + ) + + // queue to keep track of the positions + var queue = + scala.collection.mutable.Queue(1) // start the queue with position one + var position = 0 + + // makes everything look nicer + println(Console.GREEN + "Start of Anaylsis" + Console.RESET) + println("--------------------") + println("Current position: " + position) + println("Current intervals" + intervals.toString()) + println("Current queue: " + queue.toString()) + + // loop to go through queue + while (queue.nonEmpty) { + position = queue.dequeue() + + transfers(position)() + // at the end, if there was a change we add next places onto new queue + if (!intervals.equals(oldIntervals)) { + oldIntervals = intervals.clone() + topologicalMap(position).foreach(queue.enqueue(_)) + } + println("--------------------") + println("Current position: " + position) + println("Current intervals" + intervals.toString()) + println("Current queue: " + queue.toString()) + } + + // if position 3 is bottom, then we try to call 3 one time to see if there is any change + if (position != 3 && intervals(3).isEmpty()) { + transfers(3)() + println("--------------------") + println("Current position: " + position) + println("Current intervals" + intervals.toString()) + println("Current queue: " + queue.toString()) + } + + println("--------------------") + println(Console.GREEN + "End of Analysis" + Console.RESET) + println("--------------------") + + // return the interval at the end + return intervals(3) + } +} + +extension (x: State[Interval]) + def union(y: State[Interval]): State[Interval] = { + val newState = State[Interval]() + for ((k: String, v: Interval) <- x.variables) { + newState.variables(k) = v union y.variables.getOrElse(k, Identity()) + } + for ((k: String, v: Interval) <- y.variables) { + if (!x.variables.contains(k)) { + newState.variables(k) = v + } + } + newState + } + +extension (stmt: While_Statement) + // takes an interval and splits it over the conditional returning (false, true) branches + // for now only works when one variable is used in the conditional + def splitInterval( + state: State[Interval] + ): (State[Interval], State[Interval]) = { + val cond = stmt.getCond() + + (cond.a, cond.b) match { + case (a: Variable, b: Variable) => null + case ( + a: Variable, + b: Expression + ) => { + var trueBranch = state.clone() + var falseBranch = state.clone() + trueBranch.variables(a.identifier) = + trueBranch.variables(a.identifier) union b.evaluate[Interval](state) + falseBranch.variables(a.identifier) = falseBranch.variables( + a.identifier + ) negate b.evaluate[Interval](state) + (falseBranch, trueBranch) + } // split a over b with cond.comp + case ( + a: Expression, + b: Variable + ) => { + var trueBranch = state.clone() + var falseBranch = state.clone() + trueBranch.variables(b.identifier) = + trueBranch.variables(b.identifier) union a.evaluate[Interval](state) + falseBranch.variables(b.identifier) = falseBranch.variables( + b.identifier + ) negate a.evaluate[Interval](state) + (falseBranch, trueBranch) + } // split b over a with cond.comp + case (a: Expression, b: Expression) => + null // don't want to do infinite loops + + } + + } diff --git a/src/main/scala/domains/Octagonal.scala b/src/main/scala/domains/Octagonal.scala new file mode 100644 index 0000000..30daa48 --- /dev/null +++ b/src/main/scala/domains/Octagonal.scala @@ -0,0 +1,42 @@ +import scala.compiletime.ops.double +case class Octagonal(dbm: Array[Array[Float]]) {} + +def StrongClosure(m: Array[Array[Float]]): Array[Array[Float]] = { + var m_hist = Array.ofDim[Float](m.length + 1, m.length, m.length) + m_hist(0) = m + for k: Int <- 0 until m.length do m_hist(k + 1) = S(C(2 * k, m_hist(k))) + + return m_hist(m.length) + +} + +def C(k: Int, n: Array[Array[Float]]): Array[Array[Float]] = { + var ret = Array.ofDim[Float](n.length, n.length) + for + i <- 0 until n.length + j <- 0 until n.length + do + if i == j then ret(i)(i) = 0 + else + ret(i)(j) = min( + n(i)(j), + (n(i)(k) + n(k)(j)), + (n(i)(opp(k)) + n(opp(k))(j)), + (n(i)(k) + n(k)(opp(k)) + n(opp(k))(j)), + (n(i)(opp(k)) + n(opp(k))(k) + n(k)(j)) + ) + return ret +} + +def S(n: Array[Array[Float]]): Array[Array[Float]] = { + var ret = Array.ofDim[Float](n.length, n.length) + for + i <- 0 until n.length + j <- 0 until n.length + do ret(i)(j) = min(n(i)(j), (n(i)(opp(j)) + n(opp(j))(j)) / 2) + return ret; +} + +// Helper functions +def opp(i: Int): Int = if i % 2 == 0 then i + 1 else i - 1 +def min(values: Float*): Float = values.min diff --git a/src/main/scala/domains/octagonal notes.txt b/src/main/scala/domains/octagonal notes.txt new file mode 100644 index 0000000..64e5150 --- /dev/null +++ b/src/main/scala/domains/octagonal notes.txt @@ -0,0 +1,3 @@ +Notes on octagonal domains: + +seems to be essier when implemented with a Difference-Bound Matrix(DBM) diff --git a/src/main/scala/expressions/Adddition.scala b/src/main/scala/expressions/Adddition.scala new file mode 100644 index 0000000..eac2bfb --- /dev/null +++ b/src/main/scala/expressions/Adddition.scala @@ -0,0 +1,9 @@ +case class Addition(a: Expression, b: Expression, sub: Boolean = false) + extends Expression: + override def toString: String = { + "Addition(" + a.toString() + ", " + b.toString() + (if !sub then ")" + else + (", sub: " + sub + .toString() + ")" + )) + } diff --git a/src/main/scala/expressions/Conditional.scala b/src/main/scala/expressions/Conditional.scala new file mode 100644 index 0000000..72c551b --- /dev/null +++ b/src/main/scala/expressions/Conditional.scala @@ -0,0 +1,78 @@ +sealed trait ComparisonOperator + +case object LessThan extends ComparisonOperator +case object GreaterThan extends ComparisonOperator +case object Equals extends ComparisonOperator + +case class Conditional(a: Expression, comp: ComparisonOperator, b: Expression) + extends Expression { + /* override def evaluate[T <: Domain](state: State[T]): T = { + val aval = a.evaluate[T](state) + val bval = b.evaluate[T](state) + comp match { + case LessThan => (aval < bval).asInstanceOf[T] + case GreaterThan => (aval > bval).asInstanceOf[T] + case Equals => (aval == bval).asInstanceOf[T] + + } + } */ + + // override def abstract_evaluate(state: State): TwoDInterval = ??? + + // given an interval for the variable in the conditional, returns the (false, true) intervals + def splitInterval(interval: Interval): (Interval, Interval) = { + val bval = b.evaluate[Int](State[Int]()) + comp match { + case LessThan => + if (interval.high <= bval) { + (Bottom(), interval) // false, true + } else if (interval.low >= bval) { + (interval, Bottom()) // false, true + } else { + ( + Interval(bval, true, interval.high, interval.highInc), + Interval(interval.low, true, bval - 1, true) + ) // false,true + } + case GreaterThan => + if (interval.low >= bval) { + (Bottom(), interval) // false,true + } else if (interval.high <= bval) { + (interval, Bottom()) // false,true + } else { + ( + Interval(interval.low, interval.lowInc, bval, true), + Interval(bval + 1, true, interval.high, interval.highInc) + ) // false,true + } + + // TODO this will likely involve split intervals?? + // TODO ensure this follows false, true + case Equals => + if (interval.low > bval || interval.high < bval) { + (Bottom(), Bottom()) + } else if (interval.low == bval && interval.high == bval) { + (interval, interval) + } else if (interval.low == bval) { + ( + Interval(bval, true, bval, true), + Interval(bval + 1, true, interval.high, interval.highInc) + ) + } else if (interval.high == bval) { + ( + Interval(interval.low, interval.lowInc, bval - 1, true), + Interval(bval, true, bval, true) + ) + } else { + ( + Interval(interval.low, interval.lowInc, bval - 1, true), + Interval(bval, true, interval.high, interval.highInc) + ) + } + } + } + + override def toString(): String = + "Conditional(" + a.toString() + ", " + comp.toString() + ", " + b + .toString() + ")" +} diff --git a/src/main/scala/expressions/Expression.scala b/src/main/scala/expressions/Expression.scala new file mode 100644 index 0000000..7665e7f --- /dev/null +++ b/src/main/scala/expressions/Expression.scala @@ -0,0 +1,22 @@ +trait Operable: + def +(other: Operable): Operable + def -(other: Operable): Operable + def *(other: Operable): Operable + +trait Evaluator[T] { + def evaluate(expr: Expression, state: State[T]): T + def execute(stmt: Statement, state: State[T]): State[T] +} +trait Expression: + def evaluate[T](using evaluator: Evaluator[T])(state: State[T]): T = + evaluator.evaluate(this, state) + // def abstract_evaluate(state: State): Interval | TwoDInterval +end Expression + +extension (x: Operable | Int) + def +(y: Operable | Int): Operable | Int = (x, y) match { + case (x: Int, y: Int) => x + y + case (x: Int, y: Operable) => null + case (x: Operable, y: Int) => null + case (x: Operable, y: Operable) => x + y + } diff --git a/src/main/scala/expressions/Number.scala b/src/main/scala/expressions/Number.scala new file mode 100644 index 0000000..03d0360 --- /dev/null +++ b/src/main/scala/expressions/Number.scala @@ -0,0 +1,9 @@ +case class Number(num: Int) extends Expression: + /* override def evaluate[T <: Domain](state: State[T]): Concrete = Concrete( + num + ) */ + // don't love this evaluate, would love for it to return interval or whatever else the T domain is + + // override def abstract_evaluate(state: State): Interval = + // Interval(num, true, num, true) + override def toString: String = "Number(" + num.toString() + ")" diff --git a/src/main/scala/expressions/Rand.scala b/src/main/scala/expressions/Rand.scala new file mode 100644 index 0000000..1da7df2 --- /dev/null +++ b/src/main/scala/expressions/Rand.scala @@ -0,0 +1,11 @@ +case class Rand(max: Int = Int.MaxValue) extends Expression: + + /* override def abstract_evaluate(state: State): Interval = + Interval( + 0, + true, + if max == Int.MaxValue then Infinity(false) else max, + if max == Int.MaxValue then false else true + ) + */ + override def toString(): String = "Rand()" diff --git a/src/main/scala/playground/dual_evaluate.worksheet.sc b/src/main/scala/playground/dual_evaluate.worksheet.sc new file mode 100644 index 0000000..d51f138 --- /dev/null +++ b/src/main/scala/playground/dual_evaluate.worksheet.sc @@ -0,0 +1,159 @@ +object Basics { + sealed trait Expression + final case class Number(n: Int) extends Expression + final case class Addition(a: Expression, b: Expression) extends Expression + + def evaluate(e: Expression): Int = e match { + case Number(n) => n + case Addition(a, b) => evaluate(a) + evaluate(b) + } + + val test = Addition(Number(1), Number(1)) +} +Basics.evaluate(Basics.test) + +object BasicsWithAbstract { + trait Expression + trait AbstractExpression extends Expression + type Interval = scala.collection.immutable.Range + + final case class Number(n: Int) extends Expression + final case class Addition(a: Expression, b: Expression) extends Expression + final case class AbstractNumber(n: Interval) extends Expression + + extension (a: Int | Interval) { + def +(other: Int | Interval): Int | Interval = (a, other) match { + case (a: Int, b: Int) => a + b + case (a: Interval, b: Interval) => a + b + case _ => null + } + } + + def evaluate(e: Expression): Int | Interval = e match { + case Number(n) => n + case Addition(a, b) => evaluate(a) + evaluate(b) + case AbstractNumber(n) => n + } + + val test1 = + Addition(AbstractNumber(Range(1, 2)), AbstractNumber(Range(4, 7))) + val test2 = Addition(Number(1), Number(2)) +} +// BasicsWithAbstract.evaluate(BasicsWithAbstract.test1) +BasicsWithAbstract.evaluate(BasicsWithAbstract.test2) + +object Attempt1 { + case class Interval(a: Int, b: Int) { + def +(other: Interval): Interval = Interval(a + other.a, b + other.b) + } + + type Ret = Int | Interval + + trait Expression { + def evaluate(): Ret + } + + trait Plus[T](a: T, b: T) { + def evalPlus(): Ret = (a, b) match { + case (a: Int, b: Int) => a + b + case (a: Interval, b: Interval) => a + b + case _ => null + } + } + + class RealPlus[RT <: Int](a: RT, b: RT) + extends Expression + with Plus[RT](a, b) { + def evaluate(): Ret = evalPlus() + } + + class AbstPlus[AT <: Interval](a: AT, b: AT) + extends Expression + with Plus[AT](a, b) { + def evaluate(): Ret = evalPlus() + } + + val test1 = RealPlus[Int](2, 4) + val test2 = AbstPlus[Interval](Interval(1, 2), Interval(2, 2)) +} +Attempt1.test1.evaluate() +Attempt1.test2.evaluate() +//Problem with attempt1 is that it is backwards, need to find a way to reverse the order of shared extensions +//In attempt1 I wanted to pursure the dual extension of traits, similar to interfaces in java + +object Attempt2 { + case class Interval(a: Int, b: Int) { + def +(other: Interval): Interval = Interval(a + other.a, b + other.b) + } + type Ret = Int | Interval + extension (a: Ret) { + def +(b: Ret): Ret = (a, b) match { + case (a: Int, b: Int) => a + b + case (a: Interval, b: Interval) => a + b + case _ => null + } + } + abstract trait Expression + abstract trait AbstractExpression // (v: T) + + case class Number(v: Int) extends Expression + case class AbstractNumber(v: Interval) extends AbstractExpression + case class Addition[T](a: T, b: T) extends Expression with AbstractExpression + + def evaluate(e: Expression | AbstractExpression): Ret = e match { + case Number(v) => v + // wanted to do: + // case e:Addition[Expression] => ... but scala loses generic types at runtime + case e: Addition[_] => + (e.a, e.b) match { + case (a: Expression, b: Expression) => evaluate(a) + evaluate(b) + case (a: AbstractExpression, b: AbstractExpression) => + evaluate(a) + evaluate(b) + } + case AbstractNumber(v) => v + case _ => null + } + + val test = Addition[Number](Number(1), Number(1)) + val test2 = Addition[AbstractExpression]( + AbstractNumber(Interval(1, 2)), + AbstractNumber(Interval(3, 5)) + ) + +} +Attempt2.evaluate(Attempt2.test) +Attempt2.evaluate(Attempt2.test2) +//In attempt 2 I continued the extend _ with _ idea, but made a more unified evaluate expression + +object Thoughts { + abstract trait StateType + trait Concrete extends StateType + trait Abstract extends StateType + class State[ + T <: StateType + ] + // could this just be T and that is the type that the state maps variables to? + // no because what about variables of different datatypes? + + abstract trait Expression + // this function takes a state, either concrete or abstract and runs it through any expression + // lowkey may be cheating but who knows + def evaluate[T <: StateType](e: Expression, s: State[T]): State[T] = ??? + +} + +//Attempt 2 +/* object Attempt2 { + case class Interval(a: Int, b: Int) { + def +(other: Interval): Interval = Interval(a + other.a, b + other.b) + } + + type Ret = Int | Interval + trait Expression { + def evaluate(): Ret + } + def evaluate[T](e: Expression): Ret = ??? + trait RealPlus[T] + trait AbstPlus[T] + case class Plus[T](a: T, b: T) extends RealPlus[T] with AbstPlus[T] {} +} */ diff --git a/src/main/scala/playground/logic.worksheet.sc b/src/main/scala/playground/logic.worksheet.sc new file mode 100644 index 0000000..8b13789 --- /dev/null +++ b/src/main/scala/playground/logic.worksheet.sc @@ -0,0 +1 @@ + diff --git a/src/main/scala/program/Program.scala b/src/main/scala/program/Program.scala new file mode 100644 index 0000000..a1ce8ed --- /dev/null +++ b/src/main/scala/program/Program.scala @@ -0,0 +1,4 @@ +case class Program(commands: List[Statement]): + def evaluate[T](using evaluator: Evaluator[T])(state: State[T]): State[T] = + commands.foldLeft(state)((state, command) => command.execute[T](state)) + end evaluate diff --git a/src/main/scala/program/State.scala b/src/main/scala/program/State.scala new file mode 100644 index 0000000..374b3fe --- /dev/null +++ b/src/main/scala/program/State.scala @@ -0,0 +1,21 @@ +class State[T](): + var variables = collection.mutable.Map[String, T]() + def isEmpty(): Boolean = variables.isEmpty + + override def clone(): State[T] = { + val clonedState = new State[T]() + clonedState.variables = variables.clone() + clonedState + } + + override def toString(): String = + "State with variables: " + variables.toString + + override def equals(x: Any): Boolean = x match { + case other: State[_] => variables == other.variables + case _ => false + } + + // var intervals = collection.mutable.Map[String, Interval | TwoDInterval]() + +//perhaps have state hold the total interval of each variable across the whole program? diff --git a/src/main/scala/program/Variable.scala b/src/main/scala/program/Variable.scala new file mode 100644 index 0000000..0e8fe16 --- /dev/null +++ b/src/main/scala/program/Variable.scala @@ -0,0 +1,39 @@ +case class Variable(identifier: String) extends Expression { + /* override def evaluate[T <: Domain](state: State[T]): T = + state.variables.get(identifier).get */ + /* override def abstract_evaluate(state: State): Interval | TwoDInterval = + state.variables.get(identifier).get.abstract_evaluate(state) + */ + // choose not to statically type variable types + // assignment will be the way to update scope's intervals + + def assign[T](using + evaluator: Evaluator[T] + )(newValue: Expression, state: State[T]): Unit = + if (state.variables.contains(identifier)) then + state.variables(identifier) = newValue.evaluate[T](state) + // every time a variable is updated, the state will pick up the new interval + /* state.intervals(identifier) = + (state.intervals(identifier), newValue.abstract_evaluate(state)) match { + case (o: Interval, n: Interval) => o union n + case (o: TwoDInterval, n: TwoDInterval) => o union n + case _ => + throw new Exception( + "Invalid interval type" + ) // should be impossible to reach + } */ + else { + state.variables += (identifier -> newValue.evaluate[T](state)) + // state.intervals += (identifier -> newValue.abstract_evaluate(state)) + } + + // TODO work on making an addAssign method that will work for all types + def addAssign[T <: Operable | Int](value: T, state: State[T]): State[T] = + if (state.variables.contains(identifier)) then + state.variables(identifier) = + (state.variables(identifier) + value).asInstanceOf[T] + else throw new Exception("Variable not intialized") + return state + + override def toString: String = "Variable(" + identifier.toString + ")"; +} diff --git a/src/main/scala/If_Statement.scala b/src/main/scala/statements/If_Statement.txt similarity index 52% rename from src/main/scala/If_Statement.scala rename to src/main/scala/statements/If_Statement.txt index 5b31874..df67dc2 100644 --- a/src/main/scala/If_Statement.scala +++ b/src/main/scala/statements/If_Statement.txt @@ -1,100 +1,22 @@ -import scala.compiletime.ops.int +/* import scala.compiletime.ops.int class If_Statement(cond: Expression, tbranch: Expression, fbranch: Expression) extends Expression { - override def evaluate(state: State): Int | String | scala.Boolean | Point = { - if (cond.evaluate(state).asInstanceOf[scala.Boolean]) { - tbranch.evaluate(state) + override def evaluate[T <: Domain](state: State[T]): T = { + if (cond.evaluate[T](state).asInstanceOf[scala.Boolean]) { + tbranch.evaluate[T](state) } else { - fbranch.evaluate(state) + fbranch.evaluate[T](state) } } // TODO: implement this, how would you abstractly evaluate an if statement? probably merge the intervals of both branches - def abstract_evaluate(state: State): Interval = Interval(0, true, 0, true) + // def abstract_evaluate(state: State): Interval = Interval(0, true, 0, true) override def toString(): String = "If(" + cond.toString() + ") {" + tbranch.toString() + "} else {" + fbranch .toString() + "}" } -sealed trait ComparisonOperator - -case object LessThan extends ComparisonOperator -case object GreaterThan extends ComparisonOperator -case object Equals extends ComparisonOperator - -case class Conditional(a: Variable, comp: ComparisonOperator, b: Number) - extends Expression { - override def evaluate(state: State): Boolean = { - val aval = a.evaluate(state).asInstanceOf[Int] - val bval = b.evaluate(state) - comp match { - case LessThan => aval < bval - case GreaterThan => aval > bval - case Equals => aval == bval - - } - } - - override def abstract_evaluate(state: State): TwoDInterval = ??? - - // given an interval for the variable in the conditional, returns the (false, true) intervals - def splitInterval(interval: Interval): (Interval, Interval) = { - val bval = b.evaluate(State()).asInstanceOf[Int] - comp match { - case LessThan => - if (interval.high <= bval) { - (Bottom(), interval) // false, true - } else if (interval.low >= bval) { - (interval, Bottom()) // false, true - } else { - ( - Interval(bval, true, interval.high, interval.highInc), - Interval(interval.low, true, bval - 1, true) - ) // false,true - } - case GreaterThan => - if (interval.low >= bval) { - (Bottom(), interval) // false,true - } else if (interval.high <= bval) { - (interval, Bottom()) // false,true - } else { - ( - Interval(interval.low, interval.lowInc, bval, true), - Interval(bval + 1, true, interval.high, interval.highInc) - ) // false,true - } - - // TODO this will likely involve split intervals?? - // TODO ensure this follows false, true - case Equals => - if (interval.low > bval || interval.high < bval) { - (Bottom(), Bottom()) - } else if (interval.low == bval && interval.high == bval) { - (interval, interval) - } else if (interval.low == bval) { - ( - Interval(bval, true, bval, true), - Interval(bval + 1, true, interval.high, interval.highInc) - ) - } else if (interval.high == bval) { - ( - Interval(interval.low, interval.lowInc, bval - 1, true), - Interval(bval, true, bval, true) - ) - } else { - ( - Interval(interval.low, interval.lowInc, bval - 1, true), - Interval(bval, true, interval.high, interval.highInc) - ) - } - } - } - - override def toString(): String = - "Conditional(" + a.toString() + ", " + comp.toString() + ", " + b - .toString() + ")" -} /* case class LessThan(a: Expression, b: Expression) extends Conditional { override def evaluate(state: State): scala.Boolean = { @@ -182,3 +104,4 @@ case class And(a: Expression, b: Expression) extends Expression { "and(" + a.toString() + ", " + b.toString() + ")" } */ + */ diff --git a/src/main/scala/statements/Statement.scala b/src/main/scala/statements/Statement.scala new file mode 100644 index 0000000..a9b3837 --- /dev/null +++ b/src/main/scala/statements/Statement.scala @@ -0,0 +1,4 @@ +trait Statement: + def execute[T](using evaluator: Evaluator[T])(state: State[T]): State[T] = + evaluator.execute(this, state) +end Statement diff --git a/src/main/scala/statements/VariableStmts.scala b/src/main/scala/statements/VariableStmts.scala new file mode 100644 index 0000000..9c3e6cb --- /dev/null +++ b/src/main/scala/statements/VariableStmts.scala @@ -0,0 +1,16 @@ +//this class is only concrete increment(the += operator), does not rly work +case class IncrementVar(x: Variable, c: Expression) extends Statement + +case class AssignVar(identifier: String, value: Expression) extends Statement: + override def execute[T](using + evaluator: Evaluator[T] + )(state: State[T]): State[T] = { + value match { + case v: Variable => + state.variables += (identifier -> state.variables(v.identifier)) + case _ => + state.variables += (identifier -> value.evaluate[T](state)) + } + return state + } + end execute diff --git a/src/main/scala/While_Statement.scala b/src/main/scala/statements/While_Statement.scala similarity index 80% rename from src/main/scala/While_Statement.scala rename to src/main/scala/statements/While_Statement.scala index bdf1d8d..ac93160 100644 --- a/src/main/scala/While_Statement.scala +++ b/src/main/scala/statements/While_Statement.scala @@ -1,19 +1,25 @@ import java.util.concurrent.locks.Condition class While_Statement( cond: Conditional, - body: Executable -) extends Expression { - override def evaluate(state: State): Int | String | scala.Boolean = { + body: Statement +) extends Statement { + /* override def evaluate[T <: Domain](state: State[T]): T = { var num = 0 - while (cond.evaluate(state).asInstanceOf[scala.Boolean]) { - body.evaluate(state) + while (cond.evaluate[T](state).asInstanceOf[Boolean]) { + body.evaluate[T](state) } - return num // returns the number of times it looped, for now - } + return Concrete(num).asInstanceOf[T] + // returns the number of times it looped, for now + } */ - // TODO: implement this + /* override def evaluate[T](using evaluator: Evaluator[T])(state: State): T = + while (cond.evaluate[T](state).asInstanceOf[Boolean]) { + body.evaluate[T](state) + } */ + + // TODO: change this to invterval analysis through evaluate // This is where the actual beef of abstract evaluation will have to live - override def abstract_evaluate(state: State): Interval = + /* def abstract_evaluate(state: State[Interval]): Interval = // this maps each position to the next possible ones val topologicalMap = Map( 0 -> List(1), @@ -24,7 +30,7 @@ class While_Statement( // maps each position to the intervals there var intervals = collection.mutable.Map( - 0 -> state.variables("x").abstract_evaluate(state).asInstanceOf[Interval], + 0 -> Interval(0, true, 0, true), // TODO redo this, 1 -> Bottom(), 2 -> Bottom(), 3 -> Bottom() @@ -115,7 +121,13 @@ class While_Statement( // return the interval at the end return intervals(3) + */ + def evalConditional[T](using evaluator: Evaluator[T])(state: State[T]): T = + evaluator.evaluate(cond, state) + def execBody[T](using evaluator: Evaluator[T])(state: State[T]): State[T] = + evaluator.execute(body, state) + def getCond(): Conditional = cond } //if statement return two intervals (false, true) diff --git a/src/test/scala/MySuite.scala b/src/test/scala/MySuite.scala index f365df3..1d9af77 100644 --- a/src/test/scala/MySuite.scala +++ b/src/test/scala/MySuite.scala @@ -432,7 +432,7 @@ class MySuite extends munit.FunSuite { // Abstract while statement tests - test("x=Rand(4);While(x<3){x+=2}") { // normal loop + /* test("x=Rand(4);While(x<3){x+=2}") { // normal loop var state = State() Variable("x").assign(Rand(4), state) var test = While_Statement( @@ -489,7 +489,7 @@ class MySuite extends munit.FunSuite { Interval(0, false, 0, false) // sequivalent to bottom assertEquals(obtained, expected) - } + } */ // Interval union tests /* test("Interval union of (1,2] and [3,4]") { @@ -513,6 +513,104 @@ class MySuite extends munit.FunSuite { val expected = Interval(1, false, Infinity(false), false) assertEquals(obtained, expected) } */ + + // Tests done after type class overhaul + + /* test("1+1") { + val test = Addition(Number(1), Number(1)) + println(test.toString) + + // Int domain + var intState = State[Int]() + val intObtained = test.evaluate[Int](intState) + val intExpected = 2 + assertEquals(intObtained, intExpected) + + // Interval domain + var intervalState = State[Interval]() + val intervalObtained = test.evaluate[Interval](intervalState) + val intervalExpected = Interval(2, true, 2, true) + assertEquals(intervalObtained, intervalExpected) + } + + test("Rand(5)") { + val test = Rand(5) + println(test.toString) + + // Int domain + var intState = State[Int]() + val intObtained = test.evaluate[Int](intState) + val intExpected = 0 to 5 + assert(intExpected.contains(intObtained)) + + // Interval domain + var intervalState = State[Interval]() + val intervalObtained = test.evaluate[Interval](intervalState) + val intervalExpected = Interval(0, true, 5, true) + assertEquals(intervalObtained, intervalExpected) + } + + test("x=Rand(5)") { + val test = Variable("x") + println(test.toString) + + // Int domain + var intState = State[Int]() + Variable("x").assign[Int](Rand(5), intState) + val intObtained = test.evaluate[Int](intState) + val intExpected = 0 to 5 + assert(intExpected.contains(intObtained)) + + // Interval domain + var intervalState = State[Interval]() + Variable("x").assign[Interval](Rand(5), intervalState) + val intervalObtained = test.evaluate[Interval](intervalState) + val intervalExpected = Interval(0, true, 5, true) + assertEquals(intervalObtained, intervalExpected) + } + + test("x=Rand(5); While(x<3)(x+=2)") { + + val test = + While_Statement( + Conditional(Variable("x"), LessThan, Number(3)), + IncrementVar(Variable("x"), Number(2)) + ) + + // Int domain + var intState = State[Int]() + Variable("x").assign[Int](Rand(5), intState) + println(test.execute[Int](intState)) + val intObtained = test.execute[Int](intState) + + // Interval domain + var intervalState = State[Interval]() + Variable("x").assign[Interval](Rand(5), intervalState) + } + */ + // Switch to using Program + test("x=Rand(5); While(x<3)(x+=2)") { + val test = Program( + List( + AssignVar("x", Rand(5)), + While_Statement( + Conditional(Variable("x"), LessThan, Number(3)), + IncrementVar(Variable("x"), Number(2)) + ) + ) + ) + + // Int domain + var intState = State[Int]() + val intObtained = test.evaluate[Int](intState) + println(intObtained) + + // Interval domain + var intervalState = State[Interval]() + val intervalObtained = test.evaluate[Interval](intervalState) + println(intervalObtained) + + } } //start every time with x+y<=c1, x<=c2, y<=c3 diff --git a/src/test/scala/OctagonalTests.scala b/src/test/scala/OctagonalTests.scala new file mode 100644 index 0000000..8c677c6 --- /dev/null +++ b/src/test/scala/OctagonalTests.scala @@ -0,0 +1,13 @@ +class OctagonalTests extends munit.FunSuite { + test("Test 1") { + val oct = Array[Array[Float]]( + Array(0, 4, 4, 2), + Array(8, 0, 5, 7), + Array(7, 2, 0, 6), + Array(5, 4, 0, 0) + ) + + val obtained = StrongClosure(oct) + print(obtained) + } +}