Skip to content

Shared: Align SSA interfaces in Guards and ControlFlowReachability with shared SSA #20680

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Oct 23, 2025
Merged

Shared: Align SSA interfaces in Guards and ControlFlowReachability with shared SSA #20680

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f257c7a
Guards: Align the SSA signature with the one from shared SSA.
aschackmull Oct 23, 2025
72d83cc
ControlFlowReachability: Align the SSA signature with the one from sh…
aschackmull Oct 23, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 7 additions & 5 deletions cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -380,18 +380,20 @@ private module LogicInput_v1 implements GuardsImpl::LogicInputSig {
GuardsInput::Expr getARead() { result = this.getAUse().getDef() }
}

class SsaWriteDefinition extends SsaDefinition instanceof ExplicitDefinition {
GuardsInput::Expr getDefinition() { result = super.getAssignedInstruction() }
class SsaExplicitWrite extends SsaDefinition instanceof ExplicitDefinition {
GuardsInput::Expr getValue() { result = super.getAssignedInstruction() }
}

class SsaPhiNode extends SsaDefinition instanceof PhiNode {
class SsaPhiDefinition extends SsaDefinition instanceof PhiNode {
predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) {
super.hasInputFromBlock(inp, bb)
}
}

predicate parameterDefinition(GuardsInput::Parameter p, SsaDefinition def) {
def.isParameterDefinition(p)
class SsaParameterInit extends SsaDefinition {
SsaParameterInit() { this.isParameterDefinition(_) }

GuardsInput::Parameter getParameter() { this.isParameterDefinition(result) }
Comment on lines +393 to +396
Copy link
Contributor

@jketema jketema Oct 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems to be slightly more than a renaming. Did you check that this doesn't affect join-orders?

Copy link
Contributor Author

@aschackmull aschackmull Oct 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It replaces one binary predicate with another - it shouldn't make a difference whether it's a member predicate. But since you asked, I just did a DIL diff of a suitable query and verified that the generated DIL is equivalent.

}

predicate additionalImpliesStep(
Expand Down
8 changes: 4 additions & 4 deletions csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowReachability.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,13 +33,13 @@ private module ControlFlowInput implements

class SsaDefinition = Ssa::Definition;

class SsaWriteDefinition extends SsaDefinition instanceof Ssa::ExplicitDefinition {
Expr getDefinition() { result = super.getADefinition().getSource() }
class SsaExplicitWrite extends SsaDefinition instanceof Ssa::ExplicitDefinition {
Expr getValue() { result = super.getADefinition().getSource() }
}

class SsaPhiNode = Ssa::PhiNode;
class SsaPhiDefinition = Ssa::PhiNode;

class SsaUncertainDefinition = Ssa::UncertainDefinition;
class SsaUncertainWrite = Ssa::UncertainDefinition;

class GuardValue = Guards::GuardValue;

Expand Down
10 changes: 5 additions & 5 deletions csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -207,18 +207,18 @@ private module LogicInput implements GuardsImpl::LogicInputSig {
Expr getARead() { super.getARead() = result }
}

class SsaWriteDefinition extends SsaDefinition instanceof Ssa::ExplicitDefinition {
Expr getDefinition() { result = super.getADefinition().getSource() }
class SsaExplicitWrite extends SsaDefinition instanceof Ssa::ExplicitDefinition {
Expr getValue() { result = super.getADefinition().getSource() }
}

class SsaPhiNode extends SsaDefinition instanceof Ssa::PhiNode {
class SsaPhiDefinition extends SsaDefinition instanceof Ssa::PhiNode {
predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) {
super.hasInputFromBlock(inp, bb)
}
}

predicate parameterDefinition(Parameter p, SsaDefinition def) {
def.(Ssa::ImplicitParameterDefinition).getParameter() = p
class SsaParameterInit extends SsaDefinition instanceof Ssa::ImplicitParameterDefinition {
Parameter getParameter() { result = super.getParameter() }
}

predicate additionalNullCheck(GuardsImpl::PreGuard guard, GuardValue val, Expr e, boolean isNull) {
Expand Down
8 changes: 4 additions & 4 deletions java/ql/lib/semmle/code/java/controlflow/ControlFlowReachability.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,16 +31,16 @@ private module ControlFlowInput implements InputSig<Location, ControlFlowNode, B

class SsaDefinition = SSA::SsaVariable;

class SsaWriteDefinition extends SsaDefinition instanceof SSA::SsaExplicitUpdate {
Expr getDefinition() {
class SsaExplicitWrite extends SsaDefinition instanceof SSA::SsaExplicitUpdate {
Expr getValue() {
super.getDefiningExpr().(VariableAssign).getSource() = result or
super.getDefiningExpr().(AssignOp) = result
}
}

class SsaPhiNode = SSA::SsaPhiNode;
class SsaPhiDefinition = SSA::SsaPhiNode;

class SsaUncertainDefinition extends SsaDefinition instanceof SSA::SsaUncertainImplicitUpdate {
class SsaUncertainWrite extends SsaDefinition instanceof SSA::SsaUncertainImplicitUpdate {
SsaDefinition getPriorDefinition() { result = super.getPriorDef() }
}

Expand Down
20 changes: 10 additions & 10 deletions java/ql/lib/semmle/code/java/controlflow/Guards.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -415,21 +415,21 @@ private module LogicInput_v1 implements GuardsImpl::LogicInputSig {
GuardsInput::Expr getARead() { result = this.getAUse() }
}

class SsaWriteDefinition extends SsaDefinition instanceof BaseSsaUpdate {
GuardsInput::Expr getDefinition() {
class SsaExplicitWrite extends SsaDefinition instanceof BaseSsaUpdate {
GuardsInput::Expr getValue() {
super.getDefiningExpr().(VariableAssign).getSource() = result or
super.getDefiningExpr().(AssignOp) = result
}
}

class SsaPhiNode extends SsaDefinition instanceof BaseSsaPhiNode {
class SsaPhiDefinition extends SsaDefinition instanceof BaseSsaPhiNode {
predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) {
super.hasInputFromBlock(inp, bb)
}
}

predicate parameterDefinition(Parameter p, SsaDefinition def) {
def.(BaseSsaImplicitInit).isParameterDefinition(p)
class SsaParameterInit extends SsaDefinition instanceof BaseSsaImplicitInit {
Parameter getParameter() { super.isParameterDefinition(result) }
}

predicate additionalNullCheck = LogicInputCommon::additionalNullCheck/4;
Expand All @@ -446,21 +446,21 @@ private module LogicInput_v2 implements GuardsImpl::LogicInputSig {
GuardsInput::Expr getARead() { result = this.getAUse() }
}

class SsaWriteDefinition extends SsaDefinition instanceof SSA::SsaExplicitUpdate {
GuardsInput::Expr getDefinition() {
class SsaExplicitWrite extends SsaDefinition instanceof SSA::SsaExplicitUpdate {
GuardsInput::Expr getValue() {
super.getDefiningExpr().(VariableAssign).getSource() = result or
super.getDefiningExpr().(AssignOp) = result
}
}

class SsaPhiNode extends SsaDefinition instanceof SSA::SsaPhiNode {
class SsaPhiDefinition extends SsaDefinition instanceof SSA::SsaPhiNode {
predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) {
super.hasInputFromBlock(inp, bb)
}
}

predicate parameterDefinition(Parameter p, SsaDefinition def) {
def.(SSA::SsaImplicitInit).isParameterDefinition(p)
class SsaParameterInit extends SsaDefinition instanceof SSA::SsaImplicitInit {
Parameter getParameter() { super.isParameterDefinition(result) }
}

predicate additionalNullCheck = LogicInputCommon::additionalNullCheck/4;
Expand Down
26 changes: 13 additions & 13 deletions shared/controlflow/codeql/controlflow/ControlFlowReachability.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,18 +56,18 @@ signature module InputSig<LocationSig Location, TypSig ControlFlowNode, TypSig B
predicate isLiveAtEndOfBlock(BasicBlock b);
}

class SsaWriteDefinition extends SsaDefinition {
Expr getDefinition();
class SsaExplicitWrite extends SsaDefinition {
Expr getValue();
}

class SsaPhiNode extends SsaDefinition {
class SsaPhiDefinition extends SsaDefinition {
/** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb);

SsaDefinition getAnInput();
}

class SsaUncertainDefinition extends SsaDefinition {
class SsaUncertainWrite extends SsaDefinition {
/**
* Gets the immediately preceding definition. Since this update is uncertain,
* the value from the preceding definition might still be valid.
Expand Down Expand Up @@ -274,9 +274,9 @@ module Make<
* If multiple values apply, including a singleton, then we only include the
* singleton.
*/
private predicate ssaHasValue(SsaWriteDefinition def, GuardValue gv) {
private predicate ssaHasValue(SsaExplicitWrite def, GuardValue gv) {
exists(Expr e |
def.getDefinition() = e and
def.getValue() = e and
exprHasValue(e, gv) and
(any(GuardValue gv0 | exprHasValue(e, gv0)).isSingleton() implies gv.isSingleton())
)
Expand Down Expand Up @@ -398,7 +398,7 @@ module Make<
}

private predicate uncertainStep(SsaDefinition def1, SsaDefinition def2) {
def2.(SsaUncertainDefinition).getPriorDefinition() = def1 and
def2.(SsaUncertainWrite).getPriorDefinition() = def1 and
Config::uncertainFlow()
}

Expand Down Expand Up @@ -459,7 +459,7 @@ module Make<

pragma[nomagic]
private predicate phiBlock(BasicBlock bb, SourceVariable v) {
exists(SsaPhiNode phi | phi.getBasicBlock() = bb and phi.getSourceVariable() = v)
exists(SsaPhiDefinition phi | phi.getBasicBlock() = bb and phi.getSourceVariable() = v)
}

/** Holds if `def1` in `bb1` may step to `def2` in `bb2`. */
Expand All @@ -468,7 +468,7 @@ module Make<
not Config::barrierEdge(bb1, bb2) and
not ssaValueBarrierEdge(def1, bb1, bb2) and
(
def2.(SsaPhiNode).hasInputFromBlock(def1, bb1) and bb2 = def2.getBasicBlock()
def2.(SsaPhiDefinition).hasInputFromBlock(def1, bb1) and bb2 = def2.getBasicBlock()
or
exists(SourceVariable v |
ssaRelevantAtEndOfBlock(def1, bb1) and
Expand Down Expand Up @@ -661,10 +661,10 @@ module Make<
|
def.getBasicBlock().dominates(loopEntry)
or
exists(SsaPhiNode phi |
exists(SsaPhiDefinition phi |
phi.definesAt(var, loopEntry, _) and
phi.getAnInput+() = def and
def.(SsaPhiNode).getAnInput*() = phi
def.(SsaPhiDefinition).getAnInput*() = phi
)
)
}
Expand Down Expand Up @@ -703,7 +703,7 @@ module Make<
pathEdge(src, bb1, bb2) and
relevantSplit(src, var, condgv) and
lastDefInBlock(var, t, bb2) and
not t instanceof SsaPhiNode and
not t instanceof SsaPhiDefinition and
(
exists(GuardValue gv |
ssaHasValue(t, gv) and
Expand All @@ -730,7 +730,7 @@ module Make<
pathEdge(src, bb1, bb2) and
relevantSplit(src, var, condgv) and
lastDefInBlock(var, t2, bb2) and
t2.(SsaPhiNode).hasInputFromBlock(t1, bb1) and
t2.(SsaPhiDefinition).hasInputFromBlock(t1, bb1) and
(
exists(GuardValue gv |
ssaControlsPathEdge(src, t1, _, gv, bb1, bb2) and
Expand Down
Loading
Loading