Vellvm
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.
See:
Participants
- Steve Zdancewic
- Yannick Zakowski
- Calvin Beck
- Olek Gierczak
Past Contributors
- Vivien Durey
- Dmitri Garbuzov
- William Mansky
- Milo Martin
- Santosh Nagarakatte
- Emmett Neyman
- Christine Rizkallah
- Robert Zajac
- Richard Zhang
- Jianzhou Zhao
Structure of the repository
/src/ci - travis configuration
/src/coq - Coq formalization (see Denotation.v and TopLevel.v most notably)
/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
Installing / Compiling Vellvm
Assumes:
- coqc : version 8.9.1 or 8.10.0 (and coqdep, etc.)
- Coq packages:
- ext-lib (installed via, e.g. opam install coq-ext-lib)
- paco (installed via, e.g. opam install coq-paco)
- flocq (installed via, e.g. opam install coq-flocq, see note below)
- itree
(installed via, e.g. opam install coq-itree)- Currently you should actually just use the submodule (lib/InteractionTrees): see the instructions for compilation below.
- ceres (installed via, e.g. opam install coq-ceres)
- ocamlc : version 4.04 (probably works with 4.03 or later)
- OPAM packages: dune, menhir, [optional: llvm (for llvm v. 3.8)]
Compilation:
- clone the vellvm git repo with
--recurse-submoduleoption (git clone --recurse-submodules) - run
makein the /src directory
Running
Do src/vellvm -help from the command line.
Try src/vellvm -interpret tests/ll/factorial.ll.
Notes
coq-flocq
On some OSX configurations the opam installation for coq-flocq fails with a
permissions error # Failed to create server: Operation not permitted caused by
opam's sandboxing scripts. The solution is to temporarily disable opam's
sandboxing by editing ~/.opam/config to remove the lines having to do with
wrap-*-commands:.