How to check if a variable can be negative?

[frapik99]

Hi,
I'm trying to understand how to check if a number can be negative.

I write this piece of code but I'm note that it is correct:

import claripy
a = claripy.BVV(0xffffffff, 32)
b = claripy.BVS('var_b', 32)
s = claripy.Solver()
s.add(claripy.SLT(b, a))

print s.satisfiable()
print s.eval(b, 1)

The output was:

True
(4294967294L,)

The goal is to check if b can be negative.

is it the proper way of doing it?

Thanks

[zardus]

That looks like it should work, but it seems more accurate to set a = claripy.BVV(0, 32). -1 is negative, after all.

[axt]

I'm not sure if this approach is correct, but this is how I try to infer ranges of singed variables:
https://github.com/axt/angr-utils/blob/master/angrutils/expr.py

If you check the sat_negative function, what I do is to evaluate if the highest bit of the variable being one could be satisfied.

[rhelmot]

Can confirm that this approach is correct too. I have no idea what the performance looks like compared to the inequality method, but my suspicion is that z3 is more heavily optimized for inequalities than bit-extraction logic. I really wish we had someone on z3 to whom we can ask these questions, or at least someone with a background in SMT solving...

[zardus]

For bit-vectors, it wouldn't surprise me if the bit-extraction logic was better, in terms of Z3 being able to come up with simpler constraints internally for the actual solve, but I'm definitely as clueless about the inner workings of SMT solvers as the average bear.

[ltfish]

I really wish we had someone on z3 to whom we can ask these questions, or at least someone with a background in SMT solving

Just open an issue on Z3Solver GitHub repo!