Merge pull request #115 from UQ-PAC/fix-extra-mem-modifies

Propagate modifies clause through boogie program

examples/simplified_http_parse_basic/example.spec

@@ -8,11 +8,11 @@ DIRECT functions: gamma_load64, gamma_load8, memory_load8_le, bvult64, bvule64,
 
 
 Subroutine: #free
-  Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 0bv64)) == true";
-  Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 1bv64)) == true";
-  Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 2bv64)) == true";
-  Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 3bv64)) == true";
-Ensures DIRECT: "Gamma_R0 == true"
+  Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 0bv64)) == true"
+  Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 1bv64)) == true"
+  Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 2bv64)) == true"
+  Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 3bv64)) == true"
+  Ensures DIRECT: "Gamma_R0 == true"
 
 
 Subroutine: main

src/main/scala/boogie/BCmd.scala

@@ -39,7 +39,7 @@ case class BAssume(body: BExpr, comment: Option[String] = None) extends BCmd {
   override def globals: Set[BVar] = body.globals
 }
 
-case class ProcedureCall(name: String, lhss: Seq[BVar], params: Seq[BExpr], comment: Option[String] = None) extends BCmd {
+case class BProcedureCall(name: String, lhss: Seq[BVar], params: Seq[BExpr], comment: Option[String] = None) extends BCmd {
   override def toString: String = {
     if (lhss.isEmpty) {
       s"call $name();"

src/main/scala/boogie/BProgram.scala

@@ -18,7 +18,7 @@ case class BProcedure(
     requiresDirect: List[String],
     freeEnsures: List[BExpr],
     freeRequires: List[BExpr],
-    modifies: Seq[BVar],
+    modifies: Set[BVar],
     body: List[BCmdOrBlock]
 ) extends BDeclaration
     with Ordered[BProcedure] {
@@ -32,7 +32,7 @@ case class BProcedure(
     }
     val semicolon = if body.nonEmpty then "" else ";"
     val modifiesStr = if (modifies.nonEmpty) {
-      List(s"  modifies ${modifies.mkString(", ")};")
+      List(s"  modifies ${modifies.toSeq.sorted.mkString(", ")};")
     } else {
       List()
     }

src/main/scala/translating/IRToBoogie.scala

@@ -52,7 +52,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
       List(),
       List(),
       List(),
-      Seq(mem, Gamma_mem),
+      Set(mem, Gamma_mem),
       guaranteesReflexive.map(g => BAssert(g))
     )
 
@@ -64,7 +64,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     val functionsUsed3 = functionsUsed2.flatMap(p => p.functionOps).map(p => functionOpToDefinition(p))
     val functionsUsed = (functionsUsed2 ++ functionsUsed3).toList.sorted
 
-    val declarations = globalDecls ++ globalConsts ++ functionsUsed ++ rgProcs ++ procedures
+    val declarations = globalDecls ++ globalConsts ++ functionsUsed ++ pushUpModifiesFixedPoint(rgProcs ++ procedures)
     BProgram(declarations)
   }
 
@@ -82,9 +82,9 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     } else {
       reliesUsed
     }
-    val relyProc = BProcedure("rely", List(), List(), relyEnsures, List(), List(), List(), readOnlyMemory, List(), Seq(mem, Gamma_mem), List())
-    val relyTransitive = BProcedure("rely_transitive", List(), List(), reliesUsed, List(), List(), List(), List(), List(), Seq(mem, Gamma_mem), List(ProcedureCall("rely", List(), List()), ProcedureCall("rely", List(), List())))
-    val relyReflexive = BProcedure("rely_reflexive", List(), List(), List(), List(), List(), List(), List(), List(), Seq(), reliesReflexive.map(r => BAssert(r)))
+    val relyProc = BProcedure("rely", List(), List(), relyEnsures, List(), List(), List(), readOnlyMemory, List(), Set(mem, Gamma_mem), List())
+    val relyTransitive = BProcedure("rely_transitive", List(), List(), reliesUsed, List(), List(), List(), List(), List(), Set(mem, Gamma_mem), List(BProcedureCall("rely", List(), List()), BProcedureCall("rely", List(), List())))
+    val relyReflexive = BProcedure("rely_reflexive", List(), List(), List(), List(), List(), List(), List(), List(), Set(), reliesReflexive.map(r => BAssert(r)))
     List(relyProc, relyTransitive, relyReflexive)
   }
 
@@ -217,14 +217,48 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     }
   }
 
