Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
hvitved committed Jul 5, 2024
1 parent 29222e6 commit 1d5e5ac
Show file tree
Hide file tree
Showing 9 changed files with 2,053 additions and 1,006 deletions.
1,872 changes: 1,055 additions & 817 deletions java/ql/lib/semmle/code/java/dataflow/SSA.qll

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ class BaseSsaSourceVariable extends TBaseSsaSourceVariable {
}

cached
private module SsaImpl {
private module BaseSsaImpl {
/** Gets the destination variable of an update of a tracked variable. */
cached
BaseSsaSourceVariable getDestVar(VariableUpdate upd) {
Expand Down Expand Up @@ -436,7 +436,7 @@ private module SsaImpl {
}
}

private import SsaImpl
private import BaseSsaImpl
private import SsaDefReaches
import SsaPublic

Expand Down
118 changes: 13 additions & 105 deletions java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ private import FlowSummaryImpl as FlowSummaryImpl
private import DataFlowImplCommon as DataFlowImplCommon
private import semmle.code.java.controlflow.Guards
private import semmle.code.java.dataflow.RangeUtils
private import SsaImpl as SsaImpl

/** Gets a string for approximating the name of a field. */
string approximateFieldContent(FieldContent fc) { result = fc.getField().getName().prefix(1) }
Expand All @@ -22,117 +23,24 @@ private predicate deadcode(Expr e) {
}

module SsaFlow {
import codeql.ssa.Ssa
module Impl = SsaImpl::DataFlowIntegration;

private module SsaInput implements InputSig<Location> {
private import semmle.code.java.controlflow.BasicBlocks as BB
private import semmle.code.java.controlflow.Dominance as Dom
private import semmle.code.java.ControlFlowGraph as Cfg

class BasicBlock = BB::BasicBlock;

class ControlFlowNode = Cfg::ControlFlowNode;

BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { Dom::bbIDominates(result, bb) }

BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getABBSuccessor() }

class ExitBasicBlock extends BasicBlock {
ExitBasicBlock() { not exists(this.getABBSuccessor()) }
}

class SourceVariable = LocalScopeVariable;

predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
bb.getNode(i) =
any(VariableUpdate upd |
v.getAnAccess() = upd.(Assignment).getDest()
or
v = upd.(LocalVariableDeclExpr).getVariable()
or
v.getAnAccess() = upd.(UnaryAssignExpr).getExpr()
) and
certain = true
or
exists(Callable c |
bb = c.getBody() and
i = -1 and
v = c.getAParameter() and
certain = true
)
}

predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
bb.getNode(i).(VarRead).getVariable() = v and certain = true
}
}

module SsaImpl = Make<Location, SsaInput>;

module IntegrationInput implements SsaImpl::DataFlowIntegrationInputSig {
private import java as J

class Expr instanceof J::Expr {
string toString() { result = super.toString() }

Location getLocation() { result = super.getLocation() }

predicate hasCfgNode(BasicBlock bb, int i) { this = bb.(J::BasicBlock).getNode(i) }
}

class Parameter = J::Parameter;

predicate ssaDefAssigns(SsaImpl::WriteDefinition def, Expr value) {
exists(BasicBlock bb, int i, VariableUpdate upd |
def.definesAt(_, bb, i) and
bb.getNode(i) = upd
|
value = upd.(VariableAssign).getSource() or
value = upd.(AssignOp) or
value = upd.(RecordBindingVariableExpr)
)
}

predicate ssaDefInitializesParam(SsaImpl::WriteDefinition def, Parameter p) {
def.definesAt(p, _, -1)
}

private import semmle.code.java.controlflow.Guards as Guards

class Guard extends Guards::Guard {
predicate hasCfgNode(SsaInput::BasicBlock bb, int i) { this = bb.getNode(i) }
}

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

/** Gets an immediate conditional successor of basic block `bb`, if any. */
SsaInput::BasicBlock getAConditionalBasicBlockSuccessor(SsaInput::BasicBlock bb, boolean branch) {
result = bb.(Guards::ConditionBlock).getTestSuccessor(branch)
}
}

module Integration = SsaImpl::DataFlowIntegration<IntegrationInput>;

