Skip to content
Program Round-off Error Certifier via Static Analysis
Haskell Shell GAP Scala C Yacc CMake
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
LICENCES
PRECiSA Release PRECiSA 2.1.0 Aug 21, 2019
PVS Release PRECiSA 2.1.0 Aug 21, 2019
benchmarks Release PRECiSA 2.1.0 Aug 21, 2019
.gitignore Release PRECiSA 2.1.0 Aug 21, 2019
README.md Release PRECiSA 2.1.0 Aug 21, 2019

README.md

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:

To verify certificates generated by PRECiSA you need:

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

Build

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

  2. Set the environment variable KODIAK_LIB with the directory in which the libKodiakDynamic.so (or libKodiakDynamic.dylib) is present. In a bourne shell it can be set like this:

    $ export KODIAK_LIB=<directory-containing-libKodiakDynamic.so>
    
  3. Go to the root repository directory (it depends on where you have downloaded it and how you have named it).

    $ cd <your-root-repository-directory>
    
  4. Create a build directory:

    $ mkdir build
    
  5. Invoke CMake on the root of the repository from the build directory

    $ cd build
    $ cmake ../PRECiSA
    
  6. Invoke CMake's build command on the build directory

    $ cmake --build .
    

At this point, the executable should be in the current build directory. You can add the current directory to your PATH variable or install (copy) it to your place of choice.

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 >= RtoD(0) AND Y < RtoD(4))
     	THEN IF (Y > RtoD(0))
     		 THEN Dadd(X,Y)
     		 ELSE Dmul(X,Y)
     		 ENDIF
         ELSE Dsub(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.
  • --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-2.1.0 (August 2019)

Contact information

If you have any question or problem, please contact:

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 2019 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.

You can’t perform that action at this time.