PRECiSA

PRECiSA (Program Round-off Error Certifier via Static Analysis) is a fully automatic static analyzer for floating-point programs.

The main functionality of PRECiSA is the round-off error estimation. Given a floating-point program, PRECiSA computes a sound overapproximation of the round-off error that may occur together with PVS certificates ensuring its correctness. Here you can try the PRECiSA web-interface and find more information on the tool.

In addition, PRECiSA implements a program transformation from a PVS real-valued program to floating-point C code. This transformation corrects unstable tests by over-approximating the conditional guards in the if-then-else statements. The resulting transformed program emits a warning when an unstable test is detected (i.e., the floating-point computational flow diverges with respect to the ideal real number one). The generated C code is annotated with ACSL contracts that relate the floating-point implementation with the real-valued program specification.

Installation

PRECiSA runs on Linux and Mac OS X operating systems.

Prerequisites

To build and install PRECiSA you need:

• The Glorious Haskell Compiler and its package manager Cabal, both available as part of the Haskell platform,
• CMake,
• the NASA Kodiak library to compute numerical error bounds.

To verify certificates generated by PRECiSA you need:

• PVS version 6.0,
• the NASA PVS library.

If you want to use the SMT optimization you need FPRock.

Build

1. Install Kodiak producing a dynamic library libKodiakDynamic.so (for Linux) or libKodiakDynamic.dylib (for MacOS).

2. Make accessible the Kodiak dynamic library to your linker. Normally, this is done by updating the LD_LIBRARY_PATH environment variable with the directory in which the libKodiakDynamic.so (or libKodiakDynamic.dylib) file is present. Let <kodiak-directory> represent this directory. In a bourne shell that environment variable can be set like this:

   $ export LD_LIBRARY_PATH="<directory-containing-libKodiakDynamic.so>:$LD_LIBRARY_PATH"
   

   You can add the previous line to your shell initialization script (for example, ~/.profile or ~/.bashrc) to make the LD_LIBRARY_PATH change permanent.

3. Go to the PRECiSA sub-directory of the repository.

   $ cd <repository-root>/PRECiSA
   

4. Use the following commands to create a cabal sandbox in this folder and install the executable in <repository-root>/.cabal-sandbox/bin/precisa

   $ cabal v1-sandbox init    # Creates a new sandbox.
                              # Old cabal versions may need the command `cabal sandbox init` instead
   
   $ cabal v1-install --enable-optimization --extra-lib-dirs=<kodiak-directory>
   

5. Now, the precisa executable can be run with:

   $ .cabal-sandbox/bin/precisa
   

Floating-Point Round-Off Error Estimation

The input to the PRECiSA round-off error estimator are the following files:

• A program example.pvs composed of floating-point valued functions. In its current version, PRECiSA accepts a subset of the language of the Prototype Verification System (PVS), including LET-IN expressions, IF-THEN-ELSE constructions, function calls, and floating-point values and operations such as: addition, multiplication, division, subtraction, floor, square root, trigonometric functions, logarithm, and exponential. For example:

   example: THEORY
   BEGIN
   IMPORTING float@aerr754dp
  
    example (X,Y: unb_double) : unb_double =
        IF (X >= 0 AND Y < 4)
        THEN IF (Y > 0)
             THEN X+Y
             ELSE X*Y
             ENDIF
        ELSE X-Y ENDIF
  
   END example
  

• A file example.input containing initial ranges for the input variables of the program. For example:

   example(X,Y): X in [-10,10], Y in [0, 40]
  

• Optionally, a file example.path containing a set of decision paths/sub-programs of interests. The user can specify these paths by listing the paths/sub-programs of interests as a list of True and False. For instance, in the example above, the path [True, True] corresponds to the sub-program Dadd(X,Y), the path [False] to the subprogram Dsub(X,Y), and the path [True] to the subprogram IF (Y > RtoD(0)) THEN Dadd(X,Y) ELSE Dmul(X,Y) ENDIF. The analysis is done for all the execution paths in the program, or better for all combination of real/FP execution path in the program). For the selected sub-programs, a dedicated error expression representing the round-off error estimation is computed. For the others, the tool will generate an overall error which is the maximum of all the round-off error estimations corresponding to these sub-programs. If the user does not select any sub-program of interest (None), the tool will produce the overall round-off error for the stable cases (when real and floating-point execution flows coincide) and the one for the unstable cases (when real and floating-point execution flows diverge). If the user is interested in a precise analysis of the entire program (All), the analysis will generate a semantic element for each combination of real/FP execution path in the program. Examples of possible input for the decision pahts are the following:

   example(X,Y): None
  

  or

   example(X,Y): All
  

  or

   example(X,Y): [True, True]
  

