Strange behaviour with 124 constant

[kren1]

I found this strange behaviour. Given a program:

unsigned int g_893 = 124;
int safe_sub(long long p1, int p2) {
  return (p1 ^ ~9223372036854775807LL) - p2 < 0 ? 0 : p2;
}
static unsigned int magic_symbols[1] = {0};

int main() {
  g_893 = *magic_symbols;
  if(g_893 > 124) exit(0);
  if(g_893 < 124) exit(0);
  printf("%u\n", safe_sub(1UL ^ g_893, 1));
}

When compiled with version 3.4-1ubuntu3~precise2 and run like:

clang-3.4 test.c && $FUZZBALL -solver-path $STP -linux-syscalls $(objdump -D a.out | grep -P "magic_symbols"  | awk '{print  "-symbolic-region 0x"i $1 "+4"}' | tail -n1 |  head -n1) ./a.out -- a.out

It prints out 1, whereas native execution with g_893 set to 124, prints out 0. There are a couple of interesting notes here:

• If I change -symbolic-region to -symbolic-string it works fine by printing 0.
• If I initialise magic_symbols with 124, instead of 0 (to be able to use same binary for native and symbolic runs), fuzzball crashes with: Fatal error: exception Failure("int_of_string")
• The bug does not appear when compiled with gcc version 4.6.3 (Ubuntu/Linaro 4.6.3-1ubuntu5).
• If the function is inlined like so: printf("%u\n", ((1UL ^ g_893) ^ ~9223372036854775807LL) - 1 < 0 ? 0 : 1); fuzzball just keeps exploring branches.

Also attaching the binary: 124Const.zip

[smcc]

Thanks for the report, and for including a small test case. The fact that changing -symbolic-region to -symbolic-string made the problem go away was probably the strongest sign that this was a bug in FuzzBALL's formula processing. By turning on lots of tracing options and diffing the outputs, I believe I've tracked the problem down to an incorrect formula simplification rule, which I've disabled; that change makes the failure go away in my testing.

I think the Fatal error: exception Failure("int_of_string") is caused by your awk/shell address-adjusting scripting. It does sound like an internal error, but it's what FuzzBALL prints when part of a command-line option that is supposed to be a number cannot be parsed as one, in this case because you're passing a command-line option that looks like:

-symbolic-region 0x804a024:+4

When you set the first entry of magic_symbols to 124, objdump -D will disassemble the first two bytes as a legal branch instruction

804a024:       7c 00                   jl     804a026 <magic_symbols+0x2>

which matches in the grep but gets that stray ":" through the awk script. In this case you could probably get the match you want by doing head before tail. But more generally I'd suggest using nm instead of objdump -D to get symbol values in shell scripting.

[kren1]

Thanks for taking the time to debug this and providing a patch. Also thanks for suggesting using nm that does sound like a much better idea!