Skip to content

Introduce semantic layer to prepare to share range analysis #7986

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

Closed
wants to merge 9 commits into from
Closed
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
59 changes: 59 additions & 0 deletions java/ql/lib/semmle/code/java/dataflow/ArrayLengthFlow.qll
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
private import java
private import SSA
private import RangeUtils

/**
* Holds if `v` is an input to `phi` that is not along a back edge, and the
* only other input to `phi` is a `null` value.
*
* Note that the declared type of `phi` is `SsaVariable` instead of
* `SsaPhiNode` in order for the reflexive case of `nonNullSsaFwdStep*(..)` to
* have non-`SsaPhiNode` results.
*/
private predicate nonNullSsaFwdStep(SsaVariable v, SsaVariable phi) {
exists(SsaExplicitUpdate vnull, SsaPhiNode phi0 | phi0 = phi |
2 = strictcount(phi0.getAPhiInput()) and
vnull = phi0.getAPhiInput() and
v = phi0.getAPhiInput() and
not backEdge(phi0, v, _) and
vnull != v and
vnull.getDefiningExpr().(VariableAssign).getSource() instanceof NullLiteral
)
}

private predicate nonNullDefStep(Expr e1, Expr e2) {
exists(ConditionalExpr cond, boolean branch | cond = e2 |
cond.getBranchExpr(branch) = e1 and
cond.getBranchExpr(branch.booleanNot()) instanceof NullLiteral
)
}

/**
* Gets the definition of `v` provided that `v` is a non-null array with an
* explicit `ArrayCreationExpr` definition and that the definition does not go
* through a back edge.
*/
ArrayCreationExpr getArrayDef(SsaVariable v) {
exists(Expr src |
v.(SsaExplicitUpdate).getDefiningExpr().(VariableAssign).getSource() = src and
nonNullDefStep*(result, src)
)
or
exists(SsaVariable mid |
result = getArrayDef(mid) and
nonNullSsaFwdStep(mid, v)
)
}

/**
* Holds if `arrlen` is a read of an array `length` field on an array that, if
* it is non-null, is defined by `def` and that the definition can reach
* `arrlen` without going through a back edge.
*/
predicate arrayLengthDef(FieldRead arrlen, ArrayCreationExpr def) {
exists(SsaVariable arr |
arrlen.getField() instanceof ArrayLengthField and
arrlen.getQualifier() = arr.getAUse() and
def = getArrayDef(arr)
)
}
32 changes: 32 additions & 0 deletions java/ql/lib/semmle/code/java/dataflow/ConstantAnalysis.qll
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
/**
* Simple constant analysis using the Semantic interface.
*/

private import semmle.code.java.semantic.SemanticExpr
private import semmle.code.java.semantic.SemanticSSA
private import ConstantAnalysisSpecific as Specific

/** An expression that always has the same integer value. */
pragma[nomagic]
private predicate constantIntegerExpr(SemExpr e, int val) {
// An integer literal
e.(SemIntegerLiteralExpr).getIntValue() = val
or
// Copy of another constant
exists(SemSsaExplicitUpdate v, SemExpr src |
e = v.getAUse() and
src = v.getDefiningExpr().(SemVariableAssign).getSource() and
constantIntegerExpr(src, val)
)
or
// Language-specific enhancements
val = Specific::getIntConstantValue(e)
}

/** An expression that always has the same integer value. */
class SemConstantIntegerExpr extends SemExpr {
SemConstantIntegerExpr() { constantIntegerExpr(this, _) }

/** Gets the integer value of this expression. */
int getIntValue() { constantIntegerExpr(this, result) }
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
private import java
private import semmle.code.java.semantic.SemanticExpr
private import ArrayLengthFlow

/**
* Gets the constant integer value of the specified expression, if any.
*/
int getIntConstantValue(SemExpr expr) {
exists(ArrayCreationExpr a |
arrayLengthDef(getJavaExpr(expr), a) and
a.getFirstDimensionSize() = result
)
or
exists(Field a, FieldRead arrlen |
a.isFinal() and
a.getInitializer().(ArrayCreationExpr).getFirstDimensionSize() = result and
arrlen.getField() instanceof ArrayLengthField and
arrlen.getQualifier() = a.getAnAccess() and
getJavaExpr(expr) = arrlen
)
or
exists(CompileTimeConstantExpr const | const = getJavaExpr(expr) | result = const.getIntValue())
}
Loading