More examples can be found in the PRECiSA benchmarks folder.

The analysis performed by PRECiSA results in one upper-bound of the floating-point round-off error for each decision path of interest, an overall upper-bound for the rest of decision paths, and an overall upper-bound for the unstable test cases (when real and floating-point flows diverge). Additionally, PRECiSA generates two PVS theories:

• a theory containing a collection of lemmas stating symbolic accumulated round-off error estimations for the input program, and
• a theory containing a collection of lemmas stating numerical accumulated round-off error estimations. The numerical estimations are computed using Kodiak.

All the generated lemmas are equipped with PVS proof scripts that automatically discharge them.

How to run the PRECiSA round-off error estimator

We assume that precisa (the executable of PRECiSA) is in the current directory.

To launch the round-off error analysis of PRECiSA with the default parameters run:

$ ./precisa analyze "example.pvs" "example.input"

• the first parameter is the path to the PVS program to be analyzed;
• the second one is the path to the file that indicates the initial values for the input variables of the input program;

Command Line Options

• --paths example.path specifies the path to the file that indicates the decision paths of interest for every function in the program. The default is the empty set, i.e., there is no path of interest and the output of PRECiSA consists of two errors: one for the stable cases (when real and floating-point flows agree) and one for the unstable cases (when real and floating-point flows diverge).

• Options for the branch-and-bound search used to compute the numerical estimation:
  • --max-depth 7 (or -d 7) is the maximum depth of the branch-and-bound exploration with a default value of 7.
  • --precision 14 (or -p 14) is the negative exponent of 10 representing the numerical precision used. It has a default value of 14 which stands for a precision of $10$^{-14</math></span>.}

• --max-lemmas 50 (or -l 50) sets the maximum number of lemmas allowed to be generated by PRECiSA. This avoids having certificates too big to be treated. If your program generates a huge number of lemmas, this means probably that you have several nested if-then-else. In this case, try to run PRECiSA with the default settings, or try to set some decision paths of interests. Alternatively, you can activate the Stable Test Assumption.

• --assume stability (or -s) if this option is activated, real and floating-point execution flows are assumed to coincide (Stable Test Assumption). Therefore, the analysis can be unsound since the cases where the execution paths diverge (unstable cases) are not considered.

• --no-collapsed-unstables (or -u) if this option is activated, the unstable tests are not collapsed in a unique case.

• --smt-optimization (or -u) if this option is activated, PRECiSA checks the satisfiability of each path condition by calling an external SMT solver through the FPRoCK tool. In this way, it is possible to detect and remove the spurious execution paths, improving the accuracy of the round-off error estimation.

An example of how to execute PRECiSA by manually setting some options is the following:

$ ./precisa analyze "example.pvs" "example.input" --paths "example.path" --max-depth 7 --precision 14 --max-lemmas 40

How to verify the PVS certificates

PVS version 6.0 and the development version of the NASA PVS Library are required to proof-check the symbolic and the numerical certificates generated by PRECiSA in PVS. Furthermore, the directory PVS has to be added to the Unix environment variable PVS_LIBRARY_PATH. Depending upon your shell, one of the following lines has to be added to your startup script. In C shell (csh or tcsh), put this line in ~/.cshrc, where <precisapvsdir> is the absolute path to the directory PVS:

setenv PVS_LIBRARY_PATH "<precisapvsdir>:$PVS_LIBRARY_PATH"

In Borne shell (bash or sh), put this line in either ~/.bashrc or ~/.profile:

export PVS_LIBRARY_PATH="<precisapvsdir>:$PVS_LIBRARY_PATH"

You can use the proveit shell script to automatically check the proofs in the symbolic and numerical certificates generated by PRECiSA. For example, if you analyzed the program example.pvs, in the same folder you will find two files: cert_example.pvs and num_cert_example.pvs.

To check the correctness of the PVS theories in cert_example.pvs and num_cert_example.pvs you can run:

$ proveit -sc cert_example.pvs
$ proveit -sc num_cert_example.pvs

