Skip to content

Commit dee2261

Browse files
MichaelRFairhurstMichaelRFairhurst
committed
Widening/dedupe fixes, plus math lib support
1 parent 4ee7629 commit dee2261

File tree

6 files changed

+496
-77
lines changed

6 files changed

+496
-77
lines changed

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

+4-4
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,6 @@ module InvalidInfinityUsage implements DataFlow::ConfigSig {
5151
e.getType() instanceof IntegralType and
5252
e = node.asConvertedExpr()
5353
)
54-
or
55-
// Sinks are places where Infinity produce a finite value
56-
isSink(node)
5754
}
5855

5956
/**
@@ -81,7 +78,9 @@ module InvalidInfinityUsage implements DataFlow::ConfigSig {
8178
or
8279
// Unanalyzable expressions are not checked against range analysis, which assumes a finite
8380
// range.
84-
not RestrictedRangeAnalysis::analyzableExpr(node.asExpr())
81+
not RestrictedRangeAnalysis::canBoundExpr(node.asExpr())
82+
or
83+
node.asExpr().(VariableAccess).getTarget() instanceof Parameter
8584
)
8685
}
8786
}
@@ -124,6 +123,7 @@ from
124123
where
125124
elem = MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr()) and
126125
not InvalidInfinityFlow::PathGraph::edges(_, source, _, _) and
126+
not InvalidInfinityFlow::PathGraph::edges(sink, _, _, _) and
127127
not isExcluded(elem, FloatingTypes2Package::possibleMisuseOfUndetectedInfinityQuery()) and
128128
not sourceExpr.isFromTemplateInstantiation(_) and
129129
not usage.asExpr().isFromTemplateInstantiation(_) and

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

+70-4
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,73 @@ import semmle.code.cpp.dataflow.new.DataFlow
2323
import semmle.code.cpp.dataflow.new.TaintTracking
2424
import semmle.code.cpp.controlflow.Dominance
2525

26+
bindingset[name]
27+
Function getMathVariants(string name) { result.hasGlobalOrStdName([name, name + "f", name + "l"]) }
28+
29+
predicate hasDomainError(FunctionCall fc, string description) {
30+
exists(Function functionWithDomainError | fc.getTarget() = functionWithDomainError |
31+
functionWithDomainError = [getMathVariants(["acos", "asin", "atanh"])] and
32+
not (
33+
RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) <= 1.0 and
34+
RestrictedRangeAnalysis::lowerBound(fc.getArgument(0)) >= -1.0
35+
) and
36+
description =
37+
"the argument has a range " + RestrictedRangeAnalysis::lowerBound(fc.getArgument(0)) + "..." +
38+
RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) + " which is outside the domain of this function (-1.0...1.0)"
39+
or
40+
functionWithDomainError = getMathVariants(["atan2", "pow"]) and
41+
(
42+
exprMayEqualZero(fc.getArgument(0)) and
43+
exprMayEqualZero(fc.getArgument(1)) and
44+
description = "both arguments are equal to zero"
45+
)
46+
or
47+
functionWithDomainError = getMathVariants("pow") and
48+
(
49+
RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) < 0.0 and
50+
RestrictedRangeAnalysis::upperBound(fc.getArgument(1)) < 0.0 and
51+
description = "both arguments are less than zero"
52+
)
53+
or
54+
functionWithDomainError = getMathVariants("acosh") and
55+
RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) < 1.0 and
56+
description = "argument is less than 1"
57+
or
58+
//pole error is the same as domain for logb and tgamma (but not ilogb - no pole error exists)
59+
functionWithDomainError = getMathVariants(["ilogb", "logb", "tgamma"]) and
60+
exprMayEqualZero(fc.getArgument(0)) and
61+
description = "argument is equal to zero"
62+
or
63+
functionWithDomainError = getMathVariants(["log", "log10", "log2", "sqrt"]) and
64+
RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) < 0.0 and
65+
description = "argument is negative"
66+
or
67+
functionWithDomainError = getMathVariants("log1p") and
68+
RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) < -1.0 and
69+
description = "argument is less than 1"
70+
or
71+
functionWithDomainError = getMathVariants("fmod") and
72+
exprMayEqualZero(fc.getArgument(1)) and
73+
description = "y is 0"
74+
)
75+
}
76+
77+
abstract class PotentiallyNaNExpr extends Expr {
78+
abstract string getReason();
79+
}
80+
81+
class DomainErrorFunctionCall extends FunctionCall, PotentiallyNaNExpr {
82+
string reason;
83+
84+
DomainErrorFunctionCall() {
85+
hasDomainError(this, reason)
86+
}
87+
88+
override string getReason() { result = reason }
89+
}
90+
2691
// IEEE 754-1985 Section 7.1 invalid operations
27-
class InvalidOperationExpr extends BinaryOperation {
92+
class InvalidOperationExpr extends BinaryOperation, PotentiallyNaNExpr {
2893
string reason;
2994

3095
InvalidOperationExpr() {
@@ -85,7 +150,7 @@ class InvalidOperationExpr extends BinaryOperation {
85150
)
86151
}
87152

88-
string getReason() { result = reason }
153+
override string getReason() { result = reason }
89154
}
90155

91156
module InvalidNaNUsage implements DataFlow::ConfigSig {
@@ -104,7 +169,7 @@ module InvalidNaNUsage implements DataFlow::ConfigSig {
104169
* An expression which may produce a NaN output.
105170
*/
106171
additional predicate potentialSource(DataFlow::Node node) {
107-
node.asExpr() instanceof InvalidOperationExpr
172+
node.asExpr() instanceof PotentiallyNaNExpr
108173
}
109174

