Verify graph-based Galois connection in tests

[rolyp]

Tests should assert round-tripping properties of Galois connection for each test.

[rolyp]

Never got around to implementing this 3 years ago, because computing slices was too slow. Now it should be easy, so adding this into the plan.

[min-nguyen]

It seems that fwd slicing a graph, given some selections on the input expression and environment, sometimes isn't producing enough annotations on the output. This is because some sinks are also being created at run-time which the output will depend on, and these won't be found in the expression/environment. (I think this means that, even if we forward-slice a graph w.r.t all the addresses in the input expression + environment, in some cases, this still wouldn't be enough to produce selections on all the output values).

Although this limits whether we can test forward-slicing as an independent procedure, it is still possible to test round-tripping by: performing bwd slicing wrt an output value, extracting all the sinks of the resulting graph (rather than from the original expression/environment), and then fwd slicing wrt these sinks.

[rolyp]

@min-nguyen Yes I think that’s possible in principle (i.e. not ruled out by the laws of Galois connections), although I can’t right now think of a situation where a node can be created that won’t at least depend on an expression found either in the original program or in a closure reachable within the environment. Testing forward-slicing “independently” would then require knowing what these sinks are and essentially treating them similarly to inputs.

There may be more thinking to do here, i.e. we might like to determine exactly when these “untracable values” arise (intermediates we can construct without consuming any input resources) and rule them out by establishing appropriate dependencies. But what you’ve done for now looks fine.

One thing we should do is assert that sources gbwd $\subseteq$ sources gfwd since that is required by the Galois connection laws.

[min-nguyen]

@rolyp

although I can’t right now think of a situation where a node can be created that won’t at least depend on an expression found either in the original program or in a closure reachable within the environment.

It's strange, but it seems to be happening. Some entries in the out neighbours are of the form a x {} (a depends on nothing), where a can't be found in the environment or expression.

One thing we should do is assert that sources gbwd $\subseteq$ sources gfwd since that is required by the Galois connection laws.

This currently holds true for all the tests (except the slice/filter case), in a way. Specifically, the result of fwd slicing wrt the sinks of the bwd graph is consistent with the expected output (which always contains at least as many annotations as the original selected output).

[rolyp]

the result of fwd slicing wrt the sinks of the bwd graph is consistent with the expected output (which always contains at least as many annotations as the original selected output).

Yes I’m looking at that at the moment and it’s good that we can assert that. But how do we know that expected has at least as many annotations as the original output selection? (And I realise I’m missing the obvious but why isn’t the slice/filter case failing at the moment?)

[min-nguyen]

Have you changes unless false $ to unless true, in testGraph in test.Util?

[rolyp]

Now I have!

I’m still curious about the other question though..

[min-nguyen]

But how do we know that expected has at least as many annotations as the original output selection?

Well the argument expected is defined as a string in a file right? And I assume you wrote those files to be the actual bwd-then-fwd results we should expect from the original trace-based approach (containing at least as many annotations as the selected output). This is what I'm comparing against.

[rolyp]

Ah, right. Yes that’s true. (I’d forgotten that the expected values are actually the value expected after a bwd-then-fwd round trip.) I think it might still be good to enforce that as a general property. The initial output selection is currently provided by programmatically by a Selector, and the final output selection by comparing a manually supplied string against the output of a prettyprinter, so the current relationship is quite indirect with various opportunities for things to go wrong.

[rolyp]

By the way, when you uncomment the tests do the graphical tests also fail?

[min-nguyen]

Ah, right. Yes that’s true. (I’d forgotten that the expected values are actually the value expected after a bwd-then-fwd round trip.) I think it might still be good to enforce that as a general property. The initial output selection is currently provided by programmatically by a Selector, and the final output selection by comparing a manually supplied string against the output of a prettyprinter, so the current relationship is quite indirect with various opportunities for things to go wrong.

Good point, i'll do this now :)

[rolyp]

I reckon this task can be closed if you’ve added that explicit subset check (it will be easy enough to add similar checks later when we come to e.g. switch the linking examples over to the new graph approach).