Constrain Variable Ranges for Polyspace Analysis Using Manual Stubs and Manual main() Function

Constrain Variable Ranges for Polyspace Analysis Using Manual Stubs and Manual `main()` Function

This topic applies primarily to a Polyspace^® Code Prover™ analysis.

To get the most precise results from a Polyspace Code Prover analysis, the program analyzed must be as complete as possible. However, for multiple reasons, you might not be able to provide a complete program for analysis. Even for complete applications, some information such as constraints on external inputs resides outside the program. This topic shows how to constrain your analysis in a way that allows you to get precise results even for incomplete applications.

For simpler constraints, Code Prover provides a graphical interface for constraint specification. See, for instance, Specify External Constraints for Polyspace Analysis. If the options in the interface are insufficient for your context and you need to fine-tune the analysis even further, you can explicitly define the program boundary in full detail. This topic provides a conceptual framework to get you started on defining the program boundary.

Code Prover Assumptions About Variable Ranges at Program Boundary

A Polyspace Code Prover analysis has to make assumptions about variable ranges at the program boundary in order to provide sound results.

When Polyspace Code Prover analyzes a program, the analysis checks all operations likely to cause certain types of run-time errors¹ . The objective is to mathematically prove that the operations checked do not cause run-time errors or definitely cause run-time errors. If the analysis fails to prove the presence or absence of an error, it highlights the operation in orange for manual inspection. A subset of these orange checks indicate possible run-time errors but depending on how you have set up the analysis, most of the orange checks might indicate that the analysis has insufficient knowledge about your application. See also Orange Checks in Polyspace Code Prover.

To get the most number of proven results from a Polyspace Code Prover analysis, the program analyzed must be as complete as possible. However, for multiple reasons, you might not always be able to provide a complete application for analysis. For instance, you might be analyzing libraries for robustness or your complete application might be too large for a Code Prover analysis to scale. In these cases, the program module that you analyze might be incomplete in two ways:

There is no main() function that defines the entry point to your application.
Not all function implementations are available to the analysis. For instance, the program module that you are analyzing might be calling functions defined in another module that is not provided to the analysis.

Consider this simple program module:

#include <stdint.h>
int8_t getAnInput(void);

int32_t calculateSum(int32_t numberToProcess) {
    int32_t sum = 0;
    for(int32_t i = 0; i <= numberToProcess; i++) {
       sum += getAnInput();
    }
    return sum;
}

If you analyze this module with Code Prover, the following information is not available to the analysis:

Implementation of the getAnInput() function.
Call contexts of the calculateSum() function.

If the analyzed program is incomplete, Code Prover makes certain assumptions about the main() and undefined functions in order to continue with the analysis. The assumptions are broad enough to provide sound results but might be too broad for your context. For instance, if a function is not defined, Code Prover assumes a range of possible return values based on the function return type. In the preceding example, Code Prover assumes a range of [-128, 127] for the return value of getAnInput() based on the int8_t data type. However, this assumption leads to a wide range of values and the function might in reality be returning values in a narrower range.

Define Manual `main()` and Stubs to Constrain Ranges at Program Boundary

You can typically constrain a program boundary using Code Prover analysis options. For instance, if you want to constrain the input to calculateSum() or the return value of getInput(), you can use the option Constraint setup (-data-range-specifications). However, the option supports specific types of constraints. To specify more complicated constraints, you have to define your own stub and main().

Suppose that you know the following information:

calculateSum() is always called with a positive argument that cannot exceed 100.
getAnInput() returns a value that is either 0 or lies between 10 and 30 (inclusive of 10 and 30).

You can specify the following constrained ranges:

Range [1,100] on the input to calculateSum().
To specify this range, you can define a manual main() that calls calculateSum().
Range 0 ∪ [10, 30] on the return value of getAnInput().
To specify this range, you can define a manual stub for the getAnInput() function.

You can define the manual main() and stub in files separate from the original program module and provide those files to the Code Prover analysis.

Define Manual `main()`

To impose a constraint on inputs to the calculateSum() function, define a main() function that calls calculateSum() with constrained arguments. Your main() function can simply be the following:

#include <stdint.h>

int32_t calculateSum(int32_t numberToProcess);
extern int32_t arg_calculateSum;

void main() {
   int32_t sum;
   unchecked_assert(arg_calculateSum >= 1 && arg_calculateSum <= 100);
   sum = calculateSum(arg_calculateSum);
}

Following the unchecked_assert macro, the verification assumes that the assertion is true for the remaining code within the block. Therefore, in this example, the verification assumes a constrained range [1,100] for the input to calculateSum().

Define Manual Stub

To impose a constraint on the return value of getAnInput(), define a stub that constrains the range of an external variable before returning it from the function. The stub can look as follows:

#include <stdint.h>

extern int8_t arg_getAnInput;

int8_t getAnInput(void) {
   unchecked_assert(arg_getAnInput == 0 || (arg_getAnInput >= 10 && arg_getAnInput <= 30));
   return arg_getAnInput;
}

To check that the constraints are actually applied, verify the program module without and with the manual main() and stub. In the former case, you see two orange overflows that turn green when the constraints are applied. You can also verify the application of constraints using source code tooltips. For more information on the tooltips, see Variable Ranges in Source Code Tooltips After Code Prover Analysis.