ModelCacheMixin does not handle extra_constraints correctly for min

[g-kouv]

Description

Calling min with non-empty extra constraints results in an incorrect value, because the expression is found in _min_exhausted and cached results are incorrectly used to calculate the minimum.

A simple reproducer:

import claripy

s = claripy.Solver()
x = claripy.BVS("x", 64)
y = claripy.BVS("y", 64)
s.add(x - y >= 4)
s.add(y > 0)
print(s.min(x))
print(s.min(x, extra_constraints=[x > 1]))

The last line prints 3 even though the correct answer is 2.

A simple solution would skip checking _min_exhausted and using cached results when extra constraints are passed. A related bug seems to has been fixed previously in 9d4b861.

The issue also seems to apply to max and possibly eval.

Steps to reproduce the bug

No response

Environment

No response

Additional context

No response

[SanWieb]

I found a bug which I think it casued by the same issue: ModelCacheMixin takes a invalid solution from the cache.

Reproducer:

import claripy

ast = claripy.BVS("a", 64) + 0xff

s = claripy.Solver()

print("Min 1: ", s.min(ast))
print("Max 1: ", s.max(ast))

print("Min 2: ", s.min(ast))
print("Max 2: ", s.max(ast))

s = claripy.Solver()

print("")
print("Max 1: ", s.max(ast))
print("Min 1: ", s.min(ast))

print("Max 2: ", s.max(ast))
print("Min 2: ", s.min(ast))

Produced output:

Min 1:  0
Max 1:  18446744073709551615
Min 2:  255
Max 2:  18446744073709551615

Max 1:  18446744073709551615
Min 1:  0
Max 2:  257
Min 2:  0

[zwimer]

@g-kouv When I run this directly with z3: It looks like something wonky is happening in Z3 here, printing out the input and output of result = solver.check(extra_constraints) in backend_z3.py gives:

solver.check([UGE(x_0_64 - x_1_64, 4), UGT(x_1_64, 0), And(UGE(x_0_64, 0), ULE(x_0_64, 3))]) = sat

Which should be false mathematically unless I'm missing something obvious:

https://www.wolframalpha.com/input?i=x-y%3E%3D4+and+y%3E0+and+x%3E%3D0+and+x%3C%3D3
^ My sanity check

[zwimer]

Actually, I think that's the case. Adding the constraint x>y fixes the above, so the weird behavior I mentioned is likely due to emulating underflow/overflow.