diff --git a/.bsp/mill-bsp.json b/.bsp/mill-bsp.json new file mode 100644 index 000000000..3e65df116 --- /dev/null +++ b/.bsp/mill-bsp.json @@ -0,0 +1 @@ +{"name":"mill-bsp","argv":["mill", "--bsp","--disable-ticker","--color","false","--jobs","1"],"millVersion":"0.11.6","bspVersion":"2.1.0-M7","languages":["scala","java"]} \ No newline at end of file diff --git a/.github/workflows/run-examples.yml b/.github/workflows/run-examples.yml index 071920207..da18138f2 100644 --- a/.github/workflows/run-examples.yml +++ b/.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: ./scripts/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: ./scripts/mill test.testOnly BitVectorAnalysisTests + - name: IntrusiveListTest + run: ./scripts/mill test.testOnly IntrusiveListPublicInterfaceTests + - name: System Tests + run: ./scripts/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: ./scripts/mill test.testOnly SystemTests || true diff --git a/.mill-version b/.mill-version new file mode 100644 index 000000000..e5cbde33e --- /dev/null +++ b/.mill-version @@ -0,0 +1 @@ +0.11.6 diff --git a/antlr.sc b/antlr.sc new file mode 100644 index 000000000..821eb966a --- /dev/null +++ b/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) +} diff --git a/build.sc b/build.sc new file mode 100644 index 000000000..dfe4b68c9 --- /dev/null +++ b/build.sc @@ -0,0 +1,75 @@ +import mill._, mill.define._, scalalib._ + +import $file.antlr // https://index.scala-lang.org/ml86/mill-antlr + +import os.Path + +object basil extends RootModule with ScalaModule with antlr.AntlrModule { + 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" + + def mainClass = Some("Main") + + + def millSourcePath = super.millSourcePath / "src" + def ivyDeps = Agg(scalactic, antlrRuntime, sourceCode, mainArgs) + 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(outPath, expectedPath) + } + } + } + } + } + } + + def filesContentEqual(path1: Path, path2: Path): Boolean = { + os.read(path1) == os.read(path2) + } + + expectedUpdate(correctPath, true) + expectedUpdate(incorrectPath, false) + } + +} diff --git a/compose.yaml b/compose.yaml index b4974a50f..e8a58588a 100644 --- a/compose.yaml +++ b/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: diff --git a/docker/asli.Dockerfile b/docker/asli.Dockerfile index 6e4d4333c..84ab0d8d1 100644 --- a/docker/asli.Dockerfile +++ b/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 diff --git a/docker/nixdocker.Dockerfile b/docker/nixdocker.Dockerfile new file mode 100644 index 000000000..5570dc4d9 --- /dev/null +++ b/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 + diff --git a/docker/readme.md b/docker/readme.md index 298c58883..d74ed08bc 100644 --- a/docker/readme.md +++ b/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 diff --git a/readme.md b/readme.md index e4446568a..20381f576 100644 --- a/readme.md +++ b/readme.md @@ -1,8 +1,8 @@ -# BAP-to-Boogie Translator +# BIL-to-Boogie Translator ## About -The BAP-to-Boogie Translator generates semantically equivalent Boogie source files (`.bpl`) from AArch64/ARM64 +The BIL-to-Boogie Translator generates semantically equivalent Boogie source files (`.bpl`) from AArch64/ARM64 binaries that have been lifted to the BAP (Binary Analysis Platform) intermediate ADT format. This repository contains a program which takes BAP adt files and readelf output as input, and produces a boogie program. @@ -10,13 +10,29 @@ This repository contains a program which takes BAP adt files and readelf output ### Example ```sh -$ sbt "run --adt src/test/correct/secret_write/clang/secret_write.adt --relf src/test/correct/secret_write/clang/secret_write.relf --s -pec src/test/correct/secret_write/secret_write.spec --output boogie_out.bpl" -[info] welcome to sbt 1.8.2 (Private Build Java 17.0.8) -... -[info] running Main --adt src/test/correct/secret_write/clang/secret_write.adt --relf src/test/correct/secret_write/clang/secret_write -.relf --spec src/test/correct/secret_write/secret_write.spec --output boogie_out.bpl -[success] Total time: 1 s, completed Sep 11, 2023, 7:24:11 AM +$ mill run +[53/53] run +Missing arguments: -a --adt -r --relf +Expected Signature: BASIL + -a --adt BAP ADT file name. + --analyse Run static analysis pass. + --analysis-results Log analysis results in files at specified path. + --analysis-results-dot Log analysis results in .dot form at specified path. + --boogie-use-lambda-stores Use lambda representation of store operations. + --dump-il Dump the Intermediate Language to text. + -h --help Show this help message. + --interpret Run BASIL IL interpreter. + -o --output Boogie output destination file. + -r --relf Name of the file containing the output of 'readelf -s -r -W'. + -s --spec BASIL specification file. + -v --verbose Show extra debugging logs. + +$ mill run --adt src/test/correct/secret_write/clang/secret_write.adt --relf src/test/correct/secret_write/clang/secret_write.relf --spec src/test/correct/secret_write/secret_write.spec --output boogie_out.bpl +[53/53] run +[INFO] [!] Writing file... [run@RunUtils.scala:65] +[INFO] [!] Removing external function calls [loadAndTranslate@RunUtils.scala:85] +[INFO] [!] Translating to Boogie [loadAndTranslate@RunUtils.scala:114] +[INFO] [!] Done! Exiting... [loadAndTranslate@RunUtils.scala:116] $ tail boogie_out.bpl mem, Gamma_mem := memory_store32_le(mem, bvadd64(R9, 52bv64), R8[32:0]), gamma_store32(Gamma_mem, bvadd64(R9, 52bv64), Gamma_R8); assert ((bvadd64(R9, 52bv64) == $z_addr) ==> (L(mem, $x_addr) ==> Gamma_x_old)); @@ -35,127 +51,108 @@ Boogie program verifier finished with 4 verified, 0 errors ## Installation and use -### Using Containers +This is a Scala 3 project using the [mill](mill-build.com) build system, it can be run with `mill run`. -(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 +### Local Development -##### From github +The tool is a Scala project, and is therefore OS-independent, but is only tested under linux. -`podman pull ghcr.io/uq-pac/basil-dev:latest` +Furthermore, lifting input files from a given AArch64 binary is Linux-specific, and all commands given are for Linux. +On Windows, WSL2 may be used to run any Linux-specific tasks, but it is less thoroughly tested. -##### Build the images +Installing [mill](https://mill-build.com/mill/Installation_IDE_Support.html) or [sbt](https://www.scala-sbt.org/download.html) and [JDK >= 17](https://openjdk.org/install/) is required. -To build the images, from the root of the respository run +This can be done via [coursier](https://get-coursier.io/docs/cli-overview). -``` -podman-compose build -``` +A mill script is checked in at `./scripts/mill` so it does not need to be installed. -#### 2. Use the images with compose +#### IDE Support -Individual services can be built with `podman compose build $servicename` from the root of the repo. +Mill supports the Metals language server and IntelliJ through Build Server Protocol (BSP), which is the recommended use. -The services provided are: +SBT has an intellij plugin in addition to BSP. -- `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. +### Note about using sbt with IntelliJ -Or enter the dev container manually, mounting the current directory (the same as podman-compose basil-dev). +[See Also](https://github.com/UQ-PAC/bil-to-boogie-translator/wiki/Development) +The project uses sbt to build the project. For the most part this should *just work*, and there are IntelliJ run files (located in the .run folder) which automatically compile and run the project. +However, to prevent some issues in IntelliJ, it is necessary to unmark `target/scala-3.1.0/src_managed/` as a sources root folder, in the `File > Project Structure > Modules` dialog. -#### 2. Use the images manually -##### Compiler Explorer Container +--- -```sh -podman pull ghcr.io/uq-pac/basil-compiler-explorer:latest -``` +The tool takes as inputs a BAP ADT file (here denoted with `.adt`) and a file containing the output of readelf (here denoted with `.relf`), both created from the same AArch64/ARM64 binary, and outputs a semantically equivalent .bpl Boogie-language source file. The default output file is `boogie_out.bpl`, but the output location can be specified. +To build and run the tool using sbt, use the following command: -```sh -podman-compose run compiler-explorer -``` +`sbt "run --adt file.adt --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]"` where the output filename is optional and specification filenames are optional. The specification filename must end in `.spec`. -OR +or mill: -``` -podman run -p 10240:10240 ghcr.io/uq-pac/basil-compiler-explorer:latest -``` +`sbt run --adt file.adt --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]`. -##### Development/Testing Container +#### Usage -This mounts the current directory as the working directory of the container. +The `--analyse` flag is optional and enables the static analysis functionality which resolves indirect calls where possible. ``` -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 +Expected Signature: BASIL + -a --adt BAP ADT file name. + --analyse Run static analysis pass. + --analysis-results Log analysis results in files at specified path. + --analysis-results-dot Log analysis results in .dot form at specified path. + --boogie-use-lambda-stores Use lambda representation of store operations. + --dump-il Dump the Intermediate Language to text. + -h --help Show this help message. + --interpret Run BASIL IL interpreter. + -o --output Boogie output destination file. + -r --relf Name of the file containing the output of 'readelf -s -r -W'. + -s --spec BASIL specification file. + -v --verbose Show extra debugging logs. ``` -### Local Development +The sbt shell can also be used for multiple tasks with less overhead by executing `sbt` and then the relevant sbt commands. -See: [Wiki Development Page](https://github.com/UQ-PAC/bil-to-boogie-translator/wiki/Development). +To build a standalone `.jar` file, use the following command: -The tool is a Scala project, and is therefore OS-independent, but is only tested under linux. +`mill assembly` -Furthermore, lifting input files from a given AArch64 binary is Linux-specific, and all commands given are for Linux. -On Windows, WSL2 may be used to run any Linux-specific tasks, but it is less thoroughly tested. +From `sbt` the resulting `.jar` is located at `target/scala-3.1.0/wptool-boogie-assembly-0.0.1.jar` and from +`mill` this is `out/assembly.dest/out.jar`. -Installing [sbt](https://www.scala-sbt.org/download.html) and [JDK 17](https://openjdk.org/install/) is required. +To compile the source without running it - this helps IntelliJ highlight things properly: -The tool takes as inputs a BAP ADT file (here denoted with `.adt`) and a file containing the output of readelf (here denoted with `.relf`), both created from the same AArch64/ARM64 binary, and outputs a semantically equivalent .bpl Boogie-language source file. The default output file is `boogie_out.bpl`, but the output location can be specified. +`mill compile` -To build and run the tool using sbt, use the following command: -`sbt "run --adt file.adt --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]"` where the output filename is optional and specification filenames are optional. The specification filename must end in `.spec`. +#### Running Tests -#### Usage +The test suites use [ScalaTest](https://www.scalatest.org/), they can be run via. -The `--analyse` flag is optional and enables the static analysis functionality. +``` +$ mill test +``` +To run a single test suite, for example only the system tests (requires boogie): ``` -BASIL - -a --adt BAP ADT file name. - -r --relf Output of 'readelf -s -r -W'. - -s --spec BASIL specification file. - -o --output Boogie output destination file. - -v --verbose Show extra debugging logs. - --analyse Run static analysis pass. - --interpret Run BASIL IR interpreter. - -h --help Show this help message. +$ mill.test.testOnly SystemTests ``` -The sbt shell can also be used for multiple tasks with less overhead by executing `sbt` and then the relevant sbt commands. +To run single tests in from the test suite: -To build a standalone `.jar` file, use the following command: - -`sbt assembly` +``` +$ mill test.testOnly SystemTests -- -z basic_arrays_read -z basic_arrays_write +``` -This is located at `target/scala-3.1.0/wptool-boogie-assembly-0.0.1.jar`. +To update the expected basil output files from the test results run -To compile the source without running it - this helps IntelliJ highlight things properly: +``` +$ mill updateExpected +``` -`sbt compile` +This is used to keep track of which tests have passed previously, as well as changes to the basil output. ## Generating inputs (Lifting) @@ -168,13 +165,15 @@ The tool takes a `.adt` and a `.relf` file as inputs, which are produced by BAP - `bap` with the ASLp plugin - `readelf` -- cross-compiliation toolchains: +- cross-compiliation toolchains, e.g.: - `gcc-13-aarch64-linux-gnu` - `clang` -[BAP](https://github.com/BinaryAnalysisPlatform/bap) can be installed by following the instructions in the link given. +This can be installed using the [nix packages](https://github.com/katrinafyi/pac-nix). -This can also be installed using the [nix package](https://github.com/katrinafyi/pac-nix). +The `dev` podman container also contains these tools and can be used by mounting current directory into the container as described at [docker/readme.md](docker/readme.md). + +[BAP](https://github.com/BinaryAnalysisPlatform/bap) can be installed by following the instructions in the link given. Given a AArch64/ARM64 binary file (`*.out`), the `.adt` file can be produced by running @@ -182,7 +181,7 @@ Given a AArch64/ARM64 binary file (`*.out`), the `.adt` file can be produced by and the `.relf` file can be produced by running -`readelf -s -r -W *.out > *.relf`. +`aarch64-linux-gnu-readelf -s -r -W *.out > *.relf`. To cross-compile a C source file to a AArch64 binary, `gcc-aarch64-linux-gnu` must be installed. This can be done with the following commands on Ubuntu: @@ -207,20 +206,15 @@ It is recommended to use Boogie version 3.0.4 and Z3 version 4.8.8 (which is rec The `\useArrayAxioms` flag is necessary for Boogie versions 2.16.8 and greater; for earlier versions it can be removed. +### Installing boogie + Boogie can be installed through dotnet and requires dotnet 6. ``` -sudo apt-get install dotnet-sdk-6.0 +sudo apt-get install dotnet6 dotnet install boogie ``` -### Note about using sbt with IntelliJ - -[See Also](https://github.com/UQ-PAC/bil-to-boogie-translator/wiki/Development) - -The project uses sbt to build the project. For the most part this should *just work*, and there are IntelliJ run files (located in the .run folder) which automatically compile and run the project. -However, to prevent some issues in IntelliJ, it is necessary to unmark `target/scala-3.1.0/src_managed/` as a sources root folder, in the `File > Project Structure > Modules` dialog. - ## Other useful commands To compile a C file without the global offset table being used in address calculation, use the following command: diff --git a/scripts/mill b/scripts/mill new file mode 100755 index 000000000..9d343ff64 --- /dev/null +++ b/scripts/mill @@ -0,0 +1,241 @@ +#!/usr/bin/env sh + +# This is a wrapper script, that automatically download mill from GitHub release pages +# You can give the required mill version with --mill-version parameter +# If no version is given, it falls back to the value of DEFAULT_MILL_VERSION +# +# Project page: https://github.com/lefou/millw +# Script Version: 0.4.11 +# +# If you want to improve this script, please also contribute your changes back! +# +# Licensed under the Apache License, Version 2.0 + +set -e + +if [ -z "${DEFAULT_MILL_VERSION}" ] ; then + DEFAULT_MILL_VERSION="0.11.4" +fi + + +if [ -z "${GITHUB_RELEASE_CDN}" ] ; then + GITHUB_RELEASE_CDN="" +fi + + +MILL_REPO_URL="https://github.com/com-lihaoyi/mill" + +if [ -z "${CURL_CMD}" ] ; then + CURL_CMD=curl +fi + +# Explicit commandline argument takes precedence over all other methods +if [ "$1" = "--mill-version" ] ; then + shift + if [ "x$1" != "x" ] ; then + MILL_VERSION="$1" + shift + else + echo "You specified --mill-version without a version." 1>&2 + echo "Please provide a version that matches one provided on" 1>&2 + echo "${MILL_REPO_URL}/releases" 1>&2 + false + fi +fi + +# Please note, that if a MILL_VERSION is already set in the environment, +# We reuse it's value and skip searching for a value. + +# If not already set, read .mill-version file +if [ -z "${MILL_VERSION}" ] ; then + if [ -f ".mill-version" ] ; then + MILL_VERSION="$(head -n 1 .mill-version 2> /dev/null)" + elif [ -f ".config/mill-version" ] ; then + MILL_VERSION="$(head -n 1 .config/mill-version 2> /dev/null)" + fi +fi + +MILL_USER_CACHE_DIR="${XDG_CACHE_HOME:-${HOME}/.cache}/mill" + +if [ -z "${MILL_DOWNLOAD_PATH}" ] ; then + MILL_DOWNLOAD_PATH="${MILL_USER_CACHE_DIR}/download" +fi + +# If not already set, try to fetch newest from Github +if [ -z "${MILL_VERSION}" ] ; then + # TODO: try to load latest version from release page + echo "No mill version specified." 1>&2 + echo "You should provide a version via '.mill-version' file or --mill-version option." 1>&2 + + mkdir -p "${MILL_DOWNLOAD_PATH}" + LANG=C touch -d '1 hour ago' "${MILL_DOWNLOAD_PATH}/.expire_latest" 2>/dev/null || ( + # we might be on OSX or BSD which don't have -d option for touch + # but probably a -A [-][[hh]mm]SS + touch "${MILL_DOWNLOAD_PATH}/.expire_latest"; touch -A -010000 "${MILL_DOWNLOAD_PATH}/.expire_latest" + ) || ( + # in case we still failed, we retry the first touch command with the intention + # to show the (previously suppressed) error message + LANG=C touch -d '1 hour ago' "${MILL_DOWNLOAD_PATH}/.expire_latest" + ) + + # POSIX shell variant of bash's -nt operator, see https://unix.stackexchange.com/a/449744/6993 + # if [ "${MILL_DOWNLOAD_PATH}/.latest" -nt "${MILL_DOWNLOAD_PATH}/.expire_latest" ] ; then + if [ -n "$(find -L "${MILL_DOWNLOAD_PATH}/.latest" -prune -newer "${MILL_DOWNLOAD_PATH}/.expire_latest")" ]; then + # we know a current latest version + MILL_VERSION=$(head -n 1 "${MILL_DOWNLOAD_PATH}"/.latest 2> /dev/null) + fi + + if [ -z "${MILL_VERSION}" ] ; then + # we don't know a current latest version + echo "Retrieving latest mill version ..." 1>&2 + LANG=C ${CURL_CMD} -s -i -f -I ${MILL_REPO_URL}/releases/latest 2> /dev/null | grep --ignore-case Location: | sed s'/^.*tag\///' | tr -d '\r\n' > "${MILL_DOWNLOAD_PATH}/.latest" + MILL_VERSION=$(head -n 1 "${MILL_DOWNLOAD_PATH}"/.latest 2> /dev/null) + fi + + if [ -z "${MILL_VERSION}" ] ; then + # Last resort + MILL_VERSION="${DEFAULT_MILL_VERSION}" + echo "Falling back to hardcoded mill version ${MILL_VERSION}" 1>&2 + else + echo "Using mill version ${MILL_VERSION}" 1>&2 + fi +fi + +MILL="${MILL_DOWNLOAD_PATH}/${MILL_VERSION}" + +try_to_use_system_mill() { + if [ "$(uname)" != "Linux" ]; then + return 0 + fi + + MILL_IN_PATH="$(command -v mill || true)" + + if [ -z "${MILL_IN_PATH}" ]; then + return 0 + fi + + SYSTEM_MILL_FIRST_TWO_BYTES=$(head --bytes=2 "${MILL_IN_PATH}") + if [ "${SYSTEM_MILL_FIRST_TWO_BYTES}" = "#!" ]; then + # MILL_IN_PATH is (very likely) a shell script and not the mill + # executable, ignore it. + return 0 + fi + + SYSTEM_MILL_PATH=$(readlink -e "${MILL_IN_PATH}") + SYSTEM_MILL_SIZE=$(stat --format=%s "${SYSTEM_MILL_PATH}") + SYSTEM_MILL_MTIME=$(stat --format=%y "${SYSTEM_MILL_PATH}") + + if [ ! -d "${MILL_USER_CACHE_DIR}" ]; then + mkdir -p "${MILL_USER_CACHE_DIR}" + fi + + SYSTEM_MILL_INFO_FILE="${MILL_USER_CACHE_DIR}/system-mill-info" + if [ -f "${SYSTEM_MILL_INFO_FILE}" ]; then + parseSystemMillInfo() { + LINE_NUMBER="${1}" + # Select the line number of the SYSTEM_MILL_INFO_FILE, cut the + # variable definition in that line in two halves and return + # the value, and finally remove the quotes. + sed -n "${LINE_NUMBER}p" "${SYSTEM_MILL_INFO_FILE}" |\ + cut -d= -f2 |\ + sed 's/"\(.*\)"/\1/' + } + + CACHED_SYSTEM_MILL_PATH=$(parseSystemMillInfo 1) + CACHED_SYSTEM_MILL_VERSION=$(parseSystemMillInfo 2) + CACHED_SYSTEM_MILL_SIZE=$(parseSystemMillInfo 3) + CACHED_SYSTEM_MILL_MTIME=$(parseSystemMillInfo 4) + + if [ "${SYSTEM_MILL_PATH}" = "${CACHED_SYSTEM_MILL_PATH}" ] \ + && [ "${SYSTEM_MILL_SIZE}" = "${CACHED_SYSTEM_MILL_SIZE}" ] \ + && [ "${SYSTEM_MILL_MTIME}" = "${CACHED_SYSTEM_MILL_MTIME}" ]; then + if [ "${CACHED_SYSTEM_MILL_VERSION}" = "${MILL_VERSION}" ]; then + MILL="${SYSTEM_MILL_PATH}" + return 0 + else + return 0 + fi + fi + fi + + SYSTEM_MILL_VERSION=$(${SYSTEM_MILL_PATH} --version | head -n1 | sed -n 's/^Mill.*version \(.*\)/\1/p') + + cat < "${SYSTEM_MILL_INFO_FILE}" +CACHED_SYSTEM_MILL_PATH="${SYSTEM_MILL_PATH}" +CACHED_SYSTEM_MILL_VERSION="${SYSTEM_MILL_VERSION}" +CACHED_SYSTEM_MILL_SIZE="${SYSTEM_MILL_SIZE}" +CACHED_SYSTEM_MILL_MTIME="${SYSTEM_MILL_MTIME}" +EOF + + if [ "${SYSTEM_MILL_VERSION}" = "${MILL_VERSION}" ]; then + MILL="${SYSTEM_MILL_PATH}" + fi +} +try_to_use_system_mill + +# If not already downloaded, download it +if [ ! -s "${MILL}" ] ; then + + # support old non-XDG download dir + MILL_OLD_DOWNLOAD_PATH="${HOME}/.mill/download" + OLD_MILL="${MILL_OLD_DOWNLOAD_PATH}/${MILL_VERSION}" + if [ -x "${OLD_MILL}" ] ; then + MILL="${OLD_MILL}" + else + case $MILL_VERSION in + 0.0.* | 0.1.* | 0.2.* | 0.3.* | 0.4.* ) + DOWNLOAD_SUFFIX="" + DOWNLOAD_FROM_MAVEN=0 + ;; + 0.5.* | 0.6.* | 0.7.* | 0.8.* | 0.9.* | 0.10.* | 0.11.0-M* ) + DOWNLOAD_SUFFIX="-assembly" + DOWNLOAD_FROM_MAVEN=0 + ;; + *) + DOWNLOAD_SUFFIX="-assembly" + DOWNLOAD_FROM_MAVEN=1 + ;; + esac + + DOWNLOAD_FILE=$(mktemp mill.XXXXXX) + + if [ "$DOWNLOAD_FROM_MAVEN" = "1" ] ; then + DOWNLOAD_URL="https://repo1.maven.org/maven2/com/lihaoyi/mill-dist/${MILL_VERSION}/mill-dist-${MILL_VERSION}.jar" + else + MILL_VERSION_TAG=$(echo "$MILL_VERSION" | sed -E 's/([^-]+)(-M[0-9]+)?(-.*)?/\1\2/') + DOWNLOAD_URL="${GITHUB_RELEASE_CDN}${MILL_REPO_URL}/releases/download/${MILL_VERSION_TAG}/${MILL_VERSION}${DOWNLOAD_SUFFIX}" + unset MILL_VERSION_TAG + fi + + # TODO: handle command not found + echo "Downloading mill ${MILL_VERSION} from ${DOWNLOAD_URL} ..." 1>&2 + ${CURL_CMD} -f -L -o "${DOWNLOAD_FILE}" "${DOWNLOAD_URL}" + chmod +x "${DOWNLOAD_FILE}" + mkdir -p "${MILL_DOWNLOAD_PATH}" + mv "${DOWNLOAD_FILE}" "${MILL}" + + unset DOWNLOAD_FILE + unset DOWNLOAD_SUFFIX + fi +fi + +if [ -z "$MILL_MAIN_CLI" ] ; then + MILL_MAIN_CLI="${0}" +fi + +MILL_FIRST_ARG="" +if [ "$1" = "--bsp" ] || [ "$1" = "-i" ] || [ "$1" = "--interactive" ] || [ "$1" = "--no-server" ] || [ "$1" = "--repl" ] || [ "$1" = "--help" ] ; then + # Need to preserve the first position of those listed options + MILL_FIRST_ARG=$1 + shift +fi + +unset MILL_DOWNLOAD_PATH +unset MILL_OLD_DOWNLOAD_PATH +unset OLD_MILL +unset MILL_VERSION +unset MILL_REPO_URL + +# We don't quote MILL_FIRST_ARG on purpose, so we can expand the empty value without quotes +# shellcheck disable=SC2086 +exec "${MILL}" $MILL_FIRST_ARG -D "mill.main.cli=${MILL_MAIN_CLI}" "$@" diff --git a/scripts/mill.bat b/scripts/mill.bat new file mode 100644 index 000000000..5c3c3b2e8 --- /dev/null +++ b/scripts/mill.bat @@ -0,0 +1,220 @@ +@echo off + +rem This is a wrapper script, that automatically download mill from GitHub release pages +rem You can give the required mill version with --mill-version parameter +rem If no version is given, it falls back to the value of DEFAULT_MILL_VERSION +rem +rem Project page: https://github.com/lefou/millw +rem Script Version: 0.4.11 +rem +rem If you want to improve this script, please also contribute your changes back! +rem +rem Licensed under the Apache License, Version 2.0 + +rem setlocal seems to be unavailable on Windows 95/98/ME +rem but I don't think we need to support them in 2019 +setlocal enabledelayedexpansion + +if [!DEFAULT_MILL_VERSION!]==[] ( + set "DEFAULT_MILL_VERSION=0.11.4" +) + +if [!GITHUB_RELEASE_CDN!]==[] ( + set "GITHUB_RELEASE_CDN=" +) + +if [!MILL_MAIN_CLI!]==[] ( + set "MILL_MAIN_CLI=%~f0" +) + +set "MILL_REPO_URL=https://github.com/com-lihaoyi/mill" + +rem %~1% removes surrounding quotes +if [%~1%]==[--mill-version] ( + if not [%~2%]==[] ( + set MILL_VERSION=%~2% + rem shift command doesn't work within parentheses + set "STRIP_VERSION_PARAMS=true" + ) else ( + echo You specified --mill-version without a version. 1>&2 + echo Please provide a version that matches one provided on 1>&2 + echo %MILL_REPO_URL%/releases 1>&2 + exit /b 1 + ) +) + +if not defined STRIP_VERSION_PARAMS GOTO AfterStripVersionParams +rem strip the: --mill-version {version} +shift +shift +:AfterStripVersionParams + +if [!MILL_VERSION!]==[] ( + if exist .mill-version ( + set /p MILL_VERSION=<.mill-version + ) else ( + if exist .config\mill-version ( + set /p MILL_VERSION=<.config\mill-version + ) + ) +) + +if [!MILL_VERSION!]==[] ( + set MILL_VERSION=%DEFAULT_MILL_VERSION% +) + +if [!MILL_DOWNLOAD_PATH!]==[] ( + set MILL_DOWNLOAD_PATH=%USERPROFILE%\.mill\download +) + +rem without bat file extension, cmd doesn't seem to be able to run it +set MILL=%MILL_DOWNLOAD_PATH%\!MILL_VERSION!.bat + +if not exist "%MILL%" ( + set VERSION_PREFIX=%MILL_VERSION:~0,4% + # Since 0.5.0 + set DOWNLOAD_SUFFIX=-assembly + # Since 0.11.0 + set DOWNLOAD_FROM_MAVEN=1 + if [!VERSION_PREFIX!]==[0.0.] ( + set DOWNLOAD_SUFFIX= + set DOWNLOAD_FROM_MAVEN=0 + ) + if [!VERSION_PREFIX!]==[0.1.] ( + set DOWNLOAD_SUFFIX= + set DOWNLOAD_FROM_MAVEN=0 + ) + if [!VERSION_PREFIX!]==[0.2.] ( + set DOWNLOAD_SUFFIX= + set DOWNLOAD_FROM_MAVEN=0 + ) + if [!VERSION_PREFIX!]==[0.3.] ( + set DOWNLOAD_SUFFIX= + set DOWNLOAD_FROM_MAVEN=0 + ) + if [!VERSION_PREFIX!]==[0.4.] ( + set DOWNLOAD_SUFFIX= + set DOWNLOAD_FROM_MAVEN=0 + ) + if [!VERSION_PREFIX!]==[0.5.] ( + set DOWNLOAD_FROM_MAVEN=0 + ) + if [!VERSION_PREFIX!]==[0.6.] ( + set DOWNLOAD_FROM_MAVEN=0 + ) + if [!VERSION_PREFIX!]==[0.7.] ( + set DOWNLOAD_FROM_MAVEN=0 + ) + if [!VERSION_PREFIX!]==[0.8.] ( + set DOWNLOAD_FROM_MAVEN=0 + ) + if [!VERSION_PREFIX!]==[0.9.] ( + set DOWNLOAD_FROM_MAVEN=0 + ) + set VERSION_PREFIX=%MILL_VERSION:~0,5% + if [!VERSION_PREFIX!]==[0.10.] ( + set DOWNLOAD_FROM_MAVEN=0 + ) + set VERSION_PREFIX=%MILL_VERSION:~0,8% + if [!VERSION_PREFIX!]==[0.11.0-M] ( + set DOWNLOAD_FROM_MAVEN=0 + ) + set VERSION_PREFIX= + + for /F "delims=- tokens=1" %%A in ("!MILL_VERSION!") do set MILL_VERSION_BASE=%%A + for /F "delims=- tokens=2" %%A in ("!MILL_VERSION!") do set MILL_VERSION_MILESTONE=%%A + set VERSION_MILESTONE_START=!MILL_VERSION_MILESTONE:~0,1! + if [!VERSION_MILESTONE_START!]==[M] ( + set MILL_VERSION_TAG="!MILL_VERSION_BASE!-!MILL_VERSION_MILESTONE!" + ) else ( + set MILL_VERSION_TAG=!MILL_VERSION_BASE! + ) + + rem there seems to be no way to generate a unique temporary file path (on native Windows) + set DOWNLOAD_FILE=%MILL%.tmp + + if [!DOWNLOAD_FROM_MAVEN!]==[1] ( + set DOWNLOAD_URL=https://repo1.maven.org/maven2/com/lihaoyi/mill-dist/!MILL_VERSION!/mill-dist-!MILL_VERSION!.jar + ) else ( + set DOWNLOAD_URL=!GITHUB_RELEASE_CDN!%MILL_REPO_URL%/releases/download/!MILL_VERSION_TAG!/!MILL_VERSION!!DOWNLOAD_SUFFIX! + ) + + echo Downloading mill %MILL_VERSION% from !DOWNLOAD_URL! ... 1>&2 + + if not exist "%MILL_DOWNLOAD_PATH%" mkdir "%MILL_DOWNLOAD_PATH%" + rem curl is bundled with recent Windows 10 + rem but I don't think we can expect all the users to have it in 2019 + where /Q curl + if %ERRORLEVEL% EQU 0 ( + curl -f -L "!DOWNLOAD_URL!" -o "!DOWNLOAD_FILE!" + ) else ( + rem bitsadmin seems to be available on Windows 7 + rem without /dynamic, github returns 403 + rem bitsadmin is sometimes needlessly slow but it looks better with /priority foreground + bitsadmin /transfer millDownloadJob /dynamic /priority foreground "!DOWNLOAD_URL!" "!DOWNLOAD_FILE!" + ) + if not exist "!DOWNLOAD_FILE!" ( + echo Could not download mill %MILL_VERSION% 1>&2 + exit /b 1 + ) + + move /y "!DOWNLOAD_FILE!" "%MILL%" + + set DOWNLOAD_FILE= + set DOWNLOAD_SUFFIX= +) + +set MILL_DOWNLOAD_PATH= +set MILL_VERSION= +set MILL_REPO_URL= + +rem Need to preserve the first position of those listed options +set MILL_FIRST_ARG= +if [%~1%]==[--bsp] ( + set MILL_FIRST_ARG=%1% +) else ( + if [%~1%]==[-i] ( + set MILL_FIRST_ARG=%1% + ) else ( + if [%~1%]==[--interactive] ( + set MILL_FIRST_ARG=%1% + ) else ( + if [%~1%]==[--no-server] ( + set MILL_FIRST_ARG=%1% + ) else ( + if [%~1%]==[--repl] ( + set MILL_FIRST_ARG=%1% + ) else ( + if [%~1%]==[--help] ( + set MILL_FIRST_ARG=%1% + ) + ) + ) + ) + ) +) + +set "MILL_PARAMS=%*%" + +if not [!MILL_FIRST_ARG!]==[] ( + if defined STRIP_VERSION_PARAMS ( + for /f "tokens=1-3*" %%a in ("%*") do ( + set "MILL_PARAMS=%%d" + ) + ) else ( + for /f "tokens=1*" %%a in ("%*") do ( + set "MILL_PARAMS=%%b" + ) + ) +) else ( + if defined STRIP_VERSION_PARAMS ( + for /f "tokens=1-2*" %%a in ("%*") do ( + rem strip %%a - It's the "--mill-version" option. + rem strip %%b - it's the version number that comes after the option. + rem keep %%c - It's the remaining options. + set "MILL_PARAMS=%%c" + ) + ) +) + +"%MILL%" %MILL_FIRST_ARG% -D "mill.main.cli=%MILL_MAIN_CLI%" %MILL_PARAMS%