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 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 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
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: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:
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.
Commits causing diffs:
[F] Fix join of unknown set of locations.
[F] Fix strong updates when updating multiple locations.
[F] Fix strong updates when handling subprogram calls.
[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)
[F] Don't prune locations that can be only weakly updated.
functions with diffs: 10 (java perf)
[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.
[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)
[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)
[F] Fix setting the length of new array.
functions with diffs: 1 (java-perf)
[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)