110175
predicate isBarrierOut(DataFlow::Node node) {
@@ -173,13 +238,14 @@ from
173238
InvalidNaNUsage usage, Expr sourceExpr, string sourceString, Element extra, string extraString
174239
where
175240
not InvalidNaNFlow::PathGraph::edges(_, source, _, _) and
241+
not InvalidNaNFlow::PathGraph::edges(sink, _, _, _) and
176242
not sourceExpr.isFromTemplateInstantiation(_) and
177243
not usage.asExpr().isFromTemplateInstantiation(_) and
178244
elem = MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr()) and
179245
usage = sink.getNode() and
180246
sourceExpr = source.getNode().asExpr() and
181247
sourceString =
182-
" (" + source.getNode().asExpr().(InvalidOperationExpr).getReason() + ")" and
248+
" (" + source.getNode().asExpr().(PotentiallyNaNExpr).getReason() + ")" and
183249
InvalidNaNFlow::flow(source.getNode(), usage) and
184250
(
185251
if not sourceExpr.getEnclosingFunction() = usage.asExpr().getEnclosingFunction()

‎c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected

+58-24
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,21 @@ edges
2121
| test.c:77:15:77:21 | ... / ... | test.c:114:16:114:23 | l12 | provenance | |
2222
| test.c:77:15:77:21 | ... / ... | test.c:117:23:117:30 | l12 | provenance | |
2323
| test.c:77:15:77:21 | ... / ... | test.c:120:20:120:27 | l12 | provenance | |
24+
| test.c:175:22:175:22 | p | test.c:175:27:175:32 | p | provenance | |
25+
| test.c:183:34:183:34 | p | test.c:185:13:185:18 | p | provenance | |
26+
| test.c:189:32:189:32 | p | test.c:189:47:189:59 | ... + ... | provenance | Config |
27+
| test.c:189:47:189:59 | ... + ... | test.c:175:22:175:22 | p | provenance | |
28+
| test.c:189:47:189:59 | ... + ... | test.c:175:22:175:22 | p | provenance | |
29+
| test.c:189:51:189:59 | ... / ... | test.c:189:47:189:59 | ... + ... | provenance | Config |
30+
| test.c:193:13:194:15 | ... / ... | test.c:175:22:175:22 | p | provenance | |
31+
| test.c:200:25:200:33 | ... / ... | test.c:183:34:183:34 | p | provenance | |
32+
| test.c:204:19:204:27 | ... / ... | test.c:204:19:204:27 | ... / ... | provenance | |
33+
| test.c:204:19:204:27 | ... / ... | test.c:206:21:206:31 | ... + ... | provenance | Config |
34+
| test.c:206:21:206:31 | ... + ... | test.c:206:21:206:31 | ... + ... | provenance | |
35+
| test.c:206:21:206:31 | ... + ... | test.c:208:13:208:21 | middleInf | provenance | |
36+
| test.c:206:21:206:31 | ... + ... | test.c:210:23:210:31 | middleInf | provenance | |
37+
| test.c:208:13:208:21 | middleInf | test.c:175:22:175:22 | p | provenance | |
38+
| test.c:210:23:210:31 | middleInf | test.c:189:32:189:32 | p | provenance | |
2439
nodes
2540
| test.c:8:14:8:20 | ... / ... | semmle.label | ... / ... |
2641
| test.c:8:14:8:20 | ... / ... | semmle.label | ... / ... |
@@ -51,29 +66,48 @@ nodes
5166
| test.c:114:16:114:23 | l12 | semmle.label | l12 |
5267
| test.c:117:23:117:30 | l12 | semmle.label | l12 |
5368
| test.c:120:20:120:27 | l12 | semmle.label | l12 |
69+
| test.c:163:3:164:16 | ... / ... | semmle.label | ... / ... |
70+
| test.c:175:22:175:22 | p | semmle.label | p |
71+
| test.c:175:27:175:32 | p | semmle.label | p |
72+
| test.c:183:34:183:34 | p | semmle.label | p |
73+
| test.c:185:13:185:18 | p | semmle.label | p |
74+
| test.c:189:32:189:32 | p | semmle.label | p |
75+
| test.c:189:47:189:59 | ... + ... | semmle.label | ... + ... |
76+
| test.c:189:47:189:59 | ... + ... | semmle.label | ... + ... |
77+
| test.c:189:51:189:59 | ... / ... | semmle.label | ... / ... |
78+
| test.c:193:13:194:15 | ... / ... | semmle.label | ... / ... |
79+
| test.c:200:25:200:33 | ... / ... | semmle.label | ... / ... |
80+
| test.c:204:19:204:27 | ... / ... | semmle.label | ... / ... |
81+
| test.c:204:19:204:27 | ... / ... | semmle.label | ... / ... |
82+
| test.c:206:21:206:31 | ... + ... | semmle.label | ... + ... |
83+
| test.c:206:21:206:31 | ... + ... | semmle.label | ... + ... |
84+
| test.c:208:13:208:21 | middleInf | semmle.label | middleInf |
85+
| test.c:210:23:210:31 | middleInf | semmle.label | middleInf |
5486
subpaths
5587
#select
56-
| test.c:12:8:12:9 | l2 | test.c:8:14:8:20 | ... / ... | test.c:12:8:12:9 | l2 | Invalid usage of possible $@. | test.c:8:14:8:20 | ... / ... | infinity |
57-
| test.c:13:8:13:9 | l3 | test.c:8:14:8:20 | ... / ... | test.c:13:8:13:9 | l3 | Invalid usage of possible $@. | test.c:8:14:8:20 | ... / ... | infinity |
58-
| test.c:13:8:13:9 | l3 | test.c:9:14:9:16 | - ... | test.c:13:8:13:9 | l3 | Invalid usage of possible $@. | test.c:9:14:9:16 | - ... | infinity |
59-
| test.c:18:8:18:9 | l2 | test.c:8:14:8:20 | ... / ... | test.c:18:3:18:9 | l2 | Invalid usage of possible $@. | test.c:8:14:8:20 | ... / ... | infinity |
60-
| test.c:19:8:19:9 | l3 | test.c:8:14:8:20 | ... / ... | test.c:19:3:19:9 | l3 | Invalid usage of possible $@. | test.c:8:14:8:20 | ... / ... | infinity |
61-
| test.c:19:8:19:9 | l3 | test.c:9:14:9:16 | - ... | test.c:19:3:19:9 | l3 | Invalid usage of possible $@. | test.c:9:14:9:16 | - ... | infinity |
62-
| test.c:27:19:27:20 | l2 | test.c:8:14:8:20 | ... / ... | test.c:27:19:27:20 | l2 | Invalid usage of possible $@. | test.c:8:14:8:20 | ... / ... | infinity |
63-
| test.c:28:19:28:20 | l3 | test.c:8:14:8:20 | ... / ... | test.c:28:19:28:20 | l3 | Invalid usage of possible $@. | test.c:8:14:8:20 | ... / ... | infinity |
64-
| test.c:28:19:28:20 | l3 | test.c:9:14:9:16 | - ... | test.c:28:19:28:20 | l3 | Invalid usage of possible $@. | test.c:9:14:9:16 | - ... | infinity |
65-
| test.c:38:8:38:9 | l7 | test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | Invalid usage of possible $@. | test.c:31:14:32:15 | ... / ... | infinity |
66-
| test.c:61:11:61:17 | ... / ... | test.c:61:5:61:18 | ... / ... | test.c:61:5:61:18 | ... / ... | Invalid usage of possible $@. | test.c:61:5:61:18 | ... / ... | infinity |
67-
| test.c:66:11:66:19 | ... / ... | test.c:66:5:66:20 | ... / ... | test.c:66:5:66:20 | ... / ... | Invalid usage of possible $@. | test.c:66:5:66:20 | ... / ... | infinity |
68-
| test.c:72:20:72:28 | ... / ... | test.c:72:14:72:29 | ... / ... | test.c:72:14:72:29 | ... / ... | Invalid usage of possible $@. | test.c:72:14:72:29 | ... / ... | infinity |
69-
| test.c:75:24:75:32 | ... / ... | test.c:75:18:75:33 | ... / ... | test.c:75:18:75:33 | ... / ... | Invalid usage of possible $@. | test.c:75:18:75:33 | ... / ... | infinity |
70-
| test.c:79:10:79:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:79:5:79:12 | l12 | Invalid usage of possible $@. | test.c:77:15:77:21 | ... / ... | infinity |
71-
| test.c:87:10:87:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:87:5:87:12 | l12 | Invalid usage of possible $@. | test.c:77:15:77:21 | ... / ... | infinity |
72-
| test.c:91:10:91:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:91:5:91:12 | l12 | Invalid usage of possible $@. | test.c:77:15:77:21 | ... / ... | infinity |
73-
| test.c:93:10:93:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:93:5:93:12 | l12 | Invalid usage of possible $@. | test.c:77:15:77:21 | ... / ... | infinity |
74-
| test.c:99:10:99:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:99:5:99:12 | l12 | Invalid usage of possible $@. | test.c:77:15:77:21 | ... / ... | infinity |
75-
| test.c:105:10:105:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:105:5:105:12 | l12 | Invalid usage of possible $@. | test.c:77:15:77:21 | ... / ... | infinity |
76-
| test.c:111:10:111:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:111:5:111:12 | l12 | Invalid usage of possible $@. | test.c:77:15:77:21 | ... / ... | infinity |
77-
| test.c:114:21:114:23 | l12 | test.c:77:15:77:21 | ... / ... | test.c:114:16:114:23 | l12 | Invalid usage of possible $@. | test.c:77:15:77:21 | ... / ... | infinity |
78-
| test.c:117:28:117:30 | l12 | test.c:77:15:77:21 | ... / ... | test.c:117:23:117:30 | l12 | Invalid usage of possible $@. | test.c:77:15:77:21 | ... / ... | infinity |
79-
| test.c:120:25:120:27 | l12 | test.c:77:15:77:21 | ... / ... | test.c:120:20:120:27 | l12 | Invalid usage of possible $@. | test.c:77:15:77:21 | ... / ... | infinity |
88+
| test.c:12:8:12:9 | l2 | test.c:8:14:8:20 | ... / ... | test.c:12:8:12:9 | l2 | Division operation may silently underflow and produce zero, as the divisor $@. | test.c:8:14:8:20 | ... / ... | may be an infinite float value from division by zero |
89+
| test.c:13:8:13:9 | l3 | test.c:8:14:8:20 | ... / ... | test.c:13:8:13:9 | l3 | Division operation may silently underflow and produce zero, as the divisor $@. | test.c:8:14:8:20 | ... / ... | may be an infinite float value from division by zero |
90+
| test.c:18:8:18:9 | l2 | test.c:8:14:8:20 | ... / ... | test.c:18:3:18:9 | l2 | $@ casted to integer. | test.c:8:14:8:20 | ... / ... | Possibly infinite float value from division by zero |
91+
| test.c:19:8:19:9 | l3 | test.c:8:14:8:20 | ... / ... | test.c:19:3:19:9 | l3 | $@ casted to integer. | test.c:8:14:8:20 | ... / ... | Possibly infinite float value from division by zero |
92+
| test.c:27:19:27:20 | l2 | test.c:8:14:8:20 | ... / ... | test.c:27:19:27:20 | l2 | Division operation may silently underflow and produce zero, as the divisor $@. | test.c:8:14:8:20 | ... / ... | may be an infinite float value from division by zero |
93+
| test.c:28:19:28:20 | l3 | test.c:8:14:8:20 | ... / ... | test.c:28:19:28:20 | l3 | Division operation may silently underflow and produce zero, as the divisor $@. | test.c:8:14:8:20 | ... / ... | may be an infinite float value from division by zero |
94+
| test.c:38:8:38:9 | l7 | test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | $@ casted to integer. | test.c:31:14:32:15 | ... / ... | Possibly infinite float value from division by zero |
95+
| test.c:61:11:61:17 | ... / ... | test.c:61:5:61:18 | ... / ... | test.c:61:5:61:18 | ... / ... | $@ casted to integer. | test.c:61:11:61:17 | ... / ... | Possibly infinite float value from division by zero |
96+
| test.c:66:11:66:19 | ... / ... | test.c:66:5:66:20 | ... / ... | test.c:66:5:66:20 | ... / ... | $@ casted to integer. | test.c:66:11:66:19 | ... / ... | Possibly infinite float value from division by zero |
97+
| test.c:72:20:72:28 | ... / ... | test.c:72:14:72:29 | ... / ... | test.c:72:14:72:29 | ... / ... | $@ casted to integer. | test.c:72:20:72:28 | ... / ... | Possibly infinite float value from division by zero |
98+
| test.c:75:24:75:32 | ... / ... | test.c:75:18:75:33 | ... / ... | test.c:75:18:75:33 | ... / ... | $@ casted to integer. | test.c:75:24:75:32 | ... / ... | Possibly infinite float value from division by zero |
99+
| test.c:79:10:79:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:79:5:79:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
100+
| test.c:87:10:87:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:87:5:87:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
101+
| test.c:91:10:91:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:91:5:91:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
102+
| test.c:93:10:93:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:93:5:93:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
103+
| test.c:99:10:99:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:99:5:99:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
104+
| test.c:105:10:105:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:105:5:105:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
105+
| test.c:111:10:111:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:111:5:111:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
106+
| test.c:114:21:114:23 | l12 | test.c:77:15:77:21 | ... / ... | test.c:114:16:114:23 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
107+
| test.c:117:28:117:30 | l12 | test.c:77:15:77:21 | ... / ... | test.c:117:23:117:30 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
108+
| test.c:120:25:120:27 | l12 | test.c:77:15:77:21 | ... / ... | test.c:120:20:120:27 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
109+
| test.c:163:9:164:15 | ... / ... | test.c:163:3:164:16 | ... / ... | test.c:163:3:164:16 | ... / ... | $@ casted to integer. | test.c:163:9:164:15 | ... / ... | Possibly infinite float value from division by zero |
110+
| test.c:175:32:175:32 | p | test.c:189:51:189:59 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:189:6:189:24 | addInfThenCastToInt | Possibly infinite float value computed in function addInfThenCastToInt |
111+
| test.c:175:32:175:32 | p | test.c:193:13:194:15 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly infinite float value computed in function f2 |
112+
| test.c:175:32:175:32 | p | test.c:204:19:204:27 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly infinite float value computed in function f2 |
113+
| test.c:185:18:185:18 | p | test.c:200:25:200:33 | ... / ... | test.c:185:13:185:18 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly infinite float value computed in function f2 |

0 commit comments

Comments
 (0)