This is an archive of the discontinued LLVM Phabricator instance.

[Analyzer] Iterator Checker - Part 2: Increment, decrement operators and ahead-of-begin checks
ClosedPublic

Authored by baloghadamsoftware on Apr 28 2017, 6:21 AM.

Diff Detail

Repository
rL LLVM

Event Timeline

baloghadamsoftware retitled this revision from [Analyzer] Iterator Checker - Part2: Increment, decrement operators and ahead-of-begin checks to [Analyzer] Iterator Checker - Part 2: Increment, decrement operators and ahead-of-begin checks.May 4 2017, 5:30 AM
takuto.ikuta added inline comments.
lib/StaticAnalyzer/Checkers/IteratorChecker.cpp
357 ↗(On Diff #97086)
576 ↗(On Diff #97086)

oldOffset -> OldOffset?
same with L577, L580, L595, L596, L599 and so on.

941 ↗(On Diff #97086)

else after return?

945 ↗(On Diff #97086)

else after return too.

1195 ↗(On Diff #97086)

else after return?

Rebased to (committed) Part1 (rL304160) and updated according to comments.

Any progress in the review?

NoQ edited edge metadata.Jun 19 2017, 11:15 AM

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
51 ↗(On Diff #100848)

Just noticed: Constraint Manager can handle these SVals sometimes, suggesting such SVals.

125 ↗(On Diff #100848)

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.

Minor fixes according to the comments.

baloghadamsoftware marked 2 inline comments as done.Jun 22 2017, 6:53 AM
NoQ added a comment.Jun 22 2017, 8:12 AM

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.

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.

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.

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.

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.

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).

NoQ added a comment.Jun 23 2017, 2:09 AM

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).

Could you post the code you use?

NoQ added a comment.Jun 23 2017, 3:52 AM

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.

NoQ added a comment.Jun 24 2017, 11:37 PM

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).

Simplified for enhanced SValBuilder and ConstraintManager.

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.

NoQ added a comment.Dec 14 2017, 3:58 PM

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.

Updated to be based upon D41938 and D35110.

baloghadamsoftware edited reviewers, added: dcoughlin; removed: zaks.anna.Jan 11 2018, 6:49 AM

Updated to work with the latest Constrain Manager patch.

NoQ added a comment.Jun 27 2018, 12:11 PM

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 ↗(On Diff #153023)

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 ↗(On Diff #153023)

I guess we'll have this sorted out in another patch.

NoQ accepted this revision.Jun 27 2018, 12:11 PM
This revision is now accepted and ready to land.Jun 27 2018, 12:11 PM
This revision was automatically updated to reflect the committed changes.