Skip to content
This repository was archived by the owner on Apr 25, 2025. It is now read-only.
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions interpreter/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -304,6 +304,9 @@ op:
struct.get(_<sign>)? <var> <var>
struct.set <var> <var>
array.new(_<default>)? <var>
array.new_fixed <var> <nat>
array.new_elem <var> <var>
array.new_data <var> <var>
array.get(_<sign>)? <var>
array.set <var>
array.len <var>
Expand Down
4 changes: 4 additions & 0 deletions interpreter/binary/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -593,6 +593,10 @@ let rec instr s =
| 0x16l -> array_set (at var s)
| 0x17l -> let _ = var s in array_len (* TODO: remove var *)

| 0x19l -> let x = at var s in let n = u32 s in array_new_fixed x n
| 0x1bl -> let x = at var s in let y = at var s in array_new_data x y
| 0x1cl -> let x = at var s in let y = at var s in array_new_elem x y

| 0x20l -> i31_new
| 0x21l -> i31_get_s
| 0x22l -> i31_get_u
Expand Down
3 changes: 3 additions & 0 deletions interpreter/binary/encode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -397,6 +397,9 @@ struct

| ArrayNew (x, Explicit) -> op 0xfb; op 0x11; var x
| ArrayNew (x, Implicit) -> op 0xfb; op 0x12; var x
| ArrayNewFixed (x, n) -> op 0xfb; op 0x19; var x; u32 n
| ArrayNewElem (x, y) -> op 0xfb; op 0x1c; var x; var y
| ArrayNewData (x, y) -> op 0xfb; op 0x1b; var x; var y
| ArrayGet (x, None) -> op 0xfb; op 0x13; var x
| ArrayGet (x, Some SX) -> op 0xfb; op 0x14; var x
| ArrayGet (x, Some ZX) -> op 0xfb; op 0x15; var x
Expand Down
63 changes: 59 additions & 4 deletions interpreter/exec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -173,13 +173,13 @@ let rec step (c : config) : config =
let FuncType (ts1, ts2) = block_type c.frame.inst bt e.at in
let n1 = List.length ts1 in
let n2 = List.length ts2 in
let args, vs' = take n1 vs e.at, drop n1 vs e.at in
let args, vs' = split n1 vs e.at in
vs', [Label (n2, [], (args, List.map plain es')) @@ e.at]

| Loop (bt, es'), vs ->
let FuncType (ts1, ts2) = block_type c.frame.inst bt e.at in
let n1 = List.length ts1 in
let args, vs' = take n1 vs e.at, drop n1 vs e.at in
let args, vs' = split n1 vs e.at in
vs', [Label (n1, [e' @@ e.at], (args, List.map plain es')) @@ e.at]

| If (bt, es1, es2), Num (I32 i) :: vs' ->
Expand Down Expand Up @@ -813,11 +813,66 @@ let rec step (c : config) : config =
try default_value (unpacked_storage_type st), vs'
with Failure _ -> Crash.error e.at "non-defaultable type"
in
let data =
try Data.alloc_array (type_ c.frame.inst x) rtt n arg
let data =
try Data.alloc_array (type_ c.frame.inst x) rtt (Lib.List32.make n arg)
with Failure _ -> Crash.error e.at "type mismatch packing value"
in Ref (Data.DataRef data) :: vs'', []

| ArrayNewFixed (x, n), Ref (Rtt.RttRef rtt) :: vs' ->
let args, vs'' = split (I32.to_int_u n) vs' e.at in
let data =
try Data.alloc_array (type_ c.frame.inst x) rtt (List.rev args)
with Failure _ -> Crash.error e.at "type mismatch packing value"
in Ref (Data.DataRef data) :: vs'', []

| ArrayNewElem (x, y),
Ref (Rtt.RttRef rtt) :: Num (I32 n) :: Num (I32 s) :: vs' ->
if elem_oob c.frame y s n then
vs', [Trapping (table_error e.at Table.Bounds) @@ e.at]
else
let seg = elem c.frame.inst y in
let args =
List.map (fun r -> Ref r) (Lib.List32.take n (Lib.List32.drop s !seg)) in
let data =
try Data.alloc_array (type_ c.frame.inst x) rtt args
with Failure _ -> Crash.error e.at "type mismatch packing value"
in Ref (Data.DataRef data) :: vs', []

| ArrayNewData (x, y),
Ref (Rtt.RttRef rtt) :: Num (I32 n) :: Num (I32 s) :: vs' ->
if data_oob c.frame y s n then
vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at]
else
let ArrayType (FieldType (st, _)) = array_type c.frame.inst x in
let seg = data c.frame.inst y in
let bs = Bytes.of_string !seg in
let args = Lib.List32.init n
(fun i ->
let j = I32.to_int_u s + I32.to_int_u i * storage_size st in
match st with
| PackedStorageType Pack8 ->
Num (I32 (I32.of_int_u (Bytes.get_uint8 bs j)))
| PackedStorageType Pack16 ->
Num (I32 (I32.of_int_u (Bytes.get_uint16_le bs j)))
| ValueStorageType (NumType I32Type) ->
Num (I32 (Bytes.get_int32_le bs j))
| ValueStorageType (NumType I64Type) ->
Num (I64 (Bytes.get_int64_le bs j))
| ValueStorageType (NumType F32Type) ->
Num (F32 (F32.of_bits (Bytes.get_int32_le bs j)))
| ValueStorageType (NumType F64Type) ->
Num (F64 (F64.of_bits (Bytes.get_int64_le bs j)))
| ValueStorageType (VecType V128Type) ->
Vec (V128 (V128.of_bits (String.sub !seg j 16)))
| _ ->
Crash.error e.at "type mismatch packing value"
)
in
let data =
try Data.alloc_array (type_ c.frame.inst x) rtt args
with Failure _ -> Crash.error e.at "type mismatch packing value"
in Ref (Data.DataRef data) :: vs', []

