Reproducible Docker build for test cases in src/test

.gitattributes

@@ -0,0 +1,15 @@
+md5sums linguist-generated
+compiled.md5sum linguist-generated
+docker-hash linguist-generated
+*.gts linguist-generated
+*.adt linguist-generated
+*.bir linguist-generated
+*.relf linguist-generated
+
+src/test/compiled.url.txt text eol=lf
+src/test/make/docker-flake.txt text eol=lf
+
+Makefile text eol=lf
+*.sh text eol=lf
+*.mk text eol=lf
+*.md5sum text eol=lf

.github/workflows/run-examples.yml

@@ -31,25 +31,44 @@ jobs:
 
   SystemTests:
     runs-on: ubuntu-latest
-    container:
-      # Requires repo to have action access in package settings
-      image: ghcr.io/uq-pac/basil-dev:latest
-      credentials:
-        username: ${{ github.actor }}
-        password: ${{ secrets.github_token }}
+    # container:
+    #   # Requires repo to have action access in package settings
+    #   image: ghcr.io/uq-pac/basil-dev:latest
+    #   credentials:
+    #     username: ${{ github.actor }}
+    #     password: ${{ secrets.github_token }}
     steps:
       - name: Checkout
         uses: actions/checkout@v4
 
+      - uses: actions/setup-java@v4
+        with:
+          distribution: 'temurin'
+          java-version: '17'
+
+      - uses: actions/setup-dotnet@v4
+        with:
+          dotnet-version: '6.0.x'
+
+      - run: sudo apt-get update
+      - run: sudo apt-get install -y z3='4.8.12-*'
+      - run: dotnet tool install --global boogie --version '3.4.3'
+
+      - run: make extract
+        working-directory: src/test
+
       - name: System Tests
         run: ./mill test.testOnly 'SystemTests*'
+
       - uses: actions/upload-artifact@v4
