Skip to content

Commit 1c881e3

Browse files
rvermeulenrvermeulen
committed
Rewrite INT34-C as an instance of undefined behavior.
This is in preparation to share the guard validation with A4-7-1.
1 parent 36d6150 commit 1c881e3

File tree

8 files changed

+110
-87
lines changed

8 files changed

+110
-87
lines changed

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

Lines changed: 4 additions & 86 deletions
Original file line numberDiff line numberDiff line change
@@ -15,91 +15,9 @@ 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
20+
from ShiftByNegativeOrGreaterPrecisionOperand badShift
10221
where
103-
not isExcluded(badShift, Types1Package::exprShiftedbyNegativeOrGreaterPrecisionOperandQuery()) and
104-
isForbiddenShiftExpr(badShift, message)
105-
select badShift, message
22+
not isExcluded(badShift, Types1Package::exprShiftedbyNegativeOrGreaterPrecisionOperandQuery())
23+
select badShift, badShift.getReason()

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

Lines changed: 5 additions & 0 deletions
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 = "The behavior of the program is undefined because the main function is not defined according to the C standard."
31+
}
32+
2833
}

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -180,3 +180,11 @@ module MisraExpr {
180180
CValue() { isCValue(this) }
181181
}
182182
}
183+
184+
/** A class representing left and right bitwise shift operations. */
185+
class BitShiftExpr extends BinaryBitwiseOperation {
186+
BitShiftExpr() {
187+
this instanceof LShiftExpr or
188+
this instanceof RShiftExpr
189+
}
190+
}

‎cpp/common/src/codingstandards/cpp/Function.qll

Lines changed: 10 additions & 0 deletions
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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,3 +28,7 @@ class Utf16StringLiteral extends StringLiteral {
2828
class Utf32StringLiteral extends StringLiteral {
2929
Utf32StringLiteral() { this.getValueText().regexpMatch("(?s)\\s*U\".*") }
3030
}
31+
32+
class LiteralZero extends Literal {
33+
LiteralZero() { this.getValue() = "0" }
34+
}

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

Lines changed: 7 additions & 0 deletions
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/Type.qll

Lines changed: 11 additions & 0 deletions
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+
}

‎cpp/common/src/codingstandards/cpp/UndefinedBehavior.qll

Lines changed: 61 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,68 @@
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+
(
25+
getPrecision(this.getLeftOperand().getExplicitlyConverted().getUnderlyingType()) <=
26+
upperBound(this.getRightOperand()) and
27+
reason =
28+
"The operand " + this.getLeftOperand() + " is shifted by an expression " +
29+
this.getRightOperand() + " whose upper bound (" + upperBound(this.getRightOperand()) +
30+
") is greater than or equal to the precision."
31+
or
32+
lowerBound(this.getRightOperand()) < 0 and
33+
reason =
34+
"The operand " + this.getLeftOperand() + " is shifted by an expression " +
35+
this.getRightOperand() + " which may be negative."
36+
) and
37+
/*
38+
* this statement is not at a basic block where
39+
* `this_rhs < PRECISION(...)` is ensured
40+
*/
41+
42+
not exists(GuardCondition gc, BasicBlock block, Expr precisionCall, Expr lTLhs |
43+
block = this.getBasicBlock() and
44+
(
45+
precisionCall.(FunctionCall).getTarget() instanceof PopCount
46+
or
47+
precisionCall = any(PrecisionMacro pm).getAnInvocation().getExpr()
48+
)
49+
|
50+
globalValueNumber(lTLhs) = globalValueNumber(this.getRightOperand()) and
51+
gc.ensuresLt(lTLhs, precisionCall, 0, block, true)
52+
) and
53+
/*
54+
* this statement is not at a basic block where
55+
* `this_rhs < 0` is ensured
56+
*/
57+
58+
not exists(GuardCondition gc, BasicBlock block, Expr literalZero, Expr lTLhs |
59+
block = this.getBasicBlock() and
60+
literalZero instanceof LiteralZero
61+
|
62+
globalValueNumber(lTLhs) = globalValueNumber(this.getRightOperand()) and
63+
gc.ensuresLt(lTLhs, literalZero, 0, block, true)
64+
)
65+
}
66+
67+
override string getReason() { result = reason }
68+
}

0 commit comments

Comments
 (0)