Validate Python MakeSsa D facade candidate

python/ql/lib/semmle/python/dataflow/new/internal/ImportResolution.qll

@@ -92,7 +92,7 @@ module ImportResolution {
     // uncertain SSA definition for every name in the importing scope. The
     // immediately preceding definition is still potentially the value of the
     // module export.
-    SsaImpl::Impl::uncertainWriteDefinitionInput(defTo, defFrom)
+    defFrom = defTo.(SsaImpl::Ssa::SsaUncertainWrite).getPriorDefinition()
     // Note: legacy ESSA refinement-step (e.g. for `foo.bar = X`) is
     // not modelled in the new SSA beyond the cases handled above.
   }

python/ql/lib/semmle/python/dataflow/new/internal/SsaImpl.qll

@@ -256,7 +256,7 @@ private module SsaImplInput implements SsaImplCommon::InputSig<Py::Location, Cfg
   }
 }
 
-import SsaImplCommon::MakeWithCachedLivenessAndDefinitionReachability<Py::Location, CfgImpl::Cfg, SsaImplInput> as Impl
+import SsaImplCommon::Make<Py::Location, CfgImpl::Cfg, SsaImplInput> as Impl
 
 // Matching the cases in `SsaImplInput.variableWrite` above
 newtype TVariableWrite =
@@ -335,13 +335,13 @@ private module SsaInput implements Impl::SsaInputSig {
 
 module Ssa = Impl::MakeSsa<SsaInput>;
 
-final class Definition = Impl::Definition;
+final class Definition = Ssa::SsaDefinition;
 
-final class WriteDefinition = Impl::WriteDefinition;
+final class WriteDefinition = Ssa::SsaWriteDefinition;
 
-final class UncertainWriteDefinition = Impl::UncertainWriteDefinition;
+final class UncertainWriteDefinition = Ssa::SsaUncertainWrite;
 
-final class PhiNode = Impl::PhiNode;
+final class PhiNode = Ssa::SsaPhiDefinition;
 
 // ===========================================================================
 // ESSA-shaped adapter layer
@@ -524,7 +524,7 @@ class PhiFunction extends PhiNode {
    * the phi from one of its predecessor blocks). Mirrors legacy
    * ESSA's `PhiFunction.getAnInput()`.
    */
-  Ssa::SsaDefinition getAnInput() { Impl::phiHasInputFromBlock(this, result, _) }
+  Ssa::SsaDefinition getAnInput() { result = this.(Ssa::SsaPhiDefinition).getAnInput() }
 }
 
 /** An ESSA definition (legacy-shaped). */
