Skip to content

Counterexample proposal: cross-stage persistence #13

@yallop

Description

@yallop

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions