avoid hardcoded addresses in test cases, add pre-order iterator (#294)

* IndirectCallTests: auto-detect indirect call IDs

makes this not tied to specific adt files

* touch comment of ILForwardIterator

* dsa: working on detecting addresses in dsa tests

* log removed functions

* dsa fix, add postLoad parameter to loadAndTranslate

* ci: run all tests :3

* use ./mill in dev docs

* ci: exclude SystemTests from  UnitTests

* add preorder iterator test

* removed hardcoded address from DSA test

* LiveVarsAnalysisTests: avoid fixed addresses

(cherry picked from commit e9ad100)

* IndirectCallTests: use postLoad hook

* ci: omit some tests, run tests sequentially

addressing review comment #294 (comment)

* add assertion messages to SSAVar

* Fix ordering bug

* ci: add package prefixes to test names

also use test.compile instead of compile, to
pre-compile tests as well.

* DataStructureAnalysisTest: sliding-window-based heuristic for SSAVar

* fix irtest

* ignore initialisation ParamAnalysisTests

* reorganise workflows

* revert pre-order iterator changes diverging from main

* test fixes

* revert to livevars inline by default

this is the behaviour before simplification-pass merge

- also fix live-var analysis tests due to printf call overapproximating
  and changes to proc/block names and labels

* procName

* paramanalysis do not assert main has live at exit

* ignore external call params in liveness for paramamalysis

* make proceduresummarytest pass action always

---------

Co-authored-by: Alistair Michael <[email protected]>
Co-authored-by: Sadra Bayat Tork <[email protected]>
Co-authored-by: bpaul <[email protected]>

.github/workflows/run-examples.yml

@@ -8,41 +8,39 @@ on:
       - main
   workflow_dispatch:
 jobs:
-  CompileAndTest:
+  Compile:
     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 }}
     steps:
       - name: Checkout
         uses: actions/checkout@v4
 
-      - name: Compile BASIL 
-        run: ./mill compile
+      - uses: actions/setup-java@v4
+        with:
+          distribution: 'temurin'
+          java-version: '21'
 
-      - name: Bitvec Tests
-        run: ./mill test.testOnly BitVectorAnalysisTests
+      - name: Compile BASIL Mill
+        run: ./mill compile
 
-      - name: IntrusiveListTest
-        run: ./mill test.testOnly '*IntrusiveListPublicInterfaceTest'
 
-  SystemTests:
+  StandardSystemTests:
     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 }}
     steps:
       - name: Checkout
         uses: actions/checkout@v4
 
-      - name: Simplify System Tests
-        run: ./mill test.testOnly 'SimplifySystemTests*'
+      - uses: actions/setup-java@v4
+        with:
+          distribution: 'temurin'
+          java-version: '21'
+
+      - 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'
 
       - name: System Tests
         run: ./mill test.testOnly 'SystemTests*'
@@ -75,3 +73,87 @@ jobs:
           echo "$pasted" > $GITHUB_STEP_SUMMARY
         shell: "bash -xe {0}"
 
+  UnitTests:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: actions/setup-java@v4
+        with:
+          distribution: 'temurin'
+          java-version: '21'
+
+      - 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: ./mill test.compile
+
+        # every test with package prefix:
+        # sbt "show test:definedTests"
+
+        # note: tests prefixed with '!' are expected to fail.
+        #       if they are fixed, the '!' should be removed.
+
+      - run: ./mill test.testOnly IrreducibleLoop
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly BitVectorAnalysisTests
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly '*IntrusiveListPublicInterfaceTest'
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly util.intrusive_list.IntrusiveListTest 
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly DataStructureAnalysisTest
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly ParamAnalysisTests
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly LiveVarsAnalysisTests
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly ir.IRTest
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly ir.CILVisitorTest
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly ir.InterpreterTests
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly ir.InvariantTest
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly ProcedureSummaryTests || true
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly TaintAnalysisTests
+        if: ${{ ! cancelled() }}
+
+  AnalysisSystemTests:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - run: ./mill test.compile
+
+      - uses: actions/setup-java@v4
+        with:
+          distribution: 'temurin'
+          java-version: '21'
+
+      - 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: echo "All systemtest suites:" & ./mill test.testOnly '*SystemTests*' -- -z 'xxxx'
+
+      - run: ./mill test.testOnly DSAMemoryRegionSystemTestsBAP
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly DSAMemoryRegionSystemTestsGTIRB
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly AnalysisSystemTestsBAP
+        if: ${{ ! cancelled() }}
+      - run: ./mill test.testOnly AnalysisSystemTestsGTIRB
+        if: ${{ ! cancelled() }}

docker/readme.md

@@ -68,7 +68,7 @@ podman-compose run compiler-explorer
 OR
 
 ```
-podman run -p 10240:10240 ghcr.io/uq-pac/basil-compiler-explorer:latest
+podman run --rm -p 10240:10240 ghcr.io/uq-pac/basil-compiler-explorer:latest
 ```
 
 ##### Development/Testing Container
@@ -77,7 +77,7 @@ This mounts the current directory as the working directory of the container.
 
 ```
 podman pull ghcr.io/uq-pac/basil-dev /bin/bash
-podman run -v .:/host -w /host -it ghcr.io/uq-pac/basil-dev /bin/bash
+podman run --privileged --rm -v .:/host -w /host -it ghcr.io/uq-pac/basil-dev /bin/bash
 ```
 
 

docs/development/readme.md

@@ -126,31 +126,31 @@ The test suites use [ScalaTest](https://www.scalatest.org/).
 To run the primary SystemTests suites (SystemTestsBAP and SystemTestsGTIRB) (which require Boogie):
 
 ```
-$ mill.test.testOnly 'SystemTests*'
+$ ./mill test.testOnly 'SystemTests*'
 ```
 
 To run a single test from a test suite, it can be selected using globbing on the full test class name with the `testOnly` task:
 
 ```
-$ mill test.testOnly 'SystemTestsBAP' -- -z basic_arrays_read/gcc:BAP
+$ ./mill test.testOnly 'SystemTestsBAP' -- -z basic_arrays_read/gcc:BAP
 ```
 
 To update the expected BASIL output files from the SystemTests results run:
 
 ```
-$ mill updateExpected
+$ ./mill updateExpected
 ```
 
 To run another test suite, just use the name of the class containing the test suite (in this case LiveVarsAnalysisTests):
 
 ```
-$ mill.test.testOnly 'LiveVarsAnalysisTests'
+$ ./mill test.testOnly 'LiveVarsAnalysisTests'
 ```
 
 To list all test suites:
 
 ```
-$ mill.test.testOnly * -- -t ''
+$ ./mill test.testOnly '*' -- -t ''
 ```
 
 ## Performance profiling

src/main/scala/analysis/InterLiveVarsAnalysis.scala

@@ -13,8 +13,7 @@ import ir.{Assert, LocalAssign, Assume, CFGPosition, Command, DirectCall, Indire
  * Tip SPA IDE Slides include a short and clear explanation of microfunctions
  * https://cs.au.dk/~amoeller/spa/8-distributive.pdf
  */
-trait LiveVarsAnalysisFunctions(inline: Boolean) extends BackwardIDEAnalysis[Variable, TwoElement, TwoElementLattice] {
-
+trait LiveVarsAnalysisFunctions(inline: Boolean, addExternals : Boolean = true) extends BackwardIDEAnalysis[Variable, TwoElement, TwoElementLattice] {
   val valuelattice: TwoElementLattice = TwoElementLattice()
   val edgelattice: EdgeFunctionLattice[TwoElement, TwoElementLattice] = EdgeFunctionLattice(valuelattice)
   import edgelattice.{IdEdge, ConstEdge}
@@ -96,7 +95,7 @@ trait LiveVarsAnalysisFunctions(inline: Boolean) extends BackwardIDEAnalysis[Var
           case Left(value) => if value != variable then Map(d -> IdEdge()) else Map()
           case Right(_) => Map(d -> IdEdge(), Left(variable) -> ConstEdge(TwoElementTop))
         }
-      case c: DirectCall if (c.target.isExternal.contains(true) || c.target.blocks.isEmpty) => {
+      case c: DirectCall if addExternals && (c.target.isExternal.contains(true) || c.target.blocks.isEmpty) => {
         val writes = ir.transforms.externalCallWrites(c.target.procName).toSet[Variable]
         val reads = ir.transforms.externalCallReads(c.target.procName).toSet[Variable]
         d match {
@@ -131,11 +130,9 @@ trait LiveVarsAnalysisFunctions(inline: Boolean) extends BackwardIDEAnalysis[Var
   }
 }
 
-class InterLiveVarsAnalysis(program: Program)
-  extends BackwardIDESolver[Variable, TwoElement, TwoElementLattice](program), LiveVarsAnalysisFunctions(false)
 
+class InterLiveVarsAnalysis(program: Program, ignoreExternals : Boolean = false)
+  extends BackwardIDESolver[Variable, TwoElement, TwoElementLattice](program), LiveVarsAnalysisFunctions(true, !ignoreExternals)
 
-class InlineInterLiveVarsAnalysis(program: Program)
-  extends BackwardIDESolver[Variable, TwoElement, TwoElementLattice](program), LiveVarsAnalysisFunctions(true)
 
 

src/main/scala/analysis/IntraLiveVarsAnalysis.scala

@@ -3,7 +3,7 @@ package analysis
 import analysis.solvers.SimpleWorklistFixpointSolver
 import ir.*
 
-abstract class LivenessAnalysis(program: Program) extends Analysis[Any] {
+abstract class LivenessAnalysis(program: Program, addExternals: Boolean = true) extends Analysis[Any] {
   val lattice: MapLattice[CFGPosition, Set[Variable], PowersetLattice[Variable]] = MapLattice(PowersetLattice())
   val domain: Set[CFGPosition] = Set.empty ++ program
 
@@ -17,6 +17,11 @@ abstract class LivenessAnalysis(program: Program) extends Analysis[Any] {
       case a: Assume       => s ++ a.body.variables
       case a: Assert       => s ++ a.body.variables
       case i: IndirectCall => s + i.target
+      case c: DirectCall if addExternals && (c.target.isExternal.contains(true) || c.target.blocks.isEmpty) => {
+        val writes = ir.transforms.externalCallWrites(c.target.procName).toSet[Variable]
+        val reads = ir.transforms.externalCallReads(c.target.procName).toSet[Variable]
+        s -- writes ++ reads
+      }
       case c: DirectCall   => (s -- c.outParams.map(_._2)) ++ c.actualParams.flatMap(_._2.variables)
       case g: GoTo         => s
       case r: Return       => s ++ r.outParams.flatMap(_._2.variables)
@@ -27,6 +32,6 @@ abstract class LivenessAnalysis(program: Program) extends Analysis[Any] {
 }
 
 class IntraLiveVarsAnalysis(program: Program)
-    extends LivenessAnalysis(program)
+    extends LivenessAnalysis(program, false)
     with SimpleWorklistFixpointSolver[CFGPosition, Set[Variable], PowersetLattice[Variable]]
     with IRIntraproceduralBackwardDependencies

src/main/scala/analysis/MemoryModelMap.scala

@@ -443,7 +443,7 @@ class MemoryModelMap(
   }
 
   def getHeap(directCall: DirectCall): HeapRegion = {
-    require(directCall.target.name == "malloc", "Should be a malloc call")
+    require(directCall.target.procName == "malloc", "Should be a malloc call")
     heapCalls(directCall)
   }
 

src/main/scala/analysis/MemoryRegionAnalysis.scala

@@ -230,7 +230,7 @@ trait MemoryRegionAnalysis(
     val stackPointerVariables = stackDetection(n, s(0)(1))
     n match {
       case directCall: DirectCall =>
-        if (directCall.target.name == "malloc") {
+        if (directCall.target.procName == "malloc") {
           evaluateExpression(mallocVariable, constantProp(n)) match {
             case Some(b: BitVecLiteral) =>
               val negB = bv2SignedInt(b)

src/main/scala/analysis/ParamAnalysis.scala

@@ -1,4 +1,5 @@
 package analysis
+import translating.PrettyPrinter.*
 
 import ir.{BitVecType, Procedure, Program, Register, Variable, Block, Return, Unreachable, GoTo}
 
@@ -9,7 +10,7 @@ import ir.{BitVecType, Procedure, Program, Register, Variable, Block, Return, Un
  */
 class ParamAnalysis(val program: Program) extends Analysis[Any] {
   private val intraLivenessResults = IntraLiveVarsAnalysis(program).analyze()
-  private val interLivenessResults = InterLiveVarsAnalysis(program).analyze()
+  private val interLivenessResults = InterLiveVarsAnalysis(program, true).analyze()
   private var completeProcs: Set[Procedure] = Set()
   private var visitedProcs: Set[Procedure] = Set()
   private var results : Map[Procedure, Set[Variable]] = Map()

src/main/scala/analysis/ReachingDefs.scala

@@ -15,7 +15,7 @@ abstract class ReachingDefs(program: Program, writesTo: Map[Procedure, Set[Regis
         s + (loc.lhs -> Set(n))
       case load: MemoryLoad =>
         s + (load.lhs -> Set(n))
-      case DirectCall(target, _, _, _) if target.name == "malloc" =>
+      case DirectCall(target, _, _, _) if target.procName == "malloc" =>
         s + (mallocRegister -> Set(n))
       case DirectCall(target, _, _, _) if writesTo.contains(target) =>
         val result: Map[Variable, Set[CFGPosition]] = writesTo(target).foldLeft(Map[Variable, Set[CFGPosition]]()) {

src/main/scala/analysis/RegionInjector.scala

@@ -246,10 +246,10 @@ class RegionInjectorDSA(override val program: Program, DSATopDown: mutable.Map[P
     val stack = cell.node.get.flags.stack
     val name = if (stack) {
       stackCounter += 1
-      s"stack$$${stackCounter}"
+      s"stack_${stackCounter}"
     } else {
       sharedMemoryCounter += 1
-      s"mem$$${sharedMemoryCounter}"
+      s"mem_${sharedMemoryCounter}"
     }
     MergedRegionDSA(name, cell, stack)
   }

src/main/scala/analysis/VSA.scala

@@ -56,7 +56,7 @@ trait ValueSetAnalysis(program: Program, mmm: MemoryModelMap) {
     */
   def eval(cmd: Command, s: Map[Variable | MemoryRegion, Set[Value]]): Map[Variable | MemoryRegion, Set[Value]] = {
     cmd match {
-      case directCall: DirectCall if directCall.target.name == "malloc" =>
+      case directCall: DirectCall if directCall.target.procName == "malloc" =>
         val regions = mmm.nodeToRegion(cmd)
         // malloc variable
         s + (mallocVariable -> regions.map(r => AddressValue(r)))

src/main/scala/analysis/WriteToAnalysis.scala

@@ -30,7 +30,7 @@ class WriteToAnalysis(program: Program) extends Analysis[Map[Procedure, Set[Regi
             writtenTo.add(variable)
           case MemoryLoad(lhs: Register, _, _, _, _, _) if paramRegisters.contains(lhs) =>
             writtenTo.add(lhs)
-          case DirectCall(target, _, _, _) if target.name == "malloc" =>
+          case DirectCall(target, _, _, _) if target.procName == "malloc" =>
             writtenTo.add(mallocRegister)
           case d: DirectCall if program.procedures.contains(d.target) =>
             writtenTo.addAll(getWritesTos(d.target))