11/**
2- * @id c/misra/possible-misuse-of-undetected-na-n
2+ * @id c/misra/possible-misuse-of-undetected-nan
33 * @name DIR-4-15: Evaluation of floating-point expressions shall not lead to the undetected generation of NaNs
44 * @description Evaluation of floating-point expressions shall not lead to the undetected generation
55 * of NaNs.
@@ -23,66 +23,14 @@ import semmle.code.cpp.dataflow.new.DataFlow
2323import semmle.code.cpp.dataflow.new.TaintTracking
2424import 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 ) ) +
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-
7826abstract class PotentiallyNaNExpr extends Expr {
7927 abstract string getReason ( ) ;
8028}
8129
8230class DomainErrorFunctionCall extends FunctionCall , PotentiallyNaNExpr {
8331 string reason ;
8432
85- DomainErrorFunctionCall ( ) { hasDomainError ( this , reason ) }
33+ DomainErrorFunctionCall ( ) { RestrictedDomainError :: hasDomainError ( this , reason ) }
8634
8735 override string getReason ( ) { result = reason }
8836}
@@ -116,8 +64,13 @@ class InvalidOperationExpr extends BinaryOperation, PotentiallyNaNExpr {
11664 or
11765 // 7.1.3: multiplication of zero by infinity
11866 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
12174 reason = "from multiplication of zero by infinity"
12275 or
12376 // 7.1.4: Division of zero by zero, or infinity by infinity
@@ -199,30 +152,25 @@ module InvalidNaNUsage implements DataFlow::ConfigSig {
199152
200153class InvalidNaNUsage extends DataFlow:: Node {
201154 string description ;
202- string nanDescription ;
203155
204156 InvalidNaNUsage ( ) {
205157 // Case 1: NaNs shall not be compared, except to themselves
206158 exists ( ComparisonOperation cmp |
207159 this .asExpr ( ) = cmp .getAnOperand ( ) and
208160 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."
211162 )
212163 or
213164 // Case 2: NaNs and infinities shall not be cast to integers
214165 exists ( Conversion c |
215166 this .asExpr ( ) = c .getUnconverted ( ) and
216167 c .getExpr ( ) .getType ( ) instanceof FloatingPointType and
217168 c .getType ( ) instanceof IntegralType and
218- description = "$@ casted to integer." and
219- nanDescription = "Possibly NaN float value"
169+ description = "a cast to integer."
220170 )
221171 }
222172
223173 string getDescription ( ) { result = description }
224-
225- string getNaNDescription ( ) { result = nanDescription }
226174}
227175
228176module InvalidNaNFlow = DataFlow:: Global< InvalidNaNUsage > ;
@@ -231,7 +179,8 @@ import InvalidNaNFlow::PathGraph
231179
232180from
233181 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
235184where
236185 not InvalidNaNFlow:: PathGraph:: edges ( _, source , _, _) and
237186 not InvalidNaNFlow:: PathGraph:: edges ( sink , _, _, _) and
@@ -240,18 +189,14 @@ where
240189 elem = MacroUnwrapper< Expr > :: unwrapElement ( sink .getNode ( ) .asExpr ( ) ) and
241190 usage = sink .getNode ( ) and
242191 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
244194 InvalidNaNFlow:: flow ( source .getNode ( ) , usage ) and
245195 (
246196 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 = ""
256199 )
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