Storage mode analysis bug in ReML

[melsman]

The following program results in wrong output:

local
fun pr s = (print s; print "\n")

fun f `r (g: unit -> unit) : string`r =
    let val y : string `r = implode [#"H", #"i"]
    in g()
     ; y
    end

fun run () : unit =
  let with r
  in pr let val x : string`r = implode [#"H", #"e", #"j"]
        in f `[r] (fn () => pr x)
        end
  end
in
val () = run()
end

It prints Hi\nHi\n whereas it should print Hej\nHi\n.

The reason is that the compiled code stores the string Hi in region r with storage mode sat, which is a violation of the requirement $lrv(LV(R)) \cap \langle\rho\rangle = \emptyset$ in Rule (27) of [1]. Here we have $R = \mathtt{let} \mathtt{val} y : \mathtt{string`r} = [] \mathtt{in} g() ; y \mathtt{end}$ and $LV(R) = \{g\}$ and $lrv \{g\} = lrv(g) = \langle\epsilon_g\rangle \cap RegVar$. We also have $\epsilon_g \rightarrow \epsilon_{fn} \rightarrow \rho$ ($\rho$ = r) in the region flow graph $G$ .

Here is the intermediate code:

$ reml -Pcee -Paux -maximum_inline_size 0 -w 80 fun2.sml
[reading source file:	fun2.sml]
Program After Application Conversion: 
   let fun pr s = let val _ = print s in jmp print "\n" end; 
       fun f [`r:inf] g = 
           let val y = let region r31:inf in implode[sat `r] [0x48,0x69] attop r31 end; 
               val _ = g ()
           in  y
           end; 
       fun run () = 
           let region `r:inf
           in  pr 
               let val x = let region r53:inf in implode[atbot `r] [0x48,0x65,0x6a] attop r53 end; 
                   region r71:3
               in  f[atbot `r] (fn atbot r71 v102 => jmp pr x)
               end
           end; 
       val _ = run ()
   in  {||}
   end

Really, implode should be passed with attop r inside the function f.

Here is a Standard ML program that also fails to output the correct result:

local
fun pr s = (print s; print "\n")

fun f (g: unit -> unit) : string =
    let val y : string = implode [#"H", #"i"]
    in g()
     ; y
    end

fun run () : unit =
  pr let val x : string = implode [#"H", #"e", #"j"]
     in if false then x else f (fn () => pr x)
     end
in
val () = run()
end

Compile with

$ mlkit -no_gc -Pcee -Paux -maximum_inline_size 0 -debug_which_at -no_cfold -w 80 -o fun3.exe fun3.sml

[1] Birkedal, Tofte, Vejlstrup. From Region Inference to von Neumann Machines via Region Representation Inference. POPL '96.

[melsman]

The problem is that Effect.represents computes only EPS and PUT nodes.

[melsman]

Fixed by PR #209