| ArrayGet (x, exto), Num (I32 i) :: Ref (NullRef _) :: vs' ->
vs', [Trapping "null array reference" @@ e.at]

Expand Down
4 changes: 2 additions & 2 deletions interpreter/runtime/data.ml
Original file line number Diff line number Diff line change
Expand Up @@ -43,9 +43,9 @@ let alloc_struct x rtt vs =
let StructType fts = as_struct_str_type (expand_ctx_type (def_of x)) in
Struct (x, rtt, List.map2 alloc_field fts vs)

let alloc_array x rtt n v =
let alloc_array x rtt vs =
let ArrayType ft = as_array_str_type (expand_ctx_type (def_of x)) in
Array (x, rtt, List.init (Int32.to_int n) (fun _ -> alloc_field ft v))
Array (x, rtt, List.map (alloc_field ft) vs)


let type_inst_of = function
Expand Down
2 changes: 1 addition & 1 deletion interpreter/runtime/data.mli
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ type t = data
type ref_ += DataRef of data

val alloc_struct : sem_var -> Rtt.t -> value list -> data
val alloc_array : sem_var -> Rtt.t -> int32 -> value -> data
val alloc_array : sem_var -> Rtt.t -> value list -> data

val struct_type_of : data -> struct_type
val array_type_of : data -> array_type
Expand Down
3 changes: 3 additions & 0 deletions interpreter/syntax/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -205,6 +205,9 @@ and instr' =
| StructGet of idx * idx * extension option (* read structure field *)
| StructSet of idx * idx (* write structure field *)
| ArrayNew of idx * initop (* allocate array *)
| ArrayNewFixed of idx * int32 (* allocate fixed array *)
| ArrayNewElem of idx * idx (* allocate array from element segment *)
| ArrayNewData of idx * idx (* allocate array from data segment *)
| ArrayGet of idx * extension option (* read array slot *)
| ArraySet of idx (* write array slot *)
| ArrayLen (* read array length *)
Expand Down
4 changes: 3 additions & 1 deletion interpreter/syntax/free.ml
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,9 @@ let rec instr (e : instr) =
| RefNull t -> heap_type t
| RefFunc x -> funcs (idx x)
| I31New | I31Get _ -> empty
| StructNew (x, _) | ArrayNew (x, _) -> types (idx x)
| StructNew (x, _) | ArrayNew (x, _) | ArrayNewFixed (x, _) -> types (idx x)
| ArrayNewElem (x, y) -> types (idx x) ++ elems (idx y)
| ArrayNewData (x, y) -> types (idx x) ++ datas (idx y)
| StructGet (x, _, _) | StructSet (x, _) -> types (idx x)
| ArrayGet (x, _) | ArraySet x -> types (idx x)
| ArrayLen -> empty
Expand Down
3 changes: 3 additions & 0 deletions interpreter/syntax/operators.ml
Original file line number Diff line number Diff line change
Expand Up @@ -133,6 +133,9 @@ let struct_get_s x y = StructGet (x, y, Some SX)
let struct_set x y = StructSet (x, y)
let array_new x = ArrayNew (x, Explicit)
let array_new_default x = ArrayNew (x, Implicit)
let array_new_fixed x n = ArrayNewFixed (x, n)
let array_new_elem x y = ArrayNewElem (x, y)
let array_new_data x y = ArrayNewData (x, y)
let array_get x = ArrayGet (x, None)
let array_get_u x = ArrayGet (x, Some ZX)
let array_get_s x = ArrayGet (x, Some SX)
Expand Down
18 changes: 13 additions & 5 deletions interpreter/syntax/types.ml
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,11 @@ let num_size = function
let vec_size = function
| V128Type -> 16

