Shared/Java: Add shared Guards library and switch Java to use it.#19573
Shared/Java: Add shared Guards library and switch Java to use it.#19573aschackmull merged 22 commits intogithub:mainfrom
Conversation
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| } | ||
|
|
||
| private module LogicInput_v2 implements GuardsImpl::LogicInputSig { | ||
| private import semmle.code.java.dataflow.SSA as SSA |
Check warning
Code scanning / CodeQL
Names only differing by case Warning
aschackmull
force-pushed
the
guardslib
branch
2 times, most recently
from
969365f to
4abca27
Compare
aschackmull
force-pushed
the
guardslib
branch
3 times, most recently
from
f4e0076 to
ed640ab
Compare
hvitved
left a comment
hvitved
left a comment
There was a problem hiding this comment.
Looks really good, great to finally have a shared guards library 🎉
| * controls the basic block `A`, in this case because the true branch dominates | ||
| * `A`, but more elaborate controls-relationships may also hold. | ||
| * For example, in | ||
| * ``` |
There was a problem hiding this comment.
nit: add java after bacticks
| predicate strictlyDominates(BasicBlock bb); | ||
| } | ||
|
|
||
| predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2); |
There was a problem hiding this comment.
Perhaps add QL doc describing how this differs from bb1.strictlyDominates(bb2)?
There was a problem hiding this comment.
Copied qldoc from the shared BasicBlocks lib.
| /** Gets the integer that this value represents, if any. */ | ||
| int asIntValue() { this = TValue(TValueInt(result), true) } | ||
|
|
||
| /** Gets the boolean that this value represents, if any. */ |
There was a problem hiding this comment.
Why? We write e.g. "integer" with lowercase. It's not really referring to a specific class or anything, it's just the English language meaning of "boolean", right? And the ql type that's being returned is also the lowercased boolean.
There was a problem hiding this comment.
I misread it as an adjective instead of a noun.
| v1.asBooleanValue() = true and | ||
| g2.(Case).getSwitchExpr() = switchExpr and | ||
| v2.asBooleanValue() = false and | ||
| g1 != g2 |
There was a problem hiding this comment.
Would it make sense to generalize to say: if g1, v1 represents matching case i, then g2, v2 represents non-matching any case j < i?
There was a problem hiding this comment.
On second thought, why is this implication even needed? I would have thought that dominance came for free from the CFG?
There was a problem hiding this comment.
The implication is needed if the CFG uses a jump-table interpretation (which Java mostly does), because then non-matching a case isn't represented in a specific edge. And it's only the default case that tends to be relevant, since knowing e.g. not "foo" when you already know "bar" in case "foo": .. case "bar": .. tends to be pointless.
| } | ||
|
|
||
| class SsaWriteDefinition extends SsaDefinition { | ||
| Expr getDefinition(); |
There was a problem hiding this comment.
Perhaps just move this into SsaDefinition and then get rid of SsaWriteDefinition?
There was a problem hiding this comment.
I'm trying to reflect the shared SSA api as much as possible here. Hence this choice.
| * starting from a given set of base cases. | ||
| */ | ||
| cached | ||
| module ImpliesTC<baseGuardValueSig/2 baseGuardValue> { |
| * control flow. It may also be a switch case, which as a guard is considered | ||
| * to evaluate to either true or false depending on whether the case matches. | ||
| */ | ||
| final class Guard extends PreGuard { |
There was a problem hiding this comment.
Should this class have a charpred to restrict it somehow?
There was a problem hiding this comment.
That's a good question and indeed a subtle change from the language-specific guards libraries. I think we can do it with guardControlsBranchEdge(this, _, _, _) if we change a bunch of Guard references to PreGuard. Again, this is something that would merit a dca rerun, so I'd like to investigate this option as a follow-up.
There was a problem hiding this comment.
OTOH, I'm not sure that it would actually achieve much, but I do agree that it would make more sense to have it.
| predicate parameterMatch(ParameterPosition ppos, ArgumentPosition apos); | ||
|
|
||
| /** A non-overridable method with a boolean return value. */ | ||
| class BooleanMethod { |
There was a problem hiding this comment.
Could all of this logic be generalized to methods that return constant values? E.g. like a Compare method that typically returns -1, 0, or 1?
There was a problem hiding this comment.
I want to generalise it to at least null/not-null and exception/no-exception. But something based around such integers might make sense as well. I'm already working on a follow-up branch that touches on this.
| * wrappers. This can be used to instantiate the `additionalImpliesStep` | ||
| * predicate. | ||
| */ | ||
| module CustomGuard<CustomGuardInputSig CustomGuardInput> { |
There was a problem hiding this comment.
I think something like WrapperGuard would be a better name.
As we discussed offline, it might be better to remove the nesting of parameterized modules; I'll let you decide (perhaps follow-up).
There was a problem hiding this comment.
Already looking at this in a follow-up branch.
|
|
||
| class BasicBlock = J::BasicBlock; | ||
|
|
||
| predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) { J::dominatingEdge(bb1, bb2) } |
There was a problem hiding this comment.
I'm surprised that dominatingEdge is exposed directly from the java.qll module.
There was a problem hiding this comment.
Yeah, something to maybe fix in the glorious future. Historically the contents of Dominance.qll have been exposed by default for Java.
| * with logical implications based on SSA. | ||
| */ | ||
| module Logic<LogicInputSig LogicInput> { | ||
| private import LogicInput |
Check warning
Code scanning / CodeQL
Redundant import Warning
2 participants
This adds a new shared Guards library, which provides complex implication logic between guards. The implementation is heavily inspired by the corresponding Java and C# versions.
The Java Guards library is then switched to use this new library, which results in a number of precision improvements for the nullness and useless comparison test queries.
There's currently a known FP related to correlated conditions in assert statements that I've documented as a qltest. I plan to fix that in a follow-up PR.
Review of the shared implementation (the single file
shared/controlflow/codeql/controlflow/Guards.qll) is likely best done by reading the final result, but the other changes can be reviewed commit-by-commit.