[analyzer][solver] Track symbol disequalitiesClosedPublicActions

Authored by vsavchenko on Jul 7 2020, 2:13 AM.

Details

Reviewers
 NoQ dcoughlin ASDenysPetrov xazax.hun Szelethus
Commits
rGe63b488f2755: [analyzer][solver] Track symbol disequalities
Summary

This commmit adds another relation that we can track separately from
range constraints. Symbol disequality can help us understand that
two equivalence classes are not equal to each other. We can generalize
this knowledge to classes because for every a,b,c, and d that
a == b, c == d, and b != c it is true that a != d.

As a result, we can reason about other equalities/disequalities of symbols
that we know nothing else about, i.e. no constraint ranges associated
with them. However, we also benefit from the knowledge of disequal
symbols by following the rule:

`if a != b and b == C where C is a constant, a != C`

This information can refine associated ranges for different classes
and reduce the number of false positives and paths to explore.

Diff Detail

Event Timeline

vsavchenko created this revision.Jul 7 2020, 2:13 AM
Herald added a project: Restricted Project. Jul 7 2020, 2:13 AM
Herald added subscribers: cfe-commits, martong, Charusso and 7 others.
NoQ added a comment.Jul 7 2020, 9:02 PM

This looks great to me but i'd very much rather have someone else have a look, just because of the nature of the problem (:

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1579

Nit: I think it's a bit messy to use getDisequalClasses() in some places but manual lookup in other places. Like, someone may change the function and believe that they changed the entire lookup mechanism but fail to notice that the function wasn't used consitently. I think this may be worth encapsulating.

1721

Parse error; missing "we"?

1914–1916

I actually wouldn't mind duplicating a direct assertion here, given that consistency checks are pretty complicated on their own :)

clang/test/Analysis/mutually_exclusive_null_fp.cpp
26

// no-warning please? These marks make tests a lot easier to understand when you break them 5 years later.

@vsavchenko

if a != b and b == C where C is a constant, a != C

Did you take into account that e.g. a > b also is a disequality.

Did you take into account that e.g. a > b also is a disequality.

It is a very good point! I didn't take them into account (yet?) because they make the implementation a bit harder.
Right now we can decide by the look of the assumption (or symbolic expression) if it's an equality/disequality check. Later on, if we see an expression that looks like equality/disequality, we can try to see what we know about its operands. So here we have a fairly easy table (2x2) of possible outcomes: if our current knowledge of the equality/disequality matches the current check - it's true, if it's opposite - it's false.

When it comes to things like a > b, we can consider it as disequality when we start tracking it because a > b -> a != b, but cannot in the second case because a != b -/-> a > b. As the result, this beautiful symmetry that I use is gone and we need to add more data into EqualityInfo so we support the one-sidedness of that implication.

It is not a big change, but I would prefer making it separately.

vsavchenko updated this revision to Diff 276729.Jul 9 2020, 6:58 AM

Fix review remarks

vsavchenko marked 4 inline comments as done.Jul 9 2020, 7:00 AM
vsavchenko added a comment.EditedJul 13 2020, 1:28 AM

Introduction

I have some test results with execution times. Because the execution time varies from one execution to another, I've measured performance on master twice (I know that it's not very conclusive) to show that equivalence tracking doesn't affect performance of the analyzer. So, please, let's treat it more like a smoke test that everything stayed the same with a new functionality rather than a full-blown performance benchmarking.

Raw results

projectmaster run#1master run#2patch run#1
box2d137.57s156.36s142.46s
cxxopts26.74s29.31s27.01s
drogon257.43s265.88s263.00s
duckdb2251.08s2297.60s2258.06s
fmt266.96s293.06s279.26s
libsoundio33.89s35.37s36.48s
oatpp171.58s175.25s172.92s
re284.12s133.46s87.24s
simbody1405.25s1374.38s1365.58s
symengine455.94s487.50s466.28s
termbox20.91s20.28s20.88s
tinyexpr11.91s13.53s12.58s
tinyspline48.61s49.01s48.90s
tinyvm27.77s29.32s28.70s
zstd150.28s152.86s154.21s

Processed results

