Merge pull request #11198 from hvitved/ssa/expose-phi-reads

SSA: Expose phi-read nodes

Author: hvitved

csharp/ql/consistency-queries/SsaConsistency.ql

@@ -1,5 +1,6 @@
 import csharp
-import semmle.code.csharp.dataflow.internal.SsaImpl::Consistency
+import semmle.code.csharp.dataflow.internal.SsaImpl as Impl
+import Impl::Consistency
 import Ssa
 
 class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
@@ -10,6 +11,14 @@ class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
   }
 }
 
+class MyRelevantDefinitionExt extends RelevantDefinitionExt, Impl::DefinitionExt {
+  override predicate hasLocationInfo(
+    string filepath, int startline, int startcolumn, int endline, int endcolumn
+  ) {
+    this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
+  }
+}
+
 query predicate localDeclWithSsaDef(LocalVariableDeclExpr d) {
   // Local variables in C# must be initialized before every use, so uninitialized
   // local variables should not have an SSA definition, as that would imply that

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

@@ -138,25 +138,6 @@ module Ssa {
     }
   }
 
-  private string getSplitString(Definition def) {
-    exists(ControlFlow::BasicBlock bb, int i, ControlFlow::Node cfn |
-      def.definesAt(_, bb, i) and
-      result = cfn.(ControlFlow::Nodes::ElementNode).getSplitsString()
-    |
-      cfn = bb.getNode(i)
-      or
-      not exists(bb.getNode(i)) and
-      cfn = bb.getFirstNode()
-    )
-  }
-
-  private string getToStringPrefix(Definition def) {
-    result = "[" + getSplitString(def) + "] "
-    or
-    not exists(getSplitString(def)) and
-    result = ""
-  }
-
   /**
    * A static single assignment (SSA) definition. Either an explicit variable
    * definition (`ExplicitDefinition`), an implicit variable definition
@@ -521,8 +502,8 @@ module Ssa {
 
     override string toString() {
       if this.getADefinition() instanceof AssignableDefinitions::ImplicitParameterDefinition
-      then result = getToStringPrefix(this) + "SSA param(" + this.getSourceVariable() + ")"
-      else result = getToStringPrefix(this) + "SSA def(" + this.getSourceVariable() + ")"
+      then result = SsaImpl::getToStringPrefix(this) + "SSA param(" + this.getSourceVariable() + ")"
+      else result = SsaImpl::getToStringPrefix(this) + "SSA def(" + this.getSourceVariable() + ")"
     }
 
     override Location getLocation() { result = ad.getLocation() }
@@ -570,8 +551,12 @@ module Ssa {
 
     override string toString() {
       if this.getSourceVariable().getAssignable() instanceof LocalScopeVariable
-      then result = getToStringPrefix(this) + "SSA capture def(" + this.getSourceVariable() + ")"
-      else result = getToStringPrefix(this) + "SSA entry def(" + this.getSourceVariable() + ")"
+      then
+        result =
+          SsaImpl::getToStringPrefix(this) + "SSA capture def(" + this.getSourceVariable() + ")"
+      else
+        result =
+          SsaImpl::getToStringPrefix(this) + "SSA entry def(" + this.getSourceVariable() + ")"
     }
 
     override Location getLocation() { result = this.getCallable().getLocation() }
@@ -612,7 +597,7 @@ module Ssa {
     }
 
     override string toString() {
-      result = getToStringPrefix(this) + "SSA call def(" + this.getSourceVariable() + ")"
+      result = SsaImpl::getToStringPrefix(this) + "SSA call def(" + this.getSourceVariable() + ")"
     }
 
     override Location getLocation() { result = this.getCall().getLocation() }
@@ -640,7 +625,8 @@ module Ssa {
     final Definition getQualifierDefinition() { result = q }
 
     override string toString() {
-      result = getToStringPrefix(this) + "SSA qualifier def(" + this.getSourceVariable() + ")"
+      result =
+        SsaImpl::getToStringPrefix(this) + "SSA qualifier def(" + this.getSourceVariable() + ")"
     }
 
     override Location getLocation() { result = this.getQualifierDefinition().getLocation() }
@@ -682,7 +668,7 @@ module Ssa {
     }
 
     override string toString() {
-      result = getToStringPrefix(this) + "SSA phi(" + this.getSourceVariable() + ")"
+      result = SsaImpl::getToStringPrefix(this) + "SSA phi(" + this.getSourceVariable() + ")"
     }
 
     /*

csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll

@@ -49,7 +49,23 @@ private module SsaInput implements SsaImplCommon::InputSig {
   }
 }
 
-import SsaImplCommon::Make<SsaInput>
+private import SsaImplCommon::Make<SsaInput> as Impl
+
+class Definition = Impl::Definition;
+
+class WriteDefinition = Impl::WriteDefinition;
+
+class UncertainWriteDefinition = Impl::UncertainWriteDefinition;
+
+class PhiNode = Impl::PhiNode;
+
+module Consistency = Impl::Consistency;
+
+module ExposedForTestingOnly {
+  predicate ssaDefReachesReadExt = Impl::ssaDefReachesReadExt/4;
+
+  predicate phiHasInputFromBlockExt = Impl::phiHasInputFromBlockExt/3;
+}
 
 /**
  * Holds if the `i`th node of basic block `bb` reads source variable `v`.
@@ -1072,7 +1088,7 @@ private predicate adjacentDefRead(
   Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2,
   SsaInput::SourceVariable v
 ) {
-  adjacentDefRead(def, bb1, i1, bb2, i2) and
+  Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
   v = def.getSourceVariable()
 }
 
@@ -1088,7 +1104,7 @@ private predicate adjacentDefReachesRead(
   exists(SsaInput::BasicBlock bb3, int i3 |
     adjacentDefReachesRead(def, bb1, i1, bb3, i3) and
     SsaInput::variableRead(bb3, i3, _, false) and
-    adjacentDefRead(def, bb3, i3, bb2, i2)
+    Impl::adjacentDefRead(def, bb3, i3, bb2, i2)
   )
 }
 
@@ -1111,11 +1127,11 @@ private predicate adjacentDefReachesUncertainRead(
 /** Same as `lastRefRedef`, but skips uncertain reads. */
 pragma[nomagic]
 private predicate lastRefSkipUncertainReads(Definition def, SsaInput::BasicBlock bb, int i) {
-  lastRef(def, bb, i) and
+  Impl::lastRef(def, bb, i) and
   not SsaInput::variableRead(bb, i, def.getSourceVariable(), false)
   or
   exists(SsaInput::BasicBlock bb0, int i0 |
-    lastRef(def, bb0, i0) and
+    Impl::lastRef(def, bb0, i0) and
     adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
   )
 }
