Split up dependency graph implementation

[danpoe]

Part of the complexity of the current dependency graph implementation comes from the fact that data dependencies and control dependencies are computed simultaneously by the same analysis (with domain dep_graph_domaint) and then a graph is built from the result (in dependence_grapht, which is derived from ait).

Since neither control dependencies are needed to compute data dependencies (nor vice versa), the code could be simplified by computing them by separate analyses, and then another class would consume the information of both and build the dependency graph.

[tautschnig]

I'd like to note that I have got work that further splits up data dependencies (due to some recent, rather prominent event). This wouldn't really stop what's being suggested here, but it may be worth talking about before anyone actually getting to action.

[martin-cs]

I completely agree with @danpoe's suggestion. Data-dependencies are (IMHO) best computed with an abstract interpretation approach while control dependencies are (at the moment) CFG-based. Some extra complications:

1. @chrisr-diffblue is hard at work on a new way of computing data-dependencies. He will also need to handle control dependencies so may be ... supportive / enthusiastic about modularising and re-using this code.

2. There are some rather critical patches in the Toyota branch which are not (at the moment!) really suitable to merge to develop but it would be good if these didn't get broken in the next ... 6 weeks or so while we finish the project.

3. I think @danpoe has some open patches for this part of the code...

[danpoe]

A heads up on this, we are planning to do the suggested refactorings (starting in about a week or so).

Here's the plan:

• Make the control dependence computation a separate non-AI analysis. We'll also add annotations true and false to indicate whether a statement postdominates the true or false successor of a goto statement on which it depends. Moreover the function entry point will also have a dependency on all the calls to the function. These two things are requirements of an industrial partner. We'll make this configurable though.

• Make the data dependence computation a separate non-AI analysis. The analysis would iterate over the instructions in the goto program and for each use the information computed by the reaching definitions and goto rw analyses to compute the instructions on which it depends.

• The dependence graph will then take the information computed by the two analyses above and build a graph from it.

@tautschnig @martin-cs Does that sound reasonable to you?

@tautschnig Would the suggested refactoring of the data dependence computation clash with your patches that further splits up data dependencies?

[martin-cs]

1. Control dependency as non-AI. Yes; sounds good as it is basically a CFG property. I can't see that AI information will help you compute this any way other than finding dead paths and I think there are other ways of interfacing that.

2. Can you expand a bit more what you mean? I would keep the reaching definitions (and supporting analyses) as an AI analysis. I /presume/ you are proposing the lifting of the graph computation out from this so alternative reaching definitions can be used. That much I would support.

3. Sounds good.

[tautschnig]

Now that sufficient time has passed, and with regard to the possible clash: my suggestion is to introduce a concept of address dependencies. These are a subset of data dependencies that are used to compute pointer offsets or array indices. I don't strictly expect you to integrate this in your planned work, but maybe you can give it some thought. Why do I care? Speculation ...

[danpoe]

@martin-cs Yes, the reaching definitions analysis would stay as is, just the code that uses the information it computed to compute the data dependencies would become a non-AI analysis.

[danpoe]

@tautschnig Ah, I see. Yes, I think that should be mostly orthogonal to the refactorings proposed here.

[martin-cs]

@danpoe : sounds great then, esp. if we can swap in the variable sensitivity domains's last modified information.

[thomasspriggs]

I am going to close out this issue, given that it was about a refactor which @danpoe was working on and that he is not currently contributing to cbmc.