Merge pull request github#11066 from hvitved/ssa/deprecate-no-uncertain-reads-predicates

Author: hvitved

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

@@ -1067,6 +1067,59 @@ private predicate variableReadPseudo(ControlFlow::BasicBlock bb, int i, Ssa::Sou
   capturedReadIn(bb, i, v, _, _, _)
 }
 
+pragma[noinline]
+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
+  v = def.getSourceVariable()
+}
+
+private predicate adjacentDefReachesRead(
+  Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
+) {
+  exists(SsaInput::SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
+    def.definesAt(v, bb1, i1)
+    or
+    SsaInput::variableRead(bb1, i1, v, true)
+  )
+  or
+  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)
+  )
+}
+
+/** Same as `adjacentDefRead`, but skips uncertain reads. */
+pragma[nomagic]
+private predicate adjacentDefSkipUncertainReads(
+  Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
+) {
+  adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
+  SsaInput::variableRead(bb2, i2, _, true)
+}
+
+private predicate adjacentDefReachesUncertainRead(
+  Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
+) {
+  adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
+  SsaInput::variableRead(bb2, i2, _, false)
+}
+
+/** Same as `lastRefRedef`, but skips uncertain reads. */
+pragma[nomagic]
+private predicate lastRefSkipUncertainReads(Definition def, SsaInput::BasicBlock bb, int i) {
+  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
+    adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
+  )
+}
+
 cached
 private module Cached {
   cached
@@ -1237,7 +1290,7 @@ private module Cached {
   predicate firstReadSameVar(Definition def, ControlFlow::Node cfn) {
     exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 |
       def.definesAt(_, bb1, i1) and
-      adjacentDefNoUncertainReads(def, bb1, i1, bb2, i2) and
+      adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
       cfn = bb2.getNode(i2)
     )
   }
@@ -1252,20 +1305,27 @@ private module Cached {
     exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 |
       cfn1 = bb1.getNode(i1) and
       variableReadActual(bb1, i1, _) and
-      adjacentDefNoUncertainReads(def, bb1, i1, bb2, i2) and
+      adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
       cfn2 = bb2.getNode(i2)
     )
   }
 
+  /** Same as `lastRefRedef`, but skips uncertain reads. */
   cached
   predicate lastRefBeforeRedef(Definition def, ControlFlow::BasicBlock bb, int i, Definition next) {
-    lastRefRedefNoUncertainReads(def, bb, i, next)
+    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
+      adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
+    )
   }
 
   cached
   predicate lastReadSameVar(Definition def, ControlFlow::Node cfn) {
     exists(ControlFlow::BasicBlock bb, int i |
-      lastRefNoUncertainReads(def, bb, i) and
+      lastRefSkipUncertainReads(def, bb, i) and
       variableReadActual(bb, i, _) and
       cfn = bb.getNode(i)
     )

shared/ssa/codeql/ssa/Ssa.qll

@@ -660,14 +660,14 @@ module Make<InputSig Input> {
   }
 
   pragma[noinline]
-  private predicate adjacentDefRead(
+  deprecated private predicate adjacentDefRead(
     Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
   ) {
     adjacentDefRead(def, bb1, i1, bb2, i2) and
     v = def.getSourceVariable()
   }
 
-  private predicate adjacentDefReachesRead(
+  deprecated private predicate adjacentDefReachesRead(
     Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
   ) {
     exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
@@ -689,7 +689,7 @@ module Make<InputSig Input> {
    * Same as `adjacentDefRead`, but ignores uncertain reads.
    */
   pragma[nomagic]
-  predicate adjacentDefNoUncertainReads(
+  deprecated predicate adjacentDefNoUncertainReads(
     Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
   ) {
     adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
@@ -734,7 +734,7 @@ module Make<InputSig Input> {
     lastRefRedef(inp, _, _, def)
   }
 
-  private predicate adjacentDefReachesUncertainRead(
+  deprecated private predicate adjacentDefReachesUncertainRead(
     Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
   ) {
     adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
@@ -747,7 +747,9 @@ module Make<InputSig Input> {
    * Same as `lastRefRedef`, but ignores uncertain reads.
    */
   pragma[nomagic]
-  predicate lastRefRedefNoUncertainReads(Definition def, BasicBlock bb, int i, Definition next) {
+  deprecated predicate lastRefRedefNoUncertainReads(
+    Definition def, BasicBlock bb, int i, Definition next
+  ) {
     lastRefRedef(def, bb, i, next) and
     not variableRead(bb, i, def.getSourceVariable(), false)
     or
@@ -787,7 +789,7 @@ module Make<InputSig Input> {
    * Same as `lastRefRedef`, but ignores uncertain reads.
    */
   pragma[nomagic]
-  predicate lastRefNoUncertainReads(Definition def, BasicBlock bb, int i) {
+  deprecated predicate lastRefNoUncertainReads(Definition def, BasicBlock bb, int i) {
     lastRef(def, bb, i) and
     not variableRead(bb, i, def.getSourceVariable(), false)
     or