Reminder on overflow in Polyspace:
Since 12a, there are two overflow modes in Polyspace: the result of an overflowing computation can either be truncated, or a wrap-around can take place.
Example:
On a 16-bit target, with a and b signed integers, if we have
a = 20 000 .. 30 000
b = 10 000
then a + b will lead to an orange OVFL (the maximum value of a 'signed int' being 32767).
But when the overflow computation mode is truncate-on-error, only the subset that will not cause the overflow is kept. Here it means that the verification will continue with a range of [30000..32767] for res.
When the overflow computation mode is wrap-around, a wrap-around takes place for values too high or too low, and no values are removed. The value of res is [-32768 .. -25536] or [30000 .. 32767].
Another point with overflows is that it is possible to ask Polyspace to check for overflows on unsigned integer variables.
Reminder on CTO:
TargetLink is using a mechanism called ‘compute-through-overflow’ (CTO) in their generated code.
According to dSpace, this ‘compute-through-overflow’ is an optimisation that implements efficient additions and subtractions and especially avoids 64-bit operations.
The idea of CTO is to force variables to be unsigned during the computation, then to cast back the result to signed.
For example:
results = a + b
becomes
result = (signed) ( (unsigned) a + (unsigned) b )
But for Polyspace, this CTO mechanism can lead to red or orange overflows when the unsigned value is casted to signed.
For this reason, it is possible to disable the CTO mechanism. dSpace is indeed adding a comment for each cast to unsigned.
result = (signed) ( /* CTO */(unsigned) a + /* CTO */(unsigned) b )
Polyspace will recognizes this CTO comment to comment this cast:
result = (signed) ( /* CTO (unsigned)*/ a + /* CTO (unsigned)*/ b )
This is done by default when the verification is launched from Simulink. It can be enabled if the verification is launched outside Simulink by setting the environment variable POLYSPACE_TARGETLINK_STUBS to the value nopststubs.
It is then possible to:
1) activate the CTO (casts to unsigned) or not
2) detect the overflows for signed, signed and unsigned or even to disable the overflows
3) truncate the results or apply a wrap-around
Then, what is the best configuration of overflow options, knowing that:
1) Without the CTO (original computation without casts), "truncate on error" will change the default behavior defined by the C standard and reduce the range when an overflow occurs.
2) With the CTO, if overflow detection of unsigned is activated, overflows can occur if a variable is negative.
To answer this question, let's consider a line of code that contains two possible overflows: one on an sum and one for an unsigned variable casted to unsigned because of CTO:
res = a + b + c;
with the following ranges
a = 20 000 .. 30 000
b = 0 .. 10 000
c = -20 000 .. -15 000
The CTO will generate the following code:
res = (signed short) ( /* CTO */ (unsigned short) a + /* CTO */ (unsigned short) b + /* CTO */ (unsigned short) c );
If the CTO is disabled, the line will be:
res = (signed short) ( /* CTO (unsigned short) */ a + /* CTO (unsigned short) */ b + /* CTO unsigned short) */ c );
equivalent to
res = (signed short) ( a + b + c );
Here is the result for the different possibilities:
This picture shows the ranges and colors computed by Polyspace for the two CTO modes, and with, for each mode, the different options of overflow parameters: overflow detected on signed / signed and unsigned / none, and the overflow computation mode set to truncate / wrap-around.
Summary:
We can see that:
- the wrap-around mode should be set. It will not reduce the range and produce final correct ranges.
- activating the detection of overflow for unsigned will lead to overflows when the CTO is activated. So it is better to disable it (default behavior).
- even when the final range is correct, there will still be an orange checks on arithmetical operations.
Please note that since TargetLink 3.4, you can configure the tool to:
- Never implement CTO patterns
- Always apply CTO code patterns whenever an overflow can occur
- Optimized use CTO patterns to improve the code efficiency
