Dat3M
Dat3M copied to clipboard
Static/Meta assertions
Context: Our program processing frequently produces exceptions due to, e.g., unsupported intrinsics, unsupported control-flow (unnatural loops), or failure of analysis.
Problem: Sometimes, such errors occur only in dead code, i.e., they are not true errors. It would be helpful to not throw exceptions in such cases. However, it is generally not possible to determine dead code at the time of a processing pass, for example, if the pass runs before constant propagation.
Solution idea: Instead of eagerly throwing an error, we can insert a "static/meta assertion event" that contains the error message of interest. We then keep on running the processing and only after processing we check if there are any static assertions that are statically reachable and statically falsified (a static_assert(false)
would be good enough for most purposes).
We can probably reuse the Assert
event with just another flag telling if it is static or dynamic.
An alternative to these static assertions is to always produce standard assertions like in #557 and only give an error if the point of failure is dynamically reachable. Disadvantages of this are (1) that checking for assertions can get more expensive if we also need to check all our internally placed assertions and (2) when checking for liveness/races only, we do not throw errors at all and might silently produce wrong results.
We could also separate user-assertions from internal assertions and always check for internal assertions no matter the user-provided property to check for.