Merge pull request #1484 from markshannon/python-aggressive-pruning

Python: Use aggressive dead-code elimination when pruning.
2019-06-25 19:17:44 +02:00 · 2019-06-25 19:17:44 +02:00 · 76f8da8986
--- a/python/ql/src/semmle/python/Flow.qll
+++ b/python/ql/src/semmle/python/Flow.qll
@ -34,7 +34,7 @@ private AstNode toAst(ControlFlowNode n) {
 class ControlFlowNode extends @py_flow_node {

    cached ControlFlowNode() {
-        not Pruner::unreachable(this)
+        Pruner::reachable(this)
    }

    /** Whether this control flow node is a load (including those in augmented assignments) */
@ -175,12 +175,13 @@ class ControlFlowNode extends @py_flow_node {

    /** Gets a predecessor of this flow node */
    ControlFlowNode getAPredecessor() {
-        py_successors(result, this)
+        this = result.getASuccessor()
    }

    /** Gets a successor of this flow node */
    ControlFlowNode getASuccessor() {
-        py_successors(this, result)
+        py_successors(this, result) and
+        not Pruner::unreachableEdge(this, result)
    }

    /** Gets the immediate dominator of this flow node */
@ -291,22 +292,25 @@ class ControlFlowNode extends @py_flow_node {

    /** Gets a successor for this node if the relevant condition is True. */
    ControlFlowNode getATrueSuccessor() {
+        result = this.getASuccessor() and
        py_true_successors(this, result)
    }

    /** Gets a successor for this node if the relevant condition is False. */
    ControlFlowNode getAFalseSuccessor() {
+        result = this.getASuccessor() and
        py_false_successors(this, result)
    }

    /** Gets a successor for this node if an exception is raised. */
    ControlFlowNode getAnExceptionalSuccessor() {
+        result = this.getASuccessor() and
        py_exception_successors(this, result)
    }

    /** Gets a successor for this node if no exception is raised. */
    ControlFlowNode getANormalSuccessor() {
-        py_successors(this, result) and not
+        result = this.getASuccessor() and not
        py_exception_successors(this, result)
    }

@ -946,21 +950,91 @@ predicate defined_by(NameNode def, Variable v) {
    exists(NameNode p | defined_by(p, v) and p.getASuccessor() = def and not p.defines(v))
 }

-/** A basic block (ignoring exceptional flow edges to scope exit) */
-class BasicBlock extends @py_flow_node {
+/* Combine extractor-generated basic block after pruning */

-    BasicBlock() {
-        py_flow_bb_node(_, _, this, _)
+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()
+        )
    }

-    /** Whether this basic block contains the specified node */
    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
+    }
+
+    /** Whether this basic block contains the specified node */
+    predicate contains(ControlFlowNode node) {
+        this.getAPart().contains(node)
+    }
+
    /** Gets the nth node in this basic block */
    ControlFlowNode getNode(int n) {
-        py_flow_bb_node(result, _, this, n)
+        exists(BasicBlockPart part |
+            part = this.getAPart() and
+            n = part.startIndex() + part.indexOf(result)
+        )
    }

    string toString() {
@ -980,7 +1054,7 @@ class BasicBlock extends @py_flow_node {
    }

    BasicBlock getImmediateDominator() {
-        this.firstNode().getImmediateDominator().getBasicBlock() = result
+        this.getAPart().getImmediateDominator() = result.getAPart()
    }

    /** Dominance frontier of a node x is the set of all nodes `other` such that `this` dominates a predecessor
@ -996,9 +1070,10 @@ class BasicBlock extends @py_flow_node {

    /** Gets the last node in this basic block */
    ControlFlowNode getLastNode() {
-        exists(int i |
-            this.getNode(i) = result and
-            i = max(int j | py_flow_bb_node(_, _, this, j))
+        exists(BasicBlockPart part |
+            part = this.getAPart() and
+            part.isLast() and
+            result = part.lastNode()
        )
    }

--- a/python/ql/src/semmle/python/Pruning.qll
+++ b/python/ql/src/semmle/python/Pruning.qll
@ -396,16 +396,25 @@ module Pruner {
        )
    }

+    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 bb.isEntry() and
-        forall(UnprunedBasicBlock pred |
-            pred.getASuccessor() = bb
-            |
-            unreachableEdge(pred, bb)
-        )
+        not reachableBB(bb)
+    }
+
+    /** Holds if the basic block `bb` is reachable despite
+     * constraints
+     */
+    predicate reachableBB(UnprunedBasicBlock bb) {
+        bb.isEntry() or
+        reachableEdge(_, bb)
    }

    Constraint constraintFromTest(SsaVariable var, UnprunedCfgNode node) {
@ -533,18 +542,30 @@ module Pruner {
    }

    /** Holds if the edge `pred` -> `succ` should be pruned as it cannot be reached */
-    predicate unreachableEdge(UnprunedBasicBlock pred, UnprunedBasicBlock succ) {
+    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)
        )
-        or
-        unreachableBB(pred) and succ = pred.getASuccessor()
-        or
-        simply_dead(pred, succ)
    }

-    /* Helper for `unreachableEdge`, deal with inequalities here to avoid blow up */
+    /* 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()
@ -567,13 +588,13 @@ module Pruner {
    }

    /** Holds if edge is simply dead. Stuff like `if False: ...` */
-    predicate simply_dead(UnprunedBasicBlock pred, UnprunedBasicBlock succ) {
+    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 simply_dead */
+    /* Helper for simplyDead */
    private boolean constTest(UnprunedCfgNode node) {
        exists(ImmutableLiteral lit |
            result = lit.booleanValue() and lit = node.getNode()
--- a/python/ql/test/library-tests/ControlFlow/pruning/Constraint.expected
+++ b/python/ql/test/library-tests/ControlFlow/pruning/Constraint.expected
@ -105,3 +105,10 @@
 | 207 | x | x | Truthy |
 | 209 | Compare | x | < 4 |
 | 209 | x | x | Truthy |
+| 214 | None | None | Truthy |
+| 215 | x | x | Truthy |
+| 215 | y | y | Truthy |
+| 217 | x | x | Truthy |
+| 217 | y | y | Truthy |
+| 219 | x | x | Truthy |
+| 223 | y | y | Truthy |
--- a/python/ql/test/library-tests/ControlFlow/pruning/ContradictoryEdge.expected
+++ b/python/ql/test/library-tests/ControlFlow/pruning/ContradictoryEdge.expected
@ -0,0 +1,33 @@
+| 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 |
--- a/python/ql/test/library-tests/ControlFlow/pruning/ContradictoryEdge.ql
+++ b/python/ql/test/library-tests/ControlFlow/pruning/ContradictoryEdge.ql
@ -0,0 +1,12 @@
+
+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()
+
--- a/python/ql/test/library-tests/ControlFlow/pruning/Pruned.expected
+++ b/python/ql/test/library-tests/ControlFlow/pruning/Pruned.expected
@ -0,0 +1,83 @@
+| 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 |
--- a/python/ql/test/library-tests/ControlFlow/pruning/Pruned.ql
+++ b/python/ql/test/library-tests/ControlFlow/pruning/Pruned.ql
@ -0,0 +1,12 @@
+
+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()
+
--- a/python/ql/test/library-tests/ControlFlow/pruning/SimpleDead.expected
+++ b/python/ql/test/library-tests/ControlFlow/pruning/SimpleDead.expected
@ -0,0 +1,8 @@
+| 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 |
--- a/python/ql/test/library-tests/ControlFlow/pruning/SimpleDead.ql
+++ b/python/ql/test/library-tests/ControlFlow/pruning/SimpleDead.ql
@ -0,0 +1,12 @@
+
+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()
+
--- a/python/ql/test/library-tests/ControlFlow/pruning/test.expected
+++ b/python/ql/test/library-tests/ControlFlow/pruning/test.expected
@ -53,3 +53,7 @@
 | 198 | 0 |
 | 204 | 0 |
 | 210 | 0 |
+| 220 | 1 |
+| 222 | 1 |
+| 224 | 1 |
+| 226 | 1 |
--- a/python/ql/test/library-tests/ControlFlow/pruning/test.py
+++ b/python/ql/test/library-tests/ControlFlow/pruning/test.py
@ -209,3 +209,18 @@ def reversed_inequality(x):
    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
--- a/python/ql/test/library-tests/PointsTo/guarded/options
+++ b/python/ql/test/library-tests/PointsTo/guarded/options
@ -1,2 +1,2 @@
-semmle-extractor-options: --max-import-depth=3
+semmle-extractor-options: --max-import-depth=3 --dont-prune-graph
 optimize: true
--- a/python/ql/test/library-tests/PointsTo/new/options
+++ b/python/ql/test/library-tests/PointsTo/new/options
@ -1,2 +1,2 @@
-semmle-extractor-options: --max-import-depth=4
+semmle-extractor-options: --max-import-depth=4 --dont-prune-graph
 optimize: true