search

FStarLang / pulse

The Pulse separation logic DSL for F*
Apache License 2.0
6 stars 7 forks source link

Pulse and `inline_for_extraction` #166

Closed mtzguido closed 1 month ago

mtzguido commented 3 months ago

This snippet crashes on extraction

open Pulse

inline_for_extraction noextract
```pulse
fn h ()
  requires emp
  returns  x : int
  ensures  emp
{
  42
}

let h2 = h

Giving:

$ ./pulse.sh --codegen OCaml PP.fst Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error. Failure("Impossible: Unexpected term: Tm_unknown")


This happens since `h` is really added to the environment with a `Tm_unknown` with some metadata attached to the sigelt, used by the pulse extraction for decls. Our plan is to attach the metadata to the `Tm_unknown` instead (exact shape TBD) and have F*'s extraction call Pulse's extraction whenever it reaches a tagged `Tm_unknown`