One year ago, we presented on this blog what was provable about fixed-point and floating-point computations (the two forms of real types in SPARK). I used as examples codes computing approximations of Pi using the Leibniz formula and a refinement of it through the Shanks transformation. GNATprove managed to prove the exact result of the computation in only one case, the simple algorithm implemented with fixed-point values.

Since then, we have integrated static analysis in SPARK. Static analyzer CodePeer can be called as part of SPARK analysis using the switch --codepeer=on. CodePeer analysis is particularly interesting when analyzing code using floating-point computations, as CodePeer is both fast and precise for proving bounds of floating-point operations. For more details about this feature, see the SPARK User's Guide.

During the last year, we have also modified completely the way floating-point numbers are seen by SMT provers. In particular, we are now using the native support for floating-point numbers in prover Z3. So Z3 can reason precisely about floating-point computations, instead of relying on a partial axiomatization like CVC4 and Alt-Ergo still do. Improved support for floating-point computations is also expected to be available in CVC4 and Alt-Ergo in 2017.

Both of these features lead to dramatic changes in provability for code doing fixed-point and floating-point computations. On the example codes that I presented last year, GNATprove manages to prove all the results of the four computations (with fixed-points or floating-points, with Leibniz or Shanks) when CodePeer is used (without Z3). GNATprove manages to prove three of the four computations when Z3 is used (without CodePeer). The one that is not proved is the computation of the Shanks algorithm implemented using fixed-point values. In fact it is not provable with Z3 because this algorithm involves a division between fixed-point values that needs to be rounded, and the Ada standard specifies that either the fixed-point value above or the fixed-point value below is a suitable rounding. In SPARK, we strive to stay independent of such compiler-specific implementation choices, so we don't specify which value is chosen between the two different results. The reason why CodePeer manages to prove it is because CodePeer follows the choices made by GNAT in this case, as documented in the SPARK User's Guide. In addition, using either CodePeer or Z3 is sufficient to prove all the other run-time checks in the example codes (range checks, overflow checks and divisions by zero checks).

These features were included in the preview release SPARK 17.0, and initial feedback from customers show that in some cases they do improve the results of proof on code doing fixed-point and floating-point computations. In some other cases, we have witnessed regressions in proof due to the fact CVC4 and Alt-Ergo now prove fewer checks. We are actively working to revert these regressions, and we think that the new combination of analyses will lead to large improvements for proof on such codebases in the future.