Merge pull request #179 from UQ-PAC/staging

Merge staging into main

.github/workflows/run-examples.yml

@@ -8,12 +8,11 @@ on:
       - main
   workflow_dispatch:
 jobs:
-  test:
+  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
       credentials:
         username: ${{ github.actor }}
@@ -23,14 +22,29 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Compile BASIL 
-        run: sbt assembly
+        run: ./mill compile
 
       - name: Bitvec Tests
-        run: sbt "testOnly BitVectorAnalysisTests"
-
-      - name: System Tests
-        run: sbt "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"
+        run: ./mill test.testOnly BitVectorAnalysisTests
 
+      - name: IntrusiveListTest
+        run: ./mill test.testOnly IntrusiveListPublicInterfaceTests
 
+      - 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
+      credentials:
+        username: ${{ github.actor }}
+        password: ${{ secrets.github_token }}
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
 
+      - name: System Tests
+        run: ./mill test.testOnly SystemTests || true

.mill-version

@@ -0,0 +1 @@
+0.11.6

antlr.sc

@@ -0,0 +1,62 @@
+//package net.mlbox.millantlr
+// https://github.com/da-tubi/antlr4-scala-example/blob/master/antlr.sc
+import mill._
+import mill.define._
+import mill.scalalib._
+import $ivy.`org.antlr:antlr4:4.9.3`
+import org.antlr.v4.tool.{ANTLRMessage, ANTLRToolListener}
+
+import scala.collection.mutable
+
+trait AntlrModule extends JavaModule {
+  def antlrGrammarSources: mill.define.Target[Seq[mill.api.PathRef]]
+  def antlrPackage: Option[String] = None
+  def antlrGenerateVisitor: Boolean = false
+  def antlrGenerateListener: Boolean = false
+
+  def antlrGrammarSourceFiles = T {
+    antlrGrammarSources().flatMap { source =>
+      if (os.isDir(source.path)) {
+        os.walk(source.path)
+      } else {
+        Seq(source.path)
+      }
+    }.filter { path =>
+      os.isFile(path) && path.ext == "g4"
+    }.map(PathRef(_))
+  }
+
+  def antlrGenerate = T {
+    val antlrToolArgs = mutable.ArrayBuffer.empty[String]
+
+    antlrToolArgs.appendAll(antlrGrammarSourceFiles().map(_.path.relativeTo(os.pwd).toString))
+    antlrToolArgs.append("-o")
+    antlrToolArgs.append(s"${T.dest}")
+    if (antlrGenerateVisitor) {
+      antlrToolArgs.append("-visitor")
+    }
+    if (antlrGenerateListener) {
+      antlrToolArgs.append("-listener")
+    }
+    if (antlrPackage.isDefined) {
+      antlrToolArgs.append("-package")
+      antlrToolArgs.append(antlrPackage.get)
+    }
+
+    val antlrTool = new org.antlr.v4.Tool(antlrToolArgs.toArray)
+    antlrTool.addListener(new ToolListener())
+    antlrTool.processGrammarsOnCommandLine()
+
+    os.walk(T.dest).filter(path => os.isFile(path) && path.ext == "java").map(PathRef(_))
+  }
+
+  override def generatedSources = T {
+    super.generatedSources() ++ antlrGenerate()
+  }
+}
+
+class ToolListener extends ANTLRToolListener {
+  override def info(msg: String): Unit = throw new RuntimeException(msg)
+  override def error(msg: ANTLRMessage): Unit = throw new RuntimeException(msg.toString)
+  override def warning(msg: ANTLRMessage): Unit = throw new RuntimeException(msg.toString)
+}

build.sc

