Skip to content

Commit

Permalink
Java: Adopt shared SSA data-flow integration (WIP)
Browse files Browse the repository at this point in the history
  • Loading branch information
hvitved committed Jul 8, 2024
1 parent dfda6e8 commit 291e278
Show file tree
Hide file tree
Showing 20 changed files with 228 additions and 946 deletions.
868 changes: 51 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
45 changes: 44 additions & 1 deletion 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 @@ -21,6 +22,32 @@ private predicate deadcode(Expr e) {
)
}

module SsaFlow {
module Impl = SsaImpl::DataFlowIntegration;

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

predicate localFlowStep(
SsaImpl::Impl::DefinitionExt def, Node nodeFrom, Node nodeTo, boolean isUseStep
) {
not def instanceof SsaImpl::UntrackedDef and
Impl::localFlowStep(def, asNode(nodeFrom), asNode(nodeTo), isUseStep)
}

predicate localMustFlowStep(SsaImpl::Impl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
not def instanceof SsaImpl::UntrackedDef and
Impl::localMustFlowStep(def, asNode(nodeFrom), asNode(nodeTo))
}
}

cached
private module Cached {
cached
Expand All @@ -31,6 +58,7 @@ private module Cached {
not e.getType() instanceof VoidType and
not e.getParent*() instanceof Annotation
} 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 @@ -137,6 +165,8 @@ module Public {
result = this.(FieldValueNode).getField().getType()
or
result instanceof TypeObject and this instanceof AdditionalNode
or
result = this.(SsaNode).getDefinitionExt().getSourceVariable().getType()
}

/** Gets the callable in which this node occurs. */
Expand Down Expand Up @@ -198,6 +228,18 @@ module Public {
abstract predicate isParameterOf(DataFlowCallable c, int pos);
}

class SsaNode extends Node, TSsaNode {
private SsaFlow::Impl::SsaNode node;

SsaNode() { this = TSsaNode(node) }

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

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

override string toString() { result = node.toString() }
}

/**
* A parameter, viewed as a node in a data flow graph.
*/
Expand Down Expand Up @@ -398,7 +440,8 @@ module Private {
result.asSummarizedCallable() = n.(FlowSummaryNode).getSummarizedCallable() or
result.asCallable() = n.(CaptureNode).getSynthesizedCaptureNode().getEnclosingCallable() or
result.asFieldScope() = n.(FieldValueNode).getField() or
result.asCallable() = any(Expr e | n.(AdditionalNode).nodeAt(e, _)).getEnclosingCallable()
result.asCallable() = any(Expr e | n.(AdditionalNode).nodeAt(e, _)).getEnclosingCallable() or
result.asCallable() = n.(SsaNode).getDefinitionExt().getBasicBlock().getEnclosingCallable()
}

/** Holds if `p` is a `ParameterNode` of `c` with position `pos`. */
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -610,7 +610,11 @@ predicate forceHighPrecision(Content c) {
}

/** Holds if `n` should be hidden from path explanations. */
predicate nodeIsHidden(Node n) { n instanceof FlowSummaryNode }
predicate nodeIsHidden(Node n) {
n instanceof FlowSummaryNode
or
n instanceof SsaNode
}

class LambdaCallKind = Method; // the "apply" method in the functional interface

Expand Down
77 changes: 33 additions & 44 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 All @@ -108,7 +113,7 @@ private module Cached {
predicate localFlowStep(Node node1, Node node2) {
simpleLocalFlowStep0(node1, node2, _)
or
adjacentUseUse(node1.asExpr(), node2.asExpr())
SsaFlow::localFlowStep(_, node1, node2, _)
or
// Simple flow through library code is included in the exposed local
// step relation, even though flow is technically inter-procedural
Expand All @@ -125,13 +130,31 @@ private module Cached {
predicate simpleLocalFlowStep(Node node1, Node node2, string model) {
simpleLocalFlowStep0(node1, node2, model)
or
exists(boolean isUseStep |
SsaFlow::localFlowStep(_, node1, node2, isUseStep) and
not capturedVariableRead(node2) and
model = ""
|
isUseStep = false
or
not exists(FieldRead fr |
hasNonlocalValue(fr) and fr.getField().isStatic() and fr = node1.asExpr()
) and
not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(node1, _)
)
or
any(AdditionalValueStep a).step(node1, node2) and
pragma[only_bind_out](node1.getEnclosingCallable()) =
pragma[only_bind_out](node2.getEnclosingCallable()) and
model = "AdditionalValueStep" and
// prevent recursive call
(any(AdditionalValueStep a).step(_, _) implies any())
}

cached
Node getABarrierNode(Guard guard, SsaVariable def, boolean branch) {
SsaFlow::asNode(result) = SsaImpl::DataFlowIntegration::getABarrierNode(guard, def, branch)
}
}

/**
Expand All @@ -147,14 +170,7 @@ predicate localMustFlowStep(Node node1, Node node2) {
node2.(ImplicitInstanceAccess).getInstanceAccess().(OwnInstanceAccess).getEnclosingCallable()
)
or
exists(SsaImplicitInit init |
init.isParameterDefinition(node1.asParameter()) and init.getAUse() = node2.asExpr()
)
or
exists(SsaExplicitUpdate upd |
upd.getDefiningExpr().(VariableAssign).getSource() = node1.asExpr() and
upd.getAUse() = node2.asExpr()
)
SsaFlow::localMustFlowStep(_, node1, node2)
or
node2.asExpr().(CastingExpr).getExpr() = node1.asExpr()
or
Expand All @@ -169,10 +185,6 @@ predicate localMustFlowStep(Node node1, Node node2) {

import Cached

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

/**
* Holds if there is a data flow step from `e1` to `e2` that only steps from
* child to parent in the AST.
Expand Down Expand Up @@ -214,34 +226,8 @@ predicate simpleAstFlowStep(Expr e1, Expr e2) {
private predicate simpleLocalFlowStep0(Node node1, Node node2, string model) {
(
TaintTrackingUtil::forceCachingInSameStage() and
// Variable flow steps through adjacent def-use and use-use pairs.
exists(SsaExplicitUpdate upd |
upd.getDefiningExpr().(VariableAssign).getSource() = node1.asExpr() or
upd.getDefiningExpr().(AssignOp) = node1.asExpr() or
upd.getDefiningExpr().(RecordBindingVariableExpr) = node1.asExpr()
|
node2.asExpr() = upd.getAFirstUse() and
not capturedVariableRead(node2)
)
or
exists(SsaImplicitInit init |
init.isParameterDefinition(node1.asParameter()) and
node2.asExpr() = init.getAFirstUse() and
not capturedVariableRead(node2)
)
or
adjacentUseUse(node1.asExpr(), node2.asExpr()) and
not exists(FieldRead fr |
hasNonlocalValue(fr) and fr.getField().isStatic() and fr = node1.asExpr()
) and
not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(node1, _) and
not capturedVariableRead(node2)
or
ThisFlow::adjacentThisRefs(node1, node2)
or
adjacentUseUse(node1.(PostUpdateNode).getPreUpdateNode().asExpr(), node2.asExpr()) and
not capturedVariableRead(node2)
or
ThisFlow::adjacentThisRefs(node1.(PostUpdateNode).getPreUpdateNode(), node2)
or
simpleAstFlowStep(node1.asExpr(), node2.asExpr())
Expand Down Expand Up @@ -401,13 +387,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, SsaVariable v, boolean branch) {
guardChecks(g, v.getAUse(), branch)
}

/** Gets a node that is safely guarded by the given guard check. */
Node getABarrierNode() {
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)
)
}
}
54 changes: 22 additions & 32 deletions java/ql/src/Violations of Best Practice/Dead Code/DeadLocals.qll
Original file line number Diff line number Diff line change
Expand Up @@ -6,46 +6,36 @@ import java
import semmle.code.java.dataflow.SSA
private import semmle.code.java.frameworks.Assertions

