Skip to content

Implement DIR-4-15, detection of NaNs and Infinities #849

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
formatting fixes
  • Loading branch information
MichaelRFairhurst committed Feb 7, 2025
commit 99e92cff45d595f15a033dd7e3559109050e436c
14 changes: 8 additions & 6 deletions c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql
Original file line number Diff line number Diff line change
Expand Up @@ -133,13 +133,15 @@ where
(
if not sourceExpr.getEnclosingFunction() = usage.asExpr().getEnclosingFunction()
then
extraString = usage.getInfinityDescription() + " computed in function " + sourceExpr.getEnclosingFunction().getName()
and extra = sourceExpr.getEnclosingFunction()
extraString =
usage.getInfinityDescription() + " computed in function " +
sourceExpr.getEnclosingFunction().getName() and
extra = sourceExpr.getEnclosingFunction()
else (
extra = sourceExpr and
if sourceExpr instanceof DivExpr
then extraString = usage.getInfinityDescription() + " from division by zero"
else extraString = usage.getInfinityDescription()
if sourceExpr instanceof DivExpr
then extraString = usage.getInfinityDescription() + " from division by zero"
else extraString = usage.getInfinityDescription()
)
)
select elem, source, sink, usage.getDescription(), extra, extraString
select elem, source, sink, usage.getDescription(), extra, extraString
55 changes: 26 additions & 29 deletions c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,8 @@ predicate hasDomainError(FunctionCall fc, string description) {
) and
description =
"the argument has a range " + RestrictedRangeAnalysis::lowerBound(fc.getArgument(0)) + "..." +
RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) + " which is outside the domain of this function (-1.0...1.0)"
RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) +
" which is outside the domain of this function (-1.0...1.0)"
or
functionWithDomainError = getMathVariants(["atan2", "pow"]) and
(
Expand Down Expand Up @@ -81,9 +82,7 @@ abstract class PotentiallyNaNExpr extends Expr {
class DomainErrorFunctionCall extends FunctionCall, PotentiallyNaNExpr {
string reason;

DomainErrorFunctionCall() {
hasDomainError(this, reason)
}
DomainErrorFunctionCall() { hasDomainError(this, reason) }

override string getReason() { result = reason }
}
Expand Down Expand Up @@ -203,25 +202,22 @@ class InvalidNaNUsage extends DataFlow::Node {
string nanDescription;

InvalidNaNUsage() {
// Case 1: NaNs shall not be compared, except to themselves
exists(ComparisonOperation cmp |
this.asExpr() = cmp.getAnOperand() and
not hashCons(cmp.getLeftOperand()) = hashCons(cmp.getRightOperand()) and
description = "Comparison involving a $@, which always evaluates to false." and
nanDescription = "possibly NaN float value"
)
or
// Case 2: NaNs and infinities shall not be cast to integers
exists(Conversion c |
this.asExpr() = c.getUnconverted() and
c.getExpr().getType() instanceof FloatingPointType and
c.getType() instanceof IntegralType and
description = "$@ casted to integer." and
nanDescription = "Possibly NaN float value"
)
//or
//// Case 4: Functions shall not return NaNs or infinities
//exists(ReturnStmt ret | node.asExpr() = ret.getExpr())
// Case 1: NaNs shall not be compared, except to themselves
exists(ComparisonOperation cmp |
this.asExpr() = cmp.getAnOperand() and
not hashCons(cmp.getLeftOperand()) = hashCons(cmp.getRightOperand()) and
description = "Comparison involving a $@, which always evaluates to false." and
nanDescription = "possibly NaN float value"
)
or
// Case 2: NaNs and infinities shall not be cast to integers
exists(Conversion c |
this.asExpr() = c.getUnconverted() and
c.getExpr().getType() instanceof FloatingPointType and
c.getType() instanceof IntegralType and
description = "$@ casted to integer." and
nanDescription = "Possibly NaN float value"
)
}

string getDescription() { result = description }
Expand All @@ -244,17 +240,18 @@ where
elem = MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr()) and
usage = sink.getNode() and
sourceExpr = source.getNode().asExpr() and
sourceString =
" (" + source.getNode().asExpr().(PotentiallyNaNExpr).getReason() + ")" and
sourceString = " (" + source.getNode().asExpr().(PotentiallyNaNExpr).getReason() + ")" and
InvalidNaNFlow::flow(source.getNode(), usage) and
(
if not sourceExpr.getEnclosingFunction() = usage.asExpr().getEnclosingFunction()
then
extraString = usage.getNaNDescription() + sourceString + " computed in function " + sourceExpr.getEnclosingFunction().getName()
and extra = sourceExpr.getEnclosingFunction()
extraString =
usage.getNaNDescription() + sourceString + " computed in function " +
sourceExpr.getEnclosingFunction().getName() and
extra = sourceExpr.getEnclosingFunction()
else (
extra = sourceExpr and
extraString = usage.getNaNDescription() + sourceString
extraString = usage.getNaNDescription() + sourceString
)
)
select elem, source, sink, usage.getDescription(), extra, extraString
select elem, source, sink, usage.getDescription(), extra, extraString
Loading