Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Go: Fix bad join order using late inlined predicate #17437

Closed
wants to merge 4 commits into from
Closed

Go: Fix bad join order using late inlined predicate #17437

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
b99ba9b
Fix bad join order using late inlined predicate
owen-mc Sep 11, 2024
9e6477a
Remove erroneous pragma
owen-mc Sep 11, 2024
8912350
Reduce bindingset for inline_late predicate
owen-mc Sep 11, 2024
98aa1a5
Fix comment to refer to moved comment correctly
owen-mc Sep 11, 2024
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
30 changes: 22 additions & 8 deletions go/ql/lib/semmle/go/dataflow/internal/DataFlowUtil.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -376,13 +376,8 @@ module BarrierGuard<guardChecksSig/3 guardChecks> {
// Case: a function like "return someBarrierGuard(arg)"
// or "return !someBarrierGuard(arg) && otherCond(...)"
exists(boolean outcome |
ret = getUniqueOutputNode(fd, outp) and
smowton marked this conversation as resolved.
Show resolved Hide resolved
guardChecks(g, arg.asExpr(), outcome) and
// This predicate's contract is (p holds of ret ==> arg is checked),
// (and we have (this has outcome ==> arg is checked))
// but p.checkOn(ret, outcome, this) gives us (ret has outcome ==> p holds of this),
// so we need to swap outcome and (specifically boolean) p:
DataFlow::booleanProperty(outcome).checkOn(ret, p.asBoolean(), g)
guardingFunctionHelper(g, outp, p, fd, ret, outcome)
smowton marked this conversation as resolved.
Show resolved Hide resolved
)
or
// Case: a function like "return guardProxy(arg)"
Expand All @@ -396,8 +391,9 @@ module BarrierGuard<guardChecksSig/3 guardChecks> {
c = f2.getACall() and
arg = inp2.getNode(c) and
(
// See comment above ("This method's contract...") for rationale re: the inversion of
// `p` and `outpProp` here:
// See comment in `guardingFunctionHelper` ("This predicate's
// contract...") for the rationale behind the inversion of `p` and
// `outpProp` here:
outpProp.checkOn(ret, p.asBoolean(), outp2.getNode(c))
or
// The particular case where p is non-boolean (i.e., nil or non-nil), and we directly return `c`:
Expand All @@ -409,6 +405,24 @@ module BarrierGuard<guardChecksSig/3 guardChecks> {
}
}

/**
* Holds when `ret` is the unique output `outp` node of `fd`, `g` is a
* subexpression of `ret`, and when `ret` has value `outcome` then property `p`
* holds of `g`.
*/
bindingset[g]
pragma[inline_late]
private predicate guardingFunctionHelper(
Node g, FunctionOutput outp, DataFlow::Property p, FuncDecl fd, Node ret, boolean outcome
) {
ret = getUniqueOutputNode(fd, outp) and
// This predicate's contract is (p holds of ret ==> arg is checked),
// (and we have (this has outcome ==> arg is checked))
// but p.checkOn(ret, outcome, this) gives us (ret has outcome ==> p holds of this),
// so we need to swap outcome and (specifically boolean) p:
DataFlow::booleanProperty(outcome).checkOn(ret, p.asBoolean(), g)
}

DataFlow::Node getUniqueOutputNode(FuncDecl fd, FunctionOutput outp) {
result = unique(DataFlow::Node n | n = outp.getEntryNode(fd) | n)
}
Expand Down
Loading