CPP: Improvements to Buffer.qll #270
Conversation
| forex(Expr def | | ||
| DataFlow::localFlowStep(DataFlow::exprNode(def), DataFlow::exprNode(bufferExpr)) | | ||
| result = getBufferSize(def, _) | ||
| ) and |
There was a problem hiding this comment.
This use or forex reminds me of the code that was removed in https://git.semmle.com/Semmle/code/commit/90a05cd6fafcd2e179c49f17a5b67bb01de2b57d because it had bad performance on certain pathological snapshots. I'm guessing the same transformation could be needed here.
As I understand it, the performance is quadratic in the number of def: for each def the implicit exists will find one or more result, and then each of those result will be checked against every other def in the implicit forall.
There was a problem hiding this comment.
So, as I understand it the issue is that forex(x | y) is not a primitive language feature but syntax sugar for forall(x | y) and exists(x | y). Which is usually fine, but if y contains a variable from outside the forex it's possible to produce a cartesian product. I haven't been able to characterize exactly when this happens.
There was a problem hiding this comment.
Nevertheless I've made the change, and it has no noticeable effect on performance (as we'd expect outside of extreme cases).
There was a problem hiding this comment.
One way to see the the problem is that if you wrote forall instead of forex here, the compiler would rightfully complain that result was not bound: for a bufferExpr with no associated def, any value of result would satisfy the forall. This would make result take infinitely many values in the sense that the type checker considers int to be infinite.
In other words, the forall can only check whether a candidate for result has the desired properties -- it cannot generate a candidate. When it's joined with an exists, the candidates can be generated by exists, and then each candidate is checked by the forall. If there are n different candidates, and each candidate needs to be compared for equality with the n other candidates, then the run time is n^2.
As I'm writing this out, I can see that it would take some quite contrived code to trigger the quadratic behaviour.
jbj
added
the
depends on internal PR
cpp/ql/src/definitions.ql
Outdated
| forall(MyInt y | rel(x, y)) | ||
| and | ||
| exists(MyInt y | rel(x, y)) | ||
| select x |
There was a problem hiding this comment.
You accidentally committed your test code here.
There was a problem hiding this comment.
Good spot, thanks, fixed!
jbj
left a comment
jbj
left a comment
There was a problem hiding this comment.
LGTM. The internal PR passed its tests, so this should be safe to merge.
…lace-operators Extract simple in-place operators
PS: Better usability when working with nested classes
2 participants
Improve data flow handling in Buffer.qll. This should resolve the false positives that came to light after support for negative indices was added to OverflowBuffer.ql (#194).