Merge pull request #231 from UQ-PAC/yousif-fixMemoryInjection

Adding Memory Regions to IR

examples/one_function_multi_call/one_function_multi_call.c

@@ -0,0 +1,23 @@
+#include <stdio.h>
+
+// Function declarations
+int addNumbers(int a, int b);
+
+int callAddFromAnotherFunction(int x, int y) {
+    return addNumbers(x, y);
+}
+
+int callFromFun2(int x, int y) {
+    return addNumbers(x, y);
+}
+
+int addNumbers(int a, int b) {
+    return a + b;
+}
+
+int main() {
+    int resultFromMain = addNumbers(10, 5);
+    int resultFromOtherFunc = callAddFromAnotherFunction(20, 15);
+    int resultFromFun2 = callFromFun2(30, 25);
+    return 0;
+}

src/main/scala/Main.scala

@@ -49,7 +49,9 @@ object Main {
       @arg(name = "threads", short = 't', doc = "Separates threads into multiple .bpl files with given output filename as prefix (requires --analyse flag)")
       threadSplit: Flag,
       @arg(name = "summarise-procedures", doc = "Generates summaries of procedures which are used in pre/post-conditions (requires --analyse flag)")
-      summariseProcedures: Flag
+      summariseProcedures: Flag,
+      @arg(name = "memory-regions", doc = "Performs static analysis to separate memory into discrete regions in Boogie output (requires --analyse flag)")
+      memoryRegions: Flag
   )
 
   def main(args: Array[String]): Unit = {
@@ -82,7 +84,7 @@ object Main {
     val q = BASILConfig(
       loading = ILLoadingConfig(conf.inputFileName, conf.relfFileName, conf.specFileName, conf.dumpIL, conf.mainProcedureName, conf.procedureDepth),
       runInterpret = conf.interpret.value,
-      staticAnalysis = if conf.analyse.value then Some(StaticAnalysisConfig(conf.dumpIL, conf.analysisResults, conf.analysisResultsDot, conf.threadSplit.value, conf.summariseProcedures.value)) else None,
+      staticAnalysis = if conf.analyse.value then Some(StaticAnalysisConfig(conf.dumpIL, conf.analysisResults, conf.analysisResultsDot, conf.threadSplit.value, conf.summariseProcedures.value, conf.memoryRegions.value)) else None,
       boogieTranslation = BoogieGeneratorConfig(if conf.lambdaStores.value then BoogieMemoryAccessMode.LambdaStoreSelect else BoogieMemoryAccessMode.SuccessiveStoreSelect,
         true, rely, conf.threadSplit.value),
       outputPrefix = conf.outFileName,

src/main/scala/analysis/Analysis.scala

@@ -32,9 +32,9 @@ trait ConstantPropagation(val program: Program) {
 
   /** Default implementation of eval.
     */
-  def eval(exp: Expr, env: Map[Variable, FlatElement[BitVecLiteral]]): FlatElement[BitVecLiteral] =
+  def eval(exp: Expr, env: Map[Variable, FlatElement[BitVecLiteral]]): FlatElement[BitVecLiteral] = {
     import valuelattice._
-    exp match
+    exp match {
       case id: Variable => env(id)
       case n: BitVecLiteral => bv(n)
       case ze: ZeroExtend => zero_extend(ze.extension, eval(ze.body, env))
@@ -43,7 +43,7 @@ trait ConstantPropagation(val program: Program) {
       case bin: BinaryExpr =>
         val left = eval(bin.arg1, env)
         val right = eval(bin.arg2, env)
-        bin.op match
+        bin.op match {
           case BVADD => bvadd(left, right)
           case BVSUB => bvsub(left, right)
           case BVMUL => bvmul(left, right)
@@ -63,28 +63,29 @@ trait ConstantPropagation(val program: Program) {
           case BVASHR => bvashr(left, right)
           case BVCOMP => bvcomp(left, right)
           case BVCONCAT => concat(left, right)
-
+        }
       case un: UnaryExpr =>
         val arg = eval(un.arg, env)
-
-        un.op match
+        un.op match {
           case BVNOT => bvnot(arg)
           case BVNEG => bvneg(arg)
-
+        }
       case _ => valuelattice.top
+    }
+  }
+
 
   /** Transfer function for state lattice elements.
     */
-  def localTransfer(n: CFGPosition, s: Map[Variable, FlatElement[BitVecLiteral]]): Map[Variable, FlatElement[BitVecLiteral]] =
-    n match
-      case r: Command =>
-        r match
-          // assignments
-          case la: Assign =>
-            s + (la.lhs -> eval(la.rhs, s))
-          // all others: like no-ops
-          case _ => s
+  def localTransfer(n: CFGPosition, s: Map[Variable, FlatElement[BitVecLiteral]]): Map[Variable, FlatElement[BitVecLiteral]] = {
+    n match {
+      // assignments
+      case la: Assign =>
+        s + (la.lhs -> eval(la.rhs, s))
+      // all others: like no-ops
       case _ => s
+    }
+  }
 
   /** The analysis lattice.
     */
@@ -99,9 +100,10 @@ trait ConstantPropagation(val program: Program) {
 
 class ConstantPropagationSolver(program: Program) extends ConstantPropagation(program)
     with SimplePushDownWorklistFixpointSolver[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]], MapLattice[Variable, FlatElement[BitVecLiteral], ConstantPropagationLattice]]
-    with IRIntraproceduralForwardDependencies
+    with IRInterproceduralForwardDependencies
     with Analysis[Map[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]]]]
 
+
 /** Base class for value analysis with simple (non-lifted) lattice.
  */
 trait ConstantPropagationWithSSA(val program: Program, val reachingDefs: Map[CFGPosition, (Map[Variable, Set[Assign]], Map[Variable, Set[Assign]])]) {
@@ -114,9 +116,9 @@ trait ConstantPropagationWithSSA(val program: Program, val reachingDefs: Map[CFG
 
   /** Default implementation of eval.
    */
-  def eval(exp: Expr, env: Map[RegisterWrapperEqualSets, Set[BitVecLiteral]], n: CFGPosition): Set[BitVecLiteral] =
+  def eval(exp: Expr, env: Map[RegisterWrapperEqualSets, Set[BitVecLiteral]], n: CFGPosition): Set[BitVecLiteral] = {
     import valuelattice._
-    exp match
+    exp match {
       case id: Variable => env(RegisterWrapperEqualSets(id, getUse(id, n, reachingDefs)))
       case n: BitVecLiteral => bv(n)
       case ze: ZeroExtend => zero_extend(ze.extension, eval(ze.body, env, n))
@@ -125,7 +127,7 @@ trait ConstantPropagationWithSSA(val program: Program, val reachingDefs: Map[CFG
       case bin: BinaryExpr =>
         val left = eval(bin.arg1, env, n)
         val right = eval(bin.arg2, env, n)
-        bin.op match
+        bin.op match {
           case BVADD => bvadd(left, right)
           case BVSUB => bvsub(left, right)
           case BVMUL => bvmul(left, right)
@@ -145,34 +147,31 @@ trait ConstantPropagationWithSSA(val program: Program, val reachingDefs: Map[CFG
           case BVASHR => bvashr(left, right)
           case BVCOMP => bvcomp(left, right)
           case BVCONCAT => concat(left, right)
+        }
 
       case un: UnaryExpr =>
         val arg = eval(un.arg, env, n)
-
-        un.op match
+        un.op match {
           case BVNOT => bvnot(arg)
           case BVNEG => bvneg(arg)
+        }
 
       case _ => Set.empty
+    }
+  }
 
   /** Transfer function for state lattice elements.
    */
   def localTransfer(n: CFGPosition, s: Map[RegisterWrapperEqualSets, Set[BitVecLiteral]]): Map[RegisterWrapperEqualSets, Set[BitVecLiteral]] =
     n match {
-      case r: Command =>
-        r match {
-          // assignments
-          case a: Assign =>
-            val lhsWrappers = s.collect {
-              case (k, v) if RegisterVariableWrapper(k.variable, k.assigns) == RegisterVariableWrapper(a.lhs, getDefinition(a.lhs, r, reachingDefs)) => (k, v)
-            }
-            if (lhsWrappers.nonEmpty) {
-              s ++ lhsWrappers.map((k, v) => (k, v.union(eval(a.rhs, s, r))))
-            } else {
-              s + (RegisterWrapperEqualSets(a.lhs, getDefinition(a.lhs, r, reachingDefs)) -> eval(a.rhs, s, n))
-            }
-          // all others: like no-ops
-          case _ => s
+      case a: Assign =>
+        val lhsWrappers = s.collect {
+          case (k, v) if RegisterVariableWrapper(k.variable, k.assigns) == RegisterVariableWrapper(a.lhs, getDefinition(a.lhs, a, reachingDefs)) => (k, v)
+        }
+        if (lhsWrappers.nonEmpty) {
+          s ++ lhsWrappers.map((k, v) => (k, v.union(eval(a.rhs, s, a))))
+        } else {
+          s + (RegisterWrapperEqualSets(a.lhs, getDefinition(a.lhs, a, reachingDefs)) -> eval(a.rhs, s, n))
         }
       case _ => s
     }
@@ -190,5 +189,5 @@ trait ConstantPropagationWithSSA(val program: Program, val reachingDefs: Map[CFG
 
 class ConstantPropagationSolverWithSSA(program: Program, reachingDefs: Map[CFGPosition, (Map[Variable, Set[Assign]], Map[Variable, Set[Assign]])]) extends ConstantPropagationWithSSA(program, reachingDefs)
   with SimplePushDownWorklistFixpointSolver[CFGPosition, Map[RegisterWrapperEqualSets, Set[BitVecLiteral]], MapLattice[RegisterWrapperEqualSets, Set[BitVecLiteral], ConstantPropagationLatticeWithSSA]]
-  with IRIntraproceduralForwardDependencies
+  with IRInterproceduralForwardDependencies
   with Analysis[Map[CFGPosition, Map[RegisterWrapperEqualSets, Set[BitVecLiteral]]]]

src/main/scala/analysis/BitVectorEval.scala

@@ -1,7 +1,8 @@
 package analysis
-import ir._
+import ir.*
 import analysis.BitVectorEval.*
 
+import scala.annotation.tailrec
 import scala.math.pow
 
 object BitVectorEval {
@@ -337,5 +338,4 @@ object BitVectorEval {
       smt_zero_extend(i, s)
     }
   }
-
 }