OS / Environment

Distributor ID: Ubuntu
Description: Ubuntu 18.04.4 LTS
Release: 18.04
Codename: bionic

Manticore version

0.3.3

Python version

3.6.9

Dependencies

Summary of the problem

Zero division causes an exception (halting execution) on all platforms. On Linux and Wasm (and maybe others, I haven't checked), a symbolic divisor is not constrained to be non-zero. Thus, states that should be abandoned because they would cause a divide-by-zero exception/trap are not.

Step to reproduce the behavior

int main(int argc, char *argv[]) {
    long d = argv[1][0];
    long y = 1 / (d - '0');
    return 0;
}

#!/usr/bin/env python3

from manticore.native import Manticore

m = Manticore("zero-div", ["zero-div", "+"])

# Instruction immediately after idiv.
@m.hook(0x400b80)
def hook(state):
    char = state.platform.argv[1][0]
    assert not state.can_be_true(char == 48)

m.run()

$ gcc -o zero-div zero-div.c -static
# Update the hook address to the one immediately after idiv.
$ ./zero_div.py
# AssertionError

Expected behavior

There should be no assertion error because it should be impossible for the input char to be 48. One can test this by running ./zero-div 0 and getting a crash.

Actual behavior

There is an AssertionError, meaning the state after a division by zero is a valid state.

One can produce this sort of error with Wasm as well.

Any relevant logs