Incorrect detection of effect interference during extraction, part 2
use ref.Ref, mach.int.Int63 let f (x: ref (ref int63)): int63 = x.contents <- ref 3; 0 let g () = let y = ref 5 in f (ref y) + !y
is extracted to
let f (x: ((int) ref) ref) : int = begin let o = ref 3 in x.contents <- o; 0 end let g (_: unit) : int = let y = ref 5 in let o = f (ref y) in o + (!y)
So, the "read" effect of
!y has been inlined past the "reset" effect of
f (ref y). Contrarily to #200 (closed) , the obtained extracted code does not exhibit an unsoundness. But, if one were to model the C
free function using only a reset effect on the pointed zone (which is not the case currently, since resets are not available in the surface language), then it would presumably be possible to provoke a use-after-free bug.