Vellvm is a Coq formalization of the semantics of (a subset of) the LLVM compiler IR that is intended for formal verification of LLVM-based software. It is being developed at the University of Pennsylvania as part of the DeepSpec project.
- Steve Zdancewic
- Yannick Zakowski
- Calvin Beck
- Olek Gierczak
- Vivien Durey
- Dmitri Garbuzov
- William Mansky
- Milo Martin
- Santosh Nagarakatte
- Emmett Neyman
- Christine Rizkallah
- Robert Zajac
- Richard Zhang
- Jianzhou Zhao
/src/ci - travis configuration
/src/coq - Coq formalization (see StepSemantics.v)
/src/ml - OCaml glue code for working with ollvm
/src/ml/extracted - OCaml code extracted from the files in /src/coq directory
/src/doc - coqdoq [not useful yet]
/lib - for 3rd party libraries [as git submodules]
/tests - various LLVM source code tests
- coqc : version 8.8.0 (and coqdep, etc.)
- Coq packages: ext-lib (installed via, e.g. opam install coq-ext-lib)
- ocamlc : version 4.04 (probably works with 4.02 or later)
- OPAM packages: ocamlbuild, menhir, [optional: llvm (for llvm v. 3.8)]
Compilation:
- clone the vellvm git repo with
--recurse-submodule
option (git clone --recurse-submodules
) - update CompCert submodule to coq 8.7.1 compatible version:
cd lib/CompCert && git pull origin master
- compile 3rd party libraries:
- CompCert:
cd lib/Compcert && ./configure x86_64-macosx && make
- Compile Paco:
make -C lib/paco/src
- Compile InteractionTrees
- create the file
lib/InteractionTrees/_CoqPath
and edit it to contain-Q ../paco/src Paco
- run
make
from the InteractionTrees directory (do not usesetup.sh
since that will clone another copy of paco and we already assume ext-lib exists)
- create the file
- CompCert:
- run
make
in the /src directory
Do src/vellvm -help
from the command line.
Try src/vellvm -interpret tests/ll/factorial.ll
.