private predicate emptyDecl(SsaExplicitUpdate ssa) {
exists(LocalVariableDeclExpr decl |
decl = ssa.getDefiningExpr() and
not exists(decl.getInit()) and
not exists(EnhancedForStmt for | for.getVariable() = decl)
)
private predicate emptyDecl(LocalVariableDeclExpr decl) {
not exists(decl.getInit()) and
not exists(EnhancedForStmt for | for.getVariable() = decl)
}

/**
* A dead SSA variable. Excludes parameters, and phi nodes are never dead, so only includes `VariableUpdate`s.
*/
predicate deadLocal(SsaExplicitUpdate ssa) {
ssa.getSourceVariable().getVariable() instanceof LocalScopeVariable and
not exists(ssa.getAUse()) and
not exists(SsaPhiNode phi | phi.getAPhiInput() = ssa) and
not exists(SsaImplicitInit init | init.captures(ssa)) and
not emptyDecl(ssa) and
not readImplicitly(ssa, _)
/** A dead variable update. */

Check warning

Code scanning / CodeQL

Predicate QLDoc style. Warning

The QLDoc for a predicate without a result should start with 'Holds'.
predicate deadLocal(VariableUpdate upd) {
upd.getDestVar() instanceof LocalScopeVariable and
not exists(SsaExplicitUpdate ssa | upd = ssa.getDefiningExpr()) and
not emptyDecl(upd) and
not readImplicitly(upd, _)
}

/**
* A dead SSA variable that is expected to be dead as indicated by an assertion.
* A dead variable update that is expected to be dead as indicated by an assertion.
*/
predicate expectedDead(SsaExplicitUpdate ssa) {
deadLocal(ssa) and
assertFail(ssa.getBasicBlock(), _)
}
predicate expectedDead(VariableUpdate upd) { assertFail(upd.getBasicBlock(), _) }

/**
* A dead SSA variable that is overwritten by a live SSA definition.
* A dead update that is overwritten by a live update.
*/
predicate overwritten(SsaExplicitUpdate ssa) {
deadLocal(ssa) and
exists(SsaExplicitUpdate overwrite |
overwrite.getSourceVariable() = ssa.getSourceVariable() and
predicate overwritten(VariableUpdate upd) {
deadLocal(upd) and
exists(VariableUpdate overwrite |
overwrite.getDestVar() = upd.getDestVar() and
not deadLocal(overwrite) and
not overwrite.getDefiningExpr() instanceof LocalVariableDeclExpr and
not overwrite instanceof LocalVariableDeclExpr and
exists(BasicBlock bb1, BasicBlock bb2, int i, int j |
bb1.getNode(i) = ssa.getCfgNode() and
bb2.getNode(j) = overwrite.getCfgNode()
bb1.getNode(i) = upd.getControlFlowNode() and
bb2.getNode(j) = overwrite.getControlFlowNode()
|
bb1.getABBSuccessor+() = bb2
or
Expand All @@ -63,9 +53,9 @@ predicate read(LocalScopeVariable v) {
readImplicitly(_, v)
}

private predicate readImplicitly(SsaExplicitUpdate ssa, LocalScopeVariable v) {
v = ssa.getSourceVariable().getVariable() and
exists(TryStmt try | try.getAResourceVariable() = ssa.getDefiningExpr().getDestVar())
predicate readImplicitly(VariableUpdate upd, LocalScopeVariable v) {
v = upd.getDestVar() and
exists(TryStmt try | try.getAResourceVariable() = upd.getDestVar())
}

/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -40,13 +40,12 @@ predicate excludedInit(Type t, Expr decl) {
)
}

from VariableUpdate def, LocalScopeVariable v, SsaExplicitUpdate ssa
from VariableUpdate def, LocalScopeVariable v
where
def = ssa.getDefiningExpr() and
v = ssa.getSourceVariable().getVariable() and
deadLocal(ssa) and
not expectedDead(ssa) and
overwritten(ssa) and
def.getDestVar() = v and
deadLocal(def) and
not expectedDead(def) and
overwritten(def) and
not exists(LocalVariableDeclExpr decl | def = decl |
excludedInit(decl.getVariable().getType(), decl.getInit())
)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,12 @@
import java
import DeadLocals

from VariableUpdate def, LocalScopeVariable v, SsaExplicitUpdate ssa
from VariableUpdate def, LocalScopeVariable v
where
def = ssa.getDefiningExpr() and
v = ssa.getSourceVariable().getVariable() and
deadLocal(ssa) and
not expectedDead(ssa) and
not overwritten(ssa) and
def.getDestVar() = v and
deadLocal(def) and
not expectedDead(def) and
not overwritten(def) and
read(v) and
not def.(AssignExpr).getSource() instanceof NullLiteral and
(def instanceof Assignment or def.(UnaryAssignExpr).getParent() instanceof ExprStmt)
Expand Down
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
failures
testFailures
failures
Loading

0 comments on commit 291e278

Please sign in to comment.