Merge pull request #75 from UQ-PAC/prepare-analysis-devel-merge

Prepare analysis devel merge

.github/workflows/run-examples.yml

@@ -0,0 +1,36 @@
+name: Run Examples 
+on: 
+  push:
+    branches: 
+      - main
+  pull_request:
+    branches: 
+      - main
+  workflow_dispatch:
+jobs:
+  test:
+    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: Compile BASIL 
+        run: sbt assembly
+
+      - 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"
+
+
+
+

build.sbt

@@ -1,4 +1,4 @@
-import scala.sys.process.Process
+import scala.io.Source
 
 ThisBuild / scalaVersion := "3.1.0"
 ThisBuild / version := "0.0.1"
@@ -8,6 +8,8 @@ val javaTests = "com.novocode" % "junit-interface" % "0.11" % "test"
 val scalaTests = "org.scalatest" %% "scalatest" % "3.2.10" % "test"
 val scalactic = "org.scalactic" %% "scalactic" % "3.2.10"
 val antlrRuntime = "org.antlr" % "antlr4-runtime" % "4.9.3"
+val sourceCode = "com.lihaoyi" %% "sourcecode" % "0.3.0"
+val mainArgs = "com.lihaoyi" %% "mainargs" % "0.5.1"
 
 lazy val root = project
   .in(file("."))
@@ -16,12 +18,14 @@ lazy val root = project
     name := "wptool-boogie",
     Antlr4 / antlr4Version := "4.9.3",
     Antlr4 / antlr4GenVisitor := true,
-    Antlr4 / antlr4PackageName := Some("BilParser"),
-    Compile / run / mainClass := Some("main"),
+    Antlr4 / antlr4PackageName := Some("Parsers"),
+    Compile / run / mainClass := Some("Main"),
     libraryDependencies += javaTests,
     libraryDependencies += antlrRuntime,
     libraryDependencies += scalactic,
-    libraryDependencies += scalaTests
+    libraryDependencies += scalaTests,
+    libraryDependencies += sourceCode,
+    libraryDependencies += mainArgs
   )
 
 lazy val updateExpected = taskKey[Unit]("updates .expected for test cases")
@@ -44,14 +48,40 @@ updateExpected := {
           val result = IO.read(resultPath)
           val verified = result.strip().equals("Boogie program verifier finished with 0 errors")
           if (verified == shouldVerify && outPath.exists()) {
-            IO.copyFile(outPath, expectedPath)
+            if (!expectedPath.exists() || !compareFiles(outPath, expectedPath)) {
+              IO.copyFile(outPath, expectedPath)
+            }
           }
         }
       }
     }
   }
 
+  def compareFiles(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)
 }
-

compose.yaml

@@ -0,0 +1,33 @@
+services:
+  basil-build:
+    image: basil:build
+    build:
+      dockerfile: docker/asli.Dockerfile 
+      target: basil
+    volumes:
+      - ./:/host:rw
+    working_dir: /host
+  basil-dev:
+    image: ghcr.io/uq-pac/basil-dev:latest
+    build:
+      dockerfile: docker/asli.Dockerfile 
+      target: basil:dev
+    volumes:
+      - ./:/host:rw
+    working_dir: /host
+  basil:
+    image: ghcr.io/uq-pac/basil:latest
+    build:
+      dockerfile: docker/asli.Dockerfile 
+      target: minified-all
+    volumes:
+      - ./:/host:rw
+    working_dir: /host
+  compiler-explorer:
+    image: ghcr.io/uq-pac/basil-compiler-explorer:latest
+    build:
+      dockerfile: docker/godbolt.Dockerfile 
+    network_mode: host
+    ports: 
+      - "10240:10240"
+

docker/asli.Dockerfile

