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:
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:
libcontains auxiliary stuff and technical developments mentioned in Section 4;c_translationcontains the definitions and specifications from Sections 2 & 3;vcgencontains the vcgen from Section 5;testscontain tests and examples.
