Skip to content

SSA: Update data flow integration and BarrierGuard interface to use GuardValue. #20132

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.

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

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
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
Original file line number Diff line number Diff line change
Expand Up @@ -1982,19 +1982,23 @@ module IteratorFlow {

predicate allowFlowIntoUncertainDef(IteratorSsa::UncertainWriteDefinition def) { any() }

class GuardValue = Void;

class Guard extends Void {
predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
predicate hasValueBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue val
) {
none()
}

predicate controlsBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch
predicate valueControlsBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue val
) {
none()
}
}

predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) {
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, GuardValue val) {
none()
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -961,6 +961,8 @@ class GlobalDef extends Definition {
private module SsaImpl = SsaImplCommon::Make<Location, SsaInput>;

private module DataFlowIntegrationInput implements SsaImpl::DataFlowIntegrationInputSig {
private import codeql.util.Boolean

class Expr extends Instruction {
Expr() {
exists(IRBlock bb, int i |
Expand Down Expand Up @@ -992,23 +994,29 @@ private module DataFlowIntegrationInput implements SsaImpl::DataFlowIntegrationI
result instanceof FalseEdge
}

class GuardValue = Boolean;

class Guard instanceof IRGuards::IRGuardCondition {
string toString() { result = super.toString() }

predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
predicate hasValueBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue branch
) {
exists(EdgeKind kind |
super.getBlock() = bb1 and
kind = getConditionalEdge(branch) and
bb1.getSuccessor(kind) = bb2
)
}

predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
this.hasBranchEdge(bb1, bb2, branch)
predicate valueControlsBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue branch
) {
this.hasValueBranchEdge(bb1, bb2, branch)
}
}

predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) {
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, GuardValue branch) {
guard.(IRGuards::IRGuardCondition).controls(bb, branch)
}

Expand Down Expand Up @@ -1037,7 +1045,8 @@ module BarrierGuardWithIntParam<guardChecksNodeSig/4 guardChecksNode> {
}

private predicate guardChecks(
DataFlowIntegrationInput::Guard g, SsaImpl::Definition def, boolean branch, int indirectionIndex
DataFlowIntegrationInput::Guard g, SsaImpl::Definition def,
DataFlowIntegrationInput::GuardValue branch, int indirectionIndex
) {
exists(UseImpl use |
guardChecksNode(g, use.getNode(), branch, indirectionIndex) and
Expand Down
14 changes: 9 additions & 5 deletions csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -975,7 +975,8 @@ private module Cached {
cached // nothing is actually cached
module BarrierGuard<guardChecksSig/3 guardChecks> {
private predicate guardChecksAdjTypes(
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, boolean branch
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e,
DataFlowIntegrationInput::GuardValue branch
) {
exists(Guards::AbstractValues::BooleanValue v |
guardChecks(g, e.getAstNode(), v) and
Expand Down Expand Up @@ -1016,6 +1017,7 @@ string getToStringPrefix(Definition def) {
private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
private import csharp as Cs
private import semmle.code.csharp.controlflow.BasicBlocks
private import codeql.util.Boolean

class Expr extends ControlFlow::Node {
predicate hasCfgNode(ControlFlow::BasicBlock bb, int i) { this = bb.getNode(i) }
Expand All @@ -1042,12 +1044,14 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
)
}

class GuardValue = Boolean;

class Guard extends Guards::Guard {
/**
* Holds if the evaluation of this guard to `branch` corresponds to the edge
* from `bb1` to `bb2`.
*/
predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
predicate hasValueBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue branch) {
exists(ControlFlow::SuccessorTypes::ConditionalSuccessor s |
this.getAControlFlowNode() = bb1.getLastNode() and
bb2 = bb1.getASuccessorByType(s) and
Expand All @@ -1060,13 +1064,13 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
* branch edge from `bb1` to `bb2`. That is, following the edge from
* `bb1` to `bb2` implies that this guard evaluated to `branch`.
*/
predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
this.hasBranchEdge(bb1, bb2, branch)
predicate valueControlsBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue branch) {
this.hasValueBranchEdge(bb1, bb2, branch)
}
}

/** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
predicate guardDirectlyControlsBlock(Guard guard, ControlFlow::BasicBlock bb, boolean branch) {
predicate guardDirectlyControlsBlock(Guard guard, ControlFlow::BasicBlock bb, GuardValue branch) {
exists(ConditionBlock conditionBlock, ControlFlow::SuccessorTypes::ConditionalSuccessor s |
guard.getAControlFlowNode() = conditionBlock.getLastNode() and
s.getValue() = branch and
Expand Down
18 changes: 10 additions & 8 deletions java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -563,9 +563,9 @@ private module Cached {
cached // nothing is actually cached
module BarrierGuard<guardChecksSig/3 guardChecks> {
private predicate guardChecksAdjTypes(
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, boolean branch
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, Guards::GuardValue val
) {
guardChecks(g, e, branch)
guardChecks(g, e, val.asBooleanValue())
}

private Node getABarrierNodeImpl() {
Expand Down Expand Up @@ -657,16 +657,18 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
def instanceof SsaUncertainImplicitUpdate
}

class GuardValue = Guards::GuardValue;

class Guard = Guards::Guard;

/** Holds if the guard `guard` directly controls block `bb` upon evaluating to `branch`. */
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, boolean branch) {
guard.directlyControls(bb, branch)
/** Holds if the guard `guard` directly controls block `bb` upon evaluating to `val`. */
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, GuardValue val) {
guard.directlyValueControls(bb, val)
}

/** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
predicate guardControlsBlock(Guard guard, BasicBlock bb, boolean branch) {
guard.controls(bb, branch)
/** Holds if the guard `guard` controls block `bb` upon evaluating to `val`. */
predicate guardControlsBlock(Guard guard, BasicBlock bb, GuardValue val) {
guard.valueControls(bb, val)
}

predicate includeWriteDefsInFlowStep() { none() }
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -193,6 +193,8 @@ private module ConditionGuardDominators {
module MakeStateBarrierGuard<
FlowStateSig FlowState, WithFlowState<FlowState>::BarrierGuardSig BaseGuard>
{
private import codeql.util.Boolean

final private class FinalNode = DataFlow::Node;

abstract private class BarrierGuard extends FinalNode {
Expand Down Expand Up @@ -295,7 +297,7 @@ module MakeStateBarrierGuard<
}

private predicate ssa2GuardChecks(
Ssa2::SsaDataflowInput::Guard guard, Ssa2::SsaDataflowInput::Expr test, boolean branch,
Ssa2::SsaDataflowInput::Guard guard, Ssa2::SsaDataflowInput::Expr test, Boolean branch,
FlowState state
) {
exists(BarrierGuard g |
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ private import semmle.javascript.dataflow.internal.sharedlib.FlowSummaryImpl as
private import semmle.javascript.dataflow.internal.FlowSummaryPrivate as FlowSummaryPrivate
private import semmle.javascript.dataflow.internal.BarrierGuards
private import semmle.javascript.dataflow.internal.sharedlib.Ssa as Ssa2
private import codeql.util.Boolean

cached
predicate defaultAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2) {
Expand Down Expand Up @@ -37,7 +38,7 @@ predicate defaultAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2,
}

private predicate guardChecksFalsy(
Ssa2::SsaDataflowInput::Guard g, Ssa2::SsaDataflowInput::Expr e, boolean outcome
Ssa2::SsaDataflowInput::Guard g, Ssa2::SsaDataflowInput::Expr e, Boolean outcome
) {
exists(ConditionGuardNode guard |
guard.getTest() = g and
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,8 @@ module SsaConfig implements InputSig<js::DbLocation> {
import Make<js::DbLocation, SsaConfig>

module SsaDataflowInput implements DataFlowIntegrationInputSig {
private import codeql.util.Boolean

class Expr extends js::ControlFlowNode {
Expr() { this = any(SsaConfig::SourceVariable v).getAUse() }

Expand All @@ -71,14 +73,16 @@ module SsaDataflowInput implements DataFlowIntegrationInputSig {
)
}

class GuardValue = Boolean;

class Guard extends js::ControlFlowNode {
Guard() { this = any(js::ConditionGuardNode g).getTest() }

/**
* Holds if the evaluation of this guard to `branch` corresponds to the edge
* from `bb1` to `bb2`.
*/
predicate hasBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, boolean branch) {
predicate hasValueBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, GuardValue branch) {
exists(js::ConditionGuardNode g |
g.getTest() = this and
bb1 = this.getBasicBlock() and
Expand All @@ -92,13 +96,13 @@ module SsaDataflowInput implements DataFlowIntegrationInputSig {
* branch edge from `bb1` to `bb2`. That is, following the edge from
* `bb1` to `bb2` implies that this guard evaluated to `branch`.
*/
predicate controlsBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, boolean branch) {
this.hasBranchEdge(bb1, bb2, branch)
predicate valueControlsBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, GuardValue branch) {
this.hasValueBranchEdge(bb1, bb2, branch)
}
}

pragma[inline]
predicate guardDirectlyControlsBlock(Guard guard, js::BasicBlock bb, boolean branch) {
predicate guardDirectlyControlsBlock(Guard guard, js::BasicBlock bb, GuardValue branch) {
exists(js::ConditionGuardNode g |
g.getTest() = guard and
g.dominates(bb) and
Expand Down
18 changes: 13 additions & 5 deletions ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -400,7 +400,8 @@
cached // nothing is actually cached
module BarrierGuard<guardChecksSig/3 guardChecks> {
private predicate guardChecksAdjTypes(
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, boolean branch
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e,
DataFlowIntegrationInput::GuardValue branch
) {
guardChecks(g, e, branch)
}
Expand Down Expand Up @@ -475,6 +476,7 @@

private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
private import codeql.ruby.controlflow.internal.Guards as Guards
private import codeql.util.Boolean

class Expr extends Cfg::CfgNodes::ExprCfgNode {
predicate hasCfgNode(SsaInput::BasicBlock bb, int i) { this = bb.getNode(i) }
Expand All @@ -486,12 +488,16 @@
any(ParameterExt p).isInitializedBy(def) or def.(Ssa::WriteDefinition).assigns(_)
}

class GuardValue = Boolean;

class Guard extends Cfg::CfgNodes::AstCfgNode {
/**
* Holds if the evaluation of this guard to `branch` corresponds to the edge
* from `bb1` to `bb2`.
*/
predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
predicate hasValueBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue branch
) {
exists(Cfg::SuccessorTypes::ConditionalSuccessor s |
this.getBasicBlock() = bb1 and
bb2 = bb1.getASuccessor(s) and
Expand All @@ -504,13 +510,15 @@
* branch edge from `bb1` to `bb2`. That is, following the edge from
* `bb1` to `bb2` implies that this guard evaluated to `branch`.
*/
predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
this.hasBranchEdge(bb1, bb2, branch)
predicate valueControlsBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue branch
) {
this.hasValueBranchEdge(bb1, bb2, branch)
}
}

/** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) {
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, GuardValue branch) {
Guards::guardControlsBlock(guard, bb, branch)
}
}
Expand Down
18 changes: 13 additions & 5 deletions rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -301,7 +301,8 @@ private module Cached {
cached // nothing is actually cached
module BarrierGuard<guardChecksSig/3 guardChecks> {
private predicate guardChecksAdjTypes(
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, boolean branch
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e,
DataFlowIntegrationInput::GuardValue branch
) {
guardChecks(g, e, branch)
}
Expand All @@ -320,6 +321,7 @@ private import codeql.rust.dataflow.Ssa

private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
private import codeql.rust.dataflow.internal.DataFlowImpl as DataFlowImpl
private import codeql.util.Boolean

class Expr extends CfgNodes::AstCfgNode {
predicate hasCfgNode(SsaInput::BasicBlock bb, int i) { this = bb.getNode(i) }
Expand Down Expand Up @@ -348,12 +350,16 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
)
}

class GuardValue = Boolean;

class Guard extends CfgNodes::AstCfgNode {
/**
* Holds if the evaluation of this guard to `branch` corresponds to the edge
* from `bb1` to `bb2`.
*/
predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
predicate hasValueBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue branch
) {
exists(Cfg::ConditionalSuccessor s |
this = bb1.getANode() and
bb2 = bb1.getASuccessor(s) and
Expand All @@ -366,13 +372,15 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
* branch edge from `bb1` to `bb2`. That is, following the edge from
* `bb1` to `bb2` implies that this guard evaluated to `branch`.
*/
predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
this.hasBranchEdge(bb1, bb2, branch)
predicate valueControlsBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue branch
) {
this.hasValueBranchEdge(bb1, bb2, branch)
}
}

/** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) {
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, GuardValue branch) {
exists(ConditionBasicBlock conditionBlock, ConditionalSuccessor s |
guard = conditionBlock.getLastNode() and
s.getValue() = branch and
Expand Down
8 changes: 5 additions & 3 deletions shared/dataflow/codeql/dataflow/VariableCapture.qll
Original file line number Diff line number Diff line change
Expand Up @@ -733,13 +733,15 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
predicate hasCfgNode(BasicBlock bb, int i) { bb.getNode(i) = this }
}

class GuardValue = Void;

class Guard extends Void {
predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { none() }
predicate hasValueBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue val) { none() }

predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { none() }
predicate valueControlsBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue val) { none() }
}

predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, boolean branch) { none() }
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, GuardValue val) { none() }

predicate includeWriteDefsInFlowStep() { none() }

Expand Down
Loading
Loading