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.

Virtual Machine

Ubuntu ID / PASSWORD: artifact / artifact
Our development is located at: ~/Works/intptrcast

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:

/test/DAE_DSE_DLE_CP.c
/test/ArithmeticOptimizations1.c
/test/DeadCodeElimination.c
/test/OwnershipTransfer.c
/test/ArithmeticOptimizations2.c
/test/DeadCastElimination.c
/test/Drawbacks.c

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 /test/Makefile, /test/GCCVERSION, and /test/CLANGVERSION for more details.

In this artifact, we used gcc 4.8.2 and clang 3.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 (gcc 4.8.3 and clang 3.4.2), but we believe the difference is negligible. We will update the versions specified in the camera-ready version of the paper.

Coq Formalization

We fully formalized all the proofs reported in the paper in Coq. /src directory contains Coq files.

Main Result

Memory model is formalized in /src/common/Memory.v.
Memory invariant is formalized in /src/common/MemoryRelation.v.
Language syntax and semantics are formalized in /src/lang.
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 /src/lang/Adequacy.v.

Compilation

Build by make in /src directory.
In the artifact, build succeeds with Coq 8.4pl4.
For interactive theorem proving using ProofGeneral, we edited ~/.coqrc in the artifact.

Libraries

CompCert

We imported libraries from CompCert and modified for our purposes. Files originally imported from CompCert 2.4 are:

/src/lib/Axioms.v, /src/lib/Coqlib.v, /src/lib/Integers.v, /src/lib/Maps.v;
/src/common/AST.v, /src/common/Errors.v.

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 version". See /LICENSE-COMPCERT for more details.

Paco

We use Paco: A Coq Library for Parameterized Coinduction.

jeehoonkang/README.md