C++: Use StackVariable in code that uses RangeSSA

This commit is contained in:
Jonas Jensen
2019-11-19 08:48:20 +01:00
parent 29f66ff095
commit 6f9ec0409e
3 changed files with 25 additions and 31 deletions

View File

@@ -37,7 +37,7 @@ predicate flowsToExprImpl(Expr source, Expr sink, boolean pathMightOverflow) {
pathMightOverflow = false and
source.(FunctionCall).getTarget().(Snprintf).returnsFullFormatLength()
or
exists(RangeSsaDefinition def, LocalScopeVariable v |
exists(RangeSsaDefinition def, StackVariable v |
flowsToDef(source, def, v, pathMightOverflow) and
sink = def.getAUse(v)
)
@@ -63,9 +63,7 @@ predicate flowsToExprImpl(Expr source, Expr sink, boolean pathMightOverflow) {
* `pathMightOverflow` is true if there is an arithmetic operation
* on the path that might overflow.
*/
predicate flowsToDef(
Expr source, RangeSsaDefinition def, LocalScopeVariable v, boolean pathMightOverflow
) {
predicate flowsToDef(Expr source, RangeSsaDefinition def, StackVariable v, boolean pathMightOverflow) {
// Might the current definition overflow?
exists(boolean otherMightOverflow | flowsToDefImpl(source, def, v, otherMightOverflow) |
if defMightOverflow(def, v)
@@ -86,7 +84,7 @@ predicate flowsToDef(
* the path. But it is a good way to reduce the number of false positives.
*/
predicate flowsToDefImpl(
Expr source, RangeSsaDefinition def, LocalScopeVariable v, boolean pathMightOverflow
Expr source, RangeSsaDefinition def, StackVariable v, boolean pathMightOverflow
) {
// Assignment or initialization: `e = v;`
exists(Expr e |

View File

@@ -24,7 +24,7 @@ predicate nanExcludingComparison(ComparisonOperation guard, boolean polarity) {
* by virtue of the guard in `def`.
*/
private predicate excludesNan(RangeSsaDefinition def, VariableAccess v) {
exists(VariableAccess inCond, ComparisonOperation guard, boolean branch, LocalScopeVariable lsv |
exists(VariableAccess inCond, ComparisonOperation guard, boolean branch, StackVariable lsv |
def.isGuardPhi(inCond, guard, branch) and
inCond.getTarget() = lsv and
v = def.getAUse(lsv) and

View File

@@ -120,7 +120,7 @@ private predicate analyzableExpr(Expr e) {
exists(exprMinVal(e.(Conversion).getExpr())) or
// Also allow variable accesses, provided that they have SSA
// information.
exists(RangeSsaDefinition def, LocalScopeVariable v | e = def.getAUse(v))
exists(RangeSsaDefinition def, StackVariable v | e = def.getAUse(v))
)
}
@@ -136,7 +136,7 @@ private predicate analyzableExpr(Expr e) {
* here.
*/
private predicate defDependsOnDef(
RangeSsaDefinition def, LocalScopeVariable v, RangeSsaDefinition srcDef, LocalScopeVariable srcVar
RangeSsaDefinition def, StackVariable v, RangeSsaDefinition srcDef, StackVariable srcVar
) {
// Definitions with a defining value.
exists(Expr expr | assignmentDef(def, v, expr) | exprDependsOnDef(expr, srcDef, srcVar))
@@ -171,7 +171,7 @@ private predicate defDependsOnDef(
* Helper predicate for `defDependsOnDef`. This predicate matches
* the structure of `getLowerBoundsImpl` and `getUpperBoundsImpl`.
*/
private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, LocalScopeVariable srcVar) {
private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, StackVariable srcVar) {
exists(UnaryMinusExpr negateExpr | e = negateExpr |
exprDependsOnDef(negateExpr.getOperand(), srcDef, srcVar)
)
@@ -226,7 +226,7 @@ private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, LocalScope
* the structure of `getPhiLowerBounds` and `getPhiUpperBounds`.
*/
private predicate phiDependsOnDef(
RangeSsaDefinition phi, LocalScopeVariable v, RangeSsaDefinition srcDef, LocalScopeVariable srcVar
RangeSsaDefinition phi, StackVariable v, RangeSsaDefinition srcDef, StackVariable srcVar
) {
exists(VariableAccess access, ComparisonOperation guard |
access = v.getAnAccess() and
@@ -241,19 +241,17 @@ private predicate phiDependsOnDef(
/** The transitive closure of `defDependsOnDef`. */
private predicate defDependsOnDefTransitively(
RangeSsaDefinition def, LocalScopeVariable v, RangeSsaDefinition srcDef, LocalScopeVariable srcVar
RangeSsaDefinition def, StackVariable v, RangeSsaDefinition srcDef, StackVariable srcVar
) {
defDependsOnDef(def, v, srcDef, srcVar)
or
exists(RangeSsaDefinition midDef, LocalScopeVariable midVar |
defDependsOnDef(def, v, midDef, midVar)
|
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, LocalScopeVariable v) {
private predicate isRecursiveDef(RangeSsaDefinition def, StackVariable v) {
defDependsOnDefTransitively(def, v, def, v)
}
@@ -271,7 +269,7 @@ private predicate isRecursiveDef(RangeSsaDefinition def, LocalScopeVariable v) {
*
* This predicate finds all the definitions in the first set.
*/
private predicate assignmentDef(RangeSsaDefinition def, LocalScopeVariable v, Expr expr) {
private predicate assignmentDef(RangeSsaDefinition def, StackVariable v, Expr expr) {
v.getUnspecifiedType() instanceof ArithmeticType and
(
def = v.getInitializer().getExpr() and def = expr
@@ -285,7 +283,7 @@ private predicate assignmentDef(RangeSsaDefinition def, LocalScopeVariable v, Ex
}
/** See comment above sourceDef. */
private predicate analyzableDef(RangeSsaDefinition def, LocalScopeVariable v) {
private predicate analyzableDef(RangeSsaDefinition def, StackVariable v) {
assignmentDef(def, v, _) or defDependsOnDef(def, v, _, _)
}
@@ -613,7 +611,7 @@ private float getLowerBoundsImpl(Expr expr) {
)
or
// Use SSA to get the lower bounds for a variable use.
exists(RangeSsaDefinition def, LocalScopeVariable v | expr = def.getAUse(v) |
exists(RangeSsaDefinition def, StackVariable v | expr = def.getAUse(v) |
result = getDefLowerBounds(def, v)
)
}
@@ -766,7 +764,7 @@ private float getUpperBoundsImpl(Expr expr) {
)
or
// Use SSA to get the upper bounds for a variable use.
exists(RangeSsaDefinition def, LocalScopeVariable v | expr = def.getAUse(v) |
exists(RangeSsaDefinition def, StackVariable v | expr = def.getAUse(v) |
result = getDefUpperBounds(def, v)
)
}
@@ -860,7 +858,7 @@ private float boolConversionUpperBound(Expr expr) {
* 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(LocalScopeVariable v, RangeSsaDefinition phi) {
private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) {
exists(
VariableAccess access, ComparisonOperation guard, boolean branch, float defLB, float guardLB
|
@@ -877,7 +875,7 @@ private float getPhiLowerBounds(LocalScopeVariable v, RangeSsaDefinition phi) {
}
/** See comment for `getPhiLowerBounds`, above. */
private float getPhiUpperBounds(LocalScopeVariable v, RangeSsaDefinition phi) {
private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) {
exists(
VariableAccess access, ComparisonOperation guard, boolean branch, float defUB, float guardUB
|
@@ -894,7 +892,7 @@ private float getPhiUpperBounds(LocalScopeVariable v, RangeSsaDefinition phi) {
}
/** Only to be called by `getDefLowerBounds`. */
private float getDefLowerBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v) {
private float getDefLowerBoundsImpl(RangeSsaDefinition def, StackVariable v) {
// Definitions with a defining value.
exists(Expr expr | assignmentDef(def, v, expr) | result = getFullyConvertedLowerBounds(expr))
or
@@ -936,7 +934,7 @@ private float getDefLowerBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v
}
/** Only to be called by `getDefUpperBounds`. */
private float getDefUpperBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v) {
private float getDefUpperBoundsImpl(RangeSsaDefinition def, StackVariable v) {
// Definitions with a defining value.
exists(Expr expr | assignmentDef(def, v, expr) | result = getFullyConvertedUpperBounds(expr))
or
@@ -982,7 +980,7 @@ private float getDefUpperBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v
* done by `getDefLowerBoundsImpl`, but this is where widening is applied
* to prevent the analysis from exploding due to a recursive definition.
*/
private float getDefLowerBounds(RangeSsaDefinition def, LocalScopeVariable v) {
private float getDefLowerBounds(RangeSsaDefinition def, StackVariable v) {
exists(float newLB, float truncatedLB |
newLB = getDefLowerBoundsImpl(def, v) and
if varMinVal(v) <= newLB and newLB <= varMaxVal(v)
@@ -1011,7 +1009,7 @@ private float getDefLowerBounds(RangeSsaDefinition def, LocalScopeVariable v) {
}
/** See comment for `getDefLowerBounds`, above. */
private float getDefUpperBounds(RangeSsaDefinition def, LocalScopeVariable v) {
private float getDefUpperBounds(RangeSsaDefinition def, StackVariable v) {
exists(float newUB, float truncatedUB |
newUB = getDefUpperBoundsImpl(def, v) and
if varMinVal(v) <= newUB and newUB <= varMaxVal(v)
@@ -1044,9 +1042,7 @@ private float getDefUpperBounds(RangeSsaDefinition def, LocalScopeVariable v) {
* unanalyzable definitions (such as function parameters) and make their
* bounds unknown.
*/
private predicate unanalyzableDefBounds(
RangeSsaDefinition def, LocalScopeVariable v, float lb, float ub
) {
private predicate unanalyzableDefBounds(RangeSsaDefinition def, StackVariable v, float lb, float ub) {
v = def.getAVariable() and
not analyzableDef(def, v) and
lb = varMinVal(v) and
@@ -1268,13 +1264,13 @@ private module SimpleRangeAnalysisCached {
/** Holds if the definition might overflow negatively. */
cached
predicate defMightOverflowNegatively(RangeSsaDefinition def, LocalScopeVariable v) {
predicate defMightOverflowNegatively(RangeSsaDefinition def, StackVariable v) {
getDefLowerBoundsImpl(def, v) < varMinVal(v)
}
/** Holds if the definition might overflow positively. */
cached
predicate defMightOverflowPositively(RangeSsaDefinition def, LocalScopeVariable v) {
predicate defMightOverflowPositively(RangeSsaDefinition def, StackVariable v) {
getDefUpperBoundsImpl(def, v) > varMaxVal(v)
}
@@ -1283,7 +1279,7 @@ private module SimpleRangeAnalysisCached {
* negatively).
*/
cached
predicate defMightOverflow(RangeSsaDefinition def, LocalScopeVariable v) {
predicate defMightOverflow(RangeSsaDefinition def, StackVariable v) {
defMightOverflowNegatively(def, v) or
defMightOverflowPositively(def, v)
}