let value_size = function
| NumType t -> num_size t
| VecType t -> vec_size t
| RefType _ | BotType -> failwith "value_size"

let packed_size = function
| Pack8 -> 1
| Pack16 -> 2
Expand All @@ -88,11 +93,9 @@ let packed_size = function
let packed_shape_size = function
| Pack8x8 | Pack16x4 | Pack32x2 -> 8


let is_packed_storage_type = function
| ValueStorageType _ -> false
| PackedStorageType _ -> true

let storage_size = function
| PackedStorageType pt -> packed_size pt
| ValueStorageType t -> value_size t

let is_syn_var = function SynVar _ -> true | _ -> false
let is_sem_var = function SemVar _ -> true | _ -> false
Expand Down Expand Up @@ -132,6 +135,11 @@ let defaultable_value_type = function
| BotType -> assert false


let is_packed_storage_type = function
| ValueStorageType _ -> false
| PackedStorageType _ -> true


(* Projections *)

let unpacked_storage_type = function
Expand Down
3 changes: 3 additions & 0 deletions interpreter/text/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -547,6 +547,9 @@ let rec instr e =
"struct.get" ^ opt_s extension exto ^ " " ^ var x ^ " " ^ var y, []
| StructSet (x, y) -> "struct.set " ^ var x ^ " " ^ var y, []
| ArrayNew (x, op) -> "array.new" ^ initop op ^ " " ^ var x, []
| ArrayNewFixed (x, n) -> "array.new_fixed " ^ var x ^ " " ^ nat32 n, []
| ArrayNewElem (x, y) -> "array.new_elem " ^ var x ^ " " ^ var y, []
| ArrayNewData (x, y) -> "array.new_data " ^ var x ^ " " ^ var y, []
| ArrayGet (x, exto) -> "array.get" ^ opt_s extension exto ^ " " ^ var x, []
| ArraySet x -> "array.set " ^ var x, []
| ArrayLen -> "array.len", []
Expand Down
3 changes: 3 additions & 0 deletions interpreter/text/lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -296,6 +296,9 @@ rule token = parse

| "array.new" { ARRAY_NEW array_new }
| "array.new_default" { ARRAY_NEW array_new_default }
| "array.new_fixed" { ARRAY_NEW_FIXED }
| "array.new_elem" { ARRAY_NEW_ELEM }
| "array.new_data" { ARRAY_NEW_DATA }
| "array.get" { ARRAY_GET array_get }
| "array.get_"(sign as s) { ARRAY_GET (ext s array_get_s array_get_u) }
| "array.set" { ARRAY_SET }
Expand Down
10 changes: 9 additions & 1 deletion interpreter/text/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -272,7 +272,9 @@ let inline_func_type_explicit (c : context) x ft at =
%token REF_NULL REF_FUNC REF_I31 REF_DATA REF_ARRAY REF_EXTERN
%token REF_TEST REF_CAST REF_EQ
%token I31_NEW I32_GET
%token STRUCT_NEW STRUCT_GET STRUCT_SET ARRAY_NEW ARRAY_GET ARRAY_SET ARRAY_LEN
%token STRUCT_NEW STRUCT_GET STRUCT_SET
%token ARRAY_NEW ARRAY_NEW_FIXED ARRAY_NEW_ELEM ARRAY_NEW_DATA
%token ARRAY_GET ARRAY_SET ARRAY_LEN
%token RTT_CANON
%token VEC_LOAD VEC_STORE VEC_LOAD_LANE VEC_STORE_LANE
%token VEC_CONST VEC_UNARY VEC_BINARY VEC_TERNARY VEC_TEST
Expand Down Expand Up @@ -461,6 +463,9 @@ type_use :

/* Immediates */

nat32 :
| NAT { nat32 $1 (at ()) }

num :
| NAT { $1 @@ at () }
| INT { $1 @@ at () }
Expand Down Expand Up @@ -586,6 +591,9 @@ plain_instr :
| STRUCT_GET var var { fun c -> $1 ($2 c type_) ($3 c field) }
| STRUCT_SET var var { fun c -> struct_set ($2 c type_) ($3 c field) }
| ARRAY_NEW var { fun c -> $1 ($2 c type_) }
| ARRAY_NEW_FIXED var nat32 { fun c -> array_new_fixed ($2 c type_) $3 }
| ARRAY_NEW_ELEM var var { fun c -> array_new_elem ($2 c type_) ($3 c elem) }
| ARRAY_NEW_DATA var var { fun c -> array_new_data ($2 c type_) ($3 c data) }
| ARRAY_GET var { fun c -> $1 ($2 c type_) }
| ARRAY_SET var { fun c -> array_set ($2 c type_) }
| ARRAY_LEN { fun c -> array_len }
Expand Down
4 changes: 4 additions & 0 deletions interpreter/util/lib.ml
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,10 @@ end

