Merge pull request #1717 from hvitved/csharp/ssa/adjacent-perf

C#: Improve performance of SSA adjacent reads calculation

Author: calumgrant

csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll

@@ -1058,8 +1058,10 @@ module Internal {
       conditionalAssign(guard, vGuard, def, vDef.getAnExpr())
     }
 
-    private predicate relevantEq(PreSsa::Definition def, AbstractValue v) {
-      conditionalAssignVal(_, _, def, v)
+    pragma[noinline]
+    private predicate relevantEq(PreSsa::Definition def, AbstractValue v, AssignableRead ar) {
+      conditionalAssignVal(_, _, def, v) and
+      ar = def.getARead()
     }
 
     /**
@@ -1156,8 +1158,7 @@ module Internal {
     private predicate guardImpliesNotEqual(
       Expr guard, AbstractValue vGuard, PreSsa::Definition def, AbstractValue vDef
     ) {
-      relevantEq(def, vDef) and
-      exists(AssignableRead ar | ar = def.getARead() |
+      exists(AssignableRead ar | relevantEq(def, vDef, ar) |
         // For example:
         //   if (de == null); vGuard = TBooleanValue(false); vDef = TNullValue(true)
         // but not

csharp/ql/src/semmle/code/csharp/controlflow/internal/PreSsa.qll

@@ -265,89 +265,97 @@ private int maxSsaRefRank(PreBasicBlock bb, SimpleAssignable a) {
   not result + 1 = ssaRefRank(bb, _, a, _)
 }
 
-private predicate reachesEndOf(Definition def, SimpleAssignable a, PreBasicBlock bb) {
-  exists(int last | last = maxSsaRefRank(bb, a) | defReachesRank(bb, def, a, last))
-  or
-  exists(PreBasicBlock mid |
-    reachesEndOf(def, a, mid) and
-    not exists(ssaRefRank(mid, _, a, SsaDef())) and
-    bb = mid.getASuccessor()
-  )
+pragma[noinline]
+private predicate ssaDefReachesEndOfBlockRec(PreBasicBlock bb, Definition def, SimpleAssignable a) {
+  exists(PreBasicBlock idom | ssaDefReachesEndOfBlock(idom, def, a) | idom.immediatelyDominates(bb))
 }
 
-private predicate varOccursInBlock(SimpleAssignable a, PreBasicBlock bb) {
-  exists(ssaRefRank(bb, _, a, _))
+predicate ssaDefReachesEndOfBlock(PreBasicBlock bb, Definition def, SimpleAssignable a) {
+  exists(int last | last = maxSsaRefRank(bb, a) |
+    defReachesRank(bb, def, a, last) and
+    liveAtExit(bb, a)
+  )
+  or
+  ssaDefReachesEndOfBlockRec(bb, def, a) and
+  liveAtExit(bb, a) and
+  not ssaRef(bb, _, a, SsaDef())
 }
 
-pragma[nomagic]
-private predicate blockPrecedesVar(SimpleAssignable a, PreBasicBlock bb) {
-  varOccursInBlock(a, bb.getASuccessor*())
+private predicate ssaDefReachesReadWithinBlock(
+  SimpleAssignable a, Definition def, PreBasicBlock bb, int i
+) {
+  defReachesRank(bb, def, a, ssaRefRank(bb, i, a, SsaRead()))
 }
 
-private predicate varBlockReaches(SimpleAssignable a, PreBasicBlock bb1, PreBasicBlock bb2) {
-  varOccursInBlock(a, bb1) and
-  bb2 = bb1.getASuccessor() and
-  blockPrecedesVar(a, bb2)
+private predicate ssaDefReachesRead(SimpleAssignable a, Definition def, PreBasicBlock bb, int i) {
+  ssaDefReachesReadWithinBlock(a, def, bb, i)
   or
-  varBlockReachesRec(a, bb1, bb2) and
-  blockPrecedesVar(a, bb2)
+  ssaRef(bb, i, a, SsaRead()) and
+  ssaDefReachesEndOfBlock(bb.getAPredecessor(), def, a) and
+  not ssaDefReachesReadWithinBlock(a, _, bb, i)
 }
 
-pragma[nomagic]
-private predicate varBlockReachesRec(SimpleAssignable a, PreBasicBlock bb1, PreBasicBlock bb2) {
-  exists(PreBasicBlock mid | varBlockReaches(a, bb1, mid) |
-    bb2 = mid.getASuccessor() and
-    not varOccursInBlock(a, mid)
+private int ssaDefRank(Definition def, PreBasicBlock bb, int i) {
+  exists(SimpleAssignable a |
+    a = def.getAssignable() and
+    result = ssaRefRank(bb, i, a, _)
+  |
+    ssaDefReachesRead(a, def, bb, i)
+    or
+    defAt(bb, i, def, a)
   )
 }
 
-private predicate varBlockStep(SimpleAssignable a, PreBasicBlock bb1, PreBasicBlock bb2) {
-  varBlockReaches(a, bb1, bb2) and
-  varOccursInBlock(a, bb2)
+private predicate varOccursInBlock(Definition def, PreBasicBlock bb, SimpleAssignable a) {
+  exists(ssaDefRank(def, bb, _)) and
+  a = def.getAssignable()
 }
 
-private predicate adjacentVarRefs(
-  SimpleAssignable a, PreBasicBlock bb1, int i1, PreBasicBlock bb2, int i2
-) {
-  exists(int rankix |
-    bb1 = bb2 and
-    rankix = ssaRefRank(bb1, i1, a, _) and
-    rankix + 1 = ssaRefRank(bb2, i2, a, _)
-  )
+pragma[noinline]
+private PreBasicBlock getAMaybeLiveSuccessor(Definition def, PreBasicBlock bb) {
+  result = bb.getASuccessor() and
+  not varOccursInBlock(_, bb, def.getAssignable()) and
+  ssaDefReachesEndOfBlock(bb, def, _)
+}
+
+private predicate varBlockReaches(Definition def, PreBasicBlock bb1, PreBasicBlock bb2) {
+  varOccursInBlock(def, bb1, _) and
+  bb2 = bb1.getASuccessor()
   or
-  ssaRefRank(bb1, i1, a, _) = maxSsaRefRank(bb1, a) and
-  varBlockStep(a, bb1, bb2) and
-  ssaRefRank(bb2, i2, a, _) = 1
+  exists(PreBasicBlock mid | varBlockReaches(def, bb1, mid) |
+    bb2 = getAMaybeLiveSuccessor(def, mid)
+  )
 }
 
-predicate firstReadSameVar(Definition def, AssignableRead read) {
-  exists(SimpleAssignable a, PreBasicBlock b1, int i1, PreBasicBlock b2, int i2 |
-    adjacentVarRefs(a, b1, i1, b2, i2) and
-    defAt(b1, i1, def, a) and
-    readAt(b2, i2, read, a)
+private predicate varBlockReachesRead(Definition def, PreBasicBlock bb1, AssignableRead read) {
+  exists(PreBasicBlock bb2, int i2 |
+    varBlockReaches(def, bb1, bb2) and
+    ssaRefRank(bb2, i2, def.getAssignable(), SsaRead()) = 1 and
+    readAt(bb2, i2, read, _)
   )
 }
 
-predicate adjacentReadPairSameVar(AssignableRead read1, AssignableRead read2) {
-  exists(SimpleAssignable a, PreBasicBlock bb1, int i1, PreBasicBlock bb2, int i2 |
-    adjacentVarRefs(a, bb1, i1, bb2, i2) and
-    readAt(bb1, i1, read1, a) and
-    readAt(bb2, i2, read2, a)
+private predicate adjacentVarRead(Definition def, PreBasicBlock bb1, int i1, AssignableRead read) {
+  exists(int rankix, int i2 |
+    rankix = ssaDefRank(def, bb1, i1) and
+    rankix + 1 = ssaDefRank(def, bb1, i2) and
+    readAt(bb1, i2, read, _)
   )
+  or
+  ssaDefRank(def, bb1, i1) = maxSsaRefRank(bb1, def.getAssignable()) and
+  varBlockReachesRead(def, bb1, read)
 }
 
-pragma[noinline]
-private predicate ssaDefReachesEndOfBlockRec(PreBasicBlock bb, Definition def, SimpleAssignable a) {
-  exists(PreBasicBlock idom | ssaDefReachesEndOfBlock(idom, def, a) | idom.immediatelyDominates(bb))
+predicate firstReadSameVar(Definition def, AssignableRead read) {
+  exists(PreBasicBlock bb1, int i1 |
+    defAt(bb1, i1, def, _) and
+    adjacentVarRead(def, bb1, i1, read)
+  )
 }
 
-predicate ssaDefReachesEndOfBlock(PreBasicBlock bb, Definition def, SimpleAssignable a) {
-  exists(int last | last = maxSsaRefRank(bb, a) |
-    defReachesRank(bb, def, a, last) and
-    liveAtExit(bb, a)
+predicate adjacentReadPairSameVar(AssignableRead read1, AssignableRead read2) {
+  exists(Definition def, PreBasicBlock bb1, int i1 |
+    readAt(bb1, i1, read1, _) and
+    adjacentVarRead(def, bb1, i1, read2)
   )
-  or
-  ssaDefReachesEndOfBlockRec(bb, def, a) and
-  liveAtExit(bb, a) and
-  not ssaRef(bb, _, a, SsaDef())
 }

csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll

@@ -667,63 +667,82 @@ module Ssa {
       )
     }
 
-    /** Holds if `v` is defined or read in basic block `bb`. */
-    private predicate varOccursInBlock(TrackedVar v, BasicBlock bb) {
-      exists(ssaRefRank(bb, _, v, _))
+    /**
+     * Same as `ssaRefRank()`, but restricted to actual reads of `def`, or
+     * `def` itself.
+     */
+    private int ssaDefRank(TrackedDefinition def, TrackedVar v, BasicBlock bb, int i) {
+      v = def.getSourceVariable() and
+      result = ssaRefRank(bb, i, v, _) and
+      (
+        ssaDefReachesRead(_, def, bb.getNode(i), ActualRead())
+        or
+        definesAt(def, bb, i, _)
+      )
     }
 
-    /** Holds if `v` occurs in `bb` or one of `bb`'s transitive successors. */
-    private predicate blockPrecedesVar(TrackedVar v, BasicBlock bb) {
-      varOccursInBlock(v, bb)
-      or
-      blockPrecedesVar(v, bb.getASuccessor())
+    private int maxSsaDefRefRank(BasicBlock bb, TrackedVar v) {
+      result = ssaDefRank(_, v, bb, _) and
+      not result + 1 = ssaDefRank(_, v, bb, _)
     }
 
-    /**
-     * Holds if `bb2` is a transitive successor of `bb1` and `v` occurs in `bb1` and
-     * in `bb2` or one of its transitive successors but not in any block on the path
-     * between `bb1` and `bb2`.
-     */
-    private predicate varBlockReaches(TrackedVar v, BasicBlock bb1, BasicBlock bb2) {
-      varOccursInBlock(v, bb1) and
-      bb2 = bb1.getASuccessor() and
-      blockPrecedesVar(v, bb2)
-      or
-      varBlockReachesRec(v, bb1, bb2) and
-      blockPrecedesVar(v, bb2)
+    private predicate varOccursInBlock(TrackedDefinition def, BasicBlock bb, TrackedVar v) {
+      exists(ssaDefRank(def, v, bb, _))
     }
 
     pragma[noinline]
-    private predicate varBlockReachesRec(TrackedVar v, BasicBlock bb1, BasicBlock bb2) {
-      exists(BasicBlock mid | varBlockReaches(v, bb1, mid) |
-        bb2 = mid.getASuccessor() and
-        not varOccursInBlock(v, mid)
+    private BasicBlock getAMaybeLiveSuccessor(Definition def, BasicBlock bb) {
+      result = bb.getASuccessor() and
+      not varOccursInBlock(_, bb, def.getSourceVariable()) and
+      ssaDefReachesEndOfBlock(bb, def, _)
+    }
+
+    /**
+     * Holds if `def` is accessed in basic block `bb1` (either a read or a write),
+     * `bb2` is a transitive successor of `bb1`, and `def` is *maybe* read in `bb2`
+     * or one of its transitive successors, but not in any block on the path between
+     * `bb1` and `bb2`.
+     */
+    private predicate varBlockReaches(TrackedDefinition def, BasicBlock bb1, BasicBlock bb2) {
+      varOccursInBlock(def, bb1, _) and
+      bb2 = bb1.getASuccessor()
+      or
+      exists(BasicBlock mid | varBlockReaches(def, bb1, mid) |
+        bb2 = getAMaybeLiveSuccessor(def, mid)
       )
     }
 
     /**
-     * Holds if `bb2` is a transitive successor of `bb1` and `v` occurs in `bb1` and
-     * `bb2` but not in any block on the path between `bb1` and `bb2`.
+     * Holds if `def` is accessed in basic block `bb1` (either a read or a write),
+     * `def` is read at `cfn`, `cfn` is in a transitive successor block of `bb1`,
+     * and `def` is not read in any block on the path between `bb1` and `cfn`.
      */
-    private predicate varBlockStep(TrackedVar v, BasicBlock bb1, BasicBlock bb2) {
-      varBlockReaches(v, bb1, bb2) and
-      varOccursInBlock(v, bb2)
+    private predicate varBlockReachesRead(
+      TrackedDefinition def, BasicBlock bb1, ControlFlow::Node cfn
+    ) {
+      exists(BasicBlock bb2, int i2 |
+        varBlockReaches(def, bb1, bb2) and
+        ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
+        variableRead(bb2, i2, _, cfn, _)
+      )
     }
 
     /**
-     * Holds if `v` is accessed at index `i1` in basic block `bb1` and at index `i2` in
-     * basic block `bb2` and there is a path between them without any access to `v`.
+     * Holds if `def` is accessed at index `i1` in basic block `bb1` (either a read
+     * or a write), `def` is read at `cfn`, and there is a path between them without
+     * any read of `def`.
      */
-    private predicate adjacentVarRefs(TrackedVar v, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
-      exists(int rankix |
-        bb1 = bb2 and
-        rankix = ssaRefRank(bb1, i1, v, _) and
-        rankix + 1 = ssaRefRank(bb2, i2, v, _)
+    private predicate adjacentVarRead(
+      TrackedDefinition def, BasicBlock bb1, int i1, ControlFlow::Node cfn
+    ) {
+      exists(int rankix, int i2 |
+        rankix = ssaDefRank(def, _, bb1, i1) and
+        rankix + 1 = ssaDefRank(def, _, bb1, i2) and
+        variableRead(bb1, i2, _, cfn, _)
       )
       or
-      ssaRefRank(bb1, i1, v, _) = maxSsaRefRank(bb1, v) and
-      varBlockStep(v, bb1, bb2) and
-      ssaRefRank(bb2, i2, v, _) = 1
+      exists(SourceVariable v | ssaDefRank(def, v, bb1, i1) = maxSsaDefRefRank(bb1, v)) and
+      varBlockReachesRead(def, bb1, cfn)
     }
 
     cached
@@ -736,23 +755,26 @@ module Ssa {
        */
       cached
       predicate lastRead(TrackedDefinition def, ControlFlow::Node cfn) {
-        exists(TrackedVar v, BasicBlock bb, int i, int rnk |
-          exists(def.getAReadAtNode(cfn)) and
-          variableRead(bb, i, v, cfn, _) and
-          rnk = ssaRefRank(bb, i, v, SsaRead())
+        exists(BasicBlock bb1, int i1, int rnk, TrackedVar v |
+          variableRead(bb1, i1, v, cfn, _) and
+          rnk = ssaDefRank(def, v, bb1, i1)
         |
-          // Next reference to `v` inside `bb` is a write
-          rnk + 1 = ssaRefRank(bb, _, v, SsaDef())
+          // Next reference to `v` inside `bb1` is a write
+          rnk + 1 = ssaRefRank(bb1, _, v, SsaDef())
           or
-          // No next reference to `v` inside `bb`
-          rnk = maxSsaRefRank(bb, v) and
+          // No more references to `v` inside `bb1`
+          rnk = maxSsaDefRefRank(bb1, def.getSourceVariable()) and
           (
-            // Read reaches end of enclosing callable
-            not varBlockReaches(v, bb, _)
+            // Can reach exit directly
+            bb1 instanceof ControlFlow::BasicBlocks::ExitBlock
             or
-            // Read reaches an SSA definition in a successor block
-            exists(BasicBlock bb2 | varBlockReaches(v, bb, bb2) |
-              1 = ssaRefRank(bb2, _, v, SsaDef())
+            exists(BasicBlock bb2 | varBlockReaches(def, bb1, bb2) |
+              // Can reach a write using one or more steps
+              1 = ssaRefRank(bb2, _, def.getSourceVariable(), SsaDef())
+              or
+              // Can reach a block using one or more steps, where `def` is no longer live
+              not varOccursInBlock(def, bb2, _) and
+              not ssaDefReachesEndOfBlock(bb2, def, _)
             )
           )
         )
@@ -831,10 +853,9 @@ module Ssa {
        */
       cached
       predicate firstReadSameVar(TrackedDefinition def, ControlFlow::Node cfn) {
-        exists(TrackedVar v, BasicBlock b1, int i1, BasicBlock b2, int i2 |
-          adjacentVarRefs(v, b1, i1, b2, i2) and
-          definesAt(def, b1, i1, v) and
-          variableRead(b2, i2, v, cfn, _)
+        exists(BasicBlock bb1, int i1 |
+          definesAt(def, bb1, i1, _) and
+          adjacentVarRead(def, bb1, i1, cfn)
         )
       }
 
@@ -845,10 +866,9 @@ module Ssa {
        */
       cached
       predicate adjacentReadPairSameVar(ControlFlow::Node cfn1, ControlFlow::Node cfn2) {
-        exists(TrackedVar v, BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
-          adjacentVarRefs(v, bb1, i1, bb2, i2) and
-          variableRead(bb1, i1, v, cfn1, _) and
-          variableRead(bb2, i2, v, cfn2, _)
+        exists(TrackedDefinition def, BasicBlock bb1, int i1 |
+          variableRead(bb1, i1, _, cfn1, _) and
+          adjacentVarRead(def, bb1, i1, cfn2)
         )
       }
     }