hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2025-12-16 16:53:25 +01:00
Code Issues Packages Projects Releases Wiki Activity

Guards: Align the SSA signature with the one from shared SSA.

Browse Source
This commit is contained in:
Anders Schack-Mulligen
2025-10-23 10:16:38 +02:00
parent f6cddc9db7
commit f257c7a570
4 changed files with 56 additions and 50 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll
View File

@@ -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(

10
csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll
View File

@@ -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) {

20
java/ql/lib/semmle/code/java/controlflow/Guards.qll
View File

@@ -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;

64
shared/controlflow/codeql/controlflow/Guards.qll
View File

@@ -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