From b81c6cc5b6c6afb8e729e869c3ad7c96999f5995 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 26 Oct 2015 15:35:34 +0100 Subject: [PATCH 01/12] Implement tableswitch; add if_break --- ml-proto/README.md | 10 +++--- ml-proto/given/lib.ml | 7 ++++ ml-proto/given/lib.mli | 1 + ml-proto/host/lexer.mll | 8 +++-- ml-proto/host/parser.mly | 38 ++++++++++----------- ml-proto/spec/ast.ml | 47 +++++++++++++------------ ml-proto/spec/check.ml | 28 +++++++++------ ml-proto/spec/eval.ml | 26 +++++++------- ml-proto/spec/int.ml | 8 ++++- ml-proto/spec/sugar.ml | 17 +++++---- ml-proto/spec/sugar.mli | 6 ++-- ml-proto/test/labels.wast | 24 +++++++------ ml-proto/test/switch.wast | 72 ++++++++++++++++++++++++++++++++------- 13 files changed, 186 insertions(+), 106 deletions(-) diff --git a/ml-proto/README.md b/ml-proto/README.md index 9674c301ea..4fb94e1869 100644 --- a/ml-proto/README.md +++ b/ml-proto/README.md @@ -134,12 +134,12 @@ expr: ( block + ) ;; = (label (block +)) ( if ) ( if ) ;; = (if (nop)) + ( if_break ) ;; = (if (break ) (nop)) ( loop * ) ;; = (loop (block *)) ( loop ? * ) ;; = (label (loop (block ? *))) ( label ? ) ( break ? ) - ( .switch * ) - ( .switch * ) ;; = (label (.switch * )) + ( switch + ) ( call * ) ( call_import * ) ( call_indirect * ) @@ -158,8 +158,10 @@ expr: ( grow_memory ) case: - ( case * fallthrough? ) ;; = (case (block *) fallthrough?) - ( case ) ;; = (case (nop) fallthrough) + ( case * ) ;; = (case (block *)) + ( case_break ) ;; = (case (break )) + ( default * ) ;; = (default (block *)) + ( default_break ) ;; = (default (break )) func: ( func ? ? * ? * * ) type: ( type ) diff --git a/ml-proto/given/lib.ml b/ml-proto/given/lib.ml index c8b82e24cd..7414fe5928 100644 --- a/ml-proto/given/lib.ml +++ b/ml-proto/given/lib.ml @@ -50,6 +50,13 @@ struct let app f = function | Some x -> f x | None -> () + + let compare cmp_a o1 o2 = + match o1, o2 with + | None, None -> 0 + | None, Some _ -> -1 + | Some _, None -> 1 + | Some x1, Some x2 -> cmp_a x1 x2 end module Int = diff --git a/ml-proto/given/lib.mli b/ml-proto/given/lib.mli index 6818d46939..7a9e770f65 100644 --- a/ml-proto/given/lib.mli +++ b/ml-proto/given/lib.mli @@ -20,6 +20,7 @@ sig val get : 'a option -> 'a -> 'a val map : ('a -> 'b) -> 'a option -> 'b option val app : ('a -> unit) -> 'a option -> unit + val compare : ('a -> 'a -> int) -> 'a option -> 'a option -> int end module Int : diff --git a/ml-proto/host/lexer.mll b/ml-proto/host/lexer.mll index cf3ea9542e..3a83d6adda 100644 --- a/ml-proto/host/lexer.mll +++ b/ml-proto/host/lexer.mll @@ -137,13 +137,18 @@ rule token = parse | "loop" { LOOP } | "label" { LABEL } | "break" { BREAK } + | "switch" { SWITCH } | "case" { CASE } - | "fallthrough" { FALLTHROUGH } + | "default" { DEFAULT } | "call" { CALL } | "call_import" { CALL_IMPORT } | "call_indirect" { CALL_INDIRECT } | "return" { RETURN } + | "if_break" { IF_BREAK } + | "case_break" { CASE_BREAK } + | "default_break" { DEFAULT_BREAK } + | "get_local" { GET_LOCAL } | "set_local" { SET_LOCAL } @@ -158,7 +163,6 @@ rule token = parse | "offset="(digits as s) { OFFSET (Int64.of_string s) } | "align="(digits as s) { ALIGN (int_of_string s) } - | (nxx as t)".switch" { SWITCH (value_type t) } | (nxx as t)".const" { CONST (value_type t) } | (ixx as t)".clz" { UNARY (intop t Int32Op.Clz Int64Op.Clz) } diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index ef65c68700..3a5b9a6feb 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -44,6 +44,11 @@ let literal s t = | Failure reason -> Error.error s.at ("constant out of range: " ^ reason) | _ -> Error.error s.at "constant out of range" +let int32 s = + try I32.of_string s.it with + | Failure reason -> Error.error s.at ("constant out of range: " ^ reason) + | _ -> Error.error s.at "constant out of range" + (* Memory operands *) @@ -146,7 +151,8 @@ let implicit_decl c t at = %} %token INT FLOAT TEXT VAR VALUE_TYPE LPAR RPAR -%token NOP BLOCK IF LOOP LABEL BREAK SWITCH CASE FALLTHROUGH +%token NOP BLOCK IF LOOP LABEL BREAK SWITCH CASE DEFAULT +%token IF_BREAK CASE_BREAK DEFAULT_BREAK %token CALL CALL_IMPORT CALL_INDIRECT RETURN %token GET_LOCAL SET_LOCAL LOAD STORE LOAD_EXTEND STORE_WRAP OFFSET ALIGN %token CONST UNARY BINARY COMPARE CONVERT @@ -162,7 +168,6 @@ let implicit_decl c t at = %token VAR %token VALUE_TYPE %token CONST -%token SWITCH %token UNARY %token BINARY %token COMPARE @@ -241,6 +246,7 @@ expr1 : | BLOCK labeling expr expr_list { fun c -> let c', l = $2 c in block (l, $3 c' :: $4 c') } | IF expr expr expr_opt { fun c -> if_ ($2 c, $3 c, $4 c) } + | IF_BREAK expr var { fun c -> if_break ($2 c, $3 c label) } | LOOP labeling labeling expr_list { fun c -> let c', l1 = $2 c in let c'', l2 = $3 c' in loop (l1, l2, $4 c'') } @@ -252,9 +258,8 @@ expr1 : | RETURN expr_opt { let at1 = ati 1 in fun c -> return (label c ("return" @@ at1) @@ at1, $2 c) } - | SWITCH labeling expr cases - { fun c -> let c', l = $2 c in let cs, e = $4 c' in - switch (l, $1, $3 c', List.map (fun a -> a $1) cs, e) } + | SWITCH labeling expr case_list + { fun c -> let c', l = $2 c in switch (l, $3 c', $4 c') } | CALL var expr_list { fun c -> call ($2 c func, $3 c) } | CALL_IMPORT var expr_list { fun c -> call_import ($2 c import, $3 c) } | CALL_INDIRECT var expr expr_list @@ -288,23 +293,18 @@ expr_list : | expr expr_list { fun c -> $1 c :: $2 c } ; -fallthrough : - | /* empty */ { false } - | FALLTHROUGH { true } -; - case : - | LPAR case1 RPAR { let at = at () in fun c t -> $2 c t @@ at } + | LPAR case1 RPAR { let at = at () in fun c -> $2 c @@ at } ; case1 : - | CASE literal expr expr_list fallthrough - { fun c t -> case (literal $2 t, Some ($3 c :: $4 c, $5)) } - | CASE literal - { fun c t -> case (literal $2 t, None) } -; -cases : - | expr { fun c -> [], $1 c } - | case cases { fun c -> let x, y = $2 c in $1 c :: x, y } + | CASE literal expr_list { fun c -> case (Some (int32 $2), $3 c) } + | DEFAULT expr_list { fun c -> case (None, $2 c) } + | CASE_BREAK literal var { fun c -> case_break (Some (int32 $2), $3 c label) } + | DEFAULT_BREAK var { fun c -> case_break (None, $2 c label) } +; +case_list : + | case { fun c -> [$1 c] } + | case case_list { fun c -> $1 c :: $2 c } ; diff --git a/ml-proto/spec/ast.ml b/ml-proto/spec/ast.ml index 87edf3e52d..eb5c3caf22 100644 --- a/ml-proto/spec/ast.ml +++ b/ml-proto/spec/ast.ml @@ -79,35 +79,34 @@ type literal = value Source.phrase type expr = expr' Source.phrase and expr' = - | Nop (* do nothing *) - | Block of expr list (* execute in sequence *) - | If of expr * expr * expr (* conditional *) - | Loop of expr (* infinite loop *) - | Label of expr (* labelled expression *) - | Break of var * expr option (* break to n-th surrounding label *) - | Switch of value_type * expr * case list * expr (* switch, latter expr is default *) - | Call of var * expr list (* call function *) - | CallImport of var * expr list (* call imported function *) - | CallIndirect of var * expr * expr list (* call function through table *) - | GetLocal of var (* read local variable *) - | SetLocal of var * expr (* write local variable *) - | Load of memop * expr (* read memory at address *) - | Store of memop * expr * expr (* write memory at address *) - | LoadExtend of extop * expr (* read memory at address and extend *) - | StoreWrap of wrapop * expr * expr (* wrap and write to memory at address *) - | Const of literal (* constant *) - | Unary of unop * expr (* unary arithmetic operator *) - | Binary of binop * expr * expr (* binary arithmetic operator *) - | Compare of relop * expr * expr (* arithmetic comparison *) - | Convert of cvt * expr (* conversion *) - | Host of hostop * expr list (* host interaction *) + | Nop (* do nothing *) + | Block of expr list (* execute in sequence *) + | If of expr * expr * expr (* conditional *) + | Loop of expr (* infinite loop *) + | Label of expr (* labelled expression *) + | Break of var * expr option (* break to n-th surrounding label *) + | Switch of expr * case list (* table switch *) + | Call of var * expr list (* call function *) + | CallImport of var * expr list (* call imported function *) + | CallIndirect of var * expr * expr list (* call function through table *) + | GetLocal of var (* read local variable *) + | SetLocal of var * expr (* write local variable *) + | Load of memop * expr (* read memory at address *) + | Store of memop * expr * expr (* write memory at address *) + | LoadExtend of extop * expr (* read memory at address and extend *) + | StoreWrap of wrapop * expr * expr (* wrap and write to memory at address *) + | Const of literal (* constant *) + | Unary of unop * expr (* unary arithmetic operator *) + | Binary of binop * expr * expr (* binary arithmetic operator *) + | Compare of relop * expr * expr (* arithmetic comparison *) + | Convert of cvt * expr (* conversion *) + | Host of hostop * expr list (* host interaction *) and case = case' Source.phrase and case' = { - value : literal; + value : I32.t option; expr : expr; - fallthru : bool } diff --git a/ml-proto/spec/check.ml b/ml-proto/spec/check.ml index 019c11d1de..5c9dbef33a 100644 --- a/ml-proto/spec/check.ml +++ b/ml-proto/spec/check.ml @@ -36,6 +36,12 @@ let import c x = lookup "import" c.imports x let local c x = lookup "local" c.locals x let label c x = lookup "label" c.labels x +module CaseSet = Set.Make( + struct + type t = I32.t option + let compare = Lib.Option.compare I32.compare_u + end) + (* Type comparison *) @@ -138,12 +144,13 @@ let rec check_expr c et e = | Break (x, eo) -> check_expr_opt c (label c x) eo e.at - | Switch (t, e1, cs, e2) -> - require (t = Int32Type || t = Int64Type) e.at "invalid switch type"; - (* TODO: Check that cases are unique. *) - check_expr c (Some t) e1; - List.iter (check_case c t et) cs; - check_expr c et e2 + | Switch (e1, cs) -> + check_expr c (Some Int32Type) e1; + let cc, _ = List.fold_right (check_case c) cs (CaseSet.empty, et) in + let max = CaseSet.max_elt cc in + require (CaseSet.mem None cc) e.at "switch is missing default case"; + require (max = None || max = Some (I32.of_int (CaseSet.cardinal cc - 2))) + e.at "switch is not dense" | Call (x, es) -> let {ins; out} = func c x in @@ -228,10 +235,11 @@ and check_expr_opt c et eo at = and check_literal c et l = check_type (Some (type_value l.it)) et l.at -and check_case c t et case = - let {value = l; expr = e; fallthru} = case.it in - check_literal c (Some t) l; - check_expr c (if fallthru then None else et) e +and check_case c case (cc, et) = + let {value = l; expr = e} = case.it in + require (not (CaseSet.mem l cc)) case.at "duplicate case"; + check_expr c et e; + (CaseSet.add l cc, None) and check_load c et memop e1 at = check_has_memory c at; diff --git a/ml-proto/spec/eval.ml b/ml-proto/spec/eval.ml index 72a6cdd7bc..21dbd448a4 100644 --- a/ml-proto/spec/eval.ml +++ b/ml-proto/spec/eval.ml @@ -160,11 +160,15 @@ let rec eval_expr (c : config) (e : expr) = | Break (x, eo) -> raise (label c x (eval_expr_opt c eo)) - | Switch (_t, e1, cs, e2) -> - let vo = some (eval_expr c e1) e1.at in - (match List.fold_left (eval_case c vo) `Seek cs with - | `Seek | `Fallthru -> eval_expr c e2 - | `Done vs -> vs + | Switch (e1, cs) -> + let i = int32 (eval_expr c e1) e1.at in + let l = + if List.length cs = 1 || I32.gt_u i (I32.of_int (List.length cs - 2)) + then None else Some i + in + (match List.fold_left (eval_case c l) `Seek cs with + | `Seek -> error e.at "runtime crash: switch failed" + | `Found vo -> vo ) | Call (x, es) -> @@ -263,15 +267,9 @@ and eval_expr_opt c = function | Some e -> eval_expr c e | None -> None -and eval_case c vo stage case = - let {value; expr = e; fallthru} = case.it in - match stage, vo = value.it with - | `Seek, true | `Fallthru, _ -> - if fallthru - then (ignore (eval_expr c e); `Fallthru) - else `Done (eval_expr c e) - | `Seek, false | `Done _, _ -> - stage +and eval_case c l phase case = + let {value; expr = e} = case.it in + if phase = `Seek && l <> value then `Seek else `Found (eval_expr c e) and eval_func instance f vs = let args = List.map ref vs in diff --git a/ml-proto/spec/int.ml b/ml-proto/spec/int.ml index 3618d48f3f..7fbac65c4c 100644 --- a/ml-proto/spec/int.ml +++ b/ml-proto/spec/int.ml @@ -24,7 +24,7 @@ sig val of_string : string -> t val to_string : t -> string - val bitwidth : int + val bitwidth : int end module type S = @@ -64,6 +64,9 @@ sig val ge_s : t -> t -> bool val ge_u : t -> t -> bool + val compare_s : t -> t -> int + val compare_u : t -> t -> int + val of_int : int -> t val of_string : string -> t val to_string : t -> string @@ -194,4 +197,7 @@ struct let to_string = Rep.to_string let of_int = Rep.of_int + + let compare_s = compare + let compare_u x y = compare (Rep.add x Rep.min_int) (Rep.add y Rep.min_int) end diff --git a/ml-proto/spec/sugar.ml b/ml-proto/spec/sugar.ml index 9d97846024..748836826e 100644 --- a/ml-proto/spec/sugar.ml +++ b/ml-proto/spec/sugar.ml @@ -27,6 +27,9 @@ let if_ (e1, e2, eo) = let e3 = Lib.Option.get eo (Nop @@ Source.after e2.at) in If (e1, e2, e3) +let if_break (e, x) = + if_ (e, Break (x, None) @@ x.at, None) + let loop (l1, l2, es) = let e = expr_seq es in labeling l1 (Loop (labeling l2 e.it @@ e.at)) @@ -40,8 +43,8 @@ let break (x, e) = let return (x, eo) = Break (x, eo) -let switch (l, t, e1, cs, e2) = - labeling l (Switch (t, e1, cs, e2)) +let switch (l, e, cs) = + labeling l (Switch (e, cs)) let call (x, es) = Call (x, es) @@ -88,10 +91,12 @@ let convert (cvt, e) = let host (hostop, es) = Host (hostop, es) -let case (c, br) = - match br with - | Some (es, fallthru) -> {value = c; expr = expr_seq es; fallthru} - | None -> {value = c; expr = Nop @@ Source.after c.at; fallthru = true} + +let case (c, es) = + {value = c; expr = expr_seq es} + +let case_break (c, x) = + {value = c; expr = Break (x, None) @@ x.at} let func_body es = diff --git a/ml-proto/spec/sugar.mli b/ml-proto/spec/sugar.mli index 6e82ee8840..5880572696 100644 --- a/ml-proto/spec/sugar.mli +++ b/ml-proto/spec/sugar.mli @@ -6,11 +6,12 @@ and labeling' = Unlabelled | Labelled val nop : expr' val block : labeling * expr list -> expr' val if_ : expr * expr * expr option -> expr' +val if_break : expr * var -> expr' val loop : labeling * labeling * expr list -> expr' val label : expr -> expr' val break : var * expr option -> expr' val return : var * expr option -> expr' -val switch : labeling * value_type * expr * case list * expr -> expr' +val switch : labeling * expr * case list -> expr' val call : var * expr list -> expr' val call_import : var * expr list -> expr' val call_indirect : var * expr * expr list -> expr' @@ -27,6 +28,7 @@ val compare : relop * expr * expr -> expr' val convert : cvt * expr -> expr' val host : hostop * expr list -> expr' -val case : literal * (expr list * bool) option -> case' +val case : I32.t option * expr list -> case' +val case_break : I32.t option * var -> case' val func_body : expr list -> expr' diff --git a/ml-proto/test/labels.wast b/ml-proto/test/labels.wast index e4ca34d9c2..ac709fe335 100644 --- a/ml-proto/test/labels.wast +++ b/ml-proto/test/labels.wast @@ -35,21 +35,22 @@ (func $switch (param i32) (result i32) (label $ret (i32.mul (i32.const 10) - (i32.switch $exit (get_local 0) + (switch $exit (get_local 0) (case 1 (i32.const 1)) (case 2 (break $exit (i32.const 2))) (case 3 (break $ret (i32.const 3))) - (i32.const 4) + (default (i32.const 4)) + (case 0 (i32.const 5)) ) ) ) ) (func $return (param i32) (result i32) - (i32.switch (get_local 0) - (case 1 (return (i32.const 1))) - (case 2 (i32.const 2)) - (i32.const 3) + (switch (get_local 0) + (case 0 (return (i32.const 0))) + (case 1 (i32.const 1)) + (default (i32.const 2)) ) ) @@ -63,12 +64,13 @@ (assert_return (invoke "block") (i32.const 1)) (assert_return (invoke "loop1") (i32.const 5)) (assert_return (invoke "loop2") (i32.const 8)) -(assert_return (invoke "switch" (i32.const 1)) (i32.const 10)) +(assert_return (invoke "switch" (i32.const 0)) (i32.const 50)) +(assert_return (invoke "switch" (i32.const 1)) (i32.const 20)) (assert_return (invoke "switch" (i32.const 2)) (i32.const 20)) (assert_return (invoke "switch" (i32.const 3)) (i32.const 3)) -(assert_return (invoke "switch" (i32.const 4)) (i32.const 40)) -(assert_return (invoke "switch" (i32.const 5)) (i32.const 40)) -(assert_return (invoke "return" (i32.const 1)) (i32.const 1)) +(assert_return (invoke "switch" (i32.const 4)) (i32.const 50)) +(assert_return (invoke "switch" (i32.const 5)) (i32.const 50)) +(assert_return (invoke "return" (i32.const 0)) (i32.const 0)) +(assert_return (invoke "return" (i32.const 1)) (i32.const 2)) (assert_return (invoke "return" (i32.const 2)) (i32.const 2)) -(assert_return (invoke "return" (i32.const 3)) (i32.const 3)) diff --git a/ml-proto/test/switch.wast b/ml-proto/test/switch.wast index 9a13fec3b5..9deaece9ef 100644 --- a/ml-proto/test/switch.wast +++ b/ml-proto/test/switch.wast @@ -6,15 +6,16 @@ (local $j i32) (set_local $j (i32.const 100)) (label - (i32.switch (get_local $i) + (switch (get_local $i) (case 0 (return (get_local $i))) - (case 1 (nop) fallthrough) - (case 2) ;; implicit fallthrough + (case 1 (nop)) ;; fallthrough + (case 2) ;; fallthrough (case 3 (set_local $j (i32.sub (i32.const 0) (get_local $i))) (break 0)) (case 4 (break 0)) - (case 5 (set_local $j (i32.const 101))) - (case 6 (set_local $j (i32.const 101)) fallthrough) - (;default;) (set_local $j (i32.const 102)) + (case 5 (break 0 (set_local $j (i32.const 101)))) + (case 6 (set_local $j (i32.const 101))) ;; fallthrough + (default (set_local $j (i32.const 102))) + (case 7) ) ) (return (get_local $j)) @@ -26,20 +27,55 @@ (set_local $j (i64.const 100)) (return (label $l - (i64.switch (get_local $i) + (switch (i32.wrap/i64 (get_local $i)) (case 0 (return (get_local $i))) - (case 1 (nop) fallthrough) - (case 2) ;; implicit fallthrough + (case 1 (nop)) ;; fallthrough + (case 2) ;; fallthrough (case 3 (break $l (i64.sub (i64.const 0) (get_local $i)))) - (case 6 (set_local $j (i64.const 101)) fallthrough) - (;default;) (get_local $j) + (case 6 (set_local $j (i64.const 101))) ;; fallthrough + (case 4) ;; fallthrough + (case 5) ;; fallthrough + (default (break $l (get_local $j))) + (case 7 (i64.const -5)) ) ) ) ) + ;; Corner cases + (func $corner (result i32) + (local $x i32) + (switch (i32.const 0) + (default) + ) + (switch (i32.const 0) + (default (set_local $x (i32.add (get_local $x) (i32.const 1)))) + ) + (switch (i32.const 1) + (default (set_local $x (i32.add (get_local $x) (i32.const 2)))) + (case 0 (set_local $x (i32.add (get_local $x) (i32.const 4)))) + ) + (get_local $x) + ) + + ;; Break + (func $break (result i32) + (local $x i32) + (switch $l (i32.const 0) + (case_break 0 $l) + (default (set_local $x (i32.add (get_local $x) (i32.const 1)))) + ) + (switch $l (i32.const 1) + (default_break $l) + (case 0 (set_local $x (i32.add (get_local $x) (i32.const 2)))) + ) + (get_local $x) + ) + (export "stmt" $stmt) (export "expr" $expr) + (export "corner" $corner) + (export "break" $break) ) (assert_return (invoke "stmt" (i32.const 0)) (i32.const 0)) @@ -49,7 +85,7 @@ (assert_return (invoke "stmt" (i32.const 4)) (i32.const 100)) (assert_return (invoke "stmt" (i32.const 5)) (i32.const 101)) (assert_return (invoke "stmt" (i32.const 6)) (i32.const 102)) -(assert_return (invoke "stmt" (i32.const 7)) (i32.const 102)) +(assert_return (invoke "stmt" (i32.const 7)) (i32.const 100)) (assert_return (invoke "stmt" (i32.const -10)) (i32.const 102)) (assert_return (invoke "expr" (i64.const 0)) (i64.const 0)) @@ -57,5 +93,15 @@ (assert_return (invoke "expr" (i64.const 2)) (i64.const -2)) (assert_return (invoke "expr" (i64.const 3)) (i64.const -3)) (assert_return (invoke "expr" (i64.const 6)) (i64.const 101)) -(assert_return (invoke "expr" (i64.const 7)) (i64.const 100)) +(assert_return (invoke "expr" (i64.const 7)) (i64.const -5)) (assert_return (invoke "expr" (i64.const -10)) (i64.const 100)) + +(assert_return (invoke "corner") (i32.const 7)) +(assert_return (invoke "break") (i32.const 0)) + +(assert_invalid (module (func (switch (i32.const 0) (case 0)))) "switch is missing default case") +(assert_invalid (module (func (switch (i32.const 0) (default) (case 1)))) "switch is not dense") +(assert_invalid (module (func (switch (i32.const 0) (default) (case 0) (case 3)))) "switch is not dense") +(assert_invalid (module (func (switch (i32.const 0) (default) (case 0) (default)))) "duplicate case") +(assert_invalid (module (func (switch (i32.const 0) (case 0) (default) (case 0)))) "duplicate case") + From 4849bfb4be59acd6b67e52b76b0e86c535dcbdef Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 26 Oct 2015 15:48:43 +0100 Subject: [PATCH 02/12] Oversight in README --- ml-proto/README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/ml-proto/README.md b/ml-proto/README.md index 4fb94e1869..7e5800f994 100644 --- a/ml-proto/README.md +++ b/ml-proto/README.md @@ -140,6 +140,7 @@ expr: ( label ? ) ( break ? ) ( switch + ) + ( switch ? + ) ;; = (label (switch +)) ( call * ) ( call_import * ) ( call_indirect * ) From c84c23086e7698eacf31b93eafeab21d5ce192f8 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 26 Oct 2015 15:49:24 +0100 Subject: [PATCH 03/12] Typo --- ml-proto/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ml-proto/README.md b/ml-proto/README.md index 7e5800f994..e64f6bb95c 100644 --- a/ml-proto/README.md +++ b/ml-proto/README.md @@ -140,7 +140,7 @@ expr: ( label ? ) ( break ? ) ( switch + ) - ( switch ? + ) ;; = (label (switch +)) + ( switch + ) ;; = (label (switch +)) ( call * ) ( call_import * ) ( call_indirect * ) From 443692201b00d7b6392114167792bd84ca20d33a Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 28 Oct 2015 16:01:20 +0100 Subject: [PATCH 04/12] Rename break & switch to br and tableswitch --- ml-proto/README.md | 31 ++++++++------------------ ml-proto/host/lexer.mll | 10 ++++----- ml-proto/host/parser.mly | 13 ++++++----- ml-proto/spec/ast.ml | 2 +- ml-proto/spec/check.ml | 2 +- ml-proto/spec/eval.ml | 2 +- ml-proto/spec/sugar.ml | 14 ++++++------ ml-proto/spec/sugar.mli | 6 ++--- ml-proto/test/fac.wast | 4 ++-- ml-proto/test/labels.wast | 16 +++++++------- ml-proto/test/memory.wast | 4 ++-- ml-proto/test/switch.wast | 46 +++++++++++++++++++-------------------- 12 files changed, 69 insertions(+), 81 deletions(-) diff --git a/ml-proto/README.md b/ml-proto/README.md index e64f6bb95c..eb8eb1fd6b 100644 --- a/ml-proto/README.md +++ b/ml-proto/README.md @@ -82,24 +82,11 @@ Note however that the REPL currently is too dumb to allow multi-line input. :) See `wasm -h` for (the few) options. -## Language - -For most part, the language understood by the interpreter is based on Ben's V8 prototype, but I took the liberty to try out a few simplifications and generalisations: - -* *Expression Language.* There is no distinction between statements and expressions, everything is an expression. Some have an empty return type. Consequently, there is no need for a comma operator or ternary operator. - -* *Simple Loops*. Like in Ben's prototype, there is only one sort of loop, the infinite one, which can only be terminated by an explicit `break`. In such a language, a `continue` statement actually is completely redundant, because it equivalent to a `break` to a label on the loop's *body*. So I dropped `continue`. - -* *Break with Arguments.* In the spirit of a true expression language, `break` can carry arguments, which then become the result of the labelled expression it cuts to. - -* *Switch with Explicit Fallthru*. By default, a switch arm is well-behaved in that it does *not* fall through to the next case. However, it can be marked as fallthru explicitly. - - ## Core Language vs External Language The implementation tries to separate the concern of what is the language (and its semantics) from what is its external encoding. In that spirit, the actual AST is regular and minimal, while certain abbreviations are considered "syntactic sugar" of an external representation optimised for compactness. -For example, `if` always has an else-branch in the AST, but in the external format an else-less conditional is allowed as an abbreviation for one with `nop`. Similarly, blocks can sometimes be left implicit in sub-expressions. Furthermore, fallthru is a flag on each `switch` arm in the AST, but an explicit "opcode" in the external form. +For example, `if` always has an else-branch in the AST, but in the external format an else-less conditional is allowed as an abbreviation for one with `nop`. Similarly, blocks can sometimes be left implicit in sub-expressions. Here, the external format is S-expressions, but similar considerations would apply to a binary encoding. That is, there would be codes for certain abbreviations, but these are just a matter of the encoding. @@ -134,17 +121,17 @@ expr: ( block + ) ;; = (label (block +)) ( if ) ( if ) ;; = (if (nop)) - ( if_break ) ;; = (if (break ) (nop)) + ( if_br ) ;; = (if (br ) (nop)) ( loop * ) ;; = (loop (block *)) ( loop ? * ) ;; = (label (loop (block ? *))) ( label ? ) - ( break ? ) - ( switch + ) - ( switch + ) ;; = (label (switch +)) + ( br ? ) + ( tableswitch + ) + ( tableswitch + ) ;; = (label (tableswitch +)) ( call * ) ( call_import * ) ( call_indirect * ) - ( return ? ) ;; = (break ?) + ( return ? ) ;; = (br ?) ( get_local ) ( set_local ) ( .load((8|16)_)? ? ? ) @@ -160,9 +147,9 @@ expr: case: ( case * ) ;; = (case (block *)) - ( case_break ) ;; = (case (break )) + ( case_br ) ;; = (case (br )) ( default * ) ;; = (default (block *)) - ( default_break ) ;; = (default (break )) + ( default_br ) ;; = (default (br )) func: ( func ? ? * ? * * ) type: ( type ) @@ -228,7 +215,7 @@ The implementation consists of the following parts: * *Validator* (`check.ml[i]`). Does a recursive walk of the AST, passing down the *expected* type for expressions (or rather, a list thereof, because of multi-values), and checking each expression against that. An expected empty list of types can be matched by any result, corresponding to implicit dropping of unused values (e.g. in a block). -* *Evaluator* (`eval.ml[i]`, `values.ml`, `arithmetic.ml[i]`, `memory.ml[i]`). Evaluation of control transfer (`break` and `return`) is implemented using local exceptions as "labels". While these are allocated dynamically in the code and addressed via a stack, that is merely to simplify the code. In reality, these would be static jumps. +* *Evaluator* (`eval.ml[i]`, `values.ml`, `arithmetic.ml[i]`, `memory.ml[i]`). Evaluation of control transfer (`br` and `return`) is implemented using local exceptions as "labels". While these are allocated dynamically in the code and addressed via a stack, that is merely to simplify the code. In reality, these would be static jumps. * *Driver* (`main.ml`, `script.ml[i]`, `error.ml`, `print.ml[i]`, `flags.ml`). Executes scripts, reports results or errors, etc. diff --git a/ml-proto/host/lexer.mll b/ml-proto/host/lexer.mll index 3a83d6adda..86305f52d5 100644 --- a/ml-proto/host/lexer.mll +++ b/ml-proto/host/lexer.mll @@ -136,8 +136,8 @@ rule token = parse | "if" { IF } | "loop" { LOOP } | "label" { LABEL } - | "break" { BREAK } - | "switch" { SWITCH } + | "br" { BRANCH } + | "tableswitch" { SWITCH } | "case" { CASE } | "default" { DEFAULT } | "call" { CALL } @@ -145,9 +145,9 @@ rule token = parse | "call_indirect" { CALL_INDIRECT } | "return" { RETURN } - | "if_break" { IF_BREAK } - | "case_break" { CASE_BREAK } - | "default_break" { DEFAULT_BREAK } + | "if_br" { IF_BRANCH } + | "case_br" { CASE_BRANCH } + | "default_br" { DEFAULT_BRANCH } | "get_local" { GET_LOCAL } | "set_local" { SET_LOCAL } diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index 3a5b9a6feb..cc5c3e9ca4 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -151,8 +151,8 @@ let implicit_decl c t at = %} %token INT FLOAT TEXT VAR VALUE_TYPE LPAR RPAR -%token NOP BLOCK IF LOOP LABEL BREAK SWITCH CASE DEFAULT -%token IF_BREAK CASE_BREAK DEFAULT_BREAK +%token NOP BLOCK IF LOOP LABEL BRANCH SWITCH CASE DEFAULT +%token IF_BRANCH CASE_BRANCH DEFAULT_BRANCH %token CALL CALL_IMPORT CALL_INDIRECT RETURN %token GET_LOCAL SET_LOCAL LOAD STORE LOAD_EXTEND STORE_WRAP OFFSET ALIGN %token CONST UNARY BINARY COMPARE CONVERT @@ -246,7 +246,7 @@ expr1 : | BLOCK labeling expr expr_list { fun c -> let c', l = $2 c in block (l, $3 c' :: $4 c') } | IF expr expr expr_opt { fun c -> if_ ($2 c, $3 c, $4 c) } - | IF_BREAK expr var { fun c -> if_break ($2 c, $3 c label) } + | IF_BRANCH expr var { fun c -> if_branch ($2 c, $3 c label) } | LOOP labeling labeling expr_list { fun c -> let c', l1 = $2 c in let c'', l2 = $3 c' in loop (l1, l2, $4 c'') } @@ -254,7 +254,7 @@ expr1 : { fun c -> let c', l = $2 c in let c'' = if l.it = Unlabelled then anon_label c' else c' in Sugar.label ($3 c'') } - | BREAK var expr_opt { fun c -> break ($2 c label, $3 c) } + | BRANCH var expr_opt { fun c -> branch ($2 c label, $3 c) } | RETURN expr_opt { let at1 = ati 1 in fun c -> return (label c ("return" @@ at1) @@ at1, $2 c) } @@ -299,8 +299,9 @@ case : case1 : | CASE literal expr_list { fun c -> case (Some (int32 $2), $3 c) } | DEFAULT expr_list { fun c -> case (None, $2 c) } - | CASE_BREAK literal var { fun c -> case_break (Some (int32 $2), $3 c label) } - | DEFAULT_BREAK var { fun c -> case_break (None, $2 c label) } + | CASE_BRANCH literal var + { fun c -> case_branch (Some (int32 $2), $3 c label) } + | DEFAULT_BRANCH var { fun c -> case_branch (None, $2 c label) } ; case_list : | case { fun c -> [$1 c] } diff --git a/ml-proto/spec/ast.ml b/ml-proto/spec/ast.ml index eb5c3caf22..178441f9d1 100644 --- a/ml-proto/spec/ast.ml +++ b/ml-proto/spec/ast.ml @@ -84,7 +84,7 @@ and expr' = | If of expr * expr * expr (* conditional *) | Loop of expr (* infinite loop *) | Label of expr (* labelled expression *) - | Break of var * expr option (* break to n-th surrounding label *) + | Branch of var * expr option (* branch to n-th surrounding label *) | Switch of expr * case list (* table switch *) | Call of var * expr list (* call function *) | CallImport of var * expr list (* call imported function *) diff --git a/ml-proto/spec/check.ml b/ml-proto/spec/check.ml index 5c9dbef33a..13fc2e71f6 100644 --- a/ml-proto/spec/check.ml +++ b/ml-proto/spec/check.ml @@ -141,7 +141,7 @@ let rec check_expr c et e = let c' = {c with labels = et :: c.labels} in check_expr c' et e1 - | Break (x, eo) -> + | Branch (x, eo) -> check_expr_opt c (label c x) eo e.at | Switch (e1, cs) -> diff --git a/ml-proto/spec/eval.ml b/ml-proto/spec/eval.ml index 21dbd448a4..e71e352b73 100644 --- a/ml-proto/spec/eval.ml +++ b/ml-proto/spec/eval.ml @@ -157,7 +157,7 @@ let rec eval_expr (c : config) (e : expr) = let c' = {c with labels = L.label :: c.labels} in (try eval_expr c' e1 with L.Label vo -> vo) - | Break (x, eo) -> + | Branch (x, eo) -> raise (label c x (eval_expr_opt c eo)) | Switch (e1, cs) -> diff --git a/ml-proto/spec/sugar.ml b/ml-proto/spec/sugar.ml index 748836826e..ae4ce01168 100644 --- a/ml-proto/spec/sugar.ml +++ b/ml-proto/spec/sugar.ml @@ -27,8 +27,8 @@ let if_ (e1, e2, eo) = let e3 = Lib.Option.get eo (Nop @@ Source.after e2.at) in If (e1, e2, e3) -let if_break (e, x) = - if_ (e, Break (x, None) @@ x.at, None) +let if_branch (e, x) = + if_ (e, Branch (x, None) @@ x.at, None) let loop (l1, l2, es) = let e = expr_seq es in @@ -37,11 +37,11 @@ let loop (l1, l2, es) = let label e = Label e -let break (x, e) = - Break (x, e) +let branch (x, e) = + Branch (x, e) let return (x, eo) = - Break (x, eo) + Branch (x, eo) let switch (l, e, cs) = labeling l (Switch (e, cs)) @@ -95,8 +95,8 @@ let host (hostop, es) = let case (c, es) = {value = c; expr = expr_seq es} -let case_break (c, x) = - {value = c; expr = Break (x, None) @@ x.at} +let case_branch (c, x) = + {value = c; expr = Branch (x, None) @@ x.at} let func_body es = diff --git a/ml-proto/spec/sugar.mli b/ml-proto/spec/sugar.mli index 5880572696..998b1b1059 100644 --- a/ml-proto/spec/sugar.mli +++ b/ml-proto/spec/sugar.mli @@ -6,10 +6,10 @@ and labeling' = Unlabelled | Labelled val nop : expr' val block : labeling * expr list -> expr' val if_ : expr * expr * expr option -> expr' -val if_break : expr * var -> expr' +val if_branch : expr * var -> expr' val loop : labeling * labeling * expr list -> expr' val label : expr -> expr' -val break : var * expr option -> expr' +val branch : var * expr option -> expr' val return : var * expr option -> expr' val switch : labeling * expr * case list -> expr' val call : var * expr list -> expr' @@ -29,6 +29,6 @@ val convert : cvt * expr -> expr' val host : hostop * expr list -> expr' val case : I32.t option * expr list -> case' -val case_break : I32.t option * var -> case' +val case_branch : I32.t option * var -> case' val func_body : expr list -> expr' diff --git a/ml-proto/test/fac.wast b/ml-proto/test/fac.wast index cca812f94a..187c516ffc 100644 --- a/ml-proto/test/fac.wast +++ b/ml-proto/test/fac.wast @@ -29,7 +29,7 @@ (loop (if (i64.eq (get_local 1) (i64.const 0)) - (break 0) + (br 0) (block (set_local 2 (i64.mul (get_local 1) (get_local 2))) (set_local 1 (i64.sub (get_local 1) (i64.const 1))) @@ -50,7 +50,7 @@ (loop (if (i64.eq (get_local $i) (i64.const 0)) - (break $done) + (br $done) (block (set_local $res (i64.mul (get_local $i) (get_local $res))) (set_local $i (i64.sub (get_local $i) (i64.const 1))) diff --git a/ml-proto/test/labels.wast b/ml-proto/test/labels.wast index ac709fe335..b59090613f 100644 --- a/ml-proto/test/labels.wast +++ b/ml-proto/test/labels.wast @@ -1,7 +1,7 @@ (module (func $block (result i32) (block $exit - (break $exit (i32.const 1)) + (br $exit (i32.const 1)) (i32.const 0) ) ) @@ -12,7 +12,7 @@ (loop $exit (set_local $i (i32.add (get_local $i) (i32.const 1))) (if (i32.eq (get_local $i) (i32.const 5)) - (break $exit (get_local $i)) + (br $exit (get_local $i)) ) ) ) @@ -23,10 +23,10 @@ (loop $exit $cont (set_local $i (i32.add (get_local $i) (i32.const 1))) (if (i32.eq (get_local $i) (i32.const 5)) - (break $cont (i32.const -1)) + (br $cont (i32.const -1)) ) (if (i32.eq (get_local $i) (i32.const 8)) - (break $exit (get_local $i)) + (br $exit (get_local $i)) ) (set_local $i (i32.add (get_local $i) (i32.const 1))) ) @@ -35,10 +35,10 @@ (func $switch (param i32) (result i32) (label $ret (i32.mul (i32.const 10) - (switch $exit (get_local 0) + (tableswitch $exit (get_local 0) (case 1 (i32.const 1)) - (case 2 (break $exit (i32.const 2))) - (case 3 (break $ret (i32.const 3))) + (case 2 (br $exit (i32.const 2))) + (case 3 (br $ret (i32.const 3))) (default (i32.const 4)) (case 0 (i32.const 5)) ) @@ -47,7 +47,7 @@ ) (func $return (param i32) (result i32) - (switch (get_local 0) + (tableswitch (get_local 0) (case 0 (return (i32.const 0))) (case 1 (i32.const 1)) (default (i32.const 2)) diff --git a/ml-proto/test/memory.wast b/ml-proto/test/memory.wast index b09cd1488e..a277c11b76 100644 --- a/ml-proto/test/memory.wast +++ b/ml-proto/test/memory.wast @@ -98,7 +98,7 @@ (loop (if (i32.eq (get_local 0) (i32.const 0)) - (break 0) + (br 0) ) (set_local 2 (i32.mul (get_local 0) (i32.const 4))) (i32.store (get_local 2) (get_local 0)) @@ -121,7 +121,7 @@ (loop (if (i32.eq (get_local 0) (i32.const 0)) - (break 0) + (br 0) ) (set_local 2 (f64.convert_s/i32 (get_local 0))) (f64.store align=1 (get_local 0) (get_local 2)) diff --git a/ml-proto/test/switch.wast b/ml-proto/test/switch.wast index 9deaece9ef..4d17b32ed9 100644 --- a/ml-proto/test/switch.wast +++ b/ml-proto/test/switch.wast @@ -6,13 +6,13 @@ (local $j i32) (set_local $j (i32.const 100)) (label - (switch (get_local $i) + (tableswitch (get_local $i) (case 0 (return (get_local $i))) (case 1 (nop)) ;; fallthrough (case 2) ;; fallthrough - (case 3 (set_local $j (i32.sub (i32.const 0) (get_local $i))) (break 0)) - (case 4 (break 0)) - (case 5 (break 0 (set_local $j (i32.const 101)))) + (case 3 (set_local $j (i32.sub (i32.const 0) (get_local $i))) (br 0)) + (case 4 (br 0)) + (case 5 (br 0 (set_local $j (i32.const 101)))) (case 6 (set_local $j (i32.const 101))) ;; fallthrough (default (set_local $j (i32.const 102))) (case 7) @@ -27,15 +27,15 @@ (set_local $j (i64.const 100)) (return (label $l - (switch (i32.wrap/i64 (get_local $i)) + (tableswitch (i32.wrap/i64 (get_local $i)) (case 0 (return (get_local $i))) (case 1 (nop)) ;; fallthrough (case 2) ;; fallthrough - (case 3 (break $l (i64.sub (i64.const 0) (get_local $i)))) + (case 3 (br $l (i64.sub (i64.const 0) (get_local $i)))) (case 6 (set_local $j (i64.const 101))) ;; fallthrough (case 4) ;; fallthrough (case 5) ;; fallthrough - (default (break $l (get_local $j))) + (default (br $l (get_local $j))) (case 7 (i64.const -5)) ) ) @@ -45,28 +45,28 @@ ;; Corner cases (func $corner (result i32) (local $x i32) - (switch (i32.const 0) + (tableswitch (i32.const 0) (default) ) - (switch (i32.const 0) + (tableswitch (i32.const 0) (default (set_local $x (i32.add (get_local $x) (i32.const 1)))) ) - (switch (i32.const 1) + (tableswitch (i32.const 1) (default (set_local $x (i32.add (get_local $x) (i32.const 2)))) (case 0 (set_local $x (i32.add (get_local $x) (i32.const 4)))) ) (get_local $x) ) - ;; Break - (func $break (result i32) + ;; Branch + (func $branch (result i32) (local $x i32) - (switch $l (i32.const 0) - (case_break 0 $l) + (tableswitch $l (i32.const 0) + (case_br 0 $l) (default (set_local $x (i32.add (get_local $x) (i32.const 1)))) ) - (switch $l (i32.const 1) - (default_break $l) + (tableswitch $l (i32.const 1) + (default_br $l) (case 0 (set_local $x (i32.add (get_local $x) (i32.const 2)))) ) (get_local $x) @@ -75,7 +75,7 @@ (export "stmt" $stmt) (export "expr" $expr) (export "corner" $corner) - (export "break" $break) + (export "branch" $branch) ) (assert_return (invoke "stmt" (i32.const 0)) (i32.const 0)) @@ -97,11 +97,11 @@ (assert_return (invoke "expr" (i64.const -10)) (i64.const 100)) (assert_return (invoke "corner") (i32.const 7)) -(assert_return (invoke "break") (i32.const 0)) +(assert_return (invoke "branch") (i32.const 0)) -(assert_invalid (module (func (switch (i32.const 0) (case 0)))) "switch is missing default case") -(assert_invalid (module (func (switch (i32.const 0) (default) (case 1)))) "switch is not dense") -(assert_invalid (module (func (switch (i32.const 0) (default) (case 0) (case 3)))) "switch is not dense") -(assert_invalid (module (func (switch (i32.const 0) (default) (case 0) (default)))) "duplicate case") -(assert_invalid (module (func (switch (i32.const 0) (case 0) (default) (case 0)))) "duplicate case") +(assert_invalid (module (func (tableswitch (i32.const 0) (case 0)))) "switch is missing default case") +(assert_invalid (module (func (tableswitch (i32.const 0) (default) (case 1)))) "switch is not dense") +(assert_invalid (module (func (tableswitch (i32.const 0) (default) (case 0) (case 3)))) "switch is not dense") +(assert_invalid (module (func (tableswitch (i32.const 0) (default) (case 0) (default)))) "duplicate case") +(assert_invalid (module (func (tableswitch (i32.const 0) (case 0) (default) (case 0)))) "duplicate case") From 13f3a222ee199d1ea3c9da70654e5baa56ad6f6c Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 28 Oct 2015 16:12:22 +0100 Subject: [PATCH 05/12] Split if into if and if_else --- ml-proto/README.md | 4 ++-- ml-proto/host/lexer.mll | 1 + ml-proto/host/parser.mly | 5 +++-- ml-proto/spec/sugar.ml | 8 +++++--- ml-proto/spec/sugar.mli | 3 ++- ml-proto/test/fac.wast | 8 ++++---- ml-proto/test/forward.wast | 4 ++-- 7 files changed, 19 insertions(+), 14 deletions(-) diff --git a/ml-proto/README.md b/ml-proto/README.md index eb8eb1fd6b..f891670754 100644 --- a/ml-proto/README.md +++ b/ml-proto/README.md @@ -119,8 +119,8 @@ expr: ( nop ) ( block + ) ( block + ) ;; = (label (block +)) - ( if ) - ( if ) ;; = (if (nop)) + ( if_else ) + ( if ) ;; = (if_else (nop)) ( if_br ) ;; = (if (br ) (nop)) ( loop * ) ;; = (loop (block *)) ( loop ? * ) ;; = (label (loop (block ? *))) diff --git a/ml-proto/host/lexer.mll b/ml-proto/host/lexer.mll index 86305f52d5..ba98c82e80 100644 --- a/ml-proto/host/lexer.mll +++ b/ml-proto/host/lexer.mll @@ -134,6 +134,7 @@ rule token = parse | "nop" { NOP } | "block" { BLOCK } | "if" { IF } + | "if_else" { IF_ELSE } | "loop" { LOOP } | "label" { LABEL } | "br" { BRANCH } diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index cc5c3e9ca4..43281eeec0 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -151,7 +151,7 @@ let implicit_decl c t at = %} %token INT FLOAT TEXT VAR VALUE_TYPE LPAR RPAR -%token NOP BLOCK IF LOOP LABEL BRANCH SWITCH CASE DEFAULT +%token NOP BLOCK IF IF_ELSE LOOP LABEL BRANCH SWITCH CASE DEFAULT %token IF_BRANCH CASE_BRANCH DEFAULT_BRANCH %token CALL CALL_IMPORT CALL_INDIRECT RETURN %token GET_LOCAL SET_LOCAL LOAD STORE LOAD_EXTEND STORE_WRAP OFFSET ALIGN @@ -245,7 +245,8 @@ expr1 : | NOP { fun c -> nop } | BLOCK labeling expr expr_list { fun c -> let c', l = $2 c in block (l, $3 c' :: $4 c') } - | IF expr expr expr_opt { fun c -> if_ ($2 c, $3 c, $4 c) } + | IF_ELSE expr expr expr { fun c -> if_else ($2 c, $3 c, $4 c) } + | IF expr expr { fun c -> if_ ($2 c, $3 c) } | IF_BRANCH expr var { fun c -> if_branch ($2 c, $3 c label) } | LOOP labeling labeling expr_list { fun c -> let c', l1 = $2 c in let c'', l2 = $3 c' in diff --git a/ml-proto/spec/sugar.ml b/ml-proto/spec/sugar.ml index ae4ce01168..9b3b6f7d9e 100644 --- a/ml-proto/spec/sugar.ml +++ b/ml-proto/spec/sugar.ml @@ -23,12 +23,14 @@ let nop = let block (l, es) = labeling l (Block es) -let if_ (e1, e2, eo) = - let e3 = Lib.Option.get eo (Nop @@ Source.after e2.at) in +let if_else (e1, e2, e3) = If (e1, e2, e3) +let if_ (e1, e2) = + If (e1, e2, Nop @@ Source.after e2.at) + let if_branch (e, x) = - if_ (e, Branch (x, None) @@ x.at, None) + if_ (e, Branch (x, None) @@ x.at) let loop (l1, l2, es) = let e = expr_seq es in diff --git a/ml-proto/spec/sugar.mli b/ml-proto/spec/sugar.mli index 998b1b1059..510864bcae 100644 --- a/ml-proto/spec/sugar.mli +++ b/ml-proto/spec/sugar.mli @@ -5,7 +5,8 @@ and labeling' = Unlabelled | Labelled val nop : expr' val block : labeling * expr list -> expr' -val if_ : expr * expr * expr option -> expr' +val if_else : expr * expr * expr -> expr' +val if_ : expr * expr -> expr' val if_branch : expr * var -> expr' val loop : labeling * labeling * expr list -> expr' val label : expr -> expr' diff --git a/ml-proto/test/fac.wast b/ml-proto/test/fac.wast index 187c516ffc..5388b90a67 100644 --- a/ml-proto/test/fac.wast +++ b/ml-proto/test/fac.wast @@ -3,7 +3,7 @@ (module ;; Recursive factorial (func (param i64) (result i64) - (if (i64.eq (get_local 0) (i64.const 0)) + (if_else (i64.eq (get_local 0) (i64.const 0)) (i64.const 1) (i64.mul (get_local 0) (call 0 (i64.sub (get_local 0) (i64.const 1)))) ) @@ -11,7 +11,7 @@ ;; Recursive factorial named (func $fac-rec (param $n i64) (result i64) - (if (i64.eq (get_local $n) (i64.const 0)) + (if_else (i64.eq (get_local $n) (i64.const 0)) (i64.const 1) (i64.mul (get_local $n) @@ -27,7 +27,7 @@ (set_local 2 (i64.const 1)) (label (loop - (if + (if_else (i64.eq (get_local 1) (i64.const 0)) (br 0) (block @@ -48,7 +48,7 @@ (set_local $res (i64.const 1)) (label $done (loop - (if + (if_else (i64.eq (get_local $i) (i64.const 0)) (br $done) (block diff --git a/ml-proto/test/forward.wast b/ml-proto/test/forward.wast index 9c49228344..944954abaf 100644 --- a/ml-proto/test/forward.wast +++ b/ml-proto/test/forward.wast @@ -5,14 +5,14 @@ (export "odd" $odd) (func $even (param $n i32) (result i32) - (if (i32.eq (get_local $n) (i32.const 0)) + (if_else (i32.eq (get_local $n) (i32.const 0)) (i32.const 1) (call $odd (i32.sub (get_local $n) (i32.const 1))) ) ) (func $odd (param $n i32) (result i32) - (if (i32.eq (get_local $n) (i32.const 0)) + (if_else (i32.eq (get_local $n) (i32.const 0)) (i32.const 0) (call $even (i32.sub (get_local $n) (i32.const 1))) ) From cf1bd2b315936dd4a9bf5207a849f56edc2bc689 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 28 Oct 2015 16:56:09 +0100 Subject: [PATCH 06/12] Change loop to not loop --- ml-proto/README.md | 4 ++-- ml-proto/host/parser.mly | 3 ++- ml-proto/spec/check.ml | 3 ++- ml-proto/spec/eval.ml | 5 +++-- ml-proto/spec/sugar.ml | 2 +- ml-proto/test/fac.wast | 6 ++++-- ml-proto/test/labels.wast | 4 +++- ml-proto/test/memory.wast | 6 ++++-- 8 files changed, 21 insertions(+), 12 deletions(-) diff --git a/ml-proto/README.md b/ml-proto/README.md index f891670754..11daa62c94 100644 --- a/ml-proto/README.md +++ b/ml-proto/README.md @@ -122,8 +122,8 @@ expr: ( if_else ) ( if ) ;; = (if_else (nop)) ( if_br ) ;; = (if (br ) (nop)) - ( loop * ) ;; = (loop (block *)) - ( loop ? * ) ;; = (label (loop (block ? *))) + ( loop ? * ) ;; = (loop ? (block *)) + ( loop * ) ;; = (label (loop (block *))) ( label ? ) ( br ? ) ( tableswitch + ) diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index 43281eeec0..0db64b83e9 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -250,7 +250,8 @@ expr1 : | IF_BRANCH expr var { fun c -> if_branch ($2 c, $3 c label) } | LOOP labeling labeling expr_list { fun c -> let c', l1 = $2 c in let c'', l2 = $3 c' in - loop (l1, l2, $4 c'') } + let c''' = if l1.it = Unlabelled then anon_label c'' else c'' in + loop (l1, l2, $4 c''') } | LABEL labeling expr { fun c -> let c', l = $2 c in let c'' = if l.it = Unlabelled then anon_label c' else c' in diff --git a/ml-proto/spec/check.ml b/ml-proto/spec/check.ml index 13fc2e71f6..3dda142e46 100644 --- a/ml-proto/spec/check.ml +++ b/ml-proto/spec/check.ml @@ -135,7 +135,8 @@ let rec check_expr c et e = check_expr c et e3 | Loop e1 -> - check_expr c None e1 + let c' = {c with labels = None :: c.labels} in + check_expr c' et e1 | Label e1 -> let c' = {c with labels = et :: c.labels} in diff --git a/ml-proto/spec/eval.ml b/ml-proto/spec/eval.ml index e71e352b73..e2b0607dc3 100644 --- a/ml-proto/spec/eval.ml +++ b/ml-proto/spec/eval.ml @@ -149,8 +149,9 @@ let rec eval_expr (c : config) (e : expr) = eval_expr c (if i <> Int32.zero then e2 else e3) | Loop e1 -> - ignore (eval_expr c e1); - eval_expr c e + let module L = MakeLabel () in + let c' = {c with labels = L.label :: c.labels} in + (try eval_expr c' e1 with L.Label _ -> eval_expr c e) | Label e1 -> let module L = MakeLabel () in diff --git a/ml-proto/spec/sugar.ml b/ml-proto/spec/sugar.ml index 9b3b6f7d9e..0444bed30a 100644 --- a/ml-proto/spec/sugar.ml +++ b/ml-proto/spec/sugar.ml @@ -34,7 +34,7 @@ let if_branch (e, x) = let loop (l1, l2, es) = let e = expr_seq es in - labeling l1 (Loop (labeling l2 e.it @@ e.at)) + if l2.it = Unlabelled then Loop e else labeling l1 (Loop e) let label e = Label e diff --git a/ml-proto/test/fac.wast b/ml-proto/test/fac.wast index 5388b90a67..48c57bf4da 100644 --- a/ml-proto/test/fac.wast +++ b/ml-proto/test/fac.wast @@ -29,12 +29,13 @@ (loop (if_else (i64.eq (get_local 1) (i64.const 0)) - (br 0) + (br 1) (block (set_local 2 (i64.mul (get_local 1) (get_local 2))) (set_local 1 (i64.sub (get_local 1) (i64.const 1))) ) ) + (br 0) ) ) (return (get_local 2)) @@ -47,7 +48,7 @@ (set_local $i (get_local $n)) (set_local $res (i64.const 1)) (label $done - (loop + (loop $loop (if_else (i64.eq (get_local $i) (i64.const 0)) (br $done) @@ -56,6 +57,7 @@ (set_local $i (i64.sub (get_local $i) (i64.const 1))) ) ) + (br $loop) ) ) (return (get_local $res)) diff --git a/ml-proto/test/labels.wast b/ml-proto/test/labels.wast index b59090613f..95a35f6a85 100644 --- a/ml-proto/test/labels.wast +++ b/ml-proto/test/labels.wast @@ -9,11 +9,12 @@ (func $loop1 (result i32) (local $i i32) (set_local $i (i32.const 0)) - (loop $exit + (loop $exit $cont (set_local $i (i32.add (get_local $i) (i32.const 1))) (if (i32.eq (get_local $i) (i32.const 5)) (br $exit (get_local $i)) ) + (br $cont) ) ) @@ -29,6 +30,7 @@ (br $exit (get_local $i)) ) (set_local $i (i32.add (get_local $i) (i32.const 1))) + (br $cont) ) ) diff --git a/ml-proto/test/memory.wast b/ml-proto/test/memory.wast index a277c11b76..7ddc338307 100644 --- a/ml-proto/test/memory.wast +++ b/ml-proto/test/memory.wast @@ -98,7 +98,7 @@ (loop (if (i32.eq (get_local 0) (i32.const 0)) - (br 0) + (br 1) ) (set_local 2 (i32.mul (get_local 0) (i32.const 4))) (i32.store (get_local 2) (get_local 0)) @@ -108,6 +108,7 @@ (return (i32.const 0)) ) (set_local 0 (i32.sub (get_local 0) (i32.const 1))) + (br 0) ) ) (return (i32.const 1)) @@ -121,7 +122,7 @@ (loop (if (i32.eq (get_local 0) (i32.const 0)) - (br 0) + (br 1) ) (set_local 2 (f64.convert_s/i32 (get_local 0))) (f64.store align=1 (get_local 0) (get_local 2)) @@ -131,6 +132,7 @@ (return (i32.const 0)) ) (set_local 0 (i32.sub (get_local 0) (i32.const 1))) + (br 0) ) ) (return (i32.const 1)) From 75c0edeacc6b8955f9be4dc81af860cf6c1b53c8 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 28 Oct 2015 17:11:05 +0100 Subject: [PATCH 07/12] Adjust to rebase --- ml-proto/host/parser.mly | 4 ++-- ml-proto/spec/eval.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index 8d41406b4b..912ca52522 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -51,8 +51,8 @@ let literal s t = let int32 s = try I32.of_string s.it with - | Failure reason -> Error.error s.at ("constant out of range: " ^ reason) - | _ -> Error.error s.at "constant out of range" + | Failure reason -> error s.at ("constant out of range: " ^ reason) + | _ -> error s.at "constant out of range" (* Memory operands *) diff --git a/ml-proto/spec/eval.ml b/ml-proto/spec/eval.ml index eeb7047201..8fec5caad5 100644 --- a/ml-proto/spec/eval.ml +++ b/ml-proto/spec/eval.ml @@ -168,7 +168,7 @@ let rec eval_expr (c : config) (e : expr) = then None else Some i in (match List.fold_left (eval_case c l) `Seek cs with - | `Seek -> error e.at "runtime crash: switch failed" + | `Seek -> Crash.error e.at "switch failed" | `Found vo -> vo ) From 3ca89e90141aed01873baf3372804bbd34b8a8a5 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 28 Oct 2015 18:29:27 +0100 Subject: [PATCH 08/12] Fix internal naming inconsistencies --- ml-proto/host/lexer.mll | 10 +++++----- ml-proto/host/parser.mly | 22 +++++++++++----------- ml-proto/spec/sugar.ml | 18 ++++++++++++------ ml-proto/spec/sugar.mli | 12 +++++++----- 4 files changed, 35 insertions(+), 27 deletions(-) diff --git a/ml-proto/host/lexer.mll b/ml-proto/host/lexer.mll index 425a92a1d9..c3b54cb9c7 100644 --- a/ml-proto/host/lexer.mll +++ b/ml-proto/host/lexer.mll @@ -137,8 +137,8 @@ rule token = parse | "if_else" { IF_ELSE } | "loop" { LOOP } | "label" { LABEL } - | "br" { BRANCH } - | "tableswitch" { SWITCH } + | "br" { BR } + | "tableswitch" { TABLESWITCH } | "case" { CASE } | "default" { DEFAULT } | "call" { CALL } @@ -146,9 +146,9 @@ rule token = parse | "call_indirect" { CALL_INDIRECT } | "return" { RETURN } - | "if_br" { IF_BRANCH } - | "case_br" { CASE_BRANCH } - | "default_br" { DEFAULT_BRANCH } + | "br_if" { BR_IF } + | "case_br" { CASE_BR } + | "default_br" { DEFAULT_BR } | "get_local" { GET_LOCAL } | "set_local" { SET_LOCAL } diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index 912ca52522..2a6abcc69d 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -158,8 +158,8 @@ let implicit_decl c t at = %} %token INT FLOAT TEXT VAR VALUE_TYPE LPAR RPAR -%token NOP BLOCK IF IF_ELSE LOOP LABEL BRANCH SWITCH CASE DEFAULT -%token IF_BRANCH CASE_BRANCH DEFAULT_BRANCH +%token NOP BLOCK IF IF_ELSE LOOP LABEL BR TABLESWITCH CASE DEFAULT +%token BR_IF CASE_BR DEFAULT_BR %token CALL CALL_IMPORT CALL_INDIRECT RETURN %token GET_LOCAL SET_LOCAL LOAD STORE LOAD_EXTEND STORE_WRAP OFFSET ALIGN %token CONST UNARY BINARY COMPARE CONVERT @@ -254,7 +254,7 @@ expr1 : { fun c -> let c', l = $2 c in block (l, $3 c' :: $4 c') } | IF_ELSE expr expr expr { fun c -> if_else ($2 c, $3 c, $4 c) } | IF expr expr { fun c -> if_ ($2 c, $3 c) } - | IF_BRANCH expr var { fun c -> if_branch ($2 c, $3 c label) } + | BR_IF expr var { fun c -> br_if ($2 c, $3 c label) } | LOOP labeling labeling expr_list { fun c -> let c', l1 = $2 c in let c'', l2 = $3 c' in let c''' = if l1.it = Unlabelled then anon_label c'' else c'' in @@ -263,12 +263,12 @@ expr1 : { fun c -> let c', l = $2 c in let c'' = if l.it = Unlabelled then anon_label c' else c' in Sugar.label ($3 c'') } - | BRANCH var expr_opt { fun c -> branch ($2 c label, $3 c) } + | BR var expr_opt { fun c -> br ($2 c label, $3 c) } | RETURN expr_opt { let at1 = ati 1 in fun c -> return (label c ("return" @@ at1) @@ at1, $2 c) } - | SWITCH labeling expr case_list - { fun c -> let c', l = $2 c in switch (l, $3 c', $4 c') } + | TABLESWITCH labeling expr case_list + { fun c -> let c', l = $2 c in tableswitch (l, $3 c', $4 c') } | CALL var expr_list { fun c -> call ($2 c func, $3 c) } | CALL_IMPORT var expr_list { fun c -> call_import ($2 c import, $3 c) } | CALL_INDIRECT var expr expr_list @@ -306,11 +306,11 @@ case : | LPAR case1 RPAR { let at = at () in fun c -> $2 c @@ at } ; case1 : - | CASE literal expr_list { fun c -> case (Some (int32 $2), $3 c) } - | DEFAULT expr_list { fun c -> case (None, $2 c) } - | CASE_BRANCH literal var - { fun c -> case_branch (Some (int32 $2), $3 c label) } - | DEFAULT_BRANCH var { fun c -> case_branch (None, $2 c label) } + | CASE literal expr_list { fun c -> case (int32 $2, $3 c) } + | DEFAULT expr_list { fun c -> default ($2 c) } + | CASE_BR literal var + { fun c -> case_br (int32 $2, $3 c label) } + | DEFAULT_BR var { fun c -> default_br ($2 c label) } ; case_list : | case { fun c -> [$1 c] } diff --git a/ml-proto/spec/sugar.ml b/ml-proto/spec/sugar.ml index 0444bed30a..032f378189 100644 --- a/ml-proto/spec/sugar.ml +++ b/ml-proto/spec/sugar.ml @@ -29,7 +29,7 @@ let if_else (e1, e2, e3) = let if_ (e1, e2) = If (e1, e2, Nop @@ Source.after e2.at) -let if_branch (e, x) = +let br_if (e, x) = if_ (e, Branch (x, None) @@ x.at) let loop (l1, l2, es) = @@ -39,13 +39,13 @@ let loop (l1, l2, es) = let label e = Label e -let branch (x, e) = +let br (x, e) = Branch (x, e) let return (x, eo) = Branch (x, eo) -let switch (l, e, cs) = +let tableswitch (l, e, cs) = labeling l (Switch (e, cs)) let call (x, es) = @@ -95,10 +95,16 @@ let host (hostop, es) = let case (c, es) = - {value = c; expr = expr_seq es} + {value = Some c; expr = expr_seq es} -let case_branch (c, x) = - {value = c; expr = Branch (x, None) @@ x.at} +let case_br (c, x) = + {value = Some c; expr = Branch (x, None) @@ x.at} + +let default (es) = + {value = None; expr = expr_seq es} + +let default_br (x) = + {value = None; expr = Branch (x, None) @@ x.at} let func_body es = diff --git a/ml-proto/spec/sugar.mli b/ml-proto/spec/sugar.mli index 510864bcae..e2b0838ab4 100644 --- a/ml-proto/spec/sugar.mli +++ b/ml-proto/spec/sugar.mli @@ -7,12 +7,12 @@ val nop : expr' val block : labeling * expr list -> expr' val if_else : expr * expr * expr -> expr' val if_ : expr * expr -> expr' -val if_branch : expr * var -> expr' +val br_if : expr * var -> expr' val loop : labeling * labeling * expr list -> expr' val label : expr -> expr' -val branch : var * expr option -> expr' +val br : var * expr option -> expr' val return : var * expr option -> expr' -val switch : labeling * expr * case list -> expr' +val tableswitch : labeling * expr * case list -> expr' val call : var * expr list -> expr' val call_import : var * expr list -> expr' val call_indirect : var * expr * expr list -> expr' @@ -29,7 +29,9 @@ val compare : relop * expr * expr -> expr' val convert : cvt * expr -> expr' val host : hostop * expr list -> expr' -val case : I32.t option * expr list -> case' -val case_branch : I32.t option * var -> case' +val case : I32.t * expr list -> case' +val case_br : I32.t * var -> case' +val default : expr list -> case' +val default_br : var -> case' val func_body : expr list -> expr' From 8dd07448ebe6fb5f95f50bad02fe2a178fb6d861 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 29 Oct 2015 11:23:37 +0100 Subject: [PATCH 09/12] Fix oversight in README --- ml-proto/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ml-proto/README.md b/ml-proto/README.md index 6806d5cfc2..c256d3c829 100644 --- a/ml-proto/README.md +++ b/ml-proto/README.md @@ -121,17 +121,17 @@ expr: ( block + ) ;; = (label (block +)) ( if_else ) ( if ) ;; = (if_else (nop)) - ( if_br ) ;; = (if (br ) (nop)) + ( br_if ) ;; = (if (br ) (nop)) ( loop ? * ) ;; = (loop ? (block *)) ( loop * ) ;; = (label (loop (block *))) ( label ? ) ( br ? ) + ( return ? ) ;; = (br ?) ( tableswitch + ) ( tableswitch + ) ;; = (label (tableswitch +)) ( call * ) ( call_import * ) ( call_indirect * ) - ( return ? ) ;; = (br ?) ( get_local ) ( set_local ) ( .load((8|16)_)? ? ? ) From 83d01718e9787759d96042e734bb0aa8ea6491d7 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 29 Oct 2015 11:26:14 +0100 Subject: [PATCH 10/12] Fix another comment in README --- ml-proto/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ml-proto/README.md b/ml-proto/README.md index c256d3c829..c9439278d5 100644 --- a/ml-proto/README.md +++ b/ml-proto/README.md @@ -121,7 +121,7 @@ expr: ( block + ) ;; = (label (block +)) ( if_else ) ( if ) ;; = (if_else (nop)) - ( br_if ) ;; = (if (br ) (nop)) + ( br_if ) ;; = (if_else (br ) (nop)) ( loop ? * ) ;; = (loop ? (block *)) ( loop * ) ;; = (label (loop (block *))) ( label ? ) From 5dbeb12f19976e90715164639448621ad5318907 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 5 Nov 2015 12:42:12 +0100 Subject: [PATCH 11/12] Fall through br forms --- ml-proto/spec/sugar.ml | 11 ++++++----- ml-proto/spec/sugar.mli | 10 +++++----- ml-proto/test/switch.wast | 16 +++++++++++++--- 3 files changed, 24 insertions(+), 13 deletions(-) diff --git a/ml-proto/spec/sugar.ml b/ml-proto/spec/sugar.ml index 032f378189..e6c807b340 100644 --- a/ml-proto/spec/sugar.ml +++ b/ml-proto/spec/sugar.ml @@ -46,7 +46,8 @@ let return (x, eo) = Branch (x, eo) let tableswitch (l, e, cs) = - labeling l (Switch (e, cs)) + let cs1, cs2 = List.partition (fun c -> snd c.it) cs in + labeling l (Switch (e, List.map (fun c -> fst c.it @@ c.at) (cs1 @ cs2))) let call (x, es) = Call (x, es) @@ -95,16 +96,16 @@ let host (hostop, es) = let case (c, es) = - {value = Some c; expr = expr_seq es} + {value = Some c; expr = expr_seq es}, false let case_br (c, x) = - {value = Some c; expr = Branch (x, None) @@ x.at} + {value = Some c; expr = Branch (x, None) @@ x.at}, true let default (es) = - {value = None; expr = expr_seq es} + {value = None; expr = expr_seq es}, false let default_br (x) = - {value = None; expr = Branch (x, None) @@ x.at} + {value = None; expr = Branch (x, None) @@ x.at}, true let func_body es = diff --git a/ml-proto/spec/sugar.mli b/ml-proto/spec/sugar.mli index e2b0838ab4..35bea1fdf6 100644 --- a/ml-proto/spec/sugar.mli +++ b/ml-proto/spec/sugar.mli @@ -12,7 +12,7 @@ val loop : labeling * labeling * expr list -> expr' val label : expr -> expr' val br : var * expr option -> expr' val return : var * expr option -> expr' -val tableswitch : labeling * expr * case list -> expr' +val tableswitch : labeling * expr * (case' * bool) Source.phrase list -> expr' val call : var * expr list -> expr' val call_import : var * expr list -> expr' val call_indirect : var * expr * expr list -> expr' @@ -29,9 +29,9 @@ val compare : relop * expr * expr -> expr' val convert : cvt * expr -> expr' val host : hostop * expr list -> expr' -val case : I32.t * expr list -> case' -val case_br : I32.t * var -> case' -val default : expr list -> case' -val default_br : var -> case' +val case : I32.t * expr list -> case' * bool +val case_br : I32.t * var -> case' * bool +val default : expr list -> case' * bool +val default_br : var -> case' * bool val func_body : expr list -> expr' diff --git a/ml-proto/test/switch.wast b/ml-proto/test/switch.wast index 4d17b32ed9..4ad973eef9 100644 --- a/ml-proto/test/switch.wast +++ b/ml-proto/test/switch.wast @@ -69,6 +69,12 @@ (default_br $l) (case 0 (set_local $x (i32.add (get_local $x) (i32.const 2)))) ) + (tableswitch $l (i32.const 0) + (case 0) + (case_br 1 $l) + (default_br $l) + (case 2 (set_local $x (i32.add (get_local $x) (i32.const 4)))) + ) (get_local $x) ) @@ -97,11 +103,15 @@ (assert_return (invoke "expr" (i64.const -10)) (i64.const 100)) (assert_return (invoke "corner") (i32.const 7)) -(assert_return (invoke "branch") (i32.const 0)) +(assert_return (invoke "branch") (i32.const 4)) (assert_invalid (module (func (tableswitch (i32.const 0) (case 0)))) "switch is missing default case") (assert_invalid (module (func (tableswitch (i32.const 0) (default) (case 1)))) "switch is not dense") (assert_invalid (module (func (tableswitch (i32.const 0) (default) (case 0) (case 3)))) "switch is not dense") -(assert_invalid (module (func (tableswitch (i32.const 0) (default) (case 0) (default)))) "duplicate case") -(assert_invalid (module (func (tableswitch (i32.const 0) (case 0) (default) (case 0)))) "duplicate case") +(assert_invalid (module (func (tableswitch (i32.const 0) (default) (default)))) "duplicate case") +(assert_invalid (module (func (tableswitch $l (i32.const 0) (default_br $l) (default_br $l)))) "duplicate case") +(assert_invalid (module (func (tableswitch $l (i32.const 0) (default) (default_br $l)))) "duplicate case") +(assert_invalid (module (func (tableswitch (i32.const 0) (case 0) (case 0) (default)))) "duplicate case") +(assert_invalid (module (func (tableswitch $l (i32.const 0) (case_br 0 $l) (case_br 0 $l) (default)))) "duplicate case") +(assert_invalid (module (func (tableswitch $l (i32.const 0) (case 0) (case_br 0 $l) (default)))) "duplicate case") From e25be4da5022f3c559404e0faa44c3fe8508d9db Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 5 Nov 2015 13:11:12 +0100 Subject: [PATCH 12/12] Enforce br ordering --- ml-proto/host/parser.mly | 18 +++++++++++++----- ml-proto/spec/check.ml | 2 +- ml-proto/spec/sugar.ml | 11 +++++------ ml-proto/spec/sugar.mli | 10 +++++----- ml-proto/test/switch.wast | 14 ++++---------- 5 files changed, 28 insertions(+), 27 deletions(-) diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index 2a6abcc69d..52fe298a1a 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -305,16 +305,24 @@ expr_list : case : | LPAR case1 RPAR { let at = at () in fun c -> $2 c @@ at } ; +casebr : + | LPAR casebr1 RPAR { let at = at () in fun c -> $2 c @@ at } +; +casebr1 : + | CASE_BR literal var { fun c -> case_br (int32 $2, $3 c label) } + | DEFAULT_BR var { fun c -> default_br ($2 c label) } +; case1 : | CASE literal expr_list { fun c -> case (int32 $2, $3 c) } | DEFAULT expr_list { fun c -> default ($2 c) } - | CASE_BR literal var - { fun c -> case_br (int32 $2, $3 c label) } - | DEFAULT_BR var { fun c -> default_br ($2 c label) } ; case_list : - | case { fun c -> [$1 c] } - | case case_list { fun c -> $1 c :: $2 c } + | case_list1 { $1 } + | casebr case_list { fun c -> $1 c :: $2 c } +; +case_list1 : + | /* empty */ { fun c -> [] } + | case case_list1 { fun c -> $1 c :: $2 c } ; diff --git a/ml-proto/spec/check.ml b/ml-proto/spec/check.ml index 72bcdce885..6f44b41c9c 100644 --- a/ml-proto/spec/check.ml +++ b/ml-proto/spec/check.ml @@ -151,8 +151,8 @@ let rec check_expr c et e = | Switch (e1, cs) -> check_expr c (Some Int32Type) e1; let cc, _ = List.fold_right (check_case c) cs (CaseSet.empty, et) in - let max = CaseSet.max_elt cc in require (CaseSet.mem None cc) e.at "switch is missing default case"; + let max = CaseSet.max_elt cc in require (max = None || max = Some (I32.of_int (CaseSet.cardinal cc - 2))) e.at "switch is not dense" diff --git a/ml-proto/spec/sugar.ml b/ml-proto/spec/sugar.ml index e6c807b340..032f378189 100644 --- a/ml-proto/spec/sugar.ml +++ b/ml-proto/spec/sugar.ml @@ -46,8 +46,7 @@ let return (x, eo) = Branch (x, eo) let tableswitch (l, e, cs) = - let cs1, cs2 = List.partition (fun c -> snd c.it) cs in - labeling l (Switch (e, List.map (fun c -> fst c.it @@ c.at) (cs1 @ cs2))) + labeling l (Switch (e, cs)) let call (x, es) = Call (x, es) @@ -96,16 +95,16 @@ let host (hostop, es) = let case (c, es) = - {value = Some c; expr = expr_seq es}, false + {value = Some c; expr = expr_seq es} let case_br (c, x) = - {value = Some c; expr = Branch (x, None) @@ x.at}, true + {value = Some c; expr = Branch (x, None) @@ x.at} let default (es) = - {value = None; expr = expr_seq es}, false + {value = None; expr = expr_seq es} let default_br (x) = - {value = None; expr = Branch (x, None) @@ x.at}, true + {value = None; expr = Branch (x, None) @@ x.at} let func_body es = diff --git a/ml-proto/spec/sugar.mli b/ml-proto/spec/sugar.mli index 35bea1fdf6..e2b0838ab4 100644 --- a/ml-proto/spec/sugar.mli +++ b/ml-proto/spec/sugar.mli @@ -12,7 +12,7 @@ val loop : labeling * labeling * expr list -> expr' val label : expr -> expr' val br : var * expr option -> expr' val return : var * expr option -> expr' -val tableswitch : labeling * expr * (case' * bool) Source.phrase list -> expr' +val tableswitch : labeling * expr * case list -> expr' val call : var * expr list -> expr' val call_import : var * expr list -> expr' val call_indirect : var * expr * expr list -> expr' @@ -29,9 +29,9 @@ val compare : relop * expr * expr -> expr' val convert : cvt * expr -> expr' val host : hostop * expr list -> expr' -val case : I32.t * expr list -> case' * bool -val case_br : I32.t * var -> case' * bool -val default : expr list -> case' * bool -val default_br : var -> case' * bool +val case : I32.t * expr list -> case' +val case_br : I32.t * var -> case' +val default : expr list -> case' +val default_br : var -> case' val func_body : expr list -> expr' diff --git a/ml-proto/test/switch.wast b/ml-proto/test/switch.wast index 4ad973eef9..061d2f852d 100644 --- a/ml-proto/test/switch.wast +++ b/ml-proto/test/switch.wast @@ -69,12 +69,6 @@ (default_br $l) (case 0 (set_local $x (i32.add (get_local $x) (i32.const 2)))) ) - (tableswitch $l (i32.const 0) - (case 0) - (case_br 1 $l) - (default_br $l) - (case 2 (set_local $x (i32.add (get_local $x) (i32.const 4)))) - ) (get_local $x) ) @@ -103,15 +97,15 @@ (assert_return (invoke "expr" (i64.const -10)) (i64.const 100)) (assert_return (invoke "corner") (i32.const 7)) -(assert_return (invoke "branch") (i32.const 4)) +(assert_return (invoke "branch") (i32.const 0)) +(assert_invalid (module (func (tableswitch (i32.const 0)))) "switch is missing default case") (assert_invalid (module (func (tableswitch (i32.const 0) (case 0)))) "switch is missing default case") (assert_invalid (module (func (tableswitch (i32.const 0) (default) (case 1)))) "switch is not dense") (assert_invalid (module (func (tableswitch (i32.const 0) (default) (case 0) (case 3)))) "switch is not dense") (assert_invalid (module (func (tableswitch (i32.const 0) (default) (default)))) "duplicate case") (assert_invalid (module (func (tableswitch $l (i32.const 0) (default_br $l) (default_br $l)))) "duplicate case") -(assert_invalid (module (func (tableswitch $l (i32.const 0) (default) (default_br $l)))) "duplicate case") +(assert_invalid (module (func (tableswitch $l (i32.const 0) (default_br $l) (default)))) "duplicate case") (assert_invalid (module (func (tableswitch (i32.const 0) (case 0) (case 0) (default)))) "duplicate case") (assert_invalid (module (func (tableswitch $l (i32.const 0) (case_br 0 $l) (case_br 0 $l) (default)))) "duplicate case") -(assert_invalid (module (func (tableswitch $l (i32.const 0) (case 0) (case_br 0 $l) (default)))) "duplicate case") - +(assert_invalid (module (func (tableswitch $l (i32.const 0) (case_br 0 $l) (case 0) (default)))) "duplicate case")