Error "could not create uninterpreted type for Prelude.Nat" when using crucible_fresh_pointer

[brianhuffman]

Issues GaloisInc/cryptol-verifier#13 and GaloisInc/cryptol-verifier#31 both noted problems that arised when trying to do proofs about LLVM programs with specs that used crucible_fresh_pointer. Here is the small example program listed in GaloisInc/cryptol-verifier#31 (thanks to @ChrisEPhifer):

uint32_t *inc_p(uint32_t *p) {
    return p + 1;
}

and the saw-script spec:

let shift_spec = do {
    p <- crucible_fresh_pointer (llvm_array 5 (llvm_int 32));
    crucible_execute_func [p];
    crucible_return (crucible_elem p 1);
};

m <- llvm_load_module "./test.bc";

pf <- crucible_llvm_verify m "inc_p" [] false shift_spec z3;

This example no longer causes a panic, but it does cause an error:

[22:26:51.119] Loading file "/Users/huffman/Documents/saw/issue31.saw"
[22:26:51.131] Verifying inc_p ...
[22:26:51.132] Simulating inc_p ...
[22:26:51.134] Checking proof obligations inc_p ...
[22:26:51.136] Stack trace:
"crucible_llvm_verify" (/Users/huffman/Documents/saw/issue31.saw:9:7-9:27):
"z3" (/Users/huffman/Documents/saw/issue31.saw:9:58-9:60):
could not create uninterpreted type for Prelude.Nat

As I mentioned in GaloisInc/cryptol-verifier#13, the crucible_fresh_pointer statement introduces a Nat-typed variable that represents the block ID of the symbolic pointer. (For an allocated pointer, the block ID would be a concrete number.) The saw-core proof backends (e.g. z3) are not designed to handle symbolic variables of type Nat, so they fail.

To fix this, we could either extend the saw-core backends to properly support symbolic values of type Nat, or else we could modify the behavior of crucible_fresh_pointer to avoid generating a variable of type Nat (perhaps by using type Integer instead).