This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Add "Assuming..." diagnostic pieces for unsupported condition expressions.
ClosedPublic

Authored by NoQ on Aug 9 2016, 2:22 AM.

Details

Summary

In path diagnostics, the "Assuming ..." diagnostic piece represents the event (i.e. yellow in html diagnostics) of adding constraint to a symbol, and there are also "Taking ..." diagnostic pieces, which represent the decision on program path that was made based on existing constraints.

For example:

void foo(int x) {
  if (x == 2) // Assuming and Taking.
  {
    if (x == 3) { // Only Taking.
    } else {
      1 / 0; // Bug.
    }
  }
}
  1. This code would produce the "Assuming x is equal to 2" piece, which represents that on the previous execution path it was not known that x is equal to 2, but now we consider this path as separate.
  2. Then this code would produce the "Taking true branch" piece, which would tell the user that we inevitably follow the true branch because of the assumption we made earlier.
  3. Then in the inner if, this code would produce the "Taking false branch" piece. However, it would not produce the new "Assuming x is not equal to 3" piece, because it doesn't need to assume this - it is already inevitable.

Now, the problem with "Assuming ..." pieces is that they are "pretty". If the analyzer fails to pretty-print the assumption - i.e. transform "(x == 2)" to "x is equal to 2" - then it fails to add the piece, and the user gets a false impression that taking the branch was inevitable.

Expressions unsupported by the pretty-printer are fairly common and include function call expressions, field or instance variable expressions, and logical operators.

This patch adds the generic "Assuming the condition is true/false" pieces whenever the pretty-printing fails. This way we keep understanding why the analyzer thinks that a certain branch is feasible.

This patch helps a lot with understanding bug reports, which originally seem like false-positives.

I've eye-inspected all the changes on tests, and i like all the newly added pieces.

This mechanism can still be improved by supporting more expression pretty-printing.

A couple of examples:

Diff Detail

Event Timeline

NoQ updated this revision to Diff 67298.Aug 9 2016, 2:22 AM
NoQ retitled this revision from to [analyzer] Add "Assuming..." diagnostic pieces for unsupported condition expressions..
NoQ updated this object.
NoQ added a subscriber: cfe-commits.
xazax.hun edited edge metadata.EditedAug 9 2016, 3:49 AM

In case there is a more complex condition does it only highligh the part that influenced taking the branch?

E.g.:

if (a || b) { // HIghlight only a, if a was true and b was not evaluated
}
NoQ added a comment.Aug 9 2016, 8:05 AM

In case there is a more complex condition does it only highligh the part that influenced taking the branch?

E.g.:

if (a || b) { // HIghlight only a, if a was true and b was not evaluated
}

Not yet, and this part of things is still broken - perhaps more patches would be needed to address all the issues:

The hardest part would be, of course, dealing with UnknownVals and UndefinedVals in conditions, because they are completely ignored by these visitors - after all, no constraints are being added.

So we're far from consistency, just some improvements.

zaks.anna edited edge metadata.Sep 12 2016, 10:53 AM

@NoQ,

Let's test in an IDE. Can you send screenshots?

NoQ updated this revision to Diff 73014.Sep 30 2016, 2:43 AM
NoQ edited edge metadata.
  • Improve the way the new piece for if (x && y) looks in Xcode. The "Assuming the condition is true" for y is now placed at the beginning of y rather than at the beginning of x, which removes the weird arrow from y back to x in Xcode.
  • Fix condition is true vs condition is false error with odd number of !-operators within the condition (the code above was modifying the tookTrue variable before failing).

I'd be adding more fixes on top of this patch - in particular, i've managed to fix other issues with logical operators that were mentioned above.

NoQ updated this revision to Diff 73020.Sep 30 2016, 2:46 AM

Whoops sorry, wrong diff.

NoQ updated this revision to Diff 73021.Sep 30 2016, 2:53 AM

Whoops sorry, forgot to add the context.

NoQ updated this revision to Diff 73039.Sep 30 2016, 6:03 AM

Reverted to the original patch. My plan to follow-up with a fix for all logical operators made me realize that i don't need the new part here - will just follow-up with a proper fix. Sorry for the noise.

NoQ updated this revision to Diff 73469.Oct 4 2016, 6:33 AM

Brought back the fix for true/false, because it's needed after all. Added a test for that.

zaks.anna accepted this revision.Oct 4 2016, 11:51 AM
zaks.anna edited edge metadata.
This revision is now accepted and ready to land.Oct 4 2016, 11:51 AM
This revision was automatically updated to reflect the committed changes.