C++: Support dereferenced variables in simple range analysis

- Support inference of guards on reference variables
 - Support type bounds for reference variables
 - Support reference variables when widening
 - Support reference variables when determining arithmetic assignment
This commit is contained in:
lcartey@github.com
2020-08-25 11:25:53 +01:00
committed by Jonas Jensen
parent 027f22d8e7
commit a4cb774932
2 changed files with 23 additions and 9 deletions

View File

@@ -191,6 +191,8 @@ private predicate linearAccessImpl(Expr expr, VariableAccess v, float p, float q
// Base case
expr = v and p = 1.0 and q = 0.0
or
expr.(ReferenceDereferenceExpr).getExpr() = v and p = 1.0 and q = 0.0
or
// a+(p*v+b) == p*v + (a+b)
exists(AddExpr addExpr, float a, float b |
addExpr.getLeftOperand().isConstant() and
@@ -349,13 +351,25 @@ private predicate typeBounds(ArithmeticType t, float lb, float ub) {
t instanceof FloatingPointType and lb = -(1.0 / 0.0) and ub = 1.0 / 0.0
}
private Type stripReference(Type t) {
if t instanceof ReferenceType then
result = t.(ReferenceType).getBaseType()
else
result = t
}
/** Gets the type used by range analysis for the given `StackVariable`. */
Type getVariableRangeType(StackVariable v) {
result = stripReference(v.getUnspecifiedType())
}
/**
* Gets the lower bound for the unspecified type `t`.
*
* For example, if `t` is a signed 32-bit type then the result is
* `-2^31`.
*/
float typeLowerBound(ArithmeticType t) { typeBounds(t, result, _) }
float typeLowerBound(Type t) { typeBounds(stripReference(t), result, _) }
/**
* Gets the upper bound for the unspecified type `t`.
@@ -363,7 +377,7 @@ float typeLowerBound(ArithmeticType t) { typeBounds(t, result, _) }
* For example, if `t` is a signed 32-bit type then the result is
* `2^31 - 1`.
*/
float typeUpperBound(ArithmeticType t) { typeBounds(t, _, result) }
float typeUpperBound(Type t) { typeBounds(stripReference(t), _, result) }
/**
* Gets the minimum value that this expression could represent, based on

View File

@@ -485,7 +485,7 @@ private predicate isRecursiveDef(RangeSsaDefinition def, StackVariable v) {
* This predicate finds all the definitions in the first set.
*/
private predicate assignmentDef(RangeSsaDefinition def, StackVariable v, Expr expr) {
v.getUnspecifiedType() instanceof ArithmeticType and
getVariableRangeType(v) instanceof ArithmeticType and
(
def = v.getInitializer().getExpr() and def = expr
or
@@ -1329,7 +1329,7 @@ private float getDefLowerBounds(RangeSsaDefinition def, StackVariable v) {
// recursion from exploding.
result =
max(float widenLB |
widenLB = wideningLowerBounds(v.getUnspecifiedType()) and
widenLB = wideningLowerBounds(getVariableRangeType(v)) and
not widenLB > truncatedLB
|
widenLB
@@ -1359,7 +1359,7 @@ private float getDefUpperBounds(RangeSsaDefinition def, StackVariable v) {
// from exploding.
result =
min(float widenUB |
widenUB = wideningUpperBounds(v.getUnspecifiedType()) and
widenUB = wideningUpperBounds(getVariableRangeType(v)) and
not widenUB < truncatedUB
|
widenUB
@@ -1391,9 +1391,9 @@ private predicate unanalyzableDefBounds(RangeSsaDefinition def, StackVariable v,
*/
bindingset[guard, v, branch]
predicate nonNanGuardedVariable(ComparisonOperation guard, VariableAccess v, boolean branch) {
v.getUnspecifiedType() instanceof IntegralType
getVariableRangeType(v.getTarget()) instanceof IntegralType
or
v.getUnspecifiedType() instanceof FloatingPointType and v instanceof NonNanVariableAccess
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... }`
@@ -1418,7 +1418,7 @@ private predicate lowerBoundFromGuard(
then
if
strictness = Nonstrict() or
not v.getUnspecifiedType() instanceof IntegralType
not getVariableRangeType(v.getTarget()) instanceof IntegralType
then lb = childLB
else lb = childLB + 1
else lb = varMinVal(v.getTarget())
@@ -1440,7 +1440,7 @@ private predicate upperBoundFromGuard(
then
if
strictness = Nonstrict() or
not v.getUnspecifiedType() instanceof IntegralType
not getVariableRangeType(v.getTarget()) instanceof IntegralType
then ub = childUB
else ub = childUB - 1
else ub = varMaxVal(v.getTarget())