Merge pull request #1823 from markshannon/python-dont-prune-in-ql

Python: removing pruning in QL.
This commit is contained in:
Pavel Avgustinov
2019-08-27 11:32:23 +01:00
committed by GitHub
16 changed files with 10 additions and 1339 deletions

View File

@@ -1,7 +1,6 @@
import python
import semmle.python.flow.NameNode
private import semmle.python.pointsto.PointsTo
private import semmle.python.Pruning
/* Note about matching parent and child nodes and CFG splitting:
*
@@ -33,10 +32,6 @@ private AstNode toAst(ControlFlowNode n) {
*/
class ControlFlowNode extends @py_flow_node {
cached ControlFlowNode() {
Pruner::reachable(this)
}
/** Whether this control flow node is a load (including those in augmented assignments) */
predicate isLoad() {
exists(Expr e | e = toAst(this) | py_expr_contexts(_, 3, e) and not augstore(_, this))
@@ -180,8 +175,7 @@ class ControlFlowNode extends @py_flow_node {
/** Gets a successor of this flow node */
ControlFlowNode getASuccessor() {
py_successors(this, result) and
not Pruner::unreachableEdge(this, result)
py_successors(this, result)
}
/** Gets the immediate dominator of this flow node */
@@ -973,91 +967,21 @@ predicate defined_by(NameNode def, Variable v) {
exists(NameNode p | defined_by(p, v) and p.getASuccessor() = def and not p.defines(v))
}
/* Combine extractor-generated basic block after pruning */
private class BasicBlockPart extends @py_flow_node {
string toString() { result = "Basic block part" }
BasicBlockPart() {
py_flow_bb_node(_, _, this, _) and
Pruner::reachable(this)
}
predicate isHead() {
count(this.(ControlFlowNode).getAPredecessor()) != 1
or
exists(ControlFlowNode pred | pred = this.(ControlFlowNode).getAPredecessor() | strictcount(pred.getASuccessor()) > 1)
}
private BasicBlockPart previous() {
not this.isHead() and
py_flow_bb_node(this.(ControlFlowNode).getAPredecessor(), _, result, _)
}
BasicBlockPart getHead() {
this.isHead() and result = this
or
result = this.previous().getHead()
}
predicate isLast() {
not exists(BasicBlockPart part | part.previous() = this)
}
int length() {
result = max(int j | py_flow_bb_node(_, _, this, j)) + 1
}
int startIndex() {
this.isHead() and result = 0
or
exists(BasicBlockPart prev |
prev = this.previous() and
result = prev.startIndex() + prev.length()
)
}
predicate contains(ControlFlowNode node) {
py_flow_bb_node(node, _, this, _)
}
int indexOf(ControlFlowNode node) {
py_flow_bb_node(node, _, this, result)
}
ControlFlowNode lastNode() {
this.indexOf(result) = max(this.indexOf(_))
}
BasicBlockPart getImmediateDominator() {
result.contains(this.(ControlFlowNode).getImmediateDominator())
}
}
/** A basic block (ignoring exceptional flow edges to scope exit) */
class BasicBlock extends @py_flow_node {
BasicBlock() {
this.(BasicBlockPart).isHead()
}
private BasicBlockPart getAPart() {
result.getHead() = this
py_flow_bb_node(_, _, this, _)
}
/** Whether this basic block contains the specified node */
predicate contains(ControlFlowNode node) {
this.getAPart().contains(node)
py_flow_bb_node(node, _, this, _)
}
/** Gets the nth node in this basic block */
ControlFlowNode getNode(int n) {
exists(BasicBlockPart part |
part = this.getAPart() and
n = part.startIndex() + part.indexOf(result)
)
py_flow_bb_node(result, _, this, n)
}
string toString() {
@@ -1077,7 +1001,7 @@ class BasicBlock extends @py_flow_node {
}
cached BasicBlock getImmediateDominator() {
this.getAPart().getImmediateDominator() = result.getAPart()
this.firstNode().getImmediateDominator().getBasicBlock() = result
}
/** Dominance frontier of a node x is the set of all nodes `other` such that `this` dominates a predecessor
@@ -1093,10 +1017,9 @@ class BasicBlock extends @py_flow_node {
/** Gets the last node in this basic block */
ControlFlowNode getLastNode() {
exists(BasicBlockPart part |
part = this.getAPart() and
part.isLast() and
result = part.lastNode()
exists(int i |
this.getNode(i) = result and
i = max(int j | py_flow_bb_node(_, _, this, j))
)
}

View File

@@ -1,640 +0,0 @@
private import AST
private import Exprs
private import Stmts
private import Import
private import Operations
module Pruner {
/** A control flow node before pruning */
class UnprunedCfgNode extends @py_flow_node {
string toString() { none() }
/** Gets a predecessor of this flow node */
UnprunedCfgNode getAPredecessor() {
py_successors(result, this)
}
/** Gets a successor of this flow node */
UnprunedCfgNode getASuccessor() {
py_successors(this, result)
}
/** Gets the immediate dominator of this flow node */
UnprunedCfgNode getImmediateDominator() {
py_idoms(this, result)
}
/* Holds if this CFG node is a branch */
predicate isBranch() {
py_true_successors(this, _) or py_false_successors(this, _)
}
/** Gets the syntactic element corresponding to this flow node */
AstNode getNode() {
py_flow_bb_node(this, result, _, _)
}
UnprunedBasicBlock getBasicBlock() {
py_flow_bb_node(this, _, result, _)
}
/** Gets a successor for this node if the relevant condition is True. */
UnprunedCfgNode getATrueSuccessor() {
py_true_successors(this, result)
}
/** Gets a successor for this node if the relevant condition is False. */
UnprunedCfgNode getAFalseSuccessor() {
py_false_successors(this, result)
}
}
/** A control flow node corresponding to a comparison operation, such as `x<y` */
class UnprunedCompareNode extends UnprunedCfgNode {
UnprunedCompareNode() {
py_flow_bb_node(this, any(Compare c), _, _)
}
/** Whether left and right are a pair of operands for this comparison */
predicate operands(UnprunedCfgNode left, Cmpop op, UnprunedCfgNode right) {
exists(Compare c, Expr eleft, Expr eright |
this.getNode() = c and left.getNode() = eleft and right.getNode() = eright |
eleft = c.getLeft() and eright = c.getComparator(0) and op = c.getOp(0)
or
exists(int i | eleft = c.getComparator(i-1) and eright = c.getComparator(i) and op = c.getOp(i))
) and
left.getBasicBlock().dominates(this.getBasicBlock()) and
right.getBasicBlock().dominates(this.getBasicBlock())
}
}
/** A control flow node corresponding to a unary not expression: (`not x`) */
class UnprunedNot extends UnprunedCfgNode {
UnprunedNot() {
exists(UnaryExpr unary |
py_flow_bb_node(this, unary, _, _) and
unary.getOp() instanceof Not
)
}
/** Gets the control flow node corresponding to the operand of this `not` expression */
UnprunedCfgNode getOperand() {
exists(UnaryExpr u | this.getNode() = u and result.getNode() = u.getOperand()) and
result.getBasicBlock().dominates(this.getBasicBlock())
}
}
/** A basic block before pruning */
class UnprunedBasicBlock extends @py_flow_node {
UnprunedBasicBlock() {
py_flow_bb_node(_, _, this, _)
}
/** Whether this basic block contains the specified node */
predicate contains(UnprunedCfgNode node) {
py_flow_bb_node(node, _, this, _)
}
string toString() { none() }
/** Whether this basic block strictly dominates the other */
pragma[nomagic] predicate strictlyDominates(UnprunedBasicBlock other) {
other.getImmediateDominator+() = this
}
/** Whether this basic block dominates the other */
pragma[nomagic] predicate dominates(UnprunedBasicBlock other) {
this = other
or
this.strictlyDominates(other)
}
UnprunedBasicBlock getImmediateDominator() {
this.first().getImmediateDominator().getBasicBlock() = result
}
UnprunedBasicBlock getASuccessor() {
this.last().getASuccessor() = result.first()
}
UnprunedCfgNode first() {
py_flow_bb_node(result, _, this, 0)
}
UnprunedCfgNode last() {
py_flow_bb_node(result, _, this, max(int i | py_flow_bb_node(_, _, this, i)))
}
/** Gets a successor for this node if the relevant condition is True. */
UnprunedBasicBlock getATrueSuccessor() {
this.last().getATrueSuccessor() = result.first()
}
/** Gets a successor for this node if the relevant condition is False. */
UnprunedBasicBlock getAFalseSuccessor() {
this.last().getAFalseSuccessor() = result.first()
}
/** Whether this BB is the first in its scope */
predicate isEntry() {
py_scope_flow(this.first(), _, -1)
}
UnprunedCfgNode getANode() {
py_flow_bb_node(result, _, this, _)
}
}
private import Comparisons
private import SSA
private int intValue(ImmutableLiteral lit) {
result = lit.(IntegerLiteral).getValue()
or
result = lit.(NegativeIntegerLiteral).getValue()
}
newtype TConstraint =
TTruthy(boolean b) { b = true or b = false }
or
TIsNone(boolean b) { b = true or b = false }
or
TConstrainedByConstant(CompareOp op, int k) {
int_test(_, _, op, k)
or
exists(Assign a | intValue(a.getValue()) = k) and op = eq()
}
/** A constraint that may be applied to an SSA variable.
* Used for computing unreachable edges
*/
abstract class Constraint extends TConstraint {
abstract string toString();
abstract Constraint invert();
/** Holds if this constraint constrains the "truthiness" of the variable.
* That is, for a variable `var` constrained by this constraint
* `bool(var) is value`
*/
abstract predicate constrainsVariableToBe(boolean value);
/** Holds if the value constrained by this constraint cannot be `None` */
abstract predicate cannotBeNone();
}
/** A basic block ending in a test (and branch). */
class UnprunedConditionBlock extends UnprunedBasicBlock {
UnprunedConditionBlock() { this.last().isBranch() }
/** Holds if `controlled` is only reachable if the test in this block evaluates to `testIsTrue` */
predicate controls(UnprunedBasicBlock controlled, boolean testIsTrue) {
/* For this block to control the block 'controlled' with 'testIsTrue' the following must be true:
Execution must have passed through the test i.e. 'this' must strictly dominate 'controlled'.
Execution must have passed through the 'testIsTrue' edge leaving 'this'.
Although "passed through the true edge" implies that this.getATrueSuccessor() dominates 'controlled',
the reverse is not true, as flow may have passed through another edge to get to this.getATrueSuccessor()
so we need to assert that this.getATrueSuccessor() dominates 'controlled' *and* that
all predecessors of this.getATrueSuccessor() are either this or dominated by this.getATrueSuccessor().
For example, in the following python snippet:
<code>
if x:
controlled
false_successor
uncontrolled
</code>
false_successor dominates uncontrolled, but not all of its predecessors are this (if x)
or dominated by itself. Whereas in the following code:
<code>
if x:
while controlled:
also_controlled
false_successor
uncontrolled
</code>
the block 'while controlled' is controlled because all of its predecessors are this (if x)
or (in the case of 'also_controlled') dominated by itself.
The additional constraint on the predecessors of the test successor implies
that `this` strictly dominates `controlled` so that isn't necessary to check
directly.
*/
exists(UnprunedBasicBlock succ |
testIsTrue = true and succ = this.getATrueSuccessor()
or
testIsTrue = false and succ = this.getAFalseSuccessor()
|
succ.dominates(controlled) and
forall(UnprunedBasicBlock pred | pred.getASuccessor() = succ |
pred = this or succ.dominates(pred)
)
)
}
/** Holds if the edge `pred->succ` is reachable only if the test in this block evaluates to `testIsTrue` */
predicate controlsEdge(UnprunedBasicBlock pred, UnprunedBasicBlock succ, boolean testIsTrue) {
this.controls(pred, testIsTrue) and succ = pred.getASuccessor()
or
pred = this and (
testIsTrue = true and succ = this.getATrueSuccessor()
or
testIsTrue = false and succ = this.getAFalseSuccessor()
)
}
}
/** A constraint that the variable is truthy `bool(var) is True` or falsey `bool(var) is False` */
class Truthy extends Constraint, TTruthy {
private boolean booleanValue() {
this = TTruthy(result)
}
override string toString() {
result = "Truthy" and this.booleanValue() = true
or
result = "Falsey" and this.booleanValue() = false
}
override Constraint invert() {
result = TTruthy(this.booleanValue().booleanNot())
}
override predicate constrainsVariableToBe(boolean value) {
value = this.booleanValue()
}
override predicate cannotBeNone() {
this.booleanValue() = true
}
}
/** A constraint that the variable is None `(var is None) is True` or not None `(var is None) is False`.
* This includes the `is not` operator, `x is not None` being equivalent to `not x is None` */
class IsNone extends Constraint, TIsNone {
private boolean isNone() {
this = TIsNone(result)
}
override string toString() {
result = "Is None" and this.isNone() = true
or
result = "Is not None" and this.isNone() = false
}
override Constraint invert() {
result = TIsNone(this.isNone().booleanNot())
}
override predicate constrainsVariableToBe(boolean value) {
value = false and this.isNone() = true
}
override predicate cannotBeNone() {
this = TIsNone(false)
}
}
/** A constraint that the variable fulfils some equality or inequality to an integral constant.
* `(var op k) is True` where `op` is an equality or inequality operator and `k` is an integer constant
*/
class ConstrainedByConstant extends Constraint, TConstrainedByConstant {
private int intValue() {
this = TConstrainedByConstant(_, result)
}
private CompareOp getOp() {
this = TConstrainedByConstant(result, _)
}
override string toString() {
result = this.getOp().repr() + " " + this.intValue().toString()
}
override Constraint invert() {
result = TConstrainedByConstant(this.getOp().invert(), this.intValue())
}
override predicate constrainsVariableToBe(boolean value) {
this.getOp() = eq() and this.intValue() = 0 and value = false
or
value = true and (
this.getOp() = eq() and this.intValue() != 0
or
this.getOp() = lt() and this.intValue() <= 0
or
this.getOp() = le() and this.intValue() < 0
or
this.getOp() = gt() and this.intValue() >= 0
or
this.getOp() = ge() and this.intValue() > 0
)
}
predicate eq(int val) {
this = TConstrainedByConstant(eq(), val)
}
predicate ne(int val) {
this = TConstrainedByConstant(ne(), val)
}
override predicate cannotBeNone() {
this.getOp() = eq()
}
/** The minimum value that a variable fulfilling this constraint may hold
* within the bounds of a signed 32 bit number.
*/
int minValue() {
this.getOp() = eq() and result = this.intValue()
or
this.getOp() = lt() and result = -2147483648
or
this.getOp() = le() and result = -2147483648
or
this.getOp() = gt() and result = this.intValue()+1
or
this.getOp() = ge() and result = this.intValue()
}
/** The maximum value that a variable fulfilling this constraint may hold
* within the bounds of a signed 32 bit number.
*/
int maxValue() {
this.getOp() = eq() and result = this.intValue()
or
this.getOp() = gt() and result = 2147483647
or
this.getOp() = ge() and result = 2147483647
or
this.getOp() = lt() and result = this.intValue()-1
or
this.getOp() = le() and result = this.intValue()
}
}
/** Holds if the control flow node `n` is unreachable due to
* one or more constraints.
*/
predicate unreachable(UnprunedCfgNode n) {
exists(UnprunedBasicBlock bb |
unreachableBB(bb) and bb.contains(n)
)
}
predicate reachable(UnprunedCfgNode n) {
exists(UnprunedBasicBlock bb |
reachableBB(bb) and bb.contains(n)
)
}
/** Holds if the basic block `bb` is unreachable due to
* one or more constraints.
*/
predicate unreachableBB(UnprunedBasicBlock bb) {
not reachableBB(bb)
}
/** Holds if the basic block `bb` is reachable despite
* constraints
*/
predicate reachableBB(UnprunedBasicBlock bb) {
bb.isEntry() or
reachableEdge(_, bb)
}
Constraint constraintFromExpr(SsaVariable var, UnprunedCfgNode node) {
py_ssa_use(node, var) and result = TTruthy(true)
or
exists(boolean b |
none_test(node, var, b) and result = TIsNone(b)
)
or
exists(CompareOp op, int k |
int_test(node, var, op, k) and
result = TConstrainedByConstant(op, k)
)
or
result = constraintFromExpr(var, node.(UnprunedNot).getOperand()).invert()
}
Constraint constraintFromTest(SsaVariable var, UnprunedCfgNode node) {
result = constraintFromExpr(var, node) and node.isBranch()
}
predicate none_test(UnprunedCompareNode test, SsaVariable var, boolean is) {
exists(UnprunedCfgNode left, Cmpop op, UnprunedCfgNode right |
py_ssa_use(left, var) and
test.operands(left, op, right) and
right.getNode() instanceof None
|
op instanceof Is and is = true
or
op instanceof IsNot and is = false
)
}
predicate int_test(UnprunedCfgNode test, SsaVariable var, CompareOp op, int k) {
exists(UnprunedCfgNode left, UnprunedCfgNode right, Cmpop cop |
test.(UnprunedCompareNode).operands(left, cop, right)
|
op.forOp(cop) and
py_ssa_use(left, var) and
intValue(right.getNode()) = k
or
op.reverse().forOp(cop) and
py_ssa_use(right, var) and
intValue(left.getNode()) = k
)
}
private predicate constrainingValue(Expr e) {
exists(Assign a, UnprunedCfgNode asgn |
a.getValue() = e and a.getATarget() = asgn.getNode() and py_ssa_defn(_, asgn)
)
or
exists(UnaryExpr n | constrainingValue(n) and n.getOp() instanceof Not and e = n.getOperand())
}
private Constraint constraintFromValue(Expr e) {
constrainingValue(e) and
(
result = TConstrainedByConstant(eq(), intValue(e))
or
e instanceof True and result = TTruthy(true)
or
e instanceof False and result = TTruthy(false)
or
e instanceof None and result = TIsNone(true)
or
result = constraintFromValue(e.(UnaryExpr).getOperand()).invert()
)
}
/** Gets the constraint on `var` resulting from the assignment in `asgn` */
Constraint constraintFromAssignment(SsaVariable var, UnprunedCfgNode asgn) {
exists(Assign a |
a.getATarget() = asgn.getNode() and
py_ssa_defn(var, asgn) and
result = constraintFromValue(a.getValue())
)
or
module_import(asgn, var) and result = TTruthy(true)
}
/** Holds if the constraint `preval` holds for `var` on edge `pred` -> `succ` as a result of a prior test or assignment */
pragma [nomagic]
predicate priorConstraint(UnprunedBasicBlock pred, UnprunedBasicBlock succ, Constraint preval, SsaVariable var) {
not (blacklisted(var) and preval = TTruthy(_))
and
not var.getVariable().escapes()
and
exists(UnprunedBasicBlock first |
not first = pred and
first.(UnprunedConditionBlock).controlsEdge(pred, succ, true) and
preval = constraintFromTest(var, first.last())
or
not first = pred and
first.(UnprunedConditionBlock).controlsEdge(pred, succ, false) and
preval = constraintFromTest(var, first.last()).invert()
or
preval = constraintFromAssignment(var, first.getANode()) and
first.dominates(pred) and
(succ = pred.getAFalseSuccessor() or succ = pred.getATrueSuccessor())
)
}
/** Holds if `cond` holds for `var` on conditional edge `pred` -> `succ` as a result of the test for that edge */
pragma [nomagic]
predicate constraintOnBranch(UnprunedBasicBlock pred, UnprunedBasicBlock succ, Constraint cond, SsaVariable var) {
cond = constraintFromTest(var, pred.last()) and
succ = pred.getATrueSuccessor()
or
cond = constraintFromTest(var, pred.last()).invert() and
succ = pred.getAFalseSuccessor()
}
/** Holds if the pair of constraints (`preval`, `postcond`) holds on the edge `pred` -> `succ` for some SSA variable */
predicate controllingConditions(UnprunedBasicBlock pred, UnprunedBasicBlock succ, Constraint preval, Constraint postcond) {
exists(SsaVariable var |
priorConstraint(pred, succ, preval, var) and
constraintOnBranch(pred, succ, postcond, var)
)
}
/** Holds if the edge `pred` -> `succ` should be pruned as it cannot be reached */
predicate unreachableEdge(UnprunedCfgNode pred, UnprunedCfgNode succ) {
exists(UnprunedBasicBlock predBB, UnprunedBasicBlock succBB |
succBB = predBB.getASuccessor() and
not reachableEdge(predBB, succBB) and
pred = predBB.last() and succ = succBB.first()
)
}
/** Holds if the edge `pred` -> `succ` is reachable as a result of
* `pred` being reachable and this edge not being pruned. */
predicate reachableEdge(UnprunedBasicBlock pred, UnprunedBasicBlock succ) {
reachableBB(pred) and succ = pred.getASuccessor() and
not contradictoryEdge(pred, succ) and
not simplyDead(pred, succ)
}
predicate contradictoryEdge(UnprunedBasicBlock pred, UnprunedBasicBlock succ) {
exists(Constraint pre, Constraint cond |
controllingConditions(pred, succ, pre, cond) and
contradicts(pre, cond)
)
}
/* Helper for `contradictoryEdge`, deal with inequalities here to avoid blow up */
pragma [inline]
private predicate contradicts(Constraint a, Constraint b) {
a = TIsNone(true) and b.cannotBeNone()
or
a.cannotBeNone() and b = TIsNone(true)
or
a.constrainsVariableToBe(true) and b.constrainsVariableToBe(false)
or
a.constrainsVariableToBe(false) and b.constrainsVariableToBe(true)
or
a.(ConstrainedByConstant).minValue() > b.(ConstrainedByConstant).maxValue()
or
a.(ConstrainedByConstant).maxValue() < b.(ConstrainedByConstant).minValue()
or
exists(int val |
a.(ConstrainedByConstant).eq(val) and b.(ConstrainedByConstant).ne(val)
or
a.(ConstrainedByConstant).ne(val) and b.(ConstrainedByConstant).eq(val)
)
}
/** Holds if edge is simply dead. Stuff like `if False: ...` */
predicate simplyDead(UnprunedBasicBlock pred, UnprunedBasicBlock succ) {
constTest(pred.last()) = true and pred.getAFalseSuccessor() = succ
or
constTest(pred.last()) = false and pred.getATrueSuccessor() = succ
}
/* Helper for simplyDead */
private boolean constTest(UnprunedCfgNode node) {
exists(ImmutableLiteral lit |
result = lit.booleanValue() and lit = node.getNode()
)
or
result = constTest(node.(UnprunedNot).getOperand()).booleanNot()
}
/** Holds if `var` is blacklisted as having possibly been mutated */
predicate blacklisted(SsaVariable var) {
possibly_mutated(var) and not whitelisted(var)
}
predicate possibly_mutated(SsaVariable var) {
exists(Subscript subscr, UnprunedCfgNode node |
subscr.getObject() = node.getNode() and
py_ssa_use(node, var)
)
or
exists(Attribute attr, UnprunedCfgNode node |
attr.getObject() = node.getNode() and
py_ssa_use(node, var)
)
}
/** If SSA variable is defined by an import, then it should
* be whitelisted as taking an attribute cannot change its
* truthiness.
*/
predicate whitelisted(SsaVariable var) {
module_import(_, var)
}
private predicate module_import(UnprunedCfgNode asgn, SsaVariable var) {
exists(Alias alias |
alias.getValue() instanceof ImportExpr and
py_ssa_defn(var, asgn) and
alias.getAsname() = asgn.getNode()
)
}
}

View File

@@ -1,79 +0,0 @@
| 8 | test | test | Truthy | test |
| 10 | test | test | Truthy | test |
| 14 | seq | seq | Truthy | test |
| 17 | seq | seq | Truthy | test |
| 21 | UnaryExpr | t1 | Falsey | test |
| 24 | t1 | t1 | Truthy | test |
| 25 | t1 | t1 | Truthy | test |
| 26 | t2 | t2 | Truthy | test |
| 29 | t2 | t2 | Truthy | test |
| 30 | t2 | t2 | Truthy | test |
| 31 | t3 | t3 | Truthy | test |
| 31 | t4 | t4 | Truthy | test |
| 32 | t3 | t3 | Truthy | test |
| 33 | t3 | t3 | Truthy | test |
| 34 | t3 | t3 | Truthy | test |
| 35 | t4 | t4 | Truthy | test |
| 36 | t5 | t5 | Truthy | test |
| 36 | t6 | t6 | Truthy | test |
| 37 | t5 | t5 | Truthy | test |
| 38 | t5 | t5 | Truthy | test |
| 39 | t6 | t6 | Truthy | test |
| 40 | t6 | t6 | Truthy | test |
| 43 | t1 | t1 | Truthy | test |
| 44 | UnaryExpr | t2 | Falsey | test |
| 47 | t1 | t1 | Truthy | test |
| 48 | t2 | t2 | Truthy | test |
| 49 | t2 | t2 | Truthy | test |
| 51 | t2 | t2 | Truthy | test |
| 52 | t2 | t2 | Truthy | test |
| 55 | seq1 | seq1 | Truthy | test |
| 57 | UnaryExpr | seq2 | Falsey | test |
| 60 | seq1 | seq1 | Truthy | test |
| 63 | seq2 | seq2 | Truthy | test |
| 66 | seq3 | seq3 | Truthy | test |
| 68 | UnaryExpr | seq4 | Falsey | test |
| 88 | UnaryExpr | x | Falsey | test |
| 90 | y | y | Truthy | test |
| 93 | UnaryExpr | x | Falsey | test |
| 95 | y | y | Truthy | test |
| 99 | another_module | another_module | Truthy | assign |
| 102 | UnaryExpr | another_module | Falsey | test |
| 107 | UnaryExpr | t1 | Falsey | test |
| 109 | t2 | t2 | Truthy | test |
| 111 | t1 | t1 | Truthy | test |
| 113 | UnaryExpr | t2 | Falsey | test |
| 117 | UnaryExpr | test | Falsey | test |
| 119 | UnaryExpr | test | Falsey | test |
| 123 | m | m | Truthy | test |
| 126 | m | m | Truthy | test |
| 158 | Compare | ps | Is not None | test |
| 160 | Compare | ps | Is None | test |
| 172 | escapes | escapes | Is None | assign |
| 177 | Compare | escapes | Is None | test |
| 191 | true12 | true12 | == 0 | assign |
| 195 | Compare | x | < 4 | test |
| 197 | Compare | x | < 4 | test |
| 201 | Compare | x | < 4 | test |
| 203 | UnaryExpr | x | < 4 | test |
| 207 | Compare | x | < 4 | test |
| 209 | Compare | x | < 4 | test |
| 215 | x | x | Truthy | test |
| 215 | y | y | Truthy | test |
| 217 | x | x | Truthy | test |
| 217 | y | y | Truthy | test |
| 219 | x | x | Truthy | test |
| 223 | y | y | Truthy | test |
| 229 | k | k | Falsey | assign |
| 230 | k | k | Truthy | test |
| 237 | k | k | == 3 | assign |
| 238 | k | k | Truthy | test |
| 245 | k | k | Is None | assign |
| 246 | k | k | Truthy | test |
| 253 | a | a | Truthy | test |
| 254 | k | k | Truthy | assign |
| 256 | k | k | Falsey | assign |
| 257 | k | k | Truthy | test |
| 264 | var | var | Truthy | assign |
| 266 | var | var | Falsey | assign |
| 267 | var | var | Truthy | test |

View File

@@ -1,14 +0,0 @@
import python
import semmle.python.Pruning
from Pruner::Constraint c, SsaVariable var, Pruner::UnprunedCfgNode node, int line, string kind
where line = node.getNode().getLocation().getStartLine() and line > 0 and
(
c = Pruner::constraintFromTest(var, node) and kind = "test"
or
c = Pruner::constraintFromAssignment(var, node) and kind = "assign"
)
select line, node.getNode().toString(), var.getId(), c, kind

View File

@@ -1,40 +0,0 @@
| 10 | test | 11 | count |
| 24 | t1 | 24 | count |
| 25 | t1 | 26 | t2 |
| 29 | t2 | 30 | BoolExpr |
| 30 | t2 | 30 | count |
| 37 | t5 | 37 | count |
| 38 | t5 | 39 | BoolExpr |
| 39 | t6 | 39 | count |
| 40 | t6 | 20 | Function boolop |
| 47 | t1 | 48 | BoolExpr |
| 47 | t1 | 51 | BoolExpr |
| 48 | t2 | 48 | count |
| 49 | t2 | 42 | Function with_splitting |
| 51 | t2 | 51 | count |
| 52 | t2 | 42 | Function with_splitting |
| 93 | UnaryExpr | 94 | count |
| 95 | y | 96 | count |
| 102 | UnaryExpr | 103 | count |
| 111 | t1 | 113 | t2 |
| 113 | UnaryExpr | 106 | Function negated_conditional_live |
| 119 | UnaryExpr | 120 | count |
| 160 | Compare | 161 | count |
| 160 | Compare | 163 | count |
| 197 | Compare | 198 | count |
| 203 | UnaryExpr | 204 | count |
| 209 | Compare | 210 | count |
| 217 | x | 217 | UnaryExpr |
| 217 | x | 217 | y |
| 217 | y | 217 | UnaryExpr |
| 219 | x | 220 | count |
| 219 | x | 222 | count |
| 223 | y | 224 | count |
| 223 | y | 226 | count |
| 230 | k | 231 | count |
| 238 | k | 241 | count |
| 246 | k | 247 | count |
| 257 | k | 258 | count |
| 257 | k | 259 | Pass |
| 267 | var | 268 | count |
| 267 | var | 269 | Pass |

View File

@@ -1,12 +0,0 @@
import python
import semmle.python.Pruning
from Pruner::UnprunedBasicBlock pred, Pruner::UnprunedBasicBlock succ, int line1, int line2
where Pruner::contradictoryEdge(pred, succ) and
line1 = pred.last().getNode().getLocation().getStartLine() and
line2 = succ.first().getNode().getLocation().getStartLine() and
line1 > 0
select line1, pred.last().getNode().toString(), line2, succ.first().getNode().toString()

View File

@@ -1,95 +0,0 @@
| 10 | test | 11 | count |
| 11 | count | 7 | Function conditional_dead |
| 24 | count | 25 | BoolExpr |
| 24 | t1 | 24 | count |
| 25 | t1 | 26 | t2 |
| 29 | t2 | 30 | BoolExpr |
| 30 | count | 31 | BoolExpr |
| 30 | t2 | 30 | count |
| 37 | count | 38 | BoolExpr |
| 37 | t5 | 37 | count |
| 38 | t5 | 39 | BoolExpr |
| 39 | count | 40 | BoolExpr |
| 39 | t6 | 39 | count |
| 40 | t6 | 20 | Function boolop |
| 47 | t1 | 48 | BoolExpr |
| 47 | t1 | 51 | BoolExpr |
| 48 | count | 49 | BoolExpr |
| 48 | t2 | 48 | count |
| 48 | t2 | 49 | BoolExpr |
| 49 | count | 42 | Function with_splitting |
| 49 | t2 | 42 | Function with_splitting |
| 49 | t2 | 49 | count |
| 51 | count | 52 | BoolExpr |
| 51 | t2 | 51 | count |
| 51 | t2 | 52 | BoolExpr |
| 52 | count | 42 | Function with_splitting |
| 52 | t2 | 42 | Function with_splitting |
| 52 | t2 | 52 | count |
| 93 | UnaryExpr | 94 | count |
| 94 | count | 95 | y |
| 95 | y | 96 | count |
| 96 | count | 99 | ImportExpr |
| 102 | UnaryExpr | 103 | count |
| 103 | count | 106 | FunctionExpr |
| 111 | t1 | 113 | t2 |
| 113 | UnaryExpr | 106 | Function negated_conditional_live |
| 119 | UnaryExpr | 120 | count |
| 120 | count | 116 | Function negated_conditional_dead |
| 130 | None | 131 | count |
| 132 | UnaryExpr | 133 | count |
| 132 | UnaryExpr | 134 | False |
| 133 | count | 134 | False |
| 134 | False | 135 | count |
| 134 | False | 137 | count |
| 138 | True | 139 | count |
| 138 | True | 141 | count |
| 139 | count | 142 | IntegerLiteral |
| 141 | count | 142 | IntegerLiteral |
| 142 | IntegerLiteral | 143 | count |
| 142 | IntegerLiteral | 145 | count |
| 143 | count | 146 | IntegerLiteral |
| 145 | count | 146 | IntegerLiteral |
| 146 | UnaryExpr | 147 | count |
| 146 | UnaryExpr | 149 | count |
| 147 | count | 151 | False |
| 149 | count | 151 | False |
| 151 | UnaryExpr | 152 | count |
| 151 | UnaryExpr | 153 | False |
| 152 | count | 153 | False |
| 153 | UnaryExpr | 129 | Function prune_const_branches |
| 153 | UnaryExpr | 154 | count |
| 154 | count | 129 | Function prune_const_branches |
| 160 | Compare | 161 | count |
| 160 | Compare | 163 | count |
| 161 | count | 157 | Function attribute_lookup_cannot_effect_comparisons_with_immutable_constants |
| 163 | count | 157 | Function attribute_lookup_cannot_effect_comparisons_with_immutable_constants |
| 197 | Compare | 198 | count |
| 198 | count | 194 | Function inequality1 |
| 203 | UnaryExpr | 204 | count |
| 204 | count | 200 | Function inequality2 |
| 209 | Compare | 210 | count |
| 210 | count | 206 | Function reversed_inequality |
| 217 | x | 217 | UnaryExpr |
| 217 | x | 217 | y |
| 217 | y | 217 | UnaryExpr |
| 219 | x | 220 | count |
| 219 | x | 222 | count |
| 220 | count | 223 | y |
| 222 | count | 223 | y |
| 223 | y | 224 | count |
| 223 | y | 226 | count |
| 224 | count | 214 | Function split_bool1 |
| 226 | count | 214 | Function split_bool1 |
| 230 | k | 231 | count |
| 231 | count | 234 | Pass |
| 238 | k | 241 | count |
| 241 | count | 242 | Pass |
| 246 | k | 247 | count |
| 247 | count | 250 | Pass |
| 257 | k | 258 | count |
| 257 | k | 259 | Pass |
| 258 | count | 259 | Pass |
| 267 | var | 268 | count |
| 267 | var | 269 | Pass |
| 268 | count | 269 | Pass |

View File

@@ -1,12 +0,0 @@
import python
import semmle.python.Pruning
from Pruner::UnprunedCfgNode pred, Pruner::UnprunedCfgNode succ, int line1, int line2
where Pruner::unreachableEdge(pred, succ) and
line1 = pred.getNode().getLocation().getStartLine() and
line2 = succ.getNode().getLocation().getStartLine() and
line1 > 0
select line1, pred.getNode().toString(), line2, succ.getNode().toString()

View File

@@ -1,8 +0,0 @@
| 130 | None | 131 | count |
| 132 | UnaryExpr | 134 | False |
| 134 | False | 135 | count |
| 138 | True | 141 | count |
| 142 | IntegerLiteral | 143 | count |
| 146 | UnaryExpr | 149 | count |
| 151 | UnaryExpr | 152 | count |
| 153 | UnaryExpr | 129 | Function prune_const_branches |

View File

@@ -1,12 +0,0 @@
import python
import semmle.python.Pruning
from Pruner::UnprunedBasicBlock pred, Pruner::UnprunedBasicBlock succ, int line1, int line2
where Pruner::simplyDead(pred, succ) and
line1 = pred.last().getNode().getLocation().getStartLine() and
line2 = succ.first().getNode().getLocation().getStartLine() and
line1 > 0
select line1, pred.last().getNode().toString(), line2, succ.first().getNode().toString()

View File

@@ -1,2 +0,0 @@
semmle-extractor-options: --dont-prune-graph
optimize: true

View File

@@ -1,64 +0,0 @@
| 5 | 0 |
| 11 | 0 |
| 18 | 1 |
| 24 | 0 |
| 25 | 1 |
| 29 | 1 |
| 30 | 0 |
| 32 | 1 |
| 33 | 1 |
| 34 | 1 |
| 35 | 1 |
| 37 | 0 |
| 38 | 1 |
| 39 | 0 |
| 40 | 1 |
| 48 | 0 |
| 49 | 1 |
| 51 | 1 |
| 52 | 1 |
| 61 | 1 |
| 64 | 1 |
| 94 | 0 |
| 96 | 0 |
| 103 | 0 |
| 112 | 1 |
| 114 | 1 |
| 120 | 0 |
| 127 | 1 |
| 131 | 0 |
| 133 | 1 |
| 135 | 0 |
| 137 | 1 |
| 139 | 1 |
| 141 | 0 |
| 143 | 0 |
| 145 | 1 |
| 147 | 1 |
| 149 | 0 |
| 152 | 0 |
| 154 | 1 |
| 161 | 1 |
| 163 | 1 |
| 176 | 1 |
| 178 | 1 |
| 180 | 1 |
| 184 | 1 |
| 186 | 1 |
| 189 | 1 |
| 192 | 1 |
| 198 | 0 |
| 204 | 0 |
| 210 | 0 |
| 220 | 1 |
| 222 | 1 |
| 224 | 1 |
| 226 | 1 |
| 231 | 0 |
| 233 | 1 |
| 239 | 1 |
| 241 | 0 |
| 247 | 0 |
| 249 | 1 |
| 258 | 1 |
| 268 | 1 |

View File

@@ -1,269 +0,0 @@
#Test number of CFG nodes for each use of 'count'
def dead():
return 0
count
def conditional_dead(test):
if test:
return
if test:
count
def made_true(seq):
if seq:
return
seq.append(1)
if seq:
count
def boolop(t1, t2, t3, t4, t5, t6):
if not t1:
return
#bool(t1) must be True
t1 or count
t1 and count
if t2:
return
#bool(t2) must be False
t2 or count
t2 and count
if t3 or t4:
t3 or count
t3 and count
t3 or count
t4 and count
if t5 and t6:
t5 or count
t5 and count
t6 or count
t6 and count
def with_splitting(t1, t2):
if t1:
if not t2:
return
#Cannot have bool(t1) be True and bool(t2) be False
if t1:
t2 or count #Unreachable
t2 and count
else:
t2 or count
t2 and count
def loops(seq1, seq2, seq3, seq4, seq5):
if seq1:
return
if not seq2:
return
#bool(seq1) is False; bool(seq2) is True
while seq1:
count #This is unreachable, but the pop below forces us to be conservative.
seq1.pop()
while seq2:
count
seq2.pop()
if seq3:
return
if not seq4:
return
#bool(seq3) is False; bool(seq4) is True
#for var in seq3:
# count #This is unreachable, but we cannot infer this yet.
# print(var)
#for var in seq4:
# count
# print(var)
##seq5 false then made true
#if seq5:
# return
#seq5.append(1)
#for var in seq5:
# count
# print(var)
#Logic does not apply to global variables in calls,
#as they may be changed from true to false externally.
from some_module import x, y
if not x:
raise Exception()
if y:
raise Exception()
make_a_call()
if not x:
count
if y:
count
# However, modules are always true -- Which is important.
import another_module
make_a_call()
if not another_module:
count
def negated_conditional_live(t1, t2):
if not t1:
return
if t2:
return
if t1:
count
if not t2:
count
def negated_conditional_dead(test):
if not test:
return
if not test:
count
def made_true2(m):
if m:
return
del m['a']
if m:
count
def prune_const_branches():
if None:
count
if not None:
count
if False:
count
else:
count
if True:
count
else:
count
if 0:
count
else:
count
if -4:
count
else:
count
#Muliptle nots
if not not False:
count
if not not not False:
count
#ODASA-6794
def attribute_lookup_cannot_effect_comparisons_with_immutable_constants(ps):
if ps is not None:
ps_clamped = ps.clamp()
if ps is None:
count
else:
count
def func():
global escapes
so_something()
escapes = True
#Don't prune on `escapes` as it escapes.
if __name__ == '__main__':
escapes = None # global
try:
func()
except Exception as err:
count
if escapes is None:
count
else:
count
def func2():
while 1:
count
if cond12:
count
try:
true12()
count
except IOError:
true12 = 0
count
def inequality1(x):
if x < 4:
return
if x < 4:
count
def inequality2(x):
if x < 4:
return
if not x >= 4:
count
def reversed_inequality(x):
if x < 4:
return
if 4 > x:
count
#Splittings with boolean expressions:
def split_bool1(x=None,y=None):
if x and y:
raise
if not (x or y):
raise
if x:
count
else:
count
if y:
count
else:
count
def prune_on_constant1():
k = False
if k:
count
else:
count
pass
def prune_on_constant2():
k = 3
if k:
count
else:
count
pass
def prune_on_constant3():
k = None
if k:
count
else:
count
pass
def prune_on_constant_in_test(a, b):
if a:
k = True
else:
k = False
if k:
count
pass
def prune_on_constant_in_try():
try:
import foo
var = True
except:
var = False
if var:
count
pass

View File

@@ -1,5 +0,0 @@
import python
from Name n
where n.getId() = "count"
select n.getLocation().getStartLine(), count(n.getAFlowNode())

View File

@@ -1,2 +1,2 @@
semmle-extractor-options: --max-import-depth=3 --dont-prune-graph
semmle-extractor-options: --max-import-depth=3
optimize: true

View File

@@ -1,2 +1,2 @@
semmle-extractor-options: --max-import-depth=4 --dont-prune-graph
semmle-extractor-options: --max-import-depth=4
optimize: true