Semi-automated Reasoning About Non-determinism in C Expressions

Conference Paper (2019)
Author(s)

Dan Frumin (Radboud Universiteit Nijmegen)

Léon Gondelman (Radboud Universiteit Nijmegen)

R.J. Krebbers (TU Delft - Programming Languages)

Research Group
Programming Languages
Copyright
© 2019 Dan Frumin, Léon Gondelman, R.J. Krebbers
DOI related publication
https://doi.org/10.1007/978-3-030-17184-1_3
More Info
expand_more
Publication Year
2019
Language
English
Copyright
© 2019 Dan Frumin, Léon Gondelman, R.J. Krebbers
Research Group
Programming Languages
Pages (from-to)
60-87
ISBN (print)
978-3-030-17183-4
ISBN (electronic)
978-3-030-17184-1
Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Abstract

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”. These aspects should be accounted for in verification because C compilers exploit them. We present a verification condition generator (vcgen) that enables one to semi-automatically prove the absence of undefined behavior in a given C program for any evaluation order. The key novelty of our approach is a symbolic execution algorithm that computes a frame at the same time as a postcondition. The frame is used to automatically determine how resources should be distributed among subexpressions. 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 implemented our vcgen as a tactic in the Coq interactive theorem prover, and have proved correctness of it using a separation logic for the new monadic definitional semantics of a subset of C.