Merge branch 'main' into il-cfg-iterator

UQ-PAC · Nov 28, 2023 · 465a49e · 465a49e
2 parents ddb0269 + 53a2647
commit 465a49e
Show file tree

Hide file tree

Showing 14 changed files with 707 additions and 1,234 deletions.
diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
diff --git a/src/main/scala/analysis/BasicIRConstProp.scala b/src/main/scala/analysis/BasicIRConstProp.scala
@@ -1,17 +1,16 @@
 package analysis
 import ir.*
-
 import analysis.solvers.*
 
 trait ILValueAnalysisMisc:
-  val valuelattice: LatticeWithOps
-  val statelattice: MapLattice[Variable, valuelattice.type] = new MapLattice(valuelattice)
+  val valuelattice: ConstantPropagationLattice = ConstantPropagationLattice()
+  val statelattice: MapLattice[Variable, FlatElement[BitVecLiteral], ConstantPropagationLattice] = MapLattice(valuelattice)
 
   def eval(exp: Expr, env: statelattice.Element): valuelattice.Element =
     import valuelattice._
     exp match
       case id: Variable   => env(id)
-      case n: Literal     => literal(n)
+      case n: BitVecLiteral     => bv(n)
       case ze: ZeroExtend => zero_extend(ze.extension, eval(ze.body, env))
       case se: SignExtend => sign_extend(se.extension, eval(se.body, env))
       case e: Extract     => extract(e.end, e.start, eval(e.body, env))
@@ -37,20 +36,21 @@ trait ILValueAnalysisMisc:
           case BVLSHR => bvlshr(left, right)
           case BVASHR => bvashr(left, right)
           case BVCOMP => bvcomp(left, right)
+          case BVCONCAT => concat(left, right)
 
-          case BVULE => bvule(left, right)
-          case BVUGE => bvuge(left, right)
-          case BVULT => bvult(left, right)
-          case BVUGT => bvugt(left, right)
+          //case BVULE => bvule(left, right)
+          //case BVUGE => bvuge(left, right)
+          //case BVULT => bvult(left, right)
+          //case BVUGT => bvugt(left, right)
 
-          case BVSLE => bvsle(left, right)
-          case BVSGE => bvsge(left, right)
-          case BVSLT => bvslt(left, right)
-          case BVSGT => bvsgt(left, right)
+          //case BVSLE => bvsle(left, right)
+          //case BVSGE => bvsge(left, right)
+          //case BVSLT => bvslt(left, right)
+          //case BVSGT => bvsgt(left, right)
 
-          case BVCONCAT => concat(left, right)
-          case BVNEQ    => bvneq(left, right)
-          case BVEQ     => bveq(left, right)
+          //case BVCONCAT => concat(left, right)
+          //case BVNEQ    => bvneq(left, right)
+          //case BVEQ     => bveq(left, right)
 
       case un: UnaryExpr =>
         val arg = eval(un.arg, env)
@@ -76,14 +76,16 @@ trait ILValueAnalysisMisc:
 type IRNode = IntraProcIRCursor.Node
 
 object IRSimpleValueAnalysis:
-  class Solver[+L <: LatticeWithOps](prog: Program, val valuelattice: L) extends FlowSensitiveAnalysis(true)
+  class Solver(prog: Program) extends ILValueAnalysisMisc
     with IntraProcDependencies
-    with Dependencies[IRNode](true)
-    with ILValueAnalysisMisc
-    with SimplePushDownWorklistFixpointSolver[IRNode]
+    with Dependencies[IRNode]
+    with Analysis[Map[IRNode, Map[Variable, FlatElement[BitVecLiteral]]]]
+    //with SimplePushDownWorklistFixpointSolver[IRNode]
+    with SimplePushDownWorklistFixpointSolver[IRNode, Map[Variable, FlatElement[BitVecLiteral]], MapLattice[Variable, FlatElement[BitVecLiteral], ConstantPropagationLattice]]
     :
       /* Worklist initial set */
-      override val lattice: MapLattice[IRNode, statelattice.type] = MapLattice(statelattice)
+      //override val lattice: MapLattice[IRNode, statelattice.type] = MapLattice(statelattice)
+      override val lattice: MapLattice[IRNode, Map[Variable, FlatElement[BitVecLiteral]], MapLattice[Variable, FlatElement[BitVecLiteral], ConstantPropagationLattice]] = MapLattice(statelattice)
 
       override val domain : Set[IRNode] = computeDomain(prog).toSet
       def transfer(n: IRNode, s: statelattice.Element): statelattice.Element = localTransfer(n, s)