In this chapter we show how to prove the correctness of C programs that use null-terminated character strings. Here are some functions from the C standard library, strlib.c

    #include <stddef.h>

    size_t strlen(const char *str) {
      size_t i;
      for (i=0; ; i++)
        if (str[i]==0) return i;
    }

    char *strcpy(char *dest, const char *src) {
      size_t i;
      for(i = 0;; i++){
        char d = src[i];
        dest[i] = d;
        if(d == 0) return dest;
      }
    }

    int strcmp(const char *str1, const char *str2) {
      size_t i;
      for(i = 0;; i++){
        char d1 = str1[i];
        char d2 = str2[i];
        if(d1 == 0 && d2 == 0) return 0;
        else if(d1 < d2) return -1;
        else if(d1 > d2) return 1;
      }
    }    

Standard boilerplate

Representation of null-terminated strings.

Coq represents a string as a list-like Inductive of Ascii characters:

The C programming language represents a character as a byte, that is, an 8-bit signed or unsigned integer. In Coq represent the 8-bit integers using the byte type.

CompCert's Byte module is an 8-bit instantiation of the n-bit integers, just as the Int module is a 32-bit instantiation. Here, we can ask what Byte knows about the theory of 8-bit modular integers:

We can convert a Coq string to a list of bytes:

To describe a single byte in memory, we can use data_at with the signed-character type:

This data_at Tsh tschar (Vint (Int.repr 72)) p is an mpred, that is, a memory predicate in separation logic. It says, at address p in memory there is a sequence of bytes whose length is appropriate for type tschar; that is, one byte. The contents of this sequence of bytes (one byte) is a representation of the integer 72. The ownership share (access permission) of memory at address p is the "top share" Tsh

We can express the same thing using Vbyte (Byte.repr 72). In fact, Vbyte is not a primitive CompCert value, it is a definition:

The C programming language represents a string of length k as an array of nonnull characters (bytes), terminated by a null character. We represent this in separation logic using the cstring memory-predicate:

Here is an example of a cstring predicate that says, At address p there is a null-terminated string representing "Hello".

By unfolding the definition of cstring this is equivalent to,

This says, no element of the list Hello' is equal to Byte.zero. In memory at address p there is an array of 6 bytes, whose contents are the contents of Hello' with a Byte.zero appended at the end. Sometimes we know that there is a null-terminated string inside an array of length n. That is, there are k nonnull characters (where k<n), followed by a null character, followed by n-(k+1) uninitialized (or don't-care) characters. We represent this with the cstringn predicate.

Reasoning about the contents of C strings

In separation logic proofs about C strings, we often find proof goals similar to the one exemplified by this lemma:

A null-terminated string is an array of characters with three parts:

• The contents of the string, none of which is the '\0' character;
• The null termination character, equal to Byte.zero;
• the remaining garbage in the array, after the null.

When processing a string, you should maintain three kinds of assumptions above the line:

• Hypothesis H above the line says that none of the

contents is the null character;

• Hypothesis H₀ typically comes from a loop test, s[i]!=0
• H₁ typically comes from a loop invariant: suppose a

a loop iteration variable _i (with value i) is traversing the array. We expect that loop to go up to but no farther than the null character, that is, one past the contents. The cstring tactic processes all three of these hypotheses to conclude that i < Zlength contents.

But actually, cstring tactic will prove any rep_lia consequence of that fact. For example:

Here is another demonstration. When your loop on the string contents reaches the end, the loop test s[i]!=0 is false, so therefore s[i]=0.

Hypothesis H₀ expresses that the loop test determined s[i]=0. The cstring can then prove that i = Zlength contents.

Function specs

strlen(s) returns the length of the string s.

A digression about size_t

Vptrofs? Ptrofs.repr? What's that? Programmers use size_t when writing C programs that are portable to 64-bit and 32-bit installations; this typedef stands for whatever size of unsigned (long) integer is the same size as a pointer. In Verifiable C, size_t is the corresponding C unsigned type:

Then, in the RETURN clause, instead of returning the value Vlong (Int64.repr (Zlength s)) or Vint (Int.repr (Zlength s)), which would not be portable, we use Vptrofs, which stands for either Vlong or Vint, depending:

The unpronounceable "ptrofs" stands for "pointer offset". It's a CompCert thing. Don't ask. The argument of Vptrofs is a ptrofs, that is Ptrofs.int. The module Ptrofs is isomorphic to Int64 in a 64-bit configuration, and isomorphic to Int in a 32-bit configuration. Isomorphic, but not identical; there are lemmas relating them:

VST-Floyd has proof automation tactics that try to help you by applying these lemmas where appropriate. For example, in the proofs in this chapter, you don't have to do much special to deal with the Vptrofs.

End of digression about size_t

strcpy(dest,src) copies the string src to the array dest.

strcmp(s₁,s₂) compares strings s₁ and s₂ for lexicographic order. This funspec is an underspecification of the actual behavior, in that it specifies equality testing only.

Proof of the strlen function

Exercise: 2 stars, standard (body_strlen)

Look at the proof goal below the line. We have the assertion,
  PROP ( ) LOCAL (temp _str str) SEP (cstring sh s str))

