Skip to content

Instantly share code, notes, and snippets.

@jeehoonkang

jeehoonkang/README.md

Last active August 29, 2015 14:15
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jeehoonkang/32e53c387b29a299362f to your computer and use it in GitHub Desktop.
Save jeehoonkang/32e53c387b29a299362f to your computer and use it in GitHub Desktop.
Download ZIP
A Formal C Memory Model Supporting Integer-Pointer Casts
Raw
README.md

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment