Skip to content

Commit 638c083

Browse files
MichaelRFairhurstMichaelRFairhurst
committed
save work for draft PR
1 parent 70b1ed4 commit 638c083

16 files changed

+2761
-0
lines changed

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

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
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 high
8+
* @problem.severity error
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+
/**
48+
* An additional flow step to handle operations which propagate Infinity.
49+
*
50+
* This double checks that an Infinity may propagate by checking the `RestrictedRangeAnalysis`
51+
* value estimate. This is conservative, since `RestrictedRangeAnalysis` is performed locally
52+
* in scope with unanalyzable values in a finite range. However, this conservative approach
53+
* leverages analysis of guards and other local conditions to avoid false positives.
54+
*/
55+
predicate isAdditionalFlowStep(DataFlow::Node source, DataFlow::Node sink) {
56+
exists(Operation o |
57+
o.getAnOperand() = source.asExpr() and
58+
o = sink.asExpr() and
59+
potentialSource(sink)
60+
)
61+
}
62+
63+
predicate isSink(DataFlow::Node node) {
64+
(
65+
// Require that range analysis finds this value potentially infinite, to avoid false positives
66+
// in the presence of guards. This may induce false negatives.
67+
exprMayEqualInfinity(node.asExpr(), _) or
68+
// Unanalyzable expressions are not checked against range analysis, which assumes a finite
69+
// range.
70+
not RestrictedRangeAnalysis::analyzableExpr(node.asExpr())
71+
) and
72+
(
73+
// Case 2: NaNs and infinities shall not be cast to integers
74+
exists(Conversion c |
75+
node.asExpr() = c.getUnconverted() and
76+
c.getExpr().getType() instanceof FloatingPointType and
77+
c.getType() instanceof IntegralType
78+
)
79+
or
80+
// Case 3: Infinities shall not underflow or otherwise produce finite values
81+
exists(BinaryOperation op |
82+
node.asExpr() = op.getRightOperand() and
83+
op.getOperator() = ["/", "%"]
84+
)
85+
)
86+
}
87+
}
88+
89+
module InvalidInfinityFlow = DataFlow::Global<InvalidInfinityUsage>;
90+
91+
import InvalidInfinityFlow::PathGraph
92+
93+
from
94+
Element elem, InvalidInfinityFlow::PathNode source, InvalidInfinityFlow::PathNode sink,
95+
string msg, string sourceString
96+
where
97+
elem = MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr()) and
98+
not isExcluded(elem, FloatingTypes2Package::possibleMisuseOfUndetectedInfinityQuery()) and
99+
(
100+
InvalidInfinityFlow::flow(source.getNode(), sink.getNode()) and
101+
msg = "Invalid usage of possible $@." and
102+
sourceString = "infinity"
103+
)
104+
select elem, source, sink, msg, source, sourceString

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

