C++: Use StackVariable where SSA/def-use are used

These changes should not affect semantics since these uses of
`LocalScopeVariable` were already constrained to stack variables by
their use of SSA or def-use.
This commit is contained in:
Jonas Jensen
2019-11-19 10:26:27 +01:00
parent 6f9ec0409e
commit 140575ee71
14 changed files with 41 additions and 45 deletions

View File

@@ -22,7 +22,7 @@ predicate testAndBranch(Expr e, Stmt branch) {
)
}
predicate choice(LocalScopeVariable v, Stmt branch, string value) {
predicate choice(StackVariable v, Stmt branch, string value) {
exists(AnalysedExpr e |
testAndBranch(e, branch) and
(
@@ -33,7 +33,7 @@ predicate choice(LocalScopeVariable v, Stmt branch, string value) {
)
}
predicate guarded(LocalScopeVariable v, Stmt loopstart, AnalysedExpr child) {
predicate guarded(StackVariable v, Stmt loopstart, AnalysedExpr child) {
choice(v, loopstart, _) and
loopstart.getChildStmt*() = child.getEnclosingStmt() and
(definition(v, child) or exists(child.getNullSuccessor(v)))
@@ -47,9 +47,7 @@ predicate addressLeak(Variable v, Stmt leak) {
)
}
from
LocalScopeVariable v, Stmt branch, AnalysedExpr cond, string context, string test,
string testresult
from StackVariable v, Stmt branch, AnalysedExpr cond, string context, string test, string testresult
where
choice(v, branch, context) and
forall(ControlFlowNode def | definition(v, def) and definitionReaches(def, cond) |

View File

@@ -23,14 +23,14 @@ predicate closeCall(FunctionCall fc, Variable v) {
)
}
predicate openDefinition(LocalScopeVariable v, ControlFlowNode def) {
predicate openDefinition(StackVariable v, ControlFlowNode def) {
exists(Expr expr | exprDefinition(v, def, expr) and allocateDescriptorCall(expr))
}
predicate openReaches(ControlFlowNode def, ControlFlowNode node) {
exists(LocalScopeVariable v | openDefinition(v, def) and node = def.getASuccessor())
exists(StackVariable v | openDefinition(v, def) and node = def.getASuccessor())
or
exists(LocalScopeVariable v, ControlFlowNode mid |
exists(StackVariable v, ControlFlowNode mid |
openDefinition(v, def) and
openReaches(def, mid) and
not errorSuccessor(v, mid) and
@@ -40,7 +40,7 @@ predicate openReaches(ControlFlowNode def, ControlFlowNode node) {
)
}
predicate assignedToFieldOrGlobal(LocalScopeVariable v, Assignment assign) {
predicate assignedToFieldOrGlobal(StackVariable v, Assignment assign) {
exists(Variable external |
assign.getRValue() = v.getAnAccess() and
assign.getLValue().(VariableAccess).getTarget() = external and
@@ -48,7 +48,7 @@ predicate assignedToFieldOrGlobal(LocalScopeVariable v, Assignment assign) {
)
}
from LocalScopeVariable v, ControlFlowNode def, ReturnStmt ret
from StackVariable v, ControlFlowNode def, ReturnStmt ret
where
openDefinition(v, def) and
openReaches(def, ret) and

View File

@@ -11,7 +11,7 @@
import cpp
from LocalScopeVariable v, ControlFlowNode def, VariableAccess checked, VariableAccess unchecked
from StackVariable v, ControlFlowNode def, VariableAccess checked, VariableAccess unchecked
where
checked = v.getAnAccess() and
dereferenced(checked) and

View File

@@ -13,7 +13,7 @@
import cpp
predicate negativeCheck(LocalScopeVariable v, ComparisonOperation op) {
predicate negativeCheck(StackVariable v, ComparisonOperation op) {
exists(int varindex, string constant, Literal lit |
op.getChild(varindex) = v.getAnAccess() and
op.getChild(1 - varindex) = lit and
@@ -38,7 +38,7 @@ predicate negativeCheck(LocalScopeVariable v, ComparisonOperation op) {
)
}
from LocalScopeVariable v, ArrayExpr dangerous, Expr check
from StackVariable v, ArrayExpr dangerous, Expr check
where
useUsePair(v, dangerous.getArrayOffset(), check.getAChild()) and
negativeCheck(v, check) and

View File

@@ -43,7 +43,7 @@ class FunctionWithNegativeReturn extends Function {
predicate dangerousUse(IntegralReturnValue val, Expr use) {
exists(ArrayExpr ae | ae.getArrayOffset() = val and use = val)
or
exists(LocalScopeVariable v, ControlFlowNode def, ArrayExpr ae |
exists(StackVariable v, ControlFlowNode def, ArrayExpr ae |
exprDefinition(v, def, val) and
use = ae.getArrayOffset() and
not boundsChecked(v, use) and
@@ -54,7 +54,7 @@ predicate dangerousUse(IntegralReturnValue val, Expr use) {
val = use and
use.getType().getUnderlyingType() instanceof PointerType
or
exists(LocalScopeVariable v, ControlFlowNode def, AddExpr add |
exists(StackVariable v, ControlFlowNode def, AddExpr add |
exprDefinition(v, def, val) and
definitionUsePair(v, def, use) and
add.getAnOperand() = use and

View File

@@ -60,7 +60,7 @@ predicate allocExprOrIndirect(Expr alloc, string kind) {
pragma[nomagic]
private predicate allocReachesVariable(Variable v, Expr alloc, string kind) {
exists(Expr mid |
not v instanceof LocalScopeVariable and
not v instanceof StackVariable and
v.getAnAssignedValue() = mid and
allocReaches0(mid, alloc, kind)
)
@@ -76,7 +76,7 @@ private predicate allocReaches0(Expr e, Expr alloc, string kind) {
allocExprOrIndirect(alloc, kind) and
e = alloc
or
exists(SsaDefinition def, LocalScopeVariable v |
exists(SsaDefinition def, StackVariable v |
// alloc via SSA
allocReaches0(def.getAnUltimateDefiningValue(v), alloc, kind) and
e = def.getAUse(v)

View File

@@ -18,7 +18,7 @@ class MallocCall extends FunctionCall {
Expr getAllocatedSize() {
if this.getArgument(0) instanceof VariableAccess
then
exists(LocalScopeVariable v, ControlFlowNode def |
exists(StackVariable v, ControlFlowNode def |
definitionUsePair(v, def, this.getArgument(0)) and
exprDefinition(v, def, result)
)

View File

@@ -16,7 +16,7 @@ private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
import semmle.code.cpp.security.TaintTracking
predicate hasUpperBound(VariableAccess offsetExpr) {
exists(BasicBlock controlled, LocalScopeVariable offsetVar, SsaDefinition def |
exists(BasicBlock controlled, StackVariable offsetVar, SsaDefinition def |
controlled.contains(offsetExpr) and
linearBoundControls(controlled, def, offsetVar) and
offsetExpr = def.getAUse(offsetVar)
@@ -24,7 +24,7 @@ predicate hasUpperBound(VariableAccess offsetExpr) {
}
pragma[noinline]
predicate linearBoundControls(BasicBlock controlled, SsaDefinition def, LocalScopeVariable offsetVar) {
predicate linearBoundControls(BasicBlock controlled, SsaDefinition def, StackVariable offsetVar) {
exists(GuardCondition guard, boolean branch |
guard.controls(controlled, branch) and
cmpWithLinearBound(guard, def.getAUse(offsetVar), Lesser(), branch)

View File

@@ -24,7 +24,7 @@ class MallocCall extends FunctionCall {
Expr getAllocatedSize() {
if this.getArgument(0) instanceof VariableAccess
then
exists(LocalScopeVariable v, ControlFlowNode def |
exists(StackVariable v, ControlFlowNode def |
definitionUsePair(v, def, this.getArgument(0)) and
exprDefinition(v, def, result)
)

View File

@@ -82,7 +82,7 @@ FunctionCall stat(Expr path, Expr buf) {
predicate referenceTo(Expr source, Expr use) {
source = use
or
exists(SsaDefinition def, LocalScopeVariable v |
exists(SsaDefinition def, StackVariable v |
def.getAnUltimateDefiningValue(v) = source and def.getAUse(v) = use
)
}
@@ -109,9 +109,7 @@ where
)
) and
// checkUse and opUse refer to the same SSA variable
exists(SsaDefinition def, LocalScopeVariable v |
def.getAUse(v) = checkUse and def.getAUse(v) = opUse
) and
exists(SsaDefinition def, StackVariable v | def.getAUse(v) = checkUse and def.getAUse(v) = opUse) and
// opUse looks like an operation on a filename
fc = filenameOperation(opUse) and
// the return value of check is used (possibly with one step of

View File

@@ -100,9 +100,9 @@ Type baseType(Type t) {
*/
predicate exprSourceType(Expr use, Type sourceType, Location sourceLoc) {
// Reaching definitions.
if exists(SsaDefinition def, LocalScopeVariable v | use = def.getAUse(v))
if exists(SsaDefinition def, StackVariable v | use = def.getAUse(v))
then
exists(SsaDefinition def, LocalScopeVariable v | use = def.getAUse(v) |
exists(SsaDefinition def, StackVariable v | use = def.getAUse(v) |
defSourceType(def, v, sourceType, sourceLoc)
)
else
@@ -137,7 +137,7 @@ predicate exprSourceType(Expr use, Type sourceType, Location sourceLoc) {
* Holds if there is a pointer expression with type `sourceType` at
* location `sourceLoc` which might define the value of `v` at `def`.
*/
predicate defSourceType(SsaDefinition def, LocalScopeVariable v, Type sourceType, Location sourceLoc) {
predicate defSourceType(SsaDefinition def, StackVariable v, Type sourceType, Location sourceLoc) {
exprSourceType(def.getDefiningValue(v), sourceType, sourceLoc)
or
defSourceType(def.getAPhiInput(v), v, sourceType, sourceLoc)

View File

@@ -3,7 +3,7 @@ private import semmle.code.cpp.models.interfaces.ArrayFunction
private import semmle.code.cpp.models.implementations.Strcat
private predicate mayAddNullTerminatorHelper(Expr e, VariableAccess va, Expr e0) {
exists(LocalScopeVariable v0, Expr val |
exists(StackVariable v0, Expr val |
exprDefinition(v0, e, val) and
val.getAChild*() = va and
mayAddNullTerminator(e0, v0.getAnAccess())
@@ -41,7 +41,7 @@ predicate mayAddNullTerminator(Expr e, VariableAccess va) {
or
// Assignment to non-stack variable
exists(AssignExpr ae | e = ae |
not ae.getLValue().(VariableAccess).getTarget() instanceof LocalScopeVariable and
not ae.getLValue().(VariableAccess).getTarget() instanceof StackVariable and
ae.getRValue().getAChild*() = va
)
or

View File

@@ -371,7 +371,7 @@ private int int_value(Expr e) {
/** An `SsaDefinition` with an additional predicate `isLt`. */
class GuardedSsa extends SsaDefinition {
/** Holds if this `SsaDefinition` is guarded such that `this(var) < gt + k` is `testIsTrue` in `block`. */
predicate isLt(LocalScopeVariable var, Expr gt, int k, BasicBlock block, boolean testIsTrue) {
predicate isLt(StackVariable var, Expr gt, int k, BasicBlock block, boolean testIsTrue) {
exists(Expr luse, GuardCondition test | this.getAUse(var) = luse |
test.ensuresLt(luse, gt, k, block, testIsTrue)
)

View File

@@ -170,8 +170,8 @@ private newtype GVNBase =
GVN_FloatConst(float val, Type t) { mk_FloatConst(val, t, _) } or
// If the local variable does not have a defining value, then
// we use the SsaDefinition as its global value number.
GVN_UndefinedLocalScopeVariable(LocalScopeVariable x, SsaDefinition def) {
mk_UndefinedLocalScopeVariable(x, def, _)
GVN_UndefinedStackVariable(StackVariable x, SsaDefinition def) {
mk_UndefinedStackVariable(x, def, _)
} or
// Variables with no SSA information. As a crude (but safe)
// approximation, we use `mostRecentSideEffect` to compute a definition
@@ -235,8 +235,8 @@ class GVN extends GVNBase {
if this instanceof GVN_FloatConst
then result = "FloatConst"
else
if this instanceof GVN_UndefinedLocalScopeVariable
then result = "UndefinedLocalScopeVariable"
if this instanceof GVN_UndefinedStackVariable
then result = "UndefinedStackVariable"
else
if this instanceof GVN_OtherVariable
then result = "OtherVariable"
@@ -307,7 +307,7 @@ private predicate mk_FloatConst(float val, Type t, Expr e) {
t = e.getUnspecifiedType()
}
private predicate analyzableLocalScopeVariable(VariableAccess access) {
private predicate analyzableStackVariable(VariableAccess access) {
strictcount(SsaDefinition def | def.getAUse(_) = access | def) = 1 and
strictcount(SsaDefinition def, Variable v | def.getAUse(v) = access | v) = 1 and
count(SsaDefinition def, Variable v |
@@ -322,10 +322,10 @@ private predicate analyzableLocalScopeVariable(VariableAccess access) {
// defining value. If there is a defining value, then there is no
// need to generate a fresh `GVN` for the access because `globalValueNumber`
// will follow the chain and use the GVN of the defining value.
private predicate mk_UndefinedLocalScopeVariable(
LocalScopeVariable x, SsaDefinition def, VariableAccess access
private predicate mk_UndefinedStackVariable(
StackVariable x, SsaDefinition def, VariableAccess access
) {
analyzableLocalScopeVariable(access) and
analyzableStackVariable(access) and
access = def.getAUse(x) and
not exists(def.getDefiningValue(x))
}
@@ -515,16 +515,16 @@ GVN globalValueNumber(Expr e) {
)
or
// Local variable with a defining value.
exists(LocalScopeVariable x, SsaDefinition def |
analyzableLocalScopeVariable(e) and
exists(StackVariable x, SsaDefinition def |
analyzableStackVariable(e) and
e = def.getAUse(x) and
result = globalValueNumber(def.getDefiningValue(x).getFullyConverted())
)
or
// Local variable without a defining value.
exists(LocalScopeVariable x, SsaDefinition def |
mk_UndefinedLocalScopeVariable(x, def, e) and
result = GVN_UndefinedLocalScopeVariable(x, def)
exists(StackVariable x, SsaDefinition def |
mk_UndefinedStackVariable(x, def, e) and
result = GVN_UndefinedStackVariable(x, def)
)
or
// Variable with no SSA information.
@@ -594,7 +594,7 @@ private predicate analyzableConst(Expr e) {
*/
private predicate analyzableExpr(Expr e) {
analyzableConst(e) or
analyzableLocalScopeVariable(e) or
analyzableStackVariable(e) or
analyzableDotFieldAccess(e) or
analyzablePointerFieldAccess(e) or
analyzableImplicitThisFieldAccess(e) or