PVS basic troubleshooting

If the PVS verification is not behaving as expected, try cleaning the PVS binaries in the NASA PVS library. Simply run cleanbin-all in the NASA PVS library folder of your installation and try again.

Automatic generation of stable C code from PVS

The input to the PRECiSA C code generator are the following files:

• A program example.pvs composed of real-valued functions. In its current version, PRECiSA accepts a subset of the language of the Prototype Verification System (PVS), including LET expressions, IF-THEN-ELSE constructions, function calls, and floating point values and operations such as: addition, multiplication, division, subtraction, floor, square root, trigonometric functions, logarithm, and exponential. For example:

   example: THEORY
   BEGIN
  
    example (X,Y: real) : real =
        IF (X >= 0 AND Y < 4)
        THEN IF (Y > 0)
             THEN X+Y
             ELSE X*Y
             ENDIF
        ELSE X-Y ENDIF
  
   END example
  

• A file example.input containing initial ranges for the input variables of the program. For example:

   example(X,Y): X in [-10,10], Y in [0, 40]
  

The output is a C floating-point program example.c instrumented to detect unstable tests. This program is annotated with ACSL contracts stating the relation between the floating-point program and the real number specification. This annotated program can be analyzed with the Frama-C static analyzer.

Besides, PVS certificates are provided for ensuring that all the unstable tests are detected. These certificates can be automatically checked as explained here.

How to run the PRECiSA stable C code generator

We assume that precisa (the executable of PRECiSA) is in the current directory.

To launch the round-off error analysis of PRECiSA with the default parameters run:

$ ./precisa gen-code "example.pvs" "example.input"

• the first parameter is the path to the PVS program to be analyzed;
• the second one is the path to the file that indicates the initial values for the input variables of the input program;

Command Line Options

• --format FORMAT where FORMAT can be double or single, indicating the target format of the floating-point C code. The default value is double precision.

Additional information

Version

PRECiSA v-3.0.0 (July 2020)

Contact information

If you have any question or problem, please contact:

• Laura Titolo (for PRECiSA)
• Mariano Moscato (for PVS)
• Marco A. Feliu (for Kodiak)
• César A. Muñoz (PRECiSA @ NASA)

Related Publications

• Mariano Moscato, Laura Titolo, Marco Antonio Feliu Gabaldon and César Muñoz: A Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm. FM 2019

• Rocco Salvia, Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César A. Muñoz, Zvonimir Rakamaric: A Mixed Real and Floating-Point Solver. NFM 2019: 363-370

• Laura Titolo, César A. Muñoz, Marco A. Feliú, Mariano M. Moscato: Eliminating Unstable Tests in Floating-Point Programs. LOPSTR 2018: 169-183

• Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César A. Muñoz: An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs. VMCAI 2018: 516-537

• Mariano M. Moscato, Laura Titolo, Aaron Dutle, César A. Muñoz: Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis. SAFECOMP 2017: 213-229

License and Copyright Notice

The code in this repository is released under NASA’s Open Source Agreement. See the directory LICENSES.

Notices:

Copyright 2020 United States Government as represented by the Administrator of the National Aeronautics
and Space Administration. All Rights Reserved.

Disclaimers
No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY KIND,
EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT LIMITED TO, ANY WARRANTY
THAT THE SUBJECT SOFTWARE WILL CONFORM TO SPECIFICATIONS, ANY IMPLIED WARRANTIES
OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT,
ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT,
IN ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR RECIPIENT OF
ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR ANY OTHER APPLICATIONS
RESULTING FROM USE OF THE SUBJECT SOFTWARE.  FURTHER, GOVERNMENT AGENCY DISCLAIMS
ALL WARRANTIES AND LIABILITIES REGARDING THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL
SOFTWARE, AND DISTRIBUTES IT "AS IS."

Waiver and Indemnity:  RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST THE UNITED STATES
GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY PRIOR RECIPIENT. 
IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN ANY LIABILITIES, DEMANDS, DAMAGES,
EXPENSES OR LOSSES ARISING FROM SUCH USE, INCLUDING ANY DAMAGES FROM PRODUCTS BASED
ON, OR RESULTING FROM, RECIPIENT'S USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY
AND HOLD HARMLESS THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS,
AS WELL AS ANY PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW.  RECIPIENT'S SOLE REMEDY
FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS AGREEMENT.