Semi-automated reasoning about non-determinism in C expressions

Research into C verification often ignores that the C standard leaves the evaluation order of expressions unspecified, and assigns undefined behavior to write-write or read-write conflicts in subexpressions—so called “sequence point violations”. C compilers exploit these aspects for optimizations, so these aspects should be accounted for in verification.

We present a separation logic with a verification condition generator (vcgen) to semi-automatically prove the absence of undefined behavior in a given C program for any evaluation order.

We prove correctness of our vcgen with respect to a new monadic definitional semantics of a subset of C. This semantics is modular and gives a concise account of non-determinism in C.

We have formalized all of our results in Coq. In particular we have implemented our vcgen as a tactic in Coq that one can use in conjunction with manual symbolic execution tactics.

A key enabler to define and prove the correctness of our verification condition generator was to build it on top of Iris—an expressive framework for concurrent separation logic in Coq. It allowed us to leverage the Iris Proof Mode and the Iris ghost state mechanism, to verify examples with protocols on the state.

The latest version of the source code is available in the following Git repository: https://gitlab.mpi-sws.org/iris/c/.

Preprint

Our paper has been accepted for ESOP 2019. Download the latest version here: iris-c-monad.pdf. (Note: in the submission there was a typo on pg 24 in the specification of the arraycopy example, it is fixed in this version).

The slides are available in the pdf format as well: esop-talk.pdf.

Artifact

Download the version of the code that goes well with the article: iris-c-monad-0.1.1.tgz. The archive contains a README file giving an overview of the development. The arraycopy example is in the file theories/tests/array_copy.v.

The artifact is known to compile with:

  • Coq version 8.8.1
  • Development versions of std++ and Iris.

The latest code (might not correspond to the paper) is also available from Git.

Installation instructions

  • Install opam version >= 2.0
  • Add the Iris opam repository:
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
opam update
  • Install the Coq development by running opam install . in the root directory.

Alternatively, install all the dependencies manually, and run make in the top-level directory.

Code guide

The up-to-date version is always contained in the README.md file. But the rough guide is as follows. The top-level directory with all the Coq files is theories. The other subdirectories are organized like this:

  • lib contains auxiliary stuff and technical developments mentioned in Section 4;
  • c_translation contains the definitions and specifications from Sections 2 & 3;
  • vcgen contains the vcgen from Section 5;
  • tests contain tests and examples.