Allow callback inspection of exceptions which trigger TerminateState

[ranweiler]

Hi! I'm working with some Manticore-powered code that subscribes to the will_terminate_state event. The subscribing callback receives a TerminateState exception as one of its arguments. I'd like to be able to inspect the underlying exception (if any) which caused TerminateState to be raised. The motivation here is that I want to decide whether or not to flag the terminated state as a "crash" for the program being analyzed, or not (e.g. it was some other kind of out-of-band error).

Right now, I can do this by looking at the message property (a str) of the TerminateState exception, and if the message contains certain substrings, infer that the state exploration was terminated due to (for example) an InvalidMemoryAccess exception. In other words, I am indirectly checking if the exception arose due to other particular exceptions within Manticore. What I would is avoid doing this via string comparisons, which can be brittle, non-canonical, &c.

Some options to accomplish this larger goal:

1. Add a property like cause to TerminateState instances, to which we could assign the underlying exception (if any) which triggered the TerminateState.
2. Add a subclass of TerminateState called (for example) CrashState which is used in place of TerminateState when the termination reason is that the program being symbolically-executed "would have crashed", for some definition of this.

In each case, the Manticore user can now directly use class hierarchies/isinstance() to determine if the TerminateState was due to a "crash". In (1), the user must decide for themselves exactly which Manticore exceptions indicate a "program crash" (vs. a Manticore execution error). The improvement is the removal of lossy indirection via the message property. In (2), Manticore must commit to some particular exceptions as having the semantics of a "program crash". These ideas are not mutually exclusive, either, so Manticore could use CrashState where it is incontestable, and library users could use cause to narrow or expand the meaning of "crash" for their needs.

To me, (1) alone is the best choice. It would be easy to implement, might be more broadly useful, and doesn't require any big API commitments from Manticore. It also seems theoretically nicer: for a program whose native behavior would raise a SIGSEGV, some signal handler might actually avoid a crash. (2) would be extremely convenient for me as a user, but seems to place an undue (intractable?) burden on Manticore.

I'd be happy to cook up a PR for this, but wanted input from others before doing so. Thanks!

[offlinemark]

Hi @ranweiler, thank you very much for the extremely clear explanation of the issue and your thoughts on potential solutions, I appreciate it so much :)

I agree with you - I think (1) is best solution for now. I like how (2) does not involve patching more attributes onto the Exception object, but this makes the solution less powerful as the user cannot introspect into the crash as deeply. Would love to see a PR for (1)!

@yan any thoughts on this?

[yan]

Agree that (1) is best for right now, although I imagine once we have a better idea into the categories of exceptions and how they're actually used, we'll end up with a hybrid. (An extended, but still relatively shallow hierarchy of exceptions, with a cause-like field)

[ranweiler]

Great, thanks @Mossberg and @yan! I'll open a PR for (1) later tonight.

[ehennenfent]

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