Lines changed: 157 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,157 @@
1+
/**
2+
* @id c/misra/possible-misuse-of-undetected-na-n
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 high
8+
* @problem.severity error
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+
// IEEE 754-1985 Section 7.1 invalid operations
27+
class InvalidOperationExpr extends BinaryOperation {
28+
string reason;
29+
30+
InvalidOperationExpr() {
31+
// Usual arithmetic conversions in both languages mean that if either operand is a floating
32+
// type, the other one is converted to a floating type as well.
33+
getAnOperand().getFullyConverted().getType() instanceof FloatingPointType and
34+
(
35+
// 7.1.1 propagates signaling NaNs, we rely on flow analysis and/or assume quiet NaNs, so we
36+
// intentionally do not cover this case.
37+
// 7.1.2: magnitude subtraction of infinities, such as +Inf + -Inf
38+
getOperator() = "+" and
39+
exists(Boolean sign |
40+
exprMayEqualInfinity(getLeftOperand(), sign) and
41+
exprMayEqualInfinity(getRightOperand(), sign.booleanNot())
42+
) and
43+
reason = "possible addition of infinity and negative infinity"
44+
or
45+
// 7.1.2 continued
46+
getOperator() = "-" and
47+
exists(Boolean sign |
48+
exprMayEqualInfinity(getLeftOperand(), sign) and
49+
exprMayEqualInfinity(getRightOperand(), sign)
50+
) and
51+
reason = "possible subtraction of an infinity from itself"
52+
or
53+
// 7.1.3: multiplication of zero by infinity
54+
getOperator() = "*" and
55+
exprMayEqualZero(getAnOperand()) and
56+
exprMayEqualInfinity(getAnOperand(), _) and
57+
reason = "possible multiplication of zero by infinity"
58+
or
59+
// 7.1.4: Division of zero by zero, or infinity by infinity
60+
getOperator() = "/" and
61+
exprMayEqualZero(getLeftOperand()) and
62+
exprMayEqualZero(getRightOperand()) and
63+
reason = "possible division of zero by zero"
64+
or
65+
// 7.1.4 continued
66+
getOperator() = "/" and
67+
exprMayEqualInfinity(getLeftOperand(), _) and
68+
exprMayEqualInfinity(getRightOperand(), _) and
69+
reason = "possible division of infinity by infinity"
70+
or
71+
// 7.1.5: x % y where y is zero or x is infinite
72+
getOperator() = "%" and
73+
exprMayEqualInfinity(getLeftOperand(), _) and
74+
reason = "possible modulus of infinity"
75+
or
76+
// 7.1.5 continued
77+
getOperator() = "%" and
78+
exprMayEqualZero(getRightOperand()) and
79+
reason = "possible modulus by zero"
80+
// 7.1.6 handles the sqrt function, not covered here.
81+
// 7.1.7 declares exceptions during invalid conversions, which we catch as sinks in our flow
82+
// analysis.
83+
// 7.1.8 declares exceptions for unordered comparisons, which we catch as sinks in our flow
84+
// analysis.
85+
)
86+
}
87+
88+
string getReason() { result = reason }
89+
}
90+
91+
module InvalidNaNUsage implements DataFlow::ConfigSig {
92+
93+
/**
94+
* An expression which has non-NaN inputs and may produce a NaN output.
95+
*/
96+
predicate isSource(DataFlow::Node node) {
97+
potentialSource(node) and
98+
not exists(DataFlow::Node prior |
99+
isAdditionalFlowStep(prior, node) and
100+
potentialSource(prior)
101+
)
102+
}
103+
104+
/**
105+
* An expression which may produce a NaN output.
106+
*/
107+
additional predicate potentialSource(DataFlow::Node node) {
108+
node.asExpr() instanceof InvalidOperationExpr
109+
}
110+
111+
/**
112+
* Add an additional flow step to handle NaN propagation through floating point operations.
113+
*/
114+
predicate isAdditionalFlowStep(DataFlow::Node source, DataFlow::Node sink) {
115+
exists(Operation o |
116+
o.getAnOperand() = source.asExpr() and
117+
o = sink.asExpr() and
118+
o.getType() instanceof FloatingPointType
119+
)
120+
}
121+
122+
predicate isSink(DataFlow::Node node) {
123+
// Case 1: NaNs shall not be compared, except to themselves
124+
exists(ComparisonOperation cmp |
125+
node.asExpr() = cmp.getAnOperand() and
126+
not hashCons(cmp.getLeftOperand()) = hashCons(cmp.getRightOperand())
127+
)
128+
or
129+
// Case 2: NaNs and infinities shall not be cast to integers
130+
exists(Conversion c |
131+
node.asExpr() = c.getUnconverted() and
132+
c.getExpr().getType() instanceof FloatingPointType and
133+
c.getType() instanceof IntegralType
134+
)
135+
//or
136+
//// Case 4: Functions shall not return NaNs or infinities
137+
//exists(ReturnStmt ret | node.asExpr() = ret.getExpr())
138+
}
139+
}
140+
141+
module InvalidNaNFlow = DataFlow::Global<InvalidNaNUsage>;
142+
143+
import InvalidNaNFlow::PathGraph
144+
145+
from
146+
Element elem, InvalidNaNFlow::PathNode source, InvalidNaNFlow::PathNode sink, string msg,
147+
string sourceString
148+
where
149+
elem = MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr()) and
150+
not isExcluded(elem, FloatingTypes2Package::possibleMisuseOfUndetectedNaNQuery()) and
151+
(
152+
InvalidNaNFlow::flow(source.getNode(), sink.getNode()) and
153+
msg = "Invalid usage of possible $@." and
154+
sourceString =
155+
"NaN resulting from " + source.getNode().asExpr().(InvalidOperationExpr).getReason()
156+
)
157+
select elem, source, sink, msg, source, sourceString

0 commit comments

Comments
 (0)