-
Notifications
You must be signed in to change notification settings - Fork 2k
C++: Support reasoning about whether a phi node overwrites the entire buffer #21836
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
Changes from 7 commits
8e25240
b753e7d
e77d85f
6d5d57a
fc80a24
8585bb6
f40d42c
07b8d7e
25c4d9d
d93de54
c6ce13a
f77d426
f5113b1
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -136,7 +136,9 @@ private module SourceVariables { | |
| NormalSourceVariable() { this = TNormalSourceVariable(base, ind) } | ||
|
|
||
| final override string toString() { | ||
| result = repeatStars(this.getIndirection()) + base.toString() | ||
| if ind = 0 | ||
| then result = "&" + base.toString() | ||
| else result = repeatStars(this.getIndirection() - 1) + base.toString() | ||
| } | ||
| } | ||
|
|
||
|
|
@@ -157,7 +159,9 @@ private module SourceVariables { | |
| } | ||
|
|
||
| final override string toString() { | ||
| result = repeatStars(this.getIndirection()) + base.toString() + " [before crement]" | ||
| if ind = 0 | ||
| then result = "&" + base.toString() + " [before crement]" | ||
| else result = repeatStars(this.getIndirection() - 1) + base.toString() + " [before crement]" | ||
| } | ||
|
|
||
| /** | ||
|
|
@@ -1353,6 +1357,53 @@ class PhiNode extends Definition instanceof SsaImpl::PhiNode { | |
| final predicate hasInputFromBlock(Definition input, IRBlock bb) { | ||
| phiHasInputFromBlock(this, input, bb) | ||
| } | ||
|
|
||
| override int getIndirection() { result = this.getSourceVariable().getIndirection() } | ||
|
|
||
| override predicate isCertain() { | ||
| // If this phi node is part of a phi cycle of phi nodes the least | ||
| // fixed-point semantics of datalog means we don't get the right answer. | ||
| // So we perform an SCC reduction to simulate greated fixed-point semantics. | ||
|
MathiasVP marked this conversation as resolved.
Outdated
|
||
| getCycle(this).isCertain() | ||
| or | ||
| // If there is no cycle we get the right semantics through traditional | ||
| // recursion. | ||
| not exists(getCycle(this)) and | ||
| forex(Definition inp | inp = this.getAnInput() | inp.isCertain()) | ||
| } | ||
|
|
||
| final override Declaration getFunction() { | ||
| result = SsaImpl::PhiNode.super.getBasicBlock().getEnclosingFunction() | ||
| } | ||
| } | ||
|
|
||
| private PhiNode getAnInput(PhiNode phi) { result = phi.getAnInput() } | ||
|
|
||
| private predicate definitionCycle(PhiNode phi) { getAnInput+(phi) = phi } | ||
|
|
||
| private predicate hasAnInput(PhiNode phi1, PhiNode phi2) { | ||
| definitionCycle(phi1) and | ||
| definitionCycle(phi2) and | ||
| getAnInput(phi1) = phi2 | ||
| } | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is wrong. You're attempting to define SCC-internal edges here, but if two SCCs are adjacent then this will accidentally merge them. You need this instead:
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Hm, yes I can see how these two definitions aren't equivalent and that yours captures what I intended to capture. Now I'm just trying to construct an example where the two definitions would cause a change in a test 🤔 If you have one at hand I'd love to know. Otherwise I'll spend some time trying to construct one, and if all else fail I'll just replace the code with your suggestion as it's obviously the right one
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Something like this perhaps: Here
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. |
||
|
|
||
| private module PhiCycleEquivalence = QlBuiltins::EquivalenceRelation<PhiNode, hasAnInput/2>; | ||
|
|
||
| private PhiCycle getCycle(PhiNode phi) { result.getAPhiNode() = phi } | ||
|
|
||
| private class PhiCycle extends PhiCycleEquivalence::EquivalenceClass { | ||
| PhiNode getAPhiNode() { PhiCycleEquivalence::getEquivalenceClass(result) = this } | ||
|
|
||
| predicate hasPhiNode(PhiNode phi) { this.getAPhiNode() = phi } | ||
|
|
||
| string toString() { result = strictconcat(this.getAPhiNode().toString(), ", ") } | ||
|
|
||
| predicate isCertain() { | ||
| // A phi cycle is certain if all of the inputs into the phi cycle is certain. | ||
|
MathiasVP marked this conversation as resolved.
|
||
| forex(PhiNode phi | phi = this.getAPhiNode() | | ||
| forall(PhiNode inp | phi.getAnInput() = inp and not this.hasPhiNode(inp) | inp.isCertain()) | ||
| ) | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Factor out the range to make the recursion simpler. Add a member predicate and use this to define the recursive forall: Note also that I've changed the type of
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Fixed in c6ce13a |
||
| } | ||
| } | ||
|
|
||
| /** An static single assignment (SSA) definition. */ | ||
|
|
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,64 @@ | ||
| void use(...); | ||
|
|
||
| void test1() { | ||
| int x = 0; // $ certain="SSA def(&x)" certain="SSA def(x)" | ||
| use(x); | ||
|
|
||
| x = 1; // $ certain="SSA def(x)" | ||
| use(x); | ||
|
|
||
| int* p = &x; // $ certain="SSA def(&p)" certain="SSA def(p)" certain="SSA def(*p)" | ||
| use(p); | ||
|
|
||
| *p = 2; // $ certain="SSA def(*p)" | ||
| use(p); | ||
|
|
||
| p = nullptr; // $ certain="SSA def(p)" certain="SSA def(*p)" | ||
| use(p); | ||
|
|
||
| *p = 2; // $ uncertain="SSA def(*p)" | ||
| use(p); | ||
| } | ||
|
|
||
| void test2(bool b) { // $ certain="SSA def(&b)" certain="SSA def(b)" | ||
| { | ||
| int x; // $ certain="SSA def(&x)" | ||
| if(b) { | ||
| x = 0; // $ certain="SSA def(x)" | ||
| } else { | ||
| x = 1; // $ certain="SSA def(x)" | ||
| } | ||
| use(x); // $ certain="SSA phi(x)" | ||
| } | ||
|
|
||
| { | ||
| int x; // $ certain="SSA def(&x)" certain="SSA def(x)" | ||
| if(b) { | ||
| x = 0; // $ certain="SSA def(x)" | ||
| } else { | ||
|
|
||
| } | ||
| use(x); // $ certain="SSA phi(x)" | ||
| } | ||
|
|
||
| { | ||
| int x; // $ certain="SSA def(&x)" certain="SSA def(x)" | ||
| int* p = &x; // $ certain="SSA def(&p)" certain="SSA def(p)" certain="SSA def(*p)" | ||
| if(b) { | ||
| *p = 0; // $ certain="SSA def(*p)" | ||
| } else { | ||
| *(p + 1) = 1; // $ uncertain="SSA def(*p)" | ||
| } | ||
| use(p); // $ uncertain="SSA phi(*p)" | ||
| } | ||
|
|
||
| } | ||
|
|
||
| void test3(bool b) { // $ certain="SSA def(&b)" certain="SSA def(b)" | ||
| for(int i = 0; i < 10;) { // $ certain="SSA def(&i)" certain="SSA def(i)" certain="SSA phi(i)" | ||
| if(b) { | ||
| ++i; // $ certain="SSA def(i)" | ||
| } | ||
| use(i); // $ certain="SSA phi(i)" | ||
| } | ||
| } |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| import cpp | ||
| import utils.test.InlineExpectationsTest | ||
| import semmle.code.cpp.dataflow.new.DataFlow::DataFlow | ||
|
|
||
| bindingset[s] | ||
| string quote(string s) { if s.matches("% %") then result = "\"" + s + "\"" else result = s } | ||
|
|
||
| module AsDefinitionTest implements TestSig { | ||
| string getARelevantTag() { result = ["certain", "uncertain"] } | ||
|
|
||
| predicate hasActualResult(Location location, string element, string tag, string value) { | ||
| exists(Ssa::Definition d | | ||
| location = d.getLocation() and | ||
| element = d.toString() and | ||
| value = quote(d.toString()) | ||
| | | ||
| if d.isCertain() then tag = "certain" else tag = "uncertain" | ||
| ) | ||
| } | ||
| } | ||
|
|
||
| import MakeTest<AsDefinitionTest> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Mixing direct field access
indwiththis.getIndirection()becomes very confusing to read. Same issue below.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed in d93de54