Data Flow Analysis for acq-rel

[Baltoli]

Previously I've implemented a set of experiments for demonstrating the properties of my acq_rel automaton. In order to statically analyse these automata, I need to work out how best to perform the data flow analysis on the LLVM IR.

Things that need to be done in order for this to go ahead:

• Identify the start and end bounds for a usage. The simplest case is that they are call / return for the same function, so should start with this case.
• Map the assertion argument to a Value * somehow. I think this will involve ripping out the part of the AssertionSiteInstrumenter that does the argument collection and mapping - need to audit that code path to work out what class state it relies on.
• Work out the machinery for adding an LLVM pass to the project.
• Formalise the behaviours that we expect the automata to have (i.e. write up each of the executable examples and what they do / why they do it).
• Actually implement the analysis at the IR level.
• Build some examples you'd expect to be able to statically analyse and do the analysis by hand (i.e. what does the call graph look like? the data flow? control flow? maybe write parts of this up as well)

[Baltoli]

Have written up the informal specifications for the behaviour of acq_rel.

[Baltoli]

Looking into adding an LLVM pass to the static analysis now. I think what I need to do is:

• Implement the analysis as an LLVM ModulePass.
• The pass can then be run on the module given. The interface for a pass is the abstract RunOnModule method which allows us to separate concerns (but also need to pass some info into the pass - simple bound name for example).
• Can then retrieve the results from a class property.

[Baltoli]

Important

The argument collection code will modify the module IR it is run on. This is because it creates load instructions for the values in scope, and so the module pass will always need to return a value that indicates it has modified the IR.

[Baltoli]

For the most part this is done now - there are some edge cases that aren't totally covered, but the majority of the analysis exists and can be run on a module.