Clarify the semantics of EndOfInstruction()

[danmatichuk]

Currently all exceptional control flow is the result of either an assertion failure or encountering unpredictable/undefined behavior. This allows us to model assertion failure with a simple tripped flag, indicating that any state updates should be ignored (as the instruction is necessarily in an invalid/undefined state).

The EndOfInstruction() function, however, indicates that there shouldn't be any further instruction processing but that any current modifications to the system registers should be preserved.

Trying to model this carefully during symbolic execution results in an explosion of complexity, as each evaluated expression needs to check whether or not EndOfInstruction() has been tripped and stop evaluation if so.

Careful analysis needs to be done to clarify both:

• To what extent is handling this particular control flow necessary for the level of detail necessary for the semantic model we are trying to represent.

• If necessary, can this be handled elsewhere in a semantic interpretation of this function? For example, can EndOfInstruction simply checkpoint the state when it is evaluated, and have an outer evaluation framework look for the presence of such a check-pointed state.