angr / claripy

An abstraction layer for constraint solvers.
BSD 2-Clause "Simplified" License
275 stars 90 forks source link

Handle rare edge case where solver has 0 variables #332

Closed fmagin closed 1 year ago

fmagin commented 1 year ago

Under arcane circumstances I don't understand, this can happen. It didn't happen in a venv from a few days ago, but it happens now, despite using the same pinned commits of the angr repos. It also only happens with pypy and not CPython.

zwimer commented 1 year ago

Thanks for the PR! :) One note: Since the case is so rare it may be desirable to make it the second check in the if condition rather than the first, as python does lazy evaluation.

I don't deal with the frontend stuff though so I'll leave this to the other maintainers else-wise.

fmagin commented 1 year ago

Ah, sorry that I didn't explain this properly, the edge case is that min(iter(s.variables)) crashes with a ValueError: arg is an empty sequence if s.variables is empty. So the check has to come first.

The same guard/check seems to have been applied in another line in this file too, that's why I assumed that adding this check would be a good enough fix: https://github.com/angr/claripy/blob/0ac0812d77d7377fedc8a00dbd7bcf4f2df2990c/claripy/frontends/composite_frontend.py#L209

This might only mask some deeper issue, but because self._unchecked_solvers is a weakref.WeakSet I assume that typically a solver with 0 variables was already garbage collected before hitting this code, but in some rare cases it isn't.

And by rare I mean: The testcase that failed started failing has been running on every commit in our internal CI at work for ~2 years and this is the first time this issue came up IIRC

fmagin commented 1 year ago

FWIW our code at work isn't triggering this bug anymore, without any code changes, simply by building a new venv. Still seems reasonable to merge this, just in case this ever shows up again