From f257c7a5701a2d25d04903040c3e2e34aa8f4e6d Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 23 Oct 2025 10:16:38 +0200 Subject: [PATCH 1/2] Guards: Align the SSA signature with the one from shared SSA. --- .../semmle/code/cpp/controlflow/IRGuards.qll | 12 ++-- .../semmle/code/csharp/controlflow/Guards.qll | 10 +-- .../semmle/code/java/controlflow/Guards.qll | 20 +++--- .../controlflow/codeql/controlflow/Guards.qll | 64 ++++++++++--------- 4 files changed, 56 insertions(+), 50 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll b/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll index e9ff5dbf5e48..536e1750fd2f 100644 --- a/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll +++ b/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll @@ -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) } } predicate additionalImpliesStep( diff --git a/csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll b/csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll index f12fa66dde8a..3e33807991a9 100644 --- a/csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll +++ b/csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll @@ -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) { diff --git a/java/ql/lib/semmle/code/java/controlflow/Guards.qll b/java/ql/lib/semmle/code/java/controlflow/Guards.qll index ac46a2a25b72..7bc53226b814 100644 --- a/java/ql/lib/semmle/code/java/controlflow/Guards.qll +++ b/java/ql/lib/semmle/code/java/controlflow/Guards.qll @@ -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; @@ -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; diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 8c65496dce5c..74fefbb4e39c 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -536,16 +536,18 @@ module Make< Location getLocation(); } - 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); } - predicate parameterDefinition(Parameter p, SsaDefinition def); + class SsaParameterInit extends SsaDefinition { + Parameter getParameter(); + } /** * Holds if `guard` evaluating to `val` ensures that: @@ -594,7 +596,7 @@ module Make< * logical inferences from `phi` to `guard` trivial and irrelevant. */ private predicate guardControlsPhiBranch( - Guard guard, GuardValue v, SsaPhiNode phi, SsaDefinition inp + Guard guard, GuardValue v, SsaPhiDefinition phi, SsaDefinition inp ) { exists(BasicBlock bbPhi | phi.hasInputFromBlock(inp, _) and @@ -615,10 +617,12 @@ module Make< * * This makes `phi` similar to the conditional `phi = guard==v ? input : ...`. */ - private predicate guardDeterminesPhiInput(Guard guard, GuardValue v, SsaPhiNode phi, Expr input) { - exists(GuardValue dv, SsaWriteDefinition inp | + private predicate guardDeterminesPhiInput( + Guard guard, GuardValue v, SsaPhiDefinition phi, Expr input + ) { + exists(GuardValue dv, SsaExplicitWrite inp | guardControlsPhiBranch(guard, v, phi, inp) and - inp.getDefinition() = input and + inp.getValue() = input and dv = v.getDualValue() and forall(SsaDefinition other | phi.hasInputFromBlock(other, _) and other != inp | guardControlsPhiBranch(guard, dv, phi, other) @@ -644,7 +648,7 @@ module Make< ) or // An expression `x = ...` can be considered as a read of `x`. - guard.(IdExpr).getEqualChildExpr() = def.(SsaWriteDefinition).getDefinition() + guard.(IdExpr).getEqualChildExpr() = def.(SsaExplicitWrite).getValue() } private predicate valueStep(Expr e1, Expr e2) { @@ -669,10 +673,10 @@ module Make< * through a back edge. */ private SsaDefinition getAnUltimateDefinition(SsaDefinition v, boolean fromBackEdge) { - result = v and not v instanceof SsaPhiNode and fromBackEdge = false + result = v and not v instanceof SsaPhiDefinition and fromBackEdge = false or exists(SsaDefinition inp, BasicBlock bb, boolean fbe | - v.(SsaPhiNode).hasInputFromBlock(inp, bb) and + v.(SsaPhiDefinition).hasInputFromBlock(inp, bb) and result = getAnUltimateDefinition(inp, fbe) and (if v.getBasicBlock().dominates(bb) then fromBackEdge = true else fromBackEdge = fbe) ) @@ -683,9 +687,9 @@ module Make< */ private predicate hasPossibleUnknownValue(SsaDefinition v) { exists(SsaDefinition def | def = getAnUltimateDefinition(v, _) | - not exists(def.(SsaWriteDefinition).getDefinition()) + not exists(def.(SsaExplicitWrite).getValue()) or - exists(Expr e | e = possibleValue(def.(SsaWriteDefinition).getDefinition()) | + exists(Expr e | e = possibleValue(def.(SsaExplicitWrite).getValue()) | not constantHasValue(e, _) ) ) @@ -701,9 +705,9 @@ module Make< */ private predicate possibleValue(SsaDefinition v, boolean fromBackEdge, Expr e, GuardValue k) { not hasPossibleUnknownValue(v) and - exists(SsaWriteDefinition def | + exists(SsaExplicitWrite def | def = getAnUltimateDefinition(v, fromBackEdge) and - e = possibleValue(def.getDefinition()) and + e = possibleValue(def.getValue()) and constantHasValue(e, k) ) } @@ -711,7 +715,7 @@ module Make< /** * Holds if `e` equals `k` and may be assigned to `v` without going through * back edges, and all other possible ultimate definitions of `v` are different - * from `k`. The trivial case where `v` is an `SsaWriteDefinition` with `e` as + * from `k`. The trivial case where `v` is an `SsaExplicitWrite` with `e` as * the only possible value is excluded. */ private predicate uniqueValue(SsaDefinition v, Expr e, GuardValue k) { @@ -727,14 +731,14 @@ module Make< * Holds if `phi` has exactly two inputs, `def1` and `e2`, and that `def1` * does not come from a back-edge into `phi`. */ - private predicate phiWithTwoInputs(SsaPhiNode phi, SsaDefinition def1, Expr e2) { - exists(SsaWriteDefinition def2, BasicBlock bb1 | + private predicate phiWithTwoInputs(SsaPhiDefinition phi, SsaDefinition def1, Expr e2) { + exists(SsaExplicitWrite def2, BasicBlock bb1 | 2 = strictcount(SsaDefinition inp, BasicBlock bb | phi.hasInputFromBlock(inp, bb)) and phi.hasInputFromBlock(def1, bb1) and phi.hasInputFromBlock(def2, _) and def1 != def2 and not phi.getBasicBlock().dominates(bb1) and - def2.getDefinition() = e2 + def2.getValue() = e2 ) } @@ -795,8 +799,8 @@ module Make< baseSsaValueCheck(def, v, g, gv) ) or - exists(SsaWriteDefinition def | - exprHasValue(def.getDefinition(), v) and + exists(SsaExplicitWrite def | + exprHasValue(def.getValue(), v) and e = def.getARead() ) } @@ -841,7 +845,7 @@ module Make< bindingset[def1, v1] pragma[inline_late] private predicate impliesStepSsaGuard(SsaDefinition def1, GuardValue v1, Guard g2, GuardValue v2) { - def1.(SsaWriteDefinition).getDefinition() = g2 and + def1.(SsaExplicitWrite).getValue() = g2 and v1 = v2 and not exprHasValue(g2, v2) // disregard trivial guard or @@ -1032,9 +1036,9 @@ module Make< private predicate validReturnInCustomGuard( ReturnExpr ret, ParameterPosition ppos, GuardValue retval, GuardValue val ) { - exists(NonOverridableMethod m, SsaDefinition param | + exists(NonOverridableMethod m, SsaParameterInit param | m.getAReturnExpr() = ret and - parameterDefinition(m.getParameter(ppos), param) + param.getParameter() = m.getParameter(ppos) | exists(Guard g0, GuardValue v0 | directlyControlsReturn(g0, v0, ret) and @@ -1071,8 +1075,8 @@ module Make< validReturnInCustomGuard(ret, ppos, retval, val) ) or - exists(SsaDefinition param, Guard g0, GuardValue v0 | - parameterDefinition(result.getParameter(ppos), param) and + exists(SsaParameterInit param, Guard g0, GuardValue v0 | + param.getParameter() = result.getParameter(ppos) and guardDirectlyControlsExit(g0, v0) and retval = TException(false) and BranchImplies::ssaControls(param, val, g0, v0) @@ -1141,9 +1145,9 @@ module Make< private predicate validReturnInValidationWrapper( ReturnExpr ret, ParameterPosition ppos, GuardValue retval, State state ) { - exists(NonOverridableMethod m, SsaDefinition param, Guard guard, GuardValue val | + exists(NonOverridableMethod m, SsaParameterInit param, Guard guard, GuardValue val | m.getAReturnExpr() = ret and - parameterDefinition(m.getParameter(ppos), param) and + param.getParameter() = m.getParameter(ppos) and guardChecksDef(guard, param, val, state) | guard.valueControls(ret.getBasicBlock(), val) and @@ -1171,8 +1175,8 @@ module Make< validReturnInValidationWrapper(ret, ppos, retval, state) ) or - exists(SsaDefinition param, BasicBlock bb, Guard guard, GuardValue val | - parameterDefinition(result.getParameter(ppos), param) and + exists(SsaParameterInit param, BasicBlock bb, Guard guard, GuardValue val | + param.getParameter() = result.getParameter(ppos) and guardChecksDef(guard, param, val, state) and guard.valueControls(bb, val) and normalExitBlock(bb) and From 72d83cc966694b81f6e97c7ba1d263e45209d9d6 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 23 Oct 2025 10:57:21 +0200 Subject: [PATCH 2/2] ControlFlowReachability: Align the SSA signature with the one from shared SSA. --- .../controlflow/ControlFlowReachability.qll | 8 +++--- .../controlflow/ControlFlowReachability.qll | 8 +++--- .../controlflow/ControlFlowReachability.qll | 26 +++++++++---------- 3 files changed, 21 insertions(+), 21 deletions(-) diff --git a/csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowReachability.qll b/csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowReachability.qll index 9d9e3f8d458b..aafe14402c7f 100644 --- a/csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowReachability.qll +++ b/csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowReachability.qll @@ -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; diff --git a/java/ql/lib/semmle/code/java/controlflow/ControlFlowReachability.qll b/java/ql/lib/semmle/code/java/controlflow/ControlFlowReachability.qll index fbb384e2b0ed..9fe6b9b0b1df 100644 --- a/java/ql/lib/semmle/code/java/controlflow/ControlFlowReachability.qll +++ b/java/ql/lib/semmle/code/java/controlflow/ControlFlowReachability.qll @@ -31,16 +31,16 @@ private module ControlFlowInput implements InputSig