1
1
/**
2
- * @id c/misra/possible-misuse-of-undetected-na-n
2
+ * @id c/misra/possible-misuse-of-undetected-nan
3
3
* @name DIR-4-15: Evaluation of floating-point expressions shall not lead to the undetected generation of NaNs
4
4
* @description Evaluation of floating-point expressions shall not lead to the undetected generation
5
5
* of NaNs.
@@ -23,66 +23,14 @@ import semmle.code.cpp.dataflow.new.DataFlow
23
23
import semmle.code.cpp.dataflow.new.TaintTracking
24
24
import semmle.code.cpp.controlflow.Dominance
25
25
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 ) ) +
39
- " which is outside the domain of this function (-1.0...1.0)"
40
- or
41
- functionWithDomainError = getMathVariants ( [ "atan2" , "pow" ] ) and
42
- (
43
- exprMayEqualZero ( fc .getArgument ( 0 ) ) and
44
- exprMayEqualZero ( fc .getArgument ( 1 ) ) and
45
- description = "both arguments are equal to zero"
46
- )
47
- or
48
- functionWithDomainError = getMathVariants ( "pow" ) and
49
- (
50
- RestrictedRangeAnalysis:: upperBound ( fc .getArgument ( 0 ) ) < 0.0 and
51
- RestrictedRangeAnalysis:: upperBound ( fc .getArgument ( 1 ) ) < 0.0 and
52
- description = "both arguments are less than zero"
53
- )
54
- or
55
- functionWithDomainError = getMathVariants ( "acosh" ) and
56
- RestrictedRangeAnalysis:: upperBound ( fc .getArgument ( 0 ) ) < 1.0 and
57
- description = "argument is less than 1"
58
- or
59
- //pole error is the same as domain for logb and tgamma (but not ilogb - no pole error exists)
60
- functionWithDomainError = getMathVariants ( [ "ilogb" , "logb" , "tgamma" ] ) and
61
- exprMayEqualZero ( fc .getArgument ( 0 ) ) and
62
- description = "argument is equal to zero"
63
- or
64
- functionWithDomainError = getMathVariants ( [ "log" , "log10" , "log2" , "sqrt" ] ) and
65
- RestrictedRangeAnalysis:: upperBound ( fc .getArgument ( 0 ) ) < 0.0 and
66
- description = "argument is negative"
67
- or
68
- functionWithDomainError = getMathVariants ( "log1p" ) and
69
- RestrictedRangeAnalysis:: upperBound ( fc .getArgument ( 0 ) ) < - 1.0 and
70
- description = "argument is less than 1"
71
- or
72
- functionWithDomainError = getMathVariants ( "fmod" ) and
73
- exprMayEqualZero ( fc .getArgument ( 1 ) ) and
74
- description = "y is 0"
75
- )
76
- }
77
-
78
26
abstract class PotentiallyNaNExpr extends Expr {
79
27
abstract string getReason ( ) ;
80
28
}
81
29
82
30
class DomainErrorFunctionCall extends FunctionCall , PotentiallyNaNExpr {
83
31
string reason ;
84
32
85
- DomainErrorFunctionCall ( ) { hasDomainError ( this , reason ) }
33
+ DomainErrorFunctionCall ( ) { RestrictedDomainError :: hasDomainError ( this , reason ) }
86
34
87
35
override string getReason ( ) { result = reason }
88
36
}
@@ -116,8 +64,13 @@ class InvalidOperationExpr extends BinaryOperation, PotentiallyNaNExpr {
116
64
or
117
65
// 7.1.3: multiplication of zero by infinity
118
66
getOperator ( ) = "*" and
119
- exprMayEqualZero ( getAnOperand ( ) ) and
120
- exprMayEqualInfinity ( getAnOperand ( ) , _) 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
121
74
reason = "from multiplication of zero by infinity"
122
75
or
123
76
// 7.1.4: Division of zero by zero, or infinity by infinity
@@ -199,30 +152,25 @@ module InvalidNaNUsage implements DataFlow::ConfigSig {
199
152
200
153
class InvalidNaNUsage extends DataFlow:: Node {
201
154
string description ;
202
- string nanDescription ;
203
155
204
156
InvalidNaNUsage ( ) {
205
157
// Case 1: NaNs shall not be compared, except to themselves
206
158
exists ( ComparisonOperation cmp |
207
159
this .asExpr ( ) = cmp .getAnOperand ( ) and
208
160
not hashCons ( cmp .getLeftOperand ( ) ) = hashCons ( cmp .getRightOperand ( ) ) and
209
- description = "Comparison involving a $@, which always evaluates to false." and
210
- nanDescription = "possibly NaN float value"
161
+ description = "comparison, which would always evaluate to false."
211
162
)
212
163
or
213
164
// Case 2: NaNs and infinities shall not be cast to integers
214
165
exists ( Conversion c |
215
166
this .asExpr ( ) = c .getUnconverted ( ) and
216
167
c .getExpr ( ) .getType ( ) instanceof FloatingPointType and
217
168
c .getType ( ) instanceof IntegralType and
218
- description = "$@ casted to integer." and
219
- nanDescription = "Possibly NaN float value"
169
+ description = "a cast to integer."
220
170
)
221
171
}
222
172
223
173
string getDescription ( ) { result = description }
224
-
225
- string getNaNDescription ( ) { result = nanDescription }
226
174
}
227
175
228
176
module InvalidNaNFlow = DataFlow:: Global< InvalidNaNUsage > ;
@@ -231,7 +179,8 @@ import InvalidNaNFlow::PathGraph
231
179
232
180
from
233
181
Element elem , InvalidNaNFlow:: PathNode source , InvalidNaNFlow:: PathNode sink ,
234
- InvalidNaNUsage usage , Expr sourceExpr , string sourceString , Element extra , string extraString
182
+ InvalidNaNUsage usage , Expr sourceExpr , string sourceString , Function function ,
183
+ string computedInFunction
235
184
where
236
185
not InvalidNaNFlow:: PathGraph:: edges ( _, source , _, _) and
237
186
not InvalidNaNFlow:: PathGraph:: edges ( sink , _, _, _) and
@@ -240,18 +189,14 @@ where
240
189
elem = MacroUnwrapper< Expr > :: unwrapElement ( sink .getNode ( ) .asExpr ( ) ) and
241
190
usage = sink .getNode ( ) and
242
191
sourceExpr = source .getNode ( ) .asExpr ( ) and
243
- sourceString = " (" + source .getNode ( ) .asExpr ( ) .( PotentiallyNaNExpr ) .getReason ( ) + ")" and
192
+ sourceString = source .getNode ( ) .asExpr ( ) .( PotentiallyNaNExpr ) .getReason ( ) and
193
+ function = sourceExpr .getEnclosingFunction ( ) and
244
194
InvalidNaNFlow:: flow ( source .getNode ( ) , usage ) and
245
195
(
246
196
if not sourceExpr .getEnclosingFunction ( ) = usage .asExpr ( ) .getEnclosingFunction ( )
247
- then
248
- extraString =
249
- usage .getNaNDescription ( ) + sourceString + " computed in function " +
250
- sourceExpr .getEnclosingFunction ( ) .getName ( ) and
251
- extra = sourceExpr .getEnclosingFunction ( )
252
- else (
253
- extra = sourceExpr and
254
- extraString = usage .getNaNDescription ( ) + sourceString
255
- )
197
+ then computedInFunction = "computed in function $@ "
198
+ else computedInFunction = ""
256
199
)
257
- select elem , source , sink , usage .getDescription ( ) , extra , extraString
200
+ select elem , source , sink ,
201
+ "Possible NaN value $@ " + computedInFunction + "flows to " + usage .getDescription ( ) , sourceExpr ,
202
+ sourceString , function , function .getName ( )
0 commit comments