Extraction ignores preconditions

[gebner]

We like to pretend that stt is like Dv during extraction; but it is not: stt has extra preconditions that need to be satisfied. And just because an stt term is fully applied does not mean that these preconditions are met.

module DoubleFree
open Pulse
open Pulse.Lib.Box

let free (#a:Type0) (b:box a) (#v:erased a)
  : Dv (stt unit (pts_to b v) (fun _ -> emp)) =
  free b #v

let double_free (#a:Type0) (b:box a) (#v:erased a)
  : stt unit (pts_to b v) (fun _ -> emp) =
  hide_div fun () ->
  let _ = free b #v in
  free b #v

The file above extracts to ML code which would do a double free:

open Prims
let free : 'a . 'a Pulse_Lib_Box.box -> unit -> unit =
  fun b -> fun v -> Pulse_Lib_Box.free b ()
let double_free : 'a . 'a Pulse_Lib_Box.box -> unit -> unit =
  fun b ->
    fun v ->
      Pulse_Lib_Core.hide_div () () (fun uu___ -> free b (); free b ())

What's happening here is that during extraction any fully-applied stt function is extracted to a function call--even if it is not inside an bind_stt and even if the preconditions are not satisfied. The only saving grace is that hide_div is not implemented yet so the code above doesn't compile.

[gebner]

Another cool trick:

module DoubleFree2
open Pulse
open Pulse.Lib.Box
#lang-pulse

fn free' (#a: Type0) (b: box a) (#v: erased a)
  requires pts_to b v
  returns b:bool
  ensures emp
{
  free b;
  true
}

let double_free (#a:Type0) (b:box a) (#v:erased a)
  : unit -> stt bool (pts_to b v) (fun _ -> emp) =
  let f = free' b #v in
  let f = free' b #v in
  fun () -> f

This one successfully compiles to a working double-free:

open Prims
let free' b v = let uu___ = Pulse_Lib_Box.free b () in true
let double_free : 'a . 'a Pulse_Lib_Box.box -> unit -> unit -> Prims.bool =
  fun b ->
    fun v -> let f = free' b () in let f1 = free' b () in fun uu___ -> f1

Note that this requires the bool return type. It doesn't work with the unit-returning free, which is erased to ().