SimZeroDivisionException: divide by zero!

[Mic92]

ERROR   | 2018-11-29 19:27:51,615 | root | Error while finding successor for recordings/w3m-27-02ba3d6.tar.gz
Traceback (most recent call last):
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/irop.py", line 377, in calculate
    return self.extend_size(self._calculate(args))
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/irop.py", line 740, in _op_divmod
    quotient = (args[0] // claripy.ZeroExt(self._from_size - self._to_size, args[1]))
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/claripy/operations.py", line 73, in _op
    return return_type(name, fixed_args, **kwargs)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/claripy/ast/base.py", line 131, in __new__
    r = operations._handle_annotations(eb._abstract(eb.call(op, args)), args)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/claripy/backends/__init__.py", line 207, in call
    obj = getattr(operator, op)(*converted)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/claripy/bv.py", line 40, in normalize_helper
    return f(self, o)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/claripy/bv.py", line 15, in compare_guard
    return f(self, o)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/claripy/bv.py", line 116, in __floordiv__
    raise ClaripyZeroDivisionError()
claripy.errors.ClaripyZeroDivisionError

The above exception was the direct cause of the following exception:

Traceback (most recent call last):
  File "/local/incoop/hase/hase/symbex/tracer.py", line 385, in execute
    state, num_inst=1  # , force_addr=addr
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/factory.py", line 49, in successors
    return self.project.engines.successors(*args, **kwargs)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/hub.py", line 128, in successors
    r = engine.process(state, **kwargs)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/engine.py", line 135, in process
    opt_level=opt_level)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/engine.py", line 55, in process
    self._process(new_state, successors, *args, **kwargs)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/engine.py", line 185, in _process
    self._handle_irsb(state, successors, irsb, skip_stmts, last_stmt, whitelist)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/engine.py", line 264, in _handle_irsb
    cont = self._handle_statement(state, successors, stmt)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/engine.py", line 372, in _handle_statement
    s_stmt = translate_stmt(stmt, state)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/statements/__init__.py", line 29, in translate_stmt
    s.process()
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/statements/base.py", line 37, in process
    self._execute()
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/statements/wrtmp.py", line 6, in _execute
    data = self._translate_expr(self.stmt.data)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/statements/base.py", line 44, in _translate_expr
    e = translate_expr(expr, self.state)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/expressions/__init__.py", line 14, in translate_expr
    e.process()
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/expressions/base.py", line 36, in process
    self._execute()
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/expressions/op.py", line 15, in _execute
    self.expr = translate(self.state, self._expr.op, [ e.expr for e in exprs ])
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/irop.py", line 939, in translate
    return translate_inner(state, operations[op], s_args)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/irop.py", line 960, in translate_inner
    return irop.calculate(*s_args)
  File "/local/incoop/hase/.direnv/python-3.6.6/lib/python3.6/site-packages/angr/engines/vex/irop.py", line 379, in calculate
    raise SimZeroDivisionException("divide by zero!") from e
angr.errors.SimZeroDivisionException: divide by zero!

[Airtnp]

The crash site is within libasan __sanitizer_get_allocated_size and from assembly code I have no idea why this happens.

[Airtnp]

A possible solution is to change angr irop returning unconstrained while zero division happening.

[Airtnp]

Like this. https://github.com/hase-project/angr/commit/2461603941af3fb9af0ef8717d32c4e2e4f6922f

[zardus]

Could you print out that basic block? There are cases where the following combination occurs:

1. VEX doesn't put the correct guards to explicitly check against the denominator being non-zero (and explicitly raise a signal).
2. Z3 actually doesn't handle symbolic division by zero properly, which is crazy but kinda makes sense.
3. At some point later, enough things get concretized that claripy ends up using the concrete backend, which does handle zero-division, and things explode.

We try to patch up VEX output to put the explicit exits in (here: https://github.com/angr/pyvex/blob/master/pyvex_c/postprocess.c#L328), but we could have missed something.