Is it possible to check for overflow and underflow in floating point operations using Z3 verifier? If yes, how does Z3 indicate these exceptions?
1 Answers
SMTLib's floating point logic (described here: http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml, based on the paper: http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf) does not have any notions of floating-point exceptions, such as precision, underflow, overflow, div-by-zero, denormals, and invalid. A direct quote from Section VIII.B of that paper says:
Our formalization does not cover the IEEE-754 notion of exceptions or flags (the default handling of executions). This is simply because there is no notion of execution order in a logical formula, and so there is no meaningful way of expressing those notions directly in theory.
So, there is no support for the floating-point-flags in the logic, and z3 does not support them either.
Note: I personally do not agree with the reasoning given in that paper. For instance, Z3 can check overflow/underflow for bit-vector instructions, see https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf. A similar approach can be adapted for floating-point as well, with new SMTLib commands to detect PUOZDI flags. However, this isn't formalized and so far as I know no solver has implemented this idea for FPA.
Related