VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs

The “heap” in Verifiable C is actually a step indexed model of CompCert’s memories, following Hobor et al. [17].

Readers can understand the type of P as \(\text {stack} \rightarrow \text {heap} \rightarrow \text {Prop}\). But actually, this predicate must be monotonic w.r.t. the step indexing, i.e. we define it Coq as a dependent pair of a predicate and a proof of monotonicity [3, Part V].

This specification of is not strong enough, because it does not say whether the values of \(\llbracket \texttt {x} \rrbracket \) and \(\llbracket \texttt {y} \rrbracket \) change or not after running the function. In actual verification, we will use:

In actual Coq code, Clight uses identifiers to represent C variable names and C function names. So, when we write , the real Coq code is “\(\mathsf {\_swapint}\)” which is an identifier, i.e. a positive number, in Coq. Similarly, the real Coq code for is “\(\mathsf {tint}\)” whose type is \(\mathsf {Clight.type}\), a Coq inductive type representing the syntax tree of C types.

Our \(\mapsto \) and \(\mathsf {data\_at}\) predicates take another argument that we omit in this article: a permission-share indicating read-only, read-write, or various other levels of access to the data.

In CompCert 2.4 and earlier versions, the Clight type definition is a Coq inductive type. However, from CompCert 2.5, and types are represented by name instead of by structure. Specifically, every Clight program is associated with a \(\mathsf {composite\_env}\). A \(\mathsf {composite\_env}\) is a dictionary mapping every / name to a list of all its fields. The meaning of a or a needs to be interpreted by looking it up in the dictionary. From then on, \(\mathsf {reptype}\) and \(\mathsf {data\_at\_rec}\) are no longer Coq functions recursive on Coq inductive structure. The CompCert developers accepted our suggestion that every type should be tagged with a rank, which is a natural number. The ranking system ensures that the rank of a struct type is the max rank of its fields plus one; the rank of a union type is the max rank of its fields plus one; the rank of an array type is the rank of its element type plus one. The rank of elementary types (including pointers) is zero. Our current definition of \(\mathsf {reptype}\) and \(\mathsf {data\_at\_rec}\) are recursive functions on this rank.

In the Coq development, we use the name for what we call “stack” in the paper.

In our Coq development, we actually turn the symbolic clauses into binary trees first. Then we look up in these trees during symbolic evaluation. We omit the technical details here.

All the load and store rules of this section also need typechecking side conditions, i.e., \(\mathsf {tc\_expr}(\varDelta ,e)\) for each involved C expression e. We omit them for brevity.

One might wonder why the expression evaluation function does not directly return a field address. For and fields, this could work, but for array indices, it wouldn’t, because the field-address operator is only well-defined if the array index is within the array bounds, but adding an integer to a pointer is always defined in CompCert Clight, even if dereferencing it might be undefined. So the evaluation function could only use the field-address operator if the array index is within bounds, but it cannot know whether this is the case, because it does not have access to the array size.