C#: Update Base SSA library to use parameterized module

Author: hvitved

config/identical-files.json

@@ -463,7 +463,6 @@
   "SSA C#": [
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImplCommon.qll",
     "csharp/ql/lib/semmle/code/csharp/controlflow/internal/pressa/SsaImplCommon.qll",
-    "csharp/ql/lib/semmle/code/csharp/dataflow/internal/basessa/SsaImplCommon.qll",
     "ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImplCommon.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImplCommon.qll",
     "swift/ql/lib/codeql/swift/dataflow/internal/SsaImplCommon.qll"

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

@@ -4,19 +4,74 @@ import csharp
  * Provides a simple SSA implementation for local scope variables.
  */
 module BaseSsa {
-  import basessa.SsaImplSpecific
-  private import basessa.SsaImplCommon as SsaImpl
+  private import AssignableDefinitions
+  private import semmle.code.csharp.dataflow.internal.SsaImplCommon as SsaImplCommon
+
+  /**
+   * Holds if the `i`th node of basic block `bb` is assignable definition `def`,
+   * targeting local scope variable `v`.
+   */
+  private predicate definitionAt(
+    AssignableDefinition def, ControlFlow::BasicBlock bb, int i, SsaInput::SourceVariable v
+  ) {
+    bb.getNode(i) = def.getAControlFlowNode() and
+    v = def.getTarget() and
+    // In cases like `(x, x) = (0, 1)`, we discard the first (dead) definition of `x`
+    not exists(TupleAssignmentDefinition first, TupleAssignmentDefinition second | first = def |
+      second.getAssignment() = first.getAssignment() and
+      second.getEvaluationOrder() > first.getEvaluationOrder() and
+      second.getTarget() = v
+    )
+  }
+
+  private module SsaInput implements SsaImplCommon::InputSig {
+    class BasicBlock = ControlFlow::BasicBlock;
+
+    BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) {
+      result = bb.getImmediateDominator()
+    }
+
+    BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
+
+    class ExitBasicBlock = ControlFlow::BasicBlocks::ExitBlock;
+
+    pragma[noinline]
+    private Callable getAnAssigningCallable(LocalScopeVariable v) {
+      result = any(AssignableDefinition def | def.getTarget() = v).getEnclosingCallable()
+    }
+
+    class SourceVariable extends LocalScopeVariable {
+      SourceVariable() { not getAnAssigningCallable(this) != getAnAssigningCallable(this) }
+    }
+
+    predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+      exists(AssignableDefinition def |
+        definitionAt(def, bb, i, v) and
+        if def.isCertain() then certain = true else certain = false
+      )
+    }
+
+    predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+      exists(AssignableRead read |
+        read.getAControlFlowNode() = bb.getNode(i) and
+        read.getTarget() = v and
+        certain = true
+      )
+    }
+  }
+
+  private module SsaImpl = SsaImplCommon::Make<SsaInput>;
 
   class Definition extends SsaImpl::Definition {
     final AssignableRead getARead() {
-      exists(BasicBlock bb, int i |
+      exists(ControlFlow::BasicBlock bb, int i |
         SsaImpl::ssaDefReachesRead(_, this, bb, i) and
         result.getAControlFlowNode() = bb.getNode(i)
       )
     }
 
     final AssignableDefinition getDefinition() {
-      exists(BasicBlock bb, int i, SourceVariable v |
+      exists(ControlFlow::BasicBlock bb, int i, SsaInput::SourceVariable v |
         this.definesAt(v, bb, i) and
         definitionAt(result, bb, i, v)
       )