jeehoonkang/Dockerfile

## README.md

      
    Raw
  

              README.md
            
          
    Crellvm: Verified Credible Compilation for LLVM

Downloading Artifact

You can download the Crellvm repository and build it as described in the development section below:
git clone https://github.com/snu-sf/crellvm.git
cd crellvm
... // build & test
Or, you can download a Docker image in which /root/crellvm contains build result:
docker load -i pldi18-41.tar.xz
docker run -it pldi18-41/pldi18-41

# inside a docker container
cd ~/crellvm
eval `opam config env`
make all
make quick
This image is built from the attached Dockerfile.
Code Structure

Crellvm is divided roughly into the following four parts:

LLVM in lib/llvm (https://github.com/snu-sf/crellvm-llvm)
Vellvm in lib/vellvm (https://github.com/snu-sf/crellvm-vellvm)
ERHL proof checker in ocaml/ and coq/def/
Formal verification of the ERHL proof checker in coq/proof/

LLVM

Proof Generation Code in Each Pass


Register promotion: PromoteMemoryToRegister.cpp
GVN-PRE: GVN.cpp
LICM: LICM.cpp, LCSSA.cpp, SSAUpdater.cpp
InstCombine: files in the InstCombine directory

Note that all our modifications are wrapped in the crellvm::intrude() function.
Proof Generation Library


.cpp files
.h files

Most of those codes are automatically-generated codes for serialization.
Validator


def contains the definition of the proof checker and its dependency.

Validator.v contains function valid_module, which is called from main.ml.
Postcond.v contains a strong post-invariant generator.
Infrules.v contains inference rules and their semantics.


corehint contains the schema for serialization.
main.ml contains the entry point for the proof checker.  It calls valid_module extracted from Coq.
infruleGen.ml contains the custom automation functions that find appropriate inference rules.

Proof


proof contains the formal verification of the proof checker in Coq.

Refinement.v proves behavioral refinement of two modules that pass the proof checker.
SimulationNop.v proves behavioral refinement for two equivalent modules modulo nops.


Development

Requirements


Git

In Ubuntu 16.04, sudo apt install git


A C++ compiler, Boost, and CMake 3.3.2+

In Ubuntu 16.04, sudo apt install gcc libboost-all-dev cmake


OPAM: the OCaml package manager

In Ubuntu 16.04, sudo apt install opam m4 pkg-config
Also execute opam init && opam update && opam switch 4.05.0


Scala 2.11.6+ for make test

In Ubuntu 16.04, sudo apt install scala


Build

You can build the proof-generating LLVM compiler and the ERHL proof checker as follows.  (You can
change the JOBS variable, whose default is 24.  For example, you may want to make JOBS=8 llvm
for systems with 8 CPUs.)


make init: Installs Coq and OCaml libraries, and fetches and builds dependencies.


make update: Updates dependencies.


make all (default): make llvm exec proof


make quick: make llvm exec proof-quick


make llvm: Builds LLVM in .build/llvm-obj.


make opt: Builds proof-generating LLVM IR optimizer in .build/llvm-obj/bin/opt.


make exec: Builds the ERHL proof checker in ocaml/main.native.


make proof: Compiles the Coq verification of the ERHL proof checker.


make proof-quick: Compiles the Coq verification with the -quick option (useful for interactive
theorem proving).


Execution

The following executables are generated in the build process:


.build/llvm-obj/bin/opt: an LLVM IR optimizer, but it also generates ERHL proofs
See opt -help for the additional options for proof generation,
e.g. -crellvm-passwhitelist=pass_name, -crellvm-compactjson.


ocaml/main.native: the ERHL proof checker
ocaml/main.native $SRC $TGT $PROOF validates a translation from $SRC to $TGT using $PROOF
as the ERHL translation proof. See ocaml/main.native -help for more details.


Example
mkdir -p temp; cd temp

cp ../crellvm-tests/csmith/ll-files/00001.ll 00001.ll

# opt generates proof for every mem2reg transformation
../.build/llvm-obj/bin/opt -O2 \
  -crellvm-passwhitelist=mem2reg \
  00001.ll \
  -o 00001.tgt.ll -S

# Now source/target/proof triples are generated
# ex. 00001.crc32_8bytes.74.src.bc / 00001.crc32_8bytes.74.tgt.bc / 00001.crc32_8bytes.74.hint.json
#     for the `crc32_8bytes` function's 74th mem2reg translation

# Run the ERHL validator for a translation
../ocaml/main.native 00001.crc32_8bytes.74.src.bc 00001.crc32_8bytes.74.tgt.bc 00001.crc32_8bytes.74.hint.json

# `Validation succeeded.` should be printed


Interactive Theorem Proving

make proof-quick generates .vio files, which is enough for interactive theorem proving (either
in CoqIDE or ProofGeneral).
coq/status-proof.sh to grep all assumption keywords (e.g. admit, Axiom) in the Coq files.
Currently it reports several admits, all of which are either (1) OCaml utility functions that are
not relevant to the correctness of the proof checker, (2) functions that are implemented in OCaml
for performance reasons, or (3) axioms on the external functions.
Test


make test-init: Downloads benchmark programs.


make test-update: Updates benchmark programs.


make test: Performs benchmark (§7).


The benchmark programs (§7. "Benchmarks") are in the following directories: SPEC CINT2006 C
Benchmarks in crellvm-tests/speccpu2006-ll; LLVM nightly test suite in
crellvm-tests/LNT-ll; the five open-source C projects in crellvm-tests/gnu-projects-ll.
1000 randomly-generated C files (§7. "Validating Randomly Generated Programs") are in
crellvm-tests/csmith/ll-files.
FYI, crellvm-tests/BENCHMARKS.md explains how to extract .ll files from the benchmark
programs.


make test executes crellvm-tests/run-benchmark.sh, which in turn executes
crellvm-tests/crellvm-tests-parallel/src/main/scala/main.scala. scala .../main.scala -h:
Gives a manual for the internal script:

-j $CORE: number of cores used for testing.
-a $OPTION: options to be passed to opt, e.g. -O2.
-i $TESTDIR: the address of the benchmark you want to compile and validate.


For example, scala .../main.scala -j 8 -a "-O2" -i crellvm-tests/LNT-ll means:


Execute opt (proof-generating LLVM IR optimizer) and main.native (ERHL proof checker)
for each .ll files in crellvm-tests/LNT-ll.


The test result (files report.summary, report.generate, report.validate) will be in
the ./test_result.LNT-ll.0 directory.


## Dockerfile
FROM ubuntu:16.04
MAINTAINER Jeehoon Kang <jeehoon.kang@sf.snu.ac.kr>

RUN apt update && apt install -y \
  git vim \
  gcc libboost-all-dev cmake \
  opam m4 pkg-config \
  && rm -rf /var/lib/apt/lists/*

RUN opam init -y && opam switch 4.05.0

WORKDIR /root

RUN eval `opam config env` \
  && git clone https://github.com/snu-sf/crellvm.git \
  && cd crellvm && make init

RUN eval `opam config env` \
  && cd crellvm && make

RUN eval `opam config env` \
  && cd crellvm && make quick

RUN eval `opam config env` \
  && cd crellvm && make test-init

CMD bash
	FROM ubuntu:16.04
	MAINTAINER Jeehoon Kang <jeehoon.kang@sf.snu.ac.kr>

	RUN apt update && apt install -y \
	git vim \
	gcc libboost-all-dev cmake \
	opam m4 pkg-config \
	&& rm -rf /var/lib/apt/lists/*

	RUN opam init -y && opam switch 4.05.0

	WORKDIR /root

	RUN eval `opam config env` \
	&& git clone https://github.com/snu-sf/crellvm.git \
	&& cd crellvm && make init

	RUN eval `opam config env` \
	&& cd crellvm && make

	RUN eval `opam config env` \
	&& cd crellvm && make quick

	RUN eval `opam config env` \
	&& cd crellvm && make test-init

	CMD bash