"bit vectors must have same length64 32"

[weaversa]

saw bignum.saw gives some interesting results depending on the solver used (see the very bottom of bignum.saw).

w4 complains that "bit vectors must have same length64 32".

z3 gives a counter example (which I cannot understand).

abc gives:

CallStack (from HasCallStack):
  assert, called at src/Data/AIG/Operations.hs:814:14 in aig-0.2.6-HPx7nWFCiKnHUp2KsvacUU:Data.AIG.Operations

cvc4 gives:

[14:04:11.957] 
*** Data.SBV: Unexpected non-success response from CVC4:
***
***    Sent      : (set-option :global-declarations true)
***    Expected  : success
***    Received  : unsupported
***
***    Exit code : ExitFailure (-15)
***    Executable: /opt/local/bin/cvc4
***    Options   : --lang smt --incremental --interactive --no-interactive-prompt
***
***    Reason    : Backend solver reports it does not support this option.
***                Check the spelling, and if correct please report this as a
***                bug/feature request with the solver!

w4issue.tar.gz
This is a work in progress, so don't expect it to look nice...but I thought an issue was warranted.

[weaversa]

I now have one where the proof goes through with z3 but where w4 gives the 64/32 error. I could share if it would help.

[brianhuffman]

This error message originates in the saw-core-what4 package. It might be due to us constructing ill-typed saw-core terms. I'll look into it.

[brianhuffman]

I tried sticking a check_goal command before the final prover call in the bignum_verify command: Indeed, it reveals that the proof goal is ill-typed. It looks like we have an assumption containing a predicate of the form (64:[64]) == (4:[32]). I'll see if I can find where that's coming from.

[brianhuffman]

I found the problem: The terms passed as arguments to crucible_execute_func have types that don't match the ones in the C function. Here's the offending declaration from mpz.saw:

//void mpz_import (mpz_t rop, size_t count, int order, size_t size, int endian, size_t nails, const void *op)
let mpz_import_spec (count : Int) (size : Int) = do {
  ropp <- pointer WRITE (struct_t "__mpz_struct");
  opp <- pointer CONST (llvm_array (eval_int {{ `(count * size) : [32] }}) uint8_t);

  execute [ropp,
           from_cryptol {{ `count : [32] }},
           from_cryptol {{ 1 : [32] }},
           from_cryptol {{ `size : [32] }},
           from_cryptol {{ 0 : [32] }},
           from_cryptol {{ 0 : [32] }},
           opp];

  rop' <- mpz_t' (eval_int {{ `(count * size * 8) : [32] }}) "rop'" ropp;

  op' <- variable (llvm_array (eval_int {{ `(count * size) : [32] }}) uint8_t) "op'" FRESH;
  points_to opp op'.s;

  let (ropt', opt) = (rop'.t, op'.t);
  postcond {{ from_mpz`{b=count*size*8} ropt'.value == join opt }};
};

The C function prototype shows the numeric argument types alternating between int (32 bits) and size_t (64 bits). However, the saw-script spec supplies terms of type [32] for all of them. Changing the type signatures of the appropriate arguments from [32] to [64] fixes the internal type error.

The real bug here is that saw doesn't check that the types of the arguments to crucible_execute_func match the expected LLVM argument types from the bitcode file. (I suspect that crucible_llvm_verify actually does check them, but that crucible_unsafe_assume_spec does not.) We should fix that.

[brianhuffman]

This issue is related to #443, which is about type checking of function return values. Ultimately we should probably use the same type-compatibility relation to check function arguments as we use to check return values.

[brianhuffman]

Looking at the source code, it appears that my suspicion was right: There is some code for checking type compatibility of function arguments, but it is only called by crucible_llvm_verify, and not for crucible_unsafe_assume_spec.

[brianhuffman]

With #714, saw bignum.saw now gives an appropriate error message:

[01:25:00.205] Loading file "/Users/huffman/Documents/saw/issue707/w4issue/bignum.saw"
[01:25:00.208] Loading file "/Users/huffman/Documents/saw/issue707/w4issue/mpz.saw"
[01:25:00.210] Loading file "/Users/huffman/Documents/saw/issue707/w4issue/llvm.saw"
[01:25:00.760] Assume override __gmpz_init
[01:25:01.165] Stack trace:
"mpz_import_ov" (/Users/huffman/Documents/saw/issue707/w4issue/bignum.saw:114:22-114:35):
"crucible_llvm_unsafe_assume_spec" (/Users/huffman/Documents/saw/issue707/w4issue/bignum.saw:109:25-109:57):
Type mismatch in argument 2 when verifying "__gmpz_import"
Argument is declared with type: i32
but provided argument has incompatible type: i64
Note: this may be because the signature of your function changed during compilation. If using Clang, check the signature in the disassembled .ll file.

[linesthatinterlace]

The "bignum.saw" reference here - is that public? (I am currently trying to figure out how I'd do verification of a program that makes extensive use of GMP - if the library already exists in some form...)

[brianhuffman]

There's a link to a tarball in the original post.

[weaversa]

Better yet...see it in action over at https://github.com/weaversa/electionguard-c/blob/master/test/saw/bignum.saw

Though the stack branch might have something slightly up to date. It's a work in progress, so mind the dust.