Add support for bounded static analysis

[wuestholz]

This adds support for bounded abstract interpretation, which allows users to bound the analysis based on their available time or their tolerance for imprecision and spurious errors. For instance, users can bound the number of analysis steps per method using the /maxSteps command line option. In addition, users can bound common sources of imprecision, such as joins (/maxJoins), widenings (/maxWidenings), and calls (/maxCalls).

Bounding the analysis can improve precision and performance (by up to 8x in our experiments), but might miss bugs. It is meant to provide faster feedback to users (e.g., in the IDE) with fewer spurious warnings.

It allowed us to uncover 5 bugs in msbuild by focusing on high priority warnings (/warninglevel low): dotnet/msbuild#452, dotnet/msbuild#569, dotnet/msbuild#574.

[yaakov-h]

@wuestholz If I understand, bounded analysis limits the static checker in what it checks? How does this improve precision?

How does /warninglevel low mean that high-priority warnings are focused?

Hoe does limiting the static checker in what it checks uncover new bugs?

[wuestholz]

@yaakov-h Thank you for the questions. Let me try to provide some more details.

By bounding the analysis some program traces may not be checked. Intuitively, this allows the analysis to check the remaining ones more precisely. In particular, some warnings may not be reported because they hold for the traces that were analyzed. However, if the analysis wasn't bounded the analysis may consider more program traces (including ones that are actually not possible due to inherent imprecision in the analysis) and report a spurious warning. Usually precision is measured by the number of spurious warnings, while soundness is measured by the number of genuine bugs that are missed.

/warninglevel low does not report low-priority warning (ones with a low score based on Clousot's ranking).

In general, bounding the analysis does not uncover new bugs. However, it can increase the score of warnings. As a consequence, some low-priority warnings that would usually be suppressed are not suppressed when the analysis is bounded. For instance, the above bugs would have been reported as low-priority warnings without bounding the analysis. However, looking at all these warnings would have never been possible for us in reasonable time.

[yaakov-h]

Does that mean that /warninglevel low really means /ignorewarningsthatare low?

[wuestholz]

@yaakov-h Not exactly, since /warninglevel high does not mean /ignorewarningsthatare high. All warnings are scored and the warning level controls the threshold for how high that score needs to be in order to show the warning.