SAW Simulator error: Verifier.SAW.Simulator.BitBlast.toBool [_,_,_,_,_,_,_,_]

[thoughtpolice]

Consider the following example - an attempt to verify BLAKE-256:

$ git clone [email protected]:9ed2113ae0b9631d8319.git
Cloning into '9ed2113ae0b9631d8319'...
remote: Counting objects: 9, done.
remote: Compressing objects: 100% (9/9), done.
remote: Total 9 (delta 1), reused 0 (delta 0), pack-reused 0
Receiving objects: 100% (9/9), 9.91 KiB | 0 bytes/s, done.
Resolving deltas: 100% (1/1), done.
Checking connectivity... done.
$
$ cd 9ed2113ae0b9631d8319

Makefile included:

$ make
clang -emit-llvm -o blake256.bc -c blake256.c
saw blake256.saw
Loading module Cryptol
Loading file "blake256.saw"
Loading module blake256
Performing blake256 equivalence tests
Loading LLVM bytecode
Extracting the Blake256 encryption function...
Time:    10.643s
Bit blasting the terms to produce AIGs...
Time:     0.751s
Verifier.SAW.Simulator.BitBlast.toBool [_,_,_,_,_,_,_,_]
make: *** [all] Error 1

This seems like a legitimate bug. I have a ChaCha20 specification OTOH that takes nearly a minute to extract, but correctly works, and uses a very similar SAW script, so I have no clue how to work around this or what the culprit might be.

Thanks.

[atomb]

With the current version of SAW, on my machine, I'm instead encountering the problem that the extraction process doesn't terminate. I'll look into it more.

[brianhuffman]

I have a minimal example that produces the same error.

test.c:

#include <stdint.h>
uint8_t test(uint8_t x[4]) {
  return x[1];
}

test.saw:

m <- llvm_load_module "test.bc";
t <- llvm_verify m "test" [] do {
  x <- llvm_var "x" (llvm_array 4 (llvm_int 8));
  llvm_return {{ x@1 }};
  llvm_verify_tactic abc;
};

Output:

$ clang -emit-llvm -c -o test.bc test.c
$ saw test.saw
Loading module Cryptol
Loading file "test.saw"
Verifier.SAW.Simulator.BitBlast.toBool [_,_,_,_,_,_,_,_]

If we replace abc with do { print_goal; abc; }, then we can see that the error is due to a type-incorrect term being constructed by the llvm simulator. The term starts with a bound variable \(Ident "x"::Prelude.Vec 4 (Prelude.Vec 8 Prelude.Bool)) (yes, the variable's name is Ident "x", including the space and quotation marks). Later in the term we see the subterm (Prelude.bvAdd 64 Ident "x" (Prelude.bvNat 64 1)), i.e., the variable of type [4][8] is being added to a value of type [64], which is obviously a type error.

[atomb]

It looks as though this is due to insufficient type checking by llvm_symexec, along with somewhat strange semantics for the expected types of arguments. If you replace the following line in blake256.saw:

                , ("*inp", inp,  1)

with this instead

                , ("*inp", {{ inp @ 0 }},  1)

then it works. Ticket #21 is about this same issue. I'll be revisiting a lot of the design of llvm_symexec over the next weeks, and stuff like this should improve a lot.

I should add that when I say "works" above I mean just that it successfully starts a CEC run. I let it run for a while (maybe 20 minutes) without any result, and killed it. For other modern hash functions, a monolithic CEC isn't feasible, so I expect it won't be for Blake256, either. I may experiment with writing a compositional equivalence proof for this case at some point, if you don't beat me to it.

[atomb]

Most of the type checking issues underlying this have been fixed. The example @brianhuffman provided works, and the slightly modified version of the Blake256 example I suggested also works. The remaining issues should be fixed as part of #127.