Exception when a possibly negative value is cached for a shift amount

[SolalPirelli]

Run the following:

import angr
import claripy

proj = angr.Project("/bin/true")
state = proj.factory.blank_state()

x = claripy.BVS("x", 64)
state.solver.add(x < 100)

# Comment out this assert and the problem goes away (presumably because it's in the concrete backend used as a cache)
assert state.solver.satisfiable()

problem = 1 >> (1 - x)
state.solver.add(problem >= 0)
assert state.solver.satisfiable()

This leads to claripy.errors.BackendError: <claripy.backends.backend_concrete.BackendConcrete object at 0x7eff53c67880> can't handle operation __rshift__ (BV) due to a failed conversion on a child node.

Turn the >> into a claripy.LShR and the error message is more informative:

...
  File "/home/solal/.virtualenvs/test/lib/python3.8/site-packages/claripy/bv.py", line 444, in LShR
    return BVV(a.value >> b.signed, a.bits)
ValueError: negative shift count

This can be fixed by replacing .signed by .value in the right places in bv.py but since __rshift__ has a comment arithmetic shift uses the signed version, that does not sound right. Perhaps the code should check for a negative signed value and return 0 in that case?

[rhelmot]

What does z3 give you when you give it a similar problem?

[SolalPirelli]

(declare-const a (_ BitVec 8))
(declare-const b (_ BitVec 8))

(assert (bvslt b #x00))
(assert (bvsgt (bvlshr a b) #x00))

(check-sat)
(get-model)

Z3 says unsat, but replace bvsgt with = and it finds a = #x00, b = #x80. Adding constraints on a such as (assert (= a #x01)) finds a model with the same b, so it seems from Z3's perspective (positive >> negative) == 0.

SMT-LIB defines bvlshr as [[(bvlshr s t)]] := nat2bv[m](bv2nat([[s]]) div 2^(bv2nat([[t]]))) where bv2nat returns a number from 0 to 2**bits-1 (here).

Which makes me think the entire shifting logic is that file is backwards and should use unsigned versions instead. Looking at git blame, it appears the "shift uses signed" comment was intended to apply to the left operand, not the right one: https://github.com/angr/claripy/commit/4cc4ac43627357163c1f8d7be5aa4975095095f8 That is still wrong per that SMT-LIB definition, though.

[github-actions[bot]]

This issue has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

[github-actions[bot]]

This issue has been closed due to inactivity.