A Formal C Memory Model Supporting Integer-Pointer Casts
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis
This artifact consists of:
- example C source codes presented in the paper; and
- Coq formalization for our memory model and verification of example transformations.
- Ubuntu ID / PASSWORD:
- Our development is located at:
Example C Source Codes
There are 7 example C source codes in Section 3 and 5 of the
paper. The source codes are in the
/test directory. C file names
match with the name of subsections in Section 3 and 5. Here is the
list of C source codes:
In this artifact we prove the claim in the paper that compilers
perform specific optimizations or not. For this, we ship the compilers
and compilation results (
/test/*.s) in the artifact. See
- In this artifact, we used
clang3.4 from Ubuntu's default package system installed by
apt-get install gcc clang-3.4. This deviates from the versions we specified in the paper (
clang3.4.2), but we believe the difference is negligible. We will update the versions specified in the camera-ready version of the paper.
We fully formalized all the proofs reported in the paper in
/src directory contains Coq files.
- Memory model is formalized in
- Memory invariant is formalized in
- Language syntax and semantics are formalized in
- Verification examples are presented and proved in
/src/example/*.v. The Coq file names match with the name of subsections in Section 3 and 5.
- Identity compiler are proved in
/src/example/IdentityCompiler.v, and dead cast elimination pass is implemented in
/src/example/DeadCastEliminationCompiler.v. These are mentioned in Section 6.6.
- Local simulation relation is formalized in
/src/lang/SimulationLocal.v, and adequacy is proved in
In the artifact, build succeeds with Coq 8.4pl4.
For interactive theorem proving using ProofGeneral, we edited
~/.coqrcin the artifact.
We imported libraries from CompCert and modified for our purposes. Files originally imported from CompCert 2.4 are:
All these files are "dual-licensed both under the INRIA Non-Commercial
License Agreement and under the Free Software Foundation GNU General
Public License, either version 2 or (at your option) any later
/LICENSE-COMPCERT for more details.
We use Paco: A Coq Library for Parameterized Coinduction.