+  def pushUpModifiesFixedPoint(procedures: List[BProcedure]): List[BProcedure] = {
+    pushUpModifies(procedures) match {
+      case (true, proc) => pushUpModifiesFixedPoint(proc)
+      case (false, proc) => proc
+    }
+  }
+
+  def pushUpModifies(procedures: List[BProcedure]): (Boolean, List[BProcedure]) = {
+    var changed = false
+
+    val procs: List[BProcedure] = procedures.map(
+      procedure => {
+        val cmds: List[BCmd] = procedure.body.flatten {
+          case b: BBlock => b.body
+          case c: BCmd => Seq(c)
+        }
+
+        val modifies: Set[BVar] = procedure.modifies ++ cmds.collect{ case x: BProcedureCall => procedures.find(_.name == x.name)}
+          .flatten.flatMap(_.modifies)
+
+        if (procedure.modifies != procedure.modifies)
+          changed = true
+
+        procedure.copy(modifies = modifies)
+      }
+    )
+    (changed, procs)
+  }
+
+
   def translateProcedure(p: Procedure, readOnlyMemory: List[BExpr]): BProcedure = {
     val body = p.blocks.map(b => translateBlock(b))
-    // TODO don't hardcode Seq(mem, Gamma_mem) but this is necessary to work with adding rely() calls for now
-    val modifies: Seq[BVar] = {Seq(mem, Gamma_mem) ++ p.modifies
+
+    val callsRely: Boolean = body.flatten(_.body).exists(_ match
+      case BProcedureCall("rely", lhs, params, comment) => true
+      case _ => false)
+
+    val modifies: Seq[BVar] = p.modifies.toSeq
       .flatMap {
         case m: Memory   => Seq(m.toBoogie, m.toGamma)
         case r: Register => Seq(r.toBoogie, r.toGamma)
-      }}.distinct.sorted
+      }.distinct.sorted
 
     val modifiedPreserve = modifies.collect { case m: BVar if modifiedCheck.contains(m) => m }
     val modifiedPreserveEnsures: List[BExpr] = modifiedPreserve.map(m => BinaryBExpr(BoolEQ, m, Old(m))).toList
@@ -253,7 +287,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
       procRequiresDirect,
       freeEnsures,
       freeRequires,
-      modifies,
+      modifies.toSet,
       body.toList
     )
   }
@@ -278,7 +312,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
 
   def translate(j: Jump): List[BCmd] = j match {
     case d: DirectCall =>
-      val call = List(ProcedureCall(d.target.name, List(), List()))
+      val call = List(BProcedureCall(d.target.name, List(), List()))
       val returnTarget = d.returnTarget match {
         case Some(r) => List(GoToCmd(r.label))
         case None    => List(Comment("no return target"), BAssume(FalseBLiteral))
@@ -331,7 +365,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
       if (lhs == stack) {
         List(store)
       } else {
-        val rely = ProcedureCall("rely", List(), List())
+        val rely = BProcedureCall("rely", List(), List())
         val gammaValueCheck = BAssert(BinaryBExpr(BoolIMPLIES, L(lhs, rhs.index), m.rhs.value.toGamma))
         val oldAssigns =
           guaranteeOldVars.map(g => AssignCmd(g.toOldVar, BMemoryLoad(lhs, g.toAddrVar, Endian.LittleEndian, g.size)))
@@ -365,7 +399,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
         List(assign)
       } else {
         val memories = loads.map(m => m.memory).toSeq.sorted
-        List(ProcedureCall("rely", Seq(), Seq()), assign)
+        List(BProcedureCall("rely", Seq(), Seq()), assign)
       }
     case a: Assert =>
       val body = a.body.toBoogie

src/test/correct/arrays_simple/clang/arrays_simple.expected

@@ -33,7 +33,7 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns
 
 function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
 procedure rely();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
   free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
@@ -74,7 +74,7 @@ procedure rely();
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
 procedure rely_transitive()
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
 {
@@ -85,10 +85,10 @@ procedure rely_transitive()
 procedure rely_reflexive();
 
 procedure guarantee_reflexive();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
 
 procedure main()
-  modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_mem, Gamma_stack, R0, R31, R8, mem, stack;
+  modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
   free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69666bv64) == 0bv8);

src/test/correct/arrays_simple/clang_O2/arrays_simple.expected

@@ -9,7 +9,7 @@ function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
 }
 
 procedure rely();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
   free ensures (memory_load8_le(mem, 1840bv64) == 1bv8);
