Verified Value Analysis for CompCert
A companion web page
Verified Value Analysis for CompCert is built on top of the
C CompCert verified compiler. The value analysis operates on
the CFG intermediate representation and outputs a correct
interval of possible values for each program variable, at each
program point.
Page last updated on: 2013-03-29
Paper
This work has been accepted at the 20th Static Analysis Symposium
(SAS 2013).
You can access it here.
Coq Development
Download the last stable version of the Coq development:
[value-analysis.tgz]
(tested with OCaml 4.00 and Coq 8.3pl5)
Download a virtual machine image of the development:
[value-analysis-vm.zip]
This VirtualBox VM contains a Debian Linux with
precompiled binaries of our development (and the contents of the .tgz archive).
Note: after decompression it requires around 1.5 GB of disk space.
On some machines we experienced some issues with VirtualBox that were resolved
by re-adding/re-running the machine. Should you experience any issues, please contact
us to help resolve it.
Installation instructions
Note: You need OCaml (3.12 or 4.00) and Coq 8.3
(up to 8.3pl5, but not 8.4) installed on your machine.
The provided archive is already bundled with CompCert 1.11.
- Download and extract the archive
(tar xvf value-analysis.tgz).
- Inside the value-analysis directory,
run make proof to Coq-prove the analysis
and the CompCert C compiler (this can take several minutes;
adding flag -j<N> for parallel processing
can speed it up, but will require more memory).
- Run make extraction cfgcomp to extract and
compile the Coq code. This will produce a binary executable
cfgcomp that accepts some extra command-line
options specific to the value analysis.
- Go to the annotated-benchs directory and run
./cfgcomp.sh <file.c> to analyze a single file,
or ./launch_all.sh to run the analysis on all files.
In both cases, each analyzed source produces a
<file>.value.cfg file containing the program's
CFG representation annotated with the result of the analysis.
Note: to run launch_all.sh, Python must be installed on
the machine.
Afterwards, you can run cfgcomp <file> on a specific C
program to analyze it.
Additional information
- In the development, our files are placed in the vanalysis,
bourdoncle and dev directories.
Browsable version of the Coq development
The documentation gives a commented listing of the underlying Coq
specifications and proofs. Proof scripts are folded by default, but
can be viewed by clicking on "Proof".
CFG Language
- CFG: Intermediate language between Cminor and RTL.
- CFGgen: Compiler code for the construction of CFG.
- CFGgenspec: Correctness specification for CFGgen.
- CFGgenproof: Correctness proof for CFGgen.
Value analysis
Utilities and common code
CompCert original files
- Index: index of the original CompCert development.