Upstream bufferoverrun changes

[dhauzar]

This pull request contains patches we wrote with the aim to make BO work on the SIL generated by the Infer Ada frontend (developed at AdaCore). Due to the size of the diff, we are interested in upstreaming as much as possible of those patches.

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.

An example of this is the commit “[F] Fix join of an unknown set of locations.” fixing an unsoundness intended in the original design of BO. For us, the unsoundness was causing unacceptable false positives. Here is the test containing a comment (codetoanalyze/java/bufferoverrun/ArrayListTest.java:loop_on_unknown_iterator_FN) explaining that the unsoundness was intended in the original design:

  void loop_on_unknown_iterator_FN(MyI x, int j) {
    ArrayList<Integer> a = new ArrayList<>();
    ArrayList<Integer> b;
    if (unknown_bool) {
      b = a;
    } else {
      b = x.mk_unknown();
    }
    // `b` points to an zero-sized array and `Unknown` pointer.  Thus, the size of array list should
    // be evaluated to [0,+oo] in a sound design.  However, this would harm overall analysis
    // precision with introducing a lot of FPs.  To avoie that, we ignore the size of `Unknown`
    // array list here, instead we get some FNs.
    for (Integer i : b) {
      // Since size of `b` is evaluted to [0,0], here is unreachable.
      if (a.size() <= -1) {
        int[] c = new int[5];
        c[5] = 0;
      } else {
        int[] c = new int[10];
        c[10] = 0;
      }
    }
  }

If such changes are not acceptable, we would be interested in adding an option --sound-bufferoverrun. This would allow us to change the strategy used for the analysis on our side, while still reducing the size of our diff. (And hopefully make all this manageable on your side too.)

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
• [Precond]: reimplement detection of reachability in order to be able to eliminate overly strong preconditions
• [F]: other fixes
• [I]: other improvements

Overview of the impact

Here is the overview of the current state of the impact of the patches. The detailed information about individual diffs in the FB's tests is in the commit messages of commits updating test baselines.

• 22 commits
• 11 commits causing some diffs
• 2 difficult, 3 definitely needs some attention, 6 could be fine

Commits causing diffs:

[F] Fix join of unknown set of locations.

• 1 diff (diff in 1 function)
• Improvement

[F] Fix strong updates when updating multiple locations.

• 1 diff
• Regression
• Problem: BO assumes that the location (of a dereference kind) that should be weakly updated can be indeed strongly updated (this is because the function AbsLoc.can_strong_update is not sound)
• Solution
  • Modify C frontend to use a kind of pointer which makes it clear that the pointer has a single possible target to access array elements (Pk_reference)
  • Use a sound variant of AbsLoc.can_strong_update

[F] Fix strong updates when handling subprogram calls.

• 2 diffs
• Improvement, but reveals a problem - one allocsite for two different arrays (created in the same function) is got
• Solution
  • When importing an allocsite from the caller, add an identification of the call (caller + call node)
  • Or change the frontend to copy the allocsite after the call (like the Ada frontend does)

[Top] Use top as a default for value of a location.

• #functions with diffs: 97: 18 (c) + 50 (cpp) + 16 (java) + 6 (cpp perf) + 7 (java perf)
• #functions with diffs on L1, L2, and condition predetermined (“high diffs”): 6 (c) + 7 (cpp) + 0 (java)
• Main problems
• Initialization of arrays (many diffs)
  • With top as default and weak update, an array cannot be initialized without additional tricks
  • For Ada, we use builtins for initialization of arrays and copying of arrays, for local arrays without explicit initialization, we write bot for them to the abstract state (assuming that there is no access to uninitialized part of the array)
  • Another option (we had used) is to use bot as a default for locations representing arrays
• Creating additional checks resulting in may- warnings (many diffs)
  • When creating a check, if some of its constituents evaluate to bot, the check is not created -> after the change, more may- checks are created
• Writing bot as a value of an allocsite when doing malloc in a loop (one revealed diff)
  • -> problem when testing in a loop that the next array element has a different value

[F] Don't prune locations that can be only weakly updated.

• #functions with diffs: 10 (java perf)
• Most likely, the diffs are caused by the previous commit (top instead of bot as a default value) and the fact that null is not pruned out (of top)

[I] Don't store info about unkn. locations in abstr. state.

• #functions with diffs: 1 (c) + 3 (cpp)
• #functions with diffs on L1, L2, and condition predetermined: 0

[I] Prune also stack variables.

• 1 minor diff

[I] More precise handling of symbolic intervals.

• #functions with diffs: 10 (c) + 6 (cpp) + 1 (java)
• #functions with diffs on L1, L2, and condition predetermined: 8 (c) + 2 (cpp)
• Finds some new TPs, but breaks the deduplication mechanism (some warnings subsumed by others are reported)

[F] Fix type info for record fields in type environment.

• #functions with diffs: 5 (c) + 5 (cpp) + 2 (cpp-perf)
• #functions with diffs on L1, L2, and condition predetermined: 1 (c) + 1 (cpp)
• Problem: the missing type info is no longer guessed to be void

[F] Fix setting the length of new array.

• #functions with diffs: 1 (java-perf)
• Regression, not analyzed

[Precond] Reimplement detection of reachability.

• #functions with diffs: 22 (c) + 26 (cpp) + 2 (cpp-perf) + 3 (java-perf)
• #functions with diffs on L1, L2, and condition predetermined: 18 (c) + 11 (cpp)
• Both improvements (reporting violations of overly strong preconditions) and regressions (in particular losing preconditions)
• Causes of diffs
  • Propagating checks to preconditions conservatively (most of the diffs) A precondition is not created when it may be overly strong (in particular the path condition being too complex)
    • Could be made more precise, but this was not our goal
  • Latest prune is now used only to capture path conditions, no relations between variables in branches captured after join point
  • The way how latest prune is joined is currently not working well on irreducible CFGs

[yakobowski]

Note that we will of course fix the merge conflict(s) if you are interest in the patch.