BASIL produces ill-typed Boogie program

[aaronbembenek]

BASIL (commit 75603e0bf465cf04c4493271daa72283e568af8f) produces an ill-typed Boogie program given the attached files. I ran these commands and got this output:

$ ./mill run --input loop_to_x_O3.adt --relf loop_to_x_O3.relf --spec loop_to_x_O3.spec --output loop_to_x_O3.bpl
[INFO]   [!] Loading Program
[INFO]   [!] Removing external function calls
[INFO]   [!] Stripping unreachable
[INFO]   [!] Removed 17 functions (1 remaining)
[INFO]   [!] Translating to Boogie
[INFO]   [!] Writing file...
$ boogie loop_to_x_O3.bpl
loop_to_x_O3.bpl(135,4): Error: mismatched types in assignment command (cannot assign bv32 to bv64)
1 type checking errors detected in loop_to_x_O3.bpl

I compiled the original C source code (attached) with gcc -fno-plt -fno-pic -O3.

Thanks!

loop_to_x_O3.zip

[ailrst]

The type error is present from the adt file isn't caught since basil does very minimal type checking internally...

      Def(
       Tid(1_048, "%00000418"),
       Attrs([
        Attr("address", "0x618"),
        Attr("insn", "add w0, w0, w1")]),
       Var("R0", Imm(64)), PLUS(Extract(31, 0, Var("R0", Imm(64))), Extract(31, 0, Var("R1", Imm(64))))),

Which lifter are you using? This looks similar to the issues from the old primus lisp lifter plugin https://github.com/UQ-PAC/BASIL/issues/84. We only really support aarch64 binaries lifted with the asli lifter now.

Re-compiling and lifting the c program with aarch64-linux-gnu-gcc and the bap-aslp package (which uses the asli lifter plugin) here doesn't reproduce the error.

[aaronbembenek]

I had been using whichever lifter is the default when installing bap via opam. I reinstalled bap using the nix setup you linked and things seem to be working now. Thanks!

[ailrst]

Awesome :+1: