stp div by zero failure

[kren1]

I've come across a program that causes fuzzball to give STP a query that causes division by zero error:

int g_279 = 1;
int  a = 0;
static int magic_symbols[4] = {1,0,0,4};

int main() {
  g_279 = *magic_symbols;
  if(g_279 > 1) exit(0);
  if(g_279 < 1) exit(0);

  for (int i = 1; i >= 0; i--) {
    a = (g_279 == 0 ? 0 : 0 / g_279);
    a ?: 0;
    printf("end loop body \n");
  }
}

run with something like

clang -std=c99  test323.c && fuzzball -solver-path .../stp  -linux-syscalls $(objdump -D a.out | grep -P "magic_symbols"  | awk '{print  "-symbolic-string 0x"i $1 "+16"}' | tail -n1 |  head -n1) ./a.out -- a.out

Gives

end loop body
WARNING
Fatal Error: division by zero error
stp: Error: division by zero error
STP died with result code 255
STP query and results are in fuzzball-tmp-5/fuzz-6.stp and fuzzball-tmp-5/fuzz-6.stp.out
Fatal error: exception Exec_exceptions.SolverFailure

Whereas a native run prints end loop body twice as expected. I'm using clang version 3.4 and STP version 7f9069fc5ed518a225848300d1f70e055e1c60fc from bitblaze-fuzzball/stp . Note that this bug doesn't show when compiled with some compilers. For example when compiled with gcc version 4.6.3, it doesn't show up for me.

I'm also attaching the stp query that casuses the div by zero error, but I don't think this is entierly STPs fault, so I'm reporting it here:

input0_0 : BV(8);
input0_1 : BV(8);
input0_2 : BV(8);
input0_3 : BV(8);
t0 : BV(32) = ((input0_3 @ input0_2) @ (input0_1 @ input0_0));
t3 : BOOLEAN = ((0b1 = BVPLUS(32, t0,0hffffffff)[31:31]) XOR BVSLT(t0, 0h00000001));
t4 : BOOLEAN = ((t0 = 0h00000001) OR ((0b1 = BVPLUS(32, t0,0hffffffff)[31:31]) XOR t3));
QUERY(NOT (((SBVDIV(64, 0h0000000000000000,SX(t0, 64))[31:0]) = 0h00000000)
  AND (NOT (t0 = 0h00000000))
  AND (NOT ((0b1 = BVPLUS(32, t0,0hffffffff)[31:31]) XOR t3))
  AND t4
  AND (t0 = 0h00000000)));
COUNTEREXAMPLE;

Here is the actual binary for reference stpDivZero.zip

[smcc]

Though I'm somewhat biased, I tend to blame STP for this behavior. The precise semantics of division by zero are hard for SMT solver authors to agree on, but the semantics shouldn't matter much in a case like this where the path condition constrains the divisor to be non-zero. (The second argument to the SBDIV is "SX(t0, 64)", the sign-extension of t0, but elsewhere you'll see "(NOT (t0 = 0h00000000))", i.e., t0 != 0.)

I also think the STP developers agree in as much as the latest upstream versions no longer die with a division by zero error. An entry point into some of the discussion on their issue tracker, with links back to SMTLIB discussions, is:

https://github.com/stp/stp/issues/223

So one thing this brings up is that we're overdue for an update of the bitblaze-fuzzball/stp branch. If you don't care about the "-solver stpvc" library interface, you can already try using newer upstream stp binaries as external programs (in the example, just change -solver-path). I think the library interface is also one reason I've been putting off updating the branch: I'd like to recommend building STP with cryptominisat and m4ri, but I worry that all of those transitive dependencies will need to be reflected in FuzzBALL's static linking. So maybe the thing to do is to just deprecate that interface. It is convenient in simple cases not to need an external solver binary, but I think being non-incremental cancels out an overhead savings you'd hope to get from being in the same process.

But since you're reporting this as a FuzzBALL issue, and you say "I don't think this is entirely STP's fault", do you have any suggestions for something FuzzBALL should do differently? Generate a different formula to give to STP? Deal with the solver failure in a different way?

[kren1]

Thanks for taking the time to have a look at this and the detailed response. I reported it here because I had some trouble setting up with newest version of stp, so I thought there was greater coupling between the two. I also wasn't sure that fuzzball is passing the non zero constraint correctly ...

[kren1]

I'm encountering this issue frequently again, so I had some more thoughts about what fuzzball should do. When encountering a possible division by zero, fuzzball should basically branch on weather divisor is zero or not. If the division by zero path is feasible it should report it as a possible bug in the program and then explore the other path normally instead of crashing out.

Instead of branching it could just look at the stp errors and if there is a div by zero error, retry the query with the divisor constrained not to equal zero, while issuing a warning?

To motivate this, consider I'm trying to use fuzzball to prove 2 implementations of the same functions are the same like:

#include <assert.h>
int g_279 = 1;
int  a = 0;
int g_34 = 1;
static int magic_symbols[4] = {1,0,0,4};

int func(int x) {
    return 100 / x;
}

int func1(int x) {
    return 100 / (x  + 2 - 2);
}

int main() {
  g_279 = *magic_symbols;
  g_34 = *(magic_symbols +1);
  if(g_34 != g_279) exit(0);
  assert(func(g_279) == func(g_34));
    return 0;
}

There is obviously a division by zero error there, however the two implementation are the same. So I don't think fuzzball should crash. As another note fuzzball crashes with sdiv by zero error in stp, when using version 2.1.2. I also tried using version 2.2.0(which promises to solve div by zero errors), but that crashed with a different error:

Fatal Error:
stp: Error:
syntax error: line 1
syntax error, unexpected STRING_TOK, expecting LPAREN_TOK
  token: input0_4
STP died with result code 255
STP query and results are in fuzzball-tmp-7/fuzz-1.stp and fuzzball-tmp-7/fuzz-1.stp.out

[smcc]

On the STP version 2.2.0 compatibility issue, see my recent commit 6e4609bf.

[vaibhavbsharma]

On the FuzzBALL feature to allow execution to continue beyond feasible division-by-zero paths, please see my recent commit f3ab363. This change causes FuzzBALL to disqualify a path if it finds a zero divisor in a division or modulo operation. You can turn on -trace-stopping and -trace-iterations to see different iterations and the reason why they end. Please try this change out and let me know how it goes.

[kren1]

@smcc Thanks for fixing the compatibility issue.

@vaibhavbsharma That is exactly what I was looking for! Works like a charm. Cheers.