Skip to content

Commit 59ebba0

Browse files
MichaelRFairhurstMichaelRFairhurst
committed
Support guards isinf(), isfinite(), isnan(), etc
1 parent 638c083 commit 59ebba0

File tree

7 files changed

+521
-72
lines changed

7 files changed

+521
-72
lines changed

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,18 @@ module InvalidInfinityUsage implements DataFlow::ConfigSig {
4444
exprMayEqualInfinity(node.asExpr(), _)
4545
}
4646

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+
or
55+
// Sinks are places where Infinity produce a finite value
56+
isSink(node)
57+
}
58+
4759
/**
4860
* An additional flow step to handle operations which propagate Infinity.
4961
*

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

Lines changed: 26 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,6 @@ class InvalidOperationExpr extends BinaryOperation {
8989
}
9090

9191
module InvalidNaNUsage implements DataFlow::ConfigSig {
92-
9392
/**
9493
* An expression which has non-NaN inputs and may produce a NaN output.
9594
*/
@@ -108,6 +107,15 @@ module InvalidNaNUsage implements DataFlow::ConfigSig {
108107
node.asExpr() instanceof InvalidOperationExpr
109108
}
110109

110+
predicate isBarrierOut(DataFlow::Node node) {
111+
guardedNotFPClass(node.asExpr(), TNaN())
112+
or
113+
exists(Expr e |
114+
e.getType() instanceof IntegralType and
115+
e = node.asConvertedExpr()
116+
)
117+
}
118+
111119
/**
112120
* Add an additional flow step to handle NaN propagation through floating point operations.
113121
*/
@@ -120,21 +128,24 @@ module InvalidNaNUsage implements DataFlow::ConfigSig {
120128
}
121129

122130
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
131+
not guardedNotFPClass(node.asExpr(), TNaN()) and
132+
(
133+
// Case 1: NaNs shall not be compared, except to themselves
134+
exists(ComparisonOperation cmp |
135+
node.asExpr() = cmp.getAnOperand() and
136+
not hashCons(cmp.getLeftOperand()) = hashCons(cmp.getRightOperand())
137+
)
138+
or
139+
// Case 2: NaNs and infinities shall not be cast to integers
140+
exists(Conversion c |
141+
node.asExpr() = c.getUnconverted() and
142+
c.getExpr().getType() instanceof FloatingPointType and
143+
c.getType() instanceof IntegralType
144+
)
145+
//or
146+
//// Case 4: Functions shall not return NaNs or infinities
147+
//exists(ReturnStmt ret | node.asExpr() = ret.getExpr())
134148
)
135-
//or
136-
//// Case 4: Functions shall not return NaNs or infinities
137-
//exists(ReturnStmt ret | node.asExpr() = ret.getExpr())
138149
}
139150
}
140151

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

