Bug in bitwise_or_simplifier?

[edmcman]

Hello,

I am encountering a crash in angr. The exact scenario is difficult to reproduce, but I think the following information might be sufficient.

Here is a backtrace of the Claripy exception:

(Pdb) traceback.print_exc()
Traceback (most recent call last):
  File "/usr/local/lib/python3.7/site-packages/angr/engines/vex/claripy/irop.py", line 375, in calculate
    return self.extend_size(self._calculate(args))
  File "/usr/local/lib/python3.7/site-packages/angr/engines/vex/claripy/irop.py", line 437, in _op_mapped
    return getattr(claripy.ast.BV, o)(*sized_args)
  File "/usr/local/lib/python3.7/site-packages/claripy/operations.py", line 53, in _op
    simp = _handle_annotations(simplifications.simpleton.simplify(name, fixed_args), args)
  File "/usr/local/lib/python3.7/site-packages/claripy/simplifications.py", line 42, in simplify
    return self._simplifiers[op](*args)
  File "/usr/local/lib/python3.7/site-packages/claripy/simplifications.py", line 604, in bitwise_or_simplifier
    elif (a == b).is_true():
  File "/usr/local/lib/python3.7/site-packages/claripy/operations.py", line 53, in _op
    simp = _handle_annotations(simplifications.simpleton.simplify(name, fixed_args), args)
  File "/usr/local/lib/python3.7/site-packages/claripy/simplifications.py", line 42, in simplify
    return self._simplifiers[op](*args)
  File "/usr/local/lib/python3.7/site-packages/claripy/simplifications.py", line 227, in eq_simplifier
    simp = SimplificationManager.zeroext_extract_comparing_against_constant_simplifier(operator.__eq__, a, b)
  File "/usr/local/lib/python3.7/site-packages/claripy/simplifications.py", line 950, in zeroext_extract_comparing_against_constant_simplifier
    return op(ast.all_operations.ZeroExt(to_extend, a_inner_expr), b)
  File "/usr/local/lib/python3.7/site-packages/claripy/operations.py", line 53, in _op
    simp = _handle_annotations(simplifications.simpleton.simplify(name, fixed_args), args)
  File "/usr/local/lib/python3.7/site-packages/claripy/simplifications.py", line 42, in simplify
    return self._simplifiers[op](*args)
  File "/usr/local/lib/python3.7/site-packages/claripy/simplifications.py", line 232, in eq_simplifier
    simp = SimplificationManager.zeroext_comparing_against_simplifier(operator.__eq__, a, b)
  File "/usr/local/lib/python3.7/site-packages/claripy/simplifications.py", line 968, in zeroext_comparing_against_simplifier
    b_highbits = b[b.size() - 1 : b.size() - a_zeroext_bits]
  File "/usr/local/lib/python3.7/site-packages/claripy/ast/bv.py", line 72, in __getitem__
    return Extract(left, right, self)
  File "/usr/local/lib/python3.7/site-packages/claripy/operations.py", line 50, in _op
    raise ClaripyOperationError(msg)
claripy.errors.ClaripyOperationError: Extract low must be <= high

And here are the args of the bitwise OR operation:

(Pdb) print(args)
(<BV8 (0 .. mem_c0000000_255_32{UNINITIALIZED}[14:0])[15:8]>, <BV8 128>)

Any help would be appreciated.

[edmcman]

(Pdb) list
963             can be eliminated.
964             """
965             if op in {operator.__eq__, operator.__ne__} and a.op == "ZeroExt" and b.op == "BVV":
966                 # check if the high bits of b are zeros
967                 a_zeroext_bits = a.args[0]
968  ->             b_highbits = b[b.size() - 1 : b.size() - a_zeroext_bits]
969                 if (b_highbits == 0).is_true():
970                     # we can get rid of ZeroExt
971                     return op(a.args[1], b[b.size() - a_zeroext_bits - 1 : 0])
972                 elif (b_highbits == 0).is_false():
973                     # unsat
(Pdb) print(a_zeroext_bits)
-7
(Pdb) print(a)
<BV8 0#-7 .. mem_c0000000_383_32{UNINITIALIZED}[14:0]>
(Pdb) print(a)

Not sure where the -7 is coming from.

[edmcman]

This code doesn't seem quite right to me:

https://github.com/angr/claripy/blob/master/claripy/simplifications.py#L934

I think a.size() - a_hi is supposed to be a_arg.size() - a_hi unless there is a simplification I'm not seeing.

[edmcman]

I'm really unsure what the original code was shooting for. My expression looks something like this:

(0 .. stuff)[15:8] == 128:u8

Obviously the high bits of the concat are zeros. So we we could replace (0 .. stuff) with ZeroExt(stuff.size() + 1, stuff). But the extract is still there, so the final expression would be ZeroExt(stuff.size() + 1, stuff)[15:8] == 128:u8.

The current code appears to return ZeroExt(-7, stuff) == 128:u8.

The other concerning thing is that the comments say If the high bits of b are 0, Extract and Concat/ZeroExt can be eliminated. The high_bits_are_zeros flag is being set, but the extract can definitely not be eliminated! The only way I could see the extract being eliminated is if it only extracted zeros. Otherwise the extract needs to be there to get rid of the lower bits excluded by the extract.

[ltfish]

This is probably my code. I'll take a look after my meetings today.

[ltfish]

I'm going to bed now. I will come back tomorrow to explain my fix better.

Thanks for reporting!

[edmcman]

Thanks for taking a look at this! Just took a quick look at the fix. I think the constraint that lo == 0 was the missing piece that I was having trouble inferring.

One quick thought though: it looks like the rule doesn't really depend on b anymore. So does there really need to be a == b or != b for this simplification to apply?

[ltfish]

I think the constraint that lo == 0 was the missing piece that I was having trouble inferring.

That was my intent when I wrote this optimization. Obviously my test cases were too poor to catch that bug...

One quick thought though: it looks like the rule doesn't really depend on b anymore. So does there really need to be a == b or != b for this simplification to apply?

You are definitely right. However, I do not have enough evidence that shows if this optimization is necessary for other comparison operators during symbolic execution. Hence, I decided to fix the docstring, leave a TODO note, and merge the fix.

[edmcman]

Thanks again @ltfish!

[ltfish]

You are welcome!