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.