jstolarek / slicer

Companion code for paper "Imperative Functional Programs that Explain their Work", Wilmer Ricciotti, Jan Stolarek, Roly Perera and James Cheney, ICFP 2017, Oxford, UK
http://dl.acm.org/citation.cfm?id=3110258
GNU General Public License v3.0
6 stars 0 forks source link

Assignment slicing incorrect #43

Closed jamescheney closed 7 years ago

jamescheney commented 7 years ago
let t = trace (
    let a = ref 1 in
    let b = ref 1 in
    let c = ref 1 in
    b := !b + !a - !c;;
    !b) in
bwdSlice (t, 1)

In this example the slice retains initial values for a and c but not b, so there may be a bug in the slicing of assignments.

jamescheney commented 7 years ago

I think the code in the assignment case

                  do p <- storeDerefM l
                     (rho2, e2, t2') <- bwdSliceM p t2
                     (rho1, e1, t1') <- bwdSliceM (toValue l) t1
                     storeUpdateHoleM l

should be

                  do p <- storeDerefM l
                     storeUpdateHoleM l
                     (rho2, e2, t2') <- bwdSliceM p t2
                     (rho1, e1, t1') <- bwdSliceM (toValue l) t1

since the first version deletes any demand on l resulting from slicing the subtraces.

jstolarek commented 7 years ago

Yup, that was the cause. Fixed in references branch.