Review and Fix Invalid Shift Operations Checks

This topic describes how to systematically review the results of an Invalid shift operations check in Polyspace^® Code Prover™.

Follow one or more of these steps until you determine a fix for the Invalid shift operations check. There are multiple ways to fix the check. For a description of the check and code examples, see Invalid shift operations.

Sometimes, especially for an orange check, you can determine that the check does not represent a real error but a Polyspace assumption that is not true for your code. If you can use an analysis option to relax the assumption, rerun the verification using that option. Otherwise, you can add a comment and justification in your result or code.

For the general workflow that applies to all checks, see Interpret Code Prover Results in Polyspace Desktop User Interface or Interpret Code Prover Results in Polyspace Access Web Interface (Polyspace Access).

Step 1: Interpret Check Information

Select the red or orange Invalid shift operations check. Obtain the following information from the Result Details pane:

The reason for the check being red or orange. Possible reasons:
- The shift amount can be outside allowed bounds.
  The software also states the allowed range for the shift amount.
- Left operand of left shift can be negative.
In the example below, a red error occurs because the shift amount is outside allowed bounds. The allowed range for the shift amount is 0 to 31.

Possible fix: To avoid the red or orange check, perform the shift operation only if the shift amount is within bounds.
```
if(shiftAmount < (sizeof(int) * 8))
  /* Perform the shift */
else
  /* Error handling */
```
Probable root cause for the check, if the software provides this information.
In the preceding example, the software identifies a stubbed function, getVal as probable cause.
Possible fix: To avoid the orange check, constrain the return value of getVal. For instance, specify that getVal returns values in a certain range, for example, 0..10. For more information, see Code Prover Assumptions About Stubbed Functions.

Step 2: Determine Root Cause of Check

If the shift amount is outside bounds, trace the data flow for the shift variable. Identify a suitable point where you can constrain the shift variable.
In the following example, trace the data flow for shiftAmount.
```
void func(int val) {
	int shiftAmount = getShiftAmount();
	int res = val >> shiftAmount;
}
```
You might find that getShiftAmount returns full-range of values.
Possible fix:
- Perform the shift operation only if shiftAmount is between 0 and (sizeof(int))*8 - 1.
- Constrain the return value of getShiftAmount, in the body of getShiftAmount or through the Polyspace Constraint Specification interface, if you do not have the definition of getShiftAmount. For more information, see Code Prover Assumptions About Stubbed Functions.
If the left operand of a left shift operation can be negative, trace the data flow for the left operand variable. Identify a suitable point where you can constrain the left operand variable.
In the following example, trace the data flow for shiftAmount.
```
void func(int shiftAmount) {
	int val = getVal();
	int res = val << shiftAmount;
}
```
You might find that getVal returns full-range of values.
Possible fix:
- Perform the shift operation only if val is positive.
- Constrain the return value of getVal, in the body of getVal or through the Polyspace Constraint Specification interface, if you do not have the definition of getVal. For more information, see Code Prover Assumptions About Stubbed Functions.
- If you want Polyspace to allow the operation, use the analysis option Allow negative operand for left shifts. See Allow negative operand for left shifts (-allow-negative-operand-in-shift).

To trace the data flow, select the check and note the information on the Result Details pane.

If the Result Details pane shows the sequence of instructions that lead to the check, select each instruction.
If the Result Details pane shows the line number of probable cause for the check, right-click the Source pane. Select Go To Line.

Otherwise:

Find the previous write operation on the variable you want to trace.
At the previous write operation, identify a new variable to trace back.
Place your cursor on the variables involved in the write operation to see their values. The values help you decide which variable to trace.
Find the previous write operation on the new variable. Continue tracing back in this way until you identify a point to specify your constraint.

Depending on the variable, use the following navigation shortcuts to find previous instances. You can perform the following steps in the Polyspace user interface only.

Variable How to Find Previous Instances of Variable

Variable	How to Find Previous Instances of Variable
Local Variable	Use one of the following methods: Search for the variable. Right-click the variable. Select Search For All References. All instances of the variable appear on the Search pane with the current instance highlighted. On the Search pane, select the previous instances. Browse the source code. Double-click the variable on the Source pane. All instances of the variable are highlighted. Scroll up to find the previous instances.
Global Variable Right-click the variable. If the option Show In Variable Access View appears, the variable is a global variable.	Select the option Show In Variable Access View. On the Variable Access pane, the current instance of the variable is shown. On this pane, select the previous instances of the variable. Write operations on the variable are indicated with and read operations with .
Function return value ret=func();	Find the function definition. Right-click `func` on the Source pane. Select Go To Definition, if the option exists. If the definition is not available to Polyspace, selecting the option takes you to the function declaration. In the definition of `func`, identify each `return` statement. The variable that the function returns is your new variable to trace back.

Local Variable

Use one of the following methods:

Search for the variable.
1. Right-click the variable. Select Search For All References.
  All instances of the variable appear on the Search pane with the current instance highlighted.
2. On the Search pane, select the previous instances.
Browse the source code.
1. Double-click the variable on the Source pane.
  All instances of the variable are highlighted.
2. Scroll up to find the previous instances.

Global Variable

Right-click the variable. If the option Show In Variable Access View appears, the variable is a global variable.

Select the option Show In Variable Access View.
On the Variable Access pane, the current instance of the variable is shown.
On this pane, select the previous instances of the variable.
Write operations on the variable are indicated with and read operations with .

Function return value

ret=func();

Find the function definition.
Right-click func on the Source pane. Select Go To Definition, if the option exists. If the definition is not available to Polyspace, selecting the option takes you to the function declaration.
In the definition of func, identify each return statement. The variable that the function returns is your new variable to trace back.

You can also determine if variables in any operation are related from some previous operation. See Find Relations Between Variables in Code.

Step 3: Look for Common Causes of Check

Look for common causes of the Invalid Shift Operations check.

See if you have specified the right target processor type. The target processor type determines the number of bits allowed for a certain variable type.
To determine the number of bits allowed:
1. Navigate to the variable definition. Note the variable type.
  Right-click the variable and select Go To Definition, if the option exists.
2. See the number of bits allowed for the type.
  In the configuration used for your results, select the Target & Compiler node. Click the Edit button next to the Target processor type list.
For left shifts with a negative operand, see if you intended to perform a right shift instead.

Step 4: Trace Check to Polyspace Assumption

See if you can trace the orange check to a Polyspace assumption that occurs earlier in the code. If the assumption does not hold true in your case, add a comment or justification in your result or code. See Address Results in Polyspace User Interface Through Bug Fixes or Justifications or Address Results in Polyspace Access Through Bug Fixes or Justifications (Polyspace Access).

For instance, you obtain a variable from an undefined function and perform a left shift on it. Then:

Polyspace assumes that the function can return a negative value.
The left shift operation can occur on a negative value and therefore there is an orange check on the operation.
If you know that the function returns a positive value, add a comment and justification describing why you did not change your code.

For more information, see Code Prover Analysis Assumptions.