+        if: always()
         with:
           name: testresult-${{ github.run_number }}
           path: |
             src/test/*.csv
             src/test/*.svg
-      - run: |
+      - if: always()
+        run: |
           pushd src/test
           tail -n+1 summary-*.csv
           pasted="$(paste headers.md.part summary-*.md.part)"

docs/development/readme.md

@@ -105,22 +105,24 @@ The [dsl](../basil-ir.md#constructing-programs-in-code) can be used to construct
 ### Integration tests
 
 These are the `SystemTests.scala` test case with the files present in `src/test/correct` for examples that should verify and `src/test/incorrect`
-for examples that should not verify. 
+for examples that should not verify.
 
-These are lifted via the Makefiles, to add another test simply add a directory, c source file, and optionally specification file and run 
-
-```sh
-cd src/test/
-make
-```
-
-The `config.mk` file in the test directory can be used to exclude unnecessary compilers, and change compilation flags. 
-Full details can be found [here](../src/test/readme.md).
+These are run via the Makefiles in src/test.
+A Docker image is used to compile and lift examples in a reproducible way.
+See [src/test/readme.md](../src/test/readme.md) for details.
 
 ### Running Tests
 
 The test suites use [ScalaTest](https://www.scalatest.org/).
 
+This tests are defined as C source files and must be compiled before use.
+Before running any tests, download the pre-compiled test case files with:
+```bash
+$ make -C src/test extract
+```
+For more details on this process, including adding and editing test cases,
+see [src/test/readme.md](../src/test/readme.md).
+
 To run the primary SystemTests suites (SystemTestsBAP and SystemTestsGTIRB) (which require Boogie):
 
 ```

src/main/scala/ir/IRCursor.scala

@@ -97,7 +97,7 @@ trait IntraProcIRCursor extends IRWalk[CFGPosition, CFGPosition] {
       case proc: Procedure => proc.entryBlock.toSet
       case b: Block        => b.statements.headOption.orElse(Some(b.jump)).toSet
       case n: GoTo         => n.targets.asInstanceOf[Set[CFGPosition]]
-      case h: Unreachable         => Set()
+      case h: Unreachable  => Set()
       case h: Return       => Set()
       case c: Statement    => IRWalk.nextCommandInBlock(c).toSet
     }

src/main/scala/ir/Program.scala

@@ -7,6 +7,55 @@ import analysis.{BitVectorEval, MergedRegion}
 import util.intrusive_list.*
 import translating.serialiseIL
 
+
+/**
+  * Iterator in pre-order of procedures, blocks, and commands. GoTos targets are traversed in an unspecified order.
+  */
+private class ILForwardIterator(private val begin: IterableOnce[CFGPosition], val walk: IRWalk[CFGPosition, CFGPosition]) extends Iterator[CFGPosition] {
+  val seen = mutable.Set[CFGPosition]()
+  private val stack = mutable.Stack[CFGPosition]()
+  stack.pushAll(begin)
+  seen.addAll(begin)
+
+  override def hasNext: Boolean = {
+    stack.nonEmpty
+  }
+
+  override def next(): CFGPosition = {
+    val n: CFGPosition = stack.pop()
+    seen.add(n)
+
+    val next = walk.succ(n).filterNot(seen.contains(_))
+    seen.addAll(next)
+    stack.pushAll(next)
+    n
+  }
+}
+
+/**
+  * Iterator in approximate syntactic pre-order of procedures, blocks, and commands. Blocks and procedures are 
+  * not guaranteed to be in any defined order. 
+  */
+private class ILLexicalIterator(private val begin: Iterable[CFGPosition]) extends Iterator[CFGPosition] {
+  private val stack = mutable.Stack[CFGPosition]()
+  stack.pushAll(begin)
+
+  override def hasNext: Boolean = {
+    stack.nonEmpty
+  }
+
+  override def next(): CFGPosition = {
+    val n: CFGPosition = stack.pop()
+
+    stack.pushAll(n match {
+      case p: Procedure => p.blocks
+      case b: Block => Seq() ++ b.statements.toSeq ++ Seq(b.jump)
+      case s: Command => Seq()
+    })
+    n
+  }
+}
+
 class Program(var procedures: ArrayBuffer[Procedure],
               var mainProcedure: Procedure,
               val initialMemory: mutable.TreeMap[BigInt, MemorySection]) extends Iterable[CFGPosition] {
@@ -92,37 +141,16 @@ class Program(var procedures: ArrayBuffer[Procedure],
 
   }
 
-  /**
-   * Iterator in approximate syntactic pre-order of procedures, blocks, and commands. Blocks and procedures are 
-   * not guaranteed to be in any defined order. 
-   */
-  private class ILUnorderedIterator(private val begin: Program) extends Iterator[CFGPosition] {
-    private val stack = mutable.Stack[CFGPosition]()
-    stack.addAll(begin.procedures)
-
-    override def hasNext: Boolean = {
-      stack.nonEmpty
-    }
-
-    override def next(): CFGPosition = {
-      val n: CFGPosition = stack.pop()
-
-      stack.pushAll(n match {
-        case p: Procedure => p.blocks
-        case b: Block => Seq() ++ b.statements.toSeq ++ Seq(b.jump)
-        case s: Command => Seq()
-      })
-      n
-    }
-
-  }
-
   /**
    * Get an Iterator in approximate syntactic pre-order of procedures, blocks, and commands. Blocks and procedures are 
    * not guaranteed to be in any defined order. 
    */
   def iterator: Iterator[CFGPosition] = {
-    ILUnorderedIterator(this)
+    ILLexicalIterator(this.procedures)
+  }
+
+  def preOrderIterator: Iterator[CFGPosition] = {
+    ILForwardIterator(this.procedures, IntraProcIRCursor)
   }
 
   private def memoryLookup(memory: mutable.TreeMap[BigInt, MemorySection], address: BigInt) = {
@@ -166,7 +194,7 @@ class Procedure private (
                   var out: ArrayBuffer[Parameter],
                   var requires: List[BExpr],
                   var ensures: List[BExpr],
-                ) {
+                ) extends Iterable[CFGPosition] {
   private val _callers = mutable.HashSet[DirectCall]()
   _blocks.foreach(_.parent = this)
   // class invariant
@@ -177,6 +205,21 @@ class Procedure private (
     this(name, address, entryBlock, returnBlock, mutable.LinkedHashSet.from(blocks), ArrayBuffer.from(in), ArrayBuffer.from(out), List.from(requires), List.from(ensures))
   }
 
+  /**
+   * Get an Iterator in approximate syntactic pre-order of procedures, blocks, and commands. Blocks and procedures are 
+   * not guaranteed to be in any defined order. 
+   */
+  def iterator: Iterator[CFGPosition] = {
+    ILLexicalIterator(Seq(this))
+  }
+
+  /**
+   * Iterate in cfg pre order.
+   */
+  def preOrderIterator: Iterator[CFGPosition] = {
+    ILForwardIterator(Seq(this), IntraProcIRCursor)
+  }
+
   override def toString: String = {
     s"Procedure $name at ${address.getOrElse("None")} with ${blocks.size} blocks and ${in.size} in and ${out.size} out parameters"
   }
@@ -479,4 +522,4 @@ case class MemorySection(name: String, address: BigInt, size: Int, bytes: Seq[Bi
     }
   }
 
-}
+}

src/test/.gitignore

@@ -2,4 +2,17 @@
 *.csv
 *.md
 *.md.part
-*.svg
+*.svg
+
+# files reproducibly generated
+*.relf
+*.adt
+*.bir
+*.gtirb
+*.gts
+docker-hash-new
+!compiled.url.txt
+*.gz
+*.bz2
+*.xz
+*.zst

src/test/Makefile

@@ -1,12 +1,51 @@
-TARGETSS := all verify clean cleanall cleanlift recompile json cleanjson cleangts gts
+TARGETSS := all verify repro-stash repro-check md5sum-check md5sum-update clean cleanall cleanlift recompile json cleanjson cleangts gts
 
-SUBTARGETS = $(wildcard correct/*/ incorrect/*/)
-.PHONY : $(TARGETSS) $(SUBTARGETS) correct incorrect
+# subdirectories of src/test. to be entered into by this makefile.
+DIRS := correct incorrect extraspec_correct extraspec_incorrect indirect_calls memory_regions procedure_summaries
+# dirs with different directory structure: dsa, irreducible_loops
 
-$(TARGETSS): $(SUBTARGETS)
+# non-test dirs: make, scala, unimplemented
 
-correct: $(realpath $(wildcard correct/*))
-incorrect: $(realpath $(wildcard incorrect/*))
+# in case the user specfies DIRS, make sure all dirs exist.
+$(foreach d, $(DIRS), \
+  $(if $(wildcard $(d)/.), \
+    , \
+    $(error user error: directory "$(d)" in DIRS variable does not exist)))
 
-$(SUBTARGETS):
-	-$(MAKE) -C $@ -f $(realpath ./make/lift-directories.mk) $(MAKECMDGOALS)
+SUBDIRS = $(wildcard $(addsuffix /*/,$(DIRS)))
+.PHONY : $(TARGETSS) $(SUBDIRS) $(DIRS)
+
+# through some unpleasantness, this lets the user specify either DIRS or SUBDIRS
+# on the command line, and the make operation will be narrowed to that directory
+$(TARGETSS): $(SUBDIRS)
+
+$(SUBDIRS):
+	$(MAKE) -C $@ -f $(realpath ./make/lift-directories.mk) $(MAKECMDGOALS)
+
+# concats md5sums files in subdirectories into a compiled.md5sum.
+# check with `md5sum -c compiled.md5sum` in src/test.
+.PHONY: compiled.md5sum
+compiled.md5sum:
+	find $(DIRS) -name '*.md5sum' -exec cat '{}' + | sort -k2 > compiled.md5sum
+
+TARBALL := compiled.tar.zst
+
+$(TARBALL) docker-contents.txt &: compiled.md5sum
+	set -u; $$DOCKER_CMD hash > docker-contents.txt  # before compessing, make sure docker-contents.txt is up to date.
+	md5sum --quiet -c compiled.md5sum  # before compressing, make sure our files match expected hashes.
+	list=`mktemp`; cut -d' ' -f3 compiled.md5sum > $$list && tar caf $(TARBALL) -T $$list && rm $$list
+	sha1sum $(TARBALL)
+
+.PHONY: extract
+extract:
+	# log URL and expected hash
+	{ head -n1 compiled.url.txt; tail -n1 compiled.url.txt; } | cat -v
+	# check existing file, otherwise download fresh copy.
+	{ tail -n1 compiled.url.txt | sha1sum -c - ; } \
+		|| curl "$$(head -n1 compiled.url.txt)" -o $(TARBALL)
+	# check file type.
+	-file $(TARBALL)
+	# validate the hash, otherwise remove the incorrect file and abort.
+	{ tail -n1 compiled.url.txt | sha1sum -c - ; } || { rm -v $(TARBALL); exit 1; }
+	tar xf $(TARBALL) --keep-old-files --touch
+	md5sum --quiet -c compiled.md5sum  # check that extracted files match expected checksums