search

angr / claripy

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

Throw a different exception for when a solver timeout is hit #41

Closed peperunas closed 2 years ago

peperunas commented 7 years ago

While solving a challenge I noticed that the solver always throws an UnSatError exception even when the timeout is hit.

I think it should be treated in a different way. I'll try to look it up myself.

rhelmot commented 7 years ago

This is an extremely longstanding issue, and I would have sworn someone tried solving this already. @ team does anyone remember who did that?

peperunas commented 7 years ago

I'm trying to look into it but there are a lot of classes involved I'm staggered. If I can help in any way let me know. In the meantime I try to sort out all the things that are involved :-P

rhelmot commented 7 years ago

It looks like the answer to that question is "me". I found the old branch I started to fix this and pushed it to github, so now we can all see the work I did in this commit: https://github.com/angr/claripy/commit/40ad908f2a1b7d7455b1ed8887827695c101b390

It looks like most of the changes were disambiguating the UnsatError into the SatFailError -> (UnsatError, TimeoutError) hierarchy. That'll need to be propogated down to everyone that uses claripy, which was why we never merged this...

saullocarvalho commented 5 years ago

Is this still an issue? I am interested in working on it if it is still necessary.

rhelmot commented 5 years ago

Yes, it is still an issue. One small update is that since adding support for other solvers (for use with string solving), some internal APIs have been updated to pass around results as either "sat", "unsat", or "unknown". I don't know much about this or how it would affect attempting to implement this, but @Lukas-Dresel would. Lukas?

Lukas-Dresel commented 4 years ago

Oh damn, I didn't even see this, I need to manage my github notifications better, I've gotten serious notification fatigue

Lukas-Dresel commented 4 years ago

@rhelmot @saullocarvalho @peperunas

Currently you can already do solver.check_satisfiability() instead of solver.satisfiable(). This is not exported into angr's SimSolver yet I think, but there you can currently already do state.solver._solver.check_satisfiability()

Lukas-Dresel commented 4 years ago

This will return either 'SAT', 'UNSAT', or 'UNKNOWN'

Lukas-Dresel commented 4 years ago 

In [5]: s.solver._solver.check_satisfiability()                                 
Out[5]: 'SAT'
Lukas-Dresel commented 4 years ago

In terms of throwing an exception it seems to me like the only thing that would really need to be changed is in full_frontend.py to replace the instances of self.satisfiable() with self.check_satisfiability() and then throw the correct exception.

aa-software2112 commented 3 years ago

Can anyone here comment on the quality of the timeout's results?

For example, I have set a 5 second solver timeout, and I know very well that the code I am executing takes roughly 30 seconds to symbolically execute if the timeout is 5 minutes. At 5 seconds, the timeout is triggered and I call check_satisfiability(), which returns SAT. Is there a way to capture the timeout through an exception or some flag? I'm afraid that I'm introducing invalid constraint-solving results even though the timeout is being triggered and returning SAT

github-actions[bot] commented 2 years ago

This issue has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

zwimer commented 2 years ago

I believe this issue was fixed in the Z3 backend here: https://github.com/angr/claripy/blob/46b5af7432b63dea7b2e9b67c371256a2ec945e4/claripy/backends/backend_z3.py#L112 in https://github.com/angr/claripy/pull/285