Java: Autoformat semmle.code.java.controlflow.

This commit is contained in:
Anders Schack-Mulligen 2018-10-11 15:09:28 +02:00
Родитель 291fb11c48
Коммит bf63139c16
7 изменённых файлов: 254 добавлений и 178 удалений

Просмотреть файл

@ -14,21 +14,21 @@ import semmle.code.java.ControlFlowGraph
*/
class BasicBlock extends ControlFlowNode {
BasicBlock() {
not exists(this.getAPredecessor()) and exists(this.getASuccessor()) or
strictcount(this.getAPredecessor()) > 1 or
exists(ControlFlowNode pred | pred = this.getAPredecessor() | strictcount(pred.getASuccessor()) > 1)
not exists(this.getAPredecessor()) and exists(this.getASuccessor())
or
strictcount(this.getAPredecessor()) > 1
or
exists(ControlFlowNode pred | pred = this.getAPredecessor() |
strictcount(pred.getASuccessor()) > 1
)
}
/** Gets an immediate successor of this basic block. */
cached
BasicBlock getABBSuccessor() {
result = getLastNode().getASuccessor()
}
BasicBlock getABBSuccessor() { result = getLastNode().getASuccessor() }
/** Gets an immediate predecessor of this basic block. */
BasicBlock getABBPredecessor() {
result.getABBSuccessor() = this
}
BasicBlock getABBPredecessor() { result.getABBSuccessor() = this }
/** Gets a control-flow node contained in this basic block. */
ControlFlowNode getANode() { result = getNode(_) }

Просмотреть файл

@ -1,10 +1,10 @@
/**
* Provides classes and predicates for control-flow graph dominance.
*/
import java
private import semmle.code.java.ControlFlowGraph
/*
* Predicates for basic-block-level dominance.
*/
@ -20,12 +20,12 @@ private predicate flowEntry(Stmt entry) {
}
/** The successor relation for basic blocks. */
private predicate bbSucc(BasicBlock pre, BasicBlock post) {
post = pre.getABBSuccessor()
}
private predicate bbSucc(BasicBlock pre, BasicBlock post) { post = pre.getABBSuccessor() }
/** The immediate dominance relation for basic blocks. */
cached predicate bbIDominates(BasicBlock dom, BasicBlock node) = idominance(flowEntry/1, bbSucc/2)(_, dom, node)
cached
predicate bbIDominates(BasicBlock dom, BasicBlock node) =
idominance(flowEntry/1, bbSucc/2)(_, dom, node)
/** Holds if the dominance relation is calculated for `bb`. */
predicate hasDominanceInformation(BasicBlock bb) {
@ -33,34 +33,34 @@ predicate hasDominanceInformation(BasicBlock bb) {
}
/** Exit points for control-flow. */
private predicate flowExit(Callable exit) {
exists(ControlFlowNode s | s.getASuccessor() = exit)
}
private predicate flowExit(Callable exit) { exists(ControlFlowNode s | s.getASuccessor() = exit) }
/** Exit points for basic-block control-flow. */
private predicate bbSink(BasicBlock exit) {
flowExit(exit.getLastNode())
}
private predicate bbSink(BasicBlock exit) { flowExit(exit.getLastNode()) }
/** Reversed `bbSucc`. */
private predicate bbPred(BasicBlock post, BasicBlock pre) {
post = pre.getABBSuccessor()
}
private predicate bbPred(BasicBlock post, BasicBlock pre) { post = pre.getABBSuccessor() }
/** The immediate post-dominance relation on basic blocks. */
cached predicate bbIPostDominates(BasicBlock dominator, BasicBlock node) = idominance(bbSink/1,bbPred/2)(_, dominator, node)
cached
predicate bbIPostDominates(BasicBlock dominator, BasicBlock node) =
idominance(bbSink/1, bbPred/2)(_, dominator, node)
/** Holds if `dom` strictly dominates `node`. */
predicate bbStrictlyDominates(BasicBlock dom, BasicBlock node) { bbIDominates+(dom, node) }
/** Holds if `dom` dominates `node`. (This is reflexive.) */
predicate bbDominates(BasicBlock dom, BasicBlock node) { bbStrictlyDominates(dom, node) or dom = node }
predicate bbDominates(BasicBlock dom, BasicBlock node) {
bbStrictlyDominates(dom, node) or dom = node
}
/** Holds if `dom` strictly post-dominates `node`. */
predicate bbStrictlyPostDominates(BasicBlock dom, BasicBlock node) { bbIPostDominates+(dom, node) }
/** Holds if `dom` post-dominates `node`. (This is reflexive.) */
predicate bbPostDominates(BasicBlock dom, BasicBlock node) { bbStrictlyPostDominates(dom, node) or dom = node }
predicate bbPostDominates(BasicBlock dom, BasicBlock node) {
bbStrictlyPostDominates(dom, node) or dom = node
}
/**
* The dominance frontier relation for basic blocks.
@ -86,7 +86,8 @@ predicate dominanceFrontier(BasicBlock x, BasicBlock w) {
/** Immediate dominance relation on control-flow graph nodes. */
predicate iDominates(ControlFlowNode dominator, ControlFlowNode node) {
exists(BasicBlock bb, int i | dominator = bb.getNode(i) and node = bb.getNode(i+1)) or
exists(BasicBlock bb, int i | dominator = bb.getNode(i) and node = bb.getNode(i + 1))
or
exists(BasicBlock dom, BasicBlock bb |
bbIDominates(dom, bb) and
dominator = dom.getLastNode() and
@ -100,9 +101,7 @@ predicate strictlyDominates(ControlFlowNode dom, ControlFlowNode node) {
// This predicate is gigantic, so it must be inlined.
bbStrictlyDominates(dom.getBasicBlock(), node.getBasicBlock())
or
exists(BasicBlock b, int i, int j |
dom = b.getNode(i) and node = b.getNode(j) and i < j
)
exists(BasicBlock b, int i, int j | dom = b.getNode(i) and node = b.getNode(j) and i < j)
}
/** Holds if `dom` dominates `node`. (This is reflexive.) */
@ -111,9 +110,7 @@ predicate dominates(ControlFlowNode dom, ControlFlowNode node) {
// This predicate is gigantic, so it must be inlined.
bbStrictlyDominates(dom.getBasicBlock(), node.getBasicBlock())
or
exists(BasicBlock b, int i, int j |
dom = b.getNode(i) and node = b.getNode(j) and i <= j
)
exists(BasicBlock b, int i, int j | dom = b.getNode(i) and node = b.getNode(j) and i <= j)
}
/** Holds if `dom` strictly post-dominates `node`. */
@ -122,9 +119,7 @@ predicate strictlyPostDominates(ControlFlowNode dom, ControlFlowNode node) {
// This predicate is gigantic, so it must be inlined.
bbStrictlyPostDominates(dom.getBasicBlock(), node.getBasicBlock())
or
exists(BasicBlock b, int i, int j |
dom = b.getNode(i) and node = b.getNode(j) and i > j
)
exists(BasicBlock b, int i, int j | dom = b.getNode(i) and node = b.getNode(j) and i > j)
}
/** Holds if `dom` post-dominates `node`. (This is reflexive.) */
@ -133,7 +128,5 @@ predicate postDominates(ControlFlowNode dom, ControlFlowNode node) {
// This predicate is gigantic, so it must be inlined.
bbStrictlyPostDominates(dom.getBasicBlock(), node.getBasicBlock())
or
exists(BasicBlock b, int i, int j |
dom = b.getNode(i) and node = b.getNode(j) and i >= j
)
exists(BasicBlock b, int i, int j | dom = b.getNode(i) and node = b.getNode(j) and i >= j)
}

Просмотреть файл

@ -6,19 +6,13 @@ private import semmle.code.java.controlflow.internal.GuardsLogic
* A basic block that terminates in a condition, splitting the subsequent control flow.
*/
class ConditionBlock extends BasicBlock {
ConditionBlock() {
this.getLastNode() instanceof ConditionNode
}
ConditionBlock() { this.getLastNode() instanceof ConditionNode }
/** Gets the last node of this basic block. */
ConditionNode getConditionNode() {
result = this.getLastNode()
}
ConditionNode getConditionNode() { result = this.getLastNode() }
/** Gets the condition of the last node of this basic block. */
Expr getCondition() {
result = this.getConditionNode().getCondition()
}
Expr getCondition() { result = this.getConditionNode().getCondition() }
/** Gets a `true`- or `false`-successor of the last node of this basic block. */
BasicBlock getTestSuccessor(boolean testIsTrue) {
@ -63,6 +57,7 @@ class ConditionBlock extends BasicBlock {
* that `this` strictly dominates `controlled` so that isn't necessary to check
* directly.
*/
exists(BasicBlock succ |
succ = this.getTestSuccessor(testIsTrue) and
succ.bbDominates(controlled) and
@ -83,7 +78,8 @@ class ConditionBlock extends BasicBlock {
*/
class Guard extends ExprParent {
Guard() {
this.(Expr).getType() instanceof BooleanType and not this instanceof BooleanLiteral or
this.(Expr).getType() instanceof BooleanType and not this instanceof BooleanLiteral
or
this instanceof SwitchCase
}
@ -106,10 +102,9 @@ class Guard extends ExprParent {
* true.
*/
predicate isEquality(Expr e1, Expr e2, boolean polarity) {
exists(Expr exp1, Expr exp2 |
equalityGuard(this, exp1, exp2, polarity)
|
e1 = exp1.getProperExpr() and e2 = exp2.getProperExpr() or
exists(Expr exp1, Expr exp2 | equalityGuard(this, exp1, exp2, polarity) |
e1 = exp1.getProperExpr() and e2 = exp2.getProperExpr()
or
e2 = exp1.getProperExpr() and e1 = exp2.getProperExpr()
)
}
@ -123,7 +118,8 @@ class Guard extends ExprParent {
cb = bb1 and
cb.getCondition() = this and
bb2 = cb.getTestSuccessor(branch)
) or
)
or
exists(SwitchCase sc, ControlFlowNode pred |
sc = this and
branch = true and
@ -143,7 +139,8 @@ class Guard extends ExprParent {
exists(ConditionBlock cb |
cb.getCondition() = this and
cb.controls(controlled, branch)
) or
)
or
switchCaseControls(this, controlled) and branch = true
}
@ -175,7 +172,8 @@ private predicate switchCaseControls(SwitchCase sc, BasicBlock bb) {
* BaseSSA-based reasoning.
*/
predicate guardControls_v1(Guard guard, BasicBlock controlled, boolean branch) {
guard.directlyControls(controlled, branch) or
guard.directlyControls(controlled, branch)
or
exists(Guard g, boolean b |
guardControls_v1(g, controlled, b) and
implies_v1(g, b, guard, branch)
@ -189,7 +187,8 @@ predicate guardControls_v1(Guard guard, BasicBlock controlled, boolean branch) {
* RangeAnalysis.
*/
predicate guardControls_v2(Guard guard, BasicBlock controlled, boolean branch) {
guard.directlyControls(controlled, branch) or
guard.directlyControls(controlled, branch)
or
exists(Guard g, boolean b |
guardControls_v2(g, controlled, b) and
implies_v2(g, b, guard, branch)
@ -197,7 +196,8 @@ predicate guardControls_v2(Guard guard, BasicBlock controlled, boolean branch) {
}
private predicate guardControls_v3(Guard guard, BasicBlock controlled, boolean branch) {
guard.directlyControls(controlled, branch) or
guard.directlyControls(controlled, branch)
or
exists(Guard g, boolean b |
guardControls_v3(g, controlled, b) and
implies_v3(g, b, guard, branch)
@ -209,13 +209,16 @@ private predicate equalityGuard(Guard g, Expr e1, Expr e2, boolean polarity) {
eqtest = g and
polarity = eqtest.polarity() and
eqtest.hasOperands(e1, e2)
) or
)
or
exists(MethodAccess ma |
ma = g and
ma.getMethod() instanceof EqualsMethod and
polarity = true and
ma.getAnArgument() = e1 and ma.getQualifier() = e2
) or
ma.getAnArgument() = e1 and
ma.getQualifier() = e2
)
or
exists(MethodAccess ma, Method equals |
ma = g and
ma.getMethod() = equals and
@ -223,11 +226,14 @@ private predicate equalityGuard(Guard g, Expr e1, Expr e2, boolean polarity) {
equals.hasName("equals") and
equals.getNumberOfParameters() = 2 and
equals.getDeclaringType().hasQualifiedName("java.util", "Objects") and
ma.getArgument(0) = e1 and ma.getArgument(1) = e2
) or
ma.getArgument(0) = e1 and
ma.getArgument(1) = e2
)
or
exists(ConstCase cc |
cc = g and
polarity = true and
cc.getSwitch().getExpr().getProperExpr() = e1 and cc.getValue() = e2
cc.getSwitch().getExpr().getProperExpr() = e1 and
cc.getValue() = e2
)
}

Просмотреть файл

@ -25,9 +25,7 @@ abstract class ActionConfiguration extends string {
}
/** Holds if every path through `call` goes through at least one action node. */
final predicate callAlwaysPerformsAction(Call call) {
callAlwaysPerformsAction(call, this)
}
final predicate callAlwaysPerformsAction(Call call) { callAlwaysPerformsAction(call, this) }
}
/** Gets a `BasicBlock` that contains an action. */
@ -40,7 +38,9 @@ private BasicBlock actionBlock(ActionConfiguration conf) {
/** Holds if every path through `call` goes through at least one action node. */
private predicate callAlwaysPerformsAction(Call call, ActionConfiguration conf) {
forex(Callable callable | callable = viableCallable(call) | callableAlwaysPerformsAction(callable, conf))
forex(Callable callable | callable = viableCallable(call) |
callableAlwaysPerformsAction(callable, conf)
)
}
/** Holds if an action dominates the exit of the callable. */
@ -60,18 +60,20 @@ private BasicBlock nonDominatingActionBlock(ActionConfiguration conf) {
)
}
private class JoinBlock extends BasicBlock { JoinBlock() { 2 <= strictcount(this.getABBPredecessor()) } }
private class JoinBlock extends BasicBlock {
JoinBlock() { 2 <= strictcount(this.getABBPredecessor()) }
}
/**
* Holds if `bb` is a block that is collectively dominated by a set of one or
* more actions that individually does not dominate the exit.
*/
private predicate postActionBlock(BasicBlock bb, ActionConfiguration conf) {
bb = nonDominatingActionBlock(conf) or
if bb instanceof JoinBlock then
forall(BasicBlock pred | pred = bb.getABBPredecessor() | postActionBlock(pred, conf))
else
postActionBlock(bb.getABBPredecessor(), conf)
bb = nonDominatingActionBlock(conf)
or
if bb instanceof JoinBlock
then forall(BasicBlock pred | pred = bb.getABBPredecessor() | postActionBlock(pred, conf))
else postActionBlock(bb.getABBPredecessor(), conf)
}
/** Holds if every path through `callable` goes through at least one action node. */

Просмотреть файл

@ -1,6 +1,7 @@
/**
* Provides classes and predicates for identifying unreachable blocks under a "closed-world" assumption.
*/
import java
import semmle.code.java.controlflow.Guards
@ -18,14 +19,14 @@ class ConstantField extends Field {
* And that assignment is either in the appropriate initializer, or, for instance fields on
* classes with one constructor, in the constructor.
*/
forall(FieldWrite fa |
fa = getAnAccess()
|
if isStatic() then
fa.getEnclosingCallable() instanceof StaticInitializer
forall(FieldWrite fa | fa = getAnAccess() |
if isStatic()
then fa.getEnclosingCallable() instanceof StaticInitializer
else (
// Defined in the instance initializer.
fa.getEnclosingCallable() instanceof InstanceInitializer or
fa.getEnclosingCallable() instanceof InstanceInitializer
or
// It can be defined in the constructor if there is only one constructor.
(
fa.getEnclosingCallable() instanceof Constructor and
@ -40,9 +41,7 @@ class ConstantField extends Field {
*
* Note: although this value is constant, we may not be able to statically determine the value.
*/
ConstantExpr getConstantValue() {
result = getAnAssignedValue()
}
ConstantExpr getConstantValue() { result = getAnAssignedValue() }
}
/**
@ -53,7 +52,9 @@ class ConstantMethod extends Method {
// Just one return statement
count(ReturnStmt rs | rs.getEnclosingCallable() = this) = 1 and
// Which returns a constant expr
exists(ReturnStmt rs | rs.getEnclosingCallable() = this | rs.getResult() instanceof ConstantExpr) and
exists(ReturnStmt rs | rs.getEnclosingCallable() = this |
rs.getResult() instanceof ConstantExpr
) and
// And this method is not overridden
not exists(Method m | m.overrides(this))
}
@ -62,10 +63,9 @@ class ConstantMethod extends Method {
* Gets the expression representing the constant value returned.
*/
ConstantExpr getConstantValue() {
exists(ReturnStmt returnStmt |
returnStmt.getEnclosingCallable() = this
|
result = returnStmt.getResult())
exists(ReturnStmt returnStmt | returnStmt.getEnclosingCallable() = this |
result = returnStmt.getResult()
)
}
}
@ -73,8 +73,7 @@ class ConstantMethod extends Method {
* A field that appears constant, but should not be considered constant when determining
* `ConstantExpr`, and, consequently, in the unreachable blocks analysis.
*/
abstract class ExcludedConstantField extends ConstantField {
}
abstract class ExcludedConstantField extends ConstantField { }
/**
* An expression that evaluates to a constant at runtime.
@ -87,19 +86,24 @@ class ConstantExpr extends Expr {
/*
* Ignore reads of excluded fields.
*/
not this.(FieldRead).getField() instanceof ExcludedConstantField and
(
// A JLS compile time constant expr
this instanceof CompileTimeConstantExpr or
this instanceof CompileTimeConstantExpr
or
// A call to a constant method
this.(Call).getCallee() instanceof ConstantMethod or
this.(Call).getCallee() instanceof ConstantMethod
or
// A read of a constant field
exists(this.(FieldRead).getField().(ConstantField).getConstantValue()) or
exists(this.(FieldRead).getField().(ConstantField).getConstantValue())
or
// A binary expression where both sides are constant
(
this.(BinaryExpr).getLeftOperand() instanceof ConstantExpr and
this.(BinaryExpr).getRightOperand() instanceof ConstantExpr
) or
)
or
this.(ParExpr).getExpr() instanceof ConstantExpr
)
}
@ -108,22 +112,49 @@ class ConstantExpr extends Expr {
* Gets the inferred boolean value for this constant boolean expression.
*/
boolean getBooleanValue() {
result = this.(CompileTimeConstantExpr).getBooleanValue() or
result = this.(Call).getCallee().(ConstantMethod).getConstantValue().getBooleanValue() or
result = this.(FieldRead).getField().(ConstantField).getConstantValue().getBooleanValue() or
result = this.(ParExpr).getExpr().(ConstantExpr).getBooleanValue() or
result = this.(CompileTimeConstantExpr).getBooleanValue()
or
result = this.(Call).getCallee().(ConstantMethod).getConstantValue().getBooleanValue()
or
result = this.(FieldRead).getField().(ConstantField).getConstantValue().getBooleanValue()
or
result = this.(ParExpr).getExpr().(ConstantExpr).getBooleanValue()
or
// Handle binary expressions that have integer operands and a boolean result.
exists(BinaryExpr b, int left, int right |
b = this and
left = b.getLeftOperand().(ConstantExpr).getIntValue() and
right = b.getRightOperand().(ConstantExpr).getIntValue()
|
(b instanceof LTExpr and if left < right then result = true else result = false) or
(b instanceof LEExpr and if left <= right then result = true else result = false) or
(b instanceof GTExpr and if left > right then result = true else result = false) or
(b instanceof GEExpr and if left >= right then result = true else result = false) or
(b instanceof EQExpr and if left = right then result = true else result = false) or
(b instanceof NEExpr and if left != right then result = true else result = false)
(
b instanceof LTExpr and
if left < right then result = true else result = false
)
or
(
b instanceof LEExpr and
if left <= right then result = true else result = false
)
or
(
b instanceof GTExpr and
if left > right then result = true else result = false
)
or
(
b instanceof GEExpr and
if left >= right then result = true else result = false
)
or
(
b instanceof EQExpr and
if left = right then result = true else result = false
)
or
(
b instanceof NEExpr and
if left != right then result = true else result = false
)
)
}
@ -141,9 +172,7 @@ class ConstantExpr extends Expr {
* A switch statement that always selects the same case.
*/
class ConstSwitchStmt extends SwitchStmt {
ConstSwitchStmt() {
this.getExpr() instanceof ConstantExpr
}
ConstSwitchStmt() { this.getExpr() instanceof ConstantExpr }
/** Gets the `ConstCase` that matches, if any. */
ConstCase getMatchingConstCase() {
@ -156,10 +185,9 @@ class ConstSwitchStmt extends SwitchStmt {
SwitchCase getMatchingCase() {
// Must be a value we can deduce
exists(getExpr().(ConstantExpr).getIntValue()) and
if (exists(getMatchingConstCase())) then
result = getMatchingConstCase()
else
result = getDefaultCase()
if (exists(getMatchingConstCase()))
then result = getMatchingConstCase()
else result = getDefaultCase()
}
/**
@ -188,28 +216,27 @@ class UnreachableBasicBlock extends BasicBlock {
* modeled as a ConditionBlock - this case is covered by the blocks-without-a-predecessor
* check below.
*/
exists(ConditionBlock conditionBlock, boolean constant |
constant = conditionBlock.getCondition().(ConstantExpr).getBooleanValue()
|
conditionBlock.controls(this, constant.booleanNot())
) or
)
or
/*
* This block is not reachable in the CFG, and is not a callable, a body of a callable, an
* expression in an annotation, an expression in an assert statement, or a catch clause.
*/
(
forall(BasicBlock bb | bb = getABBPredecessor() | bb instanceof UnreachableBasicBlock) and
not exists(Callable c |
c.getBody() = this) and
not exists(Callable c | c.getBody() = this) and
not this instanceof Callable and
not exists(Annotation a |
a.getAChildExpr*() = this
) and
not exists(AssertStmt a |
a = this.(Expr).getEnclosingStmt()
) and
not exists(Annotation a | a.getAChildExpr*() = this) and
not exists(AssertStmt a | a = this.(Expr).getEnclosingStmt()) and
not this instanceof CatchClause
) or
)
or
// Switch statements with a constant comparison expression may have unreachable cases.
exists(ConstSwitchStmt constSwitchStmt, BasicBlock failingCaseBlock |
failingCaseBlock = constSwitchStmt.getAFailingCase().getBasicBlock()
@ -226,16 +253,12 @@ class UnreachableBasicBlock extends BasicBlock {
* An unreachable expression is an expression contained in an `UnreachableBasicBlock`.
*/
class UnreachableExpr extends Expr {
UnreachableExpr() {
getBasicBlock() instanceof UnreachableBasicBlock
}
UnreachableExpr() { getBasicBlock() instanceof UnreachableBasicBlock }
}
/**
* An unreachable statement is a statement contained in an `UnreachableBasicBlock`.
*/
class UnreachableStmt extends Stmt {
UnreachableStmt() {
getBasicBlock() instanceof UnreachableBasicBlock
}
UnreachableStmt() { getBasicBlock() instanceof UnreachableBasicBlock }
}

Просмотреть файл

@ -2,6 +2,7 @@
* Provides predicates for working with the internal logic of the `Guards`
* library.
*/
import java
import semmle.code.java.controlflow.Guards
private import semmle.code.java.dataflow.SSA
@ -17,33 +18,49 @@ private import semmle.code.java.dataflow.IntegerGuards
* Restricted to BaseSSA-based reasoning.
*/
predicate implies_v1(Guard g1, boolean b1, Guard g2, boolean b2) {
g1.(ParExpr).getExpr() = g2 and b1 = b2 and (b1 = true or b1 = false) or
g1.(AndBitwiseExpr).getAnOperand() = g2 and b1 = true and b2 = true or
g1.(OrBitwiseExpr).getAnOperand() = g2 and b1 = false and b2 = false or
g1.(AndLogicalExpr).getAnOperand() = g2 and b1 = true and b2 = true or
g1.(OrLogicalExpr).getAnOperand() = g2 and b1 = false and b2 = false or
g1.(LogNotExpr).getExpr() = g2 and b1 = b2.booleanNot() and (b1 = true or b1 = false) or
g1.(ParExpr).getExpr() = g2 and
b1 = b2 and
(b1 = true or b1 = false)
or
g1.(AndBitwiseExpr).getAnOperand() = g2 and b1 = true and b2 = true
or
g1.(OrBitwiseExpr).getAnOperand() = g2 and b1 = false and b2 = false
or
g1.(AndLogicalExpr).getAnOperand() = g2 and b1 = true and b2 = true
or
g1.(OrLogicalExpr).getAnOperand() = g2 and b1 = false and b2 = false
or
g1.(LogNotExpr).getExpr() = g2 and
b1 = b2.booleanNot() and
(b1 = true or b1 = false)
or
exists(EqualityTest eqtest, boolean polarity, BooleanLiteral boollit |
eqtest = g1 and
eqtest.hasOperands(g2, boollit) and
eqtest.polarity() = polarity and
(b1 = true or b1 = false) and
b2 = b1.booleanXor(polarity).booleanXor(boollit.getBooleanValue())
) or
)
or
exists(ConditionalExpr cond, boolean branch, BooleanLiteral boollit, boolean boolval |
cond.getTrueExpr() = boollit and branch = true or
cond.getTrueExpr() = boollit and branch = true
or
cond.getFalseExpr() = boollit and branch = false
|
cond = g1 and
boolval = boollit.getBooleanValue() and
b1 = boolval.booleanNot() and
(
g2 = cond.getCondition() and b2 = branch.booleanNot() or
g2 = cond.getTrueExpr() and b2 = b1 or
g2 = cond.getCondition() and b2 = branch.booleanNot()
or
g2 = cond.getTrueExpr() and b2 = b1
or
g2 = cond.getFalseExpr() and b2 = b1
)
) or
g1.(DefaultCase).getSwitch().getAConstCase() = g2 and b1 = true and b2 = false or
)
or
g1.(DefaultCase).getSwitch().getAConstCase() = g2 and b1 = true and b2 = false
or
exists(BaseSsaUpdate vbool |
vbool.getAUse() = g1 and
vbool.getDefiningExpr().(VariableAssign).getSource() = g2 and
@ -60,19 +77,22 @@ predicate implies_v1(Guard g1, boolean b1, Guard g2, boolean b2) {
* Allows full use of SSA but is restricted to pre-RangeAnalysis reasoning.
*/
predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
implies_v1(g1, b1, g2, b2) or
implies_v1(g1, b1, g2, b2)
or
exists(SsaExplicitUpdate vbool |
vbool.getAUse() = g1 and
vbool.getDefiningExpr().(VariableAssign).getSource() = g2 and
(b1 = true or b1 = false) and
b2 = b1
) or
)
or
exists(SsaVariable v, AbstractValue k |
// If `v = g2 ? k : ...` or `v = g2 ? ... : k` then a guard
// proving `v != k` ensures that `g2` evaluates to `b2`.
conditionalAssignVal(v, g2, b2.booleanNot(), k) and
guardImpliesNotEqual1(g1, b1, v, k)
) or
)
or
exists(SsaVariable v, Expr e, AbstractValue k |
// If `v = g2 ? k : ...` and all other assignments to `v` are different from
// `k` then a guard proving `v == k` ensures that `g2` evaluates to `b2`.
@ -90,13 +110,15 @@ predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
*/
cached
predicate implies_v3(Guard g1, boolean b1, Guard g2, boolean b2) {
implies_v2(g1, b1, g2, b2) or
implies_v2(g1, b1, g2, b2)
or
exists(SsaVariable v, AbstractValue k |
// If `v = g2 ? k : ...` or `v = g2 ? ... : k` then a guard
// proving `v != k` ensures that `g2` evaluates to `b2`.
conditionalAssignVal(v, g2, b2.booleanNot(), k) and
guardImpliesNotEqual2(g1, b1, v, k)
) or
)
or
exists(SsaVariable v |
conditionalAssign(v, g2, b2.booleanNot(), clearlyNotNullExpr()) and
guardImpliesEqual(g1, b1, v, TAbsValNull())
@ -111,42 +133,56 @@ private newtype TAbstractValue =
TAbsValEnum(EnumConstant c)
/** The value of a constant expression. */
private abstract class AbstractValue extends TAbstractValue {
abstract private class AbstractValue extends TAbstractValue {
abstract string toString();
/** Gets an expression whose value is this abstract value. */
abstract Expr getExpr();
}
private class AbsValNull extends AbstractValue, TAbsValNull {
override string toString() { result = "null" }
override Expr getExpr() { result = alwaysNullExpr() }
}
private class AbsValInt extends AbstractValue, TAbsValInt {
int i;
AbsValInt() { this = TAbsValInt(i) }
override string toString() { result = i.toString() }
override Expr getExpr() { result.(CompileTimeConstantExpr).getIntValue() = i }
}
private class AbsValChar extends AbstractValue, TAbsValChar {
string c;
AbsValChar() { this = TAbsValChar(c) }
override string toString() { result = c }
override Expr getExpr() { result.(CharacterLiteral).getValue() = c }
}
private class AbsValString extends AbstractValue, TAbsValString {
string s;
AbsValString() { this = TAbsValString(s) }
override string toString() { result = s }
override Expr getExpr() { result.(CompileTimeConstantExpr).getStringValue() = s }
}
private class AbsValEnum extends AbstractValue, TAbsValEnum {
EnumConstant c;
AbsValEnum() { this = TAbsValEnum(c) }
override string toString() { result = c.toString() }
override Expr getExpr() { result = c.getAnAccess() }
}
@ -155,11 +191,14 @@ private class AbsValEnum extends AbstractValue, TAbsValEnum {
*/
private predicate hasPossibleUnknownValue(SsaVariable v) {
exists(SsaVariable def | v.getAnUltimateDefinition() = def |
def instanceof SsaImplicitUpdate or
def instanceof SsaImplicitInit or
def instanceof SsaImplicitUpdate
or
def instanceof SsaImplicitInit
or
exists(VariableUpdate upd | upd = def.(SsaExplicitUpdate).getDefiningExpr() |
not exists(upd.(VariableAssign).getSource())
) or
)
or
exists(VariableAssign a, Expr e |
a = def.(SsaExplicitUpdate).getDefiningExpr() and
e = possibleValue(a.getSource()) and
@ -173,9 +212,12 @@ private predicate hasPossibleUnknownValue(SsaVariable v) {
* `ConditionalExpr`s. Parentheses are also removed.
*/
private Expr possibleValue(Expr e) {
result = possibleValue(e.(ParExpr).getExpr()) or
result = possibleValue(e.(ConditionalExpr).getTrueExpr()) or
result = possibleValue(e.(ConditionalExpr).getFalseExpr()) or
result = possibleValue(e.(ParExpr).getExpr())
or
result = possibleValue(e.(ConditionalExpr).getTrueExpr())
or
result = possibleValue(e.(ConditionalExpr).getFalseExpr())
or
result = e and not e instanceof ParExpr and not e instanceof ConditionalExpr
}
@ -185,7 +227,8 @@ private Expr possibleValue(Expr e) {
* through a back edge.
*/
SsaVariable getADefinition(SsaVariable v, boolean fromBackEdge) {
result = v and not v instanceof SsaPhiNode and fromBackEdge = false or
result = v and not v instanceof SsaPhiNode and fromBackEdge = false
or
exists(SsaVariable inp, BasicBlock bb, boolean fbe |
v.(SsaPhiNode).hasInputFromBlock(inp, bb) and
result = getADefinition(inp, fbe) and
@ -215,7 +258,9 @@ private predicate possibleValue(SsaVariable v, boolean fromBackEdge, Expr e, Abs
*/
private predicate uniqueValue(SsaVariable v, Expr e, AbstractValue k) {
possibleValue(v, false, e, k) and
forex(Expr other, AbstractValue otherval | possibleValue(v, _, other, otherval) and other != e | otherval != k)
forex(Expr other, AbstractValue otherval | possibleValue(v, _, other, otherval) and other != e |
otherval != k
)
}
/**
@ -231,7 +276,8 @@ private BasicBlock getBasicBlockOfGuard(Guard g) {
}
private ControlFlowNode getAGuardBranchSuccessor(Guard g, boolean branch) {
result = g.(Expr).getControlFlowNode().(ConditionNode).getABranchSuccessor(branch) or
result = g.(Expr).getControlFlowNode().(ConditionNode).getABranchSuccessor(branch)
or
result = g.(SwitchCase).getControlFlowNode() and branch = true
}
@ -243,9 +289,11 @@ private predicate conditionalAssign(SsaVariable v, Guard guard, boolean branch,
v.(SsaExplicitUpdate).getDefiningExpr().(VariableAssign).getSource().getProperExpr() = c and
guard = c.getCondition().getProperExpr()
|
branch = true and e = c.getTrueExpr().getProperExpr() or
branch = true and e = c.getTrueExpr().getProperExpr()
or
branch = false and e = c.getFalseExpr().getProperExpr()
) or
)
or
exists(SsaExplicitUpdate upd, SsaPhiNode phi |
guard.directlyControls(upd.getBasicBlock(), branch) and
upd.getDefiningExpr().(VariableAssign).getSource().getProperExpr() = e and
@ -254,7 +302,8 @@ private predicate conditionalAssign(SsaVariable v, Guard guard, boolean branch,
getBasicBlockOfGuard(guard).bbStrictlyDominates(phi.getBasicBlock()) and
not guard.directlyControls(phi.getBasicBlock(), branch) and
forall(SsaVariable other | other != upd and other = phi.getAPhiInput() |
guard.directlyControls(other.getBasicBlock(), branch.booleanNot()) or
guard.directlyControls(other.getBasicBlock(), branch.booleanNot())
or
other.getBasicBlock().bbDominates(getBasicBlockOfGuard(guard)) and
not other.isLiveAtEndOfBlock(getAGuardBranchSuccessor(guard, branch))
)
@ -275,7 +324,9 @@ private predicate relevantEq(SsaVariable v, AbstractValue val) {
/**
* Holds if the evaluation of `guard` to `branch` implies that `v` does not have the value `val`.
*/
private predicate guardImpliesNotEqual1(Guard guard, boolean branch, SsaVariable v, AbstractValue val) {
private predicate guardImpliesNotEqual1(
Guard guard, boolean branch, SsaVariable v, AbstractValue val
) {
relevantEq(v, val) and
(
guard.isEquality(v.getAUse(), val.getExpr(), branch.booleanNot())
@ -292,7 +343,9 @@ private predicate guardImpliesNotEqual1(Guard guard, boolean branch, SsaVariable
/**
* Holds if the evaluation of `guard` to `branch` implies that `v` does not have the value `val`.
*/
private predicate guardImpliesNotEqual2(Guard guard, boolean branch, SsaVariable v, AbstractValue val) {
private predicate guardImpliesNotEqual2(
Guard guard, boolean branch, SsaVariable v, AbstractValue val
) {
relevantEq(v, val) and
(
guard = directNullGuard(v, branch, false) and val = TAbsValNull()
@ -303,4 +356,3 @@ private predicate guardImpliesNotEqual2(Guard guard, boolean branch, SsaVariable
)
)
}