Merge branch 'main' into function-summaries

# Conflicts:
#	src/test/scala/SystemTests.scala

.github/workflows/run-examples.yml

@@ -46,10 +46,32 @@ jobs:
 
       - name: System Tests
         run: ./mill test.testOnly '*SystemTests*' || true
-
       - uses: actions/upload-artifact@v4
         with:
           name: testresult-${{ github.run_number }}
-          path: src/test/*.csv
+          path: |
+            src/test/*.csv
+            src/test/*.svg
+      - run: |
+          pushd src/test
+          tail -n+1 summary-*.csv
+          pasted="$(paste headers.md.part summary-*.md.part)"
+          for part in summary-*.md.part; do
+            # basename, then everything after "summary-", then everything before ".md.part" (via two rev passes)
+            testname="$(basename $part | cut -d- -f2- | rev | cut -d. -f3- | rev)"
+            [[ -n "$testname" ]]
+
+            svg="verifyTime-$testname.svg"
+            ls -l "$svg"
+
+            # 1920 hours = 80 days
+            url="$(curl -F"file=@$svg" -Fexpires=1920 http://0x0.st)"
+            [[ -n "$url" ]]
+
+            pasted="$(echo "$pasted" | sed "s#HISTO${testname}HISTO#$url#g")"
+          done
+          popd
+
+          echo "$pasted" > $GITHUB_STEP_SUMMARY
+        shell: "bash -xe {0}"
 
-      - run: tail -n+1 src/test/summary-*.csv

.gitignore

@@ -23,4 +23,7 @@ examplesold/
 src/test/scala/dump/
 src/test/analysis/dump/
 *.gtirb
-*.json
+*.json
+src/test/*.svg
+src/test/*.md.part
+src/test/summary-*.md

readme.md

@@ -35,13 +35,21 @@ Boogie program verifier finished with 4 verified, 0 errors
 
 The tool takes as inputs either a BAP ADT file (here denoted with `.adt`) or a `.gts` file produced by [gtirb-semantics](https://github.com/UQ-PAC/gtirb-semantics), as well as a file containing the output of readelf (here denoted with `.relf`), both created from the same AArch64/ARM64 binary, and outputs a semantically equivalent .bpl Boogie-language source file. The default output file is `boogie_out.bpl`, but the output location can be specified.
 
-To build and run the tool using sbt, use the following command:
+To build and run the tool use one of the the following commands:
 
-`sbt "run --input file.{adt, gts} --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]"` where the output filename is optional and specification filenames are optional. The specification filename must end in `.spec`.
-
-or mill:
-
-`mill run --input file.adt --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]`.
+sbt:
+```
+sbt "run --input file.{adt, gts} --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]"
+```
+mill (Mac OS X / Linux):
+```
+./mill run --input file.adt --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]
+```
+mill (Windows): 
+```
+./mill.bat run --input file.adt --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]
+```
+The output filename is optional and specification filenames are optional. The specification filename must end in `.spec`.
 
 #### Usage
 
@@ -82,9 +90,14 @@ See [docs/development](docs/development)
 2. Install [boogie](/docs/development/tool-installation.md)
 3. To a single system test case :
 
+Mac OS X / Linux: 
 ```
 ./mill test.testOnly '*SystemTests*' -- -z secret_write -z secret_write 
 ```
+Windows:
+```
+./mill.bat test.testOnly '*SystemTests*' -- -z secret_write -z secret_write 
+```
 
 ## Open Source License
 

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/main/scala/util/RunUtils.scala

@@ -437,21 +437,29 @@ object IRTransform {
               val procedure = c.parent.data
               val newBlocks = ArrayBuffer[Block]()
               // indirectCall.parent.parent.removeBlocks(indirectCall.returnTarget)
+              var addressExprs = List[BinaryExpr]()
               for (t <- targets) {
                 Logger.debug(targets)
+                // TODO handle external procedures without a set address but this requires more information than the analysis gives at present
                 val address = t.address.match {
                   case Some(a) => a
                   case None => throw Exception(s"resolved indirect call $indirectCall to procedure which does not have address: $t")
                 }
-                val assume = Assume(BinaryExpr(BVEQ, indirectCall.target, BitVecLiteral(address, 64)))
+                val addressExpr = BinaryExpr(BVEQ, indirectCall.target, BitVecLiteral(address, 64))
+                addressExprs ::= addressExpr
+                val assume = Assume(addressExpr)
                 val newLabel: String = block.label + t.name
                 val directCall = DirectCall(t, indirectCall.returnTarget)
                 directCall.parent = indirectCall.parent
-
                 newBlocks.append(Block(newLabel, None, ArrayBuffer(assume), directCall))
               }
               procedure.addBlocks(newBlocks)
               val newCall = GoTo(newBlocks, indirectCall.label)
+              val addressExprOr = addressExprs.tail.foldLeft(addressExprs.head) {
+                (a: BinaryExpr, b: BinaryExpr) => BinaryExpr(BoolOR, a, b)
+              }
+              val assert = Assert(addressExprOr, Some("check indirect call underapproximation"))
+              block.statements.append(assert)
               block.replaceJump(newCall)
             }
           case _ =>

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;
+}
+