Skip to content

Commit

Permalink
Add unconditional unreachable expression
Browse files Browse the repository at this point in the history
Add an expression which typechecks in any context, and always traps when
executed.
  • Loading branch information
dschuff committed Nov 6, 2015
1 parent 6717e74 commit fe6c87b
Show file tree
Hide file tree
Showing 9 changed files with 55 additions and 7 deletions.
1 change: 1 addition & 0 deletions ml-proto/host/lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -241,6 +241,7 @@ rule token = parse
| (ixx as t)".select" { SELECT ( intop t Int32Op.Select Int64Op.Select) }
| (fxx as t)".select" { SELECT ( floatop t Float32Op.Select Float64Op.Select) }

| "unreachable" { UNREACHABLE }
| "page_size" { PAGE_SIZE }
| "memory_size" { MEMORY_SIZE }
| "grow_memory" { GROW_MEMORY }
Expand Down
3 changes: 2 additions & 1 deletion ml-proto/host/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@ let implicit_decl c t at =
%token CONST UNARY BINARY COMPARE CONVERT
%token FUNC TYPE PARAM RESULT LOCAL
%token MODULE MEMORY SEGMENT IMPORT EXPORT TABLE
%token PAGE_SIZE MEMORY_SIZE GROW_MEMORY HAS_FEATURE
%token UNREACHABLE PAGE_SIZE MEMORY_SIZE GROW_MEMORY HAS_FEATURE
%token ASSERT_INVALID ASSERT_RETURN ASSERT_RETURN_NAN ASSERT_TRAP INVOKE
%token EOF

Expand Down Expand Up @@ -283,6 +283,7 @@ expr1 :
| COMPARE expr expr { fun c -> compare ($1, $2 c, $3 c) }
| CONVERT expr { fun c -> convert ($1, $2 c) }
| SELECT expr expr expr { fun c -> select ($1, $2 c, $3 c, $4 c) }
| UNREACHABLE { fun c -> unreachable }
| PAGE_SIZE { fun c -> host (PageSize, []) }
| MEMORY_SIZE { fun c -> host (MemorySize, []) }
| GROW_MEMORY expr { fun c -> host (GrowMemory, [$2 c]) }
Expand Down
1 change: 1 addition & 0 deletions ml-proto/spec/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,7 @@ and expr' =
| Compare of relop * expr * expr (* arithmetic comparison *)
| Convert of cvt * expr (* conversion *)
| Select of selectop * expr * expr * expr (* branchless conditional *)
| Unreachable (* trap *)
| Host of hostop * expr list (* host interaction *)

and case = case' Source.phrase
Expand Down
3 changes: 3 additions & 0 deletions ml-proto/spec/check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -218,6 +218,9 @@ let rec check_expr c et e =
check_expr c (Some t) e2;
check_expr c (Some t) e3

| Unreachable ->
check_type None None e.at

| Host (hostop, es) ->
let ({ins; out}, hasmem) = type_hostop hostop in
if hasmem then
Expand Down
3 changes: 3 additions & 0 deletions ml-proto/spec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -250,6 +250,9 @@ let rec eval_expr (c : config) (e : expr) =
let v2 = some (eval_expr c e3) e3.at in
Some (if cond <> Int32.zero then v1 else v2)

| Unreachable ->
Trap.error e.at "unreachable executed"

| Host (hostop, es) ->
let vs = List.map (eval_expr c) es in
eval_hostop c hostop vs e.at
Expand Down
3 changes: 3 additions & 0 deletions ml-proto/spec/sugar.ml
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,9 @@ let convert (cvt, e) =
let select (selectop, cond, e1, e2) =
Select (selectop, cond, e1, e2)

let unreachable =
Unreachable

let host (hostop, es) =
Host (hostop, es)

Expand Down
1 change: 1 addition & 0 deletions ml-proto/spec/sugar.mli
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ val binary : binop * expr * expr -> expr'
val compare : relop * expr * expr -> expr'
val convert : cvt * expr -> expr'
val select : selectop * expr * expr * expr -> expr'
val unreachable : expr'
val host : hostop * expr list -> expr'

val case : literal * (expr list * bool) option -> case'
Expand Down
12 changes: 6 additions & 6 deletions ml-proto/test/select.wast
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,9 @@

;; Check that both sides of the select are evaluated
(func $select_trap_l (param $cond i32) (result i32)
(i32.select (get_local $cond) (i32.div_s (i32.const 1)(i32.const 0)) (i32.const 0)))
(i32.select (get_local $cond) (unreachable) (i32.const 0)))
(func $select_trap_r (param $cond i32) (result i32)
(i32.select (get_local $cond) (i32.const 0) (i32.div_s (i32.const 1)(i32.const 0))))
(i32.select (get_local $cond) (i32.const 0) (unreachable)))

(export "select_i32" $select_i32)
(export "select_i64" $select_i64)
Expand All @@ -41,7 +41,7 @@
(assert_return_nan (invoke "select_f64" (i32.const 1) (f64.const nan) (f64.const 1)))
(assert_return_nan (invoke "select_f64" (i32.const 0) (f64.const 2) (f64.const nan)))

(assert_trap (invoke "select_trap_l" (i32.const 1)) "integer divide by zero")
(assert_trap (invoke "select_trap_l" (i32.const 0)) "integer divide by zero")
(assert_trap (invoke "select_trap_r" (i32.const 1)) "integer divide by zero")
(assert_trap (invoke "select_trap_r" (i32.const 0)) "integer divide by zero")
(assert_trap (invoke "select_trap_l" (i32.const 1)) "unreachable executed")
(assert_trap (invoke "select_trap_l" (i32.const 0)) "unreachable executed")
(assert_trap (invoke "select_trap_r" (i32.const 1)) "unreachable executed")
(assert_trap (invoke "select_trap_r" (i32.const 0)) "unreachable executed")
35 changes: 35 additions & 0 deletions ml-proto/test/unreachable.wast
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
(module
(func $return_i32 (result i32)
(unreachable))
(func $return_f64 (result f64)
(unreachable))

(func $if (param i32) (result f32)
(if (get_local 0) (unreachable) (f32.const 0)))

(func $block
(block (i32.const 1) (unreachable) (i32.const 2)))

(func $return_i64 (result i64)
(return (i64.const 1))
(unreachable))

(func $call (result f64)
(call $return_i32)
(unreachable))

(export "return_i32" $return_i32)
(export "return_f64" $return_f64)
(export "if" $if)
(export "block" $block)
(export "return_i64" $return_i64)
(export "call" $call)
)

(assert_trap (invoke "return_i32") "unreachable executed")
(assert_trap (invoke "return_f64") "unreachable executed")
(assert_trap (invoke "if" (i32.const 1)) "unreachable executed")
(assert_return (invoke "if" (i32.const 0)) (f32.const 0))
(assert_trap (invoke "block") "unreachable executed")
(assert_return (invoke "return_i64") (i64.const 1))
(assert_trap (invoke "call") "unreachable executed")

0 comments on commit fe6c87b

Please sign in to comment.