module List32 =
struct
let rec init n f = init' n f []
and init' n f xs =
if n = 0l then xs else init' (Int32.sub n 1l) f (f (Int32.sub n 1l) :: xs)

let rec make n x = make' n x []
and make' n x xs =
if n = 0l then xs else make' (Int32.sub n 1l) x (x::xs)
Expand Down
1 change: 1 addition & 0 deletions interpreter/util/lib.mli
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ end

module List32 :
sig
val init : int32 -> (int32 -> 'a) -> 'a list
val make : int32 -> 'a -> 'a list
val length : 'a list -> int32
val nth : 'a list -> int32 -> 'a (* raises Failure *)
Expand Down
46 changes: 35 additions & 11 deletions interpreter/valid/valid.ml
Original file line number Diff line number Diff line change
Expand Up @@ -755,8 +755,8 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
let StructType fts = struct_type c x in
require
( initop = Explicit || List.for_all (fun ft ->
defaultable_value_type (unpacked_field_type ft)) fts ) e.at
("field type is not defaultable");
defaultable_value_type (unpacked_field_type ft)) fts ) x.at
"field type is not defaultable";
let ts = if initop = Implicit then [] else List.map unpacked_field_type fts in
(ts @ [RefType (NonNullable, RttHeapType (SynVar x.it))]) -->
[RefType (NonNullable, DefHeapType (SynVar x.it))]
Expand Down Expand Up @@ -784,12 +784,35 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
let ArrayType ft = array_type c x in
require
( initop = Explicit ||
defaultable_value_type (unpacked_field_type ft) ) e.at
("array type is not defaultable");
defaultable_value_type (unpacked_field_type ft) ) x.at
"array type is not defaultable";
let ts = if initop = Implicit then [] else [unpacked_field_type ft] in
(ts @ [NumType I32Type; RefType (NonNullable, RttHeapType (SynVar x.it))]) -->
[RefType (NonNullable, DefHeapType (SynVar x.it))]

| ArrayNewFixed (x, n) ->
let ArrayType ft = array_type c x in
let ts = Lib.List32.make n (unpacked_field_type ft) in
(ts @ [RefType (NonNullable, RttHeapType (SynVar x.it))]) -->
[RefType (NonNullable, DefHeapType (SynVar x.it))]

| ArrayNewElem (x, y) ->
let ArrayType ft = array_type c x in
let rt = elem c y in
require (match_value_type c.types (RefType rt) (unpacked_field_type ft)) x.at
("type mismatch: element segment's type " ^ string_of_ref_type rt ^
" does not match array's field type " ^ string_of_field_type ft);
[NumType I32Type; NumType I32Type; RefType (NonNullable, RttHeapType (SynVar x.it))] -->
[RefType (NonNullable, DefHeapType (SynVar x.it))]

| ArrayNewData (x, y) ->
let ArrayType ft = array_type c x in
let () = data c y in
require (is_num_type (unpacked_field_type ft)) x.at
"array type is not numeric";
[NumType I32Type; NumType I32Type; RefType (NonNullable, RttHeapType (SynVar x.it))] -->
[RefType (NonNullable, DefHeapType (SynVar x.it))]

| ArrayGet (x, exto) ->
let ArrayType (FieldType (st, _)) = array_type c x in
require ((exto <> None) == is_packed_storage_type st) e.at
Expand Down Expand Up @@ -953,11 +976,9 @@ let check_func (c : context) (f : func) =

let is_const (c : context) (e : instr) =
match e.it with
| Const _
| VecConst _
| I31New
| RefNull _
| RefFunc _
| Const _ | VecConst _
| RefNull _ | RefFunc _
| I31New | StructNew _ | ArrayNew _ | ArrayNewFixed _
| RttCanon _ -> true
| GlobalGet x -> let GlobalType (_, mut) = global c x in mut = Immutable
| _ -> false
Expand Down Expand Up @@ -1065,12 +1086,15 @@ let check_module (m : module_) =
funcs = c1.funcs @ List.map (fun f -> func_type c1 f.it.ftype) funcs;
tables = c1.tables @ List.map (fun tab -> tab.it.ttype) tables;
memories = c1.memories @ List.map (fun mem -> mem.it.mtype) memories;
refs = Free.module_ ({m.it with funcs = []; start = None} @@ m.at);
}
in
let c =
{ (List.fold_left check_global c2 globals) with
elems = List.map (fun elem -> elem.it.etype) elems;
datas = List.map (fun _data -> ()) datas;
refs = Free.module_ ({m.it with funcs = []; start = None} @@ m.at);
}
in
let c = List.fold_left check_global c2 globals in
List.iter (check_table c) tables;
List.iter (check_memory c) memories;
List.iter (check_elem c) elems;
Expand Down
Loading