Static Analysis

[hernanponcedeleon]

I have been taking a look to this library for static analysis which is based on this paper. The library already has implemented several analyses that would be useful for us (like constant propagation or value analysis) and it was developed with the idea to be easy to extend. While currently there is no implementation for alias analysis, there is an issue to add support for pointers so I guess alias analysis will follow after that one.

I don't think we would be able to use the library out-of-the-box for the following reasons:

• I'm not yet sure if or how they handle concurrency. In principle there is a notion of heap and one can create several "units" ... however I found no way to model something like pthread_create. The paper claims that the library is intended to support several languages, but the language that they have for writing examples (called IMP) is closer to Java (with classes and methods).
• While the architecture for building the CFG is general and would work with our goto programs, I'm not sure if the rest of the architecture (the analysis) would work for such cases or there is an assumption that the CFG was generated using while and if instructions.
• The LISARunner allows to easily run any of the implemented analysis for programs written in IMP. However, the outcome of the analysis seems to be a .dot file with the result. I did not find a way to access the results (which is what we would need to be use then at encoding time).

Because of the above and also the fact that using this out-of-the-box would requires us writing transformations from our IR to theirs, it might make more sense to re-use some of their code (e.g. Lattices and hopefully AbstractState) but re-implement the rest (e.g. make the fix point algorithm work with our Program instead of their CFG).

[ThomasHaas]

I remember that library. Maybe we could ask them about the concurrency aspect. According to their github, they are still changing the CFG representation to be as flexible as possible. So it might be good idea to make them aware that they need to model concurrency as well.

[hernanponcedeleon]

I don't think this issues brings much value. If we ever revise the idea of properly supporting CFGs, we can still access the resource via "closed issues".