@@ -0,0 +1,200 @@
+# ====
+# ASLP
+# ====
+FROM ocaml/opam:ubuntu-23.04-ocaml-4.14 AS aslp
+USER root
+
+# Install system dependencies
+RUN apt-get update && apt-get install -y python3 libgmp-dev yasm m4 \
+  libcurl4-gnutls-dev pkg-config zlib1g-dev cmake ninja-build g++-10 \
+  radare2 z3 libz3-dev llvm-14-dev \
+  re2c \
+  libpcre3-dev \
+  && apt-get autoremove --purge -y \
+  && apt-get autoclean -y \
+
+USER opam
+ENV OPAMROOT=/home/opam/.opam
+
+# clone and install aslp
+USER opam
+RUN cd /home/opam && git clone https://github.com/UQ-PAC/aslp.git  
+RUN eval $(opam config env) && cd /home/opam/aslp && opam install . --deps-only --with-test  -j1
+RUN cd /home/opam/aslp && eval $(opam config env) && export LD_LIBRARY_PATH=`opam config var z3:lib` \
+  && make install 
+# so the aslp script is before aslp in the path 
+ENV PATH=/home/opam/aslp:$PATH
+
+# ============
+# Bap Upstream 
+# ============
+# It would be more convenient to use the dpkg package, however 
+# it requires old versions of libffi and libtinfo and generally 
+# doesn't support ubuntu well.
+# Opam install is the most reliable way.
+FROM aslp AS bap-upstream.2.5
+USER opam
+WORKDIR /home/opam
+RUN opam depext --update --install bap.2.5.0 --yes -j 1
+RUN opam install bap.2.5.0 --yes -j 1 \
+ && opam clean -acrs 
+USER root
+
+# ============
+# Bap Pac 
+# ============
+# It would be more convenient to use the dpkg package, however 
+# 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
+USER root
+# Install system dependencies
+RUN apt-get update && apt-get install -y python3 libgmp-dev yasm m4 \
+  libcurl4-gnutls-dev pkg-config zlib1g-dev cmake ninja-build g++-10 \
+  radare2 z3 libz3-dev llvm-14-dev \
+  re2c \
+  libpcre3-dev \
+  && apt-get autoremove --purge -y \
+  && apt-get autoclean -y \
+USER opam
+WORKDIR /home/opam
+#RUN eval $(opam env) && opam pin add z3 4.8.7 --yes -n   
+RUN eval $(opam env) && opam depext --install z3 -j1  # this is a separate stage since it takes a very long time to build
+RUN eval $(opam env) \
+ && opam pin add bap https://github.com/UQ-PAC/bap.git --yes -n \
+ && opam pin add asli https://github.com/UQ-PAC/asl-interpreter.git --yes -n \ 
+ && opam install --yes --deps-only bap
+RUN git clone https://github.com/UQ-PAC/bap.git 
+RUN cd bap && eval $(opam env) && opam install oasis \ 
+    &&  opam install ./opam --deps-only  -j1 \
+    && ./configure --enable-everything \
+    --disable-ghidra --disable-radare2 --disable-primus-symbolic-executor \
+    --prefix=`opam var prefix` \
+    --with-llvm-version=14 --with-llvm-config=llvm-config-14 \
+    && make && make reinstall \
+ && opam clean -acrs 
+USER root
+
+
+# ====================
+# Bap with ASLi plugin
+# ====================
+FROM bap-upsteam.2.5 AS aslp-bap-upstream
+USER opam
+RUN git clone https://github.com/UQ-PAC/bap-asli-plugin.git
+RUN cd /home/opam/bap-asli-plugin && eval $(opam env) && make
+ENV ASLI_PATH=/home/opam/aslp
+USER root 
+
+# ==================
+# Transplant bap: 
+# ------------------
+# COPY --from=aslp-bap /home/opam/.opam/4.14/bin /home/opam/.opam/4.14/bin
+# COPY --from=aslp-bap /home/opam/.opam/4.14/lib  /home/opam/.opam/4.14/lib
+# COPY --from=aslp-bap /home/opam/.opam/4.14/share /home/opam/.opam/4.14/share
+# COPY --from=aslp-bap /home/opam/aslp/mra_tools /aslp/mra_tools
+# COPY --from=aslp-bap /home/opam/aslp/tests /aslp/tests
+# COPY --from=aslp-bap /home/opam/aslp/asli /aslp/asli 
+# COPY --from=aslp-bap /home/opam/aslp/prelude.asl /aslp/prelude.asl
+# COPY --from=aslp-bap /home/opam/.opam/4.14/lib/z3 /usr/local/lib/z3
+# # opam env
+# ENV CAML_LD_LIBRARY_PATH='/home/opam/.opam/4.14/lib/stublibs:/home/opam/.opam/4.14/lib/ocaml/stublibs:/home/opam/.opam/4.14/lib/ocaml'
+# ENV OPAM_SWITCH_PREFIX='/home/opam/.opam/4.14'
+# ENV OCAML_TOPLEVEL_PATH='/home/opam/.opam/4.14/lib/toplevel'
+# ENV ASLI_PATH=/aslp/
+# ENV PATH=$PATH:/home/opam/.opam/4.14/bin
+# ------------------
+# Transplanted BAP 
+# ==================
+
+
+# =======================
+# BASIL build environment
+# =======================
+FROM 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 \
+  && apt-get autoremove --purge -y \
+  && apt-get autoclean -y
+
+# =============
+# Compile BASIL
+# =============
+FROM scala AS basil
+RUN git clone https://github.com/UQ-PAC/bil-to-boogie-translator.git /basil
+RUN cd /basil && sbt assembly
+
+# ===============
+# BASIL Dev Image 
+# ===============
+FROM scala AS basil:dev 
+# use the basil image so sbt cache is full
+RUN apt-get update && apt-get install --yes default-jre-headless python3 libgmp-dev yasm m4 \
+  libcurl4-gnutls-dev pkg-config zlib1g-dev cmake ninja-build g++-10 \
+  radare2 z3 libz3-dev llvm-14-dev \
+  re2c \
+  libpcre3-dev \
+  clang-14 clang-15 gcc-aarch64-linux-gnu \
+  dotnet6 \
+  && apt-get autoremove --purge -y \
+  && apt-get autoclean -y \
+  && dotnet tool install --global boogie
+# asli
+
+# ==================
+# Transplant bap: 
+# ------------------
+ COPY --from=aslp-bap /home/opam/.opam/4.14/bin /home/opam/.opam/4.14/bin
+ COPY --from=aslp-bap /home/opam/.opam/4.14/lib  /home/opam/.opam/4.14/lib
+ COPY --from=aslp-bap /home/opam/.opam/4.14/share /home/opam/.opam/4.14/share
+ COPY --from=aslp-bap /home/opam/.opam/4.14/lib/z3 /usr/local/lib/z3
+ # opam env
+ ENV CAML_LD_LIBRARY_PATH='/home/opam/.opam/4.14/lib/stublibs:/home/opam/.opam/4.14/lib/ocaml/stublibs:/home/opam/.opam/4.14/lib/ocaml'
+ ENV OPAM_SWITCH_PREFIX='/home/opam/.opam/4.14'
+ ENV OCAML_TOPLEVEL_PATH='/home/opam/.opam/4.14/lib/toplevel'
+ ENV ASLI_PATH=/aslp/
+ ENV PATH=$PATH:/home/opam/.opam/4.14/bin:/root/.dotnet/tools/
+# ------------------
+# Transplanted BAP 
+# ==================
+
+WORKDIR /basil
+ENV CAML_LD_LIBRARY_PATH='/home/opam/.opam/4.14/lib/stublibs:/home/opam/.opam/4.14/lib/ocaml/stublibs:/home/opam/.opam/4.14/lib/ocaml'
+ENV ASLI_PATH=/aslp/
+ENV PATH=$PATH:/home/opam/.opam/4.14/bin:/root/.dotnet/tools/
+
+
+# =============
+# Minimal image
+# =============
+FROM ubuntu:23.04 as minified-all 
+RUN apt-get update && apt-get install --yes default-jre-headless python3 libgmp-dev yasm m4 \
+  libcurl4-gnutls-dev pkg-config zlib1g-dev cmake ninja-build g++-10 \
+  radare2 z3 libz3-dev llvm-14-dev \
+  re2c \
+  libpcre3-dev \
+  clang-14 clang-15 gcc-aarch64-linux-gnu \
+  dotnet6 \
+  && apt-get autoremove --purge -y \
+  && apt-get autoclean -y \
+  && dotnet tool install --global boogie
+# ==================
+# Transplant bap: 
+# ------------------
+ COPY --from=aslp-bap /home/opam/.opam/4.14/bin /home/opam/.opam/4.14/bin
+ COPY --from=aslp-bap /home/opam/.opam/4.14/lib  /home/opam/.opam/4.14/lib
+ COPY --from=aslp-bap /home/opam/.opam/4.14/share /home/opam/.opam/4.14/share
+ COPY --from=aslp-bap /home/opam/.opam/4.14/lib/z3 /usr/local/lib/z3
+ # opam env
+ ENV CAML_LD_LIBRARY_PATH='/home/opam/.opam/4.14/lib/stublibs:/home/opam/.opam/4.14/lib/ocaml/stublibs:/home/opam/.opam/4.14/lib/ocaml'
+ ENV OPAM_SWITCH_PREFIX='/home/opam/.opam/4.14'
+ ENV OCAML_TOPLEVEL_PATH='/home/opam/.opam/4.14/lib/toplevel'
+ ENV PATH=$PATH:/home/opam/.opam/4.14/bin:/root/.dotnet/tools/
+# ------------------
+# 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
+WORKDIR /app

