diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/ImportResolution.qll b/python/ql/lib/semmle/python/dataflow/new/internal/ImportResolution.qll index 095c0938bbf2..75c89fffa6ef 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/ImportResolution.qll +++ b/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. } diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/SsaImpl.qll b/python/ql/lib/semmle/python/dataflow/new/internal/SsaImpl.qll index 41657362c1f1..e5a7e9f6a0be 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/SsaImpl.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/SsaImpl.qll @@ -256,7 +256,7 @@ private module SsaImplInput implements SsaImplCommon::InputSig as Impl +import SsaImplCommon::Make 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; -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. */ diff --git a/python/ql/test/library-tests/dataflow-new-ssa/FacadeAdapterContract.expected b/python/ql/test/library-tests/dataflow-new-ssa/FacadeAdapterContract.expected new file mode 100644 index 000000000000..44989c8cd026 --- /dev/null +++ b/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 | diff --git a/python/ql/test/library-tests/dataflow-new-ssa/FacadeAdapterContract.ql b/python/ql/test/library-tests/dataflow-new-ssa/FacadeAdapterContract.ql new file mode 100644 index 000000000000..78724e7d341d --- /dev/null +++ b/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() + ) +} diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 5dc13fdb7b88..b8fe058bc0f5 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/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 Cfg, InputSig Input, - LivenessCachingSig CacheLiveness, DefinitionReachabilityCachingSig CacheDefinitionReachability> +module Make< + LocationSig Location, BB::CfgSig Cfg, InputSig 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 Cfg, InputSig Input> -{ - import MakeImpl -} - -/** - * 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 Cfg, InputSig Input> -{ - import MakeImpl -} - -/** - * 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 Cfg, InputSig Input> -{ - import MakeImpl -}