SSA/VariableCapture: Use shared BasicBlock signature.

This commit is contained in:
Anders Schack-Mulligen
2025-08-18 16:00:14 +02:00
parent bb3abc815f
commit e53b22dfa7
5 changed files with 52 additions and 96 deletions

View File

@@ -164,6 +164,9 @@ signature module CfgSig<LocationSig Location> {
* means that the edge `(bb1, bb2)` dominates `bb3`.
*/
predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2);
/** Holds if `bb` is an entry basic block. */
predicate entryBlock(BasicBlock bb);
}
/**
@@ -398,6 +401,9 @@ module Make<LocationSig Location, InputSig<Location> Input> implements CfgSig<Lo
forall(BasicBlock pred | pred = bb2.getAPredecessor() and pred != bb1 | bb2.dominates(pred))
}
/** Holds if `bb` is an entry basic block. */
predicate entryBlock(BasicBlock bb) { nodeIsDominanceEntry(bb.getFirstNode()) }
cached
private module Cached {
private Node nodeGetAPredecessor(Node node, SuccessorType s) {
@@ -466,9 +472,6 @@ module Make<LocationSig Location, InputSig<Location> Input> implements CfgSig<Lo
cached
Node getNode(BasicBlock bb, int pos) { bbIndex(bb.getFirstNode(), result, pos) }
/** Holds if `bb` is an entry basic block. */
private predicate entryBB(BasicBlock bb) { nodeIsDominanceEntry(bb.getFirstNode()) }
cached
predicate bbSuccessor(BasicBlock bb1, BasicBlock bb2, SuccessorType t) {
bb2.getFirstNode() = nodeGetASuccessor(bb1.getLastNode(), t)
@@ -483,7 +486,7 @@ module Make<LocationSig Location, InputSig<Location> Input> implements CfgSig<Lo
/** Holds if `dom` is an immediate dominator of `bb`. */
cached
predicate bbIDominates(BasicBlock dom, BasicBlock bb) =
idominance(entryBB/1, succBB/2)(_, dom, bb)
idominance(entryBlock/1, succBB/2)(_, dom, bb)
/** Holds if `pred` is a basic block predecessor of `succ`. */
private predicate predBB(BasicBlock succ, BasicBlock pred) { succBB(pred, succ) }

View File

@@ -8,47 +8,14 @@ module;
private import codeql.util.Boolean
private import codeql.util.Unit
private import codeql.util.Location
private import codeql.controlflow.BasicBlock as BB
private import codeql.ssa.Ssa as Ssa
signature module InputSig<LocationSig Location> {
/**
* A basic block, that is, a maximal straight-line sequence of control flow nodes
* without branches or joins.
*/
class BasicBlock {
/** Gets a textual representation of this basic block. */
string toString();
signature class BasicBlockSig;
/** Gets the `i`th node in this basic block. */
ControlFlowNode getNode(int i);
/** Gets the length of this basic block. */
int length();
/** Gets the enclosing callable. */
Callable getEnclosingCallable();
/** Gets the location of this basic block. */
Location getLocation();
BasicBlock getASuccessor();
BasicBlock getImmediateDominator();
predicate inDominanceFrontier(BasicBlock df);
}
/** A control flow node. */
class ControlFlowNode {
/** Gets a textual representation of this control flow node. */
string toString();
/** Gets the location of this control flow node. */
Location getLocation();
}
/** Holds if `bb` is a control-flow entry point. */
default predicate entryBlock(BasicBlock bb) { not exists(bb.getImmediateDominator()) }
signature module InputSig<LocationSig Location, BasicBlockSig BasicBlock> {
/** Gets the enclosing callable of the basic block. */
Callable basicBlockGetEnclosingCallable(BasicBlock bb);
/** A variable that is captured in a closure. */
class CapturedVariable {
@@ -134,7 +101,9 @@ signature module InputSig<LocationSig Location> {
}
}
signature module OutputSig<LocationSig Location, InputSig<Location> I> {
signature module OutputSig<
LocationSig Location, BasicBlockSig BasicBlock, InputSig<Location, BasicBlock> I>
{
/**
* A data flow node that we need to reference in the step relations for
* captured variables.
@@ -236,9 +205,18 @@ signature module OutputSig<LocationSig Location, InputSig<Location> I> {
* Constructs the type `ClosureNode` and associated step relations, which are
* intended to be included in the data-flow node and step relations.
*/
module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig<Location, Input> {
module Flow<
LocationSig Location, BB::CfgSig<Location> Cfg, InputSig<Location, Cfg::BasicBlock> Input>
implements OutputSig<Location, Cfg::BasicBlock, Input>
{
private import Input
final private class CfgBb = Cfg::BasicBlock;
private class BasicBlock extends CfgBb {
Callable getEnclosingCallable() { result = basicBlockGetEnclosingCallable(this) }
}
additional module ConsistencyChecks {
final private class FinalExpr = Expr;
@@ -318,12 +296,12 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
query predicate localDominator(RelevantBasicBlock bb, string msg) {
msg = "BasicBlock has non-local dominator" and
bb.getEnclosingCallable() != bb.getImmediateDominator().getEnclosingCallable()
bb.getEnclosingCallable() != bb.getImmediateDominator().(BasicBlock).getEnclosingCallable()
}
query predicate localSuccessor(RelevantBasicBlock bb, string msg) {
msg = "BasicBlock has non-local successor" and
bb.getEnclosingCallable() != bb.getASuccessor().getEnclosingCallable()
bb.getEnclosingCallable() != bb.getASuccessor().(BasicBlock).getEnclosingCallable()
}
query predicate uniqueDefiningScope(CapturedVariable v, string msg) {
@@ -650,7 +628,7 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
/** Holds if `cc` needs a definition at the entry of its callable scope. */
private predicate entryDef(CaptureContainer cc, BasicBlock bb, int i) {
exists(Callable c |
entryBlock(bb) and
Cfg::entryBlock(bb) and
pragma[only_bind_out](bb.getEnclosingCallable()) = c and
i =
min(int j |
@@ -666,14 +644,10 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
)
}
private module CaptureSsaInput implements Ssa::InputSig<Location> {
final class BasicBlock = Input::BasicBlock;
final class ControlFlowNode = Input::ControlFlowNode;
private module CaptureSsaInput implements Ssa::InputSig<Location, Cfg::BasicBlock> {
class SourceVariable = CaptureContainer;
predicate variableWrite(BasicBlock bb, int i, SourceVariable cc, boolean certain) {
predicate variableWrite(Cfg::BasicBlock bb, int i, SourceVariable cc, boolean certain) {
Cached::ref() and
(
exists(CapturedVariable v | cc = TVariable(v) and captureWrite(v, bb, i, true, _))
@@ -683,9 +657,9 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
certain = true
}
predicate variableRead(BasicBlock bb, int i, SourceVariable cc, boolean certain) {
predicate variableRead(Cfg::BasicBlock bb, int i, SourceVariable cc, boolean certain) {
(
synthThisQualifier(bb, i) and cc = TThis(bb.getEnclosingCallable())
synthThisQualifier(bb, i) and cc = TThis(bb.(BasicBlock).getEnclosingCallable())
or
exists(CapturedVariable v | cc = TVariable(v) |
captureRead(v, bb, i, true, _) or synthRead(v, bb, i, true, _)
@@ -695,26 +669,30 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
}
}
private module CaptureSsa = Ssa::Make<Location, CaptureSsaInput>;
private module CaptureSsa = Ssa::Make<Location, Cfg, CaptureSsaInput>;
private module DataFlowIntegrationInput implements CaptureSsa::DataFlowIntegrationInputSig {
private import codeql.util.Void
class Expr instanceof Input::ControlFlowNode {
class Expr instanceof Cfg::ControlFlowNode {
string toString() { result = super.toString() }
predicate hasCfgNode(BasicBlock bb, int i) { bb.getNode(i) = this }
predicate hasCfgNode(Cfg::BasicBlock bb, int i) { bb.getNode(i) = this }
}
class GuardValue = Void;
class Guard extends Void {
predicate hasValueBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue val) { none() }
predicate hasValueBranchEdge(Cfg::BasicBlock bb1, Cfg::BasicBlock bb2, GuardValue val) {
none()
}
predicate valueControlsBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue val) { none() }
predicate valueControlsBranchEdge(Cfg::BasicBlock bb1, Cfg::BasicBlock bb2, GuardValue val) {
none()
}
}
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, GuardValue val) { none() }
predicate guardDirectlyControlsBlock(Guard guard, Cfg::BasicBlock bb, GuardValue val) { none() }
predicate includeWriteDefsInFlowStep() { none() }

View File

@@ -3,6 +3,7 @@ version: 2.0.14-dev
groups: shared
library: true
dependencies:
codeql/controlflow: ${workspace}
codeql/ssa: ${workspace}
codeql/typetracking: ${workspace}
codeql/util: ${workspace}

View File

@@ -5,44 +5,14 @@
overlay[local?]
module;
private import codeql.controlflow.BasicBlock as BB
private import codeql.util.Location
private import codeql.util.Unit
signature class BasicBlockSig;
/** Provides the input specification of the SSA implementation. */
signature module InputSig<LocationSig Location> {
/**
* A basic block, that is, a maximal straight-line sequence of control flow nodes
* without branches or joins.
*/
class BasicBlock {
/** Gets a textual representation of this basic block. */
string toString();
/** Gets the `i`th node in this basic block. */
ControlFlowNode getNode(int i);
/** Gets the length of this basic block. */
int length();
/** Gets the location of this basic block. */
Location getLocation();
BasicBlock getASuccessor();
BasicBlock getImmediateDominator();
predicate inDominanceFrontier(BasicBlock df);
}
/** A control flow node. */
class ControlFlowNode {
/** Gets a textual representation of this control flow node. */
string toString();
/** Gets the location of this control flow node. */
Location getLocation();
}
signature module InputSig<LocationSig Location, BasicBlockSig BasicBlock> {
/** A variable that can be SSA converted. */
class SourceVariable {
/** Gets a textual representation of this variable. */
@@ -89,7 +59,10 @@ signature module InputSig<LocationSig Location> {
* NB: If this predicate is exposed, it should be cached.
* ```
*/
module Make<LocationSig Location, InputSig<Location> Input> {
module Make<
LocationSig Location, BB::CfgSig<Location> Cfg, InputSig<Location, Cfg::BasicBlock> Input>
{
private import Cfg
private import Input
private BasicBlock getABasicBlockPredecessor(BasicBlock bb) { result.getASuccessor() = bb }

View File

@@ -3,5 +3,6 @@ version: 2.0.6-dev
groups: shared
library: true
dependencies:
codeql/controlflow: ${workspace}
codeql/util: ${workspace}
warnOnImplicitThis: true