Merge pull request #604 from markshannon/python-faster-essa-computation

Python : Speed up ESSA computation

Author: taus-semmle

python/ql/src/semmle/dataflow/SSA.qll

@@ -154,6 +154,8 @@ private string location_string(EssaVariable v) {
         |
         def = TEssaNodeDefinition(_, b, index)
         or
+        def = TEssaNodeRefinement(_, b, index)
+        or
         def = TEssaEdgeDefinition(_, _, b) and index = piIndex()
         or
         def = TPhiFunction(_, b) and index = phiIndex()
@@ -177,7 +179,11 @@ private int var_rank(EssaVariable v) {
 /** Underlying IPA type for EssaDefinition and EssaVariable. */
 private cached newtype TEssaDefinition =
     TEssaNodeDefinition(SsaSourceVariable v, BasicBlock b, int i) {
-        EssaDefinitions::variableUpdate(v, _, b, _, i)
+        EssaDefinitions::variableDefinition(v, _, b, _, i)
+    }
+    or
+    TEssaNodeRefinement(SsaSourceVariable v, BasicBlock b, int i) {
+        EssaDefinitions::variableRefinement(v, _, b, _, i)
     }
     or
     TEssaEdgeDefinition(SsaSourceVariable v, BasicBlock pred, BasicBlock succ) {
@@ -446,21 +452,15 @@ class PhiFunction extends EssaDefinition, TPhiFunction {
     }
 }
 
-library class EssaNode extends EssaDefinition, TEssaNodeDefinition {
+/** A definition of an ESSA variable that is not directly linked to
+ * another ESSA variable.
+ */
+class EssaNodeDefinition extends EssaDefinition, TEssaNodeDefinition {
 
     override string toString() {
         result = "Essa node definition"
     }
 
-    /** Gets the ControlFlowNode corresponding to this definition */
-    ControlFlowNode getDefiningNode() {
-        this.definedBy(_, result)
-    }
-
-    override Location getLocation() {
-        result = this.getDefiningNode().getLocation()
-    }
-
     override ControlFlowNode getAUse() {
         exists(SsaSourceVariable v, BasicBlock b, int i |
             this = TEssaNodeDefinition(v, b, i) and
@@ -479,6 +479,15 @@ library class EssaNode extends EssaDefinition, TEssaNodeDefinition {
         this = TEssaNodeDefinition(result, _, _)
     }
 
+    /** Gets the ControlFlowNode corresponding to this definition */
+    ControlFlowNode getDefiningNode() {
+        this.definedBy(_, result)
+    }
+
+    override Location getLocation() {
+        result = this.getDefiningNode().getLocation()
+    }
+
     override string getRepresentation() {
         result = this.getDefiningNode().toString()
     }
@@ -501,27 +510,9 @@ library class EssaNode extends EssaDefinition, TEssaNodeDefinition {
 
 }
 
-/** A definition of an ESSA variable that is not directly linked to
- * another ESSA variable.
- */
-class EssaNodeDefinition extends EssaNode {
-
-    EssaNodeDefinition() {
-        this.getSourceVariable().hasDefiningNode(this.getDefiningNode())
-    }
-
-}
-
 /** A definition of an ESSA variable that takes another ESSA variable as an input.
  */
-class EssaNodeRefinement extends EssaNode {
-
-    EssaNodeRefinement() {
-        exists(SsaSourceVariable v, ControlFlowNode def |
-            this.definedBy(v, def) and
-            v.hasRefinement(_, def)
-        )
-    }
+class EssaNodeRefinement extends EssaDefinition, TEssaNodeRefinement {
 
     override string toString() {
         result = "SSA filter definition"
@@ -533,22 +524,62 @@ class EssaNodeRefinement extends EssaNode {
         not result = potential_input(potential_input(this).getDefinition())
     }
 
+    override ControlFlowNode getAUse() {
+        exists(SsaSourceVariable v, BasicBlock b, int i |
+            this = TEssaNodeRefinement(v, b, i) and
+            SsaDefinitions::reachesUse(v, b, i, result)
+        )
+    }
+
+    override predicate reachesEndOfBlock(BasicBlock b) {
+        exists(BasicBlock defb, int i |
+            this = TEssaNodeRefinement(_, defb, i) and
+            SsaDefinitions::reachesEndOfBlock(this.getSourceVariable(), defb, i, b)
+        )
+    }
+
+    override SsaSourceVariable getSourceVariable() {
+        this = TEssaNodeRefinement(result, _, _)
+    }
+
+    /** Gets the ControlFlowNode corresponding to this definition */
+    ControlFlowNode getDefiningNode() {
+        this.definedBy(_, result)
+    }
+
+    override Location getLocation() {
+        result = this.getDefiningNode().getLocation()
+    }
+
     override string getRepresentation() {
         result = this.getAQlClass() + "(" + this.getInput().getRepresentation() + ")"
     }
 
+    override Scope getScope() {
+        exists(BasicBlock defb |
+            this = TEssaNodeRefinement(_, defb, _) and
+            result = defb.getScope()
+        )
+    }
+
+    predicate definedBy(SsaSourceVariable v, ControlFlowNode def) {
+        exists(BasicBlock b, int i |
+            def = b.getNode(i) |
+            this = TEssaNodeRefinement(v, b, i+i)
+            or
+            this = TEssaNodeRefinement(v, b, i+i+1)
+        )
+    }
+
 }
 
 pragma[noopt]
 private EssaVariable potential_input(EssaNodeRefinement ref) {
-   exists(EssaNode node, ControlFlowNode use, SsaSourceVariable var, ControlFlowNode def |
+   exists(ControlFlowNode use, SsaSourceVariable var, ControlFlowNode def |
         var.hasRefinement(use, def) and
         use = result.getAUse() and
         var = result.getSourceVariable() and
-        def = node.getDefiningNode() and
-        var = node.getSourceVariable() and
-        ref = (EssaNodeRefinement)node
+        def = ref.getDefiningNode() and
+        var = ref.getSourceVariable()
     )
 }
-
-

python/ql/src/semmle/dataflow/SsaCompute.qll

@@ -99,8 +99,19 @@ private cached module SsaComputeImpl {
     cached module EssaDefinitionsImpl {
 
         /** Whether `n` is a live update that is a definition of the variable `v`. */
-        cached predicate variableUpdate(SsaSourceVariable v, ControlFlowNode n, BasicBlock b, int rankix, int i) {
-            SsaComputeImpl::variableDef(v, n, b, i) and
+        cached predicate variableDefinition(SsaSourceVariable v, ControlFlowNode n, BasicBlock b, int rankix, int i) {
+            SsaComputeImpl::variableDefine(v, n, b, i) and
+            SsaComputeImpl::defUseRank(v, b, rankix, i) and
+           (
+                SsaComputeImpl::defUseRank(v, b, rankix+1, _) and not SsaComputeImpl::defRank(v, b, rankix+1, _)
+                or
+                not SsaComputeImpl::defUseRank(v, b, rankix+1, _) and Liveness::liveAtExit(v, b)
+            )
+        }
+
+        /** Whether `n` is a live update that is a definition of the variable `v`. */
+        cached predicate variableRefinement(SsaSourceVariable v, ControlFlowNode n, BasicBlock b, int rankix, int i) {
+            SsaComputeImpl::variableRefine(v, n, b, i) and
             SsaComputeImpl::defUseRank(v, b, rankix, i) and
            (
                 SsaComputeImpl::defUseRank(v, b, rankix+1, _) and not SsaComputeImpl::defRank(v, b, rankix+1, _)
@@ -109,6 +120,12 @@ private cached module SsaComputeImpl {
             )
         }
 
+        cached predicate variableUpdate(SsaSourceVariable v, ControlFlowNode n, BasicBlock b, int rankix, int i) {
+            variableDefinition(v, n, b, rankix, i)
+            or
+            variableRefinement(v, n, b, rankix, i)
+        }
+
         /** Holds if `def` is a pi-node for `v` on the edge `pred` -> `succ` */
         cached predicate piNode(SsaSourceVariable v, BasicBlock pred, BasicBlock succ) {
             v.hasRefinementEdge(_, pred, succ) and
@@ -128,15 +145,28 @@ private cached module SsaComputeImpl {
         }
     }
 
-    cached predicate variableDef(SsaSourceVariable v, ControlFlowNode n, BasicBlock b, int i) {
-        (v.hasDefiningNode(n) or v.hasRefinement(_, n))
+    cached predicate variableDefine(SsaSourceVariable v, ControlFlowNode n, BasicBlock b, int i) {
+        v.hasDefiningNode(n)
+        and
+        exists(int j |
+            n = b.getNode(j) and
+            i = j*2 + 1
+        )
+    }
+
+    cached predicate variableRefine(SsaSourceVariable v, ControlFlowNode n, BasicBlock b, int i) {
+        v.hasRefinement(_, n)
         and
         exists(int j |
-            n = b.getNode(j) and 
+            n = b.getNode(j) and
             i = j*2 + 1
         )
     }
 
+    cached predicate variableDef(SsaSourceVariable v, ControlFlowNode n, BasicBlock b, int i) {
+        variableDefine(v, n, b, i) or variableRefine(v, n, b, i)
+    }
+
     /**
      * A ranking of the indices `i` at which there is an SSA definition or use of
      * `v` in the basic block `b`.

python/ql/src/semmle/python/pointsto/Base.qll

@@ -202,10 +202,6 @@ predicate function_can_never_return(FunctionObject func) {
 /** Python specific sub-class of generic EssaNodeDefinition */
 class PyNodeDefinition extends EssaNodeDefinition {
 
-    PyNodeDefinition() {
-        this.getSourceVariable().hasDefiningNode(this.getDefiningNode())
-    }
-
     override string getRepresentation() {
         result = this.getAQlClass()
     }

python/ql/src/semmle/python/security/TaintTracking.qll

@@ -416,7 +416,7 @@ abstract class TaintSource extends @py_flow_node {
  * Users of the taint tracking library can override this
  * class to provide their own sources on the ESSA graph.
  */
-abstract class TaintedDefinition extends EssaNode {
+abstract class TaintedDefinition extends EssaNodeDefinition {
 
     /**
      * Holds if `this` is a source of taint kind `kind`
@@ -1067,7 +1067,9 @@ library module TaintFlowImplementation {
                 not exists(Sanitizer san |
                     san.sanitizingDefinition(kind, def)
                     or
-                    san.sanitizingNode(kind, def.(EssaNode).getDefiningNode())
+                    san.sanitizingNode(kind, def.(EssaNodeDefinition).getDefiningNode())
+                    or
+                    san.sanitizingNode(kind, def.(EssaNodeRefinement).getDefiningNode())
                 )
             )
         )