@@ -50,7 +50,7 @@ procedure rely();
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
 procedure rely_transitive()
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
 {
@@ -61,10 +61,10 @@ procedure rely_transitive()
 procedure rely_reflexive();
 
 procedure guarantee_reflexive();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
 
 procedure main()
-  modifies Gamma_R0, Gamma_mem, R0, mem;
+  modifies Gamma_R0, R0;
   free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69666bv64) == 0bv8);

src/test/correct/arrays_simple/clang_no_plt_no_pic/arrays_simple.expected

@@ -33,7 +33,7 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns
 
 function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
 procedure rely();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
   free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
@@ -74,7 +74,7 @@ procedure rely();
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
 procedure rely_transitive()
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
 {
@@ -85,10 +85,10 @@ procedure rely_transitive()
 procedure rely_reflexive();
 
 procedure guarantee_reflexive();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
 
 procedure main()
-  modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_mem, Gamma_stack, R0, R31, R8, mem, stack;
+  modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
   free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69666bv64) == 0bv8);

src/test/correct/arrays_simple/clang_pic/arrays_simple.expected

@@ -33,7 +33,7 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns
 
 function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
 procedure rely();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
   free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
@@ -74,7 +74,7 @@ procedure rely();
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
 procedure rely_transitive()
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
 {
@@ -85,10 +85,10 @@ procedure rely_transitive()
 procedure rely_reflexive();
 
 procedure guarantee_reflexive();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
 
 procedure main()
-  modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_mem, Gamma_stack, R0, R31, R8, mem, stack;
+  modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
   free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69666bv64) == 0bv8);

src/test/correct/arrays_simple/gcc_O2/arrays_simple.expected

@@ -9,7 +9,7 @@ function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
 }
 
 procedure rely();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
   free ensures (memory_load8_le(mem, 1896bv64) == 1bv8);
@@ -50,7 +50,7 @@ procedure rely();
   free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);
 
 procedure rely_transitive()
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
 {
@@ -61,10 +61,10 @@ procedure rely_transitive()
 procedure rely_reflexive();
 
 procedure guarantee_reflexive();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
 
 procedure main()
-  modifies Gamma_R0, Gamma_mem, R0, mem;
+  modifies Gamma_R0, R0;
   free requires (memory_load8_le(mem, 69632bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69633bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69634bv64) == 0bv8);

src/test/correct/basic_arrays_read/clang/basic_arrays_read.expected

@@ -37,7 +37,7 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns
 
 function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
 procedure rely();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
   ensures (old(memory_load32_le(mem, bvadd64($arr_addr, 0bv64))) == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
   free ensures (memory_load8_le(mem, 1860bv64) == 1bv8);
@@ -78,7 +78,7 @@ procedure rely();
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
 procedure rely_transitive()
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (old(memory_load32_le(mem, bvadd64($arr_addr, 0bv64))) == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
 {
   call rely();
@@ -91,7 +91,7 @@ procedure rely_reflexive()
 }
 
 procedure guarantee_reflexive()
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
 {
   assert true;
 }

src/test/correct/basic_arrays_read/clang_O2/basic_arrays_read.expected

@@ -28,7 +28,7 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns
 }
 
 procedure rely();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
   ensures (old(memory_load32_le(mem, bvadd64($arr_addr, 0bv64))) == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
   free ensures (memory_load8_le(mem, 1848bv64) == 1bv8);
@@ -69,7 +69,7 @@ procedure rely();
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
 procedure rely_transitive()
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (old(memory_load32_le(mem, bvadd64($arr_addr, 0bv64))) == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
 {
   call rely();
@@ -82,7 +82,7 @@ procedure rely_reflexive()
 }
 
 procedure guarantee_reflexive()
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
 {
   assert true;
 }

src/test/correct/basic_arrays_read/clang_no_plt_no_pic/basic_arrays_read.expected

@@ -37,7 +37,7 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns
 
 function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
 procedure rely();
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
   ensures (old(memory_load32_le(mem, bvadd64($arr_addr, 0bv64))) == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
   free ensures (memory_load8_le(mem, 1860bv64) == 1bv8);
@@ -78,7 +78,7 @@ procedure rely();
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
 procedure rely_transitive()
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
   ensures (old(memory_load32_le(mem, bvadd64($arr_addr, 0bv64))) == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
 {
   call rely();
@@ -91,7 +91,7 @@ procedure rely_reflexive()
 }
 
 procedure guarantee_reflexive()
-  modifies mem, Gamma_mem;
+  modifies Gamma_mem, mem;
 {
   assert true;
 }