Support for out-of-bound memory accesses

[natgavrilenko]

We should revise the way we handle out-of-bound memory accesses.

Ideally, we should be able to find candidate executions with out-of-bound accesses. Or at least we should treat such accesses consistently (e.g., may alias with any other memory access) and document the limitations in the README. Currently, verification results vary a lot depending on the selected solver and alias analysis method.

There is a summary of verification results for variants of a simple test. The malloc variants are added for future testing (alias analysis for malloc is currently work in progress).

tests.zip

[ThomasHaas]

The issue is a mismatch between the provenance model assumed by the alias analysis vs. the provenance model we encode.
The different alias analyses only expose parts of this issue but themselves do not really cause it.
Btw. the older alias analyses (especially alias-insensitive) should be treated as deprecated I think.

The summary is this:

• Our alias analysis assumes pointers adhere to a provenance model: each pointer has provenance data attached to it which designates what region of memory it can access. Importantly, doing pointer computation on such a pointer does not change it's provenance.
• Our assumed provenance model is that a pointer has shape (base, offset) (C-like provenance) where base is a memory object that functions as provenance data. Accesses outside of the base object are UB (i.e. offset < 0 or offset > sizeof(base))
• Our encoding, however, does not encode the provenance model (each pointer is a plain integer address). This is why the encoding is incapable of detecting OOB/UB.
• The solution(*) is to implement a proper PointerType and appropriate pointer expressions. The encoding then has to encode pointers as tuples (base, offset). The only major difficulty here is that int2ptr casts become hard to implement (and some annoying issues related to modelling pthread).

I think it is reasonable to assume that all code we support adheres to (at least) a (base, offset) provenance model, i.e., where pointers are restricted to within objects. Though we could provide configurable provenance models in principle.

I do have a BA student who is working on this and he has implemented pointer types all the way to the encoding stage.
That being said, my experience with student code is that it does not satisfy standard requirements, so I don't mind if a more experienced person wants to give it a try.

(*) A more ad-hoc (and thus approximative) solution would be to make our analyses (Alias/RA) the ground-truth of provenance: A read that has no valid rf-edge according to RA/AliasAnalysis, could be assumed to be OOB. Reading from initial memory might need special reasoning though.