@@ -538,6 +538,19 @@ class EssaVariable extends Ssa::SsaDefinition {
   /** Gets the underlying SSA definition (legacy name). */
   Ssa::SsaDefinition getDefinition() { result = this }
 
+  /**
+   * Gets a synthetic normal-exit use of this definition. These uses have no
+   * `SsaInput::Expr`, so they cannot be exposed by `SsaDefinition.getARead()`.
+   */
+  cached
+  private Cfg::ControlFlowNode getASyntheticExitUse() {
+    exists(CfgImpl::BasicBlock bb, int i |
+      Impl::ssaDefReachesRead(this.getSourceVariable(), this, bb, i) and
+      bb.getNode(i) = result and
+      result.isNormalExit()
+    )
+  }
+
   /**
    * Gets a CFG node where this definition is used. Includes regular
    * `Name` reads as well as the synthetic scope-exit "use" registered
@@ -546,10 +559,9 @@ class EssaVariable extends Ssa::SsaDefinition {
    * from `SsaSourceVariable`.
    */
   Cfg::ControlFlowNode getAUse() {
-    exists(CfgImpl::BasicBlock bb, int i |
-      Impl::ssaDefReachesRead(this.getSourceVariable(), this, bb, i) and
-      bb.getNode(i) = result
-    )
+    result.getNode() = this.(Ssa::SsaDefinition).getARead().asExpr()
+    or
+    result = this.getASyntheticExitUse()
   }
 
   /** Gets the (textual) name of the underlying variable. */

python/ql/test/library-tests/dataflow-new-ssa/FacadeAdapterContract.expected

@@ -0,0 +1,16 @@
+certain_read_mismatch_count
+| 0 |
+end_of_block_mismatch_count
+| 0 |
+phi_input_mismatch_count
+| 0 |
+uncertain_input_mismatch_count
+| 0 |
+adapter_use_mismatch_count
+| 0 |
+synthetic_exit_bypass_count
+| 14 |
+facade_exit_read_count
+| 0 |
+ordinary_exit_overlap_count
+| 0 |

python/ql/test/library-tests/dataflow-new-ssa/FacadeAdapterContract.ql

@@ -0,0 +1,99 @@
+import python
+private import semmle.python.controlflow.internal.AstNodeImpl as CfgImpl
+private import semmle.python.controlflow.internal.Cfg as Cfg
+private import semmle.python.dataflow.new.internal.SsaImpl as SsaImpl
+
+private predicate coreCertainRead(SsaImpl::Definition def, Cfg::ControlFlowNode use) {
+  exists(CfgImpl::BasicBlock bb, int i |
+    SsaImpl::Impl::ssaDefReachesRead(_, def, bb, i) and
+    bb.getNode(i) = use and
+    not use.isNormalExit()
+  )
+}
+
+private predicate facadeCertainRead(SsaImpl::Definition def, Cfg::ControlFlowNode use) {
+  use.getNode() = def.(SsaImpl::Ssa::SsaDefinition).getARead().asExpr()
+}
+
+query int certain_read_mismatch_count() {
+  result =
+    count(SsaImpl::Definition def, Cfg::ControlFlowNode use |
+      coreCertainRead(def, use) and not facadeCertainRead(def, use)
+      or
+      facadeCertainRead(def, use) and not coreCertainRead(def, use)
+    )
+}
+
+query int end_of_block_mismatch_count() {
+  result =
+    count(SsaImpl::Definition def, CfgImpl::BasicBlock bb |
+      SsaImpl::Impl::ssaDefReachesEndOfBlock(bb, def, _) and
+      not def.(SsaImpl::Ssa::SsaDefinition).isLiveAtEndOfBlock(bb)
+      or
+      def.(SsaImpl::Ssa::SsaDefinition).isLiveAtEndOfBlock(bb) and
+      not SsaImpl::Impl::ssaDefReachesEndOfBlock(bb, def, _)
+    )
+}
+
+query int phi_input_mismatch_count() {
+  result =
+    count(SsaImpl::PhiNode phi, SsaImpl::Definition input, CfgImpl::BasicBlock bb |
+      SsaImpl::Impl::phiHasInputFromBlock(phi, input, bb) and
+      not phi.(SsaImpl::Ssa::SsaPhiDefinition)
+          .hasInputFromBlock(input.(SsaImpl::Ssa::SsaDefinition), bb)
+      or
+      phi.(SsaImpl::Ssa::SsaPhiDefinition)
+          .hasInputFromBlock(input.(SsaImpl::Ssa::SsaDefinition), bb) and
+      not SsaImpl::Impl::phiHasInputFromBlock(phi, input, bb)
+    )
+}
+
+query int uncertain_input_mismatch_count() {
+  result =
+    count(SsaImpl::UncertainWriteDefinition def, SsaImpl::Definition input |
+      SsaImpl::Impl::uncertainWriteDefinitionInput(def, input) and
+      not input = def.(SsaImpl::Ssa::SsaUncertainWrite).getPriorDefinition()
+      or
+      input = def.(SsaImpl::Ssa::SsaUncertainWrite).getPriorDefinition() and
+      not SsaImpl::Impl::uncertainWriteDefinitionInput(def, input)
+    )
+}
+
+query int adapter_use_mismatch_count() {
+  result =
+    count(SsaImpl::EssaVariable def, Cfg::ControlFlowNode use |
+      exists(CfgImpl::BasicBlock bb, int i |
+        SsaImpl::Impl::ssaDefReachesRead(def.getSourceVariable(), def, bb, i) and
+        bb.getNode(i) = use
+      ) and
+      not use = def.getAUse()
+      or
+      use = def.getAUse() and
+      not exists(CfgImpl::BasicBlock bb, int i |
+        SsaImpl::Impl::ssaDefReachesRead(def.getSourceVariable(), def, bb, i) and
+        bb.getNode(i) = use
+      )
+    )
+}
+
+query int synthetic_exit_bypass_count() {
+  result =
+    count(SsaImpl::EssaVariable def, Cfg::ControlFlowNode exit |
+      exit = def.getAUse() and exit.isNormalExit()
+    )
+}
+
+query int facade_exit_read_count() {
+  result =
+    count(SsaImpl::Definition def, Cfg::ControlFlowNode exit |
+      exit = def.(SsaImpl::Ssa::SsaDefinition).getARead().getControlFlowNode() and
+      exit.isNormalExit()
+    )
+}
+
+query int ordinary_exit_overlap_count() {
+  result =
+    count(SsaImpl::Definition def, Cfg::ControlFlowNode use |
+      facadeCertainRead(def, use) and use.isNormalExit()
+    )
+}

shared/ssa/codeql/ssa/Ssa.qll

@@ -239,34 +239,6 @@ signature module SsaSig<
   }
 }
 
