Skip to content

Commit b221f4e

Browse files
authored
Merge pull request #542 from rvermeulen/rvermeulen/fix-396
Resolve FP reported in 396
2 parents 34d836f + 35df852 commit b221f4e

File tree

14 files changed

+305
-250
lines changed

14 files changed

+305
-250
lines changed

c/cert/src/rules/INT34-C/ExprShiftedbyNegativeOrGreaterPrecisionOperand.ql

+4-87
Original file line numberDiff line numberDiff line change
@@ -15,91 +15,8 @@ import codingstandards.c.cert
1515
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
1616
import semmle.code.cpp.valuenumbering.GlobalValueNumbering
1717
import semmle.code.cpp.controlflow.Guards
18+
import codingstandards.cpp.UndefinedBehavior
1819

19-
/*
20-
* Precision predicate based on a sample implementation from
21-
* https://wiki.sei.cmu.edu/confluence/display/c/INT35-C.+Use+correct+integer+precisions
22-
*/
23-
24-
/**
25-
* A function whose name is suggestive that it counts the number of bits set.
26-
*/
27-
class PopCount extends Function {
28-
PopCount() { this.getName().toLowerCase().matches("%popc%nt%") }
29-
}
30-
31-
/**
32-
* A macro which is suggestive that it is used to determine the precision of an integer.
33-
*/
34-
class PrecisionMacro extends Macro {
35-
PrecisionMacro() { this.getName().toLowerCase().matches("precision") }
36-
}
37-
38-
class LiteralZero extends Literal {
39-
LiteralZero() { this.getValue() = "0" }
40-
}
41-
42-
class BitShiftExpr extends BinaryBitwiseOperation {
43-
BitShiftExpr() {
44-
this instanceof LShiftExpr or
45-
this instanceof RShiftExpr
46-
}
47-
}
48-
49-
int getPrecision(IntegralType type) {
50-
type.isExplicitlyUnsigned() and result = type.getSize() * 8
51-
or
52-
type.isExplicitlySigned() and result = type.getSize() * 8 - 1
53-
}
54-
55-
predicate isForbiddenShiftExpr(BitShiftExpr shift, string message) {
56-
(
57-
(
58-
getPrecision(shift.getLeftOperand().getExplicitlyConverted().getUnderlyingType()) <=
59-
upperBound(shift.getRightOperand()) and
60-
message =
61-
"The operand " + shift.getLeftOperand() + " is shifted by an expression " +
62-
shift.getRightOperand() + " whose upper bound (" + upperBound(shift.getRightOperand()) +
63-
") is greater than or equal to the precision."
64-
or
65-
lowerBound(shift.getRightOperand()) < 0 and
66-
message =
67-
"The operand " + shift.getLeftOperand() + " is shifted by an expression " +
68-
shift.getRightOperand() + " which may be negative."
69-
) and
70-
/*
71-
* Shift statement is not at a basic block where
72-
* `shift_rhs < PRECISION(...)` is ensured
73-
*/
74-
75-
not exists(GuardCondition gc, BasicBlock block, Expr precisionCall, Expr lTLhs |
76-
block = shift.getBasicBlock() and
77-
(
78-
precisionCall.(FunctionCall).getTarget() instanceof PopCount
79-
or
80-
precisionCall = any(PrecisionMacro pm).getAnInvocation().getExpr()
81-
)
82-
|
83-
globalValueNumber(lTLhs) = globalValueNumber(shift.getRightOperand()) and
84-
gc.ensuresLt(lTLhs, precisionCall, 0, block, true)
85-
) and
86-
/*
87-
* Shift statement is not at a basic block where
88-
* `shift_rhs < 0` is ensured
89-
*/
90-
91-
not exists(GuardCondition gc, BasicBlock block, Expr literalZero, Expr lTLhs |
92-
block = shift.getBasicBlock() and
93-
literalZero instanceof LiteralZero
94-
|
95-
globalValueNumber(lTLhs) = globalValueNumber(shift.getRightOperand()) and
96-
gc.ensuresLt(lTLhs, literalZero, 0, block, true)
97-
)
98-
)
99-
}
100-
101-
from BinaryBitwiseOperation badShift, string message
102-
where
103-
not isExcluded(badShift, Types1Package::exprShiftedbyNegativeOrGreaterPrecisionOperandQuery()) and
104-
isForbiddenShiftExpr(badShift, message)
105-
select badShift, message
20+
from ShiftByNegativeOrGreaterPrecisionOperand badShift
21+
where not isExcluded(badShift, Types1Package::exprShiftedbyNegativeOrGreaterPrecisionOperandQuery())
22+
select badShift, badShift.getReason()

c/cert/test/rules/INT34-C/ExprShiftedbyNegativeOrGreaterPrecisionOperand.expected

+159-159
Large diffs are not rendered by default.

c/common/src/codingstandards/c/UndefinedBehavior.qll

+5
Original file line numberDiff line numberDiff line change
@@ -25,4 +25,9 @@ class CUndefinedMainDefinition extends CUndefinedBehavior, Function {
2525
(this.getName() = "main" or this.getName().indexOf("____codeql_coding_standards") = 0) and
2626
not this instanceof C99MainFunction
2727
}
28+
29+
override string getReason() {
30+
result =
31+
"The behavior of the program is undefined because the main function is not defined according to the C standard."
32+
}
2833
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
- `A4-7-1` - `IntegerExpressionLeadToDataLoss.ql`:
2+
- Address reported FP in #396. Exclude shift operations guarded to prevent undefined behavior that could lead to dataloss.
3+
- `INT34-C` - `ExprShiftedbyNegativeOrGreaterPrecisionOperand.ql`:
4+
- Format the alert message according to the style-guide.

cpp/autosar/src/rules/M0-1-4/SingleUsePODVariable.qll

+2-2
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ private string getConstExprValue(Variable v) {
1111
}
1212

1313
/**
14-
* Gets the number of uses of variable `v` in an opaque assignment, where an opaqua assignment for example a cast from one type to the other and `v` is assumed to be a member of the resulting type.
14+
* Gets the number of uses of variable `v` in an opaque assignment, where an opaque assignment is a cast from one type to the other, and `v` is assumed to be a member of the resulting type.
1515
* e.g.,
1616
* struct foo {
1717
* int bar;
@@ -42,7 +42,7 @@ Expr getIndirectSubObjectAssignedValue(MemberVariable subobject) {
4242
result = externalInitializerCall
4343
)
4444
or
45-
// the object this subject is part of is initialized and we assumes this initializes the subobject.
45+
// the object this subject is part of is initialized and we assume this initializes the subobject.
4646
instanceOfSomeStruct.getType() = someStruct and
4747
result = instanceOfSomeStruct.getInitializer().getExpr()
4848
)

cpp/autosar/test/rules/A4-7-1/IntegerExpressionLeadToDataLoss.expected

+3
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,6 @@
1010
| test.cpp:22:12:22:16 | ... + ... | Binary expression ...+... may overflow. |
1111
| test.cpp:50:7:50:14 | ... + ... | Binary expression ...+... may overflow. |
1212
| test.cpp:62:8:62:10 | ... ++ | Binary expression ...++... may overflow. |
13+
| test.cpp:91:10:91:17 | ... << ... | Binary expression ...<<... may overflow. |
14+
| test.cpp:95:10:95:17 | ... << ... | Binary expression ...<<... may overflow. |
15+
| test.cpp:98:8:98:15 | ... << ... | Binary expression ...<<... may overflow. |

cpp/autosar/test/rules/A4-7-1/test.cpp

+25
Original file line numberDiff line numberDiff line change
@@ -72,4 +72,29 @@ void test_pointer() {
7272
int *p = nullptr;
7373
p++; // COMPLIANT - not covered by this rule
7474
p--; // COMPLIANT - not covered by this rule
75+
}
76+
77+
extern unsigned int popcount(unsigned int);
78+
#define PRECISION(x) popcount(x)
79+
void test_guarded_shifts(unsigned int p1, int p2) {
80+
unsigned int l1;
81+
82+
if (p2 < popcount(p1) && p2 > 0) {
83+
l1 = p1 << p2; // COMPLIANT
84+
}
85+
86+
if (p2 < PRECISION(p1) && p2 > 0) {
87+
l1 = p1 << p2; // COMPLIANT
88+
}
89+
90+
if (p2 < popcount(p1)) {
91+
l1 = p1 << p2; // NON_COMPLIANT - p2 could be negative
92+
}
93+
94+
if (p2 > 0) {
95+
l1 = p1 << p2; // NON_COMPLIANT - p2 could have a higher precision
96+
}
97+
98+
l1 = p1 << p2; // NON_COMPLIANT - p2 may have a higher precision or could be
99+
// negative
75100
}

cpp/common/src/codingstandards/cpp/Expr.qll

+8
Original file line numberDiff line numberDiff line change
@@ -203,3 +203,11 @@ class UnevaluatedExprExtension extends Expr {
203203
)
204204
}
205205
}
206+
207+
/** A class representing left and right bitwise shift operations. */
208+
class BitShiftExpr extends BinaryBitwiseOperation {
209+
BitShiftExpr() {
210+
this instanceof LShiftExpr or
211+
this instanceof RShiftExpr
212+
}
213+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
/** A module to reason about functions, such as well-known functions. */
2+
3+
import cpp
4+
5+
/**
6+
* A function whose name is suggestive that it counts the number of bits set.
7+
*/
8+
class PopCount extends Function {
9+
PopCount() { this.getName().toLowerCase().matches("%popc%nt%") }
10+
}

cpp/common/src/codingstandards/cpp/Literals.qll

+4
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,10 @@ class Utf32StringLiteral extends StringLiteral {
3030
Utf32StringLiteral() { this.getValueText().regexpMatch("(?s)\\s*U\".*") }
3131
}
3232

33+
class LiteralZero extends Literal {
34+
LiteralZero() { this.getValue() = "0" }
35+
}
36+
3337
/**
3438
* A literal resulting from the use of a constexpr
3539
* variable, or macro expansion.

cpp/common/src/codingstandards/cpp/Macro.qll

+7
Original file line numberDiff line numberDiff line change
@@ -88,3 +88,10 @@ class UserProvidedMacro extends Macro {
8888
class LibraryMacro extends Macro {
8989
LibraryMacro() { not this instanceof UserProvidedMacro }
9090
}
91+
92+
/**
93+
* A macro which is suggestive that it is used to determine the precision of an integer.
94+
*/
95+
class PrecisionMacro extends Macro {
96+
PrecisionMacro() { this.getName().toLowerCase().matches("precision") }
97+
}

cpp/common/src/codingstandards/cpp/Overflow.qll

+5-1
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ import SimpleRangeAnalysisCustomizations
88
import semmle.code.cpp.controlflow.Guards
99
import codingstandards.cpp.dataflow.TaintTracking
1010
import semmle.code.cpp.valuenumbering.GlobalValueNumbering
11+
import codingstandards.cpp.Expr
12+
import codingstandards.cpp.UndefinedBehavior
1113

1214
/**
1315
* An integer operation that may overflow, underflow or wrap.
@@ -40,7 +42,9 @@ class InterestingOverflowingOperation extends Operation {
4042
// Not within a macro
4143
not this.isAffectedByMacro() and
4244
// Ignore pointer arithmetic
43-
not this instanceof PointerArithmeticOperation
45+
not this instanceof PointerArithmeticOperation and
46+
// In case of the shift operation, it must cause undefined behavior
47+
(this instanceof BitShiftExpr implies this instanceof ShiftByNegativeOrGreaterPrecisionOperand)
4448
}
4549

4650
/**

cpp/common/src/codingstandards/cpp/Type.qll

+11
Original file line numberDiff line numberDiff line change
@@ -59,3 +59,14 @@ Type stripSpecifiers(Type type) {
5959
then result = stripSpecifiers(type.(SpecifiedType).getBaseType())
6060
else result = type
6161
}
62+
63+
/**
64+
* Get the precision of an integral type, where precision is defined as the number of bits
65+
* that can be used to represent the numeric value.
66+
* https://wiki.sei.cmu.edu/confluence/display/c/INT35-C.+Use+correct+integer+precisions
67+
*/
68+
int getPrecision(IntegralType type) {
69+
type.isExplicitlyUnsigned() and result = type.getSize() * 8
70+
or
71+
type.isExplicitlySigned() and result = type.getSize() * 8 - 1
72+
}
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,65 @@
11
import cpp
2+
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
3+
import semmle.code.cpp.valuenumbering.GlobalValueNumbering
4+
import semmle.code.cpp.controlflow.Guards
5+
import codingstandards.cpp.Literals
6+
import codingstandards.cpp.Expr
7+
import codingstandards.cpp.Macro
8+
import codingstandards.cpp.Type
9+
import codingstandards.cpp.Function
210

311
/**
412
* Library for modeling undefined behavior.
513
*/
6-
abstract class UndefinedBehavior extends Locatable { }
14+
abstract class UndefinedBehavior extends Locatable {
15+
abstract string getReason();
16+
}
717

818
abstract class CPPUndefinedBehavior extends UndefinedBehavior { }
19+
20+
class ShiftByNegativeOrGreaterPrecisionOperand extends UndefinedBehavior, BitShiftExpr {
21+
string reason;
22+
23+
ShiftByNegativeOrGreaterPrecisionOperand() {
24+
getPrecision(this.getLeftOperand().getExplicitlyConverted().getUnderlyingType()) <=
25+
upperBound(this.getRightOperand()) and
26+
reason =
27+
"The operand '" + this.getLeftOperand() + "' is shifted by an expression '" +
28+
this.getRightOperand() + "' whose upper bound (" + upperBound(this.getRightOperand()) +
29+
") is greater than or equal to the precision." and
30+
/*
31+
* this statement is not at a basic block where
32+
* `this_rhs < PRECISION(...)` is ensured
33+
*/
34+
35+
not exists(GuardCondition gc, BasicBlock block, Expr precisionCall, Expr lTLhs |
36+
block = this.getBasicBlock() and
37+
(
38+
precisionCall.(FunctionCall).getTarget() instanceof PopCount
39+
or
40+
precisionCall = any(PrecisionMacro pm).getAnInvocation().getExpr()
41+
)
42+
|
43+
globalValueNumber(lTLhs) = globalValueNumber(this.getRightOperand()) and
44+
gc.ensuresLt(lTLhs, precisionCall, 0, block, true)
45+
)
46+
or
47+
lowerBound(this.getRightOperand()) < 0 and
48+
reason =
49+
"The operand '" + this.getLeftOperand() + "' is shifted by an expression '" +
50+
this.getRightOperand() + "' which may be negative." and
51+
/*
52+
* this statement is not at a basic block where
53+
* `this_rhs > 0` is ensured
54+
*/
55+
56+
not exists(GuardCondition gc, BasicBlock block, Expr literalZero, Expr lTLhs |
57+
block = this.getBasicBlock() and
58+
literalZero instanceof LiteralZero and
59+
globalValueNumber(lTLhs) = globalValueNumber(this.getRightOperand()) and
60+
gc.ensuresLt(literalZero, lTLhs, 0, block, true)
61+
)
62+
}
63+
64+
override string getReason() { result = reason }
65+
}

0 commit comments

Comments
 (0)