Merge pull request #4074 from jbj/SimpleRangeAnalysis-extensible

C++: extensible range analysis
This commit is contained in:
Geoffrey White
2020-08-17 14:46:57 +01:00
committed by GitHub
5 changed files with 177 additions and 16 deletions

View File

@@ -0,0 +1,78 @@
/**
* EXPERIMENTAL: The API of this module may change without notice.
*
* Provides a class for modeling `Expr`s with a restricted range.
*/
import cpp
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
/**
* EXPERIMENTAL: The API of this class may change without notice.
*
* An expression for which a range can be deduced. Extend this class to add
* functionality to the range analysis library.
*/
abstract class SimpleRangeAnalysisExpr extends Expr {
/**
* Gets the lower bound of the expression.
*
* Implementations of this predicate should use
* `getFullyConvertedLowerBounds` and `getFullyConvertedUpperBounds` for
* recursive calls to get the bounds of their children.
*/
abstract float getLowerBounds();
/**
* Gets the upper bound of the expression.
*
* Implementations of this predicate should use
* `getFullyConvertedLowerBounds` and `getFullyConvertedUpperBounds` for
* recursive calls to get the bounds of their children.
*/
abstract float getUpperBounds();
/**
* Holds if the range this expression depends on the definition `srcDef` for
* StackVariable `srcVar`.
*
* Because this predicate cannot be recursive, most implementations should
* override `dependsOnChild` instead.
*/
predicate dependsOnDef(RangeSsaDefinition srcDef, StackVariable srcVar) { none() }
/**
* Holds if this expression depends on the range of its unconverted
* subexpression `child`. This information is used to inform the range
* analysis about cyclic dependencies. Without this information, range
* analysis might work for simple cases but will go into infinite loops on
* complex code.
*
* For example, when modeling a function call whose return value depends on
* all of its arguments, implement this predicate as
* `child = this.getAnArgument()`.
*/
abstract predicate dependsOnChild(Expr child);
}
import SimpleRangeAnalysisInternal
/**
* This class exists to prevent the QL front end from emitting compile errors
* inside `SimpleRangeAnalysis.qll` about certain conjuncts being empty
* because the overrides of `SimpleRangeAnalysisExpr` that happen to be in
* scope do not make use of every feature it offers.
*/
private class Empty extends SimpleRangeAnalysisExpr {
Empty() {
// This predicate is complicated enough that the QL type checker doesn't
// see it as empty but simple enough that the optimizer should.
this = this and none()
}
override float getLowerBounds() { none() }
override float getUpperBounds() { none() }
override predicate dependsOnChild(Expr child) { none() }
}

View File

