Add Docker file

README.md

@@ -4,14 +4,18 @@
 
 ## Install dependencies
 
-- llvm-9
-- llvm-9-tools
+If you want to install Sys locally:
+
+- llvm-9, llvm-9-tools
 - [boolector](https://github.com/Boolector/boolector) configured with
   `--shared` option. See the `build()` and `package()` functions in [this
   file](https://aur.archlinux.org/cgit/aur.git/tree/PKGBUILD?h=boolector-git)
   as an example of how to install boolector after you clone it.
+  On Arch Linux, you can just install `boolector-git` from AUR.
 - The Haskell tool [Stack](https://docs.haskellstack.org/en/stable/README/)
 
+Alternatively, you can use the [Dockerfile](community/Dockerfile) from Ralf-Philipp Weinmann.
+
 ## Build project
 
 Once you have all the dependencies installed you should be able to just build the tool:
@@ -93,6 +97,12 @@ path-to-file
 
 If you inspect the [serial_read_mp_array()](./test/Bugs/Uninit/Firefox/serial.ll-O2_p#L1528) function, the buggy block path is `%4` (the first block) to `%71`,where we use [`%73`].
 
+# Help
+
+We haven't tested (and likely won't test) Sys on anything but Arch Linux. We're
+happy to integrate patches that add support for other OSes and build systems
+though!
+
 # Directory structure
 
 ```
@@ -104,5 +114,6 @@ If you inspect the [serial_read_mp_array()](./test/Bugs/Uninit/Firefox/serial.ll
 │   ├── InternalIR -- Internal IR used to represent paths for both static and symex
 │   ├── Static     -- Static checker DSL
 │   └── Symex      -- Symbolic DSL and execution engine
+├── community      -- Community files
 └── test           -- Tests
 ```

community/Dockerfile

@@ -0,0 +1,35 @@
+# Debian 10 requires LLVM 9 to be installed from source (no package, no backport),
+# hence we use Debian 11 (testing) for now (to be released in 2021).
+FROM debian:bullseye
+MAINTAINER Ralf-Philipp Weinmann <[email protected]>
+
+RUN apt-get update && apt-get upgrade -y && \
+    apt-get install -y apt-utils build-essential sudo screen tmux
+
+# Add user
+RUN useradd -c 'User' -G sudo -s /bin/bash -m -g users user
+
+# Don't require password for sudo
+RUN perl -i -pe 's/(%sudo.*) ALL/\1 NOPASSWD: ALL/' /etc/sudoers
+
+# Install packages required to build boolector and sys
+RUN apt-get install -y llvm-9 haskell-stack git cmake curl
+
+USER user
+WORKDIR /home/user
+RUN mkdir src
+WORKDIR src
+RUN git clone https://github.com/Boolector/btor2tools.git
+RUN git clone https://github.com/Boolector/boolector.git
+RUN git clone https://github.com/PLSysSec/sys.git
+
+WORKDIR btor2tools
+RUN ./configure.sh && (cd build; make)
+RUN sudo cp build/lib/libbtor2parser.so  /usr/lib/ && \
+    sudo mkdir /usr/include/btor2parser && \
+    sudo cp src/btor2parser/btor2parser.h /usr/include/btor2parser/
+WORKDIR ../boolector
+RUN ./contrib/setup-lingeling.sh && ./configure.sh --shared --prefix /usr
+RUN cd build && make && sudo make install
+WORKDIR ../sys
+RUN stack build

community/README.md

@@ -0,0 +1 @@
+This directory hosts files and tools maintained by the community.