Upstream bufferoverrun changes

[dhauzar]

This pull request contains a part of the patches we wrote with the aim to make BO work on the SIL generated by the Infer Ada frontend (developed at AdaCore).

Focus on zero false-positive rate

The main goal was to provide false-positive free analysis (we have different, more heavy-weight analyses that aim at a low or even zero number of false-negatives). Thus, only messages where BO can prove that the problem occurs are reported. The consequence of that is that an imprecision cannot be a cause of a false positive while an unsoundness can. This can cause a clash between our use of BO and the use of BO at Facebook. In order to avoid this clash, we put changes making BO sound and introducing diffs in cost analysis into options.

New options We put the changes introducing undesired diffs - in particular in cost analysis - under options. These options are:

--bo-sound-unknown-sets-join: join with an unknown set always result in an unknown set. When disabled, an unknown set behaves as bot.

--bo-bottom-as-default: use bottom as a default value instead of unknown. Enabled by default.

--bo-assume-void: assume void type as a type of record fields not in type environment. Enabled by default.

--bo-context-sensitive-allocsites: Assumes that an allocsite is imported as different allocsite from a callee to a caller in different call contexts. This assumption is ensured by the Ada frontend and makes it possible to do strong updates of locations imported from callees to callers more often. Disabled by default.

Notation

Each commit causing diffs in tests output is followed by commits updating test baselines - one commit for each group of tests (c_bufferoverrun, cpp_bufferoverrun, java_bufferoverrun, cpp_performance, and java_performance). Commit messages of commits updating baselines contain an analysis of diffs.

Each commit is marked by one of the following:

Each commit causing diffs in tests output is followed by commits updating test baselines - one commit for each group of tests (c_bufferoverrun, cpp_bufferoverrun, java_bufferoverrun, cpp_performance, and java_performance). Commit messages of commits updating baselines contain an analysis of diffs.

Each commit is marked by one of the following:

[Arrays]: changes in handling of arrays [Top]: make top default instead of bot [F]: other fixes [I]: other improvements

[facebook-github-bot]

@skcho has imported this pull request. If you are a Meta employee, you can view this diff on Phabricator.

[skcho]

@dhauzar Thank you for revising PR to have less changes in the pre-existing tests/semantics, by adding some config parameters. I appreciate that. :purple_heart: (Sorry for somewhat verbose comments.)

Many places became clearer than before by the PR. Awesome!

[facebook-github-bot]

@dhauzar has updated the pull request. You must reimport the pull request before landing.

[facebook-github-bot]

@dhauzar has updated the pull request. You must reimport the pull request before landing.

[facebook-github-bot]

@dhauzar has updated the pull request. You must reimport the pull request before landing.

[facebook-github-bot]

@dhauzar has updated the pull request. You must reimport the pull request before landing.

[facebook-github-bot]

@dhauzar has updated the pull request. You must reimport the pull request before landing.

[facebook-github-bot]

@dhauzar has updated the pull request. You must reimport the pull request before landing.

[facebook-github-bot]

@dhauzar has updated the pull request. You must reimport the pull request before landing.

[skcho]

@dhauzar I think all comments were addressed. Thank you for the updates. Let me import the PR!

[facebook-github-bot]

@skcho has imported this pull request. If you are a Meta employee, you can view this diff on Phabricator.

[dhauzar]

Thank you very much for your insightful comments @skcho, it really improved the PR :)