Lines changed: 45 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
edges
22
| test.c:8:14:8:20 | ... / ... | test.c:8:14:8:20 | ... / ... | provenance | |
3+
| test.c:8:14:8:20 | ... / ... | test.c:9:14:9:16 | - ... | provenance | Config |
34
| test.c:8:14:8:20 | ... / ... | test.c:12:8:12:9 | l2 | provenance | |
45
| test.c:8:14:8:20 | ... / ... | test.c:18:3:18:9 | l2 | provenance | |
56
| test.c:8:14:8:20 | ... / ... | test.c:27:19:27:20 | l2 | provenance | |
@@ -9,8 +10,17 @@ edges
910
| test.c:9:14:9:16 | - ... | test.c:28:19:28:20 | l3 | provenance | |
1011
| test.c:31:14:32:15 | ... / ... | test.c:31:14:32:15 | ... / ... | provenance | |
1112
| test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | provenance | |
12-
| test.c:33:14:33:22 | ... / ... | test.c:33:14:33:22 | ... / ... | provenance | |
13-
| test.c:33:14:33:22 | ... / ... | test.c:39:3:39:9 | l8 | provenance | |
13+
| test.c:77:15:77:21 | ... / ... | test.c:77:15:77:21 | ... / ... | provenance | |
14+
| test.c:77:15:77:21 | ... / ... | test.c:79:5:79:12 | l12 | provenance | |
15+
| test.c:77:15:77:21 | ... / ... | test.c:87:5:87:12 | l12 | provenance | |
16+
| test.c:77:15:77:21 | ... / ... | test.c:91:5:91:12 | l12 | provenance | |
17+
| test.c:77:15:77:21 | ... / ... | test.c:93:5:93:12 | l12 | provenance | |
18+
| test.c:77:15:77:21 | ... / ... | test.c:99:5:99:12 | l12 | provenance | |
19+
| test.c:77:15:77:21 | ... / ... | test.c:105:5:105:12 | l12 | provenance | |
20+
| test.c:77:15:77:21 | ... / ... | test.c:111:5:111:12 | l12 | provenance | |
21+
| test.c:77:15:77:21 | ... / ... | test.c:114:16:114:23 | l12 | provenance | |
22+
| test.c:77:15:77:21 | ... / ... | test.c:117:23:117:30 | l12 | provenance | |
23+
| test.c:77:15:77:21 | ... / ... | test.c:120:20:120:27 | l12 | provenance | |
1424
nodes
1525
| test.c:8:14:8:20 | ... / ... | semmle.label | ... / ... |
1626
| test.c:8:14:8:20 | ... / ... | semmle.label | ... / ... |
@@ -24,25 +34,46 @@ nodes
2434
| test.c:28:19:28:20 | l3 | semmle.label | l3 |
2535
| test.c:31:14:32:15 | ... / ... | semmle.label | ... / ... |
2636
| test.c:31:14:32:15 | ... / ... | semmle.label | ... / ... |
27-
| test.c:33:14:33:22 | ... / ... | semmle.label | ... / ... |
28-
| test.c:33:14:33:22 | ... / ... | semmle.label | ... / ... |
2937
| test.c:38:3:38:9 | l7 | semmle.label | l7 |
30-
| test.c:39:3:39:9 | l8 | semmle.label | l8 |
31-
| test.c:61:5:61:19 | ... / ... | semmle.label | ... / ... |
32-
| test.c:66:5:66:21 | ... / ... | semmle.label | ... / ... |
33-
| test.c:72:14:72:30 | ... / ... | semmle.label | ... / ... |
34-
| test.c:75:18:75:34 | ... / ... | semmle.label | ... / ... |
38+
| test.c:61:5:61:18 | ... / ... | semmle.label | ... / ... |
39+
| test.c:66:5:66:20 | ... / ... | semmle.label | ... / ... |
40+
| test.c:72:14:72:29 | ... / ... | semmle.label | ... / ... |
41+
| test.c:75:18:75:33 | ... / ... | semmle.label | ... / ... |
42+
| test.c:77:15:77:21 | ... / ... | semmle.label | ... / ... |
43+
| test.c:77:15:77:21 | ... / ... | semmle.label | ... / ... |
44+
| test.c:79:5:79:12 | l12 | semmle.label | l12 |
45+
| test.c:87:5:87:12 | l12 | semmle.label | l12 |
46+
| test.c:91:5:91:12 | l12 | semmle.label | l12 |
47+
| test.c:93:5:93:12 | l12 | semmle.label | l12 |
48+
| test.c:99:5:99:12 | l12 | semmle.label | l12 |
49+
| test.c:105:5:105:12 | l12 | semmle.label | l12 |
50+
| test.c:111:5:111:12 | l12 | semmle.label | l12 |
51+
| test.c:114:16:114:23 | l12 | semmle.label | l12 |
52+
| test.c:117:23:117:30 | l12 | semmle.label | l12 |
53+
| test.c:120:20:120:27 | l12 | semmle.label | l12 |
3554
subpaths
3655
#select
3756
| 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 |
3858
| 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 |
3959
| 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 |
4061
| 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 |
4162
| 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 |
4264
| 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 |
4365
| 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 |
44-
| test.c:39:8:39:9 | l8 | test.c:33:14:33:22 | ... / ... | test.c:39:3:39:9 | l8 | Invalid usage of possible $@. | test.c:33:14:33:22 | ... / ... | infinity |
45-
| test.c:61:12:61:18 | ... / ... | test.c:61:5:61:19 | ... / ... | test.c:61:5:61:19 | ... / ... | Invalid usage of possible $@. | test.c:61:5:61:19 | ... / ... | infinity |
46-
| test.c:66:12:66:20 | ... / ... | test.c:66:5:66:21 | ... / ... | test.c:66:5:66:21 | ... / ... | Invalid usage of possible $@. | test.c:66:5:66:21 | ... / ... | infinity |
47-
| test.c:72:21:72:29 | ... / ... | test.c:72:14:72:30 | ... / ... | test.c:72:14:72:30 | ... / ... | Invalid usage of possible $@. | test.c:72:14:72:30 | ... / ... | infinity |
48-
| test.c:75:25:75:33 | ... / ... | test.c:75:18:75:34 | ... / ... | test.c:75:18:75:34 | ... / ... | Invalid usage of possible $@. | test.c:75:18:75:34 | ... / ... | 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 |

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

