Merge pull request #221 from UQ-PAC/memory-consolidation

Fix issue with memory coalescing

src/main/scala/translating/IRToBoogie.scala

@@ -479,35 +479,71 @@ class IRToBoogie(var program: Program, var spec: Specification, var thread: Opti
 
   private def memoryToCondition(memory: ArrayBuffer[MemorySection]): List[BExpr] = {
 
-    def coalesced(): List[BExpr] = {
+    def coalesced: List[BExpr] = {
       val sections = memory.flatMap { s =>
         // Phrase the memory condition in terms of 64-bit operations, as long as the memory
-        // region is a multiple of such operations and appropriately aligned
-        if (s.address % 8 == 0 && s.bytes.size % 8 == 0) {
-          for (b <- s.bytes.indices by 8) yield {
-            // Combine the byte constants into a 64-bit value
-            val sum: BigInt =
-              (0 until 8).foldLeft(BigInt(0))((x, y) => x + (s.bytes(b + y).value * (BigInt(2).pow(y * 8))))
+        // section's size is a multiple of 64-bits and 64-bits (8 bytes) aligned
+        // If the memory section is not aligned, the initial unaligned part of it will not be coalesced into a 64-bit
+        // representations and remain as an 8-bit representations
+        // If the memory section's size is not a multiple of 64-bits, the last part of it that cannot be coalesced into
+        // a 64-bit representation will remain as an 8-bit representation
+
+        val aligned = s.address % 8
+        val alignedStart = s.address + aligned // first aligned address in the section
+
+        val alignedSizeMultiple = (s.bytes.size - aligned) % 8
+        // index of the byte that marks the end of the part that is a multiple of 64-bits
+        val alignedEnd = s.bytes.size - alignedSizeMultiple
+
+        // Aligned section that is safe to convert to 64-bit values
+        val alignedSection = for (b <- aligned until alignedEnd by 8) yield {
+          // Combine the byte constants into a 64-bit value
+          val combined: BigInt =
+            (0 until 8).foldLeft(BigInt(0))((x, y) => x + (s.bytes(b + y).value * BigInt(2).pow(y * 8)))
+          BinaryBExpr(
+            BVEQ,
+            BMemoryLoad(mem, BitVecBLiteral(s.address + b, 64), Endian.LittleEndian, 64),
+            BitVecBLiteral(combined, 64)
+          )
+        }
+
+        // If memory section is somehow not aligned (is this possible?) then don't convert the initial non-aligned
+        // section to 64-bit operations, just the rest
+        val unalignedStartSection = if (aligned == 0) {
+          Seq()
+        } else {
+          for (b <- 0 until aligned) yield {
             BinaryBExpr(
               BVEQ,
-              BMemoryLoad(mem, BitVecBLiteral(s.address + b, 64), Endian.LittleEndian, 64),
-              BitVecBLiteral(sum, 64)
+              BMemoryLoad(mem, BitVecBLiteral(s.address + b, 64), Endian.LittleEndian, 8),
+              s.bytes(b).toBoogie
             )
           }
+        }
+
+        // If the memory section is not a multiple of 64-bits then don't convert the last section to 64-bits
+        // This is not ideal but will do for now
+        // Ideal solution is to match the sizes based on the sizes listed in the symbol table, dividing further
+        // for values greater than 64-bit as much as possible
+        // But that requires more work
+        // Combine the byte constants into a 64-bit value
+        val unalignedEndSection = if (alignedSizeMultiple == 0) {
+          Seq()
         } else {
-          for (b <- s.bytes.indices) yield {
+          for (b <- alignedEnd until s.bytes.size) yield {
             BinaryBExpr(
               BVEQ,
               BMemoryLoad(mem, BitVecBLiteral(s.address + b, 64), Endian.LittleEndian, 8),
               s.bytes(b).toBoogie
             )
           }
         }
+        unalignedStartSection ++ alignedSection ++ unalignedEndSection
       }
       sections.toList
     }
 
-    def bytes(): List[BExpr] = {
+    def bytes: List[BExpr] = {
       val sections = memory.flatMap { s =>
         for (b <- s.bytes.indices) yield {
           BinaryBExpr(
@@ -520,7 +556,7 @@ class IRToBoogie(var program: Program, var spec: Specification, var thread: Opti
       sections.toList
     }
 
-    if config.coalesceConstantMemory then coalesced() else bytes()
+    if config.coalesceConstantMemory then coalesced else bytes
   }
 
   def captureStateStatement(stateName: String): BAssume = {

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

@@ -0,0 +1,112 @@
+var {:extern} Gamma_R0: bool;
+var {:extern} Gamma_R31: bool;
+var {:extern} Gamma_R8: bool;
+var {:extern} Gamma_mem: [bv64]bool;
+var {:extern} Gamma_stack: [bv64]bool;
+var {:extern} R0: bv64;
+var {:extern} R31: bv64;
+var {:extern} R8: bv64;
+var {:extern} mem: [bv64]bv8;
+var {:extern} stack: [bv64]bv8;
+const {:extern} $_IO_stdin_used_addr: bv64;
+axiom ($_IO_stdin_used_addr == 1872bv64);
+function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function {:extern} gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function {:extern} gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function {:extern} memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function {:extern} memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function {:extern} memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function {:extern} {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure {:extern} rely();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+  free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1873bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1874bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1875bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+procedure {:extern} rely_transitive();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+
+implementation {:extern} rely_transitive()
+{
+  call rely();
+  call rely();
+}
+
+procedure {:extern} rely_reflexive();
+
+procedure {:extern} guarantee_reflexive();
+  modifies Gamma_mem, mem;
+
+procedure main();
+  modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
+  free requires (memory_load64_le(mem, 69664bv64) == 0bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free requires (memory_load8_le(mem, 1872bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1873bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1874bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1875bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free requires (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free requires (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free ensures (Gamma_R31 == old(Gamma_R31));
+  free ensures (R31 == old(R31));
+  free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1873bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1874bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1875bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+implementation main()
+{
+  $main$__0__$hLpmd_ERQq2v3Sj7g4WZPA:
+    assume {:captureState "$main$__0__$hLpmd_ERQq2v3Sj7g4WZPA"} true;
+    R31, Gamma_R31 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
+    R8, Gamma_R8 := 3bv64, true;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 20bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 20bv64), Gamma_R8);
+    assume {:captureState "1820$0"} true;
+    R8, Gamma_R8 := 7bv64, true;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 28bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 28bv64), Gamma_R8);
+    assume {:captureState "1828$0"} true;
+    R8, Gamma_R8 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 20bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 20bv64));
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 8bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 8bv64), Gamma_R8);
+    assume {:captureState "1836$0"} true;
+    R0, Gamma_R0 := 0bv64, true;
+    R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
+    goto main_basil_return;
+  main_basil_return:
+    assume {:captureState "main_basil_return"} true;
+    return;
+}
+

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

@@ -0,0 +1,76 @@
+var {:extern} Gamma_R0: bool;
+var {:extern} Gamma_mem: [bv64]bool;
+var {:extern} R0: bv64;
+var {:extern} mem: [bv64]bv8;
+const {:extern} $_IO_stdin_used_addr: bv64;
+axiom ($_IO_stdin_used_addr == 1840bv64);
+function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function {:extern} memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+procedure {:extern} rely();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+  free ensures (memory_load8_le(mem, 1840bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1841bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1842bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1843bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+procedure {:extern} rely_transitive();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+
+implementation {:extern} rely_transitive()
+{
+  call rely();
+  call rely();
+}
+
+procedure {:extern} rely_reflexive();
+
+procedure {:extern} guarantee_reflexive();
+  modifies Gamma_mem, mem;
+
+procedure main();
+  modifies Gamma_R0, R0;
+  free requires (memory_load64_le(mem, 69664bv64) == 0bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free requires (memory_load8_le(mem, 1840bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1841bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1842bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1843bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free requires (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free requires (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free ensures (memory_load8_le(mem, 1840bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1841bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1842bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1843bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+implementation main()
+{
+  $main$__0__$0qtvkPMtQ8STE6UF8gIq3g:
+    assume {:captureState "$main$__0__$0qtvkPMtQ8STE6UF8gIq3g"} true;
+    R0, Gamma_R0 := 0bv64, true;
+    goto main_basil_return;
+  main_basil_return:
+    assume {:captureState "main_basil_return"} true;
+    return;
+}
+

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

@@ -0,0 +1,112 @@
+var {:extern} Gamma_R0: bool;
+var {:extern} Gamma_R31: bool;
+var {:extern} Gamma_R8: bool;
+var {:extern} Gamma_mem: [bv64]bool;
+var {:extern} Gamma_stack: [bv64]bool;
+var {:extern} R0: bv64;
+var {:extern} R31: bv64;
+var {:extern} R8: bv64;
+var {:extern} mem: [bv64]bv8;
+var {:extern} stack: [bv64]bv8;
+const {:extern} $_IO_stdin_used_addr: bv64;
+axiom ($_IO_stdin_used_addr == 1872bv64);
+function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function {:extern} gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function {:extern} gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function {:extern} memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function {:extern} memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function {:extern} memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function {:extern} {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure {:extern} rely();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+  free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1873bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1874bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1875bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+procedure {:extern} rely_transitive();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+
+implementation {:extern} rely_transitive()
+{
+  call rely();
+  call rely();
+}
+
+procedure {:extern} rely_reflexive();
+
+procedure {:extern} guarantee_reflexive();
+  modifies Gamma_mem, mem;
+
+procedure main();
+  modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
+  free requires (memory_load64_le(mem, 69664bv64) == 0bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free requires (memory_load8_le(mem, 1872bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1873bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1874bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1875bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free requires (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free requires (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free ensures (Gamma_R31 == old(Gamma_R31));
+  free ensures (R31 == old(R31));
+  free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1873bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1874bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1875bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+implementation main()
+{
+  $main$__0__$jW16aKqURYu2YiCzSOvWow:
+    assume {:captureState "$main$__0__$jW16aKqURYu2YiCzSOvWow"} true;
+    R31, Gamma_R31 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
+    R8, Gamma_R8 := 3bv64, true;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 20bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 20bv64), Gamma_R8);
+    assume {:captureState "1820$0"} true;
+    R8, Gamma_R8 := 7bv64, true;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 28bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 28bv64), Gamma_R8);
+    assume {:captureState "1828$0"} true;
+    R8, Gamma_R8 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 20bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 20bv64));
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 8bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 8bv64), Gamma_R8);
+    assume {:captureState "1836$0"} true;
+    R0, Gamma_R0 := 0bv64, true;
+    R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
+    goto main_basil_return;
+  main_basil_return:
+    assume {:captureState "main_basil_return"} true;
+    return;
+}
+