The main principle remained the same as the original ArrayBoundCheckerV2.
However, now during the simplification of 0 <= subscript-expr < extent we will assume that no overflow/underflow could have happened during the evaluation of the outer-most operator of subscript-expr. This will aggregate such assumptions into the State.
The comments in the code should make the algorithm clear enough. Besides that, I will answer any questions that might arise.
- Add more tests, reorganize current ones.
- Substitute the template machinery of the out-of-bounds-v2-false-positive-hunter.cpp test file to make it run significantly faster .
- Improve the readability of the bug report using NoteTags or BRVisitors - yet to be decided which and how to implement that.
- Update docs to reflect the current implementation.
- Document that this checker uses a heuristic.
I'm planning to come up with something to make the reports more readable. It could be a visitor or NoteTags, I haven't decided yet.
However, which makes this quite heroic is showing why a given expression is thought to be non-overflowing/under-flowing.
I don't have any source location beside the access itself. Imagine a pointer, which is modified line-by-line to point to the final destination which happens to be out-of-bound.
We check when it is dereferenced, but I can not put a NoteTag to the origin of that modification saying that 'assuming that this expression doesn't overflow/underflow'.
How can I implement meaningful diagnostics accomplishing this?
If the extent is symbolic, but the access is concrete, then we will not constrain the symbolic extent to draw the access valid.
One might implement this later though.
 I will rewrite the templated test-cases since the current implementation takes too much time to run.
The analyzer would have to simulate all the template magic just to get to the interesting memory access, which is an unacceptable slowdown IMO.
Currently, that single test file takes about 2.7 seconds to run.
Also, if any test-case fails, pretty hard to find the one that failed since warning locations shared across test-cases xD
Just to tackle the latter, I came up with a new debug expression checker that dumps the value of PRETTY_FUNCTION if a bug report with a given description is on the flight.
If you are interested, I can upstream that as well.