Merge pull request #59 from UQ-PAC/readme-updates

Readme updates

compose.yaml

@@ -1,12 +1,4 @@
 services:
-  bap:
-    image: bap-2.5-aslp
-    build:
-      dockerfile: docker/asli.Dockerfile 
-      target: aslp-bap 
-    volumes:
-      - ./:/host:rw
-    working_dir: /host
   basil-build:
     image: basil:build
     build:
@@ -31,3 +23,11 @@ services:
     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/godbolt.Dockerfile

@@ -28,8 +28,8 @@ RUN DEBIAN_FRONTEND=noninteractive apt-get update \
 ENTRYPOINT [ "make" ]
 CMD ["run"]
 
-from compiler-explorer AS  ghcr.io/uq-pac/basil-compiler-explorer:latest
-ADD basil-tool.py /compiler-explorer/basil-tool.py
+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 basil.local.properties /compiler-explorer/etc/config/c.defaults.properties
-ADD compiler-explorer.local.properties /compiler-explorer/etc/config/compiler-explorer.local.properties
+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

docker/basil-tool.py → docker/godbolt/basil-tool.py

@@ -113,9 +113,9 @@ def run_basil(tmp_dir: str, spec: str | None =None):
     readelf_file = outputs['relf']
     os.chdir(tmp_dir) # so  the output file is in the right dir
     command = f"java -jar /target/scala-3.1.0/wptool-boogie-assembly-0.0.1.jar".split(" ")
-    files = [adtfile, readelf_file]
+    files = ["-a", adtfile, "-r", readelf_file, "-o", boogie_file]
     if spec:
-        files = [adtfile, readelf_file, spec]
+        files += ["-s", spec]
         outputs["spec"] = spec 
     command += files
     logging.info(command)

docker/readme.md

@@ -1,25 +1,25 @@
 
-- asli is compiled from a git checkout of the default branch
-- bap 2.5 is compiled from opam 
-- basil is compiled from the current staet of this checkout 
-
-The provided compose targets are 
-
-- bap
-    - bap with the asli plugin
-- basil-build
-    - build basil inside a docker container, run this to enter a bash prompt inside the container with the repo mounted
-- basil-dev
-    - the basil build environment with bap and the asli plugin transplanted into it, used for building into the host 
-    environment using the toolchain provided by the container
-- basil
-    - a smaller container containng just the, bap, basil and cross-compiler binaries
 
 ---
 
-Compiling godbolt container
+#### Publishing container images to github registry:
+
+- This only needs to be done when the docker images are modified or you wish to 
+make a new version of basil available. Only the dev environment is used 
+by the github actions.
+
+1. Create a github access token with the priviledge to write to packages
+2. Login to repository with podman
 
 ```
-podman build -f docker/godbolt.Dockerfile -t ghcr.io/uq-pac/basil-compiler-explorer:latest
-podman push ghcr.io/uq-pac/basil-compiler-explorer:latest
+$ podman login ghcr.io -u $username
+Password: <enter github acccess token>
 ```
+
+3. Push the container
+
+```
+$ podman-compose push basil
+$ podman-compose push basil-dev
+```
+

readme.md

@@ -1,32 +1,70 @@
 # BAP-to-Boogie Translator
 
 ## About
-The BAP-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. 
+
+The BAP-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.
+
+### 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
+$ 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));
+    assert bvsge32(memory_load32_le(mem, $z_addr), z_old);
+    main_argv_out, Gamma_main_argv_out := R1, Gamma_R1;
+    main_result, Gamma_main_result := R0[32:0], Gamma_R0;
+    FP_out, Gamma_FP_out := R29, Gamma_R29;
+    LR_out, Gamma_LR_out := R30, Gamma_R30;
+    SP_out, Gamma_SP_out := R31, Gamma_R31;
+    return;
+}
+$ boogie boogie_out.bpl 
+
+Boogie program verifier finished with 4 verified, 0 errors
+```
 
 ## Installation and use
 
 ### 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
 
-Note it is recommended to use `podman` rather than docker.
+#### 1. Obtain the image image
+
+##### From github 
 
-1. To build the images, from the root of the respository run
+`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:
 
-- `bap`
-   - To invoke bap on its own: `podman-compose run bap`
 - `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`
@@ -39,48 +77,59 @@ The services provided are:
       - `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. 
 
-#### Compiler Explorer Container
+Or enter the dev container manually, mounting the current directory (the same as podman-compose basil-dev).
 
-```
-podman run -p 10240:10240 ghcr.io/uq-pac/basil-compiler-explorer:latest
-```
 
----
+#### 2. Use the images manually  
+
+##### Compiler Explorer Container
+
+```sh
+podman pull ghcr.io/uq-pac/basil-compiler-explorer:latest
+```
 
-#### Publishing container images to github registry:
 
-- This only needs to be done when the docker images are modified or you wish to 
-make a new version of basil available. Only the dev environment is used 
-by the github actions.
+```sh
+podman-compose run compiler-explorer
+```
 
-1. Create a github access token with the priviledge to write to packages
-2. Login to repository with podman
+OR
 
 ```
-$ podman login ghcr.io -u $username
-Password: <enter github acccess token>
+podman run -p 10240:10240 ghcr.io/uq-pac/basil-compiler-explorer:latest
 ```
 
-3. Push the container
+##### Development/Testing Container
+
+This mounts the current directory as the working directory of the container.
 
 ```
-$ podman-compose push basil
-$ podman-compose push basil-dev
+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
 ```
 
-### Native
+### Local Development 
 
-The tool is OS-independent, but producing input files from a given AArch64 binary is Linux-specific, and all commands given are for Linux. On Windows, WSL2 can be used to run any Linux-specific tasks.
+See: [Wiki Development Page](https://github.com/UQ-PAC/bil-to-boogie-translator/wiki/Development).
 
-Installing [sbt](https://www.scala-sbt.org/download.html) and [JDK 17](https://openjdk.org/install/) (or higher) is required.
+The tool is a Scala project, and is therefore OS-independent, but is only tested under linux. 
+
+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.
+
+Installing [sbt](https://www.scala-sbt.org/download.html) and [JDK 17](https://openjdk.org/install/) is required.
 
 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:
 
 `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`.
 
+#### Usage
+
 The `--analyse` flag is optional and enables the static analysis functionality.
 
 
@@ -108,11 +157,25 @@ To compile the source without running it - this helps IntelliJ highlight things
 
 `sbt compile`
 
-## Generating inputs
+## Generating inputs (Lifting)
+
+Many lifted examples are already profied in the tests directory: [src/test/correct](src/test/correct), these instructions
+are for if you want to lift new compiled binaries.
+
 The tool takes a `.adt` and a `.relf` file as inputs, which are produced by BAP and readelf, respectively.
 
+### Requirements
+
+- `bap` with the ASLp plugin
+- `readelf`
+- cross-compiliation toolchains:
+    - `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 also be installed using the [nix package](https://github.com/katrinafyi/pac-nix).
+
 Given a AArch64/ARM64 binary file (`*.out`), the `.adt` file can be produced by running
 
 `bap *.out -d adt:*.adt`
@@ -131,30 +194,36 @@ The binary (i.e `*.out`) can then be generated from a C source file using:
 
 `aarch64-linux-gnu-gcc *.c -o *.out`
 
-To compile a binary from a C source and immediately generate the required .adt and .relf files, the following command can be used:
+See [src/test/correct/liftone.sh](https://github.com/UQ-PAC/bil-to-boogie-translator/blob/main/src/test/correct/liftone.sh) for more examples
+for flag combinations that work. 
 
-`./lift.sh *.c *.adt *.relf` where `*.adt` and `*.relf` are the output file names.
+## Verifying the generated boogie (the programming language), by running boogie (the progam) on the boogie (the program)
 
-To compile a C source and then run the tool on it, generating the required files first, the following command can be used:
-
-`./run_c.sh *.c [output.bpl]` where the output filename is optional (requires `sbt assembly` first)
+[Boogie](https://github.com/boogie-org/boogie#installation) can be installed by following the instructions in the given link.
 
-To generate the required files from a AArch64 binary and then run the tool on it, the following command can be used:
+Boogie can be run on the output `*.bpl` file with the command `boogie *.bpl`. 
 
-`./run_binary.sh *.c [output.bpl]` where the output filename is optional (requires `sbt assembly` first)
+A recent boogie version is needed, for example `Boogie program verifier version 2.4.1.10503, Copyright (c) 2003-2014, Microsoft.`. 
 
-## Running Boogie on output .bpl
+With older versions and recent versions of z3 (e.g. `Z3 version 4.8.12 - 64 bit`), Z3 emits warnings about `model_compress`, since the 
+parameter name was changed. This does not prevent it from working however. 
 
-[Boogie](https://github.com/boogie-org/boogie#installation) can be installed by following the instructions in the given link.
+Boogie can be installed through dotnet and requires dotnet 6.
 
-Boogie can be run on the output `.bpl` file with the command `boogie *.bpl`. At present, there are no verification conditions, so this is just a syntax check.
+```
+sudo apt-get install dotnet-sdk-6.0
+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:
 
 `aarch64-linux-gnu-gcc -fno-plt -fno-pic *.c -o *.out`