projectmin deltamax deltawithin range
box2d-8.9%3.6%
cxxopts-7.8%1.0%
drogon-1.1%2.2%
duckdb-1.7%0.3%
fmt-4.7%4.6%
libsoundio3.1%7.6%
oatpp-1.3%0.8%
re2-34.6%3.7%
simbody-2.8%-0.6%
symengine-4.4%2.3%
termbox-0.1%3.0%
tinyexpr-7.0%5.6%
tinyspline-0.2%0.6%
tinyvm-2.1%3.3%
zstd0.9%2.6%

Diff results

The only project that had any difference in terms of warnings was simbody:

```--- Building project simbody
2020-07-08 07:53:32,956:INFO:main: Log file: /projects/simbody/ScanBuildResults/Logs/run_static_analyzer.log
2020-07-08 07:53:32,956:INFO:main: Output directory: /projects/simbody/ScanBuildResults
2020-07-08 07:54:03,447:INFO:main:   No local patches.
2020-07-08 08:16:18,536:INFO:main: Build complete (time: 1365.58). See the log for more details: /projects/simbody/ScanBuildResults/Logs/run_static_analyzer.log
2020-07-08 08:16:22,965:INFO:main: Number of bug reports (non-empty plist files) produced: 181
2020-07-08 08:16:29,197:INFO:main: REMOVED: [../SimTKmath/Optimizers/src/IpOpt/IpSymScaledMatrix.cpp] ../SimTKmath/Optimizers/src/IpOpt/IpSmartPtr.hpp#GetRawPtr:585:5, Memory error: Use of memory after it is freed
2020-07-08 08:16:29,197:INFO:main: REMOVED: [../SimTKmath/Optimizers/src/IpOpt/IpScaledMatrix.cpp] ../SimTKmath/Optimizers/src/IpOpt/IpSmartPtr.hpp#GetRawPtr:585:5, Memory error: Use of memory after it is freed
2020-07-08 08:16:29,197:INFO:main: TOTAL REPORTS: 1106
2020-07-08 08:16:29,197:INFO:main: TOTAL REMOVED: 2
2020-07-08 08:16:29,197:INFO:main: Warning: 2 differences in diagnostics.
2020-07-08 08:16:29,197:INFO:main: Error: Diffs found in strict mode (2).
2020-07-08 08:16:29,197:INFO:main: Diagnostic comparison complete (time: 6.23).
2020-07-08 08:16:29,197:INFO:main: Completed tests for project simbody (time: 1376.24).```

These two warning are two FPs related to custom ref-counting pointers and the analyzer was able to figure out that the counters could not be 1 at some point.

NoQ accepted this revision.EditedJul 13 2020, 4:39 PM

Data 👍

Maybe spend a few minutes remeasuring libsoundio more carefully, just in case? Also i really wish we had per-TU data of that kind, to see if any particular TUs have regressed significantly.

These two warning are two FPs related to custom ref-counting pointers and the analyzer was able to figure out that the counters could not be 1 at some point.

That's pretty amazing. I hate these false positives because there's often too little we can do.

This revision is now accepted and ready to land.Jul 13 2020, 4:39 PM
In D83286#2148787, @NoQ wrote:

Data 👍

Thanks 😊 These tables are already generated by a script and I plan to make it into a phabricator reporter, so it is easier to put all the data we need here.

Maybe spend a few minutes remeasuring libsoundio more carefully, just in case?

Sure, will do!

Also i really wish we had per-TU data of that kind, to see if any particular TUs have regressed significantly.

I think we even store all this information about the run, but it needs a bit of refactoring in CmpRuns.py to get it in a nice way. I think it's a good feature to put into my plan for the testing system.

Maybe spend a few minutes remeasuring libsoundio more carefully, just in case?

Sure, will do!

It turns out that libsoundio has a problem similar to re2 and varies a lot in terms of the analysis time (probably we can even try to figure out some reasons behind it sometime in the future).
Here is the chart comparing 50 runs before and after:

@xazax.hun You were interested in performance ⏫

These results here compare this patch together with D82445 against master.

@xazax.hun You were interested in performance ⏫

These results here compare this patch together with D82445 against master.

This is really great news, thanks!

This revision was automatically updated to reflect the committed changes.