Integration::Node asNode(Node n) {
Impl::Node asNode(Node n) {
n = TSsaNode(result)
or
result.(Integration::ExprNode).getExpr() = n.asExpr()
result.(Impl::ExprNode).getExpr() = n.asExpr()
or
result.(Integration::ExprPostUpdateNode).getExpr() =
n.(PostUpdateNode).getPreUpdateNode().asExpr()
result.(Impl::ExprPostUpdateNode).getExpr() = n.(PostUpdateNode).getPreUpdateNode().asExpr()
or
TExplicitParameterNode(result.(Integration::ParameterNode).getParameter()) = n
TExplicitParameterNode(result.(Impl::ParameterNode).getParameter()) = n
}

predicate localFlowStep(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
Integration::localFlowStep(def, asNode(nodeFrom), asNode(nodeTo))
predicate localFlowStep(SsaImpl::Impl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
Impl::localFlowStep(def, asNode(nodeFrom), asNode(nodeTo))
}

predicate localMustFlowStep(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
Integration::localMustFlowStep(def, asNode(nodeFrom), asNode(nodeTo))
predicate localMustFlowStep(SsaImpl::Impl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
Impl::localMustFlowStep(def, asNode(nodeFrom), asNode(nodeTo))
}
}

Expand All @@ -146,7 +54,7 @@ private module Cached {
not e.getType() instanceof VoidType and
not e.getParent*() instanceof Annotation
} or
TSsaNode(SsaFlow::Integration::SsaNode node) or
TSsaNode(SsaFlow::Impl::SsaNode node) or
TExplicitParameterNode(Parameter p) { exists(p.getCallable().getBody()) } or
TImplicitVarargsArray(Call c) {
c.getCallee().isVarargs() and
Expand Down Expand Up @@ -317,11 +225,11 @@ module Public {
}

class SsaNode extends Node, TSsaNode {

Check warning on line 227 in java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll

View workflow job for this annotation

GitHub Actions / qldoc

Missing QLdoc for class DataFlowNodes::Public::SsaNode
private SsaFlow::Integration::SsaNode node;
private SsaFlow::Impl::SsaNode node;

SsaNode() { this = TSsaNode(node) }

SsaFlow::SsaImpl::DefinitionExt getDefinitionExt() { result = node.getDefinitionExt() }
SsaImpl::Impl::DefinitionExt getDefinitionExt() { result = node.getDefinitionExt() }

Check warning on line 232 in java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll

View workflow job for this annotation

GitHub Actions / qldoc

Missing QLdoc for member-predicate DataFlowNodes::Public::SsaNode::getDefinitionExt/0

override Location getLocation() { result = node.getLocation() }

Expand Down
37 changes: 22 additions & 15 deletions java/ql/lib/semmle/code/java/dataflow/internal/DataFlowUtil.qll
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ private import semmle.code.java.dataflow.FlowSummary
private import semmle.code.java.dataflow.InstanceAccess
private import FlowSummaryImpl as FlowSummaryImpl
private import TaintTrackingUtil as TaintTrackingUtil
private import SsaImpl as SsaImpl
private import DataFlowNodes
import DataFlowNodes::Public

Expand Down Expand Up @@ -99,6 +100,10 @@ predicate hasNonlocalValue(FieldRead fr) {
)
}

private predicate capturedVariableRead(Node n) {
n.asExpr().(VarRead).getVariable() instanceof CapturedVariable
}

cached
private module Cached {
/**
Expand Down Expand Up @@ -126,6 +131,10 @@ private module Cached {
simpleLocalFlowStep0(node1, node2, model)
or
SsaFlow::localFlowStep(_, node1, node2) and
not capturedVariableRead(node2) and
not exists(FieldRead fr |
hasNonlocalValue(fr) and fr.getField().isStatic() and fr = node1.asExpr()
) and
not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(node1, _) and
model = ""
or
Expand All @@ -136,6 +145,11 @@ private module Cached {
// prevent recursive call
(any(AdditionalValueStep a).step(_, _) implies any())
}

cached

Check warning on line 149 in java/ql/lib/semmle/code/java/dataflow/internal/DataFlowUtil.qll

View workflow job for this annotation

GitHub Actions / qldoc

Missing QLdoc for classless-predicate DataFlowUtil::Cached::getABarrierNode/3
Node getABarrierNode(Guard guard, SsaVariable def, boolean branch) {
SsaFlow::asNode(result) = SsaImpl::DataFlowIntegration::getABarrierNode(guard, def, branch)
}
}

/**
Expand Down Expand Up @@ -368,23 +382,16 @@ signature predicate guardChecksSig(Guard g, Expr e, boolean branch);
* in data flow and taint tracking.
*/
module BarrierGuard<guardChecksSig/3 guardChecks> {
// pragma[nomagic]
// private predicate guardChecksSsaDef(Guard g, SsaFlow::SsaImpl::Definition def, boolean branch) {
// guardChecks(g, def.get, branch)
// }
pragma[nomagic]
private predicate guardChecksSsaDef(Guard g, SsaVariable v, boolean branch) {
guardChecks(g, v.getAUse(), branch)
}

/** Gets a node that is safely guarded by the given guard check. */
Node getABarrierNode() {
// still needed for fields
exists(Guard g, SsaVariable v, boolean branch, VarRead use |
guardChecks(g, v.getAUse(), branch) and
use = v.getAUse() and
g.controls(use.getBasicBlock(), branch) and
result.asExpr() = use
exists(Guard g, SsaVariable v, boolean branch |
guardChecksSsaDef(g, v, branch) and
result = getABarrierNode(g, v, branch)
)
// or
// exists(Guard g, SsaFlow::SsaImpl::Definition def, boolean branch |
// guardChecksSsaDef(g, def, branch) and
// SsaFlow::asNode(result) = SsaFlow::Integration::getABarrierNode(g, def, branch)
// )
}
}
Loading

0 comments on commit 1d5e5ac

Please sign in to comment.