angr / angr/claripy

ModelCacheMixin does not handle extra_constraints correctly for min

Offen
#324 3 Kommentare 0 Reaktionen 1 zugewiesene Person Beansprucht von @ltfish Auf GitHub ansehen
bug
Vorherrschende Sprache
Python
Sterne
334
Forks
105
Ø Merge
6 Std. 1 Min.
Gemergte PRs (30 T.)
3

Beschreibung

### 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_

Beitragsleitfaden

Für dieses Repository ist kein Beitragsleitfaden indexiert

Bewertung

Dieses Issue wurde noch nicht bewertet.

Neue Issues direkt in Ihr Postfach

Eine kurze Übersicht über anfängerfreundliche GitHub-Issues.