Check if user state constraints make state unsatisfiable

[offlinemark]

This issue was initially reported by @murmus. Thank you!

The state.constrain() API enables a user to add additional, arbitrary constraints onto a State. If these constraints actually make the state infeasible, this will later manifest as a SolverException when attempts to concretize symbolic data are made in this state (i.e. state.solve_one). As a side note, that exception will have an error message that is likely cryptic to the typical user (Model is not available).

If a state has been made infeasible by a user constraint, it likely means that original state was not the state their constraints were intended to be applied to.

proposed solution:

• on each constraint add, check whether added constraint make the state infeasible, if they do, abandon the state
• log this fact at the same log level as state forking, and other state related messages

alternative ideas:

• try to rollback the state and remove the constraints the user added and keep going?

[ehennenfent]

https://github.com/trailofbits/manticore/wiki/Ideas