When proving things about a string-manipulating function, the first decision is: Does this function treat the string abstractly or does it subscript the array and look at the individual characters?

• If abstract, then we should not unfold the definition cstring.
• If we subscript the array directly, we must unfold cstring.

Since this strlen function does access the array contents, we start by unfolding cstring.

Now, we have a Proposition ¬ In Byte.zero s in the SEP clause of our assertion; we can move it above the line by Intros.

Now we are at a for-loop. Unlike a simple while-loop, a for-loop may:

• break; (prematurely terminate the loop)
• continue; (prematurely terminate the body, skipping to the increment)

So therefore the simple Hoare-logic while rule is not always applicable. The general form of Verifiable C's loop tactic is:
  forward_loop Inv1 continue: Inv2 break: Inv3

where Inv1 is the invariant that holds right before the loop test, Inv2 is the invariant that holds right before the increment, and Inv3 is the postcondition of the loop. Providing continue: Inv2 is optional, as is break: Inv3. In many cases the forward_loop tactic can figure out that the continue: invariant is not needed (if the loop doesn't contain a continue statement), or the break: postcondition is not needed (if there's no break statement, or if there are no commands after the loop). So let's try this loop with only a single loop invariant:

Look at the LOCAL clause that binds temp _i to the value Vptrofs (Ptrofs.repr i). What is that? The answer is, in reasoning about C programs, we need:

• 8-bit integers, Byte.int or simply byte
• 32-bit integers, Int.int or simply int
• 64-bit integers, Int64.int

But there is also the concept expressed in C as size_t, that is, The integer type with the same number of bits as a pointer. In this might be the same as 32-bit int, or it might be the same as 64-bit int. So, just as CompCert has the Int module for reasoning about 32-bit integers and the Int64 module for 64-bit integers, it has also the Ptrofs module for reasoning about pointer offsets. Ptrofs is isomorphic to (but not identical to) either Int64 or Int, depending on the boolean value Archi.ptr64.

If this computes false, then this installation of Verifiable C is configured for 32-bit pointers; if true, then this Verifiable C is configured for 64-bit. But either way, to turn a Ptrofs.int value into a CompCert val, we have Vptrofs. And -- just as we can write C programs that are portable to 32-bit or 64-bit pointers using size_t, we can write proofs scripts portable by using Ptrofs.

And therefore, _i is a C variable of type size_t, i is a Coq variable of type Z, and and Vptrofs (Ptrofs.repr i) is a CompCert val that represents i as a val.

Now it's time to prove all the subgoals of forward_loop.

Proof of the strcpy function

Exercise: 2 stars, standard (strcpy_then_clause)

The next lemma, or some variation of it, will be useful in the proof of the strcpy function (in the then clause of the if statement).

Exercise: 2 stars, standard (strcpy_else_clause)

Useful lemmas here will be: upd_Znth_app2, sublist_split, list_repeat_app', app_Znth1, map_app, app_ass, sublist_len_1.

data_at is not injective!

The Vundef value means uninitialized or undefined or defined but don't care. Consider this lemma:

The proof goal means: If cells 0 ≤ j < i+1 are zero and cells i+1 ≤ j < n are don't care, that implies the weaker statement that cells 0 ≤ j < i are zero and cells i ≤ j < n are don't-care. Now, let's try to prove it using the same technique as in strcpy_then_clause:

Oops! The current proof goal is False! The problem was that we should not have applied derives_refl'.

Why did that work? Let's look at a simpler example.

Uncomment the following line, and notice that it solves the goal.

cancel breaks this into two subgoals:

In the first subgoal, we use the fact that |-- is reflexive

In the second subgoal, we use the fact that any value implies a Vundef, or more generally, any value implies default_val t for any CompCert type t.

The moral of the story is: When proving
   data_at sh t a p |-- data_at sh t b p

if (a=b) you can simplify the goal using
   apply derives_refl'; f_equal.

but if a is strictly more defined than b, then derives_refl' is not appropriate.

Exercise: 3 stars, standard (body_strcpy)

Because this function subscripts the strings, it does not treat the strings abstractly, we must unfold cstring and cstringn.

In the then clause of this proof, you may reach a proof goal similar to Lemma strcpy_then_clause, but not identical. In that case you may want to use the same proof techniques you used in that exercise. Ditto for the else clause, and strcpy_else_clause.

Exercise: 3 stars, standard (example_call_strcpy)

Prove the correctness of a function that calls strcpy.

  int example_call_strcpy(void) {
    char buf[10];
    strcpy(buf,"Hello");
    return buf[0];
  }

This proof is fairly straightforward. First, figure out what WITH witness to give for forward_call. Hint: look at the SEP clause of the precondition of strcpy_spec, and see how the data_at and cstring conjuncts must match your current assertion. Second, after the forward_call, don't forget to unfold cstringn; this is necessary because after the call we subscript the _buf array directly.

Exercise: 4 stars, standard, optional (body_strcmp)