@@ -0,0 +1,84 @@
+import mill._, mill.define._, scalalib._
+
+import $file.antlr // https://index.scala-lang.org/ml86/mill-antlr
+
+import os.Path
+import $ivy.`com.lihaoyi::mill-contrib-scalapblib:$MILL_VERSION`
+import contrib.scalapblib._
+
+
+
+object basil extends RootModule with ScalaModule with antlr.AntlrModule with ScalaPBModule{
+  def scalaVersion = "3.3.1"
+
+  val javaTests = ivy"com.novocode:junit-interface:0.11"
+  val scalaTests = ivy"org.scalatest::scalatest:3.2.10"
+  val scalactic = ivy"org.scalactic::scalactic:3.2.10"
+  val antlrRuntime = ivy"org.antlr:antlr4-runtime:4.9"
+  val sourceCode = ivy"com.lihaoyi::sourcecode:0.3.0"
+  val mainArgs = ivy"com.lihaoyi::mainargs:0.5.1"
+  val sprayJson = ivy"io.spray::spray-json:1.3.6"
+  val scalapb = ivy"com.thesamet.scalapb::scalapb-runtime:0.11.15" 
+
+  def scalaPBVersion = "0.11.15"
+
+
+  def mainClass = Some("Main")
+
+  override def scalaPBSources = T.sources {Seq(PathRef(this.millSourcePath / "main" / "protobuf"))}
+  def millSourcePath = super.millSourcePath / "src"
+  def ivyDeps = Agg(scalactic, antlrRuntime, sourceCode, mainArgs, sprayJson, scalapb)
+  def sources = T.sources {Seq(PathRef(this.millSourcePath / "main" / "scala" ))}
+
+
+  override def antlrPackage: Option[String] = Some("Parsers")
+  override def antlrGenerateVisitor = true
+  override def antlrGrammarSources = T.sources {
+    Seq(PathRef(millSourcePath / "main" / "antlr4"))
+  }
+
+  object test extends ScalaTests with TestModule.ScalaTest  {
+    def ivyDeps = Agg(scalaTests, javaTests)
+    def sources = T.sources {Seq(PathRef(this.millSourcePath / "scala" ))}
+  }
+
+
+  /**
+   * Updates the expected
+   */
+  def updateExpected() = 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)
+              }
+            }
+          }
+        }
+      }
+    }
+
+    def filesContentEqual(path1: Path, path2: Path): Boolean = {
+      os.read(path1) == os.read(path2)
+    }
+
+    expectedUpdate(correctPath, true)
+    expectedUpdate(incorrectPath, false)
+  }
+
+}

compose.yaml

@@ -7,6 +7,15 @@ services:
     volumes:
       - ./:/host:rw
     working_dir: /host
+  basil-nix-dev:
+    image: ghcr.io/uq-pac/basil-nix-dev:latest
+    build:
+      dockerfile: docker/nixdocker.Dockerfile
+      target: nix-dev-base
+    volumes:
+      - ./:/host:rw
+    working_dir: /host
+
   basil-dev:
     image: ghcr.io/uq-pac/basil-dev:latest
     build:

docker/asli.Dockerfile

@@ -1,7 +1,7 @@
 # ====
 # ASLP
 # ====
-FROM ocaml/opam:ubuntu-23.04-ocaml-4.14 AS aslp
+FROM docker.io/ocaml/opam:ubuntu-23.04-ocaml-4.14 AS aslp
 USER root
 
 # Install system dependencies
@@ -47,7 +47,7 @@ USER root
 # it requires old versions of libffi and libtinfo and generally 
 # doesn't support ubuntu well.
 # Opam install is the most reliable way.
-FROM ocaml/opam:ubuntu-23.04-ocaml-4.14 AS aslp-bap
+FROM docker.io/ocaml/opam:ubuntu-23.04-ocaml-4.14 AS aslp-bap
 USER root
 # Install system dependencies
 RUN apt-get update && apt-get install -y python3 libgmp-dev yasm m4 \
@@ -112,11 +112,10 @@ USER root
 # =======================
 # BASIL build environment
 # =======================
-FROM ubuntu:23.04 AS scala
+FROM docker.io/ubuntu:23.04 AS scala
 ENV PATH="$PATH:/root/.local/share/coursier/bin"
 RUN apt-get update && apt-get install default-jre-headless curl git --yes \ 
