Skip to content

Ruby: Add post-update nodes for compound arguments #10444

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Sep 22, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,12 @@ module Consistency {

/** Holds if `n` should be excluded from the consistency test `reverseRead`. */
predicate reverseReadExclude(Node n) { none() }

/** Holds if `n` should be excluded from the consistency test `postHasUniquePre`. */
predicate postHasUniquePreExclude(PostUpdateNode n) { none() }

/** Holds if `n` should be excluded from the consistency test `uniquePostUpdate`. */
predicate uniquePostUpdateExclude(Node n) { none() }
}

private class RelevantNode extends Node {
Expand Down Expand Up @@ -166,6 +172,7 @@ module Consistency {
}

query predicate postHasUniquePre(PostUpdateNode n, string msg) {
not any(ConsistencyConfiguration conf).postHasUniquePreExclude(n) and
exists(int c |
c = count(n.getPreUpdateNode()) and
c != 1 and
Expand All @@ -174,6 +181,7 @@ module Consistency {
}

query predicate uniquePostUpdate(Node n, string msg) {
not any(ConsistencyConfiguration conf).uniquePostUpdateExclude(n) and
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
msg = "Node has multiple PostUpdateNodes."
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,12 @@ module Consistency {

/** Holds if `n` should be excluded from the consistency test `reverseRead`. */
predicate reverseReadExclude(Node n) { none() }

/** Holds if `n` should be excluded from the consistency test `postHasUniquePre`. */
predicate postHasUniquePreExclude(PostUpdateNode n) { none() }

/** Holds if `n` should be excluded from the consistency test `uniquePostUpdate`. */
predicate uniquePostUpdateExclude(Node n) { none() }
}

private class RelevantNode extends Node {
Expand Down Expand Up @@ -166,6 +172,7 @@ module Consistency {
}

query predicate postHasUniquePre(PostUpdateNode n, string msg) {
not any(ConsistencyConfiguration conf).postHasUniquePreExclude(n) and
exists(int c |
c = count(n.getPreUpdateNode()) and
c != 1 and
Expand All @@ -174,6 +181,7 @@ module Consistency {
}

query predicate uniquePostUpdate(Node n, string msg) {
not any(ConsistencyConfiguration conf).uniquePostUpdateExclude(n) and
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
msg = "Node has multiple PostUpdateNodes."
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,12 @@ module Consistency {

/** Holds if `n` should be excluded from the consistency test `reverseRead`. */
predicate reverseReadExclude(Node n) { none() }

/** Holds if `n` should be excluded from the consistency test `postHasUniquePre`. */
predicate postHasUniquePreExclude(PostUpdateNode n) { none() }

/** Holds if `n` should be excluded from the consistency test `uniquePostUpdate`. */
predicate uniquePostUpdateExclude(Node n) { none() }
}

private class RelevantNode extends Node {
Expand Down Expand Up @@ -166,6 +172,7 @@ module Consistency {
}

query predicate postHasUniquePre(PostUpdateNode n, string msg) {
not any(ConsistencyConfiguration conf).postHasUniquePreExclude(n) and
exists(int c |
c = count(n.getPreUpdateNode()) and
c != 1 and
Expand All @@ -174,6 +181,7 @@ module Consistency {
}

query predicate uniquePostUpdate(Node n, string msg) {
not any(ConsistencyConfiguration conf).uniquePostUpdateExclude(n) and
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
msg = "Node has multiple PostUpdateNodes."
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,12 @@ module Consistency {

/** Holds if `n` should be excluded from the consistency test `reverseRead`. */
predicate reverseReadExclude(Node n) { none() }

/** Holds if `n` should be excluded from the consistency test `postHasUniquePre`. */
predicate postHasUniquePreExclude(PostUpdateNode n) { none() }

/** Holds if `n` should be excluded from the consistency test `uniquePostUpdate`. */
predicate uniquePostUpdateExclude(Node n) { none() }
}

private class RelevantNode extends Node {
Expand Down Expand Up @@ -166,6 +172,7 @@ module Consistency {
}

query predicate postHasUniquePre(PostUpdateNode n, string msg) {
not any(ConsistencyConfiguration conf).postHasUniquePreExclude(n) and
exists(int c |
c = count(n.getPreUpdateNode()) and
c != 1 and
Expand All @@ -174,6 +181,7 @@ module Consistency {
}

query predicate uniquePostUpdate(Node n, string msg) {
not any(ConsistencyConfiguration conf).uniquePostUpdateExclude(n) and
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
msg = "Node has multiple PostUpdateNodes."
}
Expand Down
5 changes: 4 additions & 1 deletion docs/ql-libraries/dataflow/dataflow.md
Original file line number Diff line number Diff line change
Expand Up @@ -294,7 +294,10 @@ through an additional step targeting a `PostUpdateNode`).

It is recommended to introduce `PostUpdateNode`s for all `ArgumentNode`s (this
can be skipped for immutable arguments), and all field qualifiers for both
reads and stores.
reads and stores. Note also that in the case of compund arguments, such as
`b ? x : y`, it is recommented to have post-update nodes for `x` and `y` (and
not the compound argument itself), and let `[post update] x` have both `x`
and `b ? x : y` as pre-update nodes (and similarly for `[post update] y`).

Remember to define local flow for `PostUpdateNode`s as well in
`simpleLocalFlowStep`. In general out-going local flow from `PostUpdateNode`s
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,12 @@ module Consistency {

/** Holds if `n` should be excluded from the consistency test `reverseRead`. */
predicate reverseReadExclude(Node n) { none() }

/** Holds if `n` should be excluded from the consistency test `postHasUniquePre`. */
predicate postHasUniquePreExclude(PostUpdateNode n) { none() }

/** Holds if `n` should be excluded from the consistency test `uniquePostUpdate`. */
predicate uniquePostUpdateExclude(Node n) { none() }
}

private class RelevantNode extends Node {
Expand Down Expand Up @@ -166,6 +172,7 @@ module Consistency {
}

query predicate postHasUniquePre(PostUpdateNode n, string msg) {
not any(ConsistencyConfiguration conf).postHasUniquePreExclude(n) and
exists(int c |
c = count(n.getPreUpdateNode()) and
c != 1 and
Expand All @@ -174,6 +181,7 @@ module Consistency {
}

query predicate uniquePostUpdate(Node n, string msg) {
not any(ConsistencyConfiguration conf).uniquePostUpdateExclude(n) and
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
msg = "Node has multiple PostUpdateNodes."
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,12 @@ module Consistency {

/** Holds if `n` should be excluded from the consistency test `reverseRead`. */
predicate reverseReadExclude(Node n) { none() }

/** Holds if `n` should be excluded from the consistency test `postHasUniquePre`. */
predicate postHasUniquePreExclude(PostUpdateNode n) { none() }

/** Holds if `n` should be excluded from the consistency test `uniquePostUpdate`. */
predicate uniquePostUpdateExclude(Node n) { none() }
}

private class RelevantNode extends Node {
Expand Down Expand Up @@ -166,6 +172,7 @@ module Consistency {
}

query predicate postHasUniquePre(PostUpdateNode n, string msg) {
not any(ConsistencyConfiguration conf).postHasUniquePreExclude(n) and
exists(int c |
c = count(n.getPreUpdateNode()) and
c != 1 and
Expand All @@ -174,6 +181,7 @@ module Consistency {
}

query predicate uniquePostUpdate(Node n, string msg) {
not any(ConsistencyConfiguration conf).uniquePostUpdateExclude(n) and
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
msg = "Node has multiple PostUpdateNodes."
}
Expand Down
19 changes: 18 additions & 1 deletion ruby/ql/consistency-queries/DataFlowConsistency.ql
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
import codeql.ruby.AST
import codeql.ruby.CFG
import codeql.ruby.DataFlow::DataFlow
import codeql.ruby.dataflow.internal.DataFlowPrivate
import codeql.ruby.dataflow.internal.DataFlowImplConsistency::Consistency
Expand All @@ -13,6 +14,22 @@ private class MyConsistencyConfiguration extends ConsistencyConfiguration {
or
n instanceof SynthHashSplatArgumentNode
or
not isNonConstantExpr(n.asExpr())
not isNonConstantExpr(getAPostUpdateNodeForArg(n.asExpr()))
}

override predicate postHasUniquePreExclude(PostUpdateNode n) {
exists(CfgNodes::ExprCfgNode e, CfgNodes::ExprCfgNode arg |
e = getAPostUpdateNodeForArg(arg) and
e != arg and
n = TExprPostUpdateNode(e)
)
}

override predicate uniquePostUpdateExclude(Node n) {
exists(CfgNodes::ExprCfgNode e, CfgNodes::ExprCfgNode arg |
e = getAPostUpdateNodeForArg(arg) and
e != arg and
n.asExpr() = arg
)
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,12 @@ module Consistency {

/** Holds if `n` should be excluded from the consistency test `reverseRead`. */
predicate reverseReadExclude(Node n) { none() }

/** Holds if `n` should be excluded from the consistency test `postHasUniquePre`. */
predicate postHasUniquePreExclude(PostUpdateNode n) { none() }

/** Holds if `n` should be excluded from the consistency test `uniquePostUpdate`. */
predicate uniquePostUpdateExclude(Node n) { none() }
}

private class RelevantNode extends Node {
Expand Down Expand Up @@ -166,6 +172,7 @@ module Consistency {
}

query predicate postHasUniquePre(PostUpdateNode n, string msg) {
not any(ConsistencyConfiguration conf).postHasUniquePreExclude(n) and
exists(int c |
c = count(n.getPreUpdateNode()) and
c != 1 and
Expand All @@ -174,6 +181,7 @@ module Consistency {
}

query predicate uniquePostUpdate(Node n, string msg) {
not any(ConsistencyConfiguration conf).uniquePostUpdateExclude(n) and
1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
msg = "Node has multiple PostUpdateNodes."
}
Expand Down
56 changes: 41 additions & 15 deletions ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPrivate.qll
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,32 @@ private class ExprNodeImpl extends ExprNode, NodeImpl {
override string toStringImpl() { result = this.getExprNode().toString() }
}

/**
* Gets a node that may execute last in `n`, and which, when it executes last,
* will be the value of `n`.
*/
private CfgNodes::ExprCfgNode getALastEvalNode(CfgNodes::ExprCfgNode n) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When reading the comment explaining this predicate , I had expected it to be recursive. I see you take the transitive closure later.

result = n.(CfgNodes::ExprNodes::StmtSequenceCfgNode).getLastStmt()
or
result = n.(CfgNodes::ExprNodes::ConditionalExprCfgNode).getBranch(_)
or
exists(CfgNodes::AstCfgNode branch |
branch = n.(CfgNodes::ExprNodes::CaseExprCfgNode).getBranch(_)
|
result = branch.(CfgNodes::ExprNodes::InClauseCfgNode).getBody()
or
result = branch.(CfgNodes::ExprNodes::WhenClauseCfgNode).getBody()
or
result = branch
)
}

/** Gets a node for which to construct a post-update node for argument `arg`. */
CfgNodes::ExprCfgNode getAPostUpdateNodeForArg(Argument arg) {
result = getALastEvalNode*(arg) and
not exists(getALastEvalNode(result))
}

/** Provides predicates related to local data flow. */
module LocalFlow {
private import codeql.ruby.dataflow.internal.SsaImpl
Expand Down Expand Up @@ -135,19 +161,7 @@ module LocalFlow {
or
nodeFrom.asExpr() = nodeTo.asExpr().(CfgNodes::ExprNodes::BlockArgumentCfgNode).getValue()
or
nodeFrom.asExpr() = nodeTo.asExpr().(CfgNodes::ExprNodes::StmtSequenceCfgNode).getLastStmt()
or
nodeFrom.asExpr() = nodeTo.asExpr().(CfgNodes::ExprNodes::ConditionalExprCfgNode).getBranch(_)
or
exists(CfgNodes::AstCfgNode branch |
branch = nodeTo.asExpr().(CfgNodes::ExprNodes::CaseExprCfgNode).getBranch(_)
|
nodeFrom.asExpr() = branch.(CfgNodes::ExprNodes::InClauseCfgNode).getBody()
or
nodeFrom.asExpr() = branch.(CfgNodes::ExprNodes::WhenClauseCfgNode).getBody()
or
nodeFrom.asExpr() = branch
)
nodeFrom.asExpr() = getALastEvalNode(nodeTo.asExpr())
or
exists(CfgNodes::ExprCfgNode exprTo, ReturningStatementNode n |
nodeFrom = n and
Expand Down Expand Up @@ -241,7 +255,8 @@ private module Cached {
// filter out nodes that clearly don't need post-update nodes
isNonConstantExpr(n) and
(
n instanceof Argument or
n = getAPostUpdateNodeForArg(_)
or
n = any(CfgNodes::ExprNodes::InstanceVariableAccessCfgNode v).getReceiver()
)
} or
Expand Down Expand Up @@ -1127,7 +1142,18 @@ private module PostUpdateNodes {

ExprPostUpdateNode() { this = TExprPostUpdateNode(e) }

override ExprNode getPreUpdateNode() { e = result.getExprNode() }
override ExprNode getPreUpdateNode() {
// For compund arguments, such as `m(if b then x else y)`, we want the leaf nodes
// `[post] x` and `[post] y` to have two pre-update nodes: (1) the compund argument,
// `if b then x else y`; and the (2) the underlying expressions; `x` and `y`,
// respectively.
//
// This ensures that we get flow out of the call into both leafs (1), while still
// maintaining the invariant that the underlying expression is a pre-update node (2).
e = getAPostUpdateNodeForArg(result.getExprNode())
or
e = result.getExprNode()
}

override CfgScope getCfgScope() { result = e.getExpr().getCfgScope() }

Expand Down
Loading