mirror of
https://github.com/github/codeql.git
synced 2026-04-29 18:55:14 +02:00
Merge branch 'main' into java/unsafe-get-resource
This commit is contained in:
@@ -1,6 +1,6 @@
|
||||
package,sink,source,summary,sink:bean-validation,sink:create-file,sink:groovy,sink:header-splitting,sink:information-leak,sink:intent-start,sink:jdbc-url,sink:jexl,sink:jndi-injection,sink:ldap,sink:logging,sink:mvel,sink:ognl-injection,sink:open-url,sink:pending-intent-sent,sink:set-hostname-verifier,sink:sql,sink:url-open-stream,sink:url-redirect,sink:write-file,sink:xpath,sink:xslt,sink:xss,source:android-widget,source:contentprovider,source:remote,summary:taint,summary:value
|
||||
android.app,16,,103,,,,,,7,,,,,,,,,9,,,,,,,,,,,,18,85
|
||||
android.content,24,27,100,,,,,,16,,,,,,,,,,,8,,,,,,,,27,,31,69
|
||||
android.content,24,27,108,,,,,,16,,,,,,,,,,,8,,,,,,,,27,,31,77
|
||||
android.database,59,,30,,,,,,,,,,,,,,,,,59,,,,,,,,,,30,
|
||||
android.net,,,60,,,,,,,,,,,,,,,,,,,,,,,,,,,45,15
|
||||
android.os,,,122,,,,,,,,,,,,,,,,,,,,,,,,,,,41,81
|
||||
|
||||
|
@@ -7,7 +7,7 @@ Java framework & library support
|
||||
:widths: auto
|
||||
|
||||
Framework / library,Package,Flow sources,Taint & value steps,Sinks (total),`CWE‑022` :sub:`Path injection`,`CWE‑036` :sub:`Path traversal`,`CWE‑079` :sub:`Cross-site scripting`,`CWE‑089` :sub:`SQL injection`,`CWE‑090` :sub:`LDAP injection`,`CWE‑094` :sub:`Code injection`,`CWE‑319` :sub:`Cleartext transmission`
|
||||
Android,``android.*``,46,416,108,,,3,67,,,
|
||||
Android,``android.*``,46,424,108,,,3,67,,,
|
||||
`Apache Commons Collections <https://commons.apache.org/proper/commons-collections/>`_,"``org.apache.commons.collections``, ``org.apache.commons.collections4``",,1600,,,,,,,,
|
||||
`Apache Commons IO <https://commons.apache.org/proper/commons-io/>`_,``org.apache.commons.io``,2,565,93,78,,,,,,15
|
||||
`Apache Commons Lang <https://commons.apache.org/proper/commons-lang/>`_,``org.apache.commons.lang3``,,424,,,,,,,,
|
||||
@@ -19,5 +19,5 @@ Java framework & library support
|
||||
Java extensions,"``javax.*``, ``jakarta.*``",54,552,32,,,4,,1,1,2
|
||||
`Spring <https://spring.io/>`_,``org.springframework.*``,29,472,101,,,,19,14,,29
|
||||
Others,"``androidx.slice``, ``cn.hutool.core.codec``, ``com.esotericsoftware.kryo.io``, ``com.esotericsoftware.kryo5.io``, ``com.fasterxml.jackson.core``, ``com.fasterxml.jackson.databind``, ``com.opensymphony.xwork2.ognl``, ``com.unboundid.ldap.sdk``, ``com.zaxxer.hikari``, ``flexjson``, ``groovy.lang``, ``groovy.util``, ``jodd.json``, ``net.sf.saxon.s9api``, ``ognl``, ``org.apache.commons.codec``, ``org.apache.commons.jexl2``, ``org.apache.commons.jexl3``, ``org.apache.commons.logging``, ``org.apache.commons.ognl``, ``org.apache.directory.ldap.client.api``, ``org.apache.ibatis.jdbc``, ``org.apache.log4j``, ``org.apache.logging.log4j``, ``org.apache.shiro.codec``, ``org.apache.shiro.jndi``, ``org.codehaus.groovy.control``, ``org.dom4j``, ``org.hibernate``, ``org.jboss.logging``, ``org.jdbi.v3.core``, ``org.jooq``, ``org.mvel2``, ``org.scijava.log``, ``org.slf4j``, ``org.xml.sax``, ``org.xmlpull.v1``, ``play.mvc``, ``ratpack.core.form``, ``ratpack.core.handling``, ``ratpack.core.http``, ``ratpack.exec``, ``ratpack.form``, ``ratpack.func``, ``ratpack.handling``, ``ratpack.http``, ``ratpack.util``",44,283,929,,,,14,18,,
|
||||
Totals,,183,6225,1441,106,6,10,107,33,1,81
|
||||
Totals,,183,6233,1441,106,6,10,107,33,1,81
|
||||
|
||||
|
||||
@@ -1,3 +1,18 @@
|
||||
## 0.1.0
|
||||
|
||||
### Breaking Changes
|
||||
|
||||
* The recently added flow-state versions of `isBarrierIn`, `isBarrierOut`, `isSanitizerIn`, and `isSanitizerOut` in the data flow and taint tracking libraries have been removed.
|
||||
* The `getUrl` predicate of `DeclaredRepository` in `MavenPom.qll` has been renamed to `getRepositoryUrl`.
|
||||
|
||||
### New Features
|
||||
|
||||
* There are now QL classes ErrorExpr and ErrorStmt. These may be generated by upgrade or downgrade scripts when databases cannot be fully converted.
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* Added guard preconditon support for assertion methods for popular testing libraries (e.g. Junit 4, Junit 5, TestNG).
|
||||
|
||||
## 0.0.13
|
||||
|
||||
## 0.0.12
|
||||
|
||||
@@ -1,4 +0,0 @@
|
||||
---
|
||||
category: feature
|
||||
---
|
||||
* There are now QL classes ErrorExpr and ErrorStmt. These may be generated by upgrade or downgrade scripts when databases cannot be fully converted.
|
||||
@@ -1,4 +0,0 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* Added guard preconditon support for assertion methods for popular testing libraries (e.g. Junit 4, Junit 5, TestNG).
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: fix
|
||||
---
|
||||
* The QL class `JumpStmt` has been made the superclass of `BreakStmt`, `ContinueStmt` and `YieldStmt`. This allows directly using its inherited predicates without having to explicitly cast to `JumpStmt` first.
|
||||
@@ -1,4 +0,0 @@
|
||||
---
|
||||
category: breaking
|
||||
---
|
||||
* The `getUrl` predicate of `DeclaredRepository` in `MavenPom.qll` has been renamed to `getRepositoryUrl`.
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
Improved the data flow support for the Android class `SharedPreferences$Editor`. Specifically, the fluent logic of some of its methods is now taken into account when calculating data flow.
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: breaking
|
||||
---
|
||||
The signature of `allowImplicitRead` on `DataFlow::Configuration` and `TaintTracking::Configuration` has changed from `allowImplicitRead(DataFlow::Node node, DataFlow::Content c)` to `allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c)`.
|
||||
14
java/ql/lib/change-notes/released/0.1.0.md
Normal file
14
java/ql/lib/change-notes/released/0.1.0.md
Normal file
@@ -0,0 +1,14 @@
|
||||
## 0.1.0
|
||||
|
||||
### Breaking Changes
|
||||
|
||||
* The recently added flow-state versions of `isBarrierIn`, `isBarrierOut`, `isSanitizerIn`, and `isSanitizerOut` in the data flow and taint tracking libraries have been removed.
|
||||
* The `getUrl` predicate of `DeclaredRepository` in `MavenPom.qll` has been renamed to `getRepositoryUrl`.
|
||||
|
||||
### New Features
|
||||
|
||||
* There are now QL classes ErrorExpr and ErrorStmt. These may be generated by upgrade or downgrade scripts when databases cannot be fully converted.
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* Added guard preconditon support for assertion methods for popular testing libraries (e.g. Junit 4, Junit 5, TestNG).
|
||||
@@ -1,2 +1,2 @@
|
||||
---
|
||||
lastReleaseVersion: 0.0.13
|
||||
lastReleaseVersion: 0.1.0
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
name: codeql/java-all
|
||||
version: 0.1.0-dev
|
||||
version: 0.1.1-dev
|
||||
groups: java
|
||||
dbscheme: config/semmlecode.dbscheme
|
||||
extractor: java
|
||||
|
||||
@@ -1399,7 +1399,7 @@ class SwitchExpr extends Expr, StmtParent, @switchexpr {
|
||||
Expr getAResult() {
|
||||
result = this.getACase().getRuleExpression()
|
||||
or
|
||||
exists(YieldStmt yield | yield.(JumpStmt).getTarget() = this and result = yield.getValue())
|
||||
exists(YieldStmt yield | yield.getTarget() = this and result = yield.getValue())
|
||||
}
|
||||
|
||||
/** Gets a printable representation of this expression. */
|
||||
|
||||
@@ -3,7 +3,6 @@
|
||||
*/
|
||||
|
||||
import semmle.code.Location
|
||||
import Element
|
||||
|
||||
/** A Javadoc parent is an element whose child can be some Javadoc documentation. */
|
||||
class JavadocParent extends @javadocParent, Top {
|
||||
|
||||
@@ -570,14 +570,10 @@ class ThrowStmt extends Stmt, @throwstmt {
|
||||
override string getAPrimaryQlClass() { result = "ThrowStmt" }
|
||||
}
|
||||
|
||||
/** A `break`, `yield` or `continue` statement. */
|
||||
class JumpStmt extends Stmt {
|
||||
JumpStmt() {
|
||||
this instanceof BreakStmt or
|
||||
this instanceof YieldStmt or
|
||||
this instanceof ContinueStmt
|
||||
}
|
||||
private class JumpStmt_ = @breakstmt or @yieldstmt or @continuestmt;
|
||||
|
||||
/** A `break`, `yield` or `continue` statement. */
|
||||
class JumpStmt extends Stmt, JumpStmt_ {
|
||||
/**
|
||||
* Gets the labeled statement that this `break` or
|
||||
* `continue` statement refers to, if any.
|
||||
@@ -598,12 +594,7 @@ class JumpStmt extends Stmt {
|
||||
)
|
||||
}
|
||||
|
||||
private SwitchExpr getSwitchExprTarget() { result = this.(YieldStmt).getParent+() }
|
||||
|
||||
private StmtParent getEnclosingTarget() {
|
||||
result = this.getSwitchExprTarget()
|
||||
or
|
||||
not exists(this.getSwitchExprTarget()) and
|
||||
result = this.getAPotentialTarget() and
|
||||
not exists(Stmt other | other = this.getAPotentialTarget() | other.getEnclosingStmt+() = result)
|
||||
}
|
||||
@@ -612,6 +603,7 @@ class JumpStmt extends Stmt {
|
||||
* Gets the statement or `switch` expression that this `break`, `yield` or `continue` jumps to.
|
||||
*/
|
||||
StmtParent getTarget() {
|
||||
// Note: This implementation only considers `break` and `continue`; YieldStmt overrides this predicate
|
||||
result = this.getLabelTarget()
|
||||
or
|
||||
not exists(this.getLabelTarget()) and result = this.getEnclosingTarget()
|
||||
@@ -619,7 +611,7 @@ class JumpStmt extends Stmt {
|
||||
}
|
||||
|
||||
/** A `break` statement. */
|
||||
class BreakStmt extends Stmt, @breakstmt {
|
||||
class BreakStmt extends JumpStmt, @breakstmt {
|
||||
/** Gets the label targeted by this `break` statement, if any. */
|
||||
string getLabel() { namestrings(result, _, this) }
|
||||
|
||||
@@ -640,12 +632,21 @@ class BreakStmt extends Stmt, @breakstmt {
|
||||
/**
|
||||
* A `yield` statement.
|
||||
*/
|
||||
class YieldStmt extends Stmt, @yieldstmt {
|
||||
class YieldStmt extends JumpStmt, @yieldstmt {
|
||||
/**
|
||||
* Gets the value of this `yield` statement.
|
||||
*/
|
||||
Expr getValue() { result.getParent() = this }
|
||||
|
||||
/**
|
||||
* Gets the `switch` expression target of this `yield` statement.
|
||||
*/
|
||||
override SwitchExpr getTarget() {
|
||||
// Get the innermost enclosing SwitchExpr; this works because getParent() is defined for Stmt and
|
||||
// therefore won't proceed after the innermost SwitchExpr (due to it being an Expr)
|
||||
result = this.getParent+()
|
||||
}
|
||||
|
||||
override string pp() { result = "yield ..." }
|
||||
|
||||
override string toString() { result = "yield ..." }
|
||||
@@ -656,7 +657,7 @@ class YieldStmt extends Stmt, @yieldstmt {
|
||||
}
|
||||
|
||||
/** A `continue` statement. */
|
||||
class ContinueStmt extends Stmt, @continuestmt {
|
||||
class ContinueStmt extends JumpStmt, @continuestmt {
|
||||
/** Gets the label targeted by this `continue` statement, if any. */
|
||||
string getLabel() { namestrings(result, _, this) }
|
||||
|
||||
|
||||
@@ -4,7 +4,6 @@
|
||||
|
||||
import java
|
||||
import Dominance
|
||||
import semmle.code.java.ControlFlowGraph
|
||||
|
||||
/**
|
||||
* A control-flow node that represents the start of a basic block.
|
||||
|
||||
@@ -3,7 +3,6 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
private import semmle.code.java.ControlFlowGraph
|
||||
|
||||
/*
|
||||
* Predicates for basic-block-level dominance.
|
||||
|
||||
@@ -82,6 +82,7 @@ private module Frameworks {
|
||||
private import semmle.code.java.frameworks.android.ContentProviders
|
||||
private import semmle.code.java.frameworks.android.Intent
|
||||
private import semmle.code.java.frameworks.android.Notifications
|
||||
private import semmle.code.java.frameworks.android.SharedPreferences
|
||||
private import semmle.code.java.frameworks.android.Slice
|
||||
private import semmle.code.java.frameworks.android.SQLite
|
||||
private import semmle.code.java.frameworks.android.Widget
|
||||
@@ -137,7 +138,6 @@ private module Frameworks {
|
||||
private import semmle.code.java.frameworks.MyBatis
|
||||
private import semmle.code.java.frameworks.Hibernate
|
||||
private import semmle.code.java.frameworks.jOOQ
|
||||
private import semmle.code.java.frameworks.spring.SpringHttp
|
||||
}
|
||||
|
||||
private predicate sourceModelCsv(string row) {
|
||||
|
||||
7
java/ql/lib/semmle/code/java/dataflow/TaintTracking3.qll
Normal file
7
java/ql/lib/semmle/code/java/dataflow/TaintTracking3.qll
Normal file
@@ -0,0 +1,7 @@
|
||||
/**
|
||||
* Provides classes for performing local (intra-procedural) and
|
||||
* global (inter-procedural) taint-tracking analyses.
|
||||
*/
|
||||
module TaintTracking3 {
|
||||
import semmle.code.java.dataflow.internal.tainttracking3.TaintTrackingImpl
|
||||
}
|
||||
@@ -42,9 +42,7 @@ module AccessPath {
|
||||
* Parses a lower-bounded interval `n..` and gets the lower bound.
|
||||
*/
|
||||
bindingset[arg]
|
||||
private int parseLowerBound(string arg) {
|
||||
result = arg.regexpCapture("(-?\\d+)\\.\\.", 1).toInt()
|
||||
}
|
||||
int parseLowerBound(string arg) { result = arg.regexpCapture("(-?\\d+)\\.\\.", 1).toInt() }
|
||||
|
||||
/**
|
||||
* Parses an integer constant or interval (bounded or unbounded) that explicitly
|
||||
@@ -151,7 +149,7 @@ class AccessPath extends string instanceof AccessPath::Range {
|
||||
* An access part token such as `Argument[1]` or `ReturnValue`, appearing in one or more access paths.
|
||||
*/
|
||||
class AccessPathToken extends string {
|
||||
AccessPathToken() { this = getRawToken(any(AccessPath path), _) }
|
||||
AccessPathToken() { this = getRawToken(_, _) }
|
||||
|
||||
private string getPart(int part) {
|
||||
result = this.regexpCapture("([^\\[]+)(?:\\[([^\\]]*)\\])?", part)
|
||||
|
||||
@@ -87,21 +87,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -128,7 +116,7 @@ abstract class Configuration extends string {
|
||||
* Holds if an arbitrary number of implicit read steps of content `c` may be
|
||||
* taken at `node`.
|
||||
*/
|
||||
predicate allowImplicitRead(Node node, Content c) { none() }
|
||||
predicate allowImplicitRead(Node node, ContentSet c) { none() }
|
||||
|
||||
/**
|
||||
* Gets the virtual dispatch branching limit when calculating field flow.
|
||||
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -517,16 +479,15 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
)
|
||||
}
|
||||
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
read(node1.asNode(), c, node2.asNode()) and
|
||||
pragma[nomagic]
|
||||
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
|
||||
readSet(node1.asNode(), c, node2.asNode()) and
|
||||
stepFilter(node1, node2, config)
|
||||
or
|
||||
exists(Node n |
|
||||
@@ -536,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
readSet(node1, cs, node2, config) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||
exists(ContentSet cs |
|
||||
clearsContentCached(n.asNode(), cs) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate store(
|
||||
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
|
||||
) {
|
||||
@@ -613,9 +593,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Content c |
|
||||
fwdFlowRead(c, node, cc, config) and
|
||||
fwdFlowConsCand(c, config)
|
||||
exists(ContentSet c |
|
||||
fwdFlowReadSet(c, node, cc, config) and
|
||||
fwdFlowConsCandSet(c, _, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
@@ -639,10 +619,10 @@ private module Stage1 {
|
||||
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
|
||||
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, cc, config) and
|
||||
read(mid, c, node, config)
|
||||
readSet(mid, c, node, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -660,6 +640,16 @@ private module Stage1 {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `cs` may be interpreted in a read as the target of some store
|
||||
* into `c`, in the flow covered by `fwdFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
|
||||
fwdFlowConsCand(c, config) and
|
||||
c = cs.getAReadContent()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
|
||||
exists(RetNodeEx ret |
|
||||
@@ -752,9 +742,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Content c |
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
exists(NodeEx mid, ContentSet c |
|
||||
readSet(node, c, mid, config) and
|
||||
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, toReturn, pragma[only_bind_into](config))
|
||||
)
|
||||
or
|
||||
@@ -780,10 +770,10 @@ private module Stage1 {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowConsCand(Content c, Configuration config) {
|
||||
exists(NodeEx mid, NodeEx node |
|
||||
exists(NodeEx mid, NodeEx node, ContentSet cs |
|
||||
fwdFlow(node, pragma[only_bind_into](config)) and
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
readSet(node, cs, mid, config) and
|
||||
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
|
||||
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
@@ -802,6 +792,7 @@ private module Stage1 {
|
||||
* Holds if `c` is the target of both a read and a store in the flow covered
|
||||
* by `revFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
|
||||
revFlowConsCand(c, conf) and
|
||||
revFlowStore(c, _, _, conf)
|
||||
@@ -900,9 +891,9 @@ private module Stage1 {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
|
||||
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config))
|
||||
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -912,14 +903,17 @@ private module Stage1 {
|
||||
predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
|
||||
revFlow(node, toReturn, pragma[only_bind_into](config)) and
|
||||
exists(state) and
|
||||
exists(returnAp) and
|
||||
exists(ap)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -1014,8 +1008,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -1036,8 +1030,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1189,7 +1183,7 @@ private module Stage2 {
|
||||
|
||||
bindingset[node, state, ap, config]
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
PrevStage::revFlowState(state, config) and
|
||||
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
|
||||
exists(ap) and
|
||||
not stateBarrier(node, state, config)
|
||||
}
|
||||
@@ -1614,7 +1608,7 @@ private module Stage2 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -1769,9 +1763,9 @@ private module LocalFlowBigStep {
|
||||
or
|
||||
node.asNode() instanceof OutNodeExt
|
||||
or
|
||||
store(_, _, node, _, config)
|
||||
Stage2::storeStepCand(_, _, _, node, _, config)
|
||||
or
|
||||
read(_, _, node, config)
|
||||
Stage2::readStepCand(_, _, node, config)
|
||||
or
|
||||
node instanceof FlowCheckNode
|
||||
or
|
||||
@@ -1792,8 +1786,8 @@ private module LocalFlowBigStep {
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
store(node, _, next, _, config) or
|
||||
read(node, _, next, config)
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
|
||||
@@ -1966,7 +1960,24 @@ private module Stage3 {
|
||||
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
|
||||
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
|
||||
PrevStage::revFlow(node, config) and
|
||||
clearsContentCached(node.asNode(), c)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clearContent(NodeEx node, Content c, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
|
||||
c = cs.getAReadContent() and
|
||||
clearSet(node, cs, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap, Configuration config) {
|
||||
clearContent(node, ap.getHead().getContent(), config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
|
||||
@@ -1975,7 +1986,7 @@ private module Stage3 {
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
exists(state) and
|
||||
exists(config) and
|
||||
not clear(node, ap) and
|
||||
not clear(node, ap, config) and
|
||||
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
|
||||
}
|
||||
|
||||
@@ -2403,7 +2414,7 @@ private module Stage3 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -3230,7 +3241,7 @@ private module Stage4 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -4242,7 +4253,7 @@ private module Subpaths {
|
||||
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
|
||||
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
|
||||
store(n1, _, n2, _, _) or
|
||||
read(n1, _, n2, _)
|
||||
readSet(n1, _, n2, _)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -4597,7 +4608,7 @@ private module FlowExploration {
|
||||
or
|
||||
exists(PartialPathNodeRev mid |
|
||||
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead()) and
|
||||
not clearsContentEx(node, ap.getHead()) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
|
||||
@@ -4613,7 +4624,7 @@ private module FlowExploration {
|
||||
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
|
||||
not clearsContentEx(node, ap.getHead().getContent()) and
|
||||
if node.asNode() instanceof CastingNode
|
||||
then compatibleTypes(node.getDataFlowType(), ap.getType())
|
||||
else any()
|
||||
@@ -5047,6 +5058,7 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,21 +87,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -128,7 +116,7 @@ abstract class Configuration extends string {
|
||||
* Holds if an arbitrary number of implicit read steps of content `c` may be
|
||||
* taken at `node`.
|
||||
*/
|
||||
predicate allowImplicitRead(Node node, Content c) { none() }
|
||||
predicate allowImplicitRead(Node node, ContentSet c) { none() }
|
||||
|
||||
/**
|
||||
* Gets the virtual dispatch branching limit when calculating field flow.
|
||||
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -517,16 +479,15 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
)
|
||||
}
|
||||
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
read(node1.asNode(), c, node2.asNode()) and
|
||||
pragma[nomagic]
|
||||
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
|
||||
readSet(node1.asNode(), c, node2.asNode()) and
|
||||
stepFilter(node1, node2, config)
|
||||
or
|
||||
exists(Node n |
|
||||
@@ -536,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
readSet(node1, cs, node2, config) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||
exists(ContentSet cs |
|
||||
clearsContentCached(n.asNode(), cs) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate store(
|
||||
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
|
||||
) {
|
||||
@@ -613,9 +593,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Content c |
|
||||
fwdFlowRead(c, node, cc, config) and
|
||||
fwdFlowConsCand(c, config)
|
||||
exists(ContentSet c |
|
||||
fwdFlowReadSet(c, node, cc, config) and
|
||||
fwdFlowConsCandSet(c, _, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
@@ -639,10 +619,10 @@ private module Stage1 {
|
||||
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
|
||||
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, cc, config) and
|
||||
read(mid, c, node, config)
|
||||
readSet(mid, c, node, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -660,6 +640,16 @@ private module Stage1 {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `cs` may be interpreted in a read as the target of some store
|
||||
* into `c`, in the flow covered by `fwdFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
|
||||
fwdFlowConsCand(c, config) and
|
||||
c = cs.getAReadContent()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
|
||||
exists(RetNodeEx ret |
|
||||
@@ -752,9 +742,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Content c |
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
exists(NodeEx mid, ContentSet c |
|
||||
readSet(node, c, mid, config) and
|
||||
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, toReturn, pragma[only_bind_into](config))
|
||||
)
|
||||
or
|
||||
@@ -780,10 +770,10 @@ private module Stage1 {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowConsCand(Content c, Configuration config) {
|
||||
exists(NodeEx mid, NodeEx node |
|
||||
exists(NodeEx mid, NodeEx node, ContentSet cs |
|
||||
fwdFlow(node, pragma[only_bind_into](config)) and
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
readSet(node, cs, mid, config) and
|
||||
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
|
||||
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
@@ -802,6 +792,7 @@ private module Stage1 {
|
||||
* Holds if `c` is the target of both a read and a store in the flow covered
|
||||
* by `revFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
|
||||
revFlowConsCand(c, conf) and
|
||||
revFlowStore(c, _, _, conf)
|
||||
@@ -900,9 +891,9 @@ private module Stage1 {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
|
||||
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config))
|
||||
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -912,14 +903,17 @@ private module Stage1 {
|
||||
predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
|
||||
revFlow(node, toReturn, pragma[only_bind_into](config)) and
|
||||
exists(state) and
|
||||
exists(returnAp) and
|
||||
exists(ap)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -1014,8 +1008,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -1036,8 +1030,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1189,7 +1183,7 @@ private module Stage2 {
|
||||
|
||||
bindingset[node, state, ap, config]
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
PrevStage::revFlowState(state, config) and
|
||||
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
|
||||
exists(ap) and
|
||||
not stateBarrier(node, state, config)
|
||||
}
|
||||
@@ -1614,7 +1608,7 @@ private module Stage2 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -1769,9 +1763,9 @@ private module LocalFlowBigStep {
|
||||
or
|
||||
node.asNode() instanceof OutNodeExt
|
||||
or
|
||||
store(_, _, node, _, config)
|
||||
Stage2::storeStepCand(_, _, _, node, _, config)
|
||||
or
|
||||
read(_, _, node, config)
|
||||
Stage2::readStepCand(_, _, node, config)
|
||||
or
|
||||
node instanceof FlowCheckNode
|
||||
or
|
||||
@@ -1792,8 +1786,8 @@ private module LocalFlowBigStep {
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
store(node, _, next, _, config) or
|
||||
read(node, _, next, config)
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
|
||||
@@ -1966,7 +1960,24 @@ private module Stage3 {
|
||||
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
|
||||
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
|
||||
PrevStage::revFlow(node, config) and
|
||||
clearsContentCached(node.asNode(), c)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clearContent(NodeEx node, Content c, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
|
||||
c = cs.getAReadContent() and
|
||||
clearSet(node, cs, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap, Configuration config) {
|
||||
clearContent(node, ap.getHead().getContent(), config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
|
||||
@@ -1975,7 +1986,7 @@ private module Stage3 {
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
exists(state) and
|
||||
exists(config) and
|
||||
not clear(node, ap) and
|
||||
not clear(node, ap, config) and
|
||||
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
|
||||
}
|
||||
|
||||
@@ -2403,7 +2414,7 @@ private module Stage3 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -3230,7 +3241,7 @@ private module Stage4 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -4242,7 +4253,7 @@ private module Subpaths {
|
||||
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
|
||||
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
|
||||
store(n1, _, n2, _, _) or
|
||||
read(n1, _, n2, _)
|
||||
readSet(n1, _, n2, _)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -4597,7 +4608,7 @@ private module FlowExploration {
|
||||
or
|
||||
exists(PartialPathNodeRev mid |
|
||||
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead()) and
|
||||
not clearsContentEx(node, ap.getHead()) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
|
||||
@@ -4613,7 +4624,7 @@ private module FlowExploration {
|
||||
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
|
||||
not clearsContentEx(node, ap.getHead().getContent()) and
|
||||
if node.asNode() instanceof CastingNode
|
||||
then compatibleTypes(node.getDataFlowType(), ap.getType())
|
||||
else any()
|
||||
@@ -5047,6 +5058,7 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,21 +87,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -128,7 +116,7 @@ abstract class Configuration extends string {
|
||||
* Holds if an arbitrary number of implicit read steps of content `c` may be
|
||||
* taken at `node`.
|
||||
*/
|
||||
predicate allowImplicitRead(Node node, Content c) { none() }
|
||||
predicate allowImplicitRead(Node node, ContentSet c) { none() }
|
||||
|
||||
/**
|
||||
* Gets the virtual dispatch branching limit when calculating field flow.
|
||||
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -517,16 +479,15 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
)
|
||||
}
|
||||
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
read(node1.asNode(), c, node2.asNode()) and
|
||||
pragma[nomagic]
|
||||
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
|
||||
readSet(node1.asNode(), c, node2.asNode()) and
|
||||
stepFilter(node1, node2, config)
|
||||
or
|
||||
exists(Node n |
|
||||
@@ -536,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
readSet(node1, cs, node2, config) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||
exists(ContentSet cs |
|
||||
clearsContentCached(n.asNode(), cs) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate store(
|
||||
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
|
||||
) {
|
||||
@@ -613,9 +593,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Content c |
|
||||
fwdFlowRead(c, node, cc, config) and
|
||||
fwdFlowConsCand(c, config)
|
||||
exists(ContentSet c |
|
||||
fwdFlowReadSet(c, node, cc, config) and
|
||||
fwdFlowConsCandSet(c, _, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
@@ -639,10 +619,10 @@ private module Stage1 {
|
||||
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
|
||||
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, cc, config) and
|
||||
read(mid, c, node, config)
|
||||
readSet(mid, c, node, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -660,6 +640,16 @@ private module Stage1 {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `cs` may be interpreted in a read as the target of some store
|
||||
* into `c`, in the flow covered by `fwdFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
|
||||
fwdFlowConsCand(c, config) and
|
||||
c = cs.getAReadContent()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
|
||||
exists(RetNodeEx ret |
|
||||
@@ -752,9 +742,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Content c |
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
exists(NodeEx mid, ContentSet c |
|
||||
readSet(node, c, mid, config) and
|
||||
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, toReturn, pragma[only_bind_into](config))
|
||||
)
|
||||
or
|
||||
@@ -780,10 +770,10 @@ private module Stage1 {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowConsCand(Content c, Configuration config) {
|
||||
exists(NodeEx mid, NodeEx node |
|
||||
exists(NodeEx mid, NodeEx node, ContentSet cs |
|
||||
fwdFlow(node, pragma[only_bind_into](config)) and
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
readSet(node, cs, mid, config) and
|
||||
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
|
||||
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
@@ -802,6 +792,7 @@ private module Stage1 {
|
||||
* Holds if `c` is the target of both a read and a store in the flow covered
|
||||
* by `revFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
|
||||
revFlowConsCand(c, conf) and
|
||||
revFlowStore(c, _, _, conf)
|
||||
@@ -900,9 +891,9 @@ private module Stage1 {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
|
||||
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config))
|
||||
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -912,14 +903,17 @@ private module Stage1 {
|
||||
predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
|
||||
revFlow(node, toReturn, pragma[only_bind_into](config)) and
|
||||
exists(state) and
|
||||
exists(returnAp) and
|
||||
exists(ap)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -1014,8 +1008,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -1036,8 +1030,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1189,7 +1183,7 @@ private module Stage2 {
|
||||
|
||||
bindingset[node, state, ap, config]
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
PrevStage::revFlowState(state, config) and
|
||||
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
|
||||
exists(ap) and
|
||||
not stateBarrier(node, state, config)
|
||||
}
|
||||
@@ -1614,7 +1608,7 @@ private module Stage2 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -1769,9 +1763,9 @@ private module LocalFlowBigStep {
|
||||
or
|
||||
node.asNode() instanceof OutNodeExt
|
||||
or
|
||||
store(_, _, node, _, config)
|
||||
Stage2::storeStepCand(_, _, _, node, _, config)
|
||||
or
|
||||
read(_, _, node, config)
|
||||
Stage2::readStepCand(_, _, node, config)
|
||||
or
|
||||
node instanceof FlowCheckNode
|
||||
or
|
||||
@@ -1792,8 +1786,8 @@ private module LocalFlowBigStep {
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
store(node, _, next, _, config) or
|
||||
read(node, _, next, config)
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
|
||||
@@ -1966,7 +1960,24 @@ private module Stage3 {
|
||||
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
|
||||
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
|
||||
PrevStage::revFlow(node, config) and
|
||||
clearsContentCached(node.asNode(), c)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clearContent(NodeEx node, Content c, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
|
||||
c = cs.getAReadContent() and
|
||||
clearSet(node, cs, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap, Configuration config) {
|
||||
clearContent(node, ap.getHead().getContent(), config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
|
||||
@@ -1975,7 +1986,7 @@ private module Stage3 {
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
exists(state) and
|
||||
exists(config) and
|
||||
not clear(node, ap) and
|
||||
not clear(node, ap, config) and
|
||||
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
|
||||
}
|
||||
|
||||
@@ -2403,7 +2414,7 @@ private module Stage3 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -3230,7 +3241,7 @@ private module Stage4 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -4242,7 +4253,7 @@ private module Subpaths {
|
||||
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
|
||||
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
|
||||
store(n1, _, n2, _, _) or
|
||||
read(n1, _, n2, _)
|
||||
readSet(n1, _, n2, _)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -4597,7 +4608,7 @@ private module FlowExploration {
|
||||
or
|
||||
exists(PartialPathNodeRev mid |
|
||||
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead()) and
|
||||
not clearsContentEx(node, ap.getHead()) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
|
||||
@@ -4613,7 +4624,7 @@ private module FlowExploration {
|
||||
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
|
||||
not clearsContentEx(node, ap.getHead().getContent()) and
|
||||
if node.asNode() instanceof CastingNode
|
||||
then compatibleTypes(node.getDataFlowType(), ap.getType())
|
||||
else any()
|
||||
@@ -5047,6 +5058,7 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,21 +87,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -128,7 +116,7 @@ abstract class Configuration extends string {
|
||||
* Holds if an arbitrary number of implicit read steps of content `c` may be
|
||||
* taken at `node`.
|
||||
*/
|
||||
predicate allowImplicitRead(Node node, Content c) { none() }
|
||||
predicate allowImplicitRead(Node node, ContentSet c) { none() }
|
||||
|
||||
/**
|
||||
* Gets the virtual dispatch branching limit when calculating field flow.
|
||||
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -517,16 +479,15 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
)
|
||||
}
|
||||
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
read(node1.asNode(), c, node2.asNode()) and
|
||||
pragma[nomagic]
|
||||
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
|
||||
readSet(node1.asNode(), c, node2.asNode()) and
|
||||
stepFilter(node1, node2, config)
|
||||
or
|
||||
exists(Node n |
|
||||
@@ -536,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
readSet(node1, cs, node2, config) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||
exists(ContentSet cs |
|
||||
clearsContentCached(n.asNode(), cs) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate store(
|
||||
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
|
||||
) {
|
||||
@@ -613,9 +593,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Content c |
|
||||
fwdFlowRead(c, node, cc, config) and
|
||||
fwdFlowConsCand(c, config)
|
||||
exists(ContentSet c |
|
||||
fwdFlowReadSet(c, node, cc, config) and
|
||||
fwdFlowConsCandSet(c, _, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
@@ -639,10 +619,10 @@ private module Stage1 {
|
||||
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
|
||||
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, cc, config) and
|
||||
read(mid, c, node, config)
|
||||
readSet(mid, c, node, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -660,6 +640,16 @@ private module Stage1 {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `cs` may be interpreted in a read as the target of some store
|
||||
* into `c`, in the flow covered by `fwdFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
|
||||
fwdFlowConsCand(c, config) and
|
||||
c = cs.getAReadContent()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
|
||||
exists(RetNodeEx ret |
|
||||
@@ -752,9 +742,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Content c |
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
exists(NodeEx mid, ContentSet c |
|
||||
readSet(node, c, mid, config) and
|
||||
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, toReturn, pragma[only_bind_into](config))
|
||||
)
|
||||
or
|
||||
@@ -780,10 +770,10 @@ private module Stage1 {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowConsCand(Content c, Configuration config) {
|
||||
exists(NodeEx mid, NodeEx node |
|
||||
exists(NodeEx mid, NodeEx node, ContentSet cs |
|
||||
fwdFlow(node, pragma[only_bind_into](config)) and
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
readSet(node, cs, mid, config) and
|
||||
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
|
||||
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
@@ -802,6 +792,7 @@ private module Stage1 {
|
||||
* Holds if `c` is the target of both a read and a store in the flow covered
|
||||
* by `revFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
|
||||
revFlowConsCand(c, conf) and
|
||||
revFlowStore(c, _, _, conf)
|
||||
@@ -900,9 +891,9 @@ private module Stage1 {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
|
||||
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config))
|
||||
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -912,14 +903,17 @@ private module Stage1 {
|
||||
predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
|
||||
revFlow(node, toReturn, pragma[only_bind_into](config)) and
|
||||
exists(state) and
|
||||
exists(returnAp) and
|
||||
exists(ap)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -1014,8 +1008,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -1036,8 +1030,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1189,7 +1183,7 @@ private module Stage2 {
|
||||
|
||||
bindingset[node, state, ap, config]
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
PrevStage::revFlowState(state, config) and
|
||||
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
|
||||
exists(ap) and
|
||||
not stateBarrier(node, state, config)
|
||||
}
|
||||
@@ -1614,7 +1608,7 @@ private module Stage2 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -1769,9 +1763,9 @@ private module LocalFlowBigStep {
|
||||
or
|
||||
node.asNode() instanceof OutNodeExt
|
||||
or
|
||||
store(_, _, node, _, config)
|
||||
Stage2::storeStepCand(_, _, _, node, _, config)
|
||||
or
|
||||
read(_, _, node, config)
|
||||
Stage2::readStepCand(_, _, node, config)
|
||||
or
|
||||
node instanceof FlowCheckNode
|
||||
or
|
||||
@@ -1792,8 +1786,8 @@ private module LocalFlowBigStep {
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
store(node, _, next, _, config) or
|
||||
read(node, _, next, config)
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
|
||||
@@ -1966,7 +1960,24 @@ private module Stage3 {
|
||||
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
|
||||
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
|
||||
PrevStage::revFlow(node, config) and
|
||||
clearsContentCached(node.asNode(), c)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clearContent(NodeEx node, Content c, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
|
||||
c = cs.getAReadContent() and
|
||||
clearSet(node, cs, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap, Configuration config) {
|
||||
clearContent(node, ap.getHead().getContent(), config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
|
||||
@@ -1975,7 +1986,7 @@ private module Stage3 {
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
exists(state) and
|
||||
exists(config) and
|
||||
not clear(node, ap) and
|
||||
not clear(node, ap, config) and
|
||||
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
|
||||
}
|
||||
|
||||
@@ -2403,7 +2414,7 @@ private module Stage3 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -3230,7 +3241,7 @@ private module Stage4 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -4242,7 +4253,7 @@ private module Subpaths {
|
||||
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
|
||||
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
|
||||
store(n1, _, n2, _, _) or
|
||||
read(n1, _, n2, _)
|
||||
readSet(n1, _, n2, _)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -4597,7 +4608,7 @@ private module FlowExploration {
|
||||
or
|
||||
exists(PartialPathNodeRev mid |
|
||||
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead()) and
|
||||
not clearsContentEx(node, ap.getHead()) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
|
||||
@@ -4613,7 +4624,7 @@ private module FlowExploration {
|
||||
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
|
||||
not clearsContentEx(node, ap.getHead().getContent()) and
|
||||
if node.asNode() instanceof CastingNode
|
||||
then compatibleTypes(node.getDataFlowType(), ap.getType())
|
||||
else any()
|
||||
@@ -5047,6 +5058,7 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,21 +87,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -128,7 +116,7 @@ abstract class Configuration extends string {
|
||||
* Holds if an arbitrary number of implicit read steps of content `c` may be
|
||||
* taken at `node`.
|
||||
*/
|
||||
predicate allowImplicitRead(Node node, Content c) { none() }
|
||||
predicate allowImplicitRead(Node node, ContentSet c) { none() }
|
||||
|
||||
/**
|
||||
* Gets the virtual dispatch branching limit when calculating field flow.
|
||||
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -517,16 +479,15 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
)
|
||||
}
|
||||
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
read(node1.asNode(), c, node2.asNode()) and
|
||||
pragma[nomagic]
|
||||
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
|
||||
readSet(node1.asNode(), c, node2.asNode()) and
|
||||
stepFilter(node1, node2, config)
|
||||
or
|
||||
exists(Node n |
|
||||
@@ -536,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
readSet(node1, cs, node2, config) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||
exists(ContentSet cs |
|
||||
clearsContentCached(n.asNode(), cs) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate store(
|
||||
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
|
||||
) {
|
||||
@@ -613,9 +593,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Content c |
|
||||
fwdFlowRead(c, node, cc, config) and
|
||||
fwdFlowConsCand(c, config)
|
||||
exists(ContentSet c |
|
||||
fwdFlowReadSet(c, node, cc, config) and
|
||||
fwdFlowConsCandSet(c, _, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
@@ -639,10 +619,10 @@ private module Stage1 {
|
||||
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
|
||||
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, cc, config) and
|
||||
read(mid, c, node, config)
|
||||
readSet(mid, c, node, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -660,6 +640,16 @@ private module Stage1 {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `cs` may be interpreted in a read as the target of some store
|
||||
* into `c`, in the flow covered by `fwdFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
|
||||
fwdFlowConsCand(c, config) and
|
||||
c = cs.getAReadContent()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
|
||||
exists(RetNodeEx ret |
|
||||
@@ -752,9 +742,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Content c |
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
exists(NodeEx mid, ContentSet c |
|
||||
readSet(node, c, mid, config) and
|
||||
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, toReturn, pragma[only_bind_into](config))
|
||||
)
|
||||
or
|
||||
@@ -780,10 +770,10 @@ private module Stage1 {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowConsCand(Content c, Configuration config) {
|
||||
exists(NodeEx mid, NodeEx node |
|
||||
exists(NodeEx mid, NodeEx node, ContentSet cs |
|
||||
fwdFlow(node, pragma[only_bind_into](config)) and
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
readSet(node, cs, mid, config) and
|
||||
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
|
||||
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
@@ -802,6 +792,7 @@ private module Stage1 {
|
||||
* Holds if `c` is the target of both a read and a store in the flow covered
|
||||
* by `revFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
|
||||
revFlowConsCand(c, conf) and
|
||||
revFlowStore(c, _, _, conf)
|
||||
@@ -900,9 +891,9 @@ private module Stage1 {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
|
||||
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config))
|
||||
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -912,14 +903,17 @@ private module Stage1 {
|
||||
predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
|
||||
revFlow(node, toReturn, pragma[only_bind_into](config)) and
|
||||
exists(state) and
|
||||
exists(returnAp) and
|
||||
exists(ap)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -1014,8 +1008,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -1036,8 +1030,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1189,7 +1183,7 @@ private module Stage2 {
|
||||
|
||||
bindingset[node, state, ap, config]
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
PrevStage::revFlowState(state, config) and
|
||||
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
|
||||
exists(ap) and
|
||||
not stateBarrier(node, state, config)
|
||||
}
|
||||
@@ -1614,7 +1608,7 @@ private module Stage2 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -1769,9 +1763,9 @@ private module LocalFlowBigStep {
|
||||
or
|
||||
node.asNode() instanceof OutNodeExt
|
||||
or
|
||||
store(_, _, node, _, config)
|
||||
Stage2::storeStepCand(_, _, _, node, _, config)
|
||||
or
|
||||
read(_, _, node, config)
|
||||
Stage2::readStepCand(_, _, node, config)
|
||||
or
|
||||
node instanceof FlowCheckNode
|
||||
or
|
||||
@@ -1792,8 +1786,8 @@ private module LocalFlowBigStep {
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
store(node, _, next, _, config) or
|
||||
read(node, _, next, config)
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
|
||||
@@ -1966,7 +1960,24 @@ private module Stage3 {
|
||||
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
|
||||
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
|
||||
PrevStage::revFlow(node, config) and
|
||||
clearsContentCached(node.asNode(), c)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clearContent(NodeEx node, Content c, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
|
||||
c = cs.getAReadContent() and
|
||||
clearSet(node, cs, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap, Configuration config) {
|
||||
clearContent(node, ap.getHead().getContent(), config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
|
||||
@@ -1975,7 +1986,7 @@ private module Stage3 {
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
exists(state) and
|
||||
exists(config) and
|
||||
not clear(node, ap) and
|
||||
not clear(node, ap, config) and
|
||||
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
|
||||
}
|
||||
|
||||
@@ -2403,7 +2414,7 @@ private module Stage3 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -3230,7 +3241,7 @@ private module Stage4 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -4242,7 +4253,7 @@ private module Subpaths {
|
||||
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
|
||||
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
|
||||
store(n1, _, n2, _, _) or
|
||||
read(n1, _, n2, _)
|
||||
readSet(n1, _, n2, _)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -4597,7 +4608,7 @@ private module FlowExploration {
|
||||
or
|
||||
exists(PartialPathNodeRev mid |
|
||||
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead()) and
|
||||
not clearsContentEx(node, ap.getHead()) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
|
||||
@@ -4613,7 +4624,7 @@ private module FlowExploration {
|
||||
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
|
||||
not clearsContentEx(node, ap.getHead().getContent()) and
|
||||
if node.asNode() instanceof CastingNode
|
||||
then compatibleTypes(node.getDataFlowType(), ap.getType())
|
||||
else any()
|
||||
@@ -5047,6 +5058,7 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,21 +87,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -128,7 +116,7 @@ abstract class Configuration extends string {
|
||||
* Holds if an arbitrary number of implicit read steps of content `c` may be
|
||||
* taken at `node`.
|
||||
*/
|
||||
predicate allowImplicitRead(Node node, Content c) { none() }
|
||||
predicate allowImplicitRead(Node node, ContentSet c) { none() }
|
||||
|
||||
/**
|
||||
* Gets the virtual dispatch branching limit when calculating field flow.
|
||||
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -517,16 +479,15 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
)
|
||||
}
|
||||
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
read(node1.asNode(), c, node2.asNode()) and
|
||||
pragma[nomagic]
|
||||
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
|
||||
readSet(node1.asNode(), c, node2.asNode()) and
|
||||
stepFilter(node1, node2, config)
|
||||
or
|
||||
exists(Node n |
|
||||
@@ -536,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
readSet(node1, cs, node2, config) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||
exists(ContentSet cs |
|
||||
clearsContentCached(n.asNode(), cs) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate store(
|
||||
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
|
||||
) {
|
||||
@@ -613,9 +593,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Content c |
|
||||
fwdFlowRead(c, node, cc, config) and
|
||||
fwdFlowConsCand(c, config)
|
||||
exists(ContentSet c |
|
||||
fwdFlowReadSet(c, node, cc, config) and
|
||||
fwdFlowConsCandSet(c, _, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
@@ -639,10 +619,10 @@ private module Stage1 {
|
||||
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
|
||||
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, cc, config) and
|
||||
read(mid, c, node, config)
|
||||
readSet(mid, c, node, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -660,6 +640,16 @@ private module Stage1 {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `cs` may be interpreted in a read as the target of some store
|
||||
* into `c`, in the flow covered by `fwdFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
|
||||
fwdFlowConsCand(c, config) and
|
||||
c = cs.getAReadContent()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
|
||||
exists(RetNodeEx ret |
|
||||
@@ -752,9 +742,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Content c |
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
exists(NodeEx mid, ContentSet c |
|
||||
readSet(node, c, mid, config) and
|
||||
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, toReturn, pragma[only_bind_into](config))
|
||||
)
|
||||
or
|
||||
@@ -780,10 +770,10 @@ private module Stage1 {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowConsCand(Content c, Configuration config) {
|
||||
exists(NodeEx mid, NodeEx node |
|
||||
exists(NodeEx mid, NodeEx node, ContentSet cs |
|
||||
fwdFlow(node, pragma[only_bind_into](config)) and
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
readSet(node, cs, mid, config) and
|
||||
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
|
||||
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
@@ -802,6 +792,7 @@ private module Stage1 {
|
||||
* Holds if `c` is the target of both a read and a store in the flow covered
|
||||
* by `revFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
|
||||
revFlowConsCand(c, conf) and
|
||||
revFlowStore(c, _, _, conf)
|
||||
@@ -900,9 +891,9 @@ private module Stage1 {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
|
||||
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config))
|
||||
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -912,14 +903,17 @@ private module Stage1 {
|
||||
predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
|
||||
revFlow(node, toReturn, pragma[only_bind_into](config)) and
|
||||
exists(state) and
|
||||
exists(returnAp) and
|
||||
exists(ap)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -1014,8 +1008,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -1036,8 +1030,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1189,7 +1183,7 @@ private module Stage2 {
|
||||
|
||||
bindingset[node, state, ap, config]
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
PrevStage::revFlowState(state, config) and
|
||||
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
|
||||
exists(ap) and
|
||||
not stateBarrier(node, state, config)
|
||||
}
|
||||
@@ -1614,7 +1608,7 @@ private module Stage2 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -1769,9 +1763,9 @@ private module LocalFlowBigStep {
|
||||
or
|
||||
node.asNode() instanceof OutNodeExt
|
||||
or
|
||||
store(_, _, node, _, config)
|
||||
Stage2::storeStepCand(_, _, _, node, _, config)
|
||||
or
|
||||
read(_, _, node, config)
|
||||
Stage2::readStepCand(_, _, node, config)
|
||||
or
|
||||
node instanceof FlowCheckNode
|
||||
or
|
||||
@@ -1792,8 +1786,8 @@ private module LocalFlowBigStep {
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
store(node, _, next, _, config) or
|
||||
read(node, _, next, config)
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
|
||||
@@ -1966,7 +1960,24 @@ private module Stage3 {
|
||||
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
|
||||
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
|
||||
PrevStage::revFlow(node, config) and
|
||||
clearsContentCached(node.asNode(), c)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clearContent(NodeEx node, Content c, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
|
||||
c = cs.getAReadContent() and
|
||||
clearSet(node, cs, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap, Configuration config) {
|
||||
clearContent(node, ap.getHead().getContent(), config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
|
||||
@@ -1975,7 +1986,7 @@ private module Stage3 {
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
exists(state) and
|
||||
exists(config) and
|
||||
not clear(node, ap) and
|
||||
not clear(node, ap, config) and
|
||||
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
|
||||
}
|
||||
|
||||
@@ -2403,7 +2414,7 @@ private module Stage3 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -3230,7 +3241,7 @@ private module Stage4 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -4242,7 +4253,7 @@ private module Subpaths {
|
||||
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
|
||||
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
|
||||
store(n1, _, n2, _, _) or
|
||||
read(n1, _, n2, _)
|
||||
readSet(n1, _, n2, _)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -4597,7 +4608,7 @@ private module FlowExploration {
|
||||
or
|
||||
exists(PartialPathNodeRev mid |
|
||||
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead()) and
|
||||
not clearsContentEx(node, ap.getHead()) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
|
||||
@@ -4613,7 +4624,7 @@ private module FlowExploration {
|
||||
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
|
||||
not clearsContentEx(node, ap.getHead().getContent()) and
|
||||
if node.asNode() instanceof CastingNode
|
||||
then compatibleTypes(node.getDataFlowType(), ap.getType())
|
||||
else any()
|
||||
@@ -5047,6 +5058,7 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -326,7 +326,7 @@ private module Cached {
|
||||
predicate jumpStepCached(Node node1, Node node2) { jumpStep(node1, node2) }
|
||||
|
||||
cached
|
||||
predicate clearsContentCached(Node n, Content c) { clearsContent(n, c) }
|
||||
predicate clearsContentCached(Node n, ContentSet c) { clearsContent(n, c) }
|
||||
|
||||
cached
|
||||
predicate isUnreachableInCallCached(Node n, DataFlowCall call) { isUnreachableInCall(n, call) }
|
||||
@@ -373,7 +373,7 @@ private module Cached {
|
||||
// For reads, `x.f`, we want to check that the tracked type after the read (which
|
||||
// is obtained by popping the head of the access path stack) is compatible with
|
||||
// the type of `x.f`.
|
||||
read(_, _, n)
|
||||
readSet(_, _, n)
|
||||
}
|
||||
|
||||
cached
|
||||
@@ -469,7 +469,7 @@ private module Cached {
|
||||
// read
|
||||
exists(Node mid |
|
||||
parameterValueFlowCand(p, mid, false) and
|
||||
read(mid, _, node) and
|
||||
readSet(mid, _, node) and
|
||||
read = true
|
||||
)
|
||||
or
|
||||
@@ -657,8 +657,10 @@ private module Cached {
|
||||
* Holds if `arg` flows to `out` through a call using only
|
||||
* value-preserving steps and a single read step, not taking call
|
||||
* contexts into account, thus representing a getter-step.
|
||||
*
|
||||
* This predicate is exposed for testing only.
|
||||
*/
|
||||
predicate getterStep(ArgNode arg, Content c, Node out) {
|
||||
predicate getterStep(ArgNode arg, ContentSet c, Node out) {
|
||||
argumentValueFlowsThrough(arg, TReadStepTypesSome(_, c, _), out)
|
||||
}
|
||||
|
||||
@@ -781,28 +783,30 @@ private module Cached {
|
||||
parameterValueFlow(p, n.getPreUpdateNode(), TReadStepTypesNone())
|
||||
}
|
||||
|
||||
cached
|
||||
predicate readSet(Node node1, ContentSet c, Node node2) { readStep(node1, c, node2) }
|
||||
|
||||
private predicate store(
|
||||
Node node1, Content c, Node node2, DataFlowType contentType, DataFlowType containerType
|
||||
) {
|
||||
storeStep(node1, c, node2) and
|
||||
contentType = getNodeDataFlowType(node1) and
|
||||
containerType = getNodeDataFlowType(node2)
|
||||
or
|
||||
exists(Node n1, Node n2 |
|
||||
n1 = node1.(PostUpdateNode).getPreUpdateNode() and
|
||||
n2 = node2.(PostUpdateNode).getPreUpdateNode()
|
||||
|
|
||||
argumentValueFlowsThrough(n2, TReadStepTypesSome(containerType, c, contentType), n1)
|
||||
exists(ContentSet cs | c = cs.getAStoreContent() |
|
||||
storeStep(node1, cs, node2) and
|
||||
contentType = getNodeDataFlowType(node1) and
|
||||
containerType = getNodeDataFlowType(node2)
|
||||
or
|
||||
read(n2, c, n1) and
|
||||
contentType = getNodeDataFlowType(n1) and
|
||||
containerType = getNodeDataFlowType(n2)
|
||||
exists(Node n1, Node n2 |
|
||||
n1 = node1.(PostUpdateNode).getPreUpdateNode() and
|
||||
n2 = node2.(PostUpdateNode).getPreUpdateNode()
|
||||
|
|
||||
argumentValueFlowsThrough(n2, TReadStepTypesSome(containerType, cs, contentType), n1)
|
||||
or
|
||||
readSet(n2, cs, n1) and
|
||||
contentType = getNodeDataFlowType(n1) and
|
||||
containerType = getNodeDataFlowType(n2)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
cached
|
||||
predicate read(Node node1, Content c, Node node2) { readStep(node1, c, node2) }
|
||||
|
||||
/**
|
||||
* Holds if data can flow from `node1` to `node2` via a direct assignment to
|
||||
* `f`.
|
||||
@@ -932,16 +936,16 @@ class CastingNode extends Node {
|
||||
}
|
||||
|
||||
private predicate readStepWithTypes(
|
||||
Node n1, DataFlowType container, Content c, Node n2, DataFlowType content
|
||||
Node n1, DataFlowType container, ContentSet c, Node n2, DataFlowType content
|
||||
) {
|
||||
read(n1, c, n2) and
|
||||
readSet(n1, c, n2) and
|
||||
container = getNodeDataFlowType(n1) and
|
||||
content = getNodeDataFlowType(n2)
|
||||
}
|
||||
|
||||
private newtype TReadStepTypesOption =
|
||||
TReadStepTypesNone() or
|
||||
TReadStepTypesSome(DataFlowType container, Content c, DataFlowType content) {
|
||||
TReadStepTypesSome(DataFlowType container, ContentSet c, DataFlowType content) {
|
||||
readStepWithTypes(_, container, c, _, content)
|
||||
}
|
||||
|
||||
@@ -950,7 +954,7 @@ private class ReadStepTypesOption extends TReadStepTypesOption {
|
||||
|
||||
DataFlowType getContainerType() { this = TReadStepTypesSome(result, _, _) }
|
||||
|
||||
Content getContent() { this = TReadStepTypesSome(_, result, _) }
|
||||
ContentSet getContent() { this = TReadStepTypesSome(_, result, _) }
|
||||
|
||||
DataFlowType getContentType() { this = TReadStepTypesSome(_, _, result) }
|
||||
|
||||
@@ -1325,8 +1329,6 @@ abstract class AccessPathFront extends TAccessPathFront {
|
||||
abstract boolean toBoolNonEmpty();
|
||||
|
||||
TypedContent getHead() { this = TFrontHead(result) }
|
||||
|
||||
predicate isClearedAt(Node n) { clearsContentCached(n, this.getHead().getContent()) }
|
||||
}
|
||||
|
||||
class AccessPathFrontNil extends AccessPathFront, TFrontNil {
|
||||
|
||||
@@ -87,21 +87,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -128,7 +116,7 @@ abstract class Configuration extends string {
|
||||
* Holds if an arbitrary number of implicit read steps of content `c` may be
|
||||
* taken at `node`.
|
||||
*/
|
||||
predicate allowImplicitRead(Node node, Content c) { none() }
|
||||
predicate allowImplicitRead(Node node, ContentSet c) { none() }
|
||||
|
||||
/**
|
||||
* Gets the virtual dispatch branching limit when calculating field flow.
|
||||
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -517,16 +479,15 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
)
|
||||
}
|
||||
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
read(node1.asNode(), c, node2.asNode()) and
|
||||
pragma[nomagic]
|
||||
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
|
||||
readSet(node1.asNode(), c, node2.asNode()) and
|
||||
stepFilter(node1, node2, config)
|
||||
or
|
||||
exists(Node n |
|
||||
@@ -536,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
readSet(node1, cs, node2, config) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||
exists(ContentSet cs |
|
||||
clearsContentCached(n.asNode(), cs) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate store(
|
||||
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
|
||||
) {
|
||||
@@ -613,9 +593,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Content c |
|
||||
fwdFlowRead(c, node, cc, config) and
|
||||
fwdFlowConsCand(c, config)
|
||||
exists(ContentSet c |
|
||||
fwdFlowReadSet(c, node, cc, config) and
|
||||
fwdFlowConsCandSet(c, _, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
@@ -639,10 +619,10 @@ private module Stage1 {
|
||||
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
|
||||
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, cc, config) and
|
||||
read(mid, c, node, config)
|
||||
readSet(mid, c, node, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -660,6 +640,16 @@ private module Stage1 {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `cs` may be interpreted in a read as the target of some store
|
||||
* into `c`, in the flow covered by `fwdFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
|
||||
fwdFlowConsCand(c, config) and
|
||||
c = cs.getAReadContent()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
|
||||
exists(RetNodeEx ret |
|
||||
@@ -752,9 +742,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Content c |
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
exists(NodeEx mid, ContentSet c |
|
||||
readSet(node, c, mid, config) and
|
||||
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, toReturn, pragma[only_bind_into](config))
|
||||
)
|
||||
or
|
||||
@@ -780,10 +770,10 @@ private module Stage1 {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowConsCand(Content c, Configuration config) {
|
||||
exists(NodeEx mid, NodeEx node |
|
||||
exists(NodeEx mid, NodeEx node, ContentSet cs |
|
||||
fwdFlow(node, pragma[only_bind_into](config)) and
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
readSet(node, cs, mid, config) and
|
||||
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
|
||||
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
@@ -802,6 +792,7 @@ private module Stage1 {
|
||||
* Holds if `c` is the target of both a read and a store in the flow covered
|
||||
* by `revFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
|
||||
revFlowConsCand(c, conf) and
|
||||
revFlowStore(c, _, _, conf)
|
||||
@@ -900,9 +891,9 @@ private module Stage1 {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
|
||||
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config))
|
||||
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -912,14 +903,17 @@ private module Stage1 {
|
||||
predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
|
||||
revFlow(node, toReturn, pragma[only_bind_into](config)) and
|
||||
exists(state) and
|
||||
exists(returnAp) and
|
||||
exists(ap)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -1014,8 +1008,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -1036,8 +1030,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1189,7 +1183,7 @@ private module Stage2 {
|
||||
|
||||
bindingset[node, state, ap, config]
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
PrevStage::revFlowState(state, config) and
|
||||
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
|
||||
exists(ap) and
|
||||
not stateBarrier(node, state, config)
|
||||
}
|
||||
@@ -1614,7 +1608,7 @@ private module Stage2 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -1769,9 +1763,9 @@ private module LocalFlowBigStep {
|
||||
or
|
||||
node.asNode() instanceof OutNodeExt
|
||||
or
|
||||
store(_, _, node, _, config)
|
||||
Stage2::storeStepCand(_, _, _, node, _, config)
|
||||
or
|
||||
read(_, _, node, config)
|
||||
Stage2::readStepCand(_, _, node, config)
|
||||
or
|
||||
node instanceof FlowCheckNode
|
||||
or
|
||||
@@ -1792,8 +1786,8 @@ private module LocalFlowBigStep {
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
store(node, _, next, _, config) or
|
||||
read(node, _, next, config)
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
|
||||
@@ -1966,7 +1960,24 @@ private module Stage3 {
|
||||
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
|
||||
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
|
||||
PrevStage::revFlow(node, config) and
|
||||
clearsContentCached(node.asNode(), c)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clearContent(NodeEx node, Content c, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
|
||||
c = cs.getAReadContent() and
|
||||
clearSet(node, cs, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap, Configuration config) {
|
||||
clearContent(node, ap.getHead().getContent(), config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
|
||||
@@ -1975,7 +1986,7 @@ private module Stage3 {
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
exists(state) and
|
||||
exists(config) and
|
||||
not clear(node, ap) and
|
||||
not clear(node, ap, config) and
|
||||
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
|
||||
}
|
||||
|
||||
@@ -2403,7 +2414,7 @@ private module Stage3 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -3230,7 +3241,7 @@ private module Stage4 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -4242,7 +4253,7 @@ private module Subpaths {
|
||||
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
|
||||
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
|
||||
store(n1, _, n2, _, _) or
|
||||
read(n1, _, n2, _)
|
||||
readSet(n1, _, n2, _)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -4597,7 +4608,7 @@ private module FlowExploration {
|
||||
or
|
||||
exists(PartialPathNodeRev mid |
|
||||
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead()) and
|
||||
not clearsContentEx(node, ap.getHead()) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
|
||||
@@ -4613,7 +4624,7 @@ private module FlowExploration {
|
||||
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
|
||||
not clearsContentEx(node, ap.getHead().getContent()) and
|
||||
if node.asNode() instanceof CastingNode
|
||||
then compatibleTypes(node.getDataFlowType(), ap.getType())
|
||||
else any()
|
||||
@@ -5047,6 +5058,7 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,21 +87,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -128,7 +116,7 @@ abstract class Configuration extends string {
|
||||
* Holds if an arbitrary number of implicit read steps of content `c` may be
|
||||
* taken at `node`.
|
||||
*/
|
||||
predicate allowImplicitRead(Node node, Content c) { none() }
|
||||
predicate allowImplicitRead(Node node, ContentSet c) { none() }
|
||||
|
||||
/**
|
||||
* Gets the virtual dispatch branching limit when calculating field flow.
|
||||
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -517,16 +479,15 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
)
|
||||
}
|
||||
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
read(node1.asNode(), c, node2.asNode()) and
|
||||
pragma[nomagic]
|
||||
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
|
||||
readSet(node1.asNode(), c, node2.asNode()) and
|
||||
stepFilter(node1, node2, config)
|
||||
or
|
||||
exists(Node n |
|
||||
@@ -536,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
readSet(node1, cs, node2, config) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
// inline to reduce fan-out via `getAReadContent`
|
||||
pragma[inline]
|
||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||
exists(ContentSet cs |
|
||||
clearsContentCached(n.asNode(), cs) and
|
||||
c = cs.getAReadContent()
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate store(
|
||||
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
|
||||
) {
|
||||
@@ -613,9 +593,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Content c |
|
||||
fwdFlowRead(c, node, cc, config) and
|
||||
fwdFlowConsCand(c, config)
|
||||
exists(ContentSet c |
|
||||
fwdFlowReadSet(c, node, cc, config) and
|
||||
fwdFlowConsCandSet(c, _, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
@@ -639,10 +619,10 @@ private module Stage1 {
|
||||
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
|
||||
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, cc, config) and
|
||||
read(mid, c, node, config)
|
||||
readSet(mid, c, node, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -660,6 +640,16 @@ private module Stage1 {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `cs` may be interpreted in a read as the target of some store
|
||||
* into `c`, in the flow covered by `fwdFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
|
||||
fwdFlowConsCand(c, config) and
|
||||
c = cs.getAReadContent()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
|
||||
exists(RetNodeEx ret |
|
||||
@@ -752,9 +742,9 @@ private module Stage1 {
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Content c |
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
exists(NodeEx mid, ContentSet c |
|
||||
readSet(node, c, mid, config) and
|
||||
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, toReturn, pragma[only_bind_into](config))
|
||||
)
|
||||
or
|
||||
@@ -780,10 +770,10 @@ private module Stage1 {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowConsCand(Content c, Configuration config) {
|
||||
exists(NodeEx mid, NodeEx node |
|
||||
exists(NodeEx mid, NodeEx node, ContentSet cs |
|
||||
fwdFlow(node, pragma[only_bind_into](config)) and
|
||||
read(node, c, mid, config) and
|
||||
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
|
||||
readSet(node, cs, mid, config) and
|
||||
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
|
||||
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
@@ -802,6 +792,7 @@ private module Stage1 {
|
||||
* Holds if `c` is the target of both a read and a store in the flow covered
|
||||
* by `revFlow`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
|
||||
revFlowConsCand(c, conf) and
|
||||
revFlowStore(c, _, _, conf)
|
||||
@@ -900,9 +891,9 @@ private module Stage1 {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
|
||||
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config))
|
||||
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
|
||||
read(n1, c, n2, pragma[only_bind_into](config)) and
|
||||
revFlow(n2, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -912,14 +903,17 @@ private module Stage1 {
|
||||
predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
|
||||
revFlow(node, toReturn, pragma[only_bind_into](config)) and
|
||||
exists(state) and
|
||||
exists(returnAp) and
|
||||
exists(ap)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -1014,8 +1008,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -1036,8 +1030,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1189,7 +1183,7 @@ private module Stage2 {
|
||||
|
||||
bindingset[node, state, ap, config]
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
PrevStage::revFlowState(state, config) and
|
||||
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
|
||||
exists(ap) and
|
||||
not stateBarrier(node, state, config)
|
||||
}
|
||||
@@ -1614,7 +1608,7 @@ private module Stage2 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -1769,9 +1763,9 @@ private module LocalFlowBigStep {
|
||||
or
|
||||
node.asNode() instanceof OutNodeExt
|
||||
or
|
||||
store(_, _, node, _, config)
|
||||
Stage2::storeStepCand(_, _, _, node, _, config)
|
||||
or
|
||||
read(_, _, node, config)
|
||||
Stage2::readStepCand(_, _, node, config)
|
||||
or
|
||||
node instanceof FlowCheckNode
|
||||
or
|
||||
@@ -1792,8 +1786,8 @@ private module LocalFlowBigStep {
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
store(node, _, next, _, config) or
|
||||
read(node, _, next, config)
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
|
||||
@@ -1966,7 +1960,24 @@ private module Stage3 {
|
||||
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
|
||||
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
|
||||
PrevStage::revFlow(node, config) and
|
||||
clearsContentCached(node.asNode(), c)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clearContent(NodeEx node, Content c, Configuration config) {
|
||||
exists(ContentSet cs |
|
||||
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
|
||||
c = cs.getAReadContent() and
|
||||
clearSet(node, cs, pragma[only_bind_into](config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate clear(NodeEx node, Ap ap, Configuration config) {
|
||||
clearContent(node, ap.getHead().getContent(), config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
|
||||
@@ -1975,7 +1986,7 @@ private module Stage3 {
|
||||
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
|
||||
exists(state) and
|
||||
exists(config) and
|
||||
not clear(node, ap) and
|
||||
not clear(node, ap, config) and
|
||||
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
|
||||
}
|
||||
|
||||
@@ -2403,7 +2414,7 @@ private module Stage3 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -3230,7 +3241,7 @@ private module Stage4 {
|
||||
Configuration config
|
||||
) {
|
||||
exists(Ap ap2, Content c |
|
||||
store(node1, tc, node2, contentType, config) and
|
||||
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
|
||||
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
|
||||
revFlowConsCand(ap2, c, ap1, config)
|
||||
)
|
||||
@@ -4242,7 +4253,7 @@ private module Subpaths {
|
||||
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
|
||||
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
|
||||
store(n1, _, n2, _, _) or
|
||||
read(n1, _, n2, _)
|
||||
readSet(n1, _, n2, _)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -4597,7 +4608,7 @@ private module FlowExploration {
|
||||
or
|
||||
exists(PartialPathNodeRev mid |
|
||||
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead()) and
|
||||
not clearsContentEx(node, ap.getHead()) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
|
||||
@@ -4613,7 +4624,7 @@ private module FlowExploration {
|
||||
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
|
||||
not fullBarrier(node, config) and
|
||||
not stateBarrier(node, state, config) and
|
||||
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
|
||||
not clearsContentEx(node, ap.getHead().getContent()) and
|
||||
if node.asNode() instanceof CastingNode
|
||||
then compatibleTypes(node.getDataFlowType(), ap.getType())
|
||||
else any()
|
||||
@@ -5047,6 +5058,7 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -256,6 +256,34 @@ class SyntheticFieldContent extends Content, TSyntheticFieldContent {
|
||||
override string toString() { result = s.toString() }
|
||||
}
|
||||
|
||||
/**
|
||||
* An entity that represents a set of `Content`s.
|
||||
*
|
||||
* The set may be interpreted differently depending on whether it is
|
||||
* stored into (`getAStoreContent`) or read from (`getAReadContent`).
|
||||
*/
|
||||
class ContentSet instanceof Content {
|
||||
/** Gets a content that may be stored into when storing into this set. */
|
||||
Content getAStoreContent() { result = this }
|
||||
|
||||
/** Gets a content that may be read from when reading from this set. */
|
||||
Content getAReadContent() { result = this }
|
||||
|
||||
/** Gets a textual representation of this content set. */
|
||||
string toString() { result = super.toString() }
|
||||
|
||||
/**
|
||||
* Holds if this element is at the specified location.
|
||||
* The location spans column `startcolumn` of line `startline` to
|
||||
* column `endcolumn` of line `endline` in file `filepath`.
|
||||
* For more information, see
|
||||
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
|
||||
*/
|
||||
predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
|
||||
super.hasLocationInfo(path, sl, sc, el, ec)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* A guard that validates some expression.
|
||||
*
|
||||
|
||||
@@ -24,7 +24,7 @@ module Public {
|
||||
class SummaryComponent extends TSummaryComponent {
|
||||
/** Gets a textual representation of this summary component. */
|
||||
string toString() {
|
||||
exists(Content c | this = TContentSummaryComponent(c) and result = c.toString())
|
||||
exists(ContentSet c | this = TContentSummaryComponent(c) and result = c.toString())
|
||||
or
|
||||
exists(ArgumentPosition pos |
|
||||
this = TParameterSummaryComponent(pos) and result = "parameter " + pos
|
||||
@@ -41,7 +41,7 @@ module Public {
|
||||
/** Provides predicates for constructing summary components. */
|
||||
module SummaryComponent {
|
||||
/** Gets a summary component for content `c`. */
|
||||
SummaryComponent content(Content c) { result = TContentSummaryComponent(c) }
|
||||
SummaryComponent content(ContentSet c) { result = TContentSummaryComponent(c) }
|
||||
|
||||
/** Gets a summary component for a parameter at position `pos`. */
|
||||
SummaryComponent parameter(ArgumentPosition pos) { result = TParameterSummaryComponent(pos) }
|
||||
@@ -218,7 +218,7 @@ module Public {
|
||||
* arguments at position `pos` to this callable.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate clearsContent(ParameterPosition pos, Content content) { none() }
|
||||
predicate clearsContent(ParameterPosition pos, ContentSet content) { none() }
|
||||
}
|
||||
}
|
||||
|
||||
@@ -231,7 +231,7 @@ module Private {
|
||||
import AccessPathSyntax
|
||||
|
||||
newtype TSummaryComponent =
|
||||
TContentSummaryComponent(Content c) or
|
||||
TContentSummaryComponent(ContentSet c) or
|
||||
TParameterSummaryComponent(ArgumentPosition pos) or
|
||||
TArgumentSummaryComponent(ParameterPosition pos) or
|
||||
TReturnSummaryComponent(ReturnKind rk)
|
||||
@@ -540,7 +540,7 @@ module Private {
|
||||
exists(SummarizedCallable c, SummaryComponentStack s, SummaryComponent head | head = s.head() |
|
||||
n = summaryNodeInputState(c, s) and
|
||||
(
|
||||
exists(Content cont |
|
||||
exists(ContentSet cont |
|
||||
head = TContentSummaryComponent(cont) and result = getContentType(cont)
|
||||
)
|
||||
or
|
||||
@@ -554,7 +554,7 @@ module Private {
|
||||
or
|
||||
n = summaryNodeOutputState(c, s) and
|
||||
(
|
||||
exists(Content cont |
|
||||
exists(ContentSet cont |
|
||||
head = TContentSummaryComponent(cont) and result = getContentType(cont)
|
||||
)
|
||||
or
|
||||
@@ -669,7 +669,7 @@ module Private {
|
||||
* Holds if there is a read step of content `c` from `pred` to `succ`, which
|
||||
* is synthesized from a flow summary.
|
||||
*/
|
||||
predicate summaryReadStep(Node pred, Content c, Node succ) {
|
||||
predicate summaryReadStep(Node pred, ContentSet c, Node succ) {
|
||||
exists(SummarizedCallable sc, SummaryComponentStack s |
|
||||
pred = summaryNodeInputState(sc, s.drop(1)) and
|
||||
succ = summaryNodeInputState(sc, s) and
|
||||
@@ -681,7 +681,7 @@ module Private {
|
||||
* Holds if there is a store step of content `c` from `pred` to `succ`, which
|
||||
* is synthesized from a flow summary.
|
||||
*/
|
||||
predicate summaryStoreStep(Node pred, Content c, Node succ) {
|
||||
predicate summaryStoreStep(Node pred, ContentSet c, Node succ) {
|
||||
exists(SummarizedCallable sc, SummaryComponentStack s |
|
||||
pred = summaryNodeOutputState(sc, s) and
|
||||
succ = summaryNodeOutputState(sc, s.drop(1)) and
|
||||
@@ -708,7 +708,7 @@ module Private {
|
||||
* `a` on line 2 to the post-update node for `a` on that line (via an intermediate
|
||||
* node where field `b` is cleared).
|
||||
*/
|
||||
predicate summaryClearsContent(Node n, Content c) {
|
||||
predicate summaryClearsContent(Node n, ContentSet c) {
|
||||
exists(SummarizedCallable sc, ParameterPosition pos |
|
||||
n = summaryNode(sc, TSummaryNodeClearsContentState(pos, true)) and
|
||||
sc.clearsContent(pos, c)
|
||||
@@ -730,7 +730,8 @@ module Private {
|
||||
* In such cases, it is important to prevent use-use flow out of
|
||||
* `arg` (see comment for `summaryClearsContent`).
|
||||
*/
|
||||
predicate summaryClearsContentArg(ArgNode arg, Content c) {
|
||||
pragma[nomagic]
|
||||
predicate summaryClearsContentArg(ArgNode arg, ContentSet c) {
|
||||
exists(DataFlowCall call, SummarizedCallable sc, ParameterPosition ppos |
|
||||
argumentPositionMatch(call, arg, ppos) and
|
||||
viableParam(call, sc, ppos, _) and
|
||||
@@ -775,7 +776,7 @@ module Private {
|
||||
* NOTE: This step should not be used in global data-flow/taint-tracking, but may
|
||||
* be useful to include in the exposed local data-flow/taint-tracking relations.
|
||||
*/
|
||||
predicate summaryGetterStep(ArgNode arg, Content c, Node out) {
|
||||
predicate summaryGetterStep(ArgNode arg, ContentSet c, Node out) {
|
||||
exists(ReturnKindExt rk, Node mid, ReturnNodeExt ret |
|
||||
summaryReadStep(summaryArgParam(arg, rk, out), c, mid) and
|
||||
summaryLocalStep(mid, ret, _) and
|
||||
@@ -790,7 +791,7 @@ module Private {
|
||||
* NOTE: This step should not be used in global data-flow/taint-tracking, but may
|
||||
* be useful to include in the exposed local data-flow/taint-tracking relations.
|
||||
*/
|
||||
predicate summarySetterStep(ArgNode arg, Content c, Node out) {
|
||||
predicate summarySetterStep(ArgNode arg, ContentSet c, Node out) {
|
||||
exists(ReturnKindExt rk, Node mid, ReturnNodeExt ret |
|
||||
summaryLocalStep(summaryArgParam(arg, rk, out), mid, _) and
|
||||
summaryStoreStep(mid, c, ret) and
|
||||
@@ -1130,7 +1131,7 @@ module Private {
|
||||
if preservesValue = true then value = "value" else value = "taint"
|
||||
)
|
||||
or
|
||||
exists(Content c |
|
||||
exists(ContentSet c |
|
||||
Private::Steps::summaryReadStep(a.asNode(), c, b.asNode()) and
|
||||
value = "read (" + c + ")"
|
||||
or
|
||||
|
||||
@@ -109,16 +109,6 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation into `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerIn(node, state)
|
||||
}
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
@@ -126,16 +116,6 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation out of `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerOut(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
@@ -181,7 +161,7 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
this.isAdditionalTaintStep(node1, state1, node2, state2)
|
||||
}
|
||||
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::Content c) {
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
|
||||
(this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
|
||||
defaultImplicitTaintRead(node, c)
|
||||
}
|
||||
|
||||
@@ -109,16 +109,6 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation into `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerIn(node, state)
|
||||
}
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
@@ -126,16 +116,6 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation out of `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerOut(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
@@ -181,7 +161,7 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
this.isAdditionalTaintStep(node1, state1, node2, state2)
|
||||
}
|
||||
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::Content c) {
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
|
||||
(this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
|
||||
defaultImplicitTaintRead(node, c)
|
||||
}
|
||||
|
||||
@@ -0,0 +1,176 @@
|
||||
/**
|
||||
* Provides an implementation of global (interprocedural) taint tracking.
|
||||
* This file re-exports the local (intraprocedural) taint-tracking analysis
|
||||
* from `TaintTrackingParameter::Public` and adds a global analysis, mainly
|
||||
* exposed through the `Configuration` class. For some languages, this file
|
||||
* exists in several identical copies, allowing queries to use multiple
|
||||
* `Configuration` classes that depend on each other without introducing
|
||||
* mutual recursion among those configurations.
|
||||
*/
|
||||
|
||||
import TaintTrackingParameter::Public
|
||||
private import TaintTrackingParameter::Private
|
||||
|
||||
/**
|
||||
* A configuration of interprocedural taint tracking analysis. This defines
|
||||
* sources, sinks, and any other configurable aspect of the analysis. Each
|
||||
* use of the taint tracking library must define its own unique extension of
|
||||
* this abstract class.
|
||||
*
|
||||
* A taint-tracking configuration is a special data flow configuration
|
||||
* (`DataFlow::Configuration`) that allows for flow through nodes that do not
|
||||
* necessarily preserve values but are still relevant from a taint tracking
|
||||
* perspective. (For example, string concatenation, where one of the operands
|
||||
* is tainted.)
|
||||
*
|
||||
* To create a configuration, extend this class with a subclass whose
|
||||
* characteristic predicate is a unique singleton string. For example, write
|
||||
*
|
||||
* ```ql
|
||||
* class MyAnalysisConfiguration extends TaintTracking::Configuration {
|
||||
* MyAnalysisConfiguration() { this = "MyAnalysisConfiguration" }
|
||||
* // Override `isSource` and `isSink`.
|
||||
* // Optionally override `isSanitizer`.
|
||||
* // Optionally override `isSanitizerIn`.
|
||||
* // Optionally override `isSanitizerOut`.
|
||||
* // Optionally override `isSanitizerGuard`.
|
||||
* // Optionally override `isAdditionalTaintStep`.
|
||||
* }
|
||||
* ```
|
||||
*
|
||||
* Then, to query whether there is flow between some `source` and `sink`,
|
||||
* write
|
||||
*
|
||||
* ```ql
|
||||
* exists(MyAnalysisConfiguration cfg | cfg.hasFlow(source, sink))
|
||||
* ```
|
||||
*
|
||||
* Multiple configurations can coexist, but it is unsupported to depend on
|
||||
* another `TaintTracking::Configuration` or a `DataFlow::Configuration` in the
|
||||
* overridden predicates that define sources, sinks, or additional steps.
|
||||
* Instead, the dependency should go to a `TaintTracking2::Configuration` or a
|
||||
* `DataFlow2::Configuration`, `DataFlow3::Configuration`, etc.
|
||||
*/
|
||||
abstract class Configuration extends DataFlow::Configuration {
|
||||
bindingset[this]
|
||||
Configuration() { any() }
|
||||
|
||||
/**
|
||||
* Holds if `source` is a relevant taint source.
|
||||
*
|
||||
* The smaller this predicate is, the faster `hasFlow()` will converge.
|
||||
*/
|
||||
// overridden to provide taint-tracking specific qldoc
|
||||
override predicate isSource(DataFlow::Node source) { none() }
|
||||
|
||||
/**
|
||||
* Holds if `source` is a relevant taint source with the given initial
|
||||
* `state`.
|
||||
*
|
||||
* The smaller this predicate is, the faster `hasFlow()` will converge.
|
||||
*/
|
||||
// overridden to provide taint-tracking specific qldoc
|
||||
override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) { none() }
|
||||
|
||||
/**
|
||||
* Holds if `sink` is a relevant taint sink
|
||||
*
|
||||
* The smaller this predicate is, the faster `hasFlow()` will converge.
|
||||
*/
|
||||
// overridden to provide taint-tracking specific qldoc
|
||||
override predicate isSink(DataFlow::Node sink) { none() }
|
||||
|
||||
/**
|
||||
* Holds if `sink` is a relevant taint sink accepting `state`.
|
||||
*
|
||||
* The smaller this predicate is, the faster `hasFlow()` will converge.
|
||||
*/
|
||||
// overridden to provide taint-tracking specific qldoc
|
||||
override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) { none() }
|
||||
|
||||
/** Holds if the node `node` is a taint sanitizer. */
|
||||
predicate isSanitizer(DataFlow::Node node) { none() }
|
||||
|
||||
final override predicate isBarrier(DataFlow::Node node) {
|
||||
this.isSanitizer(node) or
|
||||
defaultTaintSanitizer(node)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the node `node` is a taint sanitizer when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizer(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizer(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
predicate isSanitizerOut(DataFlow::Node node) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) {
|
||||
this.isSanitizerGuard(guard) or defaultTaintSanitizerGuard(guard)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if taint propagation through nodes guarded by `guard` is prohibited
|
||||
* when the flow state is `state`.
|
||||
*/
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) {
|
||||
this.isSanitizerGuard(guard, state)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if taint may propagate from `node1` to `node2` in addition to the normal data-flow and taint steps.
|
||||
*/
|
||||
predicate isAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2) { none() }
|
||||
|
||||
final override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
|
||||
this.isAdditionalTaintStep(node1, node2) or
|
||||
defaultAdditionalTaintStep(node1, node2)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if taint may propagate from `node1` to `node2` in addition to the normal data-flow and taint steps.
|
||||
* This step is only applicable in `state1` and updates the flow state to `state2`.
|
||||
*/
|
||||
predicate isAdditionalTaintStep(
|
||||
DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
|
||||
DataFlow::FlowState state2
|
||||
) {
|
||||
none()
|
||||
}
|
||||
|
||||
final override predicate isAdditionalFlowStep(
|
||||
DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
|
||||
DataFlow::FlowState state2
|
||||
) {
|
||||
this.isAdditionalTaintStep(node1, state1, node2, state2)
|
||||
}
|
||||
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
|
||||
(this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
|
||||
defaultImplicitTaintRead(node, c)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if taint may flow from `source` to `sink` for this configuration.
|
||||
*/
|
||||
// overridden to provide taint-tracking specific qldoc
|
||||
override predicate hasFlow(DataFlow::Node source, DataFlow::Node sink) {
|
||||
super.hasFlow(source, sink)
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,5 @@
|
||||
import semmle.code.java.dataflow.internal.TaintTrackingUtil as Public
|
||||
|
||||
module Private {
|
||||
import semmle.code.java.dataflow.DataFlow3::DataFlow3 as DataFlow
|
||||
}
|
||||
@@ -1,5 +1,4 @@
|
||||
import java
|
||||
import semmle.code.java.JDKAnnotations
|
||||
|
||||
/**
|
||||
* Direct flow of values (i.e. object references) through expressions.
|
||||
|
||||
@@ -3,8 +3,6 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.Type
|
||||
import semmle.code.java.Member
|
||||
|
||||
/*--- Types ---*/
|
||||
/** The interface `org.apache.directory.ldap.client.api.LdapConnection`. */
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
/** The interface `org.hibernate.query.QueryProducer`. */
|
||||
class HibernateQueryProducer extends RefType {
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
private class SsrfSinkCsv extends SinkModelCsv {
|
||||
override predicate row(string row) {
|
||||
|
||||
@@ -2,8 +2,7 @@
|
||||
* Provides classes and predicates for working with the Java JDBC API.
|
||||
*/
|
||||
|
||||
import semmle.code.java.Type
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
/*--- Types ---*/
|
||||
/** The interface `java.sql.Connection`. */
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
private class SsrfSinkCsv extends SinkModelCsv {
|
||||
override predicate row(string row) {
|
||||
|
||||
@@ -3,8 +3,6 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.Type
|
||||
import semmle.code.java.Member
|
||||
|
||||
/*--- Types ---*/
|
||||
/** The interface `javax.naming.Context`. */
|
||||
|
||||
@@ -2,7 +2,7 @@
|
||||
* Provides models for working with the JSON-java library (package `org.json`).
|
||||
*/
|
||||
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
private class FlowModels extends SummaryModelCsv {
|
||||
override predicate row(string row) {
|
||||
|
||||
@@ -1,7 +1,7 @@
|
||||
/** Provides classes and predicates to reason about logging. */
|
||||
|
||||
import java
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
private class LoggingSummaryModels extends SummaryModelCsv {
|
||||
override predicate row(string row) {
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
/** The class `org.apache.ibatis.jdbc.SqlRunner`. */
|
||||
class MyBatisSqlRunner extends RefType {
|
||||
|
||||
@@ -1,6 +1,6 @@
|
||||
/** Definitions related to `java.util.Optional`. */
|
||||
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
private class OptionalModel extends SummaryModelCsv {
|
||||
override predicate row(string s) {
|
||||
|
||||
@@ -1,6 +1,6 @@
|
||||
/** Definitions related to `java.util.regex`. */
|
||||
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
private class RegexModel extends SummaryModelCsv {
|
||||
override predicate row(string s) {
|
||||
|
||||
@@ -30,7 +30,7 @@ class Yaml extends RefType {
|
||||
Yaml() { this.getAnAncestor().hasQualifiedName("org.yaml.snakeyaml", "Yaml") }
|
||||
}
|
||||
|
||||
private class SafeYamlConstructionFlowConfig extends DataFlow2::Configuration {
|
||||
private class SafeYamlConstructionFlowConfig extends DataFlow3::Configuration {
|
||||
SafeYamlConstructionFlowConfig() { this = "SnakeYaml::SafeYamlConstructionFlowConfig" }
|
||||
|
||||
override predicate isSource(DataFlow::Node src) {
|
||||
@@ -65,7 +65,7 @@ private class SnakeYamlParse extends MethodAccess {
|
||||
}
|
||||
}
|
||||
|
||||
private class SafeYamlFlowConfig extends DataFlow3::Configuration {
|
||||
private class SafeYamlFlowConfig extends DataFlow2::Configuration {
|
||||
SafeYamlFlowConfig() { this = "SnakeYaml::SafeYamlFlowConfig" }
|
||||
|
||||
override predicate isSource(DataFlow::Node src) { src.asExpr() instanceof SafeYaml }
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
/** The class `org.springframework.jdbc.core.JdbcTemplate`. */
|
||||
class JdbcTemplate extends RefType {
|
||||
|
||||
@@ -3,8 +3,6 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.Type
|
||||
import semmle.code.java.Member
|
||||
|
||||
/*--- Types ---*/
|
||||
/** The class `org.springframework.ldap.core.LdapTemplate`. */
|
||||
|
||||
@@ -1,6 +1,6 @@
|
||||
/** Definitions related to `java.util.stream`. */
|
||||
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
private class StreamModel extends SummaryModelCsv {
|
||||
override predicate row(string s) {
|
||||
|
||||
@@ -3,8 +3,6 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.Type
|
||||
import semmle.code.java.Member
|
||||
|
||||
/*--- Types ---*/
|
||||
/** The interface `com.unboundid.ldap.sdk.ReadOnlySearchRequest`. */
|
||||
|
||||
@@ -3,8 +3,8 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
import semmle.code.xml.AndroidManifest
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.xml.AndroidManifest
|
||||
|
||||
/**
|
||||
* Gets a reflexive/transitive superType
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
/** The class `android.content.ContentValues`. */
|
||||
class ContentValues extends Class {
|
||||
|
||||
@@ -1,7 +1,7 @@
|
||||
import java
|
||||
private import semmle.code.java.dataflow.DataFlow
|
||||
import semmle.code.java.dataflow.FlowSteps
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.FlowSteps
|
||||
|
||||
/**
|
||||
* The class `android.content.Intent`.
|
||||
|
||||
@@ -1,9 +1,9 @@
|
||||
/** Provides classes and predicates for working with SQLite databases. */
|
||||
|
||||
import java
|
||||
import Android
|
||||
import semmle.code.java.dataflow.FlowSteps
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.FlowSteps
|
||||
private import semmle.code.java.frameworks.android.Android
|
||||
|
||||
/**
|
||||
* The class `android.database.sqlite.SQLiteDatabase`.
|
||||
|
||||
@@ -1,6 +1,7 @@
|
||||
/** Provides classes related to `android.content.SharedPreferences`. */
|
||||
|
||||
import java
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
/** The interface `android.content.SharedPreferences`. */
|
||||
class SharedPreferences extends Interface {
|
||||
@@ -55,3 +56,19 @@ class StoreSharedPreferenceMethod extends Method {
|
||||
this.hasName(["commit", "apply"])
|
||||
}
|
||||
}
|
||||
|
||||
private class SharedPreferencesSummaries extends SummaryModelCsv {
|
||||
override predicate row(string row) {
|
||||
row =
|
||||
[
|
||||
"android.content;SharedPreferences$Editor;true;clear;;;Argument[-1];ReturnValue;value",
|
||||
"android.content;SharedPreferences$Editor;true;putBoolean;;;Argument[-1];ReturnValue;value",
|
||||
"android.content;SharedPreferences$Editor;true;putFloat;;;Argument[-1];ReturnValue;value",
|
||||
"android.content;SharedPreferences$Editor;true;putInt;;;Argument[-1];ReturnValue;value",
|
||||
"android.content;SharedPreferences$Editor;true;putLong;;;Argument[-1];ReturnValue;value",
|
||||
"android.content;SharedPreferences$Editor;true;putString;;;Argument[-1];ReturnValue;value",
|
||||
"android.content;SharedPreferences$Editor;true;putStringSet;;;Argument[-1];ReturnValue;value",
|
||||
"android.content;SharedPreferences$Editor;true;remove;;;Argument[-1];ReturnValue;value"
|
||||
]
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,8 +1,8 @@
|
||||
/** Provides classes and predicates for working with Android widgets. */
|
||||
|
||||
import java
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
import semmle.code.java.dataflow.FlowSources
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.FlowSources
|
||||
|
||||
private class AndroidWidgetSourceModels extends SourceModelCsv {
|
||||
override predicate row(string row) {
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
/**
|
||||
* Methods annotated with this allow for generation of "plain SQL"
|
||||
|
||||
@@ -1,5 +1,4 @@
|
||||
import java
|
||||
import semmle.code.xml.XML
|
||||
|
||||
/**
|
||||
* Holds if any struts XML files are included in this snapshot.
|
||||
|
||||
@@ -2,9 +2,9 @@
|
||||
|
||||
import java
|
||||
import semmle.code.java.dataflow.FlowSources
|
||||
import semmle.code.java.dataflow.DataFlow3
|
||||
import semmle.code.java.dataflow.DataFlow2
|
||||
import semmle.code.java.dataflow.TaintTracking
|
||||
import semmle.code.java.dataflow.TaintTracking2
|
||||
import semmle.code.java.dataflow.TaintTracking3
|
||||
import semmle.code.java.security.AndroidIntentRedirection
|
||||
|
||||
/**
|
||||
@@ -38,7 +38,7 @@ private class OriginalIntentSanitizer extends IntentRedirectionSanitizer {
|
||||
* Data flow configuration used to discard incoming Intents
|
||||
* flowing directly to sinks that start Android components.
|
||||
*/
|
||||
private class SameIntentBeingRelaunchedConfiguration extends DataFlow3::Configuration {
|
||||
private class SameIntentBeingRelaunchedConfiguration extends DataFlow2::Configuration {
|
||||
SameIntentBeingRelaunchedConfiguration() { this = "SameIntentBeingRelaunchedConfiguration" }
|
||||
|
||||
override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
|
||||
@@ -74,7 +74,7 @@ private class IntentWithTaintedComponent extends DataFlow::Node {
|
||||
/**
|
||||
* A taint tracking configuration for tainted data flowing to an `Intent`'s component.
|
||||
*/
|
||||
private class TaintedIntentComponentConf extends TaintTracking2::Configuration {
|
||||
private class TaintedIntentComponentConf extends TaintTracking3::Configuration {
|
||||
TaintedIntentComponentConf() { this = "TaintedIntentComponentConf" }
|
||||
|
||||
override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
|
||||
|
||||
@@ -142,7 +142,7 @@ class SensitiveCommunicationConfig extends TaintTracking::Configuration {
|
||||
*/
|
||||
override predicate isSanitizer(DataFlow::Node node) { node instanceof ExplicitIntentSanitizer }
|
||||
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::Content c) {
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
|
||||
super.allowImplicitRead(node, c)
|
||||
or
|
||||
this.isSink(node)
|
||||
|
||||
@@ -3,7 +3,6 @@
|
||||
import java
|
||||
import semmle.code.java.frameworks.JAXB
|
||||
import semmle.code.java.dataflow.DataFlow
|
||||
import semmle.code.java.dataflow.DataFlow2
|
||||
import semmle.code.java.security.CleartextStorageQuery
|
||||
import semmle.code.java.security.CleartextStoragePropertiesQuery
|
||||
|
||||
@@ -74,7 +73,7 @@ private Expr getInstanceInput(DataFlow::Node instance, RefType t) {
|
||||
)
|
||||
}
|
||||
|
||||
private class ClassStoreFlowConfig extends DataFlow2::Configuration {
|
||||
private class ClassStoreFlowConfig extends DataFlow::Configuration {
|
||||
ClassStoreFlowConfig() { this = "ClassStoreFlowConfig" }
|
||||
|
||||
override predicate isSource(DataFlow::Node src) { src.asExpr() instanceof ClassStore }
|
||||
|
||||
@@ -3,6 +3,7 @@
|
||||
import java
|
||||
private import semmle.code.java.dataflow.DataFlow4
|
||||
private import semmle.code.java.dataflow.TaintTracking
|
||||
private import semmle.code.java.dataflow.TaintTracking2
|
||||
private import semmle.code.java.security.SensitiveActions
|
||||
|
||||
/** A sink representing persistent storage that saves data in clear text. */
|
||||
@@ -39,7 +40,7 @@ abstract class Storable extends Call {
|
||||
abstract Expr getAStore();
|
||||
}
|
||||
|
||||
private class SensitiveSourceFlowConfig extends TaintTracking::Configuration {
|
||||
private class SensitiveSourceFlowConfig extends TaintTracking2::Configuration {
|
||||
SensitiveSourceFlowConfig() { this = "SensitiveSourceFlowConfig" }
|
||||
|
||||
override predicate isSource(DataFlow::Node src) { src.asExpr() instanceof SensitiveExpr }
|
||||
|
||||
@@ -1,6 +1,7 @@
|
||||
/** Provides classes and predicates for working with implicit `PendingIntent`s. */
|
||||
|
||||
import java
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.TaintTracking
|
||||
private import semmle.code.java.frameworks.android.Intent
|
||||
private import semmle.code.java.frameworks.android.PendingIntent
|
||||
|
||||
@@ -36,7 +36,7 @@ class ImplicitPendingIntentStartConf extends TaintTracking::Configuration {
|
||||
any(ImplicitPendingIntentAdditionalTaintStep c).step(node1, state1, node2, state2)
|
||||
}
|
||||
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::Content c) {
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
|
||||
super.allowImplicitRead(node, c)
|
||||
or
|
||||
this.isSink(node, _) and
|
||||
|
||||
@@ -17,7 +17,7 @@ class InsecureTrustManagerConfiguration extends DataFlow::Configuration {
|
||||
|
||||
override predicate isSink(DataFlow::Node sink) { sink instanceof InsecureTrustManagerSink }
|
||||
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::Content c) {
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
|
||||
(this.isSink(node) or this.isAdditionalFlowStep(node, _)) and
|
||||
node.getType() instanceof Array and
|
||||
c instanceof DataFlow::ArrayContent
|
||||
|
||||
@@ -99,6 +99,9 @@ class AndroidProviderXmlElement extends AndroidComponentXmlElement {
|
||||
this.getAnAttribute().(AndroidPermissionXmlAttribute).isRead()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if this provider element has the attribute `android:grantUriPermissions` set to `true`.
|
||||
*/
|
||||
predicate grantsUriPermissions() {
|
||||
exists(AndroidXmlAttribute attr |
|
||||
this.getAnAttribute() = attr and
|
||||
|
||||
@@ -10,7 +10,6 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.JDKAnnotations
|
||||
|
||||
class NonConstantSourceField extends Field {
|
||||
NonConstantSourceField() {
|
||||
|
||||
@@ -1,3 +1,15 @@
|
||||
## 0.1.0
|
||||
|
||||
### Query Metadata Changes
|
||||
|
||||
* Added the `security-severity` tag to several queries.
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* Fixed "Local information disclosure in a temporary directory" (`java/local-temp-file-or-directory-information-disclosure`) to resolve false-negatives when OS isn't properly used as logical guard.
|
||||
* The `SwitchCase.getRuleExpression()` predicate now gets expressions for case rules with an expression on the right-hand side of the arrow belonging to both `SwitchStmt` and `SwitchExpr`, and the corresponding `getRuleStatement()` no longer returns an `ExprStmt` in either case. Previously `SwitchStmt` and `SwitchExpr` behaved differently in
|
||||
this respect.
|
||||
|
||||
## 0.0.13
|
||||
|
||||
## 0.0.12
|
||||
@@ -8,7 +20,7 @@
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* Updated "Local information disclosure in a temporary directory" (`java/local-temp-file-or-directory-information-disclosure`) to remove false-positives when OS is properly used as logical guard.
|
||||
* Updated "Local information disclosure in a temporary directory" (`java/local-temp-file-or-directory-information-disclosure`) to remove false-positives when OS is properly used as logical guard.
|
||||
|
||||
## 0.0.11
|
||||
|
||||
|
||||
@@ -12,7 +12,6 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.JDKAnnotations
|
||||
import semmle.code.java.Collections
|
||||
import semmle.code.java.Maps
|
||||
import semmle.code.java.frameworks.javaee.ejb.EJB
|
||||
|
||||
@@ -12,7 +12,6 @@
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.JDKAnnotations
|
||||
|
||||
predicate isSerializable(RefType t) { t.getAnAncestor() instanceof TypeSerializable }
|
||||
|
||||
|
||||
@@ -16,6 +16,6 @@ import java
|
||||
from DoStmt do, ContinueStmt continue
|
||||
where
|
||||
do.getCondition().(BooleanLiteral).getBooleanValue() = false and
|
||||
continue.(JumpStmt).getTarget() = do
|
||||
continue.getTarget() = do
|
||||
select continue, "This 'continue' never re-runs the loop - the $@ is always false.",
|
||||
do.getCondition(), "loop condition"
|
||||
|
||||
@@ -32,7 +32,7 @@ predicate loopExit(LoopStmt loop, Stmt exit) {
|
||||
exit.getEnclosingStmt*() = loop.getBody() and
|
||||
(
|
||||
exit instanceof ReturnStmt or
|
||||
exit.(BreakStmt).(JumpStmt).getTarget() = loop.getEnclosingStmt*()
|
||||
exit.(BreakStmt).getTarget() = loop.getEnclosingStmt*()
|
||||
)
|
||||
}
|
||||
|
||||
|
||||
@@ -44,11 +44,11 @@ class PointlessLoop extends WhileStmt {
|
||||
PointlessLoop() {
|
||||
this.getCondition().(BooleanLiteral).getBooleanValue() = true and
|
||||
// The only `break` must be the last statement.
|
||||
forall(BreakStmt break | break.(JumpStmt).getTarget() = this |
|
||||
forall(BreakStmt break | break.getTarget() = this |
|
||||
this.getStmt().(BlockStmt).getLastStmt() = break
|
||||
) and
|
||||
// No `continue` statements.
|
||||
not exists(ContinueStmt continue | continue.(JumpStmt).getTarget() = this)
|
||||
not exists(ContinueStmt continue | continue.getTarget() = this)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -20,7 +20,7 @@ where
|
||||
not exists(Variable cookie, MethodAccess m |
|
||||
add.getArgument(0) = cookie.getAnAccess() and
|
||||
m.getMethod().getName() = "setSecure" and
|
||||
m.getArgument(0).(BooleanLiteral).getBooleanValue() = true and
|
||||
m.getArgument(0).(CompileTimeConstantExpr).getBooleanValue() = true and
|
||||
m.getQualifier() = cookie.getAnAccess()
|
||||
)
|
||||
select add, "Cookie is added to response without the 'secure' flag being set."
|
||||
|
||||
@@ -26,7 +26,7 @@ predicate loopCondition(LoopStmt loop, Expr cond, boolean polarity) {
|
||||
ifstmt.getEnclosingStmt*() = loop.getBody() and
|
||||
ifstmt.getCondition() = cond and
|
||||
(
|
||||
exit.(BreakStmt).(JumpStmt).getTarget() = loop or
|
||||
exit.(BreakStmt).getTarget() = loop or
|
||||
exit.(ReturnStmt).getEnclosingStmt*() = loop.getBody()
|
||||
) and
|
||||
(
|
||||
|
||||
@@ -1,4 +0,0 @@
|
||||
---
|
||||
category: queryMetadata
|
||||
---
|
||||
* Added the `security-severity` tag to several queries.
|
||||
@@ -1,4 +0,0 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* Fixed "Local information disclosure in a temporary directory" (`java/local-temp-file-or-directory-information-disclosure`) to resolve false-negatives when OS isn't properly used as logical guard.
|
||||
@@ -0,0 +1,6 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* Query `java/insecure-cookie` no longer produces a false positive if
|
||||
`cookie.setSecure(...)` is called passing a constant that always equals
|
||||
`true`.
|
||||
@@ -1,5 +1,11 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
## 0.1.0
|
||||
|
||||
### Query Metadata Changes
|
||||
|
||||
* Added the `security-severity` tag to several queries.
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* Fixed "Local information disclosure in a temporary directory" (`java/local-temp-file-or-directory-information-disclosure`) to resolve false-negatives when OS isn't properly used as logical guard.
|
||||
* The `SwitchCase.getRuleExpression()` predicate now gets expressions for case rules with an expression on the right-hand side of the arrow belonging to both `SwitchStmt` and `SwitchExpr`, and the corresponding `getRuleStatement()` no longer returns an `ExprStmt` in either case. Previously `SwitchStmt` and `SwitchExpr` behaved differently in
|
||||
this respect.
|
||||
@@ -1,2 +1,2 @@
|
||||
---
|
||||
lastReleaseVersion: 0.0.13
|
||||
lastReleaseVersion: 0.1.0
|
||||
|
||||
@@ -1,5 +1,6 @@
|
||||
import java
|
||||
import semmle.code.java.dataflow.FlowSources
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.FlowSources
|
||||
|
||||
/** The class `com.jfinal.core.Controller`. */
|
||||
class JFinalController extends RefType {
|
||||
|
||||
@@ -40,7 +40,7 @@ class GetContentIntentConfig extends TaintTracking2::Configuration {
|
||||
)
|
||||
}
|
||||
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::Content content) {
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet content) {
|
||||
super.allowImplicitRead(node, content)
|
||||
or
|
||||
// Allow the wrapped intent created by Intent.getChooser to be consumed
|
||||
|
||||
@@ -11,6 +11,8 @@
|
||||
|
||||
import java
|
||||
import semmle.code.java.controlflow.Guards
|
||||
import semmle.code.java.dataflow.FlowSources
|
||||
import semmle.code.java.dataflow.TaintTracking
|
||||
import experimental.semmle.code.java.PathSanitizer
|
||||
import AndroidWebResourceResponse
|
||||
import DataFlow::PathGraph
|
||||
|
||||
@@ -12,6 +12,8 @@
|
||||
|
||||
import java
|
||||
import UnsafeUrlForward
|
||||
import semmle.code.java.dataflow.FlowSources
|
||||
import semmle.code.java.dataflow.TaintTracking
|
||||
import experimental.semmle.code.java.PathSanitizer
|
||||
import DataFlow::PathGraph
|
||||
|
||||
|
||||
@@ -1,6 +1,7 @@
|
||||
import java
|
||||
import experimental.semmle.code.java.frameworks.Jsf
|
||||
import semmle.code.java.dataflow.FlowSources
|
||||
private import experimental.semmle.code.java.frameworks.Jsf
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
private import semmle.code.java.dataflow.FlowSources
|
||||
private import semmle.code.java.dataflow.StringPrefixes
|
||||
|
||||
/** A sink for unsafe URL forward vulnerabilities. */
|
||||
|
||||
@@ -1,6 +1,7 @@
|
||||
import java
|
||||
import semmle.code.java.controlflow.Guards
|
||||
import semmle.code.java.dataflow.FlowSources
|
||||
private import semmle.code.java.controlflow.Guards
|
||||
private import semmle.code.java.dataflow.FlowSources
|
||||
private import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
/** A barrier guard that protects against path traversal vulnerabilities. */
|
||||
abstract class PathTraversalBarrierGuard extends DataFlow::BarrierGuard { }
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
name: codeql/java-queries
|
||||
version: 0.1.0-dev
|
||||
version: 0.1.1-dev
|
||||
groups:
|
||||
- java
|
||||
- queries
|
||||
|
||||
@@ -1,13 +1,9 @@
|
||||
edges
|
||||
| UnsafeReflection.java:21:28:21:60 | getParameter(...) : String | UnsafeReflection.java:25:29:25:59 | getDeclaredConstructors(...) : Constructor[] |
|
||||
| UnsafeReflection.java:21:28:21:60 | getParameter(...) : String | UnsafeReflection.java:25:29:25:62 | ...[...] |
|
||||
| UnsafeReflection.java:22:33:22:70 | getParameter(...) : String | UnsafeReflection.java:25:76:25:89 | parameterValue |
|
||||
| UnsafeReflection.java:25:29:25:59 | getDeclaredConstructors(...) : Constructor[] | UnsafeReflection.java:25:29:25:62 | ...[...] |
|
||||
| UnsafeReflection.java:33:28:33:60 | getParameter(...) : String | UnsafeReflection.java:39:13:39:38 | getDeclaredMethods(...) : Method[] |
|
||||
| UnsafeReflection.java:33:28:33:60 | getParameter(...) : String | UnsafeReflection.java:39:13:39:41 | ...[...] |
|
||||
| UnsafeReflection.java:33:28:33:60 | getParameter(...) : String | UnsafeReflection.java:39:50:39:55 | object |
|
||||
| UnsafeReflection.java:34:33:34:70 | getParameter(...) : String | UnsafeReflection.java:39:58:39:71 | parameterValue |
|
||||
| UnsafeReflection.java:39:13:39:38 | getDeclaredMethods(...) : Method[] | UnsafeReflection.java:39:13:39:41 | ...[...] |
|
||||
| UnsafeReflection.java:46:24:46:82 | beanIdOrClassName : String | UnsafeReflection.java:53:30:53:46 | beanIdOrClassName : String |
|
||||
| UnsafeReflection.java:46:132:46:168 | body : Map | UnsafeReflection.java:49:37:49:40 | body : Map |
|
||||
| UnsafeReflection.java:49:23:49:59 | (...)... : Object | UnsafeReflection.java:53:67:53:73 | rawData : Object |
|
||||
@@ -24,12 +20,10 @@ edges
|
||||
nodes
|
||||
| UnsafeReflection.java:21:28:21:60 | getParameter(...) : String | semmle.label | getParameter(...) : String |
|
||||
| UnsafeReflection.java:22:33:22:70 | getParameter(...) : String | semmle.label | getParameter(...) : String |
|
||||
| UnsafeReflection.java:25:29:25:59 | getDeclaredConstructors(...) : Constructor[] | semmle.label | getDeclaredConstructors(...) : Constructor[] |
|
||||
| UnsafeReflection.java:25:29:25:62 | ...[...] | semmle.label | ...[...] |
|
||||
| UnsafeReflection.java:25:76:25:89 | parameterValue | semmle.label | parameterValue |
|
||||
| UnsafeReflection.java:33:28:33:60 | getParameter(...) : String | semmle.label | getParameter(...) : String |
|
||||
| UnsafeReflection.java:34:33:34:70 | getParameter(...) : String | semmle.label | getParameter(...) : String |
|
||||
| UnsafeReflection.java:39:13:39:38 | getDeclaredMethods(...) : Method[] | semmle.label | getDeclaredMethods(...) : Method[] |
|
||||
| UnsafeReflection.java:39:13:39:41 | ...[...] | semmle.label | ...[...] |
|
||||
| UnsafeReflection.java:39:50:39:55 | object | semmle.label | object |
|
||||
| UnsafeReflection.java:39:58:39:71 | parameterValue | semmle.label | parameterValue |
|
||||
|
||||
@@ -3,10 +3,10 @@ import semmle.code.java.dataflow.internal.DataFlowImplCommon
|
||||
import semmle.code.java.dataflow.internal.DataFlowImplSpecific::Public
|
||||
import semmle.code.java.dataflow.internal.DataFlowImplSpecific::Private
|
||||
|
||||
from Node n1, Content f, Node n2
|
||||
from Node n1, ContentSet f, Node n2
|
||||
where
|
||||
(
|
||||
read(n1, f, n2) or
|
||||
readSet(n1, f, n2) or
|
||||
getterStep(n1, f, n2)
|
||||
) and
|
||||
n1.getEnclosingCallable().fromSource()
|
||||
|
||||
@@ -9,7 +9,7 @@ class SliceValueFlowConf extends DefaultValueFlowConf {
|
||||
}
|
||||
|
||||
class SliceTaintFlowConf extends DefaultTaintFlowConf {
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::Content c) {
|
||||
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
|
||||
super.allowImplicitRead(node, c)
|
||||
or
|
||||
isSink(node) and
|
||||
|
||||
@@ -1,3 +1,8 @@
|
||||
| stmts/A.java:18:5:18:12 | yield ... | stmts/A.java:16:10:16:18 | switch (...) |
|
||||
| stmts/A.java:22:6:22:13 | yield ... | stmts/A.java:20:14:20:22 | switch (...) |
|
||||
| stmts/A.java:25:6:25:13 | yield ... | stmts/A.java:20:14:20:22 | switch (...) |
|
||||
| stmts/A.java:34:7:34:14 | yield ... | stmts/A.java:16:10:16:18 | switch (...) |
|
||||
| stmts/A.java:37:5:37:13 | yield ... | stmts/A.java:16:10:16:18 | switch (...) |
|
||||
| stmts/B.java:8:5:8:10 | break | stmts/B.java:6:3:6:26 | for (...;...;...) |
|
||||
| stmts/B.java:10:5:10:13 | continue | stmts/B.java:6:3:6:26 | for (...;...;...) |
|
||||
| stmts/B.java:13:6:13:11 | break | stmts/B.java:11:4:11:17 | while (...) |
|
||||
|
||||
@@ -1,6 +1,14 @@
|
||||
| stmts/A.java:6:3:6:10 | case ... |
|
||||
| stmts/A.java:8:3:8:10 | case ... |
|
||||
| stmts/A.java:10:3:10:10 | default |
|
||||
| stmts/A.java:17:4:17:12 | case ... |
|
||||
| stmts/A.java:20:4:20:12 | case ... |
|
||||
| stmts/A.java:21:5:21:13 | case ... |
|
||||
| stmts/A.java:24:5:24:14 | default |
|
||||
| stmts/A.java:28:4:28:12 | case ... |
|
||||
| stmts/A.java:29:4:29:13 | default |
|
||||
| stmts/A.java:32:6:32:14 | case ... |
|
||||
| stmts/A.java:33:6:33:14 | case ... |
|
||||
| stmts/B.java:21:5:21:12 | case ... |
|
||||
| stmts/B.java:23:5:23:12 | case ... |
|
||||
| stmts/B.java:25:5:25:12 | case ... |
|
||||
|
||||
1
java/ql/test/library-tests/stmts/options
Normal file
1
java/ql/test/library-tests/stmts/options
Normal file
@@ -0,0 +1 @@
|
||||
//semmle-extractor-options: --javac-args -source 14 -target 14
|
||||
@@ -11,4 +11,31 @@ public class A {
|
||||
return x;
|
||||
}
|
||||
}
|
||||
|
||||
public int nestedSwitchExpr(int x, int y) {
|
||||
return switch(x) {
|
||||
case 1 -> {
|
||||
yield 1;
|
||||
}
|
||||
case 2 -> switch(y) {
|
||||
case 0 -> {
|
||||
yield 0;
|
||||
}
|
||||
default -> {
|
||||
yield 1;
|
||||
}
|
||||
};
|
||||
case 3 -> 3;
|
||||
default -> {
|
||||
// SwitchStmt inside SwitchExpr
|
||||
switch (y) {
|
||||
case 1 -> System.out.println("1");
|
||||
case 2 -> {
|
||||
yield 2;
|
||||
}
|
||||
}
|
||||
yield -1;
|
||||
}
|
||||
};
|
||||
}
|
||||
}
|
||||
|
||||
@@ -89,9 +89,16 @@ public class CleartextStorageSharedPrefsTest extends Activity {
|
||||
.create(context, "secret_shared_prefs", masterKey,
|
||||
EncryptedSharedPreferences.PrefKeyEncryptionScheme.AES256_SIV,
|
||||
EncryptedSharedPreferences.PrefValueEncryptionScheme.AES256_GCM)
|
||||
.edit().putString("name", name) /// Safe
|
||||
.edit().putString("name", name) // Safe
|
||||
.putString("password", password); // Safe
|
||||
|
||||
editor.commit();
|
||||
}
|
||||
|
||||
public void testSetSharedPrefs7(Context context, String name, String password) {
|
||||
SharedPreferences sharedPrefs =
|
||||
context.getSharedPreferences("user_prefs", Context.MODE_PRIVATE);
|
||||
sharedPrefs.edit().putString("name", name).apply(); // Safe
|
||||
sharedPrefs.edit().putString("password", password).apply(); // $hasCleartextStorageSharedPrefs
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user