Make dropping of values explicit

ml-proto/host/encode.ml

@@ -105,30 +105,32 @@ let encode m =
     let rec expr e =
       match e.it with
       | Nop -> op 0x00
-      | Block es -> op 0x01; list expr es; op 0x17
-      | Loop es -> op 0x02; list expr es; op 0x17
+      | Block es -> op 0x01; list expr es; op 0x0f
+      | Loop es -> op 0x02; list expr es; op 0x0f
       | If (e, es1, es2) ->
         expr e; op 0x03; list expr es1;
-        if es2 <> [] then op 0x04; list expr es2; op 0x17
+        if es2 <> [] then op 0x04; list expr es2; op 0x0f
       | Select (e1, e2, e3) -> expr e1; expr e2; expr e3; op 0x05
       | Br (x, eo) -> opt expr eo; op 0x06; arity1 eo; var x
       | Br_if (x, eo, e) -> opt expr eo; expr e; op 0x07; arity1 eo; var x
       | Br_table (xs, x, eo, e) ->
         opt expr eo; expr e; op 0x08; arity1 eo; vec var32 xs; var32 x
-
-      | Ast.I32_const c -> op 0x0a; vs32 c.it
-      | Ast.I64_const c -> op 0x0b; vs64 c.it
-      | Ast.F32_const c -> op 0x0c; f32 c.it
-      | Ast.F64_const c -> op 0x0d; f64 c.it
-
-      | Ast.Get_local x -> op 0x0e; var x
-      | Ast.Set_local (x, e) -> unary e 0x0f; var x
-
-      | Ast.Call (x, es) -> nary es 0x12; var x
-      | Ast.Call_import (x, es) -> nary es 0x1f; var x
-      | Ast.Call_indirect (x, e, es) -> expr e; nary es 0x13; var x
-      | Ast.Return eo -> nary1 eo 0x14
-      | Ast.Unreachable -> op 0x15
+      | Ast.Return eo -> nary1 eo 0x09
+      | Ast.Unreachable -> op 0x0a
+      | Ast.Drop e -> unary e 0x0b
+
+      | Ast.I32_const c -> op 0x10; vs32 c.it
+      | Ast.I64_const c -> op 0x11; vs64 c.it
+      | Ast.F32_const c -> op 0x12; f32 c.it
+      | Ast.F64_const c -> op 0x13; f64 c.it
+
+      | Ast.Get_local x -> op 0x14; var x
+      | Ast.Set_local (x, e) -> unary e 0x15; var x
+      | Ast.Tee_local (x, e) -> unary e 0x19; var x
+
+      | Ast.Call (x, es) -> nary es 0x16; var x
+      | Ast.Call_indirect (x, e, es) -> expr e; nary es 0x17; var x
+      | Ast.Call_import (x, es) -> nary es 0x18; var x
 
       | I32_load8_s (o, a, e) -> unary e 0x20; memop o a
       | I32_load8_u (o, a, e) -> unary e 0x21; memop o a

ml-proto/host/format.ml

@@ -195,6 +195,7 @@ let rec expr e =
     match e.it with
     | Nop -> "nop", []
     | Unreachable -> "unreachable", []
+    | Drop e -> "drop", [expr e]
     | Block ([], {it = Loop e; _}) -> "loop", [expr e]
     | Block (es, e) -> "block", list expr (es @ [e])
     | Loop e -> assert false
@@ -215,6 +216,7 @@ let rec expr e =
     | CallIndirect (x, e, es) -> "call_indirect " ^ var x, list expr (e::es)
     | GetLocal x -> "get_local " ^ var x, []
     | SetLocal (x, e) -> "set_local " ^ var x, [expr e]
+    | TeeLocal (x, e) -> "tee_local " ^ var x, [expr e]
     | Load (op, e) -> memop "load" op, [expr e]
     | Store (op, e1, e2) -> memop "store" op, [expr e1; expr e2]
     | LoadExtend (op, e) -> extop op, [expr e]

ml-proto/host/lexer.mll

@@ -142,6 +142,7 @@ rule token = parse
 
   | "nop" { NOP }
   | "unreachable" { UNREACHABLE }
+  | "drop" { DROP }
   | "block" { BLOCK }
   | "loop" { LOOP }
   | "br" { BR }
@@ -158,6 +159,7 @@ rule token = parse
 
   | "get_local" { GET_LOCAL }
   | "set_local" { SET_LOCAL }
+  | "tee_local" { TEE_LOCAL }
 
   | (nxx as t)".load"
     { LOAD (fun (o, a, e) ->
@@ -172,7 +174,7 @@ rule token = parse
                 (F32_store (o, (Lib.Option.get a 4), e1, e2))
                 (F64_store (o, (Lib.Option.get a 8), e1, e2))) }
   | (ixx as t)".load"(mem_size as sz)"_"(sign as s)
-    { if t = "i32" && sz = "32" then error lexbuf "unknown opcode";
+    { if t = "i32" && sz = "32" then error lexbuf "unknown operator";
       LOAD (fun (o, a, e) ->
         intop t
           (memsz sz
@@ -189,7 +191,7 @@ rule token = parse
             (ext s (I64_load32_s (o, (Lib.Option.get a 4), e))
                    (I64_load32_u (o, (Lib.Option.get a 4), e))))) }
   | (ixx as t)".store"(mem_size as sz)
-    { if t = "i32" && sz = "32" then error lexbuf "unknown opcode";
+    { if t = "i32" && sz = "32" then error lexbuf "unknown operator";
       STORE (fun (o, a, e1, e2) ->
         intop t
           (memsz sz
@@ -381,7 +383,7 @@ rule token = parse
   | space { token lexbuf }
   | '\n' { Lexing.new_line lexbuf; token lexbuf }
   | eof { EOF }
-  | _ { error lexbuf "unknown opcode" }
+  | _ { error lexbuf "unknown operator" }
 
 and comment start = parse
   | ";)" { () }

ml-proto/host/parser.mly

@@ -125,9 +125,9 @@ let implicit_decl c t at =
 %}
 
 %token NAT INT FLOAT TEXT VAR VALUE_TYPE LPAR RPAR
-%token NOP BLOCK IF THEN ELSE SELECT LOOP BR BR_IF BR_TABLE
+%token NOP DROP BLOCK IF THEN ELSE SELECT LOOP BR BR_IF BR_TABLE
 %token CALL CALL_IMPORT CALL_INDIRECT RETURN
-%token GET_LOCAL SET_LOCAL LOAD STORE OFFSET ALIGN
+%token GET_LOCAL SET_LOCAL TEE_LOCAL LOAD STORE OFFSET ALIGN
 %token CONST UNARY BINARY COMPARE CONVERT
 %token UNREACHABLE CURRENT_MEMORY GROW_MEMORY
 %token FUNC START TYPE PARAM RESULT LOCAL
@@ -231,6 +231,7 @@ expr :
 expr1 :
   | NOP { fun c -> Nop }
   | UNREACHABLE { fun c -> Unreachable }
+  | DROP expr { fun c -> Drop ($2 c) }
   | BLOCK labeling expr_list { fun c -> let c' = $2 c in Block ($3 c') }
   | LOOP labeling expr_list
     { fun c -> let c' = anon_label c in let c'' = $2 c' in Loop ($3 c'') }
@@ -260,6 +261,7 @@ expr1 :
     { fun c -> Call_indirect ($2 c type_, $3 c, $4 c) }
   | GET_LOCAL var { fun c -> Get_local ($2 c local) }
   | SET_LOCAL var expr { fun c -> Set_local ($2 c local, $3 c) }
+  | TEE_LOCAL var expr { fun c -> Tee_local ($2 c local, $3 c) }
   | LOAD offset align expr { fun c -> $1 ($2, $3, $4 c) }
   | STORE offset align expr expr { fun c -> $1 ($2, $3, $4 c, $5 c) }
   | CONST literal { fun c -> fst (literal $1 $2) }

ml-proto/spec/ast.ml

@@ -13,6 +13,7 @@ and expr' =
   (* Control *)
   | Nop
   | Unreachable
+  | Drop of expr
   | Block of expr list
   | Loop of expr list
   | Br of var * expr option
@@ -28,6 +29,7 @@ and expr' =
   (* Locals *)
   | Get_local of var
   | Set_local of var * expr
+  | Tee_local of var * expr
 
   (* Memory access *)
   | I32_load of Memory.offset * int * expr

ml-proto/spec/check.ml

@@ -14,14 +14,16 @@ let require b at s = if not b then error at s
 
 (* Context *)
 
+type expr_type_future = [`Known of expr_type | `SomeUnknown] ref
+
 type context =
 {
   types : func_type list;
   funcs : func_type list;
   imports : func_type list;
   locals : value_type list;
   return : expr_type;
-  labels : expr_type list;
+  labels : expr_type_future list;
   has_memory : bool
 }
 
@@ -36,12 +38,23 @@ let local c x = lookup "local" c.locals x
 let label c x = lookup "label" c.labels x
 
 
-(* Type comparison *)
+(* Type Unification *)
+
+let string_of_future = function
+  | `Known et -> string_of_expr_type et
+  | `SomeUnknown -> "<value_type>"
 
 let check_type actual expected at =
-  require (expected = None || actual = expected) at
+  if !expected = `SomeUnknown && actual <> None then expected := `Known actual;
+  require (!expected = `Known actual) at
     ("type mismatch: expression has type " ^ string_of_expr_type actual ^
-     " but the context requires " ^ string_of_expr_type expected)
+     " but the context requires " ^ string_of_future !expected)
+
+let some_unknown () = ref `SomeUnknown
+let known et = ref (`Known et)
+let none = known None
+let some t = known (Some t)
+let is_some et = !et <> `Known None
 
 
 (* Type Synthesis *)
@@ -99,15 +112,15 @@ let type_hostop = function
 (* Type Analysis *)
 
 (*
- * check_expr : context -> expr_type -> expr -> unit
+ * check_expr : context -> expr_type_future -> expr -> unit
  *
  * Conventions:
  *   c  : context
  *   e  : expr
  *   eo : expr option
  *   v  : value
  *   t  : value_type
- *   et : expr_type
+ *   et : expr_type_future
  *)
 
 let rec check_expr c et e =
@@ -118,37 +131,42 @@ let rec check_expr c et e =
   | Unreachable ->
     ()
 
+  | Drop e ->
+    check_expr c (some_unknown ()) e;
+    check_type None et e.at
+
   | Block (es, e) ->
     let c' = {c with labels = et :: c.labels} in
-    List.iter (check_expr c' None) es;
+    List.iter (check_expr c' none) es;
     check_expr c' et e
 
   | Loop e1 ->
-    let c' = {c with labels = None :: c.labels} in
+    let c' = {c with labels = none :: c.labels} in
     check_expr c' et e1
 
   | Break (x, eo) ->
     check_expr_opt c (label c x) eo e.at
 
   | BreakIf (x, eo, e1) ->
     check_expr_opt c (label c x) eo e.at;
-    check_expr c (Some Int32Type) e1;
+    check_expr c (some Int32Type) e1;
     check_type None et e.at
 
   | BreakTable (xs, x, eo, e1) ->
     List.iter (fun x -> check_expr_opt c (label c x) eo e.at) xs;
     check_expr_opt c (label c x) eo e.at;
-    check_expr c (Some Int32Type) e1
+    check_expr c (some Int32Type) e1
 
   | If (e1, e2, e3) ->
-    check_expr c (Some Int32Type) e1;
+    check_expr c (some Int32Type) e1;
     check_expr c et e2;
     check_expr c et e3
 
   | Select (e1, e2, e3) ->
+    require (is_some et) e.at "arity mismatch";
     check_expr c et e1;
     check_expr c et e2;
-    check_expr c (Some Int32Type) e3
+    check_expr c (some Int32Type) e3
 
   | Call (x, es) ->
     let {ins; out} = func c x in
@@ -162,17 +180,20 @@ let rec check_expr c et e =
 
   | CallIndirect (x, e1, es) ->
     let {ins; out} = type_ c.types x in
-    check_expr c (Some Int32Type) e1;
+    check_expr c (some Int32Type) e1;
     check_exprs c ins es e.at;
     check_type out et e.at
 
   | GetLocal x ->
     check_type (Some (local c x)) et e.at
 
   | SetLocal (x, e1) ->
-    let t = local c x in
-    check_expr c (Some t) e1;
-    check_type (Some t) et e.at
+    check_expr c (some (local c x)) e1;
+    check_type None et e.at
+
+  | TeeLocal (x, e1) ->
+    check_expr c (some (local c x)) e1;
+    check_type (Some (local c x)) et e.at
 
   | Load (memop, e1) ->
     check_load c et memop e1 e.at
@@ -193,29 +214,29 @@ let rec check_expr c et e =
 
   | Unary (unop, e1) ->
     let t = type_unop unop in
-    check_expr c (Some t) e1;
+    check_expr c (some t) e1;
     check_type (Some t) et e.at
 
   | Binary (binop, e1, e2) ->
     let t = type_binop binop in
-    check_expr c (Some t) e1;
-    check_expr c (Some t) e2;
+    check_expr c (some t) e1;
+    check_expr c (some t) e2;
     check_type (Some t) et e.at
 
   | Test (testop, e1) ->
     let t = type_testop testop in
-    check_expr c (Some t) e1;
+    check_expr c (some t) e1;
     check_type (Some Int32Type) et e.at
 
   | Compare (relop, e1, e2) ->
     let t = type_relop relop in
-    check_expr c (Some t) e1;
-    check_expr c (Some t) e2;
+    check_expr c (some t) e1;
+    check_expr c (some t) e2;
     check_type (Some Int32Type) et e.at
 
   | Convert (cvtop, e1) ->
     let t1, t = type_cvtop e.at cvtop in
-    check_expr c (Some t1) e1;
+    check_expr c (some t1) e1;
     check_type (Some t) et e.at
 
   | Host (hostop, es) ->
@@ -226,29 +247,30 @@ let rec check_expr c et e =
 
 and check_exprs c ts es at =
   require (List.length ts = List.length es) at "arity mismatch";
-  let ets = List.map (fun x -> Some x) ts in
+  let ets = List.map some ts in
   List.iter2 (check_expr c) ets es
 
 and check_expr_opt c et eo at =
-  match eo with
-  | Some e -> check_expr c et e
-  | None -> check_type None et at
+  match is_some et, eo with
+  | false, None -> ()
+  | true, Some e -> check_expr c et e
+  | _ -> error at "arity mismatch"
 
 and check_literal c et l =
   check_type (Some (type_value l.it)) et l.at
 
 and check_load c et memop e1 at =
   check_has_memory c at;
   check_memop memop at;
-  check_expr c (Some Int32Type) e1;
+  check_expr c (some Int32Type) e1;
   check_type (Some memop.ty) et at
 
 and check_store c et memop e1 e2 at =
   check_has_memory c at;
   check_memop memop at;
-  check_expr c (Some Int32Type) e1;
-  check_expr c (Some memop.ty) e2;
-  check_type (Some memop.ty) et at
+  check_expr c (some Int32Type) e1;
+  check_expr c (some memop.ty) e2;
+  check_type None et at
 
 and check_has_memory c at =
   require c.has_memory at "memory operators require a memory section"
@@ -280,7 +302,7 @@ let check_func c f =
   let {ftype; locals; body} = f.it in
   let s = type_ c.types ftype in
   let c' = {c with locals = s.ins @ locals; return = s.out} in
-  check_expr c' s.out body
+  check_expr c' (known s.out) body
 
 let check_elem c x =
   ignore (func c x)