From 638c083b3b55c790a3b588d9bc70ba02a0ced449 Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Tue, 29 Oct 2024 14:48:44 -0700 Subject: [PATCH 1/9] save work for draft PR --- .../PossibleMisuseOfUndetectedInfinity.ql | 104 + .../DIR-4-15/PossibleMisuseOfUndetectedNaN.ql | 157 ++ .../PossibleUndetectedNaNorInfinity.ql | 223 ++ ...ossibleMisuseOfUndetectedInfinity.expected | 48 + .../PossibleMisuseOfUndetectedInfinity.qlref | 1 + .../PossibleMisuseOfUndetectedNaN.expected | 63 + .../PossibleMisuseOfUndetectedNaN.qlref | 1 + .../PossibleUndetectedNaNorInfinity.expected | 1 + .../PossibleUndetectedNaNorInfinity.qlref | 1 + c/misra/test/rules/DIR-4-15/test.c | 76 + .../src/codingstandards/cpp/FloatingPoint.qll | 61 + .../cpp/RestrictedRangeAnalysis.qll | 1903 +++++++++++++++++ .../cpp/SimpleRangeAnalysisCustomizations.qll | 39 + .../cpp/exclusions/c/FloatingTypes2.qll | 44 + .../cpp/exclusions/c/RuleMetadata.qll | 3 + rule_packages/c/FloatingTypes2.json | 36 + 16 files changed, 2761 insertions(+) create mode 100644 c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql create mode 100644 c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql create mode 100644 c/misra/src/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.ql create mode 100644 c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected create mode 100644 c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.qlref create mode 100644 c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected create mode 100644 c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.qlref create mode 100644 c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.expected create mode 100644 c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.qlref create mode 100644 c/misra/test/rules/DIR-4-15/test.c create mode 100644 cpp/common/src/codingstandards/cpp/FloatingPoint.qll create mode 100644 cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll create mode 100644 cpp/common/src/codingstandards/cpp/exclusions/c/FloatingTypes2.qll create mode 100644 rule_packages/c/FloatingTypes2.json diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql new file mode 100644 index 0000000000..84a3fbfd3c --- /dev/null +++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql @@ -0,0 +1,104 @@ +/** + * @id c/misra/possible-misuse-of-undetected-infinity + * @name DIR-4-15: Evaluation of floating-point expressions shall not lead to the undetected generation of infinities + * @description Evaluation of floating-point expressions shall not lead to the undetected generation + * of infinities. + * @kind path-problem + * @precision high + * @problem.severity error + * @tags external/misra/id/dir-4-15 + * correctness + * external/misra/c/2012/amendment3 + * external/misra/obligation/required + */ + +import cpp +import codeql.util.Boolean +import codingstandards.c.misra +import codingstandards.cpp.RestrictedRangeAnalysis +import codingstandards.cpp.FloatingPoint +import codingstandards.cpp.AlertReporting +import semmle.code.cpp.controlflow.Guards +import semmle.code.cpp.dataflow.new.DataFlow +import semmle.code.cpp.dataflow.new.TaintTracking +import semmle.code.cpp.controlflow.Dominance + +module InvalidInfinityUsage implements DataFlow::ConfigSig { + /** + * An operation which does not have Infinity as an input, but may produce Infinity, according + * to the `RestrictedRangeAnalysis` module. + */ + predicate isSource(DataFlow::Node node) { + potentialSource(node) and + not exists(DataFlow::Node prior | + isAdditionalFlowStep(prior, node) and + potentialSource(prior) + ) + } + + /** + * An operation which may produce Infinity acconding to the `RestrictedRangeAnalysis` module. + */ + additional predicate potentialSource(DataFlow::Node node) { + node.asExpr() instanceof Operation and + exprMayEqualInfinity(node.asExpr(), _) + } + + /** + * An additional flow step to handle operations which propagate Infinity. + * + * This double checks that an Infinity may propagate by checking the `RestrictedRangeAnalysis` + * value estimate. This is conservative, since `RestrictedRangeAnalysis` is performed locally + * in scope with unanalyzable values in a finite range. However, this conservative approach + * leverages analysis of guards and other local conditions to avoid false positives. + */ + predicate isAdditionalFlowStep(DataFlow::Node source, DataFlow::Node sink) { + exists(Operation o | + o.getAnOperand() = source.asExpr() and + o = sink.asExpr() and + potentialSource(sink) + ) + } + + predicate isSink(DataFlow::Node node) { + ( + // Require that range analysis finds this value potentially infinite, to avoid false positives + // in the presence of guards. This may induce false negatives. + exprMayEqualInfinity(node.asExpr(), _) or + // Unanalyzable expressions are not checked against range analysis, which assumes a finite + // range. + not RestrictedRangeAnalysis::analyzableExpr(node.asExpr()) + ) and + ( + // Case 2: NaNs and infinities shall not be cast to integers + exists(Conversion c | + node.asExpr() = c.getUnconverted() and + c.getExpr().getType() instanceof FloatingPointType and + c.getType() instanceof IntegralType + ) + or + // Case 3: Infinities shall not underflow or otherwise produce finite values + exists(BinaryOperation op | + node.asExpr() = op.getRightOperand() and + op.getOperator() = ["/", "%"] + ) + ) + } +} + +module InvalidInfinityFlow = DataFlow::Global; + +import InvalidInfinityFlow::PathGraph + +from + Element elem, InvalidInfinityFlow::PathNode source, InvalidInfinityFlow::PathNode sink, + string msg, string sourceString +where + elem = MacroUnwrapper::unwrapElement(sink.getNode().asExpr()) and + not isExcluded(elem, FloatingTypes2Package::possibleMisuseOfUndetectedInfinityQuery()) and + ( + InvalidInfinityFlow::flow(source.getNode(), sink.getNode()) and + msg = "Invalid usage of possible $@." and + sourceString = "infinity" + ) +select elem, source, sink, msg, source, sourceString diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql new file mode 100644 index 0000000000..6962a1c36d --- /dev/null +++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql @@ -0,0 +1,157 @@ +/** + * @id c/misra/possible-misuse-of-undetected-na-n + * @name DIR-4-15: Evaluation of floating-point expressions shall not lead to the undetected generation of NaNs + * @description Evaluation of floating-point expressions shall not lead to the undetected generation + * of NaNs. + * @kind path-problem + * @precision high + * @problem.severity error + * @tags external/misra/id/dir-4-15 + * correctness + * external/misra/c/2012/amendment3 + * external/misra/obligation/required + */ + +import cpp +import codeql.util.Boolean +import codingstandards.c.misra +import codingstandards.cpp.RestrictedRangeAnalysis +import codingstandards.cpp.FloatingPoint +import codingstandards.cpp.AlertReporting +import semmle.code.cpp.controlflow.Guards +import semmle.code.cpp.dataflow.new.DataFlow +import semmle.code.cpp.dataflow.new.TaintTracking +import semmle.code.cpp.controlflow.Dominance + +// IEEE 754-1985 Section 7.1 invalid operations +class InvalidOperationExpr extends BinaryOperation { + string reason; + + InvalidOperationExpr() { + // Usual arithmetic conversions in both languages mean that if either operand is a floating + // type, the other one is converted to a floating type as well. + getAnOperand().getFullyConverted().getType() instanceof FloatingPointType and + ( + // 7.1.1 propagates signaling NaNs, we rely on flow analysis and/or assume quiet NaNs, so we + // intentionally do not cover this case. + // 7.1.2: magnitude subtraction of infinities, such as +Inf + -Inf + getOperator() = "+" and + exists(Boolean sign | + exprMayEqualInfinity(getLeftOperand(), sign) and + exprMayEqualInfinity(getRightOperand(), sign.booleanNot()) + ) and + reason = "possible addition of infinity and negative infinity" + or + // 7.1.2 continued + getOperator() = "-" and + exists(Boolean sign | + exprMayEqualInfinity(getLeftOperand(), sign) and + exprMayEqualInfinity(getRightOperand(), sign) + ) and + reason = "possible subtraction of an infinity from itself" + or + // 7.1.3: multiplication of zero by infinity + getOperator() = "*" and + exprMayEqualZero(getAnOperand()) and + exprMayEqualInfinity(getAnOperand(), _) and + reason = "possible multiplication of zero by infinity" + or + // 7.1.4: Division of zero by zero, or infinity by infinity + getOperator() = "/" and + exprMayEqualZero(getLeftOperand()) and + exprMayEqualZero(getRightOperand()) and + reason = "possible division of zero by zero" + or + // 7.1.4 continued + getOperator() = "/" and + exprMayEqualInfinity(getLeftOperand(), _) and + exprMayEqualInfinity(getRightOperand(), _) and + reason = "possible division of infinity by infinity" + or + // 7.1.5: x % y where y is zero or x is infinite + getOperator() = "%" and + exprMayEqualInfinity(getLeftOperand(), _) and + reason = "possible modulus of infinity" + or + // 7.1.5 continued + getOperator() = "%" and + exprMayEqualZero(getRightOperand()) and + reason = "possible modulus by zero" + // 7.1.6 handles the sqrt function, not covered here. + // 7.1.7 declares exceptions during invalid conversions, which we catch as sinks in our flow + // analysis. + // 7.1.8 declares exceptions for unordered comparisons, which we catch as sinks in our flow + // analysis. + ) + } + + string getReason() { result = reason } +} + +module InvalidNaNUsage implements DataFlow::ConfigSig { + + /** + * An expression which has non-NaN inputs and may produce a NaN output. + */ + predicate isSource(DataFlow::Node node) { + potentialSource(node) and + not exists(DataFlow::Node prior | + isAdditionalFlowStep(prior, node) and + potentialSource(prior) + ) + } + + /** + * An expression which may produce a NaN output. + */ + additional predicate potentialSource(DataFlow::Node node) { + node.asExpr() instanceof InvalidOperationExpr + } + + /** + * Add an additional flow step to handle NaN propagation through floating point operations. + */ + predicate isAdditionalFlowStep(DataFlow::Node source, DataFlow::Node sink) { + exists(Operation o | + o.getAnOperand() = source.asExpr() and + o = sink.asExpr() and + o.getType() instanceof FloatingPointType + ) + } + + predicate isSink(DataFlow::Node node) { + // Case 1: NaNs shall not be compared, except to themselves + exists(ComparisonOperation cmp | + node.asExpr() = cmp.getAnOperand() and + not hashCons(cmp.getLeftOperand()) = hashCons(cmp.getRightOperand()) + ) + or + // Case 2: NaNs and infinities shall not be cast to integers + exists(Conversion c | + node.asExpr() = c.getUnconverted() and + c.getExpr().getType() instanceof FloatingPointType and + c.getType() instanceof IntegralType + ) + //or + //// Case 4: Functions shall not return NaNs or infinities + //exists(ReturnStmt ret | node.asExpr() = ret.getExpr()) + } +} + +module InvalidNaNFlow = DataFlow::Global; + +import InvalidNaNFlow::PathGraph + +from + Element elem, InvalidNaNFlow::PathNode source, InvalidNaNFlow::PathNode sink, string msg, + string sourceString +where + elem = MacroUnwrapper::unwrapElement(sink.getNode().asExpr()) and + not isExcluded(elem, FloatingTypes2Package::possibleMisuseOfUndetectedNaNQuery()) and + ( + InvalidNaNFlow::flow(source.getNode(), sink.getNode()) and + msg = "Invalid usage of possible $@." and + sourceString = + "NaN resulting from " + source.getNode().asExpr().(InvalidOperationExpr).getReason() + ) +select elem, source, sink, msg, source, sourceString diff --git a/c/misra/src/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.ql b/c/misra/src/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.ql new file mode 100644 index 0000000000..94888a95e6 --- /dev/null +++ b/c/misra/src/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.ql @@ -0,0 +1,223 @@ +/** + * @id c/misra/possible-undetected-na-nor-infinity + * @name DIR-4-15: Evaluation of floating-point expressions shall not lead to the undetected generation of infinities + * @description Evaluation of floating-point expressions shall not lead to the undetected generation + * of infinities and NaNs. + * @kind path-problem + * @precision high + * @problem.severity error + * @tags external/misra/id/dir-4-15 + * correctness + * external/misra/c/2012/amendment3 + * external/misra/obligation/required + */ + +import cpp +import codeql.util.Boolean +import codingstandards.c.misra +import codingstandards.cpp.RestrictedRangeAnalysis +import codingstandards.cpp.FloatingPoint +import codingstandards.cpp.AlertReporting +import semmle.code.cpp.controlflow.Guards +import semmle.code.cpp.dataflow.new.DataFlow +import semmle.code.cpp.dataflow.new.TaintTracking +import semmle.code.cpp.controlflow.Dominance + +class CantHandleInfinityFunction extends Function { + CantHandleInfinityFunction() { not hasDefinition() and not getName() = "__fpclassifyl" } +} + +class InfinityCheckedExpr extends Expr { + InfinityCheckedExpr() { + exists(MacroInvocation mi | + mi.getMacroName() = ["isfinite", "isinf"] and + mi.getExpr() = this + ) + } + + Expr getCheckedExpr() { + result = + this.(ConditionalExpr) + .getThen() + .(LTExpr) + .getLesserOperand() + .(BitwiseAndExpr) + .getLeftOperand() + .(FunctionCall) + .getArgument(0) + } +} + +/* +signature module ResourceLeakConfigSig { + predicate isResource(DataFlow::Node node); + + predicate isFree(DataFlow::Node node, DataFlow::Node resource); + + default ControlFlowNode outOfScope(DataFlow::Node resource) { + result = resource.asExpr().getEnclosingFunction().getBlock().getLastStmt() + } + + default predicate isAlias(DataFlow::Node alias, DataFlow::Node resource) { + isResource(resource) and + DataFlow::localFlow(resource, alias) + } +} + +module ResourceLeak { + predicate isLeaked(DataFlow::Node resource, ControlFlowNode cfgNode) { + resource.asExpr() = cfgNode + or + isLeaked(resource, cfgNode.getAPredecessor()) and + not exists(DataFlow::Node free, DataFlow::Node freed | + free.asExpr() = cfgNode and + Config::isFree(free, freed) and + Config::isAlias(freed, resource) + ) + } + + private ControlFlowNode getARawLeak(DataFlow::Node resource) { + Config::isResource(resource) and + result = Config::outOfScope(resource) and + isLeaked(resource, result) + } + + ControlFlowNode getALeak(DataFlow::Node resource) { + result = getARawLeak(resource) and + not exists(DataFlow::Node dealiased | + Config::isResource(dealiased) and + Config::isAlias(resource, dealiased) and + not resource = dealiased and + result = getARawLeak(dealiased) + ) and + not exists(ControlFlowNode dominator | + dominator = getARawLeak(resource) and + strictlyDominates(dominator, result) + ) + } +} + +module MissedInfinityConfig implements ResourceLeakConfigSig { + predicate isResource(DataFlow::Node node) { + //exists(BinaryOperation expr | + // expr = node.asExpr() and + // expr.getOperator() = "/" and + // RestrictedRangeAnalysis::upperBound(expr.getRightOperand()) <= 0 and + // RestrictedRangeAnalysis::lowerBound(expr.getRightOperand()) >= 0 + //) + [ + RestrictedRangeAnalysis::upperBound(node.asExpr()), + RestrictedRangeAnalysis::lowerBound(node.asExpr()) + ].toString() = "Infinity" + //and not node.asExpr() instanceof VariableAccess + //and not node.asExpr() instanceof ArrayExpr + } + + predicate test(Expr expr, string lowerBound, string upperBound) { + //expr.getType() instanceof FloatingPointType + //and + lowerBound = RestrictedRangeAnalysis::lowerBound(expr).toString() and + upperBound = RestrictedRangeAnalysis::upperBound(expr).toString() and + [lowerBound, upperBound] = "Infinity" + } + + additional predicate testDiv( + DivExpr div, string lbDiv, string ubDiv, string lbNum, string ubNum, string lbDenom, + string ubDenom + ) { + lbDiv = RestrictedRangeAnalysis::lowerBound(div).toString() and + ubDiv = RestrictedRangeAnalysis::upperBound(div).toString() and + lbNum = RestrictedRangeAnalysis::lowerBound(div.getLeftOperand()).toString() and + ubNum = RestrictedRangeAnalysis::upperBound(div.getLeftOperand()).toString() and + lbDenom = RestrictedRangeAnalysis::lowerBound(div.getRightOperand()).toString() and + ubDenom = RestrictedRangeAnalysis::upperBound(div.getRightOperand()).toString() and + not lbDiv = ubDiv and + InvalidNaNUsage::isSource(DataFlow::exprNode(div)) + } + + predicate isFree(DataFlow::Node node, DataFlow::Node resource) { + isResource(resource) and + ( + node.asExpr().(InfinityCheckedExpr).getCheckedExpr() = resource.asExpr() + or + not [ + RestrictedRangeAnalysis::lowerBound(node.asExpr()), + RestrictedRangeAnalysis::upperBound(node.asExpr()) + ].toString() = "Infinity" and + isMove(node, resource) + ) + } + + predicate isMove(DataFlow::Node node, DataFlow::Node moved) { + isResource(moved) and + isAlias(node, moved) and + not exists(DataFlow::Node laterUse, ControlFlowNode later | + later = laterUse.asExpr() and + later = node.asExpr().getASuccessor+() and + hashCons(laterUse.asExpr()) = hashCons(moved.asExpr()) + ) + } + + ControlFlowNode outOfScope(DataFlow::Node resource) { + result = resource.asExpr().getEnclosingFunction().getBlock().getLastStmt() + or + exists(AssignExpr assign, DataFlow::Node alias | + assign.getRValue() = alias.asExpr() and + isAlias(alias, resource) and + not assign.getRValue().(VariableAccess).getTarget() instanceof StackVariable and + result = assign + ) + or + exists(FunctionCall fc | + fc.getArgument(_) = resource.asExpr() and + result = fc + ) + } + + predicate isAlias(DataFlow::Node alias, DataFlow::Node resource) { + TaintTracking::localTaint(resource, alias) + } +} + +import ResourceLeak as MissedInfinity +*/ + +//from Expr value, FunctionCall fc +//where +// not isExcluded(value, FloatingTypes2Package::possibleUndetectedNaNorInfinityQuery()) and +// [RestrictedRangeAnalysis::lowerBound(value), RestrictedRangeAnalysis::upperBound(value)].toString() = "Infinity" and +// value = fc.getAnArgument() and +// fc.getTarget() instanceof CantHandleInfinityFunction and +// not value instanceof InfinityCheckedExpr and +// not exists (GuardCondition g | +// g.controls(fc.getBasicBlock(), true) and +// g instanceof InfinityCheckedExpr +// // TODO check we check the right expr +// ) +//select +// value, "possible use of unchecked infinity as arg to " + fc.getTarget().getName() +//from DataFlow::Node node, ControlFlowNode leakPoint +//where +// not isExcluded(node.asExpr(), FloatingTypes2Package::possibleUndetectedNaNorInfinityQuery()) and +// leakPoint = MissedInfinity::getALeak(node) +// select node, "Expression generates an infinity which is not checked before $@.", leakPoint, "external leak point" + + +//import InvalidNaNFlow::PathGraph +//from Element elem, DataFlow::Node source, DataFlow::Node sink, string msg, string sourceString +from + Element elem, InvalidInfinityFlow::PathNode source, InvalidInfinityFlow::PathNode sink, + string msg, string sourceString +where + elem = MacroUnwrapper::unwrapElement(sink.getNode().asExpr()) and + not isExcluded(elem, FloatingTypes2Package::possibleUndetectedNaNorInfinityQuery()) and + ( + InvalidInfinityFlow::flow(source.getNode(), sink.getNode()) and + msg = "Invalid usage of possible $@." and + sourceString = "infinity" + //or + //InvalidNaNFlow::flow(source, sink) and + //msg = "Invalid usage of possible $@." and + //sourceString = "NaN resulting from " + source.asExpr().(InvalidOperationExpr).getReason() + ) +select elem, source, sink, msg, source, sourceString diff --git a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected new file mode 100644 index 0000000000..78f4c6baec --- /dev/null +++ b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected @@ -0,0 +1,48 @@ +edges +| test.c:8:14:8:20 | ... / ... | test.c:8:14:8:20 | ... / ... | provenance | | +| test.c:8:14:8:20 | ... / ... | test.c:12:8:12:9 | l2 | provenance | | +| test.c:8:14:8:20 | ... / ... | test.c:18:3:18:9 | l2 | provenance | | +| test.c:8:14:8:20 | ... / ... | test.c:27:19:27:20 | l2 | provenance | | +| test.c:9:14:9:16 | - ... | test.c:9:14:9:16 | - ... | provenance | | +| test.c:9:14:9:16 | - ... | test.c:13:8:13:9 | l3 | provenance | | +| test.c:9:14:9:16 | - ... | test.c:19:3:19:9 | l3 | provenance | | +| test.c:9:14:9:16 | - ... | test.c:28:19:28:20 | l3 | provenance | | +| test.c:31:14:32:15 | ... / ... | test.c:31:14:32:15 | ... / ... | provenance | | +| test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | provenance | | +| test.c:33:14:33:22 | ... / ... | test.c:33:14:33:22 | ... / ... | provenance | | +| test.c:33:14:33:22 | ... / ... | test.c:39:3:39:9 | l8 | provenance | | +nodes +| test.c:8:14:8:20 | ... / ... | semmle.label | ... / ... | +| test.c:8:14:8:20 | ... / ... | semmle.label | ... / ... | +| test.c:9:14:9:16 | - ... | semmle.label | - ... | +| test.c:9:14:9:16 | - ... | semmle.label | - ... | +| test.c:12:8:12:9 | l2 | semmle.label | l2 | +| test.c:13:8:13:9 | l3 | semmle.label | l3 | +| test.c:18:3:18:9 | l2 | semmle.label | l2 | +| test.c:19:3:19:9 | l3 | semmle.label | l3 | +| test.c:27:19:27:20 | l2 | semmle.label | l2 | +| test.c:28:19:28:20 | l3 | semmle.label | l3 | +| test.c:31:14:32:15 | ... / ... | semmle.label | ... / ... | +| test.c:31:14:32:15 | ... / ... | semmle.label | ... / ... | +| test.c:33:14:33:22 | ... / ... | semmle.label | ... / ... | +| test.c:33:14:33:22 | ... / ... | semmle.label | ... / ... | +| test.c:38:3:38:9 | l7 | semmle.label | l7 | +| test.c:39:3:39:9 | l8 | semmle.label | l8 | +| test.c:61:5:61:19 | ... / ... | semmle.label | ... / ... | +| test.c:66:5:66:21 | ... / ... | semmle.label | ... / ... | +| test.c:72:14:72:30 | ... / ... | semmle.label | ... / ... | +| test.c:75:18:75:34 | ... / ... | semmle.label | ... / ... | +subpaths +#select +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | diff --git a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.qlref b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.qlref new file mode 100644 index 0000000000..dccac37c5f --- /dev/null +++ b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.qlref @@ -0,0 +1 @@ +rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql \ No newline at end of file diff --git a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected new file mode 100644 index 0000000000..f317f236ef --- /dev/null +++ b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected @@ -0,0 +1,63 @@ +edges +| test.c:27:14:27:20 | ... / ... | test.c:27:14:27:20 | ... / ... | provenance | | +| test.c:27:14:27:20 | ... / ... | test.c:36:3:36:9 | l5 | provenance | | +| test.c:27:14:27:20 | ... / ... | test.c:46:3:46:4 | l5 | provenance | | +| test.c:27:14:27:20 | ... / ... | test.c:47:3:47:4 | l5 | provenance | | +| test.c:27:14:27:20 | ... / ... | test.c:48:3:48:4 | l5 | provenance | | +| test.c:27:14:27:20 | ... / ... | test.c:49:3:49:4 | l5 | provenance | | +| test.c:27:14:27:20 | ... / ... | test.c:50:3:50:4 | l5 | provenance | | +| test.c:27:14:27:20 | ... / ... | test.c:51:3:51:4 | l5 | provenance | | +| test.c:28:14:28:20 | ... / ... | test.c:28:14:28:20 | ... / ... | provenance | | +| test.c:28:14:28:20 | ... / ... | test.c:37:3:37:9 | l6 | provenance | | +| test.c:28:14:28:20 | ... / ... | test.c:52:3:52:4 | l6 | provenance | | +| test.c:31:14:32:15 | ... / ... | test.c:31:14:32:15 | ... / ... | provenance | | +| test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | provenance | | +| test.c:31:14:32:15 | ... / ... | test.c:53:3:53:4 | l7 | provenance | | +| test.c:33:14:33:22 | ... / ... | test.c:33:14:33:22 | ... / ... | provenance | | +| test.c:33:14:33:22 | ... / ... | test.c:39:3:39:9 | l8 | provenance | | +| test.c:33:14:33:22 | ... / ... | test.c:54:3:54:4 | l8 | provenance | | +nodes +| test.c:27:14:27:20 | ... / ... | semmle.label | ... / ... | +| test.c:27:14:27:20 | ... / ... | semmle.label | ... / ... | +| test.c:28:14:28:20 | ... / ... | semmle.label | ... / ... | +| test.c:28:14:28:20 | ... / ... | semmle.label | ... / ... | +| test.c:31:14:32:15 | ... / ... | semmle.label | ... / ... | +| test.c:31:14:32:15 | ... / ... | semmle.label | ... / ... | +| test.c:33:14:33:22 | ... / ... | semmle.label | ... / ... | +| test.c:33:14:33:22 | ... / ... | semmle.label | ... / ... | +| test.c:36:3:36:9 | l5 | semmle.label | l5 | +| test.c:37:3:37:9 | l6 | semmle.label | l6 | +| test.c:38:3:38:9 | l7 | semmle.label | l7 | +| test.c:39:3:39:9 | l8 | semmle.label | l8 | +| test.c:46:3:46:4 | l5 | semmle.label | l5 | +| test.c:47:3:47:4 | l5 | semmle.label | l5 | +| test.c:48:3:48:4 | l5 | semmle.label | l5 | +| test.c:49:3:49:4 | l5 | semmle.label | l5 | +| test.c:50:3:50:4 | l5 | semmle.label | l5 | +| test.c:51:3:51:4 | l5 | semmle.label | l5 | +| test.c:52:3:52:4 | l6 | semmle.label | l6 | +| test.c:53:3:53:4 | l7 | semmle.label | l7 | +| test.c:54:3:54:4 | l8 | semmle.label | l8 | +| test.c:61:5:61:19 | ... / ... | semmle.label | ... / ... | +| test.c:66:5:66:21 | ... / ... | semmle.label | ... / ... | +| test.c:72:14:72:30 | ... / ... | semmle.label | ... / ... | +| test.c:75:18:75:34 | ... / ... | semmle.label | ... / ... | +subpaths +#select +| 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 | +| test.c:37:8:37:9 | l6 | test.c:28:14:28:20 | ... / ... | test.c:37:3:37:9 | l6 | Invalid usage of possible $@. | test.c:28:14:28:20 | ... / ... | NaN resulting from possible division of infinity by infinity | +| 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 | ... / ... | NaN resulting from possible division of zero by zero | +| 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 | ... / ... | NaN resulting from possible division of zero by zero | +| test.c:46:3:46:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:46:3:46:4 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity | +| test.c:47:3:47:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:47:3:47:4 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity | +| test.c:48:3:48:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:48:3:48:4 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity | +| test.c:49:3:49:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:49:3:49:4 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity | +| test.c:50:3:50:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:50:3:50:4 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity | +| test.c:51:3:51:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:51:3:51:4 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | diff --git a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.qlref b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.qlref new file mode 100644 index 0000000000..d88c172bd5 --- /dev/null +++ b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.qlref @@ -0,0 +1 @@ +rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql \ No newline at end of file diff --git a/c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.expected b/c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.expected new file mode 100644 index 0000000000..2ec1a0ac6c --- /dev/null +++ b/c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.expected @@ -0,0 +1 @@ +No expected results have yet been specified \ No newline at end of file diff --git a/c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.qlref b/c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.qlref new file mode 100644 index 0000000000..1ffb7ad071 --- /dev/null +++ b/c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.qlref @@ -0,0 +1 @@ +rules/DIR-4-15/PossibleUndetectedNaNorInfinity.ql \ No newline at end of file diff --git a/c/misra/test/rules/DIR-4-15/test.c b/c/misra/test/rules/DIR-4-15/test.c new file mode 100644 index 0000000000..d634a6e594 --- /dev/null +++ b/c/misra/test/rules/DIR-4-15/test.c @@ -0,0 +1,76 @@ +#include "math.h" + +float getFloat() { return 1.0; } + +// Parameter could be infinity +void f1(float p1) { + float l1 = 1; + float l2 = 1.0 / 0; + float l3 = -l2; + + 10 / l1; // COMPLIANT + 10 / l2; // NON_COMPLIANT: Underflows to zero + 10 / l3; // NON_COMPLIANT: Underflow to negative zero + 10 / p1; // COMPLIANT: Reduce false positives by assuming not infinity + 10 / getFloat(); // COMPLIANT: Reduce false positives by assuming not infinity + + (int)l1; // COMPLIANT + (int)l2; // NON_COMPLIANT + (int)l3; // NON_COMPLIANT + (int)p1; // COMPLIANT: Reduce false positives by assuming not infinity + (int)getFloat(); // COMPLIANT: Reduce false positives by assuming not infinity + + // Not NaN: + float l4 = l1 / l1; // COMPLIANT + + // NaN because of infinity divided by itself: + float l5 = l2 / l2; // NON_COMPLIANT: Division by infinity not allowed. + float l6 = l3 / l3; // NON_COMPLIANT: Division by infinity not allowed. + + // NaN because of zero divided by itself: + float l7 = getFloat() / + p1; // COMPLIANT: Reduce false positives by assuming not infinity + float l8 = 0.0 / 0.0; + + (int)l4; // COMPLIANT + (int)l5; // NON_COMPLIANT: Casting NaN to int + (int)l6; // NON_COMPLIANT: Casting NaN to int + (int)l7; // NON_COMPLIANT: Casting NaN to int + (int)l8; // NON_COMPLIANT: Casting NaN to int + + l4 == 0; // COMPLIANT + l4 != 0; // COMPLIANT + l4 <= 0; // COMPLIANT + l4 < 0; // COMPLIANT + l4 >= 0; // COMPLIANT + l5 == 0; // NON_COMPLIANT: Comparison with NaN always false + l5 != 0; // NON_COMPLIANT: Comparison with NaN always false + l5 < 0; // NON_COMPLIANT: Comparison with NaN always false + l5 <= 0; // NON_COMPLIANT: Comparison with NaN always false + l5 > 0; // NON_COMPLIANT: Comparison with NaN always false + l5 >= 0; // NON_COMPLIANT: Comparison with NaN always false + l6 == 0; // NON_COMPLIANT: Comparison with NaN always false + l7 == 0; // NON_COMPLIANT: Comparison with NaN always false + l8 == 0; // NON_COMPLIANT: Comparison with NaN always false + + // Guards + float l9 = 0; + if (l9 != 0) { + (int) (l9 / l9); // COMPLIANT: l9 is not zero + } else { + (int) (l9 / l9); // NON_COMPLIANT: Casting NaN to integer + } + + float l10 = 0; + if (l10 == 0) { + (int) (l10 / l10); // NON_COMPLIANT: Casting NaN to integer + } else { + (int) (l10 / l10); // COMPLIANT: l10 is not zero + } + + float l11 = 0; + l11 == 0 ? (int) (l11 / l11) : 0; // NON_COMPLIANT + l11 == 0 ? 0 : (int) (l11 / l11); // COMPLIANT + l11 != 0 ? (int) (l11 / l11) : 0; // COMPLIANT + l11 != 0 ? 0 : (int) (l11 / l11); // NON_COMPLIANT +} \ No newline at end of file diff --git a/cpp/common/src/codingstandards/cpp/FloatingPoint.qll b/cpp/common/src/codingstandards/cpp/FloatingPoint.qll new file mode 100644 index 0000000000..d143f81418 --- /dev/null +++ b/cpp/common/src/codingstandards/cpp/FloatingPoint.qll @@ -0,0 +1,61 @@ +import codeql.util.Boolean +import codingstandards.cpp.RestrictedRangeAnalysis + +predicate exprMayEqualZero(Expr e) { + RestrictedRangeAnalysis::upperBound(e) >= 0 and + RestrictedRangeAnalysis::lowerBound(e) <= 0 and + not guardedNotEqualZero(e) +} + +predicate guardedNotEqualZero(Expr e) { + /* Note Boolean cmpEq, false means cmpNeq */ + exists(Expr checked, GuardCondition guard, boolean cmpEq, BooleanValue value | + hashCons(checked) = hashCons(e) and + guard.controls(e.getBasicBlock(), cmpEq) and + value.getValue() = cmpEq and + guard.comparesEq(checked, 0, false, value) + ) + or + exists(Expr checked, Expr val, int valVal, GuardCondition guard, boolean cmpEq | + hashCons(checked) = hashCons(e) and + forex(float v | + v = [RestrictedRangeAnalysis::lowerBound(val), RestrictedRangeAnalysis::upperBound(val)] + | + valVal = v + ) and + guard.controls(e.getBasicBlock(), cmpEq) and + guard.comparesEq(checked, val, -valVal, false, cmpEq) + ) +} + +predicate guardedNotInfinite(Expr e) { + /* Note Boolean cmpEq, false means cmpNeq */ + exists(Expr c, GuardCondition guard, boolean cmpEq | + hashCons(c) = hashCons(e) and + guard.controls(e, cmpEq) and + guard.comparesEq(c, 0, cmpEq.booleanNot(), _) + ) +} + +predicate test(Expr e, Expr v, int k, boolean areEqual, Boolean value, Expr gce, BasicBlock bb) { + exists(GuardCondition gc | gce = gc | + gc.controls(bb, _) and + gc.comparesEq(e, v, k, areEqual, value) and + ( + //gc.getAChild+().toString().matches("%dfYRes%") or + e.getAChild*().toString().matches("%dfPseudoPanchro%") or + v.getAChild*().toString().matches("%dfPseudoPanchro%") + ) + ) +} + +predicate exprMayEqualInfinity(Expr e, Boolean positive) { + exists(float target | + positive = true and target = 1.0 / 0.0 + or + positive = false and target = -1.0 / 0.0 + | + RestrictedRangeAnalysis::upperBound(e.getUnconverted()) = target or + RestrictedRangeAnalysis::lowerBound(e.getUnconverted()) = target + ) +} \ No newline at end of file diff --git a/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll b/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll new file mode 100644 index 0000000000..79ae2f367a --- /dev/null +++ b/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll @@ -0,0 +1,1903 @@ +import semmle.code.cpp.controlflow.Guards +import semmle.code.cpp.valuenumbering.HashCons +/** + * A fork of SimpleRangeAnalysis.qll, which is intended to only give + * results with a conservative basis. + * + * For instance, since range analysis is local, a function call (e.g. + * `f()`) is given the widest possible range in the original library. In + * this fork, we do not provide any result. + * + * Original library level doc comment from SimpleRangeAnalysis.qll: + * + * Simple range analysis library. Range analysis is usually done as an + * abstract interpretation over the lattice of range values. (A range is a + * pair, containing a lower and upper bound for the value.) The problem + * with this approach is that the lattice is very tall, which means it can + * take an extremely large number of iterations to find the least fixed + * point. This example illustrates the problem: + * + * int count = 0; + * for (; p; p = p->next) { + * count = count+1; + * } + * + * The range of 'count' is initially (0,0), then (0,1) on the second + * iteration, (0,2) on the third iteration, and so on until we eventually + * reach maxInt. + * + * This library uses a crude solution to the problem described above: if + * the upper (or lower) bound of an expression might depend recursively on + * itself then we round it up (down for lower bounds) to one of a fixed set + * of values, such as 0, 1, 2, 256, and +Inf. This limits the height of the + * lattice which ensures that the analysis will terminate in a reasonable + * amount of time. This solution is similar to the abstract interpretation + * technique known as 'widening', but it is less precise because we are + * unable to inspect the bounds from the previous iteration of the fixed + * point computation. For example, widening might be able to deduce that + * the lower bound is -11 but we would approximate it to -16. + * + * QL does not allow us to compute an aggregate over a recursive + * sub-expression, so we cannot compute the minimum lower bound and maximum + * upper bound during the recursive phase of the query. Instead, the + * recursive phase computes a set of lower bounds and a set of upper bounds + * for each expression. We compute the minimum lower bound and maximum + * upper bound after the recursion is finished. This is another reason why + * we need to limit the number of bounds per expression, because they will + * all be stored until the recursive phase is finished. + * + * The ranges are represented using a pair of floating point numbers. This + * is simpler than using integers because floating point numbers cannot + * overflow and wrap. It is also convenient because we can detect overflow + * and negative overflow by looking for bounds that are outside the range + * of the type. + */ +module RestrictedRangeAnalysis { + import cpp + private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils as Util + import semmle.code.cpp.rangeanalysis.RangeSSA + import SimpleRangeAnalysisCached + private import semmle.code.cpp.rangeanalysis.NanAnalysis + + float largeValue() { result = 1000000000000000.0 } + + /** + * This fixed set of lower bounds is used when the lower bounds of an + * expression are recursively defined. The inferred lower bound is rounded + * down to the nearest lower bound in the fixed set. This restricts the + * height of the lattice, which prevents the analysis from exploding. + * + * Note: these bounds were chosen fairly arbitrarily. Feel free to add more + * bounds to the set if it helps on specific examples and does not make + * performance dramatically worse on large codebases, such as libreoffice. + */ + private float wideningLowerBounds(ArithmeticType t) { + result = 2.0 or + result = 1.0 or + result = 0.0 or + result = -1.0 or + result = -2.0 or + result = -8.0 or + result = -16.0 or + result = -128.0 or + result = -256.0 or + result = -32768.0 or + result = -65536.0 or + result = max(float v | v = Util::typeLowerBound(t) or v = -largeValue()) + } + + /** See comment for `wideningLowerBounds`, above. */ + private float wideningUpperBounds(ArithmeticType t) { + result = -2.0 or + result = -1.0 or + result = 0.0 or + result = 1.0 or + result = 2.0 or + result = 7.0 or + result = 15.0 or + result = 127.0 or + result = 255.0 or + result = 32767.0 or + result = 65535.0 or + result = min(float v | v = Util::typeLowerBound(t) or v = largeValue()) + } + + /** + * Gets the value of the expression `e`, if it is a constant. + * This predicate also handles the case of constant variables initialized in different + * compilation units, which doesn't necessarily have a getValue() result from the extractor. + */ + private string getValue(Expr e) { + if exists(e.getValue()) + then result = e.getValue() + else + /* + * It should be safe to propagate the initialization value to a variable if: + * The type of v is const, and + * The type of v is not volatile, and + * Either: + * v is a local/global variable, or + * v is a static member variable + */ + + exists(VariableAccess access, StaticStorageDurationVariable v | + not v.getUnderlyingType().isVolatile() and + v.getUnderlyingType().isConst() and + e = access and + v = access.getTarget() and + result = getValue(v.getAnAssignedValue()) + ) + } + + private float varMaxVal(Variable v) { + result = min(float f | f = Util::varMaxVal(v) or f = largeValue()) + } + + private float varMinVal(Variable v) { + result = max(float f | f = Util::varMinVal(v) or f = -largeValue()) + } + + private float exprMaxVal(Expr e) { + result = min(float f | f = Util::exprMaxVal(e) or f = largeValue()) + } + + private float exprMinVal(Expr e) { + result = max(float f | f = Util::exprMinVal(e) or f = -largeValue()) + } + + /** + * A bitwise `&` expression in which both operands are unsigned, or are effectively + * unsigned due to being a non-negative constant. + */ + private class UnsignedBitwiseAndExpr extends BitwiseAndExpr { + UnsignedBitwiseAndExpr() { + ( + this.getLeftOperand() + .getFullyConverted() + .getType() + .getUnderlyingType() + .(IntegralType) + .isUnsigned() or + getValue(this.getLeftOperand().getFullyConverted()).toInt() >= 0 + ) and + ( + this.getRightOperand() + .getFullyConverted() + .getType() + .getUnderlyingType() + .(IntegralType) + .isUnsigned() or + getValue(this.getRightOperand().getFullyConverted()).toInt() >= 0 + ) + } + } + + /** + * Gets the floor of `v`, with additional logic to work around issues with + * large numbers. + */ + bindingset[v] + float safeFloor(float v) { + // return the floor of v + v.abs() < 2.pow(31) and + result = v.floor() + or + // `floor()` doesn't work correctly on large numbers (since it returns an integer), + // so fall back to unrounded numbers at this scale. + not v.abs() < 2.pow(31) and + result = v + } + + /** A `MulExpr` where exactly one operand is constant. */ + private class MulByConstantExpr extends MulExpr { + float constant; + Expr operand; + + MulByConstantExpr() { + exists(Expr constantExpr | + this.hasOperands(constantExpr, operand) and + constant = getValue(constantExpr.getFullyConverted()).toFloat() and + not exists(getValue(operand.getFullyConverted()).toFloat()) + ) + } + + /** Gets the value of the constant operand. */ + float getConstant() { result = constant } + + /** Gets the non-constant operand. */ + Expr getOperand() { result = operand } + } + + private class UnsignedMulExpr extends MulExpr { + UnsignedMulExpr() { + this.getType().(IntegralType).isUnsigned() and + // Avoid overlap. It should be slightly cheaper to analyze + // `MulByConstantExpr`. + not this instanceof MulByConstantExpr + } + } + + /** + * Holds if `expr` is effectively a multiplication of `operand` with the + * positive constant `positive`. + */ + private predicate effectivelyMultipliesByPositive(Expr expr, Expr operand, float positive) { + operand = expr.(MulByConstantExpr).getOperand() and + positive = expr.(MulByConstantExpr).getConstant() and + positive >= 0.0 // includes positive zero + or + operand = expr.(UnaryPlusExpr).getOperand() and + positive = 1.0 + or + operand = expr.(CommaExpr).getRightOperand() and + positive = 1.0 + or + operand = expr.(StmtExpr).getResultExpr() and + positive = 1.0 + } + + /** + * Holds if `expr` is effectively a multiplication of `operand` with the + * negative constant `negative`. + */ + private predicate effectivelyMultipliesByNegative(Expr expr, Expr operand, float negative) { + operand = expr.(MulByConstantExpr).getOperand() and + negative = expr.(MulByConstantExpr).getConstant() and + negative < 0.0 // includes negative zero + or + operand = expr.(UnaryMinusExpr).getOperand() and + negative = -1.0 + } + + private class AssignMulByConstantExpr extends AssignMulExpr { + float constant; + + AssignMulByConstantExpr() { + constant = getValue(this.getRValue().getFullyConverted()).toFloat() + } + + float getConstant() { result = constant } + } + + private class AssignMulByPositiveConstantExpr extends AssignMulByConstantExpr { + AssignMulByPositiveConstantExpr() { constant >= 0.0 } + } + + private class AssignMulByNegativeConstantExpr extends AssignMulByConstantExpr { + AssignMulByNegativeConstantExpr() { constant < 0.0 } + } + + private class UnsignedAssignMulExpr extends AssignMulExpr { + UnsignedAssignMulExpr() { + this.getType().(IntegralType).isUnsigned() and + // Avoid overlap. It should be slightly cheaper to analyze + // `AssignMulByConstantExpr`. + not this instanceof AssignMulByConstantExpr + } + } + + /** + * Holds if `expr` is effectively a division of `operand` with the + * positive constant `positive`. + */ + private predicate dividesByPositive(DivExpr expr, Expr operand, float positive) { + operand = expr.(DivExpr).getLeftOperand() and + positive = expr.(DivExpr).getRightOperand().getValue().toFloat() and + positive > 0.0 // doesn't include zero + } + + /** + * Holds if `expr` is effectively a division of `operand` with the + * negative constant `negative`. + */ + private predicate dividesByNegative(Expr expr, Expr operand, float negative) { + operand = expr.(DivExpr).getLeftOperand() and + negative = getValue(expr.(DivExpr).getRightOperand().getFullyConverted()).toFloat() and + negative < 0.0 // doesn't include zero + } + + /** + * Holds if `expr` may divide by zero. + */ + predicate dividesByZero(Expr expr) { + exists(Expr divisor | + divisor = expr.(DivExpr).getRightOperand() and + getTruncatedLowerBounds(divisor) <= 0.0 and + getTruncatedUpperBounds(divisor) >= 0.0 and + not isCheckedNotZero(divisor) + ) + } + + /** + * Holds if `expr` is checked with a guard to not be zero. + * + * Since our range analysis only tracks an upper and lower bound, that means if a variable has + * range [-10, 10], its range includes zero. In the body of an if statement that checks it's not + * equal to zero, we cannot update the range to reflect that as the upper and lower bounds are + * not changed. This problem is not the case for gt, lt, gte, lte, or ==, as these can be used to + * create a new subset range that does not include zero. + * + * It is important to know if an expr may be zero to avoid division by zero creating infinities. + */ + predicate isCheckedNotZero(Expr expr) { + exists(RangeSsaDefinition def, StackVariable v, VariableAccess guardVa, Expr guard | + // This is copied from getGuardedUpperBound, which says its only an approximation. This is + // indeed wrong in many cases. + def.isGuardPhi(v, guardVa, guard, _) and + exists(unique(BasicBlock b | b = def.(BasicBlock).getAPredecessor())) and + expr = def.getAUse(v) and + isNEPhi(v, def, guardVa, 0) + ) + or guardedHashConsNotEqualZero(expr) + } + + predicate guardedHashConsNotEqualZero(Expr e) { + /* Note Boolean cmpEq, false means cmpNeq */ + exists(Expr check, Expr val, int valVal, GuardCondition guard, boolean cmpEq | + hashCons(check) = hashCons(e) and + valVal = getValue(val).toFloat() and + guard.controls(e.getBasicBlock(), cmpEq) and + ( + guard.comparesEq(check, val, -valVal, false, cmpEq) or + guard.comparesEq(val, check, -valVal, false, cmpEq) + ) + ) + } + + /** Set of expressions which we know how to analyze. */ + predicate analyzableExpr(Expr e) { + // The type of the expression must be arithmetic. We reuse the logic in + // `exprMinVal` to check this. + exists(Util::exprMinVal(e)) and + ( + exists(getValue(e).toFloat()) + or + effectivelyMultipliesByPositive(e, _, _) + or + effectivelyMultipliesByNegative(e, _, _) + or + dividesByPositive(e, _, _) + or + dividesByNegative(e, _, _) + // Introduces non-monotonic recursion. However, analysis mostly works with this + // commented out. + // or + // dividesByZero(e) + or + e instanceof DivExpr // TODO: confirm this is OK + or + e instanceof MinExpr + or + e instanceof MaxExpr + or + e instanceof ConditionalExpr + or + e instanceof AddExpr + or + e instanceof SubExpr + or + e instanceof UnsignedMulExpr + or + e instanceof AssignExpr + or + e instanceof AssignAddExpr + or + e instanceof AssignSubExpr + or + e instanceof UnsignedAssignMulExpr + or + e instanceof AssignMulByConstantExpr + or + e instanceof CrementOperation + or + e instanceof RemExpr + or + // A conversion is analyzable, provided that its child has an arithmetic + // type. (Sometimes the child is a reference type, and so does not get + // any bounds.) Rather than checking whether the type of the child is + // arithmetic, we reuse the logic that is already encoded in + // `exprMinVal`. + exists(Util::exprMinVal(e.(Conversion).getExpr())) + or + // Also allow variable accesses, provided that they have SSA + // information. + exists(RangeSsaDefinition def | e = def.getAUse(_)) + or + e instanceof UnsignedBitwiseAndExpr + or + // `>>` by a constant + exists(getValue(e.(RShiftExpr).getRightOperand())) + ) + } + + /** + * Set of definitions that this definition depends on. The transitive + * closure of this relation is used to detect definitions which are + * recursively defined, so that we can prevent the analysis from exploding. + * + * The structure of `defDependsOnDef` and its helper predicates matches the + * structure of `getDefLowerBoundsImpl` and + * `getDefUpperBoundsImpl`. Therefore, if changes are made to the structure + * of the main analysis algorithm then matching changes need to be made + * here. + */ + private predicate defDependsOnDef( + RangeSsaDefinition def, StackVariable v, RangeSsaDefinition srcDef, StackVariable srcVar + ) { + // Definitions with a defining value. + exists(Expr expr | assignmentDef(def, v, expr) | exprDependsOnDef(expr, srcDef, srcVar)) + or + // Assignment operations with a defining value + exists(AssignOperation assignOp | + analyzableExpr(assignOp) and + def = assignOp and + def.getAVariable() = v and + exprDependsOnDef(assignOp, srcDef, srcVar) + ) + or + exists(CrementOperation crem | + def = crem and + def.getAVariable() = v and + exprDependsOnDef(crem.getOperand(), srcDef, srcVar) + ) + or + // Phi nodes. + phiDependsOnDef(def, v, srcDef, srcVar) + } + + /** + * Helper predicate for `defDependsOnDef`. This predicate matches + * the structure of `getLowerBoundsImpl` and `getUpperBoundsImpl`. + */ + private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, StackVariable srcVar) { + exists(Expr operand | + effectivelyMultipliesByNegative(e, operand, _) and + exprDependsOnDef(operand, srcDef, srcVar) + ) + or + exists(Expr operand | + effectivelyMultipliesByPositive(e, operand, _) and + exprDependsOnDef(operand, srcDef, srcVar) + ) + or + exists(Expr operand | + (dividesByPositive(e, operand, _) or dividesByNegative(e, operand, _)) and + exprDependsOnDef(operand, srcDef, srcVar) + ) + or + exists(MinExpr minExpr | e = minExpr | exprDependsOnDef(minExpr.getAnOperand(), srcDef, srcVar)) + or + exists(MaxExpr maxExpr | e = maxExpr | exprDependsOnDef(maxExpr.getAnOperand(), srcDef, srcVar)) + or + exists(ConditionalExpr condExpr | e = condExpr | + exprDependsOnDef(condExpr.getAnOperand(), srcDef, srcVar) + ) + or + exists(AddExpr addExpr | e = addExpr | exprDependsOnDef(addExpr.getAnOperand(), srcDef, srcVar)) + or + exists(SubExpr subExpr | e = subExpr | exprDependsOnDef(subExpr.getAnOperand(), srcDef, srcVar)) + or + exists(UnsignedMulExpr mulExpr | e = mulExpr | + exprDependsOnDef(mulExpr.getAnOperand(), srcDef, srcVar) + ) + or + exists(AssignExpr addExpr | e = addExpr | exprDependsOnDef(addExpr.getRValue(), srcDef, srcVar)) + or + exists(AssignAddExpr addExpr | e = addExpr | + exprDependsOnDef(addExpr.getAnOperand(), srcDef, srcVar) + ) + or + exists(AssignSubExpr subExpr | e = subExpr | + exprDependsOnDef(subExpr.getAnOperand(), srcDef, srcVar) + ) + or + exists(UnsignedAssignMulExpr mulExpr | e = mulExpr | + exprDependsOnDef(mulExpr.getAnOperand(), srcDef, srcVar) + ) + or + exists(AssignMulByConstantExpr mulExpr | e = mulExpr | + exprDependsOnDef(mulExpr.getLValue(), srcDef, srcVar) + ) + or + exists(CrementOperation crementExpr | e = crementExpr | + exprDependsOnDef(crementExpr.getOperand(), srcDef, srcVar) + ) + or + exists(RemExpr remExpr | e = remExpr | exprDependsOnDef(remExpr.getAnOperand(), srcDef, srcVar)) + or + exists(Conversion convExpr | e = convExpr | + exprDependsOnDef(convExpr.getExpr(), srcDef, srcVar) + ) + or + // unsigned `&` + exists(UnsignedBitwiseAndExpr andExpr | + andExpr = e and + exprDependsOnDef(andExpr.getAnOperand(), srcDef, srcVar) + ) + or + // `>>` by a constant + exists(RShiftExpr rs | + rs = e and + exists(getValue(rs.getRightOperand())) and + exprDependsOnDef(rs.getLeftOperand(), srcDef, srcVar) + ) + or + e = srcDef.getAUse(srcVar) + } + + /** + * Helper predicate for `defDependsOnDef`. This predicate matches + * the structure of `getPhiLowerBounds` and `getPhiUpperBounds`. + */ + private predicate phiDependsOnDef( + RangeSsaDefinition phi, StackVariable v, RangeSsaDefinition srcDef, StackVariable srcVar + ) { + exists(VariableAccess access, Expr guard | phi.isGuardPhi(v, access, guard, _) | + exprDependsOnDef(guard.(ComparisonOperation).getAnOperand(), srcDef, srcVar) or + exprDependsOnDef(access, srcDef, srcVar) + ) + or + srcDef = phi.getAPhiInput(v) and srcVar = v + } + + /** The transitive closure of `defDependsOnDef`. */ + private predicate defDependsOnDefTransitively( + RangeSsaDefinition def, StackVariable v, RangeSsaDefinition srcDef, StackVariable srcVar + ) { + defDependsOnDef(def, v, srcDef, srcVar) + or + exists(RangeSsaDefinition midDef, StackVariable midVar | + defDependsOnDef(def, v, midDef, midVar) + | + defDependsOnDefTransitively(midDef, midVar, srcDef, srcVar) + ) + } + + /** The set of definitions that depend recursively on themselves. */ + private predicate isRecursiveDef(RangeSsaDefinition def, StackVariable v) { + defDependsOnDefTransitively(def, v, def, v) + } + + /** + * Holds if the bounds of `e` depend on a recursive definition, meaning that + * `e` is likely to have many candidate bounds during the main recursion. + */ + private predicate isRecursiveExpr(Expr e) { + exists(RangeSsaDefinition def, StackVariable v | exprDependsOnDef(e, def, v) | + isRecursiveDef(def, v) + ) + } + + /** + * Holds if `binop` is a binary operation that's likely to be assigned a + * quadratic (or more) number of candidate bounds during the analysis. This can + * happen when two conditions are satisfied: + * 1. It is likely there are many more candidate bounds for `binop` than for + * its operands. For example, the number of candidate bounds for `x + y`, + * denoted here nbounds(`x + y`), will be O(nbounds(`x`) * nbounds(`y`)). + * In contrast, nbounds(`b ? x : y`) is only O(nbounds(`x`) + nbounds(`y`)). + * 2. Both operands of `binop` are recursively determined and are therefore + * likely to have a large number of candidate bounds. + */ + private predicate isRecursiveBinary(BinaryOperation binop) { + ( + binop instanceof UnsignedMulExpr + or + binop instanceof AddExpr + or + binop instanceof SubExpr + ) and + isRecursiveExpr(binop.getLeftOperand()) and + isRecursiveExpr(binop.getRightOperand()) + } + + /** + * We distinguish 3 kinds of RangeSsaDefinition: + * + * 1. Definitions with a defining value. + * For example: x = y+3 is a definition of x with defining value y+3. + * + * 2. Phi nodes: x3 = phi(x0,x1,x2) + * + * 3. Unanalyzable definitions. + * For example: a parameter is unanalyzable because we know nothing + * about its value. We assign these range [-largeValue(), largeValue()] + * + * This predicate finds all the definitions in the first set. + */ + private predicate assignmentDef(RangeSsaDefinition def, StackVariable v, Expr expr) { + Util::getVariableRangeType(v) instanceof ArithmeticType and + ( + def = v.getInitializer().getExpr() and def = expr + or + exists(AssignExpr assign | + def = assign and + assign.getLValue() = v.getAnAccess() and + expr = assign.getRValue() + ) + ) + } + + /** See comment above assignmentDef. */ + private predicate analyzableDef(RangeSsaDefinition def, StackVariable v) { + assignmentDef(def, v, _) + or + analyzableExpr(def.(AssignOperation)) and + v = def.getAVariable() + or + analyzableExpr(def.(CrementOperation)) and + v = def.getAVariable() + or + phiDependsOnDef(def, v, _, _) + } + + /** + * Computes a normal form of `x` where -0.0 has changed to +0.0. This can be + * needed on the lesser side of a floating-point comparison or on both sides of + * a floating point equality because QL does not follow IEEE in floating-point + * comparisons but instead defines -0.0 to be less than and distinct from 0.0. + */ + bindingset[x] + private float normalizeFloatUp(float x) { result = x + 0.0 } + + /** + * Computes `x + y`, rounded towards +Inf. This is the general case where both + * `x` and `y` may be large numbers. + */ + bindingset[x, y] + private float addRoundingUp(float x, float y) { + if normalizeFloatUp((x + y) - x) < y or normalizeFloatUp((x + y) - y) < x + then result = (x + y).nextUp() + else result = (x + y) + } + + /** + * Computes `x + y`, rounded towards -Inf. This is the general case where both + * `x` and `y` may be large numbers. + */ + bindingset[x, y] + private float addRoundingDown(float x, float y) { + if (x + y) - x > normalizeFloatUp(y) or (x + y) - y > normalizeFloatUp(x) + then result = (x + y).nextDown() + else result = (x + y) + } + + /** + * Computes `x + small`, rounded towards +Inf, where `small` is a small + * constant. + */ + bindingset[x, small] + private float addRoundingUpSmall(float x, float small) { + if (x + small) - x < small then result = (x + small).nextUp() else result = (x + small) + } + + /** + * Computes `x + small`, rounded towards -Inf, where `small` is a small + * constant. + */ + bindingset[x, small] + private float addRoundingDownSmall(float x, float small) { + if (x + small) - x > small then result = (x + small).nextDown() else result = (x + small) + } + + private predicate lowerBoundableExpr(Expr expr) { + (analyzableExpr(expr) or dividesByZero(expr)) and + getUpperBoundsImpl(expr) <= Util::exprMaxVal(expr) and + not exists(getValue(expr).toFloat()) + } + + /** + * Gets the lower bounds of the expression. + * + * Most of the work of computing the lower bounds is done by + * `getLowerBoundsImpl`. However, the lower bounds computed by + * `getLowerBoundsImpl` may not be representable by the result type of the + * expression. For example, if `x` and `y` are of type `int32` and each + * have lower bound -2147483648, then getLowerBoundsImpl` will compute a + * lower bound -4294967296 for the expression `x+y`, even though + * -4294967296 cannot be represented as an `int32`. Such unrepresentable + * bounds are replaced with `exprMinVal(expr)`. This predicate also adds + * `exprMinVal(expr)` as a lower bound if the expression might overflow + * positively, or if it is unanalyzable. + * + * Note: most callers should use `getFullyConvertedLowerBounds` rather than + * this predicate. + */ + private float getTruncatedLowerBounds(Expr expr) { + // If the expression evaluates to a constant, then there is no + // need to call getLowerBoundsImpl. + analyzableExpr(expr) and + result = getValue(expr).toFloat() + or + // Some of the bounds computed by getLowerBoundsImpl might + // overflow, so we replace invalid bounds with exprMinVal. + exists(float newLB | newLB = normalizeFloatUp(getLowerBoundsImpl(expr)) | + if Util::exprMinVal(expr) <= newLB and newLB <= Util::exprMaxVal(expr) + then + // Apply widening where we might get a combinatorial explosion. + if isRecursiveBinary(expr) + then + result = + max(float widenLB | + widenLB = wideningLowerBounds(expr.getUnspecifiedType()) and + not widenLB > newLB + ) + else result = newLB + else result = Util::exprMinVal(expr) + ) and + lowerBoundableExpr(expr) + or + // The expression might overflow and wrap. If so, the + // lower bound is exprMinVal. + analyzableExpr(expr) and + exprMightOverflowPositively(expr) and + not result = getValue(expr).toFloat() and + result = Util::exprMinVal(expr) + or + // The expression is not analyzable, so its lower bound is + // unknown. Note that the call to exprMinVal restricts the + // expressions to just those with arithmetic types. There is no + // need to return results for non-arithmetic expressions. + not analyzableExpr(expr) and + result = exprMinVal(expr) + } + + /** + * Gets the upper bounds of the expression. + * + * Most of the work of computing the upper bounds is done by + * `getUpperBoundsImpl`. However, the upper bounds computed by + * `getUpperBoundsImpl` may not be representable by the result type of the + * expression. For example, if `x` and `y` are of type `int32` and each + * have upper bound 2147483647, then getUpperBoundsImpl` will compute an + * upper bound 4294967294 for the expression `x+y`, even though 4294967294 + * cannot be represented as an `int32`. Such unrepresentable bounds are + * replaced with `exprMaxVal(expr)`. This predicate also adds + * `exprMaxVal(expr)` as an upper bound if the expression might overflow + * negatively, or if it is unanalyzable. + * + * Note: most callers should use `getFullyConvertedUpperBounds` rather than + * this predicate. + */ + private float getTruncatedUpperBounds(Expr expr) { + (analyzableExpr(expr) or dividesByZero(expr)) + and ( + // If the expression evaluates to a constant, then there is no + // need to call getUpperBoundsImpl. + if exists(getValue(expr).toFloat()) + then result = getValue(expr).toFloat() + else ( + // Some of the bounds computed by `getUpperBoundsImpl` + // might overflow, so we replace invalid bounds with + // `exprMaxVal`. + exists(float newUB | newUB = normalizeFloatUp(getUpperBoundsImpl(expr)) | + if Util::exprMinVal(expr) <= newUB and newUB <= Util::exprMaxVal(expr) + then + // Apply widening where we might get a combinatorial explosion. + if isRecursiveBinary(expr) + then + result = + min(float widenUB | + widenUB = wideningUpperBounds(expr.getUnspecifiedType()) and + not widenUB < newUB + ) + else result = newUB + else result = Util::exprMaxVal(expr) + ) + or + // The expression might overflow negatively and wrap. If so, + // the upper bound is `exprMaxVal`. + exprMightOverflowNegatively(expr) and + result = Util::exprMaxVal(expr) + ) + ) or + not analyzableExpr(expr) and + // The expression is not analyzable, so its upper bound is + // unknown. Note that the call to exprMaxVal restricts the + // expressions to just those with arithmetic types. There is no + // need to return results for non-arithmetic expressions. + result = exprMaxVal(expr) + } + + /** Only to be called by `getTruncatedLowerBounds`. */ + private float getLowerBoundsImpl(Expr expr) { + ( + exists(Expr operand, float operandLow, float positive | + effectivelyMultipliesByPositive(expr, operand, positive) and + operandLow = getFullyConvertedLowerBounds(operand) and + result = positive * operandLow + ) + or + exists(Expr operand, float operandHigh, float negative | + effectivelyMultipliesByNegative(expr, operand, negative) and + operandHigh = getFullyConvertedUpperBounds(operand) and + result = negative * operandHigh + ) + or + exists(Expr operand, float operandLow, float positive | + dividesByPositive(expr, operand, positive) and + operandLow = getFullyConvertedLowerBounds(operand) and + result = operandLow / positive + ) + or + exists(Expr operand, float operandLow, float negative | + dividesByNegative(expr, operand, negative) and + operandLow = getFullyConvertedUpperBounds(operand) and + result = operandLow / negative + ) + or + exists(DivExpr div | expr = div | + dividesByZero(expr) and + result = getFullyConvertedLowerBounds(div.getLeftOperand()) / 0 + ) + or + exists(MinExpr minExpr | + expr = minExpr and + // Return the union of the lower bounds from both children. + result = getFullyConvertedLowerBounds(minExpr.getAnOperand()) + ) + or + exists(MaxExpr maxExpr | + expr = maxExpr and + // Compute the cross product of the bounds from both children. We are + // using this mathematical property: + // + // max (minimum{X}, minimum{Y}) + // = minimum { max(x,y) | x in X, y in Y } + exists(float x, float y | + x = getFullyConvertedLowerBounds(maxExpr.getLeftOperand()) and + y = getFullyConvertedLowerBounds(maxExpr.getRightOperand()) and + if x >= y then result = x else result = y + ) + ) + or + // ConditionalExpr (true branch) + exists(ConditionalExpr condExpr | + expr = condExpr and + // Use `boolConversionUpperBound` to determine whether the condition + // might evaluate to `true`. + boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1 and + result = getFullyConvertedLowerBounds(condExpr.getThen()) + ) + or + // ConditionalExpr (false branch) + exists(ConditionalExpr condExpr | + expr = condExpr and + // Use `boolConversionLowerBound` to determine whether the condition + // might evaluate to `false`. + boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0 and + result = getFullyConvertedLowerBounds(condExpr.getElse()) + ) + or + exists(AddExpr addExpr, float xLow, float yLow | + expr = addExpr and + xLow = getFullyConvertedLowerBounds(addExpr.getLeftOperand()) and + yLow = getFullyConvertedLowerBounds(addExpr.getRightOperand()) and + result = addRoundingDown(xLow, yLow) + ) + or + exists(SubExpr subExpr, float xLow, float yHigh | + expr = subExpr and + xLow = getFullyConvertedLowerBounds(subExpr.getLeftOperand()) and + yHigh = getFullyConvertedUpperBounds(subExpr.getRightOperand()) and + result = addRoundingDown(xLow, -yHigh) + ) + or + exists(UnsignedMulExpr mulExpr, float xLow, float yLow | + expr = mulExpr and + xLow = getFullyConvertedLowerBounds(mulExpr.getLeftOperand()) and + yLow = getFullyConvertedLowerBounds(mulExpr.getRightOperand()) and + result = xLow * yLow + ) + or + exists(AssignExpr assign | + expr = assign and + result = getFullyConvertedLowerBounds(assign.getRValue()) + ) + or + exists(AssignAddExpr addExpr, float xLow, float yLow | + expr = addExpr and + xLow = getFullyConvertedLowerBounds(addExpr.getLValue()) and + yLow = getFullyConvertedLowerBounds(addExpr.getRValue()) and + result = addRoundingDown(xLow, yLow) + ) + or + exists(AssignSubExpr subExpr, float xLow, float yHigh | + expr = subExpr and + xLow = getFullyConvertedLowerBounds(subExpr.getLValue()) and + yHigh = getFullyConvertedUpperBounds(subExpr.getRValue()) and + result = addRoundingDown(xLow, -yHigh) + ) + or + exists(UnsignedAssignMulExpr mulExpr, float xLow, float yLow | + expr = mulExpr and + xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and + yLow = getFullyConvertedLowerBounds(mulExpr.getRValue()) and + result = xLow * yLow + ) + or + exists(AssignMulByPositiveConstantExpr mulExpr, float xLow | + expr = mulExpr and + xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and + result = xLow * mulExpr.getConstant() + ) + or + exists(AssignMulByNegativeConstantExpr mulExpr, float xHigh | + expr = mulExpr and + xHigh = getFullyConvertedUpperBounds(mulExpr.getLValue()) and + result = xHigh * mulExpr.getConstant() + ) + or + exists(PrefixIncrExpr incrExpr, float xLow | + expr = incrExpr and + xLow = getFullyConvertedLowerBounds(incrExpr.getOperand()) and + result = xLow + 1 + ) + or + exists(PrefixDecrExpr decrExpr, float xLow | + expr = decrExpr and + xLow = getFullyConvertedLowerBounds(decrExpr.getOperand()) and + result = addRoundingDownSmall(xLow, -1) + ) + or + // `PostfixIncrExpr` and `PostfixDecrExpr` return the value of their + // operand. The incrementing/decrementing behavior is handled in + // `getDefLowerBoundsImpl`. + exists(PostfixIncrExpr incrExpr | + expr = incrExpr and + result = getFullyConvertedLowerBounds(incrExpr.getOperand()) + ) + or + exists(PostfixDecrExpr decrExpr | + expr = decrExpr and + result = getFullyConvertedLowerBounds(decrExpr.getOperand()) + ) + or + exists(RemExpr remExpr | expr = remExpr | + // If both inputs are positive then the lower bound is zero. + result = 0 + or + // If either input could be negative then the output could be + // negative. If so, the lower bound of `x%y` is `-abs(y) + 1`, which is + // equal to `min(-y + 1,y - 1)`. + exists(float childLB | + childLB = getFullyConvertedLowerBounds(remExpr.getAnOperand()) and + not childLB >= 0 + | + result = getFullyConvertedLowerBounds(remExpr.getRightOperand()) - 1 + or + exists(float rhsUB | rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand()) | + result = -rhsUB + 1 + ) + ) + ) + or + // If the conversion is to an arithmetic type then we just return the + // lower bound of the child. We do not need to handle truncation and + // overflow here, because that is done in `getTruncatedLowerBounds`. + // Conversions to `bool` need to be handled specially because they test + // whether the value of the expression is equal to 0. + exists(Conversion convExpr | expr = convExpr | + if convExpr.getUnspecifiedType() instanceof BoolType + then result = boolConversionLowerBound(convExpr.getExpr()) + else result = getTruncatedLowerBounds(convExpr.getExpr()) + ) + or + // Use SSA to get the lower bounds for a variable use. + exists(RangeSsaDefinition def, StackVariable v | expr = def.getAUse(v) | + result = getDefLowerBounds(def, v) + ) + or + // unsigned `&` (tighter bounds may exist) + exists(UnsignedBitwiseAndExpr andExpr | + andExpr = expr and + result = 0.0 + ) + or + // `>>` by a constant + exists(RShiftExpr rsExpr, float left, int right | + rsExpr = expr and + left = getFullyConvertedLowerBounds(rsExpr.getLeftOperand()) and + right = getValue(rsExpr.getRightOperand().getFullyConverted()).toInt() and + result = safeFloor(left / 2.pow(right)) + ) + ) + } + + /** Only to be called by `getTruncatedUpperBounds`. */ + private float getUpperBoundsImpl(Expr expr) { + ( + exists(Expr operand, float operandHigh, float positive | + effectivelyMultipliesByPositive(expr, operand, positive) and + operandHigh = getFullyConvertedUpperBounds(operand) and + result = positive * operandHigh + ) + or + exists(Expr operand, float operandLow, float negative | + effectivelyMultipliesByNegative(expr, operand, negative) and + operandLow = getFullyConvertedLowerBounds(operand) and + result = negative * operandLow + ) + or + exists(Expr operand, float operandHigh, float positive | + dividesByPositive(expr, operand, positive) and + operandHigh = getFullyConvertedUpperBounds(operand) and + result = operandHigh / positive + ) + or + exists(Expr operand, float operandHigh, float negative | + dividesByNegative(expr, operand, negative) and + operandHigh = getFullyConvertedLowerBounds(operand) and + result = operandHigh / negative + ) + or + exists(DivExpr div | expr = div | + dividesByZero(expr) and + result = getFullyConvertedUpperBounds(div.getLeftOperand()) / 0 + ) + or + exists(MaxExpr maxExpr | + expr = maxExpr and + // Return the union of the upper bounds from both children. + result = getFullyConvertedUpperBounds(maxExpr.getAnOperand()) + ) + or + exists(MinExpr minExpr | + expr = minExpr and + // Compute the cross product of the bounds from both children. We are + // using this mathematical property: + // + // min (maximum{X}, maximum{Y}) + // = maximum { min(x,y) | x in X, y in Y } + exists(float x, float y | + x = getFullyConvertedUpperBounds(minExpr.getLeftOperand()) and + y = getFullyConvertedUpperBounds(minExpr.getRightOperand()) and + if x <= y then result = x else result = y + ) + ) + or + // ConditionalExpr (true branch) + exists(ConditionalExpr condExpr | + expr = condExpr and + // Use `boolConversionUpperBound` to determine whether the condition + // might evaluate to `true`. + boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1 and + result = getFullyConvertedUpperBounds(condExpr.getThen()) + ) + or + // ConditionalExpr (false branch) + exists(ConditionalExpr condExpr | + expr = condExpr and + // Use `boolConversionLowerBound` to determine whether the condition + // might evaluate to `false`. + boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0 and + result = getFullyConvertedUpperBounds(condExpr.getElse()) + ) + or + exists(AddExpr addExpr, float xHigh, float yHigh | + expr = addExpr and + xHigh = getFullyConvertedUpperBounds(addExpr.getLeftOperand()) and + yHigh = getFullyConvertedUpperBounds(addExpr.getRightOperand()) and + result = addRoundingUp(xHigh, yHigh) + ) + or + exists(SubExpr subExpr, float xHigh, float yLow | + expr = subExpr and + xHigh = getFullyConvertedUpperBounds(subExpr.getLeftOperand()) and + yLow = getFullyConvertedLowerBounds(subExpr.getRightOperand()) and + result = addRoundingUp(xHigh, -yLow) + ) + or + exists(UnsignedMulExpr mulExpr, float xHigh, float yHigh | + expr = mulExpr and + xHigh = getFullyConvertedUpperBounds(mulExpr.getLeftOperand()) and + yHigh = getFullyConvertedUpperBounds(mulExpr.getRightOperand()) and + result = xHigh * yHigh + ) + or + exists(AssignExpr assign | + expr = assign and + result = getFullyConvertedUpperBounds(assign.getRValue()) + ) + or + exists(AssignAddExpr addExpr, float xHigh, float yHigh | + expr = addExpr and + xHigh = getFullyConvertedUpperBounds(addExpr.getLValue()) and + yHigh = getFullyConvertedUpperBounds(addExpr.getRValue()) and + result = addRoundingUp(xHigh, yHigh) + ) + or + exists(AssignSubExpr subExpr, float xHigh, float yLow | + expr = subExpr and + xHigh = getFullyConvertedUpperBounds(subExpr.getLValue()) and + yLow = getFullyConvertedLowerBounds(subExpr.getRValue()) and + result = addRoundingUp(xHigh, -yLow) + ) + or + exists(UnsignedAssignMulExpr mulExpr, float xHigh, float yHigh | + expr = mulExpr and + xHigh = getFullyConvertedUpperBounds(mulExpr.getLValue()) and + yHigh = getFullyConvertedUpperBounds(mulExpr.getRValue()) and + result = xHigh * yHigh + ) + or + exists(AssignMulByPositiveConstantExpr mulExpr, float xHigh | + expr = mulExpr and + xHigh = getFullyConvertedUpperBounds(mulExpr.getLValue()) and + result = xHigh * mulExpr.getConstant() + ) + or + exists(AssignMulByNegativeConstantExpr mulExpr, float xLow | + expr = mulExpr and + xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and + result = xLow * mulExpr.getConstant() + ) + or + exists(PrefixIncrExpr incrExpr, float xHigh | + expr = incrExpr and + xHigh = getFullyConvertedUpperBounds(incrExpr.getOperand()) and + result = addRoundingUpSmall(xHigh, 1) + ) + or + exists(PrefixDecrExpr decrExpr, float xHigh | + expr = decrExpr and + xHigh = getFullyConvertedUpperBounds(decrExpr.getOperand()) and + result = xHigh - 1 + ) + or + // `PostfixIncrExpr` and `PostfixDecrExpr` return the value of their operand. + // The incrementing/decrementing behavior is handled in + // `getDefUpperBoundsImpl`. + exists(PostfixIncrExpr incrExpr | + expr = incrExpr and + result = getFullyConvertedUpperBounds(incrExpr.getOperand()) + ) + or + exists(PostfixDecrExpr decrExpr | + expr = decrExpr and + result = getFullyConvertedUpperBounds(decrExpr.getOperand()) + ) + or + exists(RemExpr remExpr, float rhsUB | + expr = remExpr and + rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand()) + | + result = rhsUB - 1 + or + // If the right hand side could be negative then we need to take its + // absolute value. Since `abs(x) = max(-x,x)` this is equivalent to + // adding `-rhsLB` to the set of upper bounds. + exists(float rhsLB | + rhsLB = getFullyConvertedLowerBounds(remExpr.getRightOperand()) and + not rhsLB >= 0 + | + result = -rhsLB + 1 + ) + ) + or + // If the conversion is to an arithmetic type then we just return the + // upper bound of the child. We do not need to handle truncation and + // overflow here, because that is done in `getTruncatedUpperBounds`. + // Conversions to `bool` need to be handled specially because they test + // whether the value of the expression is equal to 0. + exists(Conversion convExpr | expr = convExpr | + if convExpr.getUnspecifiedType() instanceof BoolType + then result = boolConversionUpperBound(convExpr.getExpr()) + else result = getTruncatedUpperBounds(convExpr.getExpr()) + ) + or + // Use SSA to get the upper bounds for a variable use. + exists(RangeSsaDefinition def, StackVariable v | expr = def.getAUse(v) | + result = getDefUpperBounds(def, v) + ) + or + // unsigned `&` (tighter bounds may exist) + exists(UnsignedBitwiseAndExpr andExpr, float left, float right | + andExpr = expr and + left = getFullyConvertedUpperBounds(andExpr.getLeftOperand()) and + right = getFullyConvertedUpperBounds(andExpr.getRightOperand()) and + result = left.minimum(right) + ) + or + // `>>` by a constant + exists(RShiftExpr rsExpr, float left, int right | + rsExpr = expr and + left = getFullyConvertedUpperBounds(rsExpr.getLeftOperand()) and + right = getValue(rsExpr.getRightOperand().getFullyConverted()).toInt() and + result = safeFloor(left / 2.pow(right)) + ) + ) + } + + /** + * Holds if `expr` is converted to `bool` or if it is the child of a + * logical operation. + * + * The purpose of this predicate is to optimize `boolConversionLowerBound` + * and `boolConversionUpperBound` by preventing them from computing + * unnecessary results. In other words, `exprIsUsedAsBool(expr)` holds if + * `expr` is an expression that might be passed as an argument to + * `boolConversionLowerBound` or `boolConversionUpperBound`. + */ + private predicate exprIsUsedAsBool(Expr expr) { + expr = any(BinaryLogicalOperation op).getAnOperand().getFullyConverted() + or + expr = any(UnaryLogicalOperation op).getOperand().getFullyConverted() + or + expr = any(ConditionalExpr c).getCondition().getFullyConverted() + or + exists(Conversion cast | cast.getUnspecifiedType() instanceof BoolType | expr = cast.getExpr()) + } + + /** + * Gets the lower bound of the conversion `(bool)expr`. If we can prove that + * the value of `expr` is never 0 then `lb = 1`. Otherwise `lb = 0`. + */ + private float boolConversionLowerBound(Expr expr) { + // Case 1: if the range for `expr` includes the value 0, + // then `result = 0`. + exprIsUsedAsBool(expr) and + exists(float lb | lb = getTruncatedLowerBounds(expr) and not lb > 0) and + exists(float ub | ub = getTruncatedUpperBounds(expr) and not ub < 0) and + result = 0 + or + // Case 2a: if the range for `expr` does not include the value 0, + // then `result = 1`. + exprIsUsedAsBool(expr) and getTruncatedLowerBounds(expr) > 0 and result = 1 + or + // Case 2b: if the range for `expr` does not include the value 0, + // then `result = 1`. + exprIsUsedAsBool(expr) and getTruncatedUpperBounds(expr) < 0 and result = 1 + or + // Case 3: the type of `expr` is not arithmetic. For example, it might + // be a pointer. + exprIsUsedAsBool(expr) and not exists(Util::exprMinVal(expr)) and result = 0 + } + + /** + * Gets the upper bound of the conversion `(bool)expr`. If we can prove that + * the value of `expr` is always 0 then `ub = 0`. Otherwise `ub = 1`. + */ + private float boolConversionUpperBound(Expr expr) { + // Case 1a: if the upper bound of the operand is <= 0, then the upper + // bound might be 0. + exprIsUsedAsBool(expr) and getTruncatedUpperBounds(expr) <= 0 and result = 0 + or + // Case 1b: if the upper bound of the operand is not <= 0, then the upper + // bound is 1. + exprIsUsedAsBool(expr) and + exists(float ub | ub = getTruncatedUpperBounds(expr) and not ub <= 0) and + result = 1 + or + // Case 2a: if the lower bound of the operand is >= 0, then the upper + // bound might be 0. + exprIsUsedAsBool(expr) and getTruncatedLowerBounds(expr) >= 0 and result = 0 + or + // Case 2b: if the lower bound of the operand is not >= 0, then the upper + // bound is 1. + exprIsUsedAsBool(expr) and + exists(float lb | lb = getTruncatedLowerBounds(expr) and not lb >= 0) and + result = 1 + or + // Case 3: the type of `expr` is not arithmetic. For example, it might + // be a pointer. + exprIsUsedAsBool(expr) and not exists(Util::exprMaxVal(expr)) and result = 1 + } + + /** + * This predicate computes the lower bounds of a phi definition. If the + * phi definition corresponds to a guard, then the guard is used to + * deduce a better lower bound. + * For example: + * + * def: x = y % 10; + * guard: if (x >= 2) { + * block: f(x) + * } + * + * In this example, the lower bound of x is 0, but we can + * use the guard to deduce that the lower bound is 2 inside the block. + */ + private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) { + exists(VariableAccess access, Expr guard, boolean branch, float defLB, float guardLB | + phi.isGuardPhi(v, access, guard, branch) and + lowerBoundFromGuard(guard, access, guardLB, branch) and + defLB = getFullyConvertedLowerBounds(access) + | + // Compute the maximum of `guardLB` and `defLB`. + if guardLB > defLB then result = guardLB else result = defLB + ) + or + exists(VariableAccess access, float neConstant, float lower | + isNEPhi(v, phi, access, neConstant) and + lower = getTruncatedLowerBounds(access) and + if lower = neConstant then result = lower + 1 else result = lower + ) + or + exists(VariableAccess access | + isUnsupportedGuardPhi(v, phi, access) and + result = getTruncatedLowerBounds(access) + ) + or + result = getDefLowerBounds(phi.getAPhiInput(v), v) + } + + /** See comment for `getPhiLowerBounds`, above. */ + private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) { + exists(VariableAccess access, Expr guard, boolean branch, float defUB, float guardUB | + phi.isGuardPhi(v, access, guard, branch) and + upperBoundFromGuard(guard, access, guardUB, branch) and + defUB = getFullyConvertedUpperBounds(access) + | + // Compute the minimum of `guardUB` and `defUB`. + if guardUB < defUB then result = guardUB else result = defUB + ) + or + exists(VariableAccess access, float neConstant, float upper | + isNEPhi(v, phi, access, neConstant) and + upper = getTruncatedUpperBounds(access) and + if upper = neConstant then result = upper - 1 else result = upper + ) + or + exists(VariableAccess access | + isUnsupportedGuardPhi(v, phi, access) and + result = getTruncatedUpperBounds(access) + ) + or + result = getDefUpperBounds(phi.getAPhiInput(v), v) + } + + /** Only to be called by `getDefLowerBounds`. */ + private float getDefLowerBoundsImpl(RangeSsaDefinition def, StackVariable v) { + // Definitions with a defining value. + exists(Expr expr | assignmentDef(def, v, expr) | result = getFullyConvertedLowerBounds(expr)) + or + // Assignment operations with a defining value + exists(AssignOperation assignOp | + def = assignOp and + assignOp.getLValue() = v.getAnAccess() and + result = getTruncatedLowerBounds(assignOp) + ) + or + exists(IncrementOperation incr, float newLB | + def = incr and + incr.getOperand() = v.getAnAccess() and + newLB = getFullyConvertedLowerBounds(incr.getOperand()) and + result = newLB + 1 + ) + or + exists(DecrementOperation decr, float newLB | + def = decr and + decr.getOperand() = v.getAnAccess() and + newLB = getFullyConvertedLowerBounds(decr.getOperand()) and + result = addRoundingDownSmall(newLB, -1) + ) + or + // Phi nodes. + result = getPhiLowerBounds(v, def) + or + // Unanalyzable definitions. + unanalyzableDefBounds(def, v, result, _) + } + + /** Only to be called by `getDefUpperBounds`. */ + private float getDefUpperBoundsImpl(RangeSsaDefinition def, StackVariable v) { + // Definitions with a defining value. + exists(Expr expr | assignmentDef(def, v, expr) | result = getFullyConvertedUpperBounds(expr)) + or + // Assignment operations with a defining value + exists(AssignOperation assignOp | + def = assignOp and + assignOp.getLValue() = v.getAnAccess() and + result = getTruncatedUpperBounds(assignOp) + ) + or + exists(IncrementOperation incr, float newUB | + def = incr and + incr.getOperand() = v.getAnAccess() and + newUB = getFullyConvertedUpperBounds(incr.getOperand()) and + result = addRoundingUpSmall(newUB, 1) + ) + or + exists(DecrementOperation decr, float newUB | + def = decr and + decr.getOperand() = v.getAnAccess() and + newUB = getFullyConvertedUpperBounds(decr.getOperand()) and + result = newUB - 1 + ) + or + // Phi nodes. + result = getPhiUpperBounds(v, def) + or + // Unanalyzable definitions. + unanalyzableDefBounds(def, v, _, result) + } + + /** + * Helper for `getDefLowerBounds` and `getDefUpperBounds`. Find the set of + * unanalyzable definitions (such as function parameters) and make their + * bounds unknown. + */ + private predicate unanalyzableDefBounds( + RangeSsaDefinition def, StackVariable v, float lb, float ub + ) { + v = def.getAVariable() and + not analyzableDef(def, v) and + lb = varMinVal(v) and + ub = varMaxVal(v) + } + + /** + * Holds if in the `branch` branch of a guard `guard` involving `v`, + * we know that `v` is not NaN, and therefore it is safe to make range + * inferences about `v`. + */ + bindingset[guard, v, branch] + predicate nonNanGuardedVariable(Expr guard, VariableAccess v, boolean branch) { + Util::getVariableRangeType(v.getTarget()) instanceof IntegralType + or + Util::getVariableRangeType(v.getTarget()) instanceof FloatingPointType and + v instanceof NonNanVariableAccess + or + // The reason the following case is here is to ensure that when we say + // `if (x > 5) { ...then... } else { ...else... }` + // it is ok to conclude that `x > 5` in the `then`, (though not safe + // to conclude that x <= 5 in `else`) even if we had no prior + // knowledge of `x` not being `NaN`. + nanExcludingComparison(guard, branch) + } + + /** + * If the guard is a comparison of the form `p*v + q r`, then this + * predicate uses the bounds information for `r` to compute a lower bound + * for `v`. + */ + private predicate lowerBoundFromGuard(Expr guard, VariableAccess v, float lb, boolean branch) { + exists(float childLB, Util::RelationStrictness strictness | + boundFromGuard(guard, v, childLB, true, strictness, branch) + | + if nonNanGuardedVariable(guard, v, branch) + then + if + strictness = Util::Nonstrict() or + not Util::getVariableRangeType(v.getTarget()) instanceof IntegralType + then lb = childLB + else lb = childLB + 1 + else lb = varMinVal(v.getTarget()) + ) + } + + /** + * If the guard is a comparison of the form `p*v + q r`, then this + * predicate uses the bounds information for `r` to compute a upper bound + * for `v`. + */ + private predicate upperBoundFromGuard(Expr guard, VariableAccess v, float ub, boolean branch) { + exists(float childUB, Util::RelationStrictness strictness | + boundFromGuard(guard, v, childUB, false, strictness, branch) + | + if nonNanGuardedVariable(guard, v, branch) + then + if + strictness = Util::Nonstrict() or + not Util::getVariableRangeType(v.getTarget()) instanceof IntegralType + then ub = childUB + else ub = childUB - 1 + else ub = varMaxVal(v.getTarget()) + ) + } + + /** + * This predicate simplifies the results returned by + * `linearBoundFromGuard`. + */ + private predicate boundFromGuard( + Expr guard, VariableAccess v, float boundValue, boolean isLowerBound, + Util::RelationStrictness strictness, boolean branch + ) { + exists(float p, float q, float r, boolean isLB | + linearBoundFromGuard(guard, v, p, q, r, isLB, strictness, branch) and + boundValue = (r - q) / p + | + // If the multiplier is negative then the direction of the comparison + // needs to be flipped. + p > 0 and isLowerBound = isLB + or + p < 0 and isLowerBound = isLB.booleanNot() + ) + or + // When `!e` is true, we know that `0 <= e <= 0` + exists(float p, float q, Expr e | + Util::linearAccess(e, v, p, q) and + Util::eqZeroWithNegate(guard, e, true, branch) and + boundValue = (0.0 - q) / p and + isLowerBound = [false, true] and + strictness = Util::Nonstrict() + ) + } + + /** + * This predicate finds guards of the form `p*v + q < r or p*v + q == r` + * and decomposes them into a tuple of values which can be used to deduce a + * lower or upper bound for `v`. + */ + private predicate linearBoundFromGuard( + ComparisonOperation guard, VariableAccess v, float p, float q, float boundValue, + boolean isLowerBound, // Is this a lower or an upper bound? + Util::RelationStrictness strictness, boolean branch // Which control-flow branch is this bound valid on? + ) { + // For the comparison x < RHS, we create two bounds: + // + // 1. x < upperbound(RHS) + // 2. x >= typeLowerBound(RHS.getUnspecifiedType()) + // + exists(Expr lhs, Expr rhs, Util::RelationDirection dir, Util::RelationStrictness st | + Util::linearAccess(lhs, v, p, q) and + Util::relOpWithSwapAndNegate(guard, lhs, rhs, dir, st, branch) + | + isLowerBound = Util::directionIsGreater(dir) and + strictness = st and + getBounds(rhs, boundValue, isLowerBound) + or + isLowerBound = Util::directionIsLesser(dir) and + strictness = Util::Nonstrict() and + exprTypeBounds(rhs, boundValue, isLowerBound) + ) + or + // For x == RHS, we create the following bounds: + // + // 1. x <= upperbound(RHS) + // 2. x >= lowerbound(RHS) + // + exists(Expr lhs, Expr rhs | + Util::linearAccess(lhs, v, p, q) and + Util::eqOpWithSwapAndNegate(guard, lhs, rhs, true, branch) and + getBounds(rhs, boundValue, isLowerBound) and + strictness = Util::Nonstrict() + ) + // x != RHS and !x are handled elsewhere + } + + /** Utility for `linearBoundFromGuard`. */ + private predicate getBounds(Expr expr, float boundValue, boolean isLowerBound) { + isLowerBound = true and boundValue = getFullyConvertedLowerBounds(expr) + or + isLowerBound = false and boundValue = getFullyConvertedUpperBounds(expr) + } + + /** Utility for `linearBoundFromGuard`. */ + private predicate exprTypeBounds(Expr expr, float boundValue, boolean isLowerBound) { + isLowerBound = true and boundValue = exprMinVal(expr.getFullyConverted()) + or + isLowerBound = false and boundValue = exprMaxVal(expr.getFullyConverted()) + } + + /** + * Holds if `(v, phi)` ensures that `access` is not equal to `neConstant`. For + * example, the condition `if (x + 1 != 3)` ensures that `x` is not equal to 2. + * Only integral types are supported. + */ + private predicate isNEPhi( + Variable v, RangeSsaDefinition phi, VariableAccess access, float neConstant + ) { + exists( + ComparisonOperation cmp, boolean branch, Expr linearExpr, Expr rExpr, float p, float q, + float r + | + phi.isGuardPhi(v, access, cmp, branch) and + Util::eqOpWithSwapAndNegate(cmp, linearExpr, rExpr, false, branch) and + v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!=` is too imprecise + r = getValue(rExpr).toFloat() and + Util::linearAccess(linearExpr, access, p, q) and + neConstant = (r - q) / p + ) + or + exists(Expr op, boolean branch, Expr linearExpr, float p, float q | + phi.isGuardPhi(v, access, op, branch) and + Util::eqZeroWithNegate(op, linearExpr, false, branch) and + v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!` is too imprecise + Util::linearAccess(linearExpr, access, p, q) and + neConstant = (0.0 - q) / p + ) + } + + /** + * Holds if `(v, phi)` constrains the value of `access` but in a way that + * doesn't allow this library to constrain the upper or lower bounds of + * `access`. An example is `if (x != y)` if neither `x` nor `y` is a + * compile-time constant. + */ + private predicate isUnsupportedGuardPhi(Variable v, RangeSsaDefinition phi, VariableAccess access) { + exists(Expr cmp, boolean branch | + Util::eqOpWithSwapAndNegate(cmp, _, _, false, branch) + or + Util::eqZeroWithNegate(cmp, _, false, branch) + | + phi.isGuardPhi(v, access, cmp, branch) and + not isNEPhi(v, phi, access, _) + ) + } + + /** + * Gets the upper bound of the expression, if the expression is guarded. + * An upper bound can only be found, if a guard phi node can be found, and the + * expression has only one immediate predecessor. + */ + private float getGuardedUpperBound(VariableAccess guardedAccess) { + exists( + RangeSsaDefinition def, StackVariable v, VariableAccess guardVa, Expr guard, boolean branch + | + def.isGuardPhi(v, guardVa, guard, branch) and + // If the basic block for the variable access being examined has + // more than one predecessor, the guard phi node could originate + // from one of the predecessors. This is because the guard phi + // node is attached to the block at the end of the edge and not on + // the actual edge. It is therefore not possible to determine which + // edge the guard phi node belongs to. The predicate below ensures + // that there is one predecessor, albeit somewhat conservative. + exists(unique(BasicBlock b | b = def.(BasicBlock).getAPredecessor())) and + guardedAccess = def.getAUse(v) and + result = max(float ub | upperBoundFromGuard(guard, guardVa, ub, branch)) and + not convertedExprMightOverflow(guard.getAChild+()) + ) + } + + cached + private module SimpleRangeAnalysisCached { + /** + * Gets the lower bound of the expression. + * + * Note: expressions in C/C++ are often implicitly or explicitly cast to a + * different result type. Such casts can cause the value of the expression + * to overflow or to be truncated. This predicate computes the lower bound + * of the expression without including the effect of the casts. To compute + * the lower bound of the expression after all the casts have been applied, + * call `lowerBound` like this: + * + * `lowerBound(expr.getFullyConverted())` + */ + cached + float lowerBound(Expr expr) { + // Combine the lower bounds returned by getTruncatedLowerBounds into a + // single minimum value. + result = min(float lb | lb = getTruncatedLowerBounds(expr) | lb) + } + + /** + * Gets the upper bound of the expression. + * + * Note: expressions in C/C++ are often implicitly or explicitly cast to a + * different result type. Such casts can cause the value of the expression + * to overflow or to be truncated. This predicate computes the upper bound + * of the expression without including the effect of the casts. To compute + * the upper bound of the expression after all the casts have been applied, + * call `upperBound` like this: + * + * `upperBound(expr.getFullyConverted())` + */ + cached + float upperBound(Expr expr) { + // Combine the upper bounds returned by getTruncatedUpperBounds and + // getGuardedUpperBound into a single maximum value + result = min([max(getTruncatedUpperBounds(expr)), getGuardedUpperBound(expr)]) + } + + /** Holds if the upper bound of `expr` may have been widened. This means the upper bound is in practice likely to be overly wide. */ + cached + predicate upperBoundMayBeWidened(Expr e) { + isRecursiveExpr(e) and + // Widening is not a problem if the post-analysis in `getGuardedUpperBound` has overridden the widening. + // Note that the RHS of `<` may be multi-valued. + not getGuardedUpperBound(e) < getTruncatedUpperBounds(e) + } + + /** + * Holds if `expr` has a provably empty range. For example: + * + * 10 < expr and expr < 5 + * + * The range of an expression can only be empty if it can never be + * executed. For example: + * + * if (10 < x) { + * if (x < 5) { + * // Unreachable code + * return x; // x has an empty range: 10 < x && x < 5 + * } + * } + */ + cached + predicate exprWithEmptyRange(Expr expr) { + analyzableExpr(expr) and + ( + not exists(lowerBound(expr)) or + not exists(upperBound(expr)) or + lowerBound(expr) > upperBound(expr) + ) + } + + /** Holds if the definition might overflow negatively. */ + cached + predicate defMightOverflowNegatively(RangeSsaDefinition def, StackVariable v) { + getDefLowerBoundsImpl(def, v) < Util::varMinVal(v) + } + + /** Holds if the definition might overflow positively. */ + cached + predicate defMightOverflowPositively(RangeSsaDefinition def, StackVariable v) { + getDefUpperBoundsImpl(def, v) > Util::varMaxVal(v) + } + + /** + * Holds if the definition might overflow (either positively or + * negatively). + */ + cached + predicate defMightOverflow(RangeSsaDefinition def, StackVariable v) { + defMightOverflowNegatively(def, v) or + defMightOverflowPositively(def, v) + } + + /** + * Holds if `e` is an expression where the concept of overflow makes sense. + * This predicate is used to filter out some of the unanalyzable expressions + * from `exprMightOverflowPositively` and `exprMightOverflowNegatively`. + */ + pragma[inline] + private predicate exprThatCanOverflow(Expr e) { + e instanceof UnaryArithmeticOperation or + e instanceof BinaryArithmeticOperation or + e instanceof AssignArithmeticOperation or + e instanceof LShiftExpr or + e instanceof AssignLShiftExpr + } + + /** + * Holds if the expression might overflow negatively. This predicate + * does not consider the possibility that the expression might overflow + * due to a conversion. + */ + cached + predicate exprMightOverflowNegatively(Expr expr) { + getLowerBoundsImpl(expr) < Util::exprMinVal(expr) + or + // The lower bound of the expression `x--` is the same as the lower + // bound of `x`, so the standard logic (above) does not work for + // detecting whether it might overflow. + getLowerBoundsImpl(expr.(PostfixDecrExpr)) = Util::exprMinVal(expr) + or + // We can't conclude that any unanalyzable expression might overflow. This + // is because there are many expressions that the range analysis doesn't + // handle, but where the concept of overflow doesn't make sense. + exprThatCanOverflow(expr) and not analyzableExpr(expr) + } + + /** + * Holds if the expression might overflow negatively. Conversions + * are also taken into account. For example the expression + * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than + * due to the addition. + */ + cached + predicate convertedExprMightOverflowNegatively(Expr expr) { + exprMightOverflowNegatively(expr) or + convertedExprMightOverflowNegatively(expr.getConversion()) + } + + /** + * Holds if the expression might overflow positively. This predicate + * does not consider the possibility that the expression might overflow + * due to a conversion. + */ + cached + predicate exprMightOverflowPositively(Expr expr) { + getUpperBoundsImpl(expr) > Util::exprMaxVal(expr) + or + // The upper bound of the expression `x++` is the same as the upper + // bound of `x`, so the standard logic (above) does not work for + // detecting whether it might overflow. + getUpperBoundsImpl(expr.(PostfixIncrExpr)) = Util::exprMaxVal(expr) + } + + /** + * Holds if the expression might overflow positively. Conversions + * are also taken into account. For example the expression + * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than + * due to the addition. + */ + cached + predicate convertedExprMightOverflowPositively(Expr expr) { + exprMightOverflowPositively(expr) or + convertedExprMightOverflowPositively(expr.getConversion()) + } + + /** + * Holds if the expression might overflow (either positively or + * negatively). The possibility that the expression might overflow + * due to an implicit or explicit cast is also considered. + */ + cached + predicate convertedExprMightOverflow(Expr expr) { + convertedExprMightOverflowNegatively(expr) or + convertedExprMightOverflowPositively(expr) + } + } + + /** + * Gets the truncated lower bounds of the fully converted expression. + */ + float getFullyConvertedLowerBounds(Expr expr) { + result = getTruncatedLowerBounds(expr.getFullyConverted()) + } + + /** + * Gets the truncated upper bounds of the fully converted expression. + */ + float getFullyConvertedUpperBounds(Expr expr) { + result = getTruncatedUpperBounds(expr.getFullyConverted()) + } + + /** + * Get the lower bounds for a `RangeSsaDefinition`. Most of the work is + * done by `getDefLowerBoundsImpl`, but this is where widening is applied + * to prevent the analysis from exploding due to a recursive definition. + */ + float getDefLowerBounds(RangeSsaDefinition def, StackVariable v) { + exists(float newLB, float truncatedLB | + newLB = getDefLowerBoundsImpl(def, v) and + if Util::varMinVal(v) <= newLB and newLB <= Util::varMaxVal(v) + then truncatedLB = newLB + else truncatedLB = Util::varMinVal(v) + | + // Widening: check whether the new lower bound is from a source which + // depends recursively on the current definition. + if isRecursiveDef(def, v) + then + // The new lower bound is from a recursive source, so we round + // down to one of a limited set of values to prevent the + // recursion from exploding. + result = + max(float widenLB | + widenLB = wideningLowerBounds(Util::getVariableRangeType(v)) and + not widenLB > truncatedLB + | + widenLB + ) + else result = truncatedLB + ) + or + // The definition might overflow positively and wrap. If so, the lower + // bound is `typeLowerBound`. + defMightOverflowPositively(def, v) and result = Util::varMinVal(v) + } + + /** See comment for `getDefLowerBounds`, above. */ + float getDefUpperBounds(RangeSsaDefinition def, StackVariable v) { + exists(float newUB, float truncatedUB | + newUB = getDefUpperBoundsImpl(def, v) and + if Util::varMinVal(v) <= newUB and newUB <= Util::varMaxVal(v) + then truncatedUB = newUB + else truncatedUB = Util::varMaxVal(v) + | + // Widening: check whether the new upper bound is from a source which + // depends recursively on the current definition. + if isRecursiveDef(def, v) + then + // The new upper bound is from a recursive source, so we round + // up to one of a fixed set of values to prevent the recursion + // from exploding. + result = + min(float widenUB | + widenUB = wideningUpperBounds(Util::getVariableRangeType(v)) and + not widenUB < truncatedUB + | + widenUB + ) + else result = truncatedUB + ) + or + // The definition might overflow negatively and wrap. If so, the upper + // bound is `typeUpperBound`. + defMightOverflowNegatively(def, v) and result = Util::varMaxVal(v) + } +} diff --git a/cpp/common/src/codingstandards/cpp/SimpleRangeAnalysisCustomizations.qll b/cpp/common/src/codingstandards/cpp/SimpleRangeAnalysisCustomizations.qll index 5144f63dc2..2688452d28 100644 --- a/cpp/common/src/codingstandards/cpp/SimpleRangeAnalysisCustomizations.qll +++ b/cpp/common/src/codingstandards/cpp/SimpleRangeAnalysisCustomizations.qll @@ -14,6 +14,45 @@ import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils import experimental.semmle.code.cpp.rangeanalysis.extensions.ConstantBitwiseAndExprRange private import experimental.semmle.code.cpp.models.interfaces.SimpleRangeAnalysisExpr +// Disabled, causing performance issues in grpc: +/* +private class DivByConstantExpr extends SimpleRangeAnalysisExpr, DivExpr { + float quotient; + + DivByConstantExpr() { + quotient = evaluateConstantExpr(getRightOperand()) + } + + override predicate dependsOnChild(Expr e) { + e = getLeftOperand() + } + + override float getLowerBounds() { + exists(float numerator | + result = numerator / quotient and + if (quotient > 0) then + // x / y where and y is positive scales the UB/LB. + numerator = getFullyConvertedLowerBounds(getLeftOperand()) + else + // x / -y where and -y is negative will invert and scale the UB/LB. + numerator = getFullyConvertedUpperBounds(getLeftOperand()) + ) + } + + override float getUpperBounds() { + exists(float numerator | + result = numerator / quotient and + if (quotient > 0) then + // x / y where and y is positive scales the UB/LB. + numerator = getFullyConvertedUpperBounds(getLeftOperand()) + else + // x / -y where and -y is negative will invert and scale the UB/LB. + numerator = getFullyConvertedLowerBounds(getLeftOperand()) + ) + } +} + */ + /** * A range analysis extension that support bitwise `|` and `|=` where at least one operand is a * non-negative constant. diff --git a/cpp/common/src/codingstandards/cpp/exclusions/c/FloatingTypes2.qll b/cpp/common/src/codingstandards/cpp/exclusions/c/FloatingTypes2.qll new file mode 100644 index 0000000000..7cdc6430a3 --- /dev/null +++ b/cpp/common/src/codingstandards/cpp/exclusions/c/FloatingTypes2.qll @@ -0,0 +1,44 @@ +//** THIS FILE IS AUTOGENERATED, DO NOT MODIFY DIRECTLY. **/ +import cpp +import RuleMetadata +import codingstandards.cpp.exclusions.RuleMetadata + +newtype FloatingTypes2Query = + TPossibleMisuseOfUndetectedInfinityQuery() or + TPossibleMisuseOfUndetectedNaNQuery() + +predicate isFloatingTypes2QueryMetadata(Query query, string queryId, string ruleId, string category) { + query = + // `Query` instance for the `possibleMisuseOfUndetectedInfinity` query + FloatingTypes2Package::possibleMisuseOfUndetectedInfinityQuery() and + queryId = + // `@id` for the `possibleMisuseOfUndetectedInfinity` query + "c/misra/possible-misuse-of-undetected-infinity" and + ruleId = "DIR-4-15" and + category = "required" + or + query = + // `Query` instance for the `possibleMisuseOfUndetectedNaN` query + FloatingTypes2Package::possibleMisuseOfUndetectedNaNQuery() and + queryId = + // `@id` for the `possibleMisuseOfUndetectedNaN` query + "c/misra/possible-misuse-of-undetected-na-n" and + ruleId = "DIR-4-15" and + category = "required" +} + +module FloatingTypes2Package { + Query possibleMisuseOfUndetectedInfinityQuery() { + //autogenerate `Query` type + result = + // `Query` type for `possibleMisuseOfUndetectedInfinity` query + TQueryC(TFloatingTypes2PackageQuery(TPossibleMisuseOfUndetectedInfinityQuery())) + } + + Query possibleMisuseOfUndetectedNaNQuery() { + //autogenerate `Query` type + result = + // `Query` type for `possibleMisuseOfUndetectedNaN` query + TQueryC(TFloatingTypes2PackageQuery(TPossibleMisuseOfUndetectedNaNQuery())) + } +} diff --git a/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll b/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll index 6ab695fb99..41ae2931b1 100644 --- a/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll +++ b/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll @@ -32,6 +32,7 @@ import Declarations8 import EssentialTypes import Expressions import FloatingTypes +import FloatingTypes2 import FunctionTypes import IO1 import IO2 @@ -112,6 +113,7 @@ newtype TCQuery = TEssentialTypesPackageQuery(EssentialTypesQuery q) or TExpressionsPackageQuery(ExpressionsQuery q) or TFloatingTypesPackageQuery(FloatingTypesQuery q) or + TFloatingTypes2PackageQuery(FloatingTypes2Query q) or TFunctionTypesPackageQuery(FunctionTypesQuery q) or TIO1PackageQuery(IO1Query q) or TIO2PackageQuery(IO2Query q) or @@ -192,6 +194,7 @@ predicate isQueryMetadata(Query query, string queryId, string ruleId, string cat isEssentialTypesQueryMetadata(query, queryId, ruleId, category) or isExpressionsQueryMetadata(query, queryId, ruleId, category) or isFloatingTypesQueryMetadata(query, queryId, ruleId, category) or + isFloatingTypes2QueryMetadata(query, queryId, ruleId, category) or isFunctionTypesQueryMetadata(query, queryId, ruleId, category) or isIO1QueryMetadata(query, queryId, ruleId, category) or isIO2QueryMetadata(query, queryId, ruleId, category) or diff --git a/rule_packages/c/FloatingTypes2.json b/rule_packages/c/FloatingTypes2.json new file mode 100644 index 0000000000..152ead08d3 --- /dev/null +++ b/rule_packages/c/FloatingTypes2.json @@ -0,0 +1,36 @@ +{ + "MISRA-C-2012": { + "DIR-4-15": { + "properties": { + "obligation": "required" + }, + "queries": [ + { + "description": "Evaluation of floating-point expressions shall not lead to the undetected generation of infinities.", + "kind": "path-problem", + "name": "Evaluation of floating-point expressions shall not lead to the undetected generation of infinities", + "precision": "high", + "severity": "error", + "short_name": "PossibleMisuseOfUndetectedInfinity", + "tags": [ + "correctness", + "external/misra/c/2012/amendment3" + ] + }, + { + "description": "Evaluation of floating-point expressions shall not lead to the undetected generation of NaNs.", + "kind": "path-problem", + "name": "Evaluation of floating-point expressions shall not lead to the undetected generation of NaNs", + "precision": "high", + "severity": "error", + "short_name": "PossibleMisuseOfUndetectedNaN", + "tags": [ + "correctness", + "external/misra/c/2012/amendment3" + ] + } + ], + "title": "Evaluation of floating-point expressions shall not lead to the undetected generation of infinities and NaNs" + } + } +} \ No newline at end of file From 59ebba0f3c52d090b1c07c0e732db7d740485870 Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Mon, 3 Feb 2025 19:11:59 -0800 Subject: [PATCH 2/9] Support guards isinf(), isfinite(), isnan(), etc --- .../PossibleMisuseOfUndetectedInfinity.ql | 12 + .../DIR-4-15/PossibleMisuseOfUndetectedNaN.ql | 41 ++- ...ossibleMisuseOfUndetectedInfinity.expected | 59 +++- .../PossibleMisuseOfUndetectedNaN.expected | 43 ++- c/misra/test/rules/DIR-4-15/test.c | 99 +++++- .../src/codingstandards/cpp/FloatingPoint.qll | 317 +++++++++++++++++- .../cpp/RestrictedRangeAnalysis.qll | 22 +- 7 files changed, 521 insertions(+), 72 deletions(-) diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql index 84a3fbfd3c..97dd251083 100644 --- a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql +++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql @@ -44,6 +44,18 @@ module InvalidInfinityUsage implements DataFlow::ConfigSig { exprMayEqualInfinity(node.asExpr(), _) } + predicate isBarrierOut(DataFlow::Node node) { + guardedNotFPClass(node.asExpr(), TInfinite()) + or + exists(Expr e | + e.getType() instanceof IntegralType and + e = node.asConvertedExpr() + ) + or + // Sinks are places where Infinity produce a finite value + isSink(node) + } + /** * An additional flow step to handle operations which propagate Infinity. * diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql index 6962a1c36d..036d470247 100644 --- a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql +++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql @@ -89,7 +89,6 @@ class InvalidOperationExpr extends BinaryOperation { } module InvalidNaNUsage implements DataFlow::ConfigSig { - /** * An expression which has non-NaN inputs and may produce a NaN output. */ @@ -108,6 +107,15 @@ module InvalidNaNUsage implements DataFlow::ConfigSig { node.asExpr() instanceof InvalidOperationExpr } + predicate isBarrierOut(DataFlow::Node node) { + guardedNotFPClass(node.asExpr(), TNaN()) + or + exists(Expr e | + e.getType() instanceof IntegralType and + e = node.asConvertedExpr() + ) + } + /** * Add an additional flow step to handle NaN propagation through floating point operations. */ @@ -120,21 +128,24 @@ module InvalidNaNUsage implements DataFlow::ConfigSig { } predicate isSink(DataFlow::Node node) { - // Case 1: NaNs shall not be compared, except to themselves - exists(ComparisonOperation cmp | - node.asExpr() = cmp.getAnOperand() and - not hashCons(cmp.getLeftOperand()) = hashCons(cmp.getRightOperand()) - ) - or - // Case 2: NaNs and infinities shall not be cast to integers - exists(Conversion c | - node.asExpr() = c.getUnconverted() and - c.getExpr().getType() instanceof FloatingPointType and - c.getType() instanceof IntegralType + not guardedNotFPClass(node.asExpr(), TNaN()) and + ( + // Case 1: NaNs shall not be compared, except to themselves + exists(ComparisonOperation cmp | + node.asExpr() = cmp.getAnOperand() and + not hashCons(cmp.getLeftOperand()) = hashCons(cmp.getRightOperand()) + ) + or + // Case 2: NaNs and infinities shall not be cast to integers + exists(Conversion c | + node.asExpr() = c.getUnconverted() and + c.getExpr().getType() instanceof FloatingPointType and + c.getType() instanceof IntegralType + ) + //or + //// Case 4: Functions shall not return NaNs or infinities + //exists(ReturnStmt ret | node.asExpr() = ret.getExpr()) ) - //or - //// Case 4: Functions shall not return NaNs or infinities - //exists(ReturnStmt ret | node.asExpr() = ret.getExpr()) } } diff --git a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected index 78f4c6baec..75534df6a0 100644 --- a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected +++ b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected @@ -1,5 +1,6 @@ edges | test.c:8:14:8:20 | ... / ... | test.c:8:14:8:20 | ... / ... | provenance | | +| test.c:8:14:8:20 | ... / ... | test.c:9:14:9:16 | - ... | provenance | Config | | test.c:8:14:8:20 | ... / ... | test.c:12:8:12:9 | l2 | provenance | | | test.c:8:14:8:20 | ... / ... | test.c:18:3:18:9 | l2 | provenance | | | test.c:8:14:8:20 | ... / ... | test.c:27:19:27:20 | l2 | provenance | | @@ -9,8 +10,17 @@ edges | test.c:9:14:9:16 | - ... | test.c:28:19:28:20 | l3 | provenance | | | test.c:31:14:32:15 | ... / ... | test.c:31:14:32:15 | ... / ... | provenance | | | test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | provenance | | -| test.c:33:14:33:22 | ... / ... | test.c:33:14:33:22 | ... / ... | provenance | | -| test.c:33:14:33:22 | ... / ... | test.c:39:3:39:9 | l8 | provenance | | +| test.c:77:15:77:21 | ... / ... | test.c:77:15:77:21 | ... / ... | provenance | | +| test.c:77:15:77:21 | ... / ... | test.c:79:5:79:12 | l12 | provenance | | +| test.c:77:15:77:21 | ... / ... | test.c:87:5:87:12 | l12 | provenance | | +| test.c:77:15:77:21 | ... / ... | test.c:91:5:91:12 | l12 | provenance | | +| test.c:77:15:77:21 | ... / ... | test.c:93:5:93:12 | l12 | provenance | | +| test.c:77:15:77:21 | ... / ... | test.c:99:5:99:12 | l12 | provenance | | +| test.c:77:15:77:21 | ... / ... | test.c:105:5:105:12 | l12 | provenance | | +| test.c:77:15:77:21 | ... / ... | test.c:111:5:111:12 | l12 | provenance | | +| test.c:77:15:77:21 | ... / ... | test.c:114:16:114:23 | l12 | provenance | | +| test.c:77:15:77:21 | ... / ... | test.c:117:23:117:30 | l12 | provenance | | +| test.c:77:15:77:21 | ... / ... | test.c:120:20:120:27 | l12 | provenance | | nodes | test.c:8:14:8:20 | ... / ... | semmle.label | ... / ... | | test.c:8:14:8:20 | ... / ... | semmle.label | ... / ... | @@ -24,25 +34,46 @@ nodes | test.c:28:19:28:20 | l3 | semmle.label | l3 | | test.c:31:14:32:15 | ... / ... | semmle.label | ... / ... | | test.c:31:14:32:15 | ... / ... | semmle.label | ... / ... | -| test.c:33:14:33:22 | ... / ... | semmle.label | ... / ... | -| test.c:33:14:33:22 | ... / ... | semmle.label | ... / ... | | test.c:38:3:38:9 | l7 | semmle.label | l7 | -| test.c:39:3:39:9 | l8 | semmle.label | l8 | -| test.c:61:5:61:19 | ... / ... | semmle.label | ... / ... | -| test.c:66:5:66:21 | ... / ... | semmle.label | ... / ... | -| test.c:72:14:72:30 | ... / ... | semmle.label | ... / ... | -| test.c:75:18:75:34 | ... / ... | semmle.label | ... / ... | +| test.c:61:5:61:18 | ... / ... | semmle.label | ... / ... | +| test.c:66:5:66:20 | ... / ... | semmle.label | ... / ... | +| test.c:72:14:72:29 | ... / ... | semmle.label | ... / ... | +| test.c:75:18:75:33 | ... / ... | semmle.label | ... / ... | +| test.c:77:15:77:21 | ... / ... | semmle.label | ... / ... | +| test.c:77:15:77:21 | ... / ... | semmle.label | ... / ... | +| test.c:79:5:79:12 | l12 | semmle.label | l12 | +| test.c:87:5:87:12 | l12 | semmle.label | l12 | +| test.c:91:5:91:12 | l12 | semmle.label | l12 | +| test.c:93:5:93:12 | l12 | semmle.label | l12 | +| test.c:99:5:99:12 | l12 | semmle.label | l12 | +| test.c:105:5:105:12 | l12 | semmle.label | l12 | +| test.c:111:5:111:12 | l12 | semmle.label | l12 | +| test.c:114:16:114:23 | l12 | semmle.label | l12 | +| test.c:117:23:117:30 | l12 | semmle.label | l12 | +| test.c:120:20:120:27 | l12 | semmle.label | l12 | subpaths #select | 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 | +| 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 | | 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 | | 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 | +| 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 | | 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 | | 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 | +| 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 | | 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 | | 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | diff --git a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected index f317f236ef..e59d43d867 100644 --- a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected +++ b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected @@ -16,6 +16,15 @@ edges | test.c:33:14:33:22 | ... / ... | test.c:33:14:33:22 | ... / ... | provenance | | | test.c:33:14:33:22 | ... / ... | test.c:39:3:39:9 | l8 | provenance | | | test.c:33:14:33:22 | ... / ... | test.c:54:3:54:4 | l8 | provenance | | +| test.c:122:15:122:21 | ... / ... | test.c:122:15:122:21 | ... / ... | provenance | | +| test.c:122:15:122:21 | ... / ... | test.c:126:5:126:12 | l13 | provenance | | +| test.c:122:15:122:21 | ... / ... | test.c:132:5:132:12 | l13 | provenance | | +| test.c:122:15:122:21 | ... / ... | test.c:138:5:138:12 | l13 | provenance | | +| test.c:122:15:122:21 | ... / ... | test.c:144:5:144:12 | l13 | provenance | | +| test.c:122:15:122:21 | ... / ... | test.c:148:5:148:12 | l13 | provenance | | +| test.c:122:15:122:21 | ... / ... | test.c:154:20:154:27 | l13 | provenance | | +| test.c:122:15:122:21 | ... / ... | test.c:156:23:156:30 | l13 | provenance | | +| test.c:122:15:122:21 | ... / ... | test.c:157:16:157:23 | l13 | provenance | | nodes | test.c:27:14:27:20 | ... / ... | semmle.label | ... / ... | | test.c:27:14:27:20 | ... / ... | semmle.label | ... / ... | @@ -38,10 +47,20 @@ nodes | test.c:52:3:52:4 | l6 | semmle.label | l6 | | test.c:53:3:53:4 | l7 | semmle.label | l7 | | test.c:54:3:54:4 | l8 | semmle.label | l8 | -| test.c:61:5:61:19 | ... / ... | semmle.label | ... / ... | -| test.c:66:5:66:21 | ... / ... | semmle.label | ... / ... | -| test.c:72:14:72:30 | ... / ... | semmle.label | ... / ... | -| test.c:75:18:75:34 | ... / ... | semmle.label | ... / ... | +| test.c:61:5:61:18 | ... / ... | semmle.label | ... / ... | +| test.c:66:5:66:20 | ... / ... | semmle.label | ... / ... | +| test.c:72:14:72:29 | ... / ... | semmle.label | ... / ... | +| test.c:75:18:75:33 | ... / ... | semmle.label | ... / ... | +| test.c:122:15:122:21 | ... / ... | semmle.label | ... / ... | +| test.c:122:15:122:21 | ... / ... | semmle.label | ... / ... | +| test.c:126:5:126:12 | l13 | semmle.label | l13 | +| test.c:132:5:132:12 | l13 | semmle.label | l13 | +| test.c:138:5:138:12 | l13 | semmle.label | l13 | +| test.c:144:5:144:12 | l13 | semmle.label | l13 | +| test.c:148:5:148:12 | l13 | semmle.label | l13 | +| test.c:154:20:154:27 | l13 | semmle.label | l13 | +| test.c:156:23:156:30 | l13 | semmle.label | l13 | +| test.c:157:16:157:23 | l13 | semmle.label | l13 | subpaths #select | 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 | 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 | | 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 | | 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 | -| 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 | -| 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 | -| 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 | -| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | +| 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 | diff --git a/c/misra/test/rules/DIR-4-15/test.c b/c/misra/test/rules/DIR-4-15/test.c index d634a6e594..d0f9ab5418 100644 --- a/c/misra/test/rules/DIR-4-15/test.c +++ b/c/misra/test/rules/DIR-4-15/test.c @@ -56,21 +56,104 @@ void f1(float p1) { // Guards float l9 = 0; if (l9 != 0) { - (int) (l9 / l9); // COMPLIANT: l9 is not zero + (int)(l9 / l9); // COMPLIANT: l9 is not zero } else { - (int) (l9 / l9); // NON_COMPLIANT: Casting NaN to integer + (int)(l9 / l9); // NON_COMPLIANT: Guarded to not be NaN } float l10 = 0; if (l10 == 0) { - (int) (l10 / l10); // NON_COMPLIANT: Casting NaN to integer + (int)(l10 / l10); // NON_COMPLIANT: Casting NaN to integer } else { - (int) (l10 / l10); // COMPLIANT: l10 is not zero + (int)(l10 / l10); // COMPLIANT: Guarded to not be NaN } float l11 = 0; - l11 == 0 ? (int) (l11 / l11) : 0; // NON_COMPLIANT - l11 == 0 ? 0 : (int) (l11 / l11); // COMPLIANT - l11 != 0 ? (int) (l11 / l11) : 0; // COMPLIANT - l11 != 0 ? 0 : (int) (l11 / l11); // NON_COMPLIANT + l11 == 0 ? (int)(l11 / l11) : 0; // NON_COMPLIANT + l11 == 0 ? 0 : (int)(l11 / l11); // COMPLIANT + l11 != 0 ? (int)(l11 / l11) : 0; // COMPLIANT + l11 != 0 ? 0 : (int)(l11 / l11); // NON_COMPLIANT + + float l12 = 1.0 / 0; + if (isinf(l12)) { + (int)l12; // NON_COMPLIANT: Casting Infinity to integer + } else { + (int)l12; // COMPLIANT: Guarded not to be Infinity + } + + if (!isinf(l12)) { + (int)l12; // COMPLIANT: Guarded not to be Infinity + } else { + (int)l12; // NON_COMPLIANT: Casting Infinity to integer + } + + if (isinf(l12) == 1) { + (int)l12; // NON_COMPLIANT: Must be +Infinity + } else { + (int)l12; // NON_COMPLIANT: May be -Infinity + } + + if (isfinite(l12)) { + (int)l12; // COMPLIANT: Guarded not to be Infinity + } else { + (int)l12; // NON_COMPLIANT: Casting Infinity to integer + } + + if (isnormal(l12)) { + (int)l12; // COMPLIANT: Guarded not to be Infinity + } else { + (int)l12; // NON_COMPLIANT: Casting Infinity to integer + } + + if (isnan(l12)) { + (int)l12; // COMPLIANT: Guarded not to be Infinity + } else { + (int)l12; // NON_COMPLIANT: Casting Infinity to integer + } + + isinf(l12) ? (int)l12 : 0; // NON_COMPLIANT: Check on wrong branch + isinf(l12) ? 0 : (int)l12; // COMPLIANT: Checked not infinite before use + isfinite(l12) ? (int)l12 : 0; // COMPLIANT: Checked finite before use + isfinite(l12) ? 0 : (int)l12; // NON_COMPLIANT: Checked on wrong branch + isnan(l12) ? (int)l12 + : 0; // COMPLIANT: Checked NaN, therefore not infinite, before use + isnan(l12) ? 0 : (int)l12; // NON_COMPLIANT: Check on wrong branch + + float l13 = 0.0 / 0; + if (isinf(l13)) { + (int)l13; // COMPLIANT: Guarded not to be NaN + } else { + (int)l13; // NON_COMPLIANT: Casting NaN to integer + } + + if (isinf(l13) == 1) { + (int)l13; // COMPLIANT: Guarded not to be NaN (must be +Infinity) + } else { + (int)l13; // NON_COMPLIANT: Casting NaN to integer + } + + if (isfinite(l13)) { + (int)l13; // COMPLIANT: Guarded not to be NaN + } else { + (int)l13; // NON_COMPLIANT: Casting NaN to integer + } + + if (isnormal(l13)) { + (int)l13; // COMPLIANT: Guarded not to be NaN + } else { + (int)l13; // NON_COMPLIANT: Casting NaN to integer + } + + if (isnan(l13)) { + (int)l13; // NON_COMPLIANT: Casting NaN to integer + } else { + (int)l13; // COMPLIANT: Guarded not to be NaN + } + + isinf(l13) ? (int)l13 : 0; // COMPLIANT: Checked infinite, therefore not NaN, before use + isinf(l13) ? 0 : (int)l13; // COMPLIANT: Check on wrong branch + isfinite(l13) ? (int)l13 : 0; // COMPLIANT: Checked finite before use + isfinite(l13) ? 0 : (int)l13; // NON_COMPLIANT: Checked on wrong branch + isnan(l13) ? (int)l13 : 0; // NON_COMPLIANT: Check on wrong branch + isnan(l13) ? 0 : (int)l13; // COMPLIANT: Checked not NaN before use } \ No newline at end of file diff --git a/cpp/common/src/codingstandards/cpp/FloatingPoint.qll b/cpp/common/src/codingstandards/cpp/FloatingPoint.qll index d143f81418..f3ba8dba18 100644 --- a/cpp/common/src/codingstandards/cpp/FloatingPoint.qll +++ b/cpp/common/src/codingstandards/cpp/FloatingPoint.qll @@ -7,6 +7,294 @@ predicate exprMayEqualZero(Expr e) { not guardedNotEqualZero(e) } +newtype TFPClassification = + TFinite() or + TNaN() or + TInfinite() + +class FPClassification extends TFPClassification { + string toString() { + this = TFinite() and + result = "finite" + or + this = TNaN() and + result = "NaN" + or + this = TInfinite() and + result = "infinite" + } +} + +newtype TFPClassificationConstraint = + /* The value may be infinite, NaN, or finite. */ + TUnclassified() or + /** + * The value must be one of: infinite, NaN, or finite. + * + * If strict is `true` then this inverts naively. For example, `!isfinite(x)` means `x` must not + * be finite. However, `!iszero(x)` is true for some finite values, and inverts to + * `TUnclassified`. + */ + TExactFPClassification(TFPClassification cls, Boolean strict) or + /* The value must not be one of: infinite, NaN, or finite. */ + TExcludeFPClassification(TFPClassification cls1) + +class FPClassificationConstraint extends TFPClassificationConstraint { + string toString() { + this = TUnclassified() and + result = "unclassified" + or + exists(FPClassification cls, Boolean strict | + this = TExactFPClassification(cls, strict) and + result = "must be " + cls.toString() + ", strict: " + strict.toString() + or + this = TExcludeFPClassification(cls) and + result = "must NOT be " + cls.toString() + ) + } + + /** + * Invert the constraint, for instance, "must be finite" becomes "must not be finite". + * + * Non-strict exact constraints are inverted to the unclassified constraint. For example, + * `iszero(x)` guarantees `x` to be finite, however, `!iszero(x)` can be true for all three + * classes of floating point values. + * + * The unclassified constraint inverts to itself. + */ + FPClassificationConstraint invert() { + // Unclassified inverts to itself. + this = TUnclassified() and result = this + or + exists(FPClassification cls | + // `!isfinite()` implies is infinite or NaN. + this = TExactFPClassification(cls, true) and + result = TExcludeFPClassification(cls) + or + // `!iszero()` implies nothing. + this = TExactFPClassification(cls, false) and + result = TUnclassified() + or + // For completeness: `!isfinite(x) ? ... : x` would imply `isfinite(x)`. + this = TExcludeFPClassification(cls) and + result = TExactFPClassification(cls, true) + ) + } + + /** + * Naively invert the constraint, for instance, "must be finite" becomes "must not be finite". + * + * Word of caution: inverting a guard condition does not necessarily invert the constraint. For + * example, `iszero(x)` guarantees `x` to be finite, however, `isnotzero(x)` does not guarantee + * `x` not to be finite. + * + * The unclassified constraint is not inverted. + */ + FPClassificationConstraint naiveInversion() { + this = TUnclassified() and result = this + or + exists(FPClassification cls | + this = TExactFPClassification(cls, _) and + result = TExcludeFPClassification(cls) + or + this = TExcludeFPClassification(cls) and + result = TExactFPClassification(cls, true) + ) + } + + predicate mustBe(FPClassification cls) { this = TExactFPClassification(cls, _) } + + predicate mustNotBe(FPClassification cls) { + this = TExcludeFPClassification(cls) + or + this = TExactFPClassification(_, _) and + not this = TExactFPClassification(cls, _) + } + + predicate mayBe(FPClassification cls) { not mustNotBe(cls) } +} + +/** + * The names of the functions or macros that classify floating point values. + * + * These names reflect a check that a value is finite, or infinite, or NaN. Finite and NaN checks + * are either strict (return true for all values in the class) or not (return true for some + * values). + * + * The infinite check is always strict, and specially, returns 1 or -1 for positive or negative + * infinity. + */ +newtype TFPClassifierName = + TClassifiesFinite(string name, boolean strict) { + strict = true and + name = ["finite" + ["", "l", "f"], "isfinite"] + or + strict = false and + name = ["isnormal", "issubnormal", "iszero"] + } or + TClassifiesNaN(string name, boolean strict) { + strict = true and + name = "isnan" + ["", "f", "l"] + or + strict = false and + name = "issignaling" + } or + TClassifiesInfinite(string name) { name = "isinf" + ["", "f", "l"] } + +class FPClassifierName extends TFPClassifierName { + string name; + boolean strict; + + FPClassifierName() { + this = TClassifiesFinite(name, strict) + or + this = TClassifiesInfinite(name) and + strict = true + or + this = TClassifiesNaN(name, strict) + } + + string toString() { result = name } + + /** The classification name, for instance, "isfinite". */ + string getName() { result = name } + + /** + * Whether the check holds for all values in the class, or only some. + * + * For instance, "isfinite" is strict because it returns true for all finite values, but + * "isnormal" is not as it returns false for some finite values. + */ + predicate isStrict() { strict = true } + + FPClassificationConstraint getConstraint() { + this = TClassifiesFinite(_, strict) and + result = TExactFPClassification(any(TFinite t), strict) + or + this = TClassifiesNaN(_, strict) and + result = TExactFPClassification(any(TNaN t), strict) + or + this = TClassifiesInfinite(_) and + // TODO: isinf() is special + result = TExactFPClassification(any(TInfinite t), false) + } +} + +/** + * An invocation of a classification function, for instance, "isfinite(x)", implemented as a macro. + */ +class FPClassifierMacroInvocation extends MacroInvocation { + FPClassifierName classifier; + + FPClassifierMacroInvocation() { getMacroName() = classifier.getName() } + + Expr getCheckedExpr() { + // Getting the checked expr in a cross-platform way is extroardinarily difficult, as glibc has + // multiple conditional implementations of the same macro. Assume the checked expr is a + // variable access so we can search optimistically like so: + exists(VariableAccess va | + va.getTarget().getName() = getExpandedArgument(0) and + va = getAnExpandedElement() and + result = va + ) + } + + /** + * The classification name, for instance, "isfinite". + */ + FPClassifierName getFPClassifierName() { result = classifier } +} + +/** + * A classification function, for instance, "isfinite", when implemented as a function. + */ +class FPClassifierFunction extends Function { + FPClassifierName classifier; + + FPClassifierFunction() { getName() = classifier.getName() } + + FPClassifierName getFPClassifierName() { result = classifier } +} + +class FPClassificationGuard instanceof GuardCondition { + Expr floatExpr; + Expr checkResultExpr; + FPClassifierName classifier; + + FPClassificationGuard() { + super.comparesEq(checkResultExpr, _, _, _) and + ( + exists(FPClassifierMacroInvocation m | + floatExpr = m.getCheckedExpr() and + checkResultExpr = m.getExpr() and + classifier = m.getFPClassifierName() + ) + or + exists(FunctionCall fc, FPClassifierFunction f | + fc.getTarget() = f and + floatExpr = fc.getArgument(0) and + checkResultExpr = fc and + classifier = f.getFPClassifierName() + ) + ) + } + + string toString() { + result = + classifier.toString() + " guard on " + floatExpr.toString() + " via " + + checkResultExpr.toString() + } + + predicate constrainsFPClass(Expr e, FPClassificationConstraint constraint, Boolean testIsTrue) { + floatExpr = e and + exists(BooleanValue value, boolean areEqual, int testResult, FPClassificationConstraint base | + super.comparesEq(checkResultExpr, testResult, areEqual, value) and + base = getBaseConstraint(areEqual, testResult) and + if value.getValue() = testIsTrue then constraint = base else constraint = base.invert() + ) + } + + // Helper function, gets base constraint assuming `classifier() == value` or `classifier != value`. + private FPClassificationConstraint getBaseConstraint(Boolean areEqual, int testResult) { + exists(FPClassificationConstraint base | + testResult = 0 and + exists(Boolean strict | + // Handle isfinite() != 0: + classifier = TClassifiesFinite(_, strict) and + base = TExactFPClassification(TFinite(), strict) + or + // Handle isNaN() != 0: + classifier = TClassifiesNaN(_, strict) and + base = TExactFPClassification(TNaN(), strict) + or + // Handle isinf() != 0, which matches for +/- infinity: + classifier = TClassifiesInfinite(_) and + base = TExactFPClassification(TInfinite(), true) + ) and + // Invert the base constraint in the case of `classifier() == 0` + if areEqual = false then result = base else result = base.invert() + or + // Handle isinf() == 1 or isInf() == -1, which matches for one of +/- infinity: + testResult = 1 and + classifier = TClassifiesInfinite(_) and + base = TExactFPClassification(TInfinite(), false) and + // Invert the base constraint in the case of `classifier() != 1` + if areEqual = true then result = base else result = base.invert() + // TODO: handle fpclassify() == FP_INFINITE, FP_NAN, FP_NORMAL, FP_ZERO, etc. + ) + } + + predicate controls(Expr e, boolean testIsTrue) { + exists(IRGuardCondition irg, IRBlock irb, Instruction eir, BooleanValue bval | + irg.getUnconvertedResultExpression() = this and + bval.getValue() = testIsTrue and + irg.valueControls(irb, bval) and + eir.getAst().(ControlFlowNode).getBasicBlock() = e.getBasicBlock() and + eir.getBlock() = irb + ) + } +} + predicate guardedNotEqualZero(Expr e) { /* Note Boolean cmpEq, false means cmpNeq */ exists(Expr checked, GuardCondition guard, boolean cmpEq, BooleanValue value | @@ -28,24 +316,15 @@ predicate guardedNotEqualZero(Expr e) { ) } -predicate guardedNotInfinite(Expr e) { +predicate guardedNotFPClass(Expr e, FPClassification cls) { /* Note Boolean cmpEq, false means cmpNeq */ - exists(Expr c, GuardCondition guard, boolean cmpEq | - hashCons(c) = hashCons(e) and + exists( + Expr checked, FPClassificationGuard guard, FPClassificationConstraint constraint, boolean cmpEq + | + hashCons(checked) = hashCons(e) and guard.controls(e, cmpEq) and - guard.comparesEq(c, 0, cmpEq.booleanNot(), _) - ) -} - -predicate test(Expr e, Expr v, int k, boolean areEqual, Boolean value, Expr gce, BasicBlock bb) { - exists(GuardCondition gc | gce = gc | - gc.controls(bb, _) and - gc.comparesEq(e, v, k, areEqual, value) and - ( - //gc.getAChild+().toString().matches("%dfYRes%") or - e.getAChild*().toString().matches("%dfPseudoPanchro%") or - v.getAChild*().toString().matches("%dfPseudoPanchro%") - ) + guard.constrainsFPClass(checked, constraint, cmpEq) and + constraint.mustNotBe(cls) ) } @@ -57,5 +336,7 @@ predicate exprMayEqualInfinity(Expr e, Boolean positive) { | RestrictedRangeAnalysis::upperBound(e.getUnconverted()) = target or RestrictedRangeAnalysis::lowerBound(e.getUnconverted()) = target - ) -} \ No newline at end of file + ) and + not guardedNotFPClass(e, TInfinite()) and + not e.getType() instanceof IntegralType +} diff --git a/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll b/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll index 79ae2f367a..9b4bba8980 100644 --- a/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll +++ b/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll @@ -297,17 +297,21 @@ module RestrictedRangeAnalysis { } /** - * Holds if `expr` may divide by zero. + * Holds if `expr` may divide by zero. Excludes dividing a constant zero divided by zero, + * which produces NaN instead of an infinite value. */ - predicate dividesByZero(Expr expr) { - exists(Expr divisor | + predicate dividesNonzeroByZero(Expr expr) { + exists(Expr divisor, Expr numerator | divisor = expr.(DivExpr).getRightOperand() and + numerator = expr.(DivExpr).getLeftOperand() and getTruncatedLowerBounds(divisor) <= 0.0 and getTruncatedUpperBounds(divisor) >= 0.0 and - not isCheckedNotZero(divisor) + not isCheckedNotZero(divisor) and + not getValue(numerator).toFloat() = 0.0 ) } + /** * Holds if `expr` is checked with a guard to not be zero. * @@ -362,7 +366,7 @@ module RestrictedRangeAnalysis { // Introduces non-monotonic recursion. However, analysis mostly works with this // commented out. // or - // dividesByZero(e) + // dividesNonzeroByZero(e) or e instanceof DivExpr // TODO: confirm this is OK or @@ -681,7 +685,7 @@ module RestrictedRangeAnalysis { } private predicate lowerBoundableExpr(Expr expr) { - (analyzableExpr(expr) or dividesByZero(expr)) and + (analyzableExpr(expr) or dividesNonzeroByZero(expr)) and getUpperBoundsImpl(expr) <= Util::exprMaxVal(expr) and not exists(getValue(expr).toFloat()) } @@ -760,7 +764,7 @@ module RestrictedRangeAnalysis { * this predicate. */ private float getTruncatedUpperBounds(Expr expr) { - (analyzableExpr(expr) or dividesByZero(expr)) + (analyzableExpr(expr) or dividesNonzeroByZero(expr)) and ( // If the expression evaluates to a constant, then there is no // need to call getUpperBoundsImpl. @@ -827,7 +831,7 @@ module RestrictedRangeAnalysis { ) or exists(DivExpr div | expr = div | - dividesByZero(expr) and + dividesNonzeroByZero(expr) and result = getFullyConvertedLowerBounds(div.getLeftOperand()) / 0 ) or @@ -1032,7 +1036,7 @@ module RestrictedRangeAnalysis { ) or exists(DivExpr div | expr = div | - dividesByZero(expr) and + dividesNonzeroByZero(expr) and result = getFullyConvertedUpperBounds(div.getLeftOperand()) / 0 ) or From 4ee762909b228630ae6f7da1bcab8ba7922b2df5 Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Thu, 6 Feb 2025 12:00:56 -0800 Subject: [PATCH 3/9] Deduplicate and filter results, improve messages, handle performance issue --- .../PossibleMisuseOfUndetectedInfinity.ql | 69 ++++-- .../DIR-4-15/PossibleMisuseOfUndetectedNaN.ql | 68 ++++-- .../PossibleUndetectedNaNorInfinity.ql | 223 ------------------ .../PossibleUndetectedNaNorInfinity.expected | 1 - .../PossibleUndetectedNaNorInfinity.qlref | 1 - .../cpp/RestrictedRangeAnalysis.qll | 126 ++++++++-- 6 files changed, 207 insertions(+), 281 deletions(-) delete mode 100644 c/misra/src/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.ql delete mode 100644 c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.expected delete mode 100644 c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.qlref diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql index 97dd251083..10c370690b 100644 --- a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql +++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql @@ -73,44 +73,73 @@ module InvalidInfinityUsage implements DataFlow::ConfigSig { } predicate isSink(DataFlow::Node node) { + node instanceof InvalidInfinityUsage and ( // Require that range analysis finds this value potentially infinite, to avoid false positives // in the presence of guards. This may induce false negatives. - exprMayEqualInfinity(node.asExpr(), _) or + exprMayEqualInfinity(node.asExpr(), _) + or // Unanalyzable expressions are not checked against range analysis, which assumes a finite // range. not RestrictedRangeAnalysis::analyzableExpr(node.asExpr()) - ) and - ( - // Case 2: NaNs and infinities shall not be cast to integers - exists(Conversion c | - node.asExpr() = c.getUnconverted() and - c.getExpr().getType() instanceof FloatingPointType and - c.getType() instanceof IntegralType - ) - or - // Case 3: Infinities shall not underflow or otherwise produce finite values - exists(BinaryOperation op | - node.asExpr() = op.getRightOperand() and - op.getOperator() = ["/", "%"] - ) ) } } +class InvalidInfinityUsage extends DataFlow::Node { + string description; + string infinityDescription; + + InvalidInfinityUsage() { + // Case 2: NaNs and infinities shall not be cast to integers + exists(Conversion c | + asExpr() = c.getUnconverted() and + c.getExpr().getType() instanceof FloatingPointType and + c.getType() instanceof IntegralType and + description = "$@ casted to integer." and + infinityDescription = "Possibly infinite float value" + ) + or + // Case 3: Infinities shall not underflow or otherwise produce finite values + exists(BinaryOperation op | + asExpr() = op.getRightOperand() and + op.getOperator() = "/" and + description = "Division operation may silently underflow and produce zero, as the divisor $@." and + infinityDescription = "may be an infinite float value" + ) + } + + string getDescription() { result = description } + + string getInfinityDescription() { result = infinityDescription } +} + module InvalidInfinityFlow = DataFlow::Global; import InvalidInfinityFlow::PathGraph from Element elem, InvalidInfinityFlow::PathNode source, InvalidInfinityFlow::PathNode sink, - string msg, string sourceString + InvalidInfinityUsage usage, Expr sourceExpr, Element extra, string extraString where elem = MacroUnwrapper::unwrapElement(sink.getNode().asExpr()) and + not InvalidInfinityFlow::PathGraph::edges(_, source, _, _) and not isExcluded(elem, FloatingTypes2Package::possibleMisuseOfUndetectedInfinityQuery()) and + not sourceExpr.isFromTemplateInstantiation(_) and + not usage.asExpr().isFromTemplateInstantiation(_) and + usage = sink.getNode() and + sourceExpr = source.getNode().asExpr() and + InvalidInfinityFlow::flow(source.getNode(), usage) and ( - InvalidInfinityFlow::flow(source.getNode(), sink.getNode()) and - msg = "Invalid usage of possible $@." and - sourceString = "infinity" + if not sourceExpr.getEnclosingFunction() = usage.asExpr().getEnclosingFunction() + then + 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() + ) ) -select elem, source, sink, msg, source, sourceString +select elem, source, sink, usage.getDescription(), extra, extraString \ No newline at end of file diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql index 036d470247..942715fe2f 100644 --- a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql +++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql @@ -40,7 +40,7 @@ class InvalidOperationExpr extends BinaryOperation { exprMayEqualInfinity(getLeftOperand(), sign) and exprMayEqualInfinity(getRightOperand(), sign.booleanNot()) ) and - reason = "possible addition of infinity and negative infinity" + reason = "from addition of infinity and negative infinity" or // 7.1.2 continued getOperator() = "-" and @@ -48,35 +48,35 @@ class InvalidOperationExpr extends BinaryOperation { exprMayEqualInfinity(getLeftOperand(), sign) and exprMayEqualInfinity(getRightOperand(), sign) ) and - reason = "possible subtraction of an infinity from itself" + reason = "from subtraction of an infinity from itself" or // 7.1.3: multiplication of zero by infinity getOperator() = "*" and exprMayEqualZero(getAnOperand()) and exprMayEqualInfinity(getAnOperand(), _) and - reason = "possible multiplication of zero by infinity" + reason = "from multiplication of zero by infinity" or // 7.1.4: Division of zero by zero, or infinity by infinity getOperator() = "/" and exprMayEqualZero(getLeftOperand()) and exprMayEqualZero(getRightOperand()) and - reason = "possible division of zero by zero" + reason = "from division of zero by zero" or // 7.1.4 continued getOperator() = "/" and exprMayEqualInfinity(getLeftOperand(), _) and exprMayEqualInfinity(getRightOperand(), _) and - reason = "possible division of infinity by infinity" + reason = "from division of infinity by infinity" or // 7.1.5: x % y where y is zero or x is infinite getOperator() = "%" and exprMayEqualInfinity(getLeftOperand(), _) and - reason = "possible modulus of infinity" + reason = "from modulus of infinity" or // 7.1.5 continued getOperator() = "%" and exprMayEqualZero(getRightOperand()) and - reason = "possible modulus by zero" + reason = "from modulus by zero" // 7.1.6 handles the sqrt function, not covered here. // 7.1.7 declares exceptions during invalid conversions, which we catch as sinks in our flow // analysis. @@ -129,24 +129,39 @@ module InvalidNaNUsage implements DataFlow::ConfigSig { predicate isSink(DataFlow::Node node) { not guardedNotFPClass(node.asExpr(), TNaN()) and - ( + node instanceof InvalidNaNUsage + } +} + +class InvalidNaNUsage extends DataFlow::Node { + string description; + string nanDescription; + + InvalidNaNUsage() { // Case 1: NaNs shall not be compared, except to themselves exists(ComparisonOperation cmp | - node.asExpr() = cmp.getAnOperand() and - not hashCons(cmp.getLeftOperand()) = hashCons(cmp.getRightOperand()) + 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 | - node.asExpr() = c.getUnconverted() and + this.asExpr() = c.getUnconverted() and c.getExpr().getType() instanceof FloatingPointType and - c.getType() instanceof IntegralType + 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()) - ) } + + string getDescription() { result = description } + + string getNaNDescription() { result = nanDescription } } module InvalidNaNFlow = DataFlow::Global; @@ -154,15 +169,26 @@ module InvalidNaNFlow = DataFlow::Global; import InvalidNaNFlow::PathGraph from - Element elem, InvalidNaNFlow::PathNode source, InvalidNaNFlow::PathNode sink, string msg, - string sourceString + Element elem, InvalidNaNFlow::PathNode source, InvalidNaNFlow::PathNode sink, + InvalidNaNUsage usage, Expr sourceExpr, string sourceString, Element extra, string extraString where + not InvalidNaNFlow::PathGraph::edges(_, source, _, _) and + not sourceExpr.isFromTemplateInstantiation(_) and + not usage.asExpr().isFromTemplateInstantiation(_) and elem = MacroUnwrapper::unwrapElement(sink.getNode().asExpr()) and - not isExcluded(elem, FloatingTypes2Package::possibleMisuseOfUndetectedNaNQuery()) and - ( - InvalidNaNFlow::flow(source.getNode(), sink.getNode()) and - msg = "Invalid usage of possible $@." and + usage = sink.getNode() and + sourceExpr = source.getNode().asExpr() and sourceString = - "NaN resulting from " + source.getNode().asExpr().(InvalidOperationExpr).getReason() + " (" + source.getNode().asExpr().(InvalidOperationExpr).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() + else ( + extra = sourceExpr and + extraString = usage.getNaNDescription() + sourceString + ) ) -select elem, source, sink, msg, source, sourceString +select elem, source, sink, usage.getDescription(), extra, extraString \ No newline at end of file diff --git a/c/misra/src/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.ql b/c/misra/src/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.ql deleted file mode 100644 index 94888a95e6..0000000000 --- a/c/misra/src/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.ql +++ /dev/null @@ -1,223 +0,0 @@ -/** - * @id c/misra/possible-undetected-na-nor-infinity - * @name DIR-4-15: Evaluation of floating-point expressions shall not lead to the undetected generation of infinities - * @description Evaluation of floating-point expressions shall not lead to the undetected generation - * of infinities and NaNs. - * @kind path-problem - * @precision high - * @problem.severity error - * @tags external/misra/id/dir-4-15 - * correctness - * external/misra/c/2012/amendment3 - * external/misra/obligation/required - */ - -import cpp -import codeql.util.Boolean -import codingstandards.c.misra -import codingstandards.cpp.RestrictedRangeAnalysis -import codingstandards.cpp.FloatingPoint -import codingstandards.cpp.AlertReporting -import semmle.code.cpp.controlflow.Guards -import semmle.code.cpp.dataflow.new.DataFlow -import semmle.code.cpp.dataflow.new.TaintTracking -import semmle.code.cpp.controlflow.Dominance - -class CantHandleInfinityFunction extends Function { - CantHandleInfinityFunction() { not hasDefinition() and not getName() = "__fpclassifyl" } -} - -class InfinityCheckedExpr extends Expr { - InfinityCheckedExpr() { - exists(MacroInvocation mi | - mi.getMacroName() = ["isfinite", "isinf"] and - mi.getExpr() = this - ) - } - - Expr getCheckedExpr() { - result = - this.(ConditionalExpr) - .getThen() - .(LTExpr) - .getLesserOperand() - .(BitwiseAndExpr) - .getLeftOperand() - .(FunctionCall) - .getArgument(0) - } -} - -/* -signature module ResourceLeakConfigSig { - predicate isResource(DataFlow::Node node); - - predicate isFree(DataFlow::Node node, DataFlow::Node resource); - - default ControlFlowNode outOfScope(DataFlow::Node resource) { - result = resource.asExpr().getEnclosingFunction().getBlock().getLastStmt() - } - - default predicate isAlias(DataFlow::Node alias, DataFlow::Node resource) { - isResource(resource) and - DataFlow::localFlow(resource, alias) - } -} - -module ResourceLeak { - predicate isLeaked(DataFlow::Node resource, ControlFlowNode cfgNode) { - resource.asExpr() = cfgNode - or - isLeaked(resource, cfgNode.getAPredecessor()) and - not exists(DataFlow::Node free, DataFlow::Node freed | - free.asExpr() = cfgNode and - Config::isFree(free, freed) and - Config::isAlias(freed, resource) - ) - } - - private ControlFlowNode getARawLeak(DataFlow::Node resource) { - Config::isResource(resource) and - result = Config::outOfScope(resource) and - isLeaked(resource, result) - } - - ControlFlowNode getALeak(DataFlow::Node resource) { - result = getARawLeak(resource) and - not exists(DataFlow::Node dealiased | - Config::isResource(dealiased) and - Config::isAlias(resource, dealiased) and - not resource = dealiased and - result = getARawLeak(dealiased) - ) and - not exists(ControlFlowNode dominator | - dominator = getARawLeak(resource) and - strictlyDominates(dominator, result) - ) - } -} - -module MissedInfinityConfig implements ResourceLeakConfigSig { - predicate isResource(DataFlow::Node node) { - //exists(BinaryOperation expr | - // expr = node.asExpr() and - // expr.getOperator() = "/" and - // RestrictedRangeAnalysis::upperBound(expr.getRightOperand()) <= 0 and - // RestrictedRangeAnalysis::lowerBound(expr.getRightOperand()) >= 0 - //) - [ - RestrictedRangeAnalysis::upperBound(node.asExpr()), - RestrictedRangeAnalysis::lowerBound(node.asExpr()) - ].toString() = "Infinity" - //and not node.asExpr() instanceof VariableAccess - //and not node.asExpr() instanceof ArrayExpr - } - - predicate test(Expr expr, string lowerBound, string upperBound) { - //expr.getType() instanceof FloatingPointType - //and - lowerBound = RestrictedRangeAnalysis::lowerBound(expr).toString() and - upperBound = RestrictedRangeAnalysis::upperBound(expr).toString() and - [lowerBound, upperBound] = "Infinity" - } - - additional predicate testDiv( - DivExpr div, string lbDiv, string ubDiv, string lbNum, string ubNum, string lbDenom, - string ubDenom - ) { - lbDiv = RestrictedRangeAnalysis::lowerBound(div).toString() and - ubDiv = RestrictedRangeAnalysis::upperBound(div).toString() and - lbNum = RestrictedRangeAnalysis::lowerBound(div.getLeftOperand()).toString() and - ubNum = RestrictedRangeAnalysis::upperBound(div.getLeftOperand()).toString() and - lbDenom = RestrictedRangeAnalysis::lowerBound(div.getRightOperand()).toString() and - ubDenom = RestrictedRangeAnalysis::upperBound(div.getRightOperand()).toString() and - not lbDiv = ubDiv and - InvalidNaNUsage::isSource(DataFlow::exprNode(div)) - } - - predicate isFree(DataFlow::Node node, DataFlow::Node resource) { - isResource(resource) and - ( - node.asExpr().(InfinityCheckedExpr).getCheckedExpr() = resource.asExpr() - or - not [ - RestrictedRangeAnalysis::lowerBound(node.asExpr()), - RestrictedRangeAnalysis::upperBound(node.asExpr()) - ].toString() = "Infinity" and - isMove(node, resource) - ) - } - - predicate isMove(DataFlow::Node node, DataFlow::Node moved) { - isResource(moved) and - isAlias(node, moved) and - not exists(DataFlow::Node laterUse, ControlFlowNode later | - later = laterUse.asExpr() and - later = node.asExpr().getASuccessor+() and - hashCons(laterUse.asExpr()) = hashCons(moved.asExpr()) - ) - } - - ControlFlowNode outOfScope(DataFlow::Node resource) { - result = resource.asExpr().getEnclosingFunction().getBlock().getLastStmt() - or - exists(AssignExpr assign, DataFlow::Node alias | - assign.getRValue() = alias.asExpr() and - isAlias(alias, resource) and - not assign.getRValue().(VariableAccess).getTarget() instanceof StackVariable and - result = assign - ) - or - exists(FunctionCall fc | - fc.getArgument(_) = resource.asExpr() and - result = fc - ) - } - - predicate isAlias(DataFlow::Node alias, DataFlow::Node resource) { - TaintTracking::localTaint(resource, alias) - } -} - -import ResourceLeak as MissedInfinity -*/ - -//from Expr value, FunctionCall fc -//where -// not isExcluded(value, FloatingTypes2Package::possibleUndetectedNaNorInfinityQuery()) and -// [RestrictedRangeAnalysis::lowerBound(value), RestrictedRangeAnalysis::upperBound(value)].toString() = "Infinity" and -// value = fc.getAnArgument() and -// fc.getTarget() instanceof CantHandleInfinityFunction and -// not value instanceof InfinityCheckedExpr and -// not exists (GuardCondition g | -// g.controls(fc.getBasicBlock(), true) and -// g instanceof InfinityCheckedExpr -// // TODO check we check the right expr -// ) -//select -// value, "possible use of unchecked infinity as arg to " + fc.getTarget().getName() -//from DataFlow::Node node, ControlFlowNode leakPoint -//where -// not isExcluded(node.asExpr(), FloatingTypes2Package::possibleUndetectedNaNorInfinityQuery()) and -// leakPoint = MissedInfinity::getALeak(node) -// select node, "Expression generates an infinity which is not checked before $@.", leakPoint, "external leak point" - - -//import InvalidNaNFlow::PathGraph -//from Element elem, DataFlow::Node source, DataFlow::Node sink, string msg, string sourceString -from - Element elem, InvalidInfinityFlow::PathNode source, InvalidInfinityFlow::PathNode sink, - string msg, string sourceString -where - elem = MacroUnwrapper::unwrapElement(sink.getNode().asExpr()) and - not isExcluded(elem, FloatingTypes2Package::possibleUndetectedNaNorInfinityQuery()) and - ( - InvalidInfinityFlow::flow(source.getNode(), sink.getNode()) and - msg = "Invalid usage of possible $@." and - sourceString = "infinity" - //or - //InvalidNaNFlow::flow(source, sink) and - //msg = "Invalid usage of possible $@." and - //sourceString = "NaN resulting from " + source.asExpr().(InvalidOperationExpr).getReason() - ) -select elem, source, sink, msg, source, sourceString diff --git a/c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.expected b/c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.expected deleted file mode 100644 index 2ec1a0ac6c..0000000000 --- a/c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.expected +++ /dev/null @@ -1 +0,0 @@ -No expected results have yet been specified \ No newline at end of file diff --git a/c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.qlref b/c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.qlref deleted file mode 100644 index 1ffb7ad071..0000000000 --- a/c/misra/test/rules/DIR-4-15/PossibleUndetectedNaNorInfinity.qlref +++ /dev/null @@ -1 +0,0 @@ -rules/DIR-4-15/PossibleUndetectedNaNorInfinity.ql \ No newline at end of file diff --git a/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll b/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll index 9b4bba8980..8ae3c9c38b 100644 --- a/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll +++ b/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll @@ -1,5 +1,6 @@ import semmle.code.cpp.controlflow.Guards import semmle.code.cpp.valuenumbering.HashCons + /** * A fork of SimpleRangeAnalysis.qll, which is intended to only give * results with a conservative basis. @@ -311,7 +312,6 @@ module RestrictedRangeAnalysis { ) } - /** * Holds if `expr` is checked with a guard to not be zero. * @@ -332,7 +332,8 @@ module RestrictedRangeAnalysis { expr = def.getAUse(v) and isNEPhi(v, def, guardVa, 0) ) - or guardedHashConsNotEqualZero(expr) + or + guardedHashConsNotEqualZero(expr) } predicate guardedHashConsNotEqualZero(Expr e) { @@ -342,8 +343,8 @@ module RestrictedRangeAnalysis { valVal = getValue(val).toFloat() and guard.controls(e.getBasicBlock(), cmpEq) and ( - guard.comparesEq(check, val, -valVal, false, cmpEq) or - guard.comparesEq(val, check, -valVal, false, cmpEq) + guard.comparesEq(check, val, -valVal, false, cmpEq) or + guard.comparesEq(val, check, -valVal, false, cmpEq) ) ) } @@ -363,11 +364,11 @@ module RestrictedRangeAnalysis { dividesByPositive(e, _, _) or dividesByNegative(e, _, _) + or // Introduces non-monotonic recursion. However, analysis mostly works with this // commented out. // or // dividesNonzeroByZero(e) - or e instanceof DivExpr // TODO: confirm this is OK or e instanceof MinExpr @@ -469,6 +470,8 @@ module RestrictedRangeAnalysis { exprDependsOnDef(operand, srcDef, srcVar) ) or + exists(DivExpr div | div = e | exprDependsOnDef(div.getAnOperand(), srcDef, srcVar)) + or exists(MinExpr minExpr | e = minExpr | exprDependsOnDef(minExpr.getAnOperand(), srcDef, srcVar)) or exists(MaxExpr maxExpr | e = maxExpr | exprDependsOnDef(maxExpr.getAnOperand(), srcDef, srcVar)) @@ -595,6 +598,98 @@ module RestrictedRangeAnalysis { isRecursiveExpr(binop.getRightOperand()) } + private predicate applyWideningToBinary(BinaryOperation op) { + // Original behavior: + isRecursiveBinary(op) + or + // As we added support for DivExpr, we found cases of combinatorial explosion that are not + // caused by recursion. Given expr `x` that depends on a phi node that has evaluated y unique + // values, `x + x` will in the worst case evaluate to y^2 unique values, even if `x` is not + // recursive. By adding support for division, we have revealed certain pathological cases in + // open source code, for instance `posix_time_from_utc` from boringssl. We can reduce this + // greatly by widening, and targeting division effectively reduces the chains of evaluations + // that cause this issue while preserving the original behavior. + // + // There is also a set of functions intended to estimate the combinations of phi nodes each + // expression depends on, which could be used to accurately widen only expensive nodes. However, + // that estimation is more involved than it may seem, and hasn't yet resulted in a net + // improvement. See `estimatedPhiCombinationsExpr` and `estimatedPhiCombinationsDef`. + // + // This approach currently has the best performance. + op instanceof DivExpr + } + + /** + * Recursively scan this expr to see how many phi nodes it depends on. Binary expressions + * induce a combination effect, so `a + b` where `a` depends on 3 phi nodes and `b` depends on 4 + * will induce 3*4 = 12 phi node combinations. + * + * This currently requires additional optimization to be useful in practice. + */ + int estimatedPhiCombinationsExpr(Expr expr) { + if isRecursiveExpr(expr) + // Assume 10 values were computed to analyze recursive expressions. + then result = 10 + else ( + exists(RangeSsaDefinition def, StackVariable v | expr = def.getAUse(v) | + def.isPhiNode(v) and + result = estimatedPhiCombinationsDef(def, v) + ) + or + exists(BinaryOperation binop | + binop = expr and + result = + estimatedPhiCombinationsExpr(binop.getLeftOperand()) * + estimatedPhiCombinationsExpr(binop.getRightOperand()) + ) + or + not expr instanceof BinaryOperation and + exists(RangeSsaDefinition def, StackVariable v | exprDependsOnDef(expr, def, v) | + result = estimatedPhiCombinationsDef(def, v) + ) + or + not expr instanceof BinaryOperation and + not exprDependsOnDef(expr, _, _) and result = 1 + ) + } + + /** + * Recursively scan this def to see how many phi nodes it depends on. + * + * If this def is a phi node, it sums its downstream cost and adds one to account for itself, + * which is not exactly correct. + * + * This def may also be a crement expression (not currently supported), or an assign expr + * (currently not supported), or an unanalyzable expression which is the root of the recursion + * and given a value of 1. + */ + language[monotonicAggregates] + int estimatedPhiCombinationsDef(RangeSsaDefinition def, StackVariable v) { + if isRecursiveDef(def, v) + // Assume 10 values were computed to analyze recursive expressions. + then result = 10 + else ( + if def.isPhiNode(v) + then + exists(Expr e | e = def.getAUse(v) | + result = + 1 + + sum(RangeSsaDefinition srcDef | + srcDef = def.getAPhiInput(v) + | + estimatedPhiCombinationsDef(srcDef, v) + ) + ) + else ( + exists(Expr expr | assignmentDef(def, v, expr) | result = estimatedPhiCombinationsExpr(expr)) + or + v = def.getAVariable() and + not assignmentDef(def, v, _) and + result = 1 + ) + ) + } + /** * We distinguish 3 kinds of RangeSsaDefinition: * @@ -719,7 +814,7 @@ module RestrictedRangeAnalysis { if Util::exprMinVal(expr) <= newLB and newLB <= Util::exprMaxVal(expr) then // Apply widening where we might get a combinatorial explosion. - if isRecursiveBinary(expr) + if applyWideningToBinary(expr) then result = max(float widenLB | @@ -764,8 +859,8 @@ module RestrictedRangeAnalysis { * this predicate. */ private float getTruncatedUpperBounds(Expr expr) { - (analyzableExpr(expr) or dividesNonzeroByZero(expr)) - and ( + (analyzableExpr(expr) or dividesNonzeroByZero(expr)) and + ( // If the expression evaluates to a constant, then there is no // need to call getUpperBoundsImpl. if exists(getValue(expr).toFloat()) @@ -778,7 +873,7 @@ module RestrictedRangeAnalysis { if Util::exprMinVal(expr) <= newUB and newUB <= Util::exprMaxVal(expr) then // Apply widening where we might get a combinatorial explosion. - if isRecursiveBinary(expr) + if applyWideningToBinary(expr) then result = min(float widenUB | @@ -794,13 +889,14 @@ module RestrictedRangeAnalysis { exprMightOverflowNegatively(expr) and result = Util::exprMaxVal(expr) ) - ) or + ) + or not analyzableExpr(expr) and - // The expression is not analyzable, so its upper bound is - // unknown. Note that the call to exprMaxVal restricts the - // expressions to just those with arithmetic types. There is no - // need to return results for non-arithmetic expressions. - result = exprMaxVal(expr) + // The expression is not analyzable, so its upper bound is + // unknown. Note that the call to exprMaxVal restricts the + // expressions to just those with arithmetic types. There is no + // need to return results for non-arithmetic expressions. + result = exprMaxVal(expr) } /** Only to be called by `getTruncatedLowerBounds`. */ From dee226188f61262f5f5a02173c1545c7ad8783ca Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Fri, 7 Feb 2025 04:28:13 -0800 Subject: [PATCH 4/9] Widening/dedupe fixes, plus math lib support --- .../PossibleMisuseOfUndetectedInfinity.ql | 8 +- .../DIR-4-15/PossibleMisuseOfUndetectedNaN.ql | 74 +++++- ...ossibleMisuseOfUndetectedInfinity.expected | 82 ++++-- .../PossibleMisuseOfUndetectedNaN.expected | 108 +++++--- c/misra/test/rules/DIR-4-15/test.c | 59 ++++- .../cpp/RestrictedRangeAnalysis.qll | 242 +++++++++++++++++- 6 files changed, 496 insertions(+), 77 deletions(-) diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql index 10c370690b..357a8fce71 100644 --- a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql +++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql @@ -51,9 +51,6 @@ module InvalidInfinityUsage implements DataFlow::ConfigSig { e.getType() instanceof IntegralType and e = node.asConvertedExpr() ) - or - // Sinks are places where Infinity produce a finite value - isSink(node) } /** @@ -81,7 +78,9 @@ module InvalidInfinityUsage implements DataFlow::ConfigSig { or // Unanalyzable expressions are not checked against range analysis, which assumes a finite // range. - not RestrictedRangeAnalysis::analyzableExpr(node.asExpr()) + not RestrictedRangeAnalysis::canBoundExpr(node.asExpr()) + or + node.asExpr().(VariableAccess).getTarget() instanceof Parameter ) } } @@ -124,6 +123,7 @@ from where elem = MacroUnwrapper::unwrapElement(sink.getNode().asExpr()) and not InvalidInfinityFlow::PathGraph::edges(_, source, _, _) and + not InvalidInfinityFlow::PathGraph::edges(sink, _, _, _) and not isExcluded(elem, FloatingTypes2Package::possibleMisuseOfUndetectedInfinityQuery()) and not sourceExpr.isFromTemplateInstantiation(_) and not usage.asExpr().isFromTemplateInstantiation(_) and diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql index 942715fe2f..f850cc3e55 100644 --- a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql +++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql @@ -23,8 +23,73 @@ import semmle.code.cpp.dataflow.new.DataFlow import semmle.code.cpp.dataflow.new.TaintTracking import semmle.code.cpp.controlflow.Dominance +bindingset[name] +Function getMathVariants(string name) { result.hasGlobalOrStdName([name, name + "f", name + "l"]) } + +predicate hasDomainError(FunctionCall fc, string description) { + exists(Function functionWithDomainError | fc.getTarget() = functionWithDomainError | + functionWithDomainError = [getMathVariants(["acos", "asin", "atanh"])] and + not ( + RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) <= 1.0 and + RestrictedRangeAnalysis::lowerBound(fc.getArgument(0)) >= -1.0 + ) 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)" + or + functionWithDomainError = getMathVariants(["atan2", "pow"]) and + ( + exprMayEqualZero(fc.getArgument(0)) and + exprMayEqualZero(fc.getArgument(1)) and + description = "both arguments are equal to zero" + ) + or + functionWithDomainError = getMathVariants("pow") and + ( + RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) < 0.0 and + RestrictedRangeAnalysis::upperBound(fc.getArgument(1)) < 0.0 and + description = "both arguments are less than zero" + ) + or + functionWithDomainError = getMathVariants("acosh") and + RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) < 1.0 and + description = "argument is less than 1" + or + //pole error is the same as domain for logb and tgamma (but not ilogb - no pole error exists) + functionWithDomainError = getMathVariants(["ilogb", "logb", "tgamma"]) and + exprMayEqualZero(fc.getArgument(0)) and + description = "argument is equal to zero" + or + functionWithDomainError = getMathVariants(["log", "log10", "log2", "sqrt"]) and + RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) < 0.0 and + description = "argument is negative" + or + functionWithDomainError = getMathVariants("log1p") and + RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) < -1.0 and + description = "argument is less than 1" + or + functionWithDomainError = getMathVariants("fmod") and + exprMayEqualZero(fc.getArgument(1)) and + description = "y is 0" + ) +} + +abstract class PotentiallyNaNExpr extends Expr { + abstract string getReason(); +} + +class DomainErrorFunctionCall extends FunctionCall, PotentiallyNaNExpr { + string reason; + + DomainErrorFunctionCall() { + hasDomainError(this, reason) + } + + override string getReason() { result = reason } +} + // IEEE 754-1985 Section 7.1 invalid operations -class InvalidOperationExpr extends BinaryOperation { +class InvalidOperationExpr extends BinaryOperation, PotentiallyNaNExpr { string reason; InvalidOperationExpr() { @@ -85,7 +150,7 @@ class InvalidOperationExpr extends BinaryOperation { ) } - string getReason() { result = reason } + override string getReason() { result = reason } } module InvalidNaNUsage implements DataFlow::ConfigSig { @@ -104,7 +169,7 @@ module InvalidNaNUsage implements DataFlow::ConfigSig { * An expression which may produce a NaN output. */ additional predicate potentialSource(DataFlow::Node node) { - node.asExpr() instanceof InvalidOperationExpr + node.asExpr() instanceof PotentiallyNaNExpr } predicate isBarrierOut(DataFlow::Node node) { @@ -173,13 +238,14 @@ from InvalidNaNUsage usage, Expr sourceExpr, string sourceString, Element extra, string extraString where not InvalidNaNFlow::PathGraph::edges(_, source, _, _) and + not InvalidNaNFlow::PathGraph::edges(sink, _, _, _) and not sourceExpr.isFromTemplateInstantiation(_) and not usage.asExpr().isFromTemplateInstantiation(_) and elem = MacroUnwrapper::unwrapElement(sink.getNode().asExpr()) and usage = sink.getNode() and sourceExpr = source.getNode().asExpr() and sourceString = - " (" + source.getNode().asExpr().(InvalidOperationExpr).getReason() + ")" and + " (" + source.getNode().asExpr().(PotentiallyNaNExpr).getReason() + ")" and InvalidNaNFlow::flow(source.getNode(), usage) and ( if not sourceExpr.getEnclosingFunction() = usage.asExpr().getEnclosingFunction() diff --git a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected index 75534df6a0..f1f08b5a51 100644 --- a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected +++ b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected @@ -21,6 +21,21 @@ edges | test.c:77:15:77:21 | ... / ... | test.c:114:16:114:23 | l12 | provenance | | | test.c:77:15:77:21 | ... / ... | test.c:117:23:117:30 | l12 | provenance | | | test.c:77:15:77:21 | ... / ... | test.c:120:20:120:27 | l12 | provenance | | +| test.c:175:22:175:22 | p | test.c:175:27:175:32 | p | provenance | | +| test.c:183:34:183:34 | p | test.c:185:13:185:18 | p | provenance | | +| test.c:189:32:189:32 | p | test.c:189:47:189:59 | ... + ... | provenance | Config | +| test.c:189:47:189:59 | ... + ... | test.c:175:22:175:22 | p | provenance | | +| test.c:189:47:189:59 | ... + ... | test.c:175:22:175:22 | p | provenance | | +| test.c:189:51:189:59 | ... / ... | test.c:189:47:189:59 | ... + ... | provenance | Config | +| test.c:193:13:194:15 | ... / ... | test.c:175:22:175:22 | p | provenance | | +| test.c:200:25:200:33 | ... / ... | test.c:183:34:183:34 | p | provenance | | +| test.c:204:19:204:27 | ... / ... | test.c:204:19:204:27 | ... / ... | provenance | | +| test.c:204:19:204:27 | ... / ... | test.c:206:21:206:31 | ... + ... | provenance | Config | +| test.c:206:21:206:31 | ... + ... | test.c:206:21:206:31 | ... + ... | provenance | | +| test.c:206:21:206:31 | ... + ... | test.c:208:13:208:21 | middleInf | provenance | | +| test.c:206:21:206:31 | ... + ... | test.c:210:23:210:31 | middleInf | provenance | | +| test.c:208:13:208:21 | middleInf | test.c:175:22:175:22 | p | provenance | | +| test.c:210:23:210:31 | middleInf | test.c:189:32:189:32 | p | provenance | | nodes | test.c:8:14:8:20 | ... / ... | semmle.label | ... / ... | | test.c:8:14:8:20 | ... / ... | semmle.label | ... / ... | @@ -51,29 +66,48 @@ nodes | test.c:114:16:114:23 | l12 | semmle.label | l12 | | test.c:117:23:117:30 | l12 | semmle.label | l12 | | test.c:120:20:120:27 | l12 | semmle.label | l12 | +| test.c:163:3:164:16 | ... / ... | semmle.label | ... / ... | +| test.c:175:22:175:22 | p | semmle.label | p | +| test.c:175:27:175:32 | p | semmle.label | p | +| test.c:183:34:183:34 | p | semmle.label | p | +| test.c:185:13:185:18 | p | semmle.label | p | +| test.c:189:32:189:32 | p | semmle.label | p | +| test.c:189:47:189:59 | ... + ... | semmle.label | ... + ... | +| test.c:189:47:189:59 | ... + ... | semmle.label | ... + ... | +| test.c:189:51:189:59 | ... / ... | semmle.label | ... / ... | +| test.c:193:13:194:15 | ... / ... | semmle.label | ... / ... | +| test.c:200:25:200:33 | ... / ... | semmle.label | ... / ... | +| test.c:204:19:204:27 | ... / ... | semmle.label | ... / ... | +| test.c:204:19:204:27 | ... / ... | semmle.label | ... / ... | +| test.c:206:21:206:31 | ... + ... | semmle.label | ... + ... | +| test.c:206:21:206:31 | ... + ... | semmle.label | ... + ... | +| test.c:208:13:208:21 | middleInf | semmle.label | middleInf | +| test.c:210:23:210:31 | middleInf | semmle.label | middleInf | subpaths #select -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | +| test.c:12:8:12:9 | l2 | test.c:8:14:8:20 | ... / ... | test.c:12:8:12:9 | l2 | Division operation may silently underflow and produce zero, as the divisor $@. | test.c:8:14:8:20 | ... / ... | may be an infinite float value from division by zero | +| test.c:13:8:13:9 | l3 | test.c:8:14:8:20 | ... / ... | test.c:13:8:13:9 | l3 | Division operation may silently underflow and produce zero, as the divisor $@. | test.c:8:14:8:20 | ... / ... | may be an infinite float value from division by zero | +| test.c:18:8:18:9 | l2 | test.c:8:14:8:20 | ... / ... | test.c:18:3:18:9 | l2 | $@ casted to integer. | test.c:8:14:8:20 | ... / ... | Possibly infinite float value from division by zero | +| test.c:19:8:19:9 | l3 | test.c:8:14:8:20 | ... / ... | test.c:19:3:19:9 | l3 | $@ casted to integer. | test.c:8:14:8:20 | ... / ... | Possibly infinite float value from division by zero | +| test.c:27:19:27:20 | l2 | test.c:8:14:8:20 | ... / ... | test.c:27:19:27:20 | l2 | Division operation may silently underflow and produce zero, as the divisor $@. | test.c:8:14:8:20 | ... / ... | may be an infinite float value from division by zero | +| test.c:28:19:28:20 | l3 | test.c:8:14:8:20 | ... / ... | test.c:28:19:28:20 | l3 | Division operation may silently underflow and produce zero, as the divisor $@. | test.c:8:14:8:20 | ... / ... | may be an infinite float value from division by zero | +| test.c:38:8:38:9 | l7 | test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | $@ casted to integer. | test.c:31:14:32:15 | ... / ... | Possibly infinite float value from division by zero | +| test.c:61:11:61:17 | ... / ... | test.c:61:5:61:18 | ... / ... | test.c:61:5:61:18 | ... / ... | $@ casted to integer. | test.c:61:11:61:17 | ... / ... | Possibly infinite float value from division by zero | +| test.c:66:11:66:19 | ... / ... | test.c:66:5:66:20 | ... / ... | test.c:66:5:66:20 | ... / ... | $@ casted to integer. | test.c:66:11:66:19 | ... / ... | Possibly infinite float value from division by zero | +| test.c:72:20:72:28 | ... / ... | test.c:72:14:72:29 | ... / ... | test.c:72:14:72:29 | ... / ... | $@ casted to integer. | test.c:72:20:72:28 | ... / ... | Possibly infinite float value from division by zero | +| test.c:75:24:75:32 | ... / ... | test.c:75:18:75:33 | ... / ... | test.c:75:18:75:33 | ... / ... | $@ casted to integer. | test.c:75:24:75:32 | ... / ... | Possibly infinite float value from division by zero | +| test.c:79:10:79:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:79:5:79:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero | +| test.c:87:10:87:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:87:5:87:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero | +| test.c:91:10:91:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:91:5:91:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero | +| test.c:93:10:93:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:93:5:93:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero | +| test.c:99:10:99:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:99:5:99:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero | +| test.c:105:10:105:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:105:5:105:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero | +| test.c:111:10:111:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:111:5:111:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero | +| test.c:114:21:114:23 | l12 | test.c:77:15:77:21 | ... / ... | test.c:114:16:114:23 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero | +| test.c:117:28:117:30 | l12 | test.c:77:15:77:21 | ... / ... | test.c:117:23:117:30 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero | +| test.c:120:25:120:27 | l12 | test.c:77:15:77:21 | ... / ... | test.c:120:20:120:27 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero | +| test.c:163:9:164:15 | ... / ... | test.c:163:3:164:16 | ... / ... | test.c:163:3:164:16 | ... / ... | $@ casted to integer. | test.c:163:9:164:15 | ... / ... | Possibly infinite float value from division by zero | +| test.c:175:32:175:32 | p | test.c:189:51:189:59 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:189:6:189:24 | addInfThenCastToInt | Possibly infinite float value computed in function addInfThenCastToInt | +| test.c:175:32:175:32 | p | test.c:193:13:194:15 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly infinite float value computed in function f2 | +| test.c:175:32:175:32 | p | test.c:204:19:204:27 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly infinite float value computed in function f2 | +| test.c:185:18:185:18 | p | test.c:200:25:200:33 | ... / ... | test.c:185:13:185:18 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly infinite float value computed in function f2 | diff --git a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected index e59d43d867..e0047d9ef7 100644 --- a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected +++ b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected @@ -22,9 +22,27 @@ edges | test.c:122:15:122:21 | ... / ... | test.c:138:5:138:12 | l13 | provenance | | | test.c:122:15:122:21 | ... / ... | test.c:144:5:144:12 | l13 | provenance | | | test.c:122:15:122:21 | ... / ... | test.c:148:5:148:12 | l13 | provenance | | -| test.c:122:15:122:21 | ... / ... | test.c:154:20:154:27 | l13 | provenance | | -| test.c:122:15:122:21 | ... / ... | test.c:156:23:156:30 | l13 | provenance | | -| test.c:122:15:122:21 | ... / ... | test.c:157:16:157:23 | l13 | provenance | | +| test.c:122:15:122:21 | ... / ... | test.c:155:20:155:27 | l13 | provenance | | +| test.c:122:15:122:21 | ... / ... | test.c:157:23:157:30 | l13 | provenance | | +| test.c:122:15:122:21 | ... / ... | test.c:158:16:158:23 | l13 | provenance | | +| test.c:175:22:175:22 | p | test.c:175:27:175:32 | p | provenance | | +| test.c:183:34:183:34 | p | test.c:185:13:185:18 | p | provenance | | +| test.c:188:32:188:32 | p | test.c:188:47:188:51 | ... + ... | provenance | Config | +| test.c:188:47:188:51 | ... + ... | test.c:175:22:175:22 | p | provenance | | +| test.c:190:32:190:32 | p | test.c:190:47:190:59 | ... + ... | provenance | Config | +| test.c:190:47:190:59 | ... + ... | test.c:175:22:175:22 | p | provenance | | +| test.c:190:47:190:59 | ... + ... | test.c:175:22:175:22 | p | provenance | | +| test.c:190:51:190:59 | ... / ... | test.c:190:47:190:59 | ... + ... | provenance | Config | +| test.c:195:13:195:21 | ... / ... | test.c:175:22:175:22 | p | provenance | | +| test.c:199:23:199:31 | ... / ... | test.c:188:32:188:32 | p | provenance | | +| test.c:201:25:201:33 | ... / ... | test.c:183:34:183:34 | p | provenance | | +| test.c:205:19:205:27 | ... / ... | test.c:205:19:205:27 | ... / ... | provenance | | +| test.c:205:19:205:27 | ... / ... | test.c:207:21:207:31 | ... + ... | provenance | Config | +| test.c:207:21:207:31 | ... + ... | test.c:207:21:207:31 | ... + ... | provenance | | +| test.c:207:21:207:31 | ... + ... | test.c:209:13:209:21 | middleNaN | provenance | | +| test.c:207:21:207:31 | ... + ... | test.c:211:23:211:31 | middleNaN | provenance | | +| test.c:209:13:209:21 | middleNaN | test.c:175:22:175:22 | p | provenance | | +| test.c:211:23:211:31 | middleNaN | test.c:190:32:190:32 | p | provenance | | nodes | test.c:27:14:27:20 | ... / ... | semmle.label | ... / ... | | test.c:27:14:27:20 | ... / ... | semmle.label | ... / ... | @@ -58,33 +76,61 @@ nodes | test.c:138:5:138:12 | l13 | semmle.label | l13 | | test.c:144:5:144:12 | l13 | semmle.label | l13 | | test.c:148:5:148:12 | l13 | semmle.label | l13 | -| test.c:154:20:154:27 | l13 | semmle.label | l13 | -| test.c:156:23:156:30 | l13 | semmle.label | l13 | -| test.c:157:16:157:23 | l13 | semmle.label | l13 | +| test.c:155:20:155:27 | l13 | semmle.label | l13 | +| test.c:157:23:157:30 | l13 | semmle.label | l13 | +| test.c:158:16:158:23 | l13 | semmle.label | l13 | +| test.c:166:3:166:18 | call to pow | semmle.label | call to pow | +| test.c:171:3:171:15 | call to acos | semmle.label | call to acos | +| test.c:175:22:175:22 | p | semmle.label | p | +| test.c:175:27:175:32 | p | semmle.label | p | +| test.c:183:34:183:34 | p | semmle.label | p | +| test.c:185:13:185:18 | p | semmle.label | p | +| test.c:188:32:188:32 | p | semmle.label | p | +| test.c:188:47:188:51 | ... + ... | semmle.label | ... + ... | +| test.c:190:32:190:32 | p | semmle.label | p | +| test.c:190:47:190:59 | ... + ... | semmle.label | ... + ... | +| test.c:190:47:190:59 | ... + ... | semmle.label | ... + ... | +| test.c:190:51:190:59 | ... / ... | semmle.label | ... / ... | +| test.c:195:13:195:21 | ... / ... | semmle.label | ... / ... | +| test.c:199:23:199:31 | ... / ... | semmle.label | ... / ... | +| test.c:201:25:201:33 | ... / ... | semmle.label | ... / ... | +| test.c:205:19:205:27 | ... / ... | semmle.label | ... / ... | +| test.c:205:19:205:27 | ... / ... | semmle.label | ... / ... | +| test.c:207:21:207:31 | ... + ... | semmle.label | ... + ... | +| test.c:207:21:207:31 | ... + ... | semmle.label | ... + ... | +| test.c:209:13:209:21 | middleNaN | semmle.label | middleNaN | +| test.c:211:23:211:31 | middleNaN | semmle.label | middleNaN | subpaths #select -| 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 | -| test.c:37:8:37:9 | l6 | test.c:28:14:28:20 | ... / ... | test.c:37:3:37:9 | l6 | Invalid usage of possible $@. | test.c:28:14:28:20 | ... / ... | NaN resulting from possible division of infinity by infinity | -| 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 | ... / ... | NaN resulting from possible division of zero by zero | -| 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 | ... / ... | NaN resulting from possible division of zero by zero | -| test.c:46:3:46:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:46:3:46:4 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity | -| test.c:47:3:47:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:47:3:47:4 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity | -| test.c:48:3:48:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:48:3:48:4 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity | -| test.c:49:3:49:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:49:3:49:4 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity | -| test.c:50:3:50:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:50:3:50:4 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity | -| test.c:51:3:51:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:51:3:51:4 | l5 | Invalid usage of possible $@. | test.c:27:14:27:20 | ... / ... | NaN resulting from possible division of infinity by infinity | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | -| 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 | +| test.c:36:8:36:9 | l5 | test.c:27:14:27:20 | ... / ... | test.c:36:3:36:9 | l5 | $@ casted to integer. | test.c:27:14:27:20 | ... / ... | Possibly NaN float value (from division of infinity by infinity) | +| test.c:37:8:37:9 | l6 | test.c:28:14:28:20 | ... / ... | test.c:37:3:37:9 | l6 | $@ casted to integer. | test.c:28:14:28:20 | ... / ... | Possibly NaN float value (from division of infinity by infinity) | +| test.c:38:8:38:9 | l7 | test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | $@ casted to integer. | test.c:31:14:32:15 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:39:8:39:9 | l8 | test.c:33:14:33:22 | ... / ... | test.c:39:3:39:9 | l8 | $@ casted to integer. | test.c:33:14:33:22 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:46:3:46:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:46:3:46:4 | l5 | Comparison involving a $@, which always evaluates to false. | test.c:27:14:27:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) | +| test.c:47:3:47:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:47:3:47:4 | l5 | Comparison involving a $@, which always evaluates to false. | test.c:27:14:27:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) | +| test.c:48:3:48:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:48:3:48:4 | l5 | Comparison involving a $@, which always evaluates to false. | test.c:27:14:27:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) | +| test.c:49:3:49:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:49:3:49:4 | l5 | Comparison involving a $@, which always evaluates to false. | test.c:27:14:27:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) | +| test.c:50:3:50:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:50:3:50:4 | l5 | Comparison involving a $@, which always evaluates to false. | test.c:27:14:27:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) | +| test.c:51:3:51:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:51:3:51:4 | l5 | Comparison involving a $@, which always evaluates to false. | test.c:27:14:27:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) | +| test.c:52:3:52:4 | l6 | test.c:28:14:28:20 | ... / ... | test.c:52:3:52:4 | l6 | Comparison involving a $@, which always evaluates to false. | test.c:28:14:28:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) | +| test.c:53:3:53:4 | l7 | test.c:31:14:32:15 | ... / ... | test.c:53:3:53:4 | l7 | Comparison involving a $@, which always evaluates to false. | test.c:31:14:32:15 | ... / ... | possibly NaN float value (from division of zero by zero) | +| test.c:54:3:54:4 | l8 | test.c:33:14:33:22 | ... / ... | test.c:54:3:54:4 | l8 | Comparison involving a $@, which always evaluates to false. | test.c:33:14:33:22 | ... / ... | possibly NaN float value (from division of zero by zero) | +| test.c:61:11:61:17 | ... / ... | test.c:61:5:61:18 | ... / ... | test.c:61:5:61:18 | ... / ... | $@ casted to integer. | test.c:61:11:61:17 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:66:11:66:19 | ... / ... | test.c:66:5:66:20 | ... / ... | test.c:66:5:66:20 | ... / ... | $@ casted to integer. | test.c:66:11:66:19 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:72:20:72:28 | ... / ... | test.c:72:14:72:29 | ... / ... | test.c:72:14:72:29 | ... / ... | $@ casted to integer. | test.c:72:20:72:28 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:75:24:75:32 | ... / ... | test.c:75:18:75:33 | ... / ... | test.c:75:18:75:33 | ... / ... | $@ casted to integer. | test.c:75:24:75:32 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:126:10:126:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:126:5:126:12 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:132:10:132:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:132:5:132:12 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:138:10:138:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:138:5:138:12 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:144:10:144:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:144:5:144:12 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:148:10:148:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:148:5:148:12 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:155:25:155:27 | l13 | test.c:122:15:122:21 | ... / ... | test.c:155:20:155:27 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:157:28:157:30 | l13 | test.c:122:15:122:21 | ... / ... | test.c:157:23:157:30 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:158:21:158:23 | l13 | test.c:122:15:122:21 | ... / ... | test.c:158:16:158:23 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) | +| test.c:166:8:166:10 | call to pow | test.c:166:3:166:18 | call to pow | test.c:166:3:166:18 | call to pow | $@ casted to integer. | test.c:166:8:166:10 | call to pow | Possibly NaN float value (both arguments are equal to zero) | +| test.c:171:8:171:11 | call to acos | test.c:171:3:171:15 | call to acos | test.c:171:3:171:15 | call to acos | $@ casted to integer. | test.c:171:8:171:11 | call to acos | Possibly NaN float value (the argument has a range -1000000000000000...1000000000000000 which is outside the domain of this function (-1.0...1.0)) | +| test.c:175:32:175:32 | p | test.c:190:51:190:59 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:190:6:190:24 | addNaNThenCastToInt | Possibly NaN float value (from division of zero by zero) computed in function addNaNThenCastToInt | +| test.c:175:32:175:32 | p | test.c:195:13:195:21 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly NaN float value (from division of zero by zero) computed in function f2 | +| test.c:175:32:175:32 | p | test.c:199:23:199:31 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly NaN float value (from division of zero by zero) computed in function f2 | +| test.c:175:32:175:32 | p | test.c:205:19:205:27 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly NaN float value (from division of zero by zero) computed in function f2 | +| test.c:185:18:185:18 | p | test.c:201:25:201:33 | ... / ... | test.c:185:13:185:18 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly NaN float value (from division of zero by zero) computed in function f2 | diff --git a/c/misra/test/rules/DIR-4-15/test.c b/c/misra/test/rules/DIR-4-15/test.c index d0f9ab5418..e615d3447a 100644 --- a/c/misra/test/rules/DIR-4-15/test.c +++ b/c/misra/test/rules/DIR-4-15/test.c @@ -150,10 +150,63 @@ void f1(float p1) { (int)l13; // COMPLIANT: Guarded not to be NaN } - isinf(l13) ? (int)l13 : 0; // COMPLIANT: Checked infinite, therefore not NaN, before use + isinf(l13) ? (int)l13 + : 0; // COMPLIANT: Checked infinite, therefore not NaN, before use isinf(l13) ? 0 : (int)l13; // COMPLIANT: Check on wrong branch isfinite(l13) ? (int)l13 : 0; // COMPLIANT: Checked finite before use isfinite(l13) ? 0 : (int)l13; // NON_COMPLIANT: Checked on wrong branch - isnan(l13) ? (int)l13 : 0; // NON_COMPLIANT: Check on wrong branch - isnan(l13) ? 0 : (int)l13; // COMPLIANT: Checked not NaN before use + isnan(l13) ? (int)l13 : 0; // NON_COMPLIANT: Check on wrong branch + isnan(l13) ? 0 : (int)l13; // COMPLIANT: Checked not NaN before use + + (int)pow(2, p1); // NON_COMPLIANT: likely to be Infinity + (int)pow(2, sin(p1)); // COMPLIANT: not likely to be Infinity + (int)(1 / + sin(p1)); // NON_COMPLIANT: possible infinity from zero in denominator + (int)(1 / log(p1)); // COMPLIANT: not possibly zero in denominator + (int)pow(p1, p1); // NON_COMPLIANT: NaN if p1 is zero + if (p1 != 0) { + (int)pow(p1, p1); // COMPLIANT: p1 is not zero + } + + (int)acos(p1); // NON_COMPLIANT: NaN if p1 is not within -1..1 + (int)acos(cos(p1)); // COMPLIANT: cos(p1) is within -1..1 +} + +void castToInt(float p) { (int)p; } + +void checkBeforeCastToInt(float p) { + if (isfinite(p)) { + castToInt(p); + } +} + +void castToIntToFloatToInt(float p) { + // This should be reported as a violation, but not downstream from here. + castToInt((int)p); +} + +void addOneThenCastToInt(float p) { castToInt(p + 1); } +void addInfThenCastToInt(float p) { castToInt(p + 1.0 / 0.0); } +void addNaNThenCastToInt(float p) { castToInt(p + 0.0 / 0.0); } + +void f2() { + castToInt(1.0 / + 0.0); // NON_COMPLIANT: Infinity flows to denominator in division + castToInt(0.0 / 0.0); // NON_COMPLIANT: NaN flows to denominator in division + checkBeforeCastToInt(1.0 / 0.0); // COMPLIANT + checkBeforeCastToInt(0.0 / 0.0); // COMPLIANT + addOneThenCastToInt(1.0 / 0.0); // NON_COMPLIANT[False negative] + addOneThenCastToInt(0.0 / 0.0); // NON_COMPLIANT + castToIntToFloatToInt(1.0 / 0.0); // NON_COMPLIANT + castToIntToFloatToInt(0.0 / 0.0); // NON_COMPLIANT + + // Check that during flow analysis, we only report the true root cause: + float rootInf = 1.0 / 0.0; + float rootNaN = 0.0 / 0.0; + float middleInf = rootInf + 1; + float middleNaN = rootNaN + 1; + castToInt(middleInf); // NON_COMPLIANT + castToInt(middleNaN); // NON_COMPLIANT + addInfThenCastToInt(middleInf); // NON_COMPLIANT + addNaNThenCastToInt(middleNaN); // NON_COMPLIANT } \ No newline at end of file diff --git a/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll b/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll index 8ae3c9c38b..0c98824dbf 100644 --- a/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll +++ b/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll @@ -84,7 +84,9 @@ module RestrictedRangeAnalysis { result = -256.0 or result = -32768.0 or result = -65536.0 or - result = max(float v | v = Util::typeLowerBound(t) or v = -largeValue()) + result = -largeValue() or + result = Util::typeLowerBound(t) + //result = max(float v | v = Util::typeLowerBound(t) or v = -largeValue()) } /** See comment for `wideningLowerBounds`, above. */ @@ -100,7 +102,9 @@ module RestrictedRangeAnalysis { result = 255.0 or result = 32767.0 or result = 65535.0 or - result = min(float v | v = Util::typeLowerBound(t) or v = largeValue()) + result = largeValue() or + result = Util::typeUpperBound(t) + //result = min(float v | v = Util::typeLowerBound(t) or v = largeValue()) } /** @@ -312,6 +316,196 @@ module RestrictedRangeAnalysis { ) } + bindingset[name] + Function getMathVariants(string name) { + result.hasGlobalOrStdName([name, name + "f", name + "l"]) + } + + /** + * New support added for mathematical functions that either monotonically increase, or decrease, + * or that have a known lower or upper bound. + * + * For instance, log(x) monotonically increases over x, and acos(x) monotonically decreases, + * while sin(x) has a known output range of -1 to 1. + * + * `pow` is especially common so minimal work is done to support that here as well. `pow(c, x)` + * monotonically increases or decreases over `x` if `c` is a constant, though the reverse is not + * true except in special cases. + */ + newtype TSupportedMathFunctionCall = + /* A monotonically increasing function call. `extra` is a constant for `pow(x, c)`. */ + TMonotonicIncrease(FunctionCall fc, Expr input, float extra) { + // Note: Codeql has no default implementation in codeql for exp2, atanh, acosh, asinh, or + // log1p so we haven't taken the time to support them yet. + fc.getTarget() = + getMathVariants(["log", "log2", "log10", "exp", "asin", "atan", "sinh", "sqrt"]) and + input = fc.getArgument(0) and + extra = 0.0 + or + // Notes: pow is monotonic if the base argument is constant, increasing if the base is greater + // than 1 or between -1 and 0, and decreasing otherwise. A constant power is monotonic over the + // base in the positive or negative domain, but distinguishing those separately can introduce + // non-monotonic recursion errors. + fc.getTarget() = getMathVariants("pow") and + extra = fc.getArgument(0).getValue().toFloat() and + ( + extra > 1.0 + or + extra < 0.0 and extra > -1.0 + ) and + input = fc.getArgument(1) + } or + /* A monotonically decreasing function call. `extra` is a constant for `pow(x, c)`. */ + TMonotonicDecrease(FunctionCall fc, Expr input, float extra) { + fc.getTarget() = getMathVariants(["acos"]) and + input = fc.getArgument(0) and + extra = 0.0 + or + fc.getTarget() = getMathVariants("pow") and + extra = fc.getArgument(0).getValue().toFloat() and + ( + extra < -1.0 + or + extra > 0.0 and extra < 1.0 + ) and + input = fc.getArgument(1) + } or + /* A non-mononotic function call with a known lower bound. */ + TNonMonotonicLowerBound(FunctionCall fc, float lb) { + fc.getTarget() = getMathVariants("cosh") and + lb = 1.0 + or + fc.getTarget() = getMathVariants(["cos", "sin"]) and + lb = -1.0 + } or + /* A non-mononotic function call with a known upper bound. */ + TNonMonotonicUpperBound(FunctionCall fc, float lb) { + fc.getTarget() = getMathVariants(["cos", "sin"]) and + lb = 1.0 + } + + /** + * A function call that is supported by range analysis. + */ + class SupportedFunctionCall extends TSupportedMathFunctionCall { + string toString() { + exists(FunctionCall fc | + this = TMonotonicIncrease(fc, _, _) and + result = "Monotonic increase " + fc.getTarget().getName() + or + this = TMonotonicDecrease(fc, _, _) and + result = "Monotonic decrease " + fc.getTarget().getName() + or + this = TNonMonotonicLowerBound(fc, _) and + result = "Nonmonotonic lower bound " + fc.getTarget().getName() + or + this = TNonMonotonicUpperBound(fc, _) and + result = "Nonmonotonic upper bound " + fc.getTarget().getName() + ) + } + + /** Get the function call node this algebraic type corresponds to. */ + FunctionCall getFunctionCall() { + this = TMonotonicIncrease(result, _, _) + or + this = TMonotonicDecrease(result, _, _) + or + this = TNonMonotonicLowerBound(result, _) + or + this = TNonMonotonicUpperBound(result, _) + } + + /** Get the function name (`sin`, `pow`, etc.) without the `l` or `f` suffix. */ + bindingset[this, result] + string getBaseFunctionName() { getMathVariants(result) = getFunctionCall().getTarget() } + + /** + * Compute a result bound based on an input value and an extra constant value. + * + * The functions `getUpperBound()` and `getLowerBound()` automatically handle the differences + * between monotonically increasing and decreasing functions, and provide the input value. The + * `extra` float exists to support `pow(x, c)` for the constant `c`, otherwise it is `0.0`. + */ + bindingset[value, extra, this] + float compute(float value, float extra) { + exists(string name | name = getBaseFunctionName() | + name = "log" and + result = value.log() + or + name = "log2" and + result = value.log2() + or + name = "log10" and + result = value.log10() + or + name = "exp" and + result = value.exp() + or + name = "asin" and + result = value.asin() + or + name = "atan" and + result = value.atan() + or + name = "acos" and + result = value.acos() + or + name = "sinh" and + result = value.sinh() + or + name = "sqrt" and + result = value.sqrt() + or + name = "pow" and + result = extra.pow(value) + ) + } + + /** + * Get the lower bound of this function, based on its fixed range (if it has one) or based on + * the lower or upper bound of its input, if it is a monotonically increasing or decreasing + * function. + */ + float getLowerBound() { + this = TNonMonotonicLowerBound(_, result) + or + exists(Expr expr, float bound, float extra | + ( + this = TMonotonicIncrease(_, expr, extra) and + bound = getFullyConvertedLowerBounds(expr) + or + this = TMonotonicDecrease(_, expr, extra) and + bound = getFullyConvertedUpperBounds(expr) + ) and + result = compute(bound, extra) + ) + } + + /** + * Get the lower bound of this function, based on its fixed range (if it has one) or based on + * the lower or upper bound of its input, if it is a monotonically increasing or decreasing + * function. + */ + float getUpperBound() { + this = TNonMonotonicUpperBound(_, result) + or + exists(Expr expr, float bound, float extra | + ( + this = TMonotonicIncrease(_, expr, extra) and + bound = getFullyConvertedUpperBounds(expr) + or + this = TMonotonicDecrease(_, expr, extra) and + bound = getFullyConvertedLowerBounds(expr) + ) and + result = compute(bound, extra) + ) + } + } + + predicate supportedMathFunction(FunctionCall fc) { + exists(SupportedFunctionCall sfc | sfc.getFunctionCall() = fc) + } + /** * Holds if `expr` is checked with a guard to not be zero. * @@ -371,6 +565,8 @@ module RestrictedRangeAnalysis { // dividesNonzeroByZero(e) e instanceof DivExpr // TODO: confirm this is OK or + supportedMathFunction(e) + or e instanceof MinExpr or e instanceof MaxExpr @@ -628,8 +824,9 @@ module RestrictedRangeAnalysis { */ int estimatedPhiCombinationsExpr(Expr expr) { if isRecursiveExpr(expr) - // Assume 10 values were computed to analyze recursive expressions. - then result = 10 + then + // Assume 10 values were computed to analyze recursive expressions. + result = 10 else ( exists(RangeSsaDefinition def, StackVariable v | expr = def.getAUse(v) | def.isPhiNode(v) and @@ -649,16 +846,17 @@ module RestrictedRangeAnalysis { ) or not expr instanceof BinaryOperation and - not exprDependsOnDef(expr, _, _) and result = 1 + not exprDependsOnDef(expr, _, _) and + result = 1 ) } /** * Recursively scan this def to see how many phi nodes it depends on. - * + * * If this def is a phi node, it sums its downstream cost and adds one to account for itself, - * which is not exactly correct. - * + * which is not exactly correct. + * * This def may also be a crement expression (not currently supported), or an assign expr * (currently not supported), or an unanalyzable expression which is the root of the recursion * and given a value of 1. @@ -666,8 +864,9 @@ module RestrictedRangeAnalysis { language[monotonicAggregates] int estimatedPhiCombinationsDef(RangeSsaDefinition def, StackVariable v) { if isRecursiveDef(def, v) - // Assume 10 values were computed to analyze recursive expressions. - then result = 10 + then + // Assume 10 values were computed to analyze recursive expressions. + result = 10 else ( if def.isPhiNode(v) then @@ -681,7 +880,9 @@ module RestrictedRangeAnalysis { ) ) else ( - exists(Expr expr | assignmentDef(def, v, expr) | result = estimatedPhiCombinationsExpr(expr)) + exists(Expr expr | assignmentDef(def, v, expr) | + result = estimatedPhiCombinationsExpr(expr) + ) or v = def.getAVariable() and not assignmentDef(def, v, _) and @@ -730,6 +931,17 @@ module RestrictedRangeAnalysis { phiDependsOnDef(def, v, _, _) } + predicate canBoundExpr(Expr e) { + exists(RangeSsaDefinition def, StackVariable v | e = def.getAUse(v) | + analyzableDef(def, v) + ) or + analyzableExpr(e) + or + exists(getGuardedUpperBound(e)) + or + lowerBoundFromGuard(e, _, _, _) + } + /** * Computes a normal form of `x` where -0.0 has changed to +0.0. This can be * needed on the lesser side of a floating-point comparison or on both sides of @@ -931,6 +1143,10 @@ module RestrictedRangeAnalysis { result = getFullyConvertedLowerBounds(div.getLeftOperand()) / 0 ) or + exists(SupportedFunctionCall sfc | sfc.getFunctionCall() = expr | + result = sfc.getLowerBound() + ) + or exists(MinExpr minExpr | expr = minExpr and // Return the union of the lower bounds from both children. @@ -1136,6 +1352,10 @@ module RestrictedRangeAnalysis { result = getFullyConvertedUpperBounds(div.getLeftOperand()) / 0 ) or + exists(SupportedFunctionCall sfc | sfc.getFunctionCall() = expr | + result = sfc.getUpperBound() + ) + or exists(MaxExpr maxExpr | expr = maxExpr and // Return the union of the upper bounds from both children. From 99e92cff45d595f15a033dd7e3559109050e436c Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Fri, 7 Feb 2025 04:31:30 -0800 Subject: [PATCH 5/9] formatting fixes --- .../PossibleMisuseOfUndetectedInfinity.ql | 14 +++-- .../DIR-4-15/PossibleMisuseOfUndetectedNaN.ql | 55 +++++++++---------- 2 files changed, 34 insertions(+), 35 deletions(-) diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql index 357a8fce71..61753c98a9 100644 --- a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql +++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql @@ -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 \ No newline at end of file +select elem, source, sink, usage.getDescription(), extra, extraString diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql index f850cc3e55..701834ca3f 100644 --- a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql +++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql @@ -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 ( @@ -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 } } @@ -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 } @@ -244,17 +240,18 @@ where elem = MacroUnwrapper::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 \ No newline at end of file +select elem, source, sink, usage.getDescription(), extra, extraString From c473ea0a98848fad8d40e2b292322decfdd4f755 Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Fri, 7 Feb 2025 04:33:16 -0800 Subject: [PATCH 6/9] C formatting fix --- c/misra/test/rules/DIR-4-15/test.c | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/c/misra/test/rules/DIR-4-15/test.c b/c/misra/test/rules/DIR-4-15/test.c index e615d3447a..a827a7df97 100644 --- a/c/misra/test/rules/DIR-4-15/test.c +++ b/c/misra/test/rules/DIR-4-15/test.c @@ -162,8 +162,8 @@ void f1(float p1) { (int)pow(2, sin(p1)); // COMPLIANT: not likely to be Infinity (int)(1 / sin(p1)); // NON_COMPLIANT: possible infinity from zero in denominator - (int)(1 / log(p1)); // COMPLIANT: not possibly zero in denominator - (int)pow(p1, p1); // NON_COMPLIANT: NaN if p1 is zero + (int)(1 / log(p1)); // COMPLIANT: not possibly zero in denominator + (int)pow(p1, p1); // NON_COMPLIANT: NaN if p1 is zero if (p1 != 0) { (int)pow(p1, p1); // COMPLIANT: p1 is not zero } @@ -193,10 +193,10 @@ void f2() { castToInt(1.0 / 0.0); // NON_COMPLIANT: Infinity flows to denominator in division castToInt(0.0 / 0.0); // NON_COMPLIANT: NaN flows to denominator in division - checkBeforeCastToInt(1.0 / 0.0); // COMPLIANT - checkBeforeCastToInt(0.0 / 0.0); // COMPLIANT - addOneThenCastToInt(1.0 / 0.0); // NON_COMPLIANT[False negative] - addOneThenCastToInt(0.0 / 0.0); // NON_COMPLIANT + checkBeforeCastToInt(1.0 / 0.0); // COMPLIANT + checkBeforeCastToInt(0.0 / 0.0); // COMPLIANT + addOneThenCastToInt(1.0 / 0.0); // NON_COMPLIANT[False negative] + addOneThenCastToInt(0.0 / 0.0); // NON_COMPLIANT castToIntToFloatToInt(1.0 / 0.0); // NON_COMPLIANT castToIntToFloatToInt(0.0 / 0.0); // NON_COMPLIANT From c0e2020d70840f1f558ec567ef056cedb7687f7d Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Fri, 7 Feb 2025 04:34:58 -0800 Subject: [PATCH 7/9] Format range analysis qll --- .../src/codingstandards/cpp/RestrictedRangeAnalysis.qll | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll b/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll index 0c98824dbf..b81f113281 100644 --- a/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll +++ b/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll @@ -932,9 +932,8 @@ module RestrictedRangeAnalysis { } predicate canBoundExpr(Expr e) { - exists(RangeSsaDefinition def, StackVariable v | e = def.getAUse(v) | - analyzableDef(def, v) - ) or + exists(RangeSsaDefinition def, StackVariable v | e = def.getAUse(v) | analyzableDef(def, v)) + or analyzableExpr(e) or exists(getGuardedUpperBound(e)) From 09891b09d71ff26c6ac2a7e65bdc3442c6ec1f6a Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Fri, 7 Feb 2025 04:37:25 -0800 Subject: [PATCH 8/9] Remove changes to SimpleRangeAnalysisCustomizations.qll --- .../cpp/SimpleRangeAnalysisCustomizations.qll | 39 ------------------- 1 file changed, 39 deletions(-) diff --git a/cpp/common/src/codingstandards/cpp/SimpleRangeAnalysisCustomizations.qll b/cpp/common/src/codingstandards/cpp/SimpleRangeAnalysisCustomizations.qll index 2688452d28..5144f63dc2 100644 --- a/cpp/common/src/codingstandards/cpp/SimpleRangeAnalysisCustomizations.qll +++ b/cpp/common/src/codingstandards/cpp/SimpleRangeAnalysisCustomizations.qll @@ -14,45 +14,6 @@ import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils import experimental.semmle.code.cpp.rangeanalysis.extensions.ConstantBitwiseAndExprRange private import experimental.semmle.code.cpp.models.interfaces.SimpleRangeAnalysisExpr -// Disabled, causing performance issues in grpc: -/* -private class DivByConstantExpr extends SimpleRangeAnalysisExpr, DivExpr { - float quotient; - - DivByConstantExpr() { - quotient = evaluateConstantExpr(getRightOperand()) - } - - override predicate dependsOnChild(Expr e) { - e = getLeftOperand() - } - - override float getLowerBounds() { - exists(float numerator | - result = numerator / quotient and - if (quotient > 0) then - // x / y where and y is positive scales the UB/LB. - numerator = getFullyConvertedLowerBounds(getLeftOperand()) - else - // x / -y where and -y is negative will invert and scale the UB/LB. - numerator = getFullyConvertedUpperBounds(getLeftOperand()) - ) - } - - override float getUpperBounds() { - exists(float numerator | - result = numerator / quotient and - if (quotient > 0) then - // x / y where and y is positive scales the UB/LB. - numerator = getFullyConvertedUpperBounds(getLeftOperand()) - else - // x / -y where and -y is negative will invert and scale the UB/LB. - numerator = getFullyConvertedLowerBounds(getLeftOperand()) - ) - } -} - */ - /** * A range analysis extension that support bitwise `|` and `|=` where at least one operand is a * non-negative constant. From 2a0d6cb36c45deef89434d05eb942aabb21e62a4 Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Fri, 7 Feb 2025 04:41:16 -0800 Subject: [PATCH 9/9] Set more accurate query metadata --- .../rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql | 4 ++-- .../src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql | 4 ++-- rule_packages/c/FloatingTypes2.json | 8 ++++---- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql index 61753c98a9..3d54b4f829 100644 --- a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql +++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql @@ -4,8 +4,8 @@ * @description Evaluation of floating-point expressions shall not lead to the undetected generation * of infinities. * @kind path-problem - * @precision high - * @problem.severity error + * @precision medium + * @problem.severity warning * @tags external/misra/id/dir-4-15 * correctness * external/misra/c/2012/amendment3 diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql index 701834ca3f..2835a454d9 100644 --- a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql +++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql @@ -4,8 +4,8 @@ * @description Evaluation of floating-point expressions shall not lead to the undetected generation * of NaNs. * @kind path-problem - * @precision high - * @problem.severity error + * @precision low + * @problem.severity warning * @tags external/misra/id/dir-4-15 * correctness * external/misra/c/2012/amendment3 diff --git a/rule_packages/c/FloatingTypes2.json b/rule_packages/c/FloatingTypes2.json index 152ead08d3..3f4771dcc6 100644 --- a/rule_packages/c/FloatingTypes2.json +++ b/rule_packages/c/FloatingTypes2.json @@ -9,8 +9,8 @@ "description": "Evaluation of floating-point expressions shall not lead to the undetected generation of infinities.", "kind": "path-problem", "name": "Evaluation of floating-point expressions shall not lead to the undetected generation of infinities", - "precision": "high", - "severity": "error", + "precision": "medium", + "severity": "warning", "short_name": "PossibleMisuseOfUndetectedInfinity", "tags": [ "correctness", @@ -21,8 +21,8 @@ "description": "Evaluation of floating-point expressions shall not lead to the undetected generation of NaNs.", "kind": "path-problem", "name": "Evaluation of floating-point expressions shall not lead to the undetected generation of NaNs", - "precision": "high", - "severity": "error", + "precision": "low", + "severity": "warning", "short_name": "PossibleMisuseOfUndetectedNaN", "tags": [ "correctness",