Closed Baltoli closed 7 years ago
Have written up the informal specifications for the behaviour of acq_rel
.
Looking into adding an LLVM pass to the static analysis now. I think what I need to do is:
ModulePass
.RunOnModule
method which allows us to separate concerns (but also need to pass some info into the pass - simple bound name for example).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.
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.
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:
Value *
somehow. I think this will involve ripping out the part of theAssertionSiteInstrumenter
that does the argument collection and mapping - need to audit that code path to work out what class state it relies on.