Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up
Appearance settings

Commitd34b85c

Browse files
Merge pull request#849 from github/michaelrfairhurst/implement-floatingtype-package
Implement DIR-4-15, detection of NaNs and Infinities
2 parents8f65892 +8885ee1 commitd34b85c

14 files changed

+3548
-52
lines changed
Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
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 medium
8+
* @problem.severity warning
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 InvalidInfinityUsageimplements 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+
predicateisSource(DataFlow::Nodenode){
32+
potentialSource(node)and
33+
notexists(DataFlow::Nodeprior|
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+
additionalpredicatepotentialSource(DataFlow::Nodenode){
43+
node.asExpr()instanceofOperationand
44+
exprMayEqualInfinity(node.asExpr(), _)
45+
}
46+
47+
predicateisBarrierOut(DataFlow::Nodenode){
48+
guardedNotFPClass(node.asExpr(),TInfinite())
49+
or
50+
exists(Expre|
51+
e.getType()instanceofIntegralTypeand
52+
e=node.asConvertedExpr()
53+
)
54+
}
55+
56+
/**
57+
* An additional flow step to handle operations which propagate Infinity.
58+
*
59+
* This double checks that an Infinity may propagate by checking the `RestrictedRangeAnalysis`
60+
* value estimate. This is conservative, since `RestrictedRangeAnalysis` is performed locally
61+
* in scope with unanalyzable values in a finite range. However, this conservative approach
62+
* leverages analysis of guards and other local conditions to avoid false positives.
63+
*/
64+
predicateisAdditionalFlowStep(DataFlow::Nodesource, DataFlow::Nodesink){
65+
exists(Operationo|
66+
o.getAnOperand()=source.asExpr()and
67+
o=sink.asExpr()and
68+
potentialSource(sink)
69+
)
70+
}
71+
72+
predicateisSink(DataFlow::Nodenode){
73+
nodeinstanceofInvalidInfinityUsageand
74+
(
75+
// Require that range analysis finds this value potentially infinite, to avoid false positives
76+
// in the presence of guards. This may induce false negatives.
77+
exprMayEqualInfinity(node.asExpr(), _)
78+
or
79+
// Unanalyzable expressions are not checked against range analysis, which assumes a finite
80+
// range.
81+
not RestrictedRangeAnalysis::canBoundExpr(node.asExpr())
82+
or
83+
node.asExpr().(VariableAccess).getTarget()instanceofParameter
84+
)
85+
}
86+
}
87+
88+
classInvalidInfinityUsageextends DataFlow::Node{
89+
stringdescription;
90+
91+
InvalidInfinityUsage(){
92+
// Case 2: NaNs and infinities shall not be cast to integers
93+
exists(Conversionc|
94+
asExpr()=c.getUnconverted()and
95+
c.getExpr().getType()instanceofFloatingPointTypeand
96+
c.getType()instanceofIntegralTypeand
97+
description="cast to integer."
98+
)
99+
or
100+
// Case 3: Infinities shall not underflow or otherwise produce finite values
101+
exists(BinaryOperationop|
102+
asExpr()=op.getRightOperand()and
103+
op.getOperator()="/"and
104+
description="divisor, which would silently underflow and produce zero."
105+
)
106+
}
107+
108+
stringgetDescription(){result=description}
109+
}
110+
111+
module InvalidInfinityFlow= DataFlow::Global<InvalidInfinityUsage>;
112+
113+
import InvalidInfinityFlow::PathGraph
114+
115+
from
116+
Elementelem, InvalidInfinityFlow::PathNodesource, InvalidInfinityFlow::PathNodesink,
117+
InvalidInfinityUsageusage,ExprsourceExpr,stringsourceString,Functionfunction,
118+
stringcomputedInFunction
119+
where
120+
elem= MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr())and
121+
not InvalidInfinityFlow::PathGraph::edges(_,source, _, _)and
122+
not InvalidInfinityFlow::PathGraph::edges(sink, _, _, _)and
123+
notisExcluded(elem, FloatingTypes2Package::possibleMisuseOfUndetectedInfinityQuery())and
124+
notsourceExpr.isFromTemplateInstantiation(_)and
125+
notusage.asExpr().isFromTemplateInstantiation(_)and
126+
usage=sink.getNode()and
127+
sourceExpr=source.getNode().asExpr()and
128+
function=sourceExpr.getEnclosingFunction()and
129+
InvalidInfinityFlow::flow(source.getNode(),usage)and
130+
(
131+
ifnotsourceExpr.getEnclosingFunction()=usage.asExpr().getEnclosingFunction()
132+
thencomputedInFunction="computed in function $@ "
133+
elsecomputedInFunction=""
134+
)and
135+
(
136+
ifsourceExprinstanceofDivExpr
137+
thensourceString="from division by zero"
138+
elsesourceString=sourceExpr.toString()
139+
)
140+
selectelem,source,sink,
141+
"Possibly infinite float value $@ "+computedInFunction+"flows to "+usage.getDescription(),
142+
sourceExpr,sourceString,function,function.getName()
Lines changed: 202 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,202 @@
1+
/**
2+
* @id c/misra/possible-misuse-of-undetected-nan
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 low
8+
* @problem.severity warning
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+
abstractclassPotentiallyNaNExprextendsExpr{
27+
abstractstringgetReason();
28+
}
29+
30+
classDomainErrorFunctionCallextendsFunctionCall,PotentiallyNaNExpr{
31+
stringreason;
32+
33+
DomainErrorFunctionCall(){ RestrictedDomainError::hasDomainError(this,reason)}
34+
35+
overridestringgetReason(){result=reason}
36+
}
37+
38+
// IEEE 754-1985 Section 7.1 invalid operations
39+
classInvalidOperationExprextendsBinaryOperation,PotentiallyNaNExpr{
40+
stringreason;
41+
42+
InvalidOperationExpr(){
43+
// Usual arithmetic conversions in both languages mean that if either operand is a floating
44+
// type, the other one is converted to a floating type as well.
45+
getAnOperand().getFullyConverted().getType()instanceofFloatingPointTypeand
46+
(
47+
// 7.1.1 propagates signaling NaNs, we rely on flow analysis and/or assume quiet NaNs, so we
48+
// intentionally do not cover this case.
49+
// 7.1.2: magnitude subtraction of infinities, such as +Inf + -Inf
50+
getOperator()="+"and
51+
exists(Booleansign|
52+
exprMayEqualInfinity(getLeftOperand(),sign)and
53+
exprMayEqualInfinity(getRightOperand(),sign.booleanNot())
54+
)and
55+
reason="from addition of infinity and negative infinity"
56+
or
57+
// 7.1.2 continued
58+
getOperator()="-"and
59+
exists(Booleansign|
60+
exprMayEqualInfinity(getLeftOperand(),sign)and
61+
exprMayEqualInfinity(getRightOperand(),sign)
62+
)and
63+
reason="from subtraction of an infinity from itself"
64+
or
65+
// 7.1.3: multiplication of zero by infinity
66+
getOperator()="*"and
67+
exists(ExprzeroOp,ExprinfinityOp|
68+
zeroOp=getAnOperand()and
69+
infinityOp=getAnOperand()and
70+
notzeroOp=infinityOpand
71+
exprMayEqualZero(zeroOp)and
72+
exprMayEqualInfinity(infinityOp, _)
73+
)and
74+
reason="from multiplication of zero by infinity"
75+
or
76+
// 7.1.4: Division of zero by zero, or infinity by infinity
77+
getOperator()="/"and
78+
exprMayEqualZero(getLeftOperand())and
79+
exprMayEqualZero(getRightOperand())and
80+
reason="from division of zero by zero"
81+
or
82+
// 7.1.4 continued
83+
getOperator()="/"and
84+
exprMayEqualInfinity(getLeftOperand(), _)and
85+
exprMayEqualInfinity(getRightOperand(), _)and
86+
reason="from division of infinity by infinity"
87+
or
88+
// 7.1.5: x % y where y is zero or x is infinite
89+
getOperator()="%"and
90+
exprMayEqualInfinity(getLeftOperand(), _)and
91+
reason="from modulus of infinity"
92+
or
93+
// 7.1.5 continued
94+
getOperator()="%"and
95+
exprMayEqualZero(getRightOperand())and
96+
reason="from modulus by zero"
97+
// 7.1.6 handles the sqrt function, not covered here.
98+
// 7.1.7 declares exceptions during invalid conversions, which we catch as sinks in our flow
99+
// analysis.
100+
// 7.1.8 declares exceptions for unordered comparisons, which we catch as sinks in our flow
101+
// analysis.
102+
)
103+
}
104+
105+
overridestringgetReason(){result=reason}
106+
}
107+
108+
module InvalidNaNUsageimplements DataFlow::ConfigSig{
109+
/**
110+
* An expression which has non-NaN inputs and may produce a NaN output.
111+
*/
112+
predicateisSource(DataFlow::Nodenode){
113+
potentialSource(node)and
114+
notexists(DataFlow::Nodeprior|
115+
isAdditionalFlowStep(prior,node)and
116+
potentialSource(prior)
117+
)
118+
}
119+
120+
/**
121+
* An expression which may produce a NaN output.
122+
*/
123+
additionalpredicatepotentialSource(DataFlow::Nodenode){
124+
node.asExpr()instanceofPotentiallyNaNExpr
125+
}
126+
127+
predicateisBarrierOut(DataFlow::Nodenode){
128+
guardedNotFPClass(node.asExpr(),TNaN())
129+
or
130+
exists(Expre|
131+
e.getType()instanceofIntegralTypeand
132+
e=node.asConvertedExpr()
133+
)
134+
}
135+
136+
/**
137+
* Add an additional flow step to handle NaN propagation through floating point operations.
138+
*/
139+
predicateisAdditionalFlowStep(DataFlow::Nodesource, DataFlow::Nodesink){
140+
exists(Operationo|
141+
o.getAnOperand()=source.asExpr()and
142+
o=sink.asExpr()and
143+
o.getType()instanceofFloatingPointType
144+
)
145+
}
146+
147+
predicateisSink(DataFlow::Nodenode){
148+
notguardedNotFPClass(node.asExpr(),TNaN())and
149+
nodeinstanceofInvalidNaNUsage
150+
}
151+
}
152+
153+
classInvalidNaNUsageextends DataFlow::Node{
154+
stringdescription;
155+
156+
InvalidNaNUsage(){
157+
// Case 1: NaNs shall not be compared, except to themselves
158+
exists(ComparisonOperationcmp|
159+
this.asExpr()=cmp.getAnOperand()and
160+
nothashCons(cmp.getLeftOperand())=hashCons(cmp.getRightOperand())and
161+
description="comparison, which would always evaluate to false."
162+
)
163+
or
164+
// Case 2: NaNs and infinities shall not be cast to integers
165+
exists(Conversionc|
166+
this.asExpr()=c.getUnconverted()and
167+
c.getExpr().getType()instanceofFloatingPointTypeand
168+
c.getType()instanceofIntegralTypeand
169+
description="a cast to integer."
170+
)
171+
}
172+
173+
stringgetDescription(){result=description}
174+
}
175+
176+
module InvalidNaNFlow= DataFlow::Global<InvalidNaNUsage>;
177+
178+
import InvalidNaNFlow::PathGraph
179+
180+
from
181+
Elementelem, InvalidNaNFlow::PathNodesource, InvalidNaNFlow::PathNodesink,
182+
InvalidNaNUsageusage,ExprsourceExpr,stringsourceString,Functionfunction,
183+
stringcomputedInFunction
184+
where
185+
not InvalidNaNFlow::PathGraph::edges(_,source, _, _)and
186+
not InvalidNaNFlow::PathGraph::edges(sink, _, _, _)and
187+
notsourceExpr.isFromTemplateInstantiation(_)and
188+
notusage.asExpr().isFromTemplateInstantiation(_)and
189+
elem= MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr())and
190+
usage=sink.getNode()and
191+
sourceExpr=source.getNode().asExpr()and
192+
sourceString=source.getNode().asExpr().(PotentiallyNaNExpr).getReason()and
193+
function=sourceExpr.getEnclosingFunction()and
194+
InvalidNaNFlow::flow(source.getNode(),usage)and
195+
(
196+
ifnotsourceExpr.getEnclosingFunction()=usage.asExpr().getEnclosingFunction()
197+
thencomputedInFunction="computed in function $@ "
198+
elsecomputedInFunction=""
199+
)
200+
selectelem,source,sink,
201+
"Possible NaN value $@ "+computedInFunction+"flows to "+usage.getDescription(),sourceExpr,
202+
sourceString,function,function.getName()

0 commit comments

Comments
 (0)
[8]ページ先頭
©2009-2025 Movatter.jp