Merge branch 'main' into memory-consolidation

.github/workflows/run-examples.yml

@@ -10,7 +10,6 @@ on:
 jobs:
   CompileAndTest:
     runs-on: ubuntu-latest
-    timeout-minutes: 10 
     container:
       # Requires repo to have action access in package settings
       image: ghcr.io/uq-pac/basil-dev:latest
@@ -28,14 +27,13 @@ jobs:
         run: ./mill test.testOnly BitVectorAnalysisTests
 
       - name: IntrusiveListTest
-        run: ./mill test.testOnly IntrusiveListPublicInterfaceTests
+        run: ./mill test.testOnly '*IntrusiveListPublicInterfaceTest'
 
       - name: System Tests
         run: ./mill test.testOnly *SystemTests -- -z basic_assign_increment/gcc_no_plt_no_pic -z basic_assign_increment/clang_no_plt_no_pic -z secret_write/gcc_no_plt_no_pic
 
   SystemTests:
     runs-on: ubuntu-latest
-    timeout-minutes: 10 
     container:
       # Requires repo to have action access in package settings
       image: ghcr.io/uq-pac/basil-dev:latest
@@ -47,4 +45,11 @@ jobs:
         uses: actions/checkout@v4
 
       - name: System Tests
-        run: ./mill test.testOnly SystemTests || true
+        run: ./mill test.testOnly '*SystemTests*' || true
+
+      - uses: actions/upload-artifact@v4
+        with:
+          name: testresult-${{ github.run_number }}
+          path: src/test/*.csv
+
+      - run: tail -n+1 src/test/summary-*.csv

build.sbt

@@ -54,7 +54,7 @@ updateExpectedBAP := {
         val name = e.getName
         val outPath = v / (name + "_bap.bpl")
         val expectedPath = v / (name + ".expected")
-        val resultPath = v / (name + "_result.txt")
+        val resultPath = v / (name + "_bap_result.txt")
         if (resultPath.exists()) {
           val result = IO.read(resultPath)
           val verified = result.strip().equals("Boogie program verifier finished with 0 errors")
@@ -96,3 +96,61 @@ updateExpectedBAP := {
   expectedUpdate(correctPath, true)
   expectedUpdate(incorrectPath, false)
 }
+
+lazy val updateExpectedGTIRB = taskKey[Unit]("updates .expected for GTIRB test cases")
+
+updateExpectedGTIRB := {
+  val correctPath = baseDirectory.value / "src" / "test" / "correct"
+  val incorrectPath = baseDirectory.value / "src" / "test" / "incorrect"
+
+  def expectedUpdate(path: File, shouldVerify: Boolean): Unit = {
+    val log = streams.value.log
+    val examples = (path * "*") filter { _.isDirectory }
+    for (e <- examples.get()) {
+      val variations = (e * "*") filter { _.isDirectory }
+      for (v <- variations.get()) {
+        val name = e.getName
+        val outPath = v / (name + "_gtirb.bpl")
+        val expectedPath = v / (name + "_gtirb.expected")
+        val resultPath = v / (name + "_gtirb_result.txt")
+        if (resultPath.exists()) {
+          val result = IO.read(resultPath)
+          val verified = result.strip().equals("Boogie program verifier finished with 0 errors")
+          if (verified == shouldVerify) {
+            if (outPath.exists() && !(expectedPath.exists() && filesContentEqual(outPath, expectedPath))) {
+              IO.copyFile(outPath, expectedPath)
+            }
+          }
+        }
+      }
+    }
+  }
+
+  def filesContentEqual(path1: File, path2: File): Boolean = {
+    val source1 = Source.fromFile(path1)
+    val source2 = Source.fromFile(path2)
+    val lines1 = source1.getLines
+    val lines2 = source2.getLines
+    while (lines1.hasNext && lines2.hasNext) {
+      val line1 = lines1.next()
+      val line2 = lines2.next()
+      if (line1 != line2) {
+        source1.close
+        source2.close
+        return false
+      }
+    }
+    if (lines1.hasNext || lines2.hasNext) {
+      source1.close
+      source2.close
+      return false
+    }
+
+    source1.close
+    source2.close
+    true
+  }
+
+  expectedUpdate(correctPath, true)
+  expectedUpdate(incorrectPath, false)
+}

build.sc

@@ -46,39 +46,58 @@ object basil extends RootModule with ScalaModule with antlr.AntlrModule with Sca
   /**
    * Updates the expected
    */
-  def updateExpected() = T.command {
-    val correctPath = test.millSourcePath /  "correct"
+
+  def updateExpectedBAP() = T.command {
+    val correctPath = test.millSourcePath / "correct"
+    val incorrectPath = test.millSourcePath / "incorrect"
+
+    expectedUpdate(correctPath, true, true)
+    expectedUpdate(incorrectPath, false, true)
+  }
+
+  def updateExpectedGTIRB() = T.command {
+    val correctPath = test.millSourcePath / "correct"
     val incorrectPath = test.millSourcePath / "incorrect"
 
-    def expectedUpdate(path: Path, shouldVerify: Boolean): Unit = {
-      val examples = os.list(path).filter(os.isDir)
-      for (e <- examples) {
-        val variations = os.list(e).filter(os.isDir)
-        for (v <- variations) {
-          val name = e.last
-          val outPath = v / (name + ".bpl")
-          val expectedPath = v / (name + ".expected")
-          val resultPath = v / (name + "_result.txt")
-          if (os.exists(resultPath)) {
-            val result = os.read(resultPath)
-            val verified = result.strip().equals("Boogie program verifier finished with 0 errors")
-            if (verified == shouldVerify) {
-              if (os.exists(outPath) && !(os.exists(expectedPath) && filesContentEqual(outPath, expectedPath))) {
-                println(s"updated $expectedPath")
-                os.copy.over(outPath, expectedPath)
-              }
+    expectedUpdate(correctPath, true, false)
+    expectedUpdate(incorrectPath, false, false)
+  }
+
+  def expectedUpdate(path: Path, shouldVerify: Boolean, BAPVariant: Boolean): Unit = {
+    val examples = os.list(path).filter(os.isDir)
+    for (e <- examples) {
+      val variations = os.list(e).filter(os.isDir)
+      for (v <- variations) {
+        val name = e.last
+        val suffix = if (BAPVariant) {
+          "_bap"
+        } else {
+          "_gtirb"
+        }
+        val expectedSuffix = if (BAPVariant) {
+          ""
+        } else {
+          "_gtirb"
+        }
+        val outPath = v / (name + suffix + ".bpl")
+        val expectedPath = v / (name + expectedSuffix + ".expected")
+        val resultPath = v / (name + suffix + "_result.txt")
+        if (os.exists(resultPath)) {
+          val result = os.read(resultPath)
+          val verified = result.strip().equals("Boogie program verifier finished with 0 errors")
+          if (verified == shouldVerify) {
+            if (os.exists(outPath) && !(os.exists(expectedPath) && filesContentEqual(outPath, expectedPath))) {
+              println(s"updated $expectedPath")
+              os.copy.over(outPath, expectedPath)
             }
           }
         }
       }
     }
+  }
 
-    def filesContentEqual(path1: Path, path2: Path): Boolean = {
-      os.read(path1) == os.read(path2)
-    }
-
-    expectedUpdate(correctPath, true)
-    expectedUpdate(incorrectPath, false)
+  def filesContentEqual(path1: Path, path2: Path): Boolean = {
+    os.read.lines(path1) == os.read.lines(path2)
   }
 
 }