docker/godbolt.Dockerfile

@@ -0,0 +1,35 @@
+FROM ghcr.io/uq-pac/basil:latest as compiler-explorer
+# https://github.com/madduci/docker-compiler-explorer/tree/master
+RUN DEBIAN_FRONTEND=noninteractive apt-get update \
+    && apt-get install -y curl \
+    && curl -sL https://deb.nodesource.com/setup_18.x | bash - \
+    && apt-get install -y \
+        wget \
+        ca-certificates \
+        nodejs \
+        make \
+        git \
+        dotnet6 \
+    && apt-get autoremove --purge -y \
+    && apt-get autoclean -y \
+    && dotnet tool install --global boogie  || true
+# to force a new clone after a new commit
+ADD https://api.github.com/repos/ailrst/compiler-explorer/branches/main /tmp/head 
+RUN rm -rf /var/cache/apt/* /tmp/* \
+    && git clone https://github.com/ailrst/compiler-explorer.git /compiler-explorer \
+    && cd /compiler-explorer \
+    && echo "Add missing dependencies" \
+    && npm i @sentry/node \
+    && npm run webpack
+WORKDIR /compiler-explorer
+RUN DEBIAN_FRONTEND=noninteractive apt-get update \
+    && apt-get install clang gcc gcc-13-aarch64-linux-gnu  binutils-aarch64-linux-gnu gcc-13-cross-base libc6-dev-arm64-cross libc6-dev-armel-cross libc6-dev-armhf-cross libc6-dev-i386 -y \
+    && apt-get autoclean -y
+ENTRYPOINT [ "make" ]
+CMD ["run"]
+
+FROM compiler-explorer AS  ghcr.io/uq-pac/basil-compiler-explorer:latest
+ADD docker/godbolt/basil-tool.py /compiler-explorer/basil-tool.py
+RUN chmod +x /compiler-explorer/basil-tool.py
+ADD docker/godbolt/basil.local.properties /compiler-explorer/etc/config/c.defaults.properties
+ADD docker/godbolt/compiler-explorer.local.properties /compiler-explorer/etc/config/compiler-explorer.local.properties