@@ -44,6 +44,7 @@
import cpp
private import RangeAnalysisUtils
private import experimental.semmle.code.cpp.models.interfaces.SimpleRangeAnalysisExpr
import RangeSSA
import SimpleRangeAnalysisCached
private import NanAnalysis
@@ -213,6 +214,9 @@ private predicate analyzableExpr(Expr e) {
or
// `>>` by a constant
exists(e.(RShiftExpr).getRightOperand().getValue())
or
// A modeled expression for range analysis
e instanceof SimpleRangeAnalysisExpr
)
}
@@ -328,6 +332,16 @@ private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, StackVaria
)
or
e = srcDef.getAUse(srcVar)
or
// A modeled expression for range analysis
exists(SimpleRangeAnalysisExpr rae | rae = e |
rae.dependsOnDef(srcDef, srcVar)
or
exists(Expr child |
rae.dependsOnChild(child) and
exprDependsOnDef(child, srcDef, srcVar)
)
)
}
/**
@@ -445,13 +459,6 @@ private float addRoundingDownSmall(float x, float small) {
if (x + small) - x > small then result = (x + small).nextDown() else result = (x + small)
}
/**
* Gets the truncated lower bounds of the fully converted expression.
*/
private float getFullyConvertedLowerBounds(Expr expr) {
result = getTruncatedLowerBounds(expr.getFullyConverted())
}
/**
* Gets the lower bounds of the expression.
*
@@ -498,13 +505,6 @@ private float getTruncatedLowerBounds(Expr expr) {
result = exprMinVal(expr)
}
/**
* Gets the truncated upper bounds of the fully converted expression.
*/
private float getFullyConvertedUpperBounds(Expr expr) {
result = getTruncatedUpperBounds(expr.getFullyConverted())
}
/**
* Gets the upper bounds of the expression.
*
@@ -728,7 +728,9 @@ private float getLowerBoundsImpl(Expr expr) {
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)
result = getDefLowerBounds(def, v) and
// Not explicitly modeled by a SimpleRangeAnalysisExpr
not expr instanceof SimpleRangeAnalysisExpr
)
or
// unsigned `&` (tighter bounds may exist)
@@ -744,6 +746,12 @@ private float getLowerBoundsImpl(Expr expr) {
right = rsExpr.getRightOperand().getFullyConverted().getValue().toInt() and
result = safeFloor(left / 2.pow(right))
)
or
// A modeled expression for range analysis
exists(SimpleRangeAnalysisExpr rangeAnalysisExpr |
rangeAnalysisExpr = expr and
result = rangeAnalysisExpr.getLowerBounds()
)
}
/** Only to be called by `getTruncatedUpperBounds`. */
@@ -902,7 +910,9 @@ private float getUpperBoundsImpl(Expr expr) {
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)
result = getDefUpperBounds(def, v) and
// Not explicitly modeled by a SimpleRangeAnalysisExpr
not expr instanceof SimpleRangeAnalysisExpr
)
or
// unsigned `&` (tighter bounds may exist)
@@ -920,6 +930,12 @@ private float getUpperBoundsImpl(Expr expr) {
right = rsExpr.getRightOperand().getFullyConverted().getValue().toInt() and
result = safeFloor(left / 2.pow(right))
)
or
// A modeled expression for range analysis
exists(SimpleRangeAnalysisExpr rangeAnalysisExpr |
rangeAnalysisExpr = expr and
result = rangeAnalysisExpr.getUpperBounds()
)
}
/**
@@ -1504,3 +1520,25 @@ private module SimpleRangeAnalysisCached {
convertedExprMightOverflowPositively(expr)
}
}
/**
* INTERNAL: do not use. This module contains utilities for use in the
* experimental `SimpleRangeAnalysisExpr` module.
*/
module SimpleRangeAnalysisInternal {
/**
* 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())
}
}
private import SimpleRangeAnalysisInternal

View File

@@ -0,0 +1,9 @@
/// Adds its arguments (has custom modeling in QL)
int custom_add_function(int a, int b);
int test_extensibility_add(int x) {
if (x >= -10 && x <= 10) {
int result = custom_add_function(x, 100);
return result; // 90 .. 110
}
}

View File

@@ -0,0 +1,4 @@
| extensibility.c:5:7:5:7 | x | -2.147483648E9 | 2.147483647E9 |
| extensibility.c:5:19:5:19 | x | -10.0 | 2.147483647E9 |
| extensibility.c:6:38:6:38 | x | -10.0 | 10.0 |
| extensibility.c:7:12:7:17 | result | 90.0 | 110.0 |

View File

@@ -0,0 +1,32 @@
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
import experimental.semmle.code.cpp.models.interfaces.SimpleRangeAnalysisExpr
class CustomAddFunctionCall extends SimpleRangeAnalysisExpr, FunctionCall {
CustomAddFunctionCall() { this.getTarget().hasGlobalName("custom_add_function") }
override float getLowerBounds() {
exists(float lower0, float lower1 |
lower0 = getFullyConvertedLowerBounds(this.getArgument(0)) and
lower1 = getFullyConvertedLowerBounds(this.getArgument(1)) and
// Note: this rounds toward 0, not -Inf as it should
result = lower0 + lower1
)
}
override float getUpperBounds() {
exists(float upper0, float upper1 |
upper0 = getFullyConvertedUpperBounds(this.getArgument(0)) and
upper1 = getFullyConvertedUpperBounds(this.getArgument(1)) and
// Note: this rounds toward 0, not Inf as it should
result = upper0 + upper1
)
}
override predicate dependsOnChild(Expr child) { child = this.getAnArgument() }
}
from VariableAccess expr, float lower, float upper
where
lower = lowerBound(expr) and
upper = upperBound(expr)
select expr, lower, upper