Example: Find First Set

As a first example, we consider showing the equivalence of several quite different implementations of the POSIX ffs function, which identifies the position of the first 1 bit in a word. The function takes an integer as input, treated as a vector of bits, and returns another integer which indicates the index of the first bit set (zero being the least significant). This function can be implemented in several ways with different performance and code clarity tradeoffs, and we would like to show those different implementations are equivalent.

Reference Implementation

One simple implementation takes the form of a loop with an index initialized to zero, and a mask initialized to have the least significant bit set. On each iteration, we increment the index, and shift the mask to the left. Then we can use a bitwise “and” operation to test the bit at the index indicated by the index variable. The following C code (which is also in the ffs.c file on GitHub) uses this approach.

uint32_t ffs_ref(uint32_t word) {
    int i = 0;
    if(!word)
        return 0;
    for(int cnt = 0; cnt < 32; cnt++)
        if(((1 << i++) & word) != 0)
            return i;
    return 0; // notreached
}

This implementation is relatively straightforward, and a proficient C programmer would probably have little difficulty believing its correctness. However, the number of branches taken during execution could be as many as 32, depending on the input value. It’s possible to implement the same algorithm with significantly fewer branches, and no backward branches.

Alternative Implementations

An alternative implementation, taken by the following function (also in ffs.c), treats the bits of the input word in chunks, allowing sequences of zero bits to be skipped over more quickly.

uint32_t ffs_imp(uint32_t i) {
    char n = 1;
    if (!(i & 0xffff)) { n += 16; i >>= 16; }
    if (!(i & 0x00ff)) { n += 8;  i >>= 8; }
    if (!(i & 0x000f)) { n += 4;  i >>= 4; }
    if (!(i & 0x0003)) { n += 2;  i >>= 2; }
    return (i) ? (n+((i+1) & 0x01)) : 0;
}

Another optimized version, in the following rather mysterious program (also in ffs.c), based on the ffs implementation in musl libc.

uint32_t ffs_musl (uint32_t x)
{
  static const char debruijn32[32] = {
    0, 1, 23, 2, 29, 24, 19, 3, 30, 27, 25, 11, 20, 8, 4, 13,
    31, 22, 28, 18, 26, 10, 7, 12, 21, 17, 9, 6, 16, 5, 15, 14
  };
  return x ? debruijn32[(x&-x)*0x076be629 >> 27]+1 : 0;
}

These optimized versions are much less obvious than the reference implementation. They might be faster, but how do we gain confidence that they calculate the same results as the reference implementation?

Finally, consider a buggy implementation which is correct on all but one possible input (also in ffs.c). Although contrived, this program represents a case where traditional testing – as opposed to verification – is unlikely to be helpful.

uint32_t ffs_bug(uint32_t word) {
    // injected bug:
    if(word == 0x101010) return 4; // instead of 5
    return ffs_ref(word);
}

SAWScript allows us to state these problems concisely, and to quickly and automatically 1) prove the equivalence of the reference and optimized implementations on all possible inputs, and 2) find an input exhibiting the bug in the third version.

Generating LLVM Code

SAW can analyze LLVM code, but most programs are originally written in a higher-level language such as C, as in our example. Therefore, the C code must be translated to LLVM, using something like the following command:

$ clang -g -c -emit-llvm -o ffs.bc ffs.c

The -g flag instructs clang to include debugging information, which is useful in SAW to refer to variables and struct fields using the same names as in C. We have tested SAW successfully with versions of clang from 3.6 to 7.0. Please report it as a bug on GitHub if SAW fails to parse any LLVM bitcode file.

This command, and following command examples in this tutorial, can be run from the code directory on GitHub. A Makefile also exists in that directory, providing quick shortcuts for tasks like this. For instance, we can get the same effect as the previous command by running:

$ make ffs.bc

Equivalence Proof

We now show how to use SAWScript to prove the equivalence of the reference and implementation versions of the FFS algorithm, and exhibit the bug in the buggy implementation.

A SAWScript program is typically structured as a sequence of commands, potentially along with definitions of functions that abstract over commonly-used combinations of commands.

The following script (in ffs_llvm.saw) is sufficient to automatically prove the equivalence of ffs_ref with ffs_imp and ffs_musl, and identify the bug in ffs_bug.

set_base 16;

print "Extracting reference term: ffs_ref";
l <- llvm_load_module "ffs.bc";
ffs_ref <- llvm_extract l "ffs_ref";

print "Extracting implementation term: ffs_imp";
ffs_imp <- llvm_extract l "ffs_imp";

print "Extracting implementation term: ffs_musl";
ffs_musl <- llvm_extract l "ffs_musl";

print "Extracting buggy term: ffs_bug";
ffs_bug <- llvm_extract l "ffs_bug";

print "Proving equivalence: ffs_ref == ffs_imp";
let thm1 = {{ \x -> ffs_ref x == ffs_imp x }};
result <- prove abc thm1;
print result;

print "Proving equivalence: ffs_ref == ffs_musl";
let thm2 = {{ \x -> ffs_ref x == ffs_musl x }};
result <- prove abc thm2;
print result;

print "Finding bug via sat search: ffs_ref != ffs_bug";
let thm3 = {{ \x -> ffs_ref x != ffs_bug x }};
result <- sat abc thm3;
print result;

