Interface for function summaries/data flow analysis

[fortunac]

We should design an interface that can connect a possible data flow analysis with WP.

Some suggestions/notes:

• a config file that maps a function to a summary
• different summary descriptions: nop, chaos, memory information/pointers
• use sexp_of_map to read the map from the config file into WP

[codyroux]

Generally I'd expect this to be implemented in the same way as the VSA, that is using http://binaryanalysisplatform.github.io/bap/api/odoc/bap/Bap/Std/Value/index.html, to register a module, with a field in the Project.storage data structure, of type Dict.t.

Main differences:

• The information transmitted will be a map from TIDs to elements of the abstract domain (did we ever figure out whether these are unique when comparing binaries?)
• The abstract domain is a set of variables (registers/virtual registers). Being a member of that set means "definitely a pointer to the heap" and otherwise means "can be anything, including a pointer to the heap".

Though this is not really addressing this ticket, some implementation details:

• I'll be using the fixpoint method from here: http://binaryanalysisplatform.github.io/bap/api/odoc/graphlib/Graphlib/Std/Graphlib/index.html Seems pretty straightforward.
• I'll need to build a whole-program CFG first though, which for some reason isn't available. I'm also thinking of having a finer-grained graph with a node per instruction, since we both want abstract state at the beginning of a block and also at the end, if there's a call.
• I suspect we'll eventually need an abstract state for memory accesses. This sadly means there will be aliasing issues, which might be already handled by some other pass, but otherwise needs some gnarly heuristics (or a good ol' VSA). An unsound but easy heuristic is: distinct expressions represent different regions of memory, within a function boundary. IDK I'll have to ask Ivan.

Thoughts and suggestions are welcome.