scCryptolType: unsupported type panic

[ChrisEPhifer]

Consider the following C function, in test.c and compiled to test.bc:

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

And the following SAWScript which attempts to verify this function in the simplest manner possible:

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 causes a panic in cryptol-verifier, with the following output:

%< --------------------------------------------------- 
  Revision:  f72b9cf80ecc73de169ef2ea11ed8ff446e3faef
  Branch:    HEAD
  Location:  scCryptolType
  Message:   scCryptolType: unsupported type (var_blk0!_52 : Prelude.Nat)
-> (var_off0!_53 : Prelude.Vec 64 Prelude.Bool)
-> Prelude.Bool
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-verifier-0.1-1QjHQ00Twwj8Hfjv7aovd3:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:1363:19 in cryptol-verifier-0.1-1QjHQ00Twwj8Hfjv7aovd3:Verifier.SAW.Cryptol
%< ---------------------------------------------------

Which appears to be a very similar failure to that seen in #13 (using only SAW primitives.)

[brianhuffman]

As of GaloisInc/saw-script@7e6e0ab, it looks like this produces a different error message:

[18:50:02.415] Loading file "/Users/huffman/Documents/saw/issue31.saw"
[18:50:02.419] Verifying inc_p ...
[18:50:02.419] Simulating inc_p ...
[18:50:02.420] Checking proof obligations inc_p ...
[18:50:02.422] 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

[brianhuffman]

Bisection shows that the panic was fixed in revision GaloisInc/saw-script@f7bb948, which was part of GaloisInc/saw-script#728.

The remaining error message is due to the fact that crucible_fresh_pointer introduces a fresh saw-core variable of type Nat, but the saw-core proof backends can't handle symbolic variables of that type. As the remaining problem is not related to the cryptol-verifier package, I suggest closing this ticket and opening a new ticket for the could not create uninterpreted type for Prelude.Nat error on the saw-script issue tracker.

[brianhuffman]

Upon closer inspection, it appears that this is exactly the same problem as #13, so I'm closing as duplicate.