Merge pull request #245 from UQ-PAC/test-cleanup

Tests Cleanup

.github/workflows/run-examples.yml

@@ -29,9 +29,6 @@ jobs:
       - name: IntrusiveListTest
         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
     container:
@@ -45,7 +42,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: System Tests
-        run: ./mill test.testOnly '*SystemTests*' || true
+        run: ./mill test.testOnly 'SystemTests*'
       - uses: actions/upload-artifact@v4
         with:
           name: testresult-${{ github.run_number }}

build.sbt

@@ -44,57 +44,9 @@ lazy val updateExpectedBAP = taskKey[Unit]("updates .expected for BAP test cases
 updateExpectedBAP := {
   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 + "_bap.bpl")
-        val expectedPath = v / (name + ".expected")
-        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")
-          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)
+  val log = streams.value.log
+  expectedUpdate(correctPath, true, true)
+  expectedUpdate(incorrectPath, false, true)
 }
 
 lazy val updateExpectedGTIRB = taskKey[Unit]("updates .expected for GTIRB test cases")
@@ -103,54 +55,81 @@ 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)
-            }
+  val log = streams.value.log
+  expectedUpdate(correctPath, true, false)
+  expectedUpdate(incorrectPath, false, false)
+}
+
+lazy val updateExpectedExtraSpec = taskKey[Unit]("updates .expected for ExtraSpec test cases")
+
+updateExpectedExtraSpec := {
+  val correctPath = baseDirectory.value / "src" / "test" / "extraspec_correct"
+  val incorrectPath = baseDirectory.value / "src" / "test" / "extraspec_incorrect"
+
+  val log = streams.value.log
+  expectedUpdate(correctPath, true, true)
+  expectedUpdate(incorrectPath, false, true)
+  expectedUpdate(correctPath, true, false)
+  expectedUpdate(incorrectPath, false, false)
+}
+
+def expectedUpdate(path: File, shouldVerify: Boolean, BAPVariant: Boolean): Unit = {
+  val examples = (path * "*") filter {
+    _.isDirectory
+  }
+  for (e <- examples.get()) {
+    val variations = (e * "*") filter {
+      _.isDirectory
+    }
+    for (v <- variations.get()) {
+      val name = e.getName
+      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 (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) {
+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
-    true
+    return false
   }
 
-  expectedUpdate(correctPath, true)
-  expectedUpdate(incorrectPath, false)
+  source1.close
+  source2.close
+  true
 }

build.sc

@@ -63,6 +63,15 @@ object basil extends RootModule with ScalaModule with antlr.AntlrModule with Sca
     expectedUpdate(incorrectPath, false, false)
   }
 
+  def updateExpectedExtraSpec() = T.command {
+    val correctPath = test.millSourcePath / "extraspec_correct"
+    val incorrectPath = test.millSourcePath / "extraspec_incorrect"
+    expectedUpdate(correctPath, true, true)
+    expectedUpdate(incorrectPath, false, true)
+    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) {

docs/usage.md

@@ -21,7 +21,7 @@ The steps below describe the dependencies required,
 then the steps to obtain these input files
 and run BASIL.
 
-<!-- These instructions are automated in [lift_adt.sh](../../scripts/lift_adt.sh). -->
+<!-- These instructions are automated in [lift.sh](../../scripts/lift.sh). -->
 
 [tests]: /src/test/correct
 [spec]: /src/test/correct/secret_write/secret_write.spec
@@ -171,13 +171,7 @@ passing the `smt.array.extensional=false` configuration to Z3 through Boogie's C
 boogie example.bpl /proverOpt:O:smt.array.extensional=false
 ```
 
-## Other useful tasks 
-
-To compile a C file without the global offset table being used in address calculation, use the following command:
-
-```bash
-aarch64-linux-gnu-gcc -fno-plt -fno-pic *.c -o *.out
-```
+## Other useful tasks
 
 To produce assembly from the binary, use:
 ```bash
@@ -189,11 +183,6 @@ To view the hex dump of the data section of the binary:
 readelf -x .data *.out
 ```
 
-To compile a C file with the stack guard turned off:
-```bash
-aarch64-linux-gnu-gcc -fno-stack-protector -fno-plt -fno-pic *.c -o *.out
-```
-
 To examine the ASLp semantics of a particular instruction,
 see [ASLp's README](https://github.com/UQ-PAC/aslp?tab=readme-ov-file#using-the-asl-partial-evaluator)
 or [aslp-web](https://katrinafyi.github.io/aslp-web/).