Skip to content

Navigation Menu

Sign in

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Appearance settings

Commit d34b85c

Browse filesBrowse 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
Copy full SHA for d34b85c

14 files changed

+3548
-52
lines changed

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

Copy file name to clipboard
+142Lines changed: 142 additions & 0 deletions
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

Copy file name to clipboard
+202Lines changed: 202 additions & 0 deletions
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 (0)
Morty Proxy This is a proxified and sanitized view of the page, visit original site.