@@ -1237,7 +1253,7 @@ private module Cached {
       v = def.getSourceVariable() and
       capturedReadIn(_, _, v, edef.getSourceVariable(), c, additionalCalls) and
       def = def0.getAnUltimateDefinition() and
-      ssaDefReachesRead(_, def0, bb, i) and
+      Impl::ssaDefReachesRead(_, def0, bb, i) and
       capturedReadIn(bb, i, v, _, _, _) and
       c = bb.getNode(i)
     )
@@ -1264,18 +1280,18 @@ private module Cached {
 
   cached
   predicate isLiveAtEndOfBlock(Definition def, ControlFlow::BasicBlock bb) {
-    ssaDefReachesEndOfBlock(bb, def, _)
+    Impl::ssaDefReachesEndOfBlock(bb, def, _)
   }
 
   cached
-  Definition phiHasInputFromBlock(PhiNode phi, ControlFlow::BasicBlock bb) {
-    phiHasInputFromBlock(phi, result, bb)
+  Definition phiHasInputFromBlock(Ssa::PhiNode phi, ControlFlow::BasicBlock bb) {
+    Impl::phiHasInputFromBlock(phi, result, bb)
   }
 
   cached
   AssignableRead getAReadAtNode(Definition def, ControlFlow::Node cfn) {
     exists(Ssa::SourceVariable v, ControlFlow::BasicBlock bb, int i |
-      ssaDefReachesRead(v, def, bb, i) and
+      Impl::ssaDefReachesRead(v, def, bb, i) and
       variableReadActual(bb, i, v) and
       cfn = bb.getNode(i) and
       result.getAControlFlowNode() = cfn
@@ -1313,11 +1329,11 @@ private module Cached {
   /** Same as `lastRefRedef`, but skips uncertain reads. */
   cached
   predicate lastRefBeforeRedef(Definition def, ControlFlow::BasicBlock bb, int i, Definition next) {
-    lastRefRedef(def, bb, i, next) and
+    Impl::lastRefRedef(def, bb, i, next) and
     not SsaInput::variableRead(bb, i, def.getSourceVariable(), false)
     or
     exists(SsaInput::BasicBlock bb0, int i0 |
-      lastRefRedef(def, bb0, i0, next) and
+      Impl::lastRefRedef(def, bb0, i0, next) and
       adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
     )
   }
@@ -1333,7 +1349,7 @@ private module Cached {
 
   cached
   Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def) {
-    uncertainWriteDefinitionInput(def, result)
+    Impl::uncertainWriteDefinitionInput(def, result)
   }
 
   cached
@@ -1343,10 +1359,57 @@ private module Cached {
       v = def.getSourceVariable() and
       p = v.getAssignable() and
       def = def0.getAnUltimateDefinition() and
-      ssaDefReachesRead(_, def0, bb, i) and
+      Impl::ssaDefReachesRead(_, def0, bb, i) and
       outRefExitRead(bb, i, v)
     )
   }
 }
 
 import Cached
+
+private string getSplitString(DefinitionExt def) {
+  exists(ControlFlow::BasicBlock bb, int i, ControlFlow::Node cfn |
+    def.definesAt(_, bb, i, _) and
+    result = cfn.(ControlFlow::Nodes::ElementNode).getSplitsString()
+  |
+    cfn = bb.getNode(i)
+    or
+    not exists(bb.getNode(i)) and
+    cfn = bb.getFirstNode()
+  )
+}
+
+string getToStringPrefix(DefinitionExt def) {
+  result = "[" + getSplitString(def) + "] "
+  or
+  not exists(getSplitString(def)) and
+  result = ""
+}
+
+/**
+ * An extended static single assignment (SSA) definition.
+ *
+ * This is either a normal SSA definition (`Definition`) or a
+ * phi-read node (`PhiReadNode`).
+ *
+ * Only intended for internal use.
+ */
+class DefinitionExt extends Impl::DefinitionExt {
+  override string toString() { result = this.(Ssa::Definition).toString() }
+
+  /** Gets the location of this definition. */
+  Location getLocation() { result = this.(Ssa::Definition).getLocation() }
+}
+
+/**
+ * A phi-read node.
+ *
+ * Only intended for internal use.
+ */
+class PhiReadNode extends DefinitionExt, Impl::PhiReadNode {
+  override string toString() {
+    result = getToStringPrefix(this) + "SSA phi read(" + this.getSourceVariable() + ")"
+  }
+
+  override Location getLocation() { result = this.getBasicBlock().getLocation() }
+}

csharp/ql/test/library-tests/dataflow/ssa/SSAPhiRead.expected

@@ -1,4 +1,30 @@
-| DefUse.cs:63:9:63:14 | this.Field2 | DefUse.cs:80:30:80:31 | access to local variable x1 |
-| Fields.cs:65:24:65:32 | this.LoopField | Fields.cs:63:16:63:28 | this access |
-| Properties.cs:65:24:65:31 | this.LoopProp | Properties.cs:63:16:63:16 | access to parameter i |
-| Test.cs:78:13:78:13 | x | Test.cs:90:9:97:9 | if (...) ... |
+phiReadNode
+| DefUse.cs:80:30:80:31 | SSA phi read(this.Field2) | DefUse.cs:63:9:63:14 | this.Field2 |
+| Fields.cs:63:16:63:28 | SSA phi read(this.LoopField) | Fields.cs:65:24:65:32 | this.LoopField |
+| Patterns.cs:20:9:38:9 | SSA phi read(o) | Patterns.cs:7:16:7:16 | o |
+| Properties.cs:63:16:63:16 | SSA phi read(this.LoopProp) | Properties.cs:65:24:65:31 | this.LoopProp |
+| Test.cs:25:16:25:16 | SSA phi read(x) | Test.cs:8:13:8:13 | x |
+| Test.cs:90:9:97:9 | SSA phi read(x) | Test.cs:78:13:78:13 | x |
+| Test.cs:99:9:99:15 | SSA phi read(x) | Test.cs:78:13:78:13 | x |
+phiReadNodeRead
+| DefUse.cs:80:30:80:31 | SSA phi read(this.Field2) | DefUse.cs:63:9:63:14 | this.Field2 | DefUse.cs:80:37:80:42 | access to field Field2 |
+| Fields.cs:63:16:63:28 | SSA phi read(this.LoopField) | Fields.cs:65:24:65:32 | this.LoopField | Fields.cs:65:24:65:32 | access to field LoopField |
+| Patterns.cs:20:9:38:9 | SSA phi read(o) | Patterns.cs:7:16:7:16 | o | Patterns.cs:20:17:20:17 | access to local variable o |
+| Properties.cs:63:16:63:16 | SSA phi read(this.LoopProp) | Properties.cs:65:24:65:31 | this.LoopProp | Properties.cs:65:24:65:31 | access to property LoopProp |
+| Test.cs:25:16:25:16 | SSA phi read(x) | Test.cs:8:13:8:13 | x | Test.cs:25:16:25:16 | access to local variable x |
+| Test.cs:90:9:97:9 | SSA phi read(x) | Test.cs:78:13:78:13 | x | Test.cs:92:17:92:17 | access to local variable x |
+| Test.cs:90:9:97:9 | SSA phi read(x) | Test.cs:78:13:78:13 | x | Test.cs:96:17:96:17 | access to local variable x |
+| Test.cs:99:9:99:15 | SSA phi read(x) | Test.cs:78:13:78:13 | x | Test.cs:99:13:99:13 | access to local variable x |
+| Test.cs:99:9:99:15 | SSA phi read(x) | Test.cs:78:13:78:13 | x | Test.cs:104:17:104:17 | access to local variable x |
+phiReadInput
+| DefUse.cs:80:30:80:31 | SSA phi read(this.Field2) | DefUse.cs:63:9:63:18 | SSA def(this.Field2) |
+| DefUse.cs:80:30:80:31 | SSA phi read(this.Field2) | DefUse.cs:80:30:80:31 | SSA phi read(this.Field2) |
+| Fields.cs:63:16:63:28 | SSA phi read(this.LoopField) | Fields.cs:61:17:61:17 | SSA entry def(this.LoopField) |
+| Fields.cs:63:16:63:28 | SSA phi read(this.LoopField) | Fields.cs:63:16:63:28 | SSA phi read(this.LoopField) |
+| Patterns.cs:20:9:38:9 | SSA phi read(o) | Patterns.cs:7:16:7:23 | SSA def(o) |
+| Properties.cs:63:16:63:16 | SSA phi read(this.LoopProp) | Properties.cs:61:17:61:17 | SSA entry def(this.LoopProp) |
+| Properties.cs:63:16:63:16 | SSA phi read(this.LoopProp) | Properties.cs:63:16:63:16 | SSA phi read(this.LoopProp) |
+| Test.cs:25:16:25:16 | SSA phi read(x) | Test.cs:24:9:24:15 | SSA phi(x) |
+| Test.cs:25:16:25:16 | SSA phi read(x) | Test.cs:25:16:25:16 | SSA phi read(x) |
+| Test.cs:90:9:97:9 | SSA phi read(x) | Test.cs:78:13:78:17 | SSA def(x) |
+| Test.cs:99:9:99:15 | SSA phi read(x) | Test.cs:90:9:97:9 | SSA phi read(x) |

csharp/ql/test/library-tests/dataflow/ssa/SSAPhiRead.ql

@@ -1,6 +1,17 @@
 import csharp
 import semmle.code.csharp.dataflow.internal.SsaImpl
+import ExposedForTestingOnly
 
-from Ssa::SourceVariable v, ControlFlow::BasicBlock bb
-where phiReadExposedForTesting(bb, v)
-select v, bb
+query predicate phiReadNode(PhiReadNode phi, Ssa::SourceVariable v) { phi.getSourceVariable() = v }
+
+query predicate phiReadNodeRead(PhiReadNode phi, Ssa::SourceVariable v, ControlFlow::Node read) {
+  phi.getSourceVariable() = v and
+  exists(ControlFlow::BasicBlock bb, int i |
+    ssaDefReachesReadExt(v, phi, bb, i) and
+    read = bb.getNode(i)
+  )
+}
+
+query predicate phiReadInput(PhiReadNode phi, DefinitionExt inp) {
+  phiHasInputFromBlockExt(phi, inp, _)
+}

csharp/ql/test/library-tests/dataflow/ssa/Test.cs

@@ -95,7 +95,7 @@ void phiReads(bool b1, bool b2, bool b3, bool b4, bool b5, bool b6)
         {
             use(x);
         }
-        // no phi_use for `x`, because actual use exists in the block
+        // phi_use for `x`, even though there is an actual use in the block
         use(x);
 
 

ruby/ql/consistency-queries/SsaConsistency.ql

@@ -1,5 +1,6 @@
 import codeql.ruby.dataflow.SSA
-import codeql.ruby.dataflow.internal.SsaImpl::Consistency
+import codeql.ruby.dataflow.internal.SsaImpl
+import Consistency
 
 class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
   override predicate hasLocationInfo(
@@ -8,3 +9,11 @@ class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
     this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
   }
 }
+
+class MyRelevantDefinitionExt extends RelevantDefinitionExt, DefinitionExt {
+  override predicate hasLocationInfo(
+    string filepath, int startline, int startcolumn, int endline, int endcolumn
+  ) {
+    this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
+  }
+}