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 https://github.com/angr/claripy/commit/9d4b861ecfd4763be75c2ef7563a895aafe9db4f.

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