Lines changed: 35 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,15 @@ edges
1616
| test.c:33:14:33:22 | ... / ... | test.c:33:14:33:22 | ... / ... | provenance | |
1717
| test.c:33:14:33:22 | ... / ... | test.c:39:3:39:9 | l8 | provenance | |
1818
| test.c:33:14:33:22 | ... / ... | test.c:54:3:54:4 | l8 | provenance | |
19+
| test.c:122:15:122:21 | ... / ... | test.c:122:15:122:21 | ... / ... | provenance | |
20+
| test.c:122:15:122:21 | ... / ... | test.c:126:5:126:12 | l13 | provenance | |
21+
| test.c:122:15:122:21 | ... / ... | test.c:132:5:132:12 | l13 | provenance | |
22+
| test.c:122:15:122:21 | ... / ... | test.c:138:5:138:12 | l13 | provenance | |
23+
| test.c:122:15:122:21 | ... / ... | test.c:144:5:144:12 | l13 | provenance | |
24+
| test.c:122:15:122:21 | ... / ... | test.c:148:5:148:12 | l13 | provenance | |
25+
| test.c:122:15:122:21 | ... / ... | test.c:154:20:154:27 | l13 | provenance | |
26+
| test.c:122:15:122:21 | ... / ... | test.c:156:23:156:30 | l13 | provenance | |
27+
| test.c:122:15:122:21 | ... / ... | test.c:157:16:157:23 | l13 | provenance | |
1928
nodes
2029
| test.c:27:14:27:20 | ... / ... | semmle.label | ... / ... |
2130
| test.c:27:14:27:20 | ... / ... | semmle.label | ... / ... |
@@ -38,10 +47,20 @@ nodes
3847
| test.c:52:3:52:4 | l6 | semmle.label | l6 |
3948
| test.c:53:3:53:4 | l7 | semmle.label | l7 |
4049
| test.c:54:3:54:4 | l8 | semmle.label | l8 |
41-
| test.c:61:5:61:19 | ... / ... | semmle.label | ... / ... |
42-
| test.c:66:5:66:21 | ... / ... | semmle.label | ... / ... |
43-
| test.c:72:14:72:30 | ... / ... | semmle.label | ... / ... |
44-
| test.c:75:18:75:34 | ... / ... | semmle.label | ... / ... |
50+
| test.c:61:5:61:18 | ... / ... | semmle.label | ... / ... |
51+
| test.c:66:5:66:20 | ... / ... | semmle.label | ... / ... |
52+
| test.c:72:14:72:29 | ... / ... | semmle.label | ... / ... |
53+
| test.c:75:18:75:33 | ... / ... | semmle.label | ... / ... |
54+
| test.c:122:15:122:21 | ... / ... | semmle.label | ... / ... |
55+
| test.c:122:15:122:21 | ... / ... | semmle.label | ... / ... |
56+
| test.c:126:5:126:12 | l13 | semmle.label | l13 |
57+
| test.c:132:5:132:12 | l13 | semmle.label | l13 |
58+
| test.c:138:5:138:12 | l13 | semmle.label | l13 |
59+
| test.c:144:5:144:12 | l13 | semmle.label | l13 |
60+
| test.c:148:5:148:12 | l13 | semmle.label | l13 |
61+
| test.c:154:20:154:27 | l13 | semmle.label | l13 |
62+
| test.c:156:23:156:30 | l13 | semmle.label | l13 |
63+
| test.c:157:16:157:23 | l13 | semmle.label | l13 |
4564
subpaths
4665
#select
4766
| test.c:36:8:36:9 | l5 | test.c:27:14:27:20 | ... / ... | test.c:36:3:36:9 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity |
@@ -57,7 +76,15 @@ subpaths
5776
| test.c:52:3:52:4 | l6 | test.c:28:14:28:20 | ... / ... | test.c:52:3:52:4 | l6 | Invalid usage of possible $@. | test.c:28:14:28:20 | ... / ... | NaN resulting from possible division of infinity by infinity |
5877
| test.c:53:3:53:4 | l7 | test.c:31:14:32:15 | ... / ... | test.c:53:3:53:4 | l7 | Invalid usage of possible $@. | test.c:31:14:32:15 | ... / ... | NaN resulting from possible division of zero by zero |
5978
| test.c:54:3:54:4 | l8 | test.c:33:14:33:22 | ... / ... | test.c:54:3:54:4 | l8 | Invalid usage of possible $@. | test.c:33:14:33:22 | ... / ... | NaN resulting from possible division of zero by zero |
60-
| test.c:61:12:61:18 | ... / ... | test.c:61:5:61:19 | ... / ... | test.c:61:5:61:19 | ... / ... | Invalid usage of possible $@. | test.c:61:5:61:19 | ... / ... | NaN resulting from possible division of zero by zero |
61-
| test.c:66:12:66:20 | ... / ... | test.c:66:5:66:21 | ... / ... | test.c:66:5:66:21 | ... / ... | Invalid usage of possible $@. | test.c:66:5:66:21 | ... / ... | NaN resulting from possible division of zero by zero |
62-
| test.c:72:21:72:29 | ... / ... | test.c:72:14:72:30 | ... / ... | test.c:72:14:72:30 | ... / ... | Invalid usage of possible $@. | test.c:72:14:72:30 | ... / ... | NaN resulting from possible division of zero by zero |
63-
| test.c:75:25:75:33 | ... / ... | test.c:75:18:75:34 | ... / ... | test.c:75:18:75:34 | ... / ... | Invalid usage of possible $@. | test.c:75:18:75:34 | ... / ... | NaN resulting from possible division of zero by zero |
79+
| 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 | ... / ... | NaN resulting from possible division of zero by zero |
80+
| 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 | ... / ... | NaN resulting from possible division of zero by zero |
81+
| 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 | ... / ... | NaN resulting from possible division of zero by zero |
82+
| 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 | ... / ... | NaN resulting from possible division of zero by zero |
83+
| test.c:126:10:126:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:126:5:126:12 | l13 | Invalid usage of possible $@. | test.c:122:15:122:21 | ... / ... | NaN resulting from possible division of zero by zero |
84+
| test.c:132:10:132:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:132:5:132:12 | l13 | Invalid usage of possible $@. | test.c:122:15:122:21 | ... / ... | NaN resulting from possible division of zero by zero |
85+
| test.c:138:10:138:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:138:5:138:12 | l13 | Invalid usage of possible $@. | test.c:122:15:122:21 | ... / ... | NaN resulting from possible division of zero by zero |
86+
| test.c:144:10:144:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:144:5:144:12 | l13 | Invalid usage of possible $@. | test.c:122:15:122:21 | ... / ... | NaN resulting from possible division of zero by zero |
87+
| test.c:148:10:148:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:148:5:148:12 | l13 | Invalid usage of possible $@. | test.c:122:15:122:21 | ... / ... | NaN resulting from possible division of zero by zero |
88+
| test.c:154:25:154:27 | l13 | test.c:122:15:122:21 | ... / ... | test.c:154:20:154:27 | l13 | Invalid usage of possible $@. | test.c:122:15:122:21 | ... / ... | NaN resulting from possible division of zero by zero |
89+
| test.c:156:28:156:30 | l13 | test.c:122:15:122:21 | ... / ... | test.c:156:23:156:30 | l13 | Invalid usage of possible $@. | test.c:122:15:122:21 | ... / ... | NaN resulting from possible division of zero by zero |
90+
| test.c:157:21:157:23 | l13 | test.c:122:15:122:21 | ... / ... | test.c:157:16:157:23 | l13 | Invalid usage of possible $@. | test.c:122:15:122:21 | ... / ... | NaN resulting from possible division of zero by zero |

0 commit comments

Comments
 (0)