print "Finding bug via failed proof: ffs_ref == ffs_bug";
let thm4 = {{ \x -> ffs_ref x == ffs_bug x }};
result <- prove abc thm4;
print result;

print "Done.";

In this script, the print commands simply display text for the user. The llvm_extract command instructs the SAWScript interpreter to perform symbolic simulation of the given C function (e.g., ffs_ref) from a given bitcode file (e.g., ffs.bc), and return a term representing the semantics of the function.

The let statement then constructs a new term corresponding to the assertion of equality between two existing terms. Arbitrary Cryptol expressions can be embedded within SAWScript; to distinguish Cryptol code from SAWScript commands, the Cryptol code is placed within double brackets {{ and }}.

The prove command can verify the validity of such an assertion, or produce a counter-example that invalidates it. The abc parameter indicates what theorem prover to use; SAWScript offers support for many other SAT and SMT solvers as well as user definable simplification tactics.

Similarly, the sat command works in the opposite direction to prove. It attempts to find a value for which the given assertion is true, and fails if there is no such value.

If the saw executable is in your PATH, you can run the script above with

$ saw ffs_llvm.saw



Loading file "ffs_llvm.saw"
Extracting reference term: ffs_ref
Extracting implementation term: ffs_imp
Extracting implementation term: ffs_musl
Extracting buggy term: ffs_bug
Proving equivalence: ffs_ref == ffs_imp
Valid
Proving equivalence: ffs_ref == ffs_musl
Valid
Finding bug via sat search: ffs_ref != ffs_bug
Sat: [x = 0x101010]
Finding bug via failed proof: ffs_ref == ffs_bug
prove: 1 unsolved subgoal(s)
Invalid: [x = 0x101010]
Done.

Note that both explicitly searching for an input exhibiting the bug (with sat) and attempting to prove the false equivalence (with prove) exhibit the bug. Symmetrically, we could use sat to prove the equivalence of ffs_ref and ffs_imp, by checking that the corresponding disequality is unsatisfiable. Indeed, this exactly what happens behind the scenes: prove abc <goal> is essentially not (sat abc (not <goal>)).

Cross-Language Proofs

We can implement the FFS algorithm in Java with code almost identical to the C version.

The reference version (in FFS.java) uses a loop, like the C version:

    static int ffs_ref(int word) {
        int i = 0;
        if(word == 0)
            return 0;
        for(int cnt = 0; cnt < 32; cnt++)
            if(((1 << i++) & word) != 0)
                return i;
        return 0;
    }

And the efficient implementation uses a fixed sequence of masking and shifting operations:

    static int ffs_imp(int i) {
        byte n = 1;
        if ((i & 0xffff) == 0) { n += 16; i >>= 16; }
        if ((i & 0x00ff) == 0) { n +=  8; i >>=  8; }
        if ((i & 0x000f) == 0) { n +=  4; i >>=  4; }
        if ((i & 0x0003) == 0) { n +=  2; i >>=  2; }
        if (i != 0) { return (n+((i+1) & 0x01)); } else { return 0; }
    }

Although in this case we can look at the C and Java code and see that they perform almost identical operations, the low-level operators available in C and Java do differ somewhat. Therefore, it would be nice to be able to gain confidence that they do, indeed, perform the same operation.

We can do this with a process very similar to that used to compare the reference and implementation versions of the algorithm in a single language.

First, we compile the Java code to a JVM class file.

$ javac -g FFS.java

Like with clang, the -g flag instructs javac to include debugging information, which can be useful to preserve variable names.

Using saw with Java code requires a command-line option -b that locates Java. Run the code in this section with the command:

$ saw -b <path to directory where Java lives> ffs_compare.saw

Alternatively, if Java is located on your PATH, you can omit the -b option entirely.

Both Oracle JDK and OpenJDK versions 6 through 8 work well with SAW. SAW also includes experimental support for JDK 9 and later. Code that only involves primitive data types (such as FFS.java above) is known to work well under JDK 9+, but there are some as-of-yet unresolved issues in verifying code involving classes such as String. For more information on these issues, refer to this GitHub issue.

Now we can do the proof both within and across languages (from ffs_compare.saw):

import "ffs.cry";
j <- java_load_class "FFS";
java_ffs_ref <- jvm_extract j "ffs_ref";
java_ffs_imp <- jvm_extract j "ffs_imp";

l <- llvm_load_module "ffs.bc";
c_ffs_ref <- llvm_extract l "ffs_ref";
c_ffs_imp <- llvm_extract l "ffs_imp";

print "java ref <-> java imp";
let thm1 = {{ \x -> java_ffs_ref x == java_ffs_imp x }};
prove_print abc thm1;

print "c ref <-> c imp";
let thm2 = {{ \x -> c_ffs_ref x == c_ffs_imp x }};
prove_print abc thm2;

print "java imp <-> c imp";
let thm3 = {{ \x -> java_ffs_imp x == c_ffs_imp x }};
prove_print abc thm3;

print "cryptol imp <-> c imp";
let thm4 = {{ \x -> ffs_imp x == c_ffs_imp x }};
prove_print abc thm4;

print "cryptol imp <-> cryptol ref";
let thm5 = {{ \x -> ffs_imp x == ffs_ref x }};
prove_print abc thm5;

print "Done.";

Here, the jvm_extract function works like llvm_extract, but on a Java class and method name. The prove_print command works similarly to the prove followed by print combination used for the LLVM example above.