Addition + exception slicing bug about slicer

[jamescheney]

I agree. I thought about how to accomplish this and it seems a little tricky. Basically, if the trace raised an exception then we just want to slice the one subtrace that raised the exception w.r.t. the exception criterion. However, we also have to slice the preceding arguments' subtraces w.r.t. ret [] because they may have had side effects; consider

let x = ref 1 in
(x := !x - 1;; 42) + (1/ !x)

here the reason an exception was raised is that x was decremented on the LHS of +, so we had better slice the trace of the LHS, but we can get rid of the 42:

let x = ref 1 in
(x := !x - 1;; _) + (1/ if !x == 0 then raise "Division_by_zero" else _)

(but currently we don't.)

[jstolarek]

(but currently we don't.)

I guess we should leave this ticket open as a reminder?

BTW. If I say:

let t = trace (
    let x = ref 1 in
    (x := !x - 1;; 42) + (1/ !x) ) in
bwdSlice (t, raise "Division by zero" )

then indeed I get the slice which is identical to full program. But if I instead say:

let t = trace (
    let x = ref 1 in
    (x := !x - 1;; 42) + (1/ !x) ) in
bwdSlice (t, raise (_:string) )

the intention being "I know I got some sort of exception, show me how I got it" then I get this:

val it = _ : trace(int)

Not a very useful answer. Is this intended to work like this?

[jamescheney]

This seems like it may be an artifact of the fact that we have changed "/" to throw an exception on division by zero without adjusting the definition of isExn. We may need to add information to the trace indicating that an exception was raised during a primitive operation.

[jstolarek]

I've been looking at this for the past hour with no progress.

This seems like it may be an artifact of the fact that we have changed "/" to throw an exception on division by zero

No, that's not because of an implicit exception generated by division by 0 (though this also seems wrong - more on this in a moment). If I say:

let t = trace (
    let x = ref 1 in
    (x := !x - 1;; 42) + raise "foo" ) in
bwdSlice (t, raise "foo" )

then this produces:

val it = let x = _
in (_ ;; 42) + (raise "foo") : trace(int)

But if I replace the slicing criterion with raise (_:string) then I again get an empty trace: val it = _ : trace(int)

without adjusting the definition of isExn.

It seems to me that definition of isExn does the right thing:

isExn (TOp _ ts) = any isExn ts

It will report an exception if any of the arguments raised one. What seems fishy is the fact that returning an implicit exception is not reflected in any way in the trace. I assume this is what you meant by "we may need to add information to the trace indicating that an exception was raised during a primitive operation". It seems we might need another constructor in Trace to represent an implicitly raised exception. But I think this is a problem independent of the original issue reported in this ticket.

BTW. I was convinced that the originally reported problem of slicing

let t6 = trace ( 1 + (raise "foo") ) in
bwdSlice (t6, raise "foo")

was fixed by the outcomes patch, but I just realized it was not. We still get 1 + (raise "foo") as the slice.

[jamescheney]

Yes, I thought about this while working on "outcomes" but didn't see exactly the right thing to do.

The issue is that TOp has a list of subtraces. Either

• all of them succeeded and returned, in which case we should slice all w.r.t. ORet VStar.
• one of them raised an exception, in which case the earlier ones succeeded and the later ones are THole. In this case we want to slice wr.t. [ORet VHole,...,ORet VHole, exn, EHole,...,EHole] where exn is the exception outcome OExn v we were slicing through TOp.
• in any case we want to slice backwards through the list so that any store side-effects are handled in the right order (in reverse order, currently accomplished via foldR)

I think the issue of implicit exceptions raised by "/" is a separate tricky thing. Probably this just needs a flag on TOp to record the case where all operands succeeded but the operation raised an exception, which we want to handle similarly to when it returned normally. "Minimal" slicing might be operation-dependent, for example, for division by zero we only need to know that the denominator was zero and it doesn't matter what the numerator was, but I think it is fine to assume that all arguments are potentially relevant to the exception being raised.

[jstolarek]

In this case we want to slice wr.t. [ORet VHole,...,ORet VHole, exn, EHole,...,EHole]

EHole or OHole?

I think the issue of implicit exceptions raised by "/" is a separate tricky thing. Probably this just needs a flag on TOp to record the case where all operands succeeded but the operation raised an exception

Agreed - started #52 to track this.

[jstolarek]

I've made a stab at this (and #52) on branch T47. I admit I've run out of steam for today, at least with coding, so my attempt was a bit chaotic. I added a flag to TOp that indicates whether operator raised an exception (so True if it raised, false if it executed successfully). That flag is used by isExn. When slicing TOp I took care to construct a list as described by @jamescheney.

The problem I reported originally in this issue now works. What doesn't work is the second of our ICFP examples and James' test case from 1st comment. I'm not sure how to proceed here.

Also, it seems to me that slicing w.r.t. raise (_:string) doesn't work simply because of that:

    (OExn VHole, _) | allStoreHoles ->
        return (bot, EHole, TSlicedHole (storeWrites trace) RetRaise)

[jamescheney]

Yes, we should remove that case if we want the implementation to match the "hybrid slicing" that we have been working on in the paper. We should also remove the first case:

    (OExn VHole, TRaise t) ->
        do (rho, e, t') <- bwdSliceM (OExn VStar) t
           return (rho, ERaise e, TRaise t')

which does not correspond to anything in the paper now.

[jstolarek]

I assume the plan is to have implementation of hybrid slicing before the deadline?

[jamescheney]

Yes, I will try to work on it (in a branch) tomorrow. It should not require major changes since we already added outcomes ret/raise/hole.

[jstolarek]

If this requires writing slicing rules that include OHole/OStar results, would it make sense to start off with my T47 branch? I'm not planning to touch the code tomorrow, just focus on writing and coming up with an interesting example to show in the paper.

[jamescheney]

I think T47 fixes #47 and #52 as is, though I haven't looked to see why the examples you mentioned don't work. So I would lean toward merging T47 as is (I had a look over the changes and it seems fine to me). I also think the changes to incorporate hybrid slicing are orthogonal enough that I could work on that independently without problems.

[jstolarek]

I'm reluctant to merge T47 in this state - not until I understand why this breaks other things (IMO much more important things - an example from our paper!). I suspect that more rules for OHole are required to make this work properly - the ones I wrote are ad-hoc.

[jamescheney]

The logic for slicing the subtraces of TOp doesn't deal correctly with the case TOp True ts (that is when the operation itself throws an exception, not a subtrace.) In that case, the current code is slicing all subtraces w.r.t. OHole because there is no exception subtrace. Changing the test "not (isExn trace)" to "not (any isExn ts)" seems to fix the problem, I've committed that (b195f2d).

[jstolarek]

Ah, of course. I think I was to tired yesterday to spot this. Sorry.

I'll wait with merging this branch until you finish with hybrid slicing.

[jamescheney]

I am just about to start, so I'll merge it now so that I ca start from that.

[jstolarek]

Sure, but please see my comment on the pull request