Merge pull request #407 from UQ-PAC/collapsed-interval

DSA Clean Up

Author: sadrabt

examples/cntlm-noduk/cntlm-noduk.gts

@@ -4,15 +4,16 @@ import bap.*
 import boogie.*
 import translating.*
 import util.RunUtils
-import scala.sys.process.*
 
+import scala.sys.process.*
 import java.io.File
 import scala.collection.mutable.{ArrayBuffer, Set}
 import scala.collection.{immutable, mutable}
 import scala.language.postfixOps
 import scala.sys.process.*
 import util.*
-import mainargs.{main, arg, ParserForClass, Flag}
+import mainargs.{Flag, ParserForClass, arg, main}
+import util.DSAConfig.{Checks, Prereq, Standard}
 import util.boogie_interaction.BoogieResultKind
 
 object Main {
@@ -241,14 +242,12 @@ object Main {
 
     val dsa: Option[DSAConfig] = if (conf.simplify.value) {
       conf.dsaType match
-        case Some("set") => Some(DSAConfig(immutable.Set(DSAAnalysis.Set)))
-        case Some("field") => Some(DSAConfig(immutable.Set(DSAAnalysis.Field)))
-        case Some("norm") => Some(DSAConfig(immutable.Set(DSAAnalysis.Norm)))
-        case Some("all") => Some(DSAConfig(immutable.Set(DSAAnalysis.Set, DSAAnalysis.Field, DSAAnalysis.Norm)))
-        case Some("none") => Some(DSAConfig(immutable.Set.empty))
-        case None => None
+        case Some("prereq") => Some(Prereq)
+        case Some("checks") => Some(Checks)
+        case Some("standard") => Some(Standard)
+        case None => Some(Standard)
         case Some(_) =>
-          throw new IllegalArgumentException("Illegal option to dsa, allowed are: (none|set|field|norm|all)")
+          throw new IllegalArgumentException("Illegal option to dsa, allowed are: (prereq|standard|checks)")
     } else {
       None
     }

src/main/scala/Main.scala

@@ -0,0 +1,121 @@
+package analysis.data_structure_analysis
+
+import analysis.solvers.{DSAUnionFindSolver, OffsetUnionFindSolver, UnionFindSolver}
+import ir.eval.BitVectorEval.{bv2SignedInt, isNegative}
+import ir.{BVADD, BinaryExpr, BitVecLiteral, Expr, LocalAssign, Procedure, Program, Register}
+import specification.{ExternalFunction, SymbolTableEntry}
+import util.{DSALogger, IRContext}
+
+import java.io.File
+import scala.collection.{SortedSet, mutable}
+
+/**
+ * Integer Interval with top and bottom
+ * start (s) <= end (e)
+ * For purposes of overlapping and size the interval is inclusive of s and exclusive of e
+ */
+enum DSInterval extends Offsets {
+  case Top
+  case Bot
+  case Value(s: Int, e: Int)
+
+  this match
+    case DSInterval.Value(s, e) => assert(s <= e, "start of interval should be less than its end")
+    case _ =>
+
+  override def toString: String =
+    this match
+      case DSInterval.Top => "Top"
+      case DSInterval.Bot => "Bot"
+      case DSInterval.Value(start, end) => s"${start}_$end"
+
+  def start: Option[Int] =
+    this match
+      case DSInterval.Value(s, e) => Some(s)
+      case _ => None
+
+  def end: Option[Int] =
+    this match
+      case DSInterval.Value(s, e) => Some(e)
+      case _ => None
+
+  def size: Option[Int] =
+    this match
+      case DSInterval.Value(start, end) => Some(end - start)
+      case _ => None
+
+  def move(func: Int => Int): DSInterval =
+    this match
+      case DSInterval.Value(start, end) => Value(func(start), func(end))
+      case x => x
+
+  def isEmpty: Boolean = this.size.contains(0)
+
+  def growTo(size: Int): DSInterval =
+    this match
+      case DSInterval.Top => DSInterval.Top
+      case DSInterval.Value(start, end) => DSInterval(start, math.max(end, start + size))
+      case _ => this
+
+  def contains(offset: Int): Boolean =
+    this match
+      case DSInterval.Top => true
+      case DSInterval.Value(start, end) => start <= offset && (end > offset || end == start)
+      case _ => false
+
+  def contains(interval: DSInterval): Boolean =
+    (this, interval) match
+      case (DSInterval.Top, _) => true
+      case (_, DSInterval.Top) => false // this is not top
+      case (a, b) if a == b => true
+      case (DSInterval.Value(s, e), _) if s == e => false
+      case (DSInterval.Value(start1, end1), DSInterval.Value(start2, end2)) =>
+        start1 <= start2 && (end1 > end2 || (start2 < end2 && end1 >= end2))
+      case _ => false
+
+  def isOverlapping(other: DSInterval): Boolean =
+    (this, other) match
+      case (DSInterval.Top, _) => true
+      case (_, DSInterval.Top) => true
+      case (a, b) if a == b => true
+      case (DSInterval.Value(s1, e1), DSInterval.Value(s2, e2)) =>
+        (s2 < e1 && s2 >= s1) || (s1 < e2 && s1 >= s2)
+      case _ => false
+
+  def join(other: DSInterval): DSInterval = {
+    (this, other) match
+      case (DSInterval.Top, _) => DSInterval.Top
+      case (_, DSInterval.Top) => DSInterval.Top
+      case (DSInterval.Bot, x) => x
+      case (x, DSInterval.Bot) => x
+      case (DSInterval.Value(start1, end1), DSInterval.Value(start2, end2)) =>
+        DSInterval(math.min(start1, start2), math.max(end1, end2))
+  }
+
+  override def toOffsets: Set[Int] = {
+    this match
+      case DSInterval.Value(s, e) => Set(s to e: _*)
+      case _ => throw Exception("Attempted to retrieve offsets from top/bot")
+  }
+
+  override def toIntervals: Set[DSInterval] = {
+    this match
+      case DSInterval.Bot => Set.empty
+      case x => Set(x)
+  }
+
+}
+
+object DSInterval {
+  def apply(start: Int, end: Int) = {
+    require(start <= end, "start of interval should be less than it's end")
+    DSInterval.Value(start, end)
+  }
+  def join(interval1: DSInterval, interval2: DSInterval): DSInterval = interval1.join(interval2)
+  implicit def orderingByTuple[T <: DSInterval]: Ordering[T] =
+    Ordering.by {
+      case DSInterval.Value(start, end) =>
+        (start, end)
+      case _ => (Int.MinValue, Int.MinValue)
+    }
+}