- && curl -fL https://github.com/coursier/coursier/releases/latest/download/cs-x86_64-pc-linux.gz | gzip -d > cs && chmod +x cs && ./cs setup --yes \
- && apt-get remove curl --yes \
+ && curl -fL https://github.com/coursier/coursier/releases/latest/download/cs-x86_64-pc-linux.gz | gzip -d > cs && chmod +x cs && ./cs setup --yes && cs install mill \
   && apt-get autoremove --purge -y \
   && apt-get autoclean -y
 
@@ -196,5 +195,5 @@ RUN apt-get update && apt-get install --yes default-jre-headless python3 libgmp-
 # ------------------
 # Transplanted BAP 
 # ==================
-COPY --from=basil /basil/target/scala-3.1.0/wptool-boogie-assembly-0.0.1.jar /target/scala-3.1.0/wptool-boogie-assembly-0.0.1.jar
+COPY --from=basil /basil/target/scala-3.3.0/wptool-boogie-assembly-0.0.1.jar /target/scala-3.3.0/wptool-boogie-assembly-0.0.1.jar
 WORKDIR /app

docker/nixdocker.Dockerfile

@@ -0,0 +1,12 @@
+
+FROM docker.io/nixos/nix:latest AS nix-dev-base 
+RUN nix-channel --update
+RUN printf '%s\n' "extra-experimental-features = nix-command flakes" "extra-trusted-users = $USER" | tee -a /etc/nix/nix.conf 
+RUN  nix profile install --impure 'github:katrinafyi/pac-nix#aslp'  
+RUN  nix profile install --impure 'github:katrinafyi/pac-nix#bap-aslp'  
+RUN  nix profile install --impure 'nixpkgs#boogie'
+RUN  nix profile install --impure 'nixpkgs#openjdk'
+RUN  nix profile install --impure 'nixpkgs#coursier' && cs setup --yes
+RUN  cs install mill
+ENV  PATH=$PATH:/root/.local/share/coursier/bin
+

docker/readme.md

@@ -2,6 +2,84 @@
 
 ---
 
+### Using Containers 
+
+(This method has only been tested on linux)
+
+The docker config can be used to provide bap with the asli-plugin as well as compile the tool itself.
+
+Requirements:
+
+- podman, podman-compose
+
+#### 1. Obtain the image image
+
+##### From github 
+
+`podman pull ghcr.io/uq-pac/basil-dev:latest`
+
+##### Build the images
+
+To build the images, from the root of the respository run
+
+```
+podman-compose build
+```
+
+#### 2. Use the images with compose 
+
+Individual services can be built with `podman compose build $servicename` from the root of the repo. 
+
+The services provided are:
+
+- `basil-dev` dev environment containng scala build environment, bap and cross-compilers
+   - To compile basil into the current directory using the sbt and scala provided by the docker image: 
+      - `podman compose run basil-dev sbt assembly`
+   - To enter a shell inside the container
+      - `podman compose run basil-build`
+- `basil-build`
+   - The same as above however containg only the scala build environment and compiled basil
+   - To recompile with the currently checked-out repo run `podman-compose build basil-build`
+   - To enter a shell inside the container
+      - `podman compose run basil-build`
+- `basil` precompiled jar file and tools
+   - To run the jar inside the docker image `podman-compose run basil-dev $arguments...`
+- `compiler-explorer`
+    - instance of [godbolt.org](godbolt.org) with the tools installed. 
+
+Or enter the dev container manually, mounting the current directory (the same as podman-compose basil-dev).
+
+
+#### 2. Use the images manually  
+
+##### Compiler Explorer Container
+
+```sh
+podman pull ghcr.io/uq-pac/basil-compiler-explorer:latest
+```
+
+
+```sh
+podman-compose run compiler-explorer
+```
+
+OR
+
+```
+podman run -p 10240:10240 ghcr.io/uq-pac/basil-compiler-explorer:latest
+```
+
+##### Development/Testing Container
+
+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
+```
+
+
+
 #### Publishing container images to github registry:
 
 - This only needs to be done when the docker images are modified or you wish to