how to prove the correctness of a c program with coq

Question

I want to prove the correctness of some of my programs but I don't know where to start. Let's say I have the following program, how can I prove its correctness or lack there of. How can I go from the source below and plug them into a theorem prover. Coq or ACL2 or pretty much anything.

The code below just counts the bytes that it reads from the standard input. It has 2 versions, one does a byte by byte count, the other reads them by unsigned integer size chunks when possible. I know it's not portable or pretty, it's just an example that could get me started. With some help.

The code works and I know it's correct and I know how to write unit tests for it but I don't know how to prove anything about it.

#include <stdio.h>
#include <unistd.h>
#include <stdlib.h>

unsigned count_bytes1(unsigned char * bytes, unsigned len) {
    unsigned count=0;
    unsigned i;
    for (i=0;i<len;i++) {
        count+=bytes[i];
    }
    return count;
}
unsigned count_word(unsigned word) {
    unsigned tmp = word;
    if (sizeof(unsigned)==4) {
        tmp = (0x00FF00FFU&tmp) + (( (0xFF00FF00U)&tmp)>>8);
        tmp = (0x0000FFFFU&tmp) + (( (0xFFFF0000U)&tmp)>>16);
        return tmp;
    }
    if (sizeof(unsigned)==8) {
        tmp = (0x00FF00FF00FF00FFU&tmp) + (( (0xFF00FF00FF00FF00U)&tmp)>>8);
        tmp = (0x0000FFFF0000FFFFU&tmp) + (( (0xFFFF0000FFFF0000U)&tmp)>>16);
        tmp = (0x00000000FFFFFFFFU&tmp) + (( (0xFFFFFFFF00000000U)&tmp)>>32);
        return tmp;
    }
    return tmp;
}
unsigned count_bytes2(unsigned char * bytes, unsigned len) {
    unsigned count=0;
    unsigned i;
    for (i=0;i<len;) {
        if ((unsigned long long)(bytes+i) % sizeof(unsigned) ==0) {
            unsigned * words = (unsigned *) (bytes + i);
            while (len-i >= sizeof(unsigned)) {
                count += count_word (*words);
                words++;
                i+=sizeof(unsigned);
            }
        }
        if (i<len) {
            count+=bytes[i];
            i++;
        }
    }
    return count;
}

int main () {
    unsigned char * bytes;
    unsigned len=8192;
    bytes=(unsigned char *)malloc(len);
    len = read (0,bytes,len);
    printf ("%u %u\n",count_bytes1(bytes,len),count_bytes2(bytes,len));
    return 0;
}

Answer 1

A more basic issue is whether or not a file that purportedly contains say non trivial C programs actually contains valid C programs. Not only the must conditions in the ANSI C spec but all the should and should not conditions as well. Often our compiler would be accused of not working properly but when the developers looked at the source "code" they found that it did not contain C. Note that the compiler and runtime are supposed to enforce all of the must conditions but what should occur when a should condition is violated is undefined. One could put out code that erased all the users files upon detecting such a condition. Of course a reputable compiler would not do that but it is not prohibited. Typically at low opt, code that one would expect that what got generated sort of did what you expect, but a high opt compiled one could output total garbage. Personally I would not in general compile a production C app at high opt but would only use moderate code optimization as it is hard to be sure that the code one writes is infact valid C, and I read the ANSI C spec a number of times.

Answer 2

1. Know what you are proving: specification

First, decide what it is you want to prove for your function. For instance, write a contract for your function, using the ACSL specification language:

/*@ ensures \result >= x && \result >= y; 
    ensures \result == x || \result == y; 
*/ 
int max (int x, int y);

2. Verification

Then, you may prove that your implementation satisfies the specification, for instance with Frama-C's WP plug-in.

The WP plug-in will generate proof obligations, the verification of which will ensure that the implementation is correct with respect to the specification. You can prove these in Coq 8.4+ if it amuses you (but almost nobody who actually does this does not first apply available, fully automatic SMT provers such as Alt-Ergo).

---

PS: it appears that you are trying to prove that one C function is equivalent to another, that is, to use a simple C function as specification for an optimized one. Proving the equivalence of one with respect to the other is the approach followed in this article:

José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, and Bárbara Vieira. Verifying cryptographic software correctness with respect to reference implementations. In FMICS’09, volume 5825 of LNCS, pages 37–52, 2009.