Details
- Reviewers
NoQ dcoughlin george.karpenkov - Commits
- rGb03ed5e41490: [Analyzer] Iterator Checker - Part 2: Increment, decrement operators and ahead…
rC335835: [Analyzer] Iterator Checker - Part 2: Increment, decrement operators and ahead…
rL335835: [Analyzer] Iterator Checker - Part 2: Increment, decrement operators and ahead…
Diff Detail
Event Timeline
lib/StaticAnalyzer/Checkers/IteratorChecker.cpp | ||
---|---|---|
357 | We cannot use else after return? | |
576 | oldOffset -> OldOffset? | |
941 | else after return? | |
945 | else after return too. | |
1195 | else after return? |
I'm sorry, i'd try to get back to this and unblock your progress as soon as possible.
One thing i notice is that you manipulate symbolic expressions manually, however many of the things that you need, eg stuff in your compose() method, seem to be already available in SValBuilder::evalBinOp(). I think you could simplify the code significantly if you rely on it.
One of the downsides of SValBuilder::evalBinOp() is that it sometimes simplifies some operations to UnknownVal when it knows that the rest of the analyzer would be unable to handle the results anyway. I'm not sure if your approach is more clever than the rest of the analyzer when it comes to handling such values. However, in any case, we're thinking about lifting these limitations in D28953, so it might be a good idea to wait for that to land as well.
lib/StaticAnalyzer/Checkers/IteratorChecker.cpp | ||
---|---|---|
15 | Just noticed: Constraint Manager can handle these SVals sometimes, suggesting such SVals. | |
66 | Just noticed: can we mark these as const, because there are no methods to modify them? I guess you intended to keep objects of this class immutable. |
I tried SValBuilder::evalBinOp() first but it did not help too much. It could decide only if I compared the same conjured symbols or different ones, but nothing more. It always gave me UnknownVal. Even if comparing ${conj_X} == ${conj_X} + n where n was a concrete integer. So I have to compare the symbol part and the concrete integer part separately. Waiting is not an option for us since we are a bit delayed with this checker. I have to bring them out of alpha until the end of the year. If Z3 constraint solver is accepted and will be the default constraint manager, then I can somewhat simplify my code. That patch is under review for long and I am not sure whether it will be the default ever.
In any case, it's not right to have two SValBuilders. Your code simplifies symbolic expressions of numeric types, SValBuilder does the same thing, there's no need to duplicate. It would be much better to move the functionality you need (and already have implemented) directly to SValBuilder.
I'm sure that simplification (($x + N) + M) ~> ($x + (M + N)) is already working in SValBuilder. I think it's totally worth it to add (($x + M) == ($x + N)) ~> (M == N) and (($x + M) - ($x + N)) ~> M - N into SValBuilder in case it's not already there, because the whole analyzer would immediately benefit from that, not just your checker.
Generally, i totally encourage you to modify the analyzer's core to fit your purposes, even if to reduce code duplication. It's not worth it to teach the core constraint manager how to work with user-defined types such as iterators, but it's definitely worth it to teach SValBuilder how to handle numeric-type symbols better.
I don't expect Z3 to be on by default soon, however i'm only pointing to the changes in the mainline SValBuilder in that patch. Z3 doesn't replace SValBuilder, it only replaces the constraint manager. However, SValBuilder needs to provide accurate SVals to Z3, which means that a lot of UnknownVals need to go away. We're discussing if they should go away completely even if Z3 isn't on.
While moving things out of alpha is pretty much the primary goal of any work we do, sacrificing quality defeats that purpose. We can only afford to enable things by default when we know they're ready. This checker is research-heavy and as such hard to plan. We need to understand the decisions and trade-offs that you made.
I'm sure that simplification (($x + N) + M) ~> ($x + (M + N)) is already working in SValBuilder.
No, it is unfortunately not working: I tried to increase ${conj_X} by 1, then again by 1, and I got symbolic expression (${conj_X}+1)+1).
For example,
$ cat test.c
void clang_analyzer_dump(int); int bar(); void foo() { int x = bar(); clang_analyzer_dump(x); ++x; clang_analyzer_dump(x); ++x; clang_analyzer_dump(x); }
$ ~/debug/bin/clang -cc1 -analyze -analyzer-checker=debug.ExprInspection test.c
test.c:7:3: warning: conj_$2{int} clang_analyzer_dump(x); ^~~~~~~~~~~~~~~~~~~~~~ test.c:9:3: warning: (conj_$2{int}) + 1 clang_analyzer_dump(x); ^~~~~~~~~~~~~~~~~~~~~~ test.c:11:3: warning: (conj_$2{int}) + 2 clang_analyzer_dump(x); ^~~~~~~~~~~~~~~~~~~~~~ 3 warnings generated.
So i'm sure we're already doing this everywhere.
SymbolManager::getSymIntExpr() replaced by SValBuilder::evalBinOp(), function compact() eliminated.
Now I can improve SValBuilder to compare {conj_X}+n to conj_X}+m, but I am not sure if it helps to simplify compare() much. How to handle cases where I have to compare {conj_X}+n to {conj_Y}+m, an we have a range [k..k] for {conj_X}-{conj_Y} in the constraint manager. I still need to decompose the two expressions, retrieve the single length range and adjust one of the sides of the comparison. I think I should not add such complicated code (i.e. retrieving single length range from the constrain manager) to SValBuilder.
SValBuilder simplifies the symbolic expressions to a certain "canonical" form - collapses ($x op N) op M to single-op expressions, reorders N op $x to $x op N, unpacks !$x into $x == 0, etc.), and ConstraintManager makes assumptions over such "canonical" symbolic expressions (but unable to handle non-canonical symbolic expressions).
I propose to canonicalize ($x + N) == ($y + M) to ($x - $y) == (M - N) in SValBuilder, and then ConstraintManager should be able to assume over it, as long as it has a range for ($x - $y). ConstraintManager would also need an update to support reversing the range when he only has a range for ($y - $x) but not for ($x - $y).
It seems that review on D35109 is stuck forever. So maybe we should forget about this simplification and return to the local solution I tried to use here originally. It is Part2, and we need to go through all parts as soon as possible. In the meanwhile I also tested the whole iterator solution on the whole Clang project and got rid of many false positives. So the checker itself is very promissing.
This patch would be in a good shape once we settle the rearrangement stuff. I had a look at all follow-up patches and identified other, hopefully smaller, places where i have overall design concerns; otherwise, the rest of the patches also look safe and straightforward.
I think this looks good. There's a problem with missing construction contexts, but i guess that's not the checker's fault, so let's add a FIXME and commit.
lib/StaticAnalyzer/Checkers/IteratorChecker.cpp | ||
---|---|---|
454–455 | This deserves a FIXME because that's definitely unreliable (i.e. if another checker subscribes to the operator call and adds a transition before you, you'll break because you'd have to ascend two nodes above, not one). The proper fix is to make the CFG provide a ConstructionContext for the CXXOperatorCallExpr, which would turn the corresponding CFGStmt element into a CFGCXXRecordTypedCall element, which will allow ExprEngine to foresee that the begin()/end() call constructs the object directly in the temporary region that CXXOperatorCallExpr takes as its implicit object argument. The proper fix is not hard, but there are still a lot of simpler and more common cases that we don't handle. | |
476–502 | I guess we'll have this sorted out in another patch. |
Just noticed: Constraint Manager can handle these SVals sometimes, suggesting such SVals.