llvm_verify_x86 fails to find struct field name that llvm_verify can find

[RyanGlScott]

Given this C code:

#include <stdint.h>

struct s {
  uint8_t x1;
  uint8_t x2;
};

uint8_t get_x2(struct s *ss) {
  return ss->x2;
}

int main() {
  return 0;
}

And this SAW specification:

enable_experimental;

let get_x2_spec = do {
  ss <- llvm_alloc (llvm_alias "struct.s");
  z <- llvm_fresh_var "z" (llvm_int 8);
  llvm_points_to (llvm_field ss "x2") (llvm_term z);
  llvm_execute_func [ss];
  llvm_return (llvm_term z);
};

m <- llvm_load_module "test.bc";

llvm_verify     m              "get_x2" [] false get_x2_spec (w4_unint_z3 []);
llvm_verify_x86 m "./test.exe" "get_x2" [] false get_x2_spec (w4_unint_z3 []);

I would expect both the llvm_verify and llvm_verify_x86 invocations to succeed. In practice, however, only the former succeeds:

$ clang -g -frecord-command-line -O0 -c -emit-llvm test.c -o test.bc
$ clang -g -frecord-command-line -O0 -c test.c -o test.o
$ clang -g -frecord-command-line -O0 test.o -o test.exe
$ ~/Software/saw-0.9/bin/saw test.saw


[18:08:37.673] Loading file "/home/rscott/Documents/Hacking/C/test_bitfield_x86/test.saw"
[18:08:37.695] Verifying get_x2 ...
[18:08:37.695] Simulating get_x2 ...
[18:08:37.695] Checking proof obligations get_x2 ...
[18:08:37.695] Proof succeeded! get_x2
[18:08:37.696] Finding symbol for "get_x2"
[18:08:37.697] Found symbol at address 0x401110, building CFG
[18:08:39.232] Simulating function "get_x2" (at address 0x401110)
[18:08:39.232] Examining specification to determine preconditions
[18:08:39.234] Stack trace:
"llvm_verify_x86" (/home/rscott/Documents/Hacking/C/test_bitfield_x86/test.saw:14:1-14:16):
Unable to resolve field name: "x2"
No field names were found for this struct

[RyanGlScott]

Ah, I think I see why this is happening. Patch incoming.