Skip to content

Commit d34b85c

Browse files
MichaelRFairhurstMichaelRFairhurst
authored
Merge pull request #849 from github/michaelrfairhurst/implement-floatingtype-package
Implement DIR-4-15, detection of NaNs and Infinities
2 parents 8f65892 + 8885ee1 commit d34b85c

14 files changed

+3548
-52
lines changed

‎c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql

+142
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
/**
2+
* @id c/misra/possible-misuse-of-undetected-infinity
3+
* @name DIR-4-15: Evaluation of floating-point expressions shall not lead to the undetected generation of infinities
4+
* @description Evaluation of floating-point expressions shall not lead to the undetected generation
5+
* of infinities.
6+
* @kind path-problem
7+
* @precision medium
8+
* @problem.severity warning
9+
* @tags external/misra/id/dir-4-15
10+
* correctness
11+
* external/misra/c/2012/amendment3
12+
* external/misra/obligation/required
13+
*/
14+
15+
import cpp
16+
import codeql.util.Boolean
17+
import codingstandards.c.misra
18+
import codingstandards.cpp.RestrictedRangeAnalysis
19+
import codingstandards.cpp.FloatingPoint
20+
import codingstandards.cpp.AlertReporting
21+
import semmle.code.cpp.controlflow.Guards
22+
import semmle.code.cpp.dataflow.new.DataFlow
23+
import semmle.code.cpp.dataflow.new.TaintTracking
24+
import semmle.code.cpp.controlflow.Dominance
25+
26+
module InvalidInfinityUsage implements DataFlow::ConfigSig {
27+
/**
28+
* An operation which does not have Infinity as an input, but may produce Infinity, according
29+
* to the `RestrictedRangeAnalysis` module.
30+
*/
31+
predicate isSource(DataFlow::Node node) {
32+
potentialSource(node) and
33+
not exists(DataFlow::Node prior |
34+
isAdditionalFlowStep(prior, node) and
35+
potentialSource(prior)
36+
)
37+
}
38+
39+
/**
40+
* An operation which may produce Infinity acconding to the `RestrictedRangeAnalysis` module.
41+
*/
42+
additional predicate potentialSource(DataFlow::Node node) {
43+
node.asExpr() instanceof Operation and
44+
exprMayEqualInfinity(node.asExpr(), _)
45+
}
46+
47+
predicate isBarrierOut(DataFlow::Node node) {
48+
guardedNotFPClass(node.asExpr(), TInfinite())
49+
or
50+
exists(Expr e |
51+
e.getType() instanceof IntegralType and
52+
e = node.asConvertedExpr()
53+
)
54+
}
55+
56+
/**
57+
* An additional flow step to handle operations which propagate Infinity.
58+
*
59+
* This double checks that an Infinity may propagate by checking the `RestrictedRangeAnalysis`
60+
* value estimate. This is conservative, since `RestrictedRangeAnalysis` is performed locally
61+
* in scope with unanalyzable values in a finite range. However, this conservative approach
62+
* leverages analysis of guards and other local conditions to avoid false positives.
63+
*/
64+
predicate isAdditionalFlowStep(DataFlow::Node source, DataFlow::Node sink) {
65+
exists(Operation o |
66+
o.getAnOperand() = source.asExpr() and
67+
o = sink.asExpr() and
68+
potentialSource(sink)
69+
)
70+
}
71+
72+
predicate isSink(DataFlow::Node node) {
73+
node instanceof InvalidInfinityUsage and
74+
(
75+
// Require that range analysis finds this value potentially infinite, to avoid false positives
76+
// in the presence of guards. This may induce false negatives.
77+
exprMayEqualInfinity(node.asExpr(), _)
78+
or
79+
// Unanalyzable expressions are not checked against range analysis, which assumes a finite
80+
// range.
81+
not RestrictedRangeAnalysis::canBoundExpr(node.asExpr())
82+
or
83+
node.asExpr().(VariableAccess).getTarget() instanceof Parameter
84+
)
85+
}
86+
}
87+
88+
class InvalidInfinityUsage extends DataFlow::Node {
89+
string description;
90+
91+
InvalidInfinityUsage() {
92+
// Case 2: NaNs and infinities shall not be cast to integers
93+
exists(Conversion c |
94+
asExpr() = c.getUnconverted() and
95+
c.getExpr().getType() instanceof FloatingPointType and
96+
c.getType() instanceof IntegralType and
97+
description = "cast to integer."
98+
)
99+
or
100+
// Case 3: Infinities shall not underflow or otherwise produce finite values
101+
exists(BinaryOperation op |
102+
asExpr() = op.getRightOperand() and
103+
op.getOperator() = "/" and
104+
description = "divisor, which would silently underflow and produce zero."
105+
)
106+
}
107+
108+
string getDescription() { result = description }
109+
}
110+
111+
module InvalidInfinityFlow = DataFlow::Global<InvalidInfinityUsage>;
112+
113+
import InvalidInfinityFlow::PathGraph
114+
115+
from
116+
Element elem, InvalidInfinityFlow::PathNode source, InvalidInfinityFlow::PathNode sink,
117+
InvalidInfinityUsage usage, Expr sourceExpr, string sourceString, Function function,
118+
string computedInFunction
119+
where
120+
elem = MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr()) and
121+
not InvalidInfinityFlow::PathGraph::edges(_, source, _, _) and
122+
not InvalidInfinityFlow::PathGraph::edges(sink, _, _, _) and
123+
not isExcluded(elem, FloatingTypes2Package::possibleMisuseOfUndetectedInfinityQuery()) and
124+
not sourceExpr.isFromTemplateInstantiation(_) and
125+
not usage.asExpr().isFromTemplateInstantiation(_) and
126+
usage = sink.getNode() and
127+
sourceExpr = source.getNode().asExpr() and
128+
function = sourceExpr.getEnclosingFunction() and
129+
InvalidInfinityFlow::flow(source.getNode(), usage) and
130+
(
131+
if not sourceExpr.getEnclosingFunction() = usage.asExpr().getEnclosingFunction()
132+
then computedInFunction = "computed in function $@ "
133+
else computedInFunction = ""
134+
) and
135+
(
136+
if sourceExpr instanceof DivExpr
137+
then sourceString = "from division by zero"
138+
else sourceString = sourceExpr.toString()
139+
)
140+
select elem, source, sink,
141+
"Possibly infinite float value $@ " + computedInFunction + "flows to " + usage.getDescription(),
142+
sourceExpr, sourceString, function, function.getName()

‎c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql

+202
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,202 @@
1+
/**
2+
* @id c/misra/possible-misuse-of-undetected-nan
3+
* @name DIR-4-15: Evaluation of floating-point expressions shall not lead to the undetected generation of NaNs
4+
* @description Evaluation of floating-point expressions shall not lead to the undetected generation
5+
* of NaNs.
6+
* @kind path-problem
7+
* @precision low
8+
* @problem.severity warning
9+
* @tags external/misra/id/dir-4-15
10+
* correctness
11+
* external/misra/c/2012/amendment3
12+
* external/misra/obligation/required
13+
*/
14+
15+
import cpp
16+
import codeql.util.Boolean
17+
import codingstandards.c.misra
18+
import codingstandards.cpp.RestrictedRangeAnalysis
19+
import codingstandards.cpp.FloatingPoint
20+
import codingstandards.cpp.AlertReporting
21+
import semmle.code.cpp.controlflow.Guards
22+
import semmle.code.cpp.dataflow.new.DataFlow
23+
import semmle.code.cpp.dataflow.new.TaintTracking
24+
import semmle.code.cpp.controlflow.Dominance
25+
26+
abstract class PotentiallyNaNExpr extends Expr {
27+
abstract string getReason();
28+
}
29+
30+
class DomainErrorFunctionCall extends FunctionCall, PotentiallyNaNExpr {
31+
string reason;
32+
33+
DomainErrorFunctionCall() { RestrictedDomainError::hasDomainError(this, reason) }
34+
35+
override string getReason() { result = reason }
36+
}
37+
38+
// IEEE 754-1985 Section 7.1 invalid operations
39+
class InvalidOperationExpr extends BinaryOperation, PotentiallyNaNExpr {
40+
string reason;
41+
42+
InvalidOperationExpr() {
43+
// Usual arithmetic conversions in both languages mean that if either operand is a floating
44+
// type, the other one is converted to a floating type as well.
45+
getAnOperand().getFullyConverted().getType() instanceof FloatingPointType and
46+
(
47+
// 7.1.1 propagates signaling NaNs, we rely on flow analysis and/or assume quiet NaNs, so we
48+
// intentionally do not cover this case.
49+
// 7.1.2: magnitude subtraction of infinities, such as +Inf + -Inf
50+
getOperator() = "+" and
51+
exists(Boolean sign |
52+
exprMayEqualInfinity(getLeftOperand(), sign) and
53+
exprMayEqualInfinity(getRightOperand(), sign.booleanNot())
54+
) and
55+
reason = "from addition of infinity and negative infinity"
56+
or
57+
// 7.1.2 continued
58+
getOperator() = "-" and
59+
exists(Boolean sign |
60+
exprMayEqualInfinity(getLeftOperand(), sign) and
61+
exprMayEqualInfinity(getRightOperand(), sign)
62+
) and
63+
reason = "from subtraction of an infinity from itself"
64+
or
65+
// 7.1.3: multiplication of zero by infinity
66+
getOperator() = "*" and
67+
exists(Expr zeroOp, Expr infinityOp |
68+
zeroOp = getAnOperand() and
69+
infinityOp = getAnOperand() and
70+
not zeroOp = infinityOp and
71+
exprMayEqualZero(zeroOp) and
72+
exprMayEqualInfinity(infinityOp, _)
73+
) and
74+
reason = "from multiplication of zero by infinity"
75+
or
76+
// 7.1.4: Division of zero by zero, or infinity by infinity
77+
getOperator() = "/" and
78+
exprMayEqualZero(getLeftOperand()) and
79+
exprMayEqualZero(getRightOperand()) and
80+
reason = "from division of zero by zero"
81+
or
82+
// 7.1.4 continued
83+
getOperator() = "/" and
84+
exprMayEqualInfinity(getLeftOperand(), _) and
85+
exprMayEqualInfinity(getRightOperand(), _) and
86+
reason = "from division of infinity by infinity"
87+
or
88+
// 7.1.5: x % y where y is zero or x is infinite
89+
getOperator() = "%" and
90+
exprMayEqualInfinity(getLeftOperand(), _) and
91+
reason = "from modulus of infinity"
92+
or
93+
// 7.1.5 continued
94+
getOperator() = "%" and
95+
exprMayEqualZero(getRightOperand()) and
96+
reason = "from modulus by zero"
97+
// 7.1.6 handles the sqrt function, not covered here.
98+
// 7.1.7 declares exceptions during invalid conversions, which we catch as sinks in our flow
99+
// analysis.
100+
// 7.1.8 declares exceptions for unordered comparisons, which we catch as sinks in our flow
101+
// analysis.
102+
)
103+
}
104+
105+
override string getReason() { result = reason }
106+
}
107+
108+
module InvalidNaNUsage implements DataFlow::ConfigSig {
109+
/**
110+
* An expression which has non-NaN inputs and may produce a NaN output.
111+
*/
112+
predicate isSource(DataFlow::Node node) {
113+
potentialSource(node) and
114+
not exists(DataFlow::Node prior |
115+
isAdditionalFlowStep(prior, node) and
116+
potentialSource(prior)
117+
)
118+
}
119+
120+
/**
121+
* An expression which may produce a NaN output.
122+
*/
123+
additional predicate potentialSource(DataFlow::Node node) {
124+
node.asExpr() instanceof PotentiallyNaNExpr
125+
}
126+
127+
predicate isBarrierOut(DataFlow::Node node) {
128+
guardedNotFPClass(node.asExpr(), TNaN())
129+
or
130+
exists(Expr e |
131+
e.getType() instanceof IntegralType and
132+
e = node.asConvertedExpr()
133+
)
134+
}
135+
136+
/**
137+
* Add an additional flow step to handle NaN propagation through floating point operations.
138+
*/
139+
predicate isAdditionalFlowStep(DataFlow::Node source, DataFlow::Node sink) {
140+
exists(Operation o |
141+
o.getAnOperand() = source.asExpr() and
142+
o = sink.asExpr() and
143+
o.getType() instanceof FloatingPointType
144+
)
145+
}
146+
147+
predicate isSink(DataFlow::Node node) {
148+
not guardedNotFPClass(node.asExpr(), TNaN()) and
149+
node instanceof InvalidNaNUsage
150+
}
151+
}
152+
153+
class InvalidNaNUsage extends DataFlow::Node {
154+
string description;
155+
156+
InvalidNaNUsage() {
157+
// Case 1: NaNs shall not be compared, except to themselves
158+
exists(ComparisonOperation cmp |
159+
this.asExpr() = cmp.getAnOperand() and
160+
not hashCons(cmp.getLeftOperand()) = hashCons(cmp.getRightOperand()) and
161+
description = "comparison, which would always evaluate to false."
162+
)
163+
or
164+
// Case 2: NaNs and infinities shall not be cast to integers
165+
exists(Conversion c |
166+
this.asExpr() = c.getUnconverted() and
167+
c.getExpr().getType() instanceof FloatingPointType and
168+
c.getType() instanceof IntegralType and
169+
description = "a cast to integer."
170+
)
171+
}
172+
173+
string getDescription() { result = description }
174+
}
175+
176+
module InvalidNaNFlow = DataFlow::Global<InvalidNaNUsage>;
177+
178+
import InvalidNaNFlow::PathGraph
179+
180+
from
181+
Element elem, InvalidNaNFlow::PathNode source, InvalidNaNFlow::PathNode sink,
182+
InvalidNaNUsage usage, Expr sourceExpr, string sourceString, Function function,
183+
string computedInFunction
184+
where
185+
not InvalidNaNFlow::PathGraph::edges(_, source, _, _) and
186+
not InvalidNaNFlow::PathGraph::edges(sink, _, _, _) and
187+
not sourceExpr.isFromTemplateInstantiation(_) and
188+
not usage.asExpr().isFromTemplateInstantiation(_) and
189+
elem = MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr()) and
190+
usage = sink.getNode() and
191+
sourceExpr = source.getNode().asExpr() and
192+
sourceString = source.getNode().asExpr().(PotentiallyNaNExpr).getReason() and
193+
function = sourceExpr.getEnclosingFunction() and
194+
InvalidNaNFlow::flow(source.getNode(), usage) and
195+
(
196+
if not sourceExpr.getEnclosingFunction() = usage.asExpr().getEnclosingFunction()
197+
then computedInFunction = "computed in function $@ "
198+
else computedInFunction = ""
199+
)
200+
select elem, source, sink,
201+
"Possible NaN value $@ " + computedInFunction + "flows to " + usage.getDescription(), sourceExpr,
202+
sourceString, function, function.getName()

0 commit comments

Comments
 (0)