counterexamples icon indicating copy to clipboard operation
counterexamples copied to clipboard

Counterexample proposal: cross-stage persistence

Open yallop opened this issue 3 years ago • 0 comments

The following MetaOCaml code, distilled from

Generating code with polymorphic let a ballad of value restriction, copying and sharing Oleg Kiselyov

involves an unsound interaction between three MetaOCaml features:

  • polymorphic let
  • mutable references
  • cross-stage persistence
let lift x = .<x>.

let foo = Runcode.run
  .<let f () = .~(lift (ref None)) in
   f () := Some 2;
   match !(f ()) with Some x ->  x ^ "3" | None -> "" >.

Running it in (the latest versions of) BER MetaOCaml produces a segmentation fault.

yallop avatar Dec 27 '21 15:12 yallop