type error on import from LLVM code

[kouzdra]

#include <stdint.h>

typedef int32_t my_int;

my_int ref (my_int n) {
return n/2;
}

my_int imp (my_int n) {
return n>>1;
}

during checking by script:

l <- llvm_load_module "div2.bc";
ref <- crucible_llvm_extract l "ref";
imp <- crucible_llvm_extract l "imp";

let thm1 = {{ \x -> ref x == imp x }};
result <- prove abc thm1;
print result;

produces the following error:

[18:58:10.555] Proving equivalence: ref == imp [18:58:10.582] Cryptol error: [error] at /home/msk/WORK/SNOB/SAW/sl-basic/sandbox/div2_llvm.saw:11:30--11:33: Type mismatch: Expected type: 33 Inferred type: 32

Actually - type of ref is:

(arg_0 : Prelude.bitvector 32) -> Prelude.Vec **33** Prelude.Bool

not

(arg_0 : Prelude.bitvector 32) -> Prelude.Vec **32** Prelude.Bool

as imp, and should be.

[brianhuffman]

The problem is in the saw-core backend of crucible, which is generating saw-core terms with the wrong types. I created a ticket: GaloisInc/crucible#356.

[brianhuffman]

Once pull request GaloisInc/crucible#357 is merged and we update the submodule version, we should be all set.

[brianhuffman]

Fixed in e0db646.