-private signature module LivenessCachingSig {
-  predicate enabled();
-}
-
-private module NoLivenessCaching implements LivenessCachingSig {
-  pragma[inline]
-  predicate enabled() { none() }
-}
-
-private module LivenessCaching implements LivenessCachingSig {
-  pragma[inline]
-  predicate enabled() { any() }
-}
-
-private signature module DefinitionReachabilityCachingSig {
-  predicate enabled();
-}
-
-private module NoDefinitionReachabilityCaching implements DefinitionReachabilityCachingSig {
-  pragma[inline]
-  predicate enabled() { none() }
-}
-
-private module DefinitionReachabilityCaching implements DefinitionReachabilityCachingSig {
-  pragma[inline]
-  predicate enabled() { any() }
-}
-
 /**
  * Provides an SSA implementation.
  *
@@ -284,9 +256,8 @@ private module DefinitionReachabilityCaching implements DefinitionReachabilityCa
  * NB: If this predicate is exposed, it should be cached.
  * ```
  */
-private module MakeImpl<
-  LocationSig Location, BB::CfgSig<Location> Cfg, InputSig<Location, Cfg::BasicBlock> Input,
-  LivenessCachingSig CacheLiveness, DefinitionReachabilityCachingSig CacheDefinitionReachability>
+module Make<
+  LocationSig Location, BB::CfgSig<Location> Cfg, InputSig<Location, Cfg::BasicBlock> Input>
 {
   private import Cfg
   private import Input
@@ -415,21 +386,7 @@ private module MakeImpl<
     /**
      * Holds if source variable `v` is live at the end of basic block `bb`.
      */
-    private predicate liveAtExitUncached(BasicBlock bb, SourceVariable v) {
-      liveAtEntry(bb.getASuccessor(), v)
-    }
-
-    cached
-    private predicate liveAtExitCached(BasicBlock bb, SourceVariable v) {
-      liveAtEntry(bb.getASuccessor(), v)
-    }
-
-    pragma[inline]
-    predicate liveAtExit(BasicBlock bb, SourceVariable v) {
-      not CacheLiveness::enabled() and liveAtExitUncached(bb, v)
-      or
-      CacheLiveness::enabled() and liveAtExitCached(bb, v)
-    }
+    predicate liveAtExit(BasicBlock bb, SourceVariable v) { liveAtEntry(bb.getASuccessor(), v) }
 
     /**
      * Holds if variable `v` is live in basic block `bb` at rank `rnk`.
@@ -544,22 +501,7 @@ private module MakeImpl<
      * Holds if the SSA definition `def` reaches rank index `rnk` in its own
      * basic block `bb`.
      */
-    private predicate ssaDefReachesRankUncached(
-      BasicBlock bb, Definition def, int rnk, SourceVariable v
-    ) {
-      exists(int i |
-        rnk = refRank(bb, i, v, Def()) and
-        def.definesAt(v, bb, i)
-      )
-      or
-      ssaDefReachesRank(bb, def, rnk - 1, v) and
-      rnk = refRank(bb, _, v, Read())
-    }
-
-    cached
-    private predicate ssaDefReachesRankCached(
-      BasicBlock bb, Definition def, int rnk, SourceVariable v
-    ) {
+    predicate ssaDefReachesRank(BasicBlock bb, Definition def, int rnk, SourceVariable v) {
       exists(int i |
         rnk = refRank(bb, i, v, Def()) and
         def.definesAt(v, bb, i)
@@ -569,15 +511,6 @@ private module MakeImpl<
       rnk = refRank(bb, _, v, Read())
     }
 
-    pragma[inline]
-    predicate ssaDefReachesRank(BasicBlock bb, Definition def, int rnk, SourceVariable v) {
-      not CacheDefinitionReachability::enabled() and
-      ssaDefReachesRankUncached(bb, def, rnk, v)
-      or
-      CacheDefinitionReachability::enabled() and
-      ssaDefReachesRankCached(bb, def, rnk, v)
-    }
-
     /**
      * Holds if `v` is live at the end of basic block `bb` with the same value as at
      * the end of the immediate dominator, `idom`, of `bb`.
@@ -595,30 +528,7 @@ private module MakeImpl<
      * SSA definition of `v`.
      */
     pragma[nomagic]
-    private predicate ssaDefReachesEndOfBlockUncached(
-      BasicBlock bb, Definition def, SourceVariable v
-    ) {
-      exists(int last |
-        last = maxRefRank(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and
-        ssaDefReachesRank(bb, def, last, v) and
-        liveAtExit(bb, v)
-      )
-      or
-      exists(BasicBlock idom |
-        // The construction of SSA form ensures that each read of a variable is
-        // dominated by its definition. An SSA definition therefore reaches a
-        // control flow node if it is the _closest_ SSA definition that dominates
-        // the node. If two definitions dominate a node then one must dominate the
-        // other, so therefore the definition of _closest_ is given by the dominator
-        // tree. Thus, reaching definitions can be calculated in terms of dominance.
-        ssaDefReachesEndOfBlock(idom, def, v) and
-        liveThrough(idom, bb, v)
-      )
-    }
-
-    pragma[nomagic]
-    cached
-    private predicate ssaDefReachesEndOfBlockCached(BasicBlock bb, Definition def, SourceVariable v) {
+    predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
       exists(int last |
         last = maxRefRank(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and
         ssaDefReachesRank(bb, def, last, v) and
@@ -637,15 +547,6 @@ private module MakeImpl<
       )
     }
 
-    pragma[inline]
-    predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
-      not CacheDefinitionReachability::enabled() and
-      ssaDefReachesEndOfBlockUncached(bb, def, v)
-      or
-      CacheDefinitionReachability::enabled() and
-      ssaDefReachesEndOfBlockCached(bb, def, v)
-    }
-
     /**
      * Holds if the SSA definition of `v` at `def` reaches index `i` in its own
      * basic block `bb`, without crossing another SSA definition of `v`.
@@ -2301,33 +2202,3 @@ private module MakeImpl<
     }
   }
 }
-
-/** Provides the default demand-specialized SSA implementation. */
-module Make<
-  LocationSig Location, BB::CfgSig<Location> Cfg, InputSig<Location, Cfg::BasicBlock> Input>
-{
-  import MakeImpl<Location, Cfg, Input, NoLivenessCaching, NoDefinitionReachabilityCaching>
-}
-
-/**
- * Provides an SSA implementation that caches the complete source-variable liveness relation.
- *
- * Use this when the same SSA instantiation is exposed through multiple cached API stages.
- */
-module MakeWithCachedLiveness<
-  LocationSig Location, BB::CfgSig<Location> Cfg, InputSig<Location, Cfg::BasicBlock> Input>
-{
-  import MakeImpl<Location, Cfg, Input, LivenessCaching, NoDefinitionReachabilityCaching>
-}
-
-/**
- * Provides an SSA implementation that caches complete source-variable liveness and
- * definition-reachability relations.
- *
- * Use this when the same SSA instantiation is exposed through multiple cached API stages.
- */
-module MakeWithCachedLivenessAndDefinitionReachability<
-  LocationSig Location, BB::CfgSig<Location> Cfg, InputSig<Location, Cfg::BasicBlock> Input>
-{
-  import MakeImpl<Location, Cfg, Input, LivenessCaching, DefinitionReachabilityCaching>
-}