Skip to content
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
4 changes: 2 additions & 2 deletions interpreter/exec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -755,7 +755,7 @@ let rec step (c : config) : config =
| StructGet (x, i, exto), Ref NullRef :: vs' ->
vs', [Trapping "null structure reference" @@ e.at]

| StructGet (x, i, exto), Ref Aggr.(StructRef (Struct (_, fs, _))) :: vs' ->
| StructGet (x, i, exto), Ref Aggr.(StructRef (Struct (_, _, fs))) :: vs' ->
let f =
try Lib.List32.nth fs i
with Failure _ -> Crash.error e.at "undefined field"
Expand All @@ -766,7 +766,7 @@ let rec step (c : config) : config =
| StructSet (x, i), v :: Ref NullRef :: vs' ->
vs', [Trapping "null structure reference" @@ e.at]

| StructSet (x, i), v :: Ref Aggr.(StructRef (Struct (_, fs, _))) :: vs' ->
| StructSet (x, i), v :: Ref Aggr.(StructRef (Struct (_, _, fs))) :: vs' ->
let f =
try Lib.List32.nth fs i
with Failure _ -> Crash.error e.at "undefined field"
Expand Down
8 changes: 4 additions & 4 deletions interpreter/runtime/aggr.ml
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ type field =
| ValField of value ref
| PackField of packtype * int ref

type struct_ = Struct of deftype * field list * ref_ option
type struct_ = Struct of deftype * ref_ option * field list
type array = Array of deftype * field list

type ref_ += StructRef of struct_
Expand Down Expand Up @@ -43,7 +43,7 @@ let array_length (Array (_, fs)) = Lib.List32.length fs
let alloc_struct dt vs desc =
assert Free.((deftype dt).types = Set.empty);
let fts = structtype_of_comptype (expand_deftype dt) in
Struct (dt, List.map2 alloc_field fts vs, desc)
Struct (dt, desc, List.map2 alloc_field fts vs)

let alloc_array dt vs =
assert Free.((deftype dt).types = Set.empty);
Expand All @@ -55,7 +55,7 @@ let type_of_struct (Struct (dt, _, _)) = dt
let type_of_array (Array (dt, _)) = dt

let read_desc = function
| StructRef (Struct (_, _, Some desc)) -> Some desc
| StructRef (Struct (_, Some desc, _)) -> Some desc
| _ -> None

let () =
Expand Down Expand Up @@ -87,6 +87,6 @@ let () =
let nest = ref 0 in
(* TODO: print descriptor *)
Value.string_of_ref' := function
| StructRef (Struct (_, fs, _)) -> string_of_aggr "struct" nest fs
| StructRef (Struct (_, _, fs)) -> string_of_aggr "struct" nest fs
| ArrayRef (Array (_, fs)) -> string_of_aggr "array" nest fs
| r -> string_of_ref' r
2 changes: 1 addition & 1 deletion interpreter/runtime/aggr.mli
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ type field =
| ValField of value ref
| PackField of packtype * int ref

type struct_ = Struct of deftype * field list * ref_ option
type struct_ = Struct of deftype * ref_ option * field list
type array = Array of deftype * field list

type ref_ += StructRef of struct_
Expand Down
84 changes: 71 additions & 13 deletions spectec/src/backend-interpreter/construct.ml
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ let error_instr category instr' =

(* Constant *)

let version = ref 3
let version = ref 4


(* Destruct *)
Expand Down Expand Up @@ -109,6 +109,11 @@ let al_to_mut: value -> mut = function
| OptV _ -> Var
| v -> error_value "mut" v

let al_to_exact: value -> exact = function
| OptV None -> Inexact
| OptV _ -> Exact
| v -> error_value "exact" v

let rec al_to_storagetype: value -> storagetype = function
| CaseV ("I8", []) -> PackStorageT I8T
| CaseV ("I16", []) -> PackStorageT I16T
Expand All @@ -127,8 +132,23 @@ and al_to_comptype: value -> comptype = function
| CaseV ("->", [ rt1; rt2 ]) -> FuncT (al_to_resulttype rt1, (al_to_resulttype rt2))
| v -> error_value "comptype" v

and al_to_desctype: value-> desctype = function
| v -> DescT (None, None, al_to_comptype v) (* TODO *)
and al_to_describes: value -> typeuse = function
| CaseV ("DESCRIBES", [ tu ]) -> al_to_typeuse tu
| v -> error_value "describes" v

and al_to_descriptor: value -> typeuse = function
| CaseV ("DESCRIPTOR", [ tu ]) -> al_to_typeuse tu
| v -> error_value "descriptor" v

and al_to_desctype: value -> desctype = function
| v when !version <= 3 -> DescT (None, None, al_to_comptype v)
| CaseV ("", [ dcs; dcr; ct ]) | TupV [ dcs; dcr; ct ] ->
DescT (
al_to_opt al_to_describes dcs,
al_to_opt al_to_descriptor dcr,
al_to_comptype ct
)
| v -> error_value "desctype" v

and al_to_subtype: value -> subtype = function
| CaseV ("SUB", [ fin; tul; st ]) ->
Expand Down Expand Up @@ -172,7 +192,10 @@ and al_to_heaptype: value -> heaptype = function
| "EXTERN" | "EXTERNREF" -> ExternHT
| "NOEXTERN" -> NoExternHT
| _ -> error_value "absheaptype" v)
| CaseV (("_IDX" | "REC" | "_DEF"), _) as v -> UseHT (Inexact, al_to_typeuse v) (* TODO: exactness *)
| CaseV ("_HT", [ CaseV ("", [ ex; tu ]) | TupV [ ex; tu ] ]) ->
UseHT (al_to_exact ex, al_to_typeuse tu)
| CaseV (("_IDX" | "REC" | "_DEF"), _) as v when !version <= 3 ->
UseHT (Inexact, al_to_typeuse v)
| v -> error_value "heaptype" v

and al_to_reftype: value -> reftype = function
Expand Down Expand Up @@ -792,6 +815,10 @@ and al_to_instr': value -> Ast.instr' = function
BrOnCast (al_to_idx idx, al_to_reftype rt1, al_to_reftype rt2)
| CaseV ("BR_ON_CAST_FAIL", [ idx; rt1; rt2 ]) ->
BrOnCastFail (al_to_idx idx, al_to_reftype rt1, al_to_reftype rt2)
| CaseV ("BR_ON_CAST_DESC_EQ", [ idx; rt1; rt2 ]) ->
BrOnCastDescEq (al_to_idx idx, al_to_reftype rt1, al_to_reftype rt2)
| CaseV ("BR_ON_CAST_DESC_EQ_FAIL", [ idx; rt1; rt2 ]) ->
BrOnCastDescEqFail (al_to_idx idx, al_to_reftype rt1, al_to_reftype rt2)
| CaseV ("RETURN", []) -> Return
| CaseV ("CALL", [ idx ]) -> Call (al_to_idx idx)
| CaseV ("CALL_REF", [ typeuse ]) -> CallRef (al_to_idx_of_typeuse typeuse)
Expand Down Expand Up @@ -822,6 +849,8 @@ and al_to_instr': value -> Ast.instr' = function
| CaseV ("REF.AS_NON_NULL", []) -> RefAsNonNull
| CaseV ("REF.TEST", [ rt ]) -> RefTest (al_to_reftype rt)
| CaseV ("REF.CAST", [ rt ]) -> RefCast (al_to_reftype rt)
| CaseV ("REF.CAST_DESC_EQ", [ rt ]) -> RefCastDescEq (al_to_reftype rt)
| CaseV ("REF.GET_DESC", [ idx ]) -> RefGetDesc (al_to_idx idx)
| CaseV ("REF.EQ", []) -> RefEq
| CaseV ("REF.I31", []) -> RefI31
| CaseV ("I31.GET", [ sx ]) -> I31Get (al_to_sx sx)
Expand Down Expand Up @@ -916,7 +945,10 @@ let al_to_data': value -> data' = function
let al_to_data: value -> data = al_to_phrase al_to_data'

let al_to_externtype = function
| CaseV ("FUNC", [typeuse]) -> ExternFuncT (Inexact, al_to_typeuse typeuse) (* TODO: exactness *)
| CaseV ("FUNC", [ typeuse ]) when !version <= 3 ->
ExternFuncT (Inexact, al_to_typeuse typeuse)
| CaseV ("FUNC", [ CaseV ("", [ ex; tu ]) | TupV [ ex; tu ] ]) ->
ExternFuncT (al_to_exact ex, al_to_typeuse tu)
| CaseV ("GLOBAL", [globaltype]) -> ExternGlobalT (al_to_globaltype globaltype)
| CaseV ("TABLE", [tabletype]) -> ExternTableT (al_to_tabletype tabletype)
| CaseV ("MEM", [memtype]) -> ExternMemoryT (al_to_memorytype memtype)
Expand Down Expand Up @@ -990,10 +1022,15 @@ and al_to_array: value -> Aggr.array = function

and al_to_struct: value -> Aggr.struct_ = function
| StrV r when Record.mem "TYPE" r && Record.mem "FIELDS" r ->
let desc =
if Record.mem "DESC" r then
al_to_opt (fun a -> al_to_ref (CaseV ("REF.STRUCT_ADDR", [ a ]))) (Record.find "DESC" r)
else None
in
Aggr.Struct (
al_to_deftype (Record.find "TYPE" r),
al_to_list al_to_field (Record.find "FIELDS" r),
None (* TODO: descriptors *)
desc,
al_to_list al_to_field (Record.find "FIELDS" r)
)
| v -> error_value "struct" v

Expand Down Expand Up @@ -1131,6 +1168,10 @@ let al_of_mut = function
| Cons -> none "MUT"
| Var -> some "MUT"

let al_of_exact = function
| Inexact -> none "EXACT"
| Exact -> some "EXACT"

let rec al_of_storagetype = function
| ValStorageT vt -> al_of_valtype vt
| PackStorageT _ as st -> nullary (string_of_storagetype st)
Expand All @@ -1145,8 +1186,18 @@ and al_of_comptype = function
| ArrayT ft -> CaseV ("ARRAY", [ al_of_fieldtype ft ])
| FuncT (rt1, rt2) -> CaseV ("->", [ al_of_resulttype rt1; al_of_resulttype rt2 ])

and al_of_describes tu = CaseV ("DESCRIBES", [ al_of_typeuse tu ])

and al_of_descriptor tu = CaseV ("DESCRIPTOR", [ al_of_typeuse tu ])

and al_of_desctype = function
| DescT (_, _, ct) -> al_of_comptype ct (* TODO *)
| DescT (_, _, ct) when !version <= 3 -> al_of_comptype ct
| DescT (dcs, dcr, ct) ->
CaseV ("", [
al_of_opt al_of_describes dcs;
al_of_opt al_of_descriptor dcr;
al_of_comptype ct;
])

and al_of_subtype = function
| SubT (fin, tul, st) ->
Expand All @@ -1169,7 +1220,9 @@ and al_of_typeuse_of_idx = function
| idx -> CaseV ("_IDX", [ al_of_idx idx ])

and al_of_heaptype = function
| UseHT (_, tu) -> al_of_typeuse tu (* TODO: exactness *)
| UseHT (_, tu) when !version <= 3 -> al_of_typeuse tu
| UseHT (ex, tu) ->
CaseV ("_HT", [ CaseV ("", [ al_of_exact ex; al_of_typeuse tu ]) ])
| BotHT -> nullary "BOT"
| FuncHT | ExternHT as ht when !version <= 2 ->
string_of_heaptype ht ^ "REF" |> nullary
Expand Down Expand Up @@ -1833,7 +1886,7 @@ let rec al_of_instr instr =
let args = (if !version = 1 then [] else [ al_of_idx idx1 ]) @ [ al_of_typeuse_of_idx idx2 ] in
CaseV ("CALL_INDIRECT", args)
| ReturnCall idx -> CaseV ("RETURN_CALL", [ al_of_idx idx ])
| ReturnCallRef idx -> CaseV ("RETURN_CALL_REF", [ al_of_idx idx ])
| ReturnCallRef idx -> CaseV ("RETURN_CALL_REF", [ al_of_typeuse_of_idx idx ])
| ReturnCallIndirect (idx1, idx2) ->
CaseV ("RETURN_CALL_INDIRECT", [ al_of_idx idx1; al_of_typeuse_of_idx idx2 ])
| Throw idx -> CaseV ("THROW", [ al_of_idx idx ])
Expand Down Expand Up @@ -1864,8 +1917,10 @@ let rec al_of_instr instr =
| RefEq -> nullary "REF.EQ"
| RefI31 -> nullary "REF.I31"
| I31Get sx -> CaseV ("I31.GET", [ al_of_sx sx ])
| StructNew (idx, Explicit, _) -> CaseV ("STRUCT.NEW", [ al_of_idx idx ]) (* TODO(tlively): descriptors *)
| StructNew (idx, Implicit, _) -> CaseV ("STRUCT.NEW_DEFAULT", [ al_of_idx idx ]) (* TODO(tlively): descriptors *)
| StructNew (idx, Explicit, NoDesc) -> CaseV ("STRUCT.NEW", [ al_of_idx idx ])
| StructNew (idx, Implicit, NoDesc) -> CaseV ("STRUCT.NEW_DEFAULT", [ al_of_idx idx ])
| StructNew (idx, Explicit, Desc) -> CaseV ("STRUCT.NEW_DESC", [ al_of_idx idx ])
| StructNew (idx, Implicit, Desc) -> CaseV ("STRUCT.NEW_DEFAULT_DESC", [ al_of_idx idx ])
| StructGet (idx1, idx2, sx_opt) ->
CaseV ("STRUCT.GET", [
al_of_opt al_of_sx sx_opt;
Expand Down Expand Up @@ -1988,7 +2043,10 @@ let al_of_data data =


let al_of_externtype = function
| ExternFuncT (_, typeuse) -> CaseV ("FUNC", [al_of_typeuse typeuse]) (* TODO: exactness *)
| ExternFuncT (_, typeuse) when !version <= 3 ->
CaseV ("FUNC", [ al_of_typeuse typeuse ])
| ExternFuncT (ex, typeuse) ->
CaseV ("FUNC", [ CaseV ("", [ al_of_exact ex; al_of_typeuse typeuse ]) ])
| ExternGlobalT (globaltype) -> CaseV ("GLOBAL", [al_of_globaltype globaltype])
| ExternTableT (tabletype) -> CaseV ("TABLE", [al_of_tabletype tabletype])
| ExternMemoryT (memtype) -> CaseV ("MEM", [al_of_memorytype memtype])
Expand Down
6 changes: 5 additions & 1 deletion spectec/src/backend-interpreter/host.ml
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,14 @@ let spectest () =
let ptype = Array.map nullary type_tags in
let arrow = CaseV ("->", [ listV ptype; listV [||] ]) in
let ftype = CaseV ("->", [ listV ptype; listV [||] ]) in
let desctype =
if !Construct.version <= 3 then ftype
else CaseV ("", [ none "DESCRIBES"; none "DESCRIPTOR"; ftype ])
in
let dtype =
CaseV ("_DEF", [
CaseV ("REC", [
[| CaseV ("SUB", [some "FINAL"; listV [||]; ftype]) |] |> listV
[| CaseV ("SUB", [some "FINAL"; listV [||]; desctype]) |] |> listV
]); natV Z.zero
]) in
let tidx = CaseV ("", [ natV Z.zero ]) in
Expand Down
8 changes: 8 additions & 0 deletions spectec/src/backend-interpreter/interpreter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -192,6 +192,9 @@ and check_type ty v expr =
(* absheaptype *)
| CaseV (aht, []) when List.mem aht abs_heaptypes ->
boolV (ty = "absheaptype" || ty = "heaptype")
(* concrete heaptype *)
| CaseV ("_HT", [ _ ]) ->
boolV (ty = "heaptype")
(* deftype *)
| CaseV ("_DEF", [ _; _ ]) ->
boolV (ty = "heaptype" || ty = "typeuse" || ty = "deftype")
Expand All @@ -201,6 +204,11 @@ and check_type ty v expr =
(* heaptype *)
| CaseV ("REC", [ _ ]) ->
boolV (ty = "heaptype" || ty = "typeuse" || ty = "typevar")
(* exactdeftype / exacttypeuse *)
| CaseV ("", [ OptV _; CaseV ("_DEF", [ _; _ ]) ]) ->
boolV (ty = "exactdeftype" || ty = "exacttypeuse")
| CaseV ("", [ OptV _; CaseV (("_IDX" | "REC"), [ _ ]) ]) ->
boolV (ty = "exacttypeuse")
(* packval *)
| CaseV ("PACK", CaseV (pt, [])::_) when List.mem pt pnn_types ->
boolV (ty = "val")
Expand Down
16 changes: 13 additions & 3 deletions spectec/src/backend-interpreter/relation.ml
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,11 @@ let ref_ok =
let field_name = String.sub name 4 (String.length name - 9) in
let object_ = listv_nth (Ds.Store.access (field_name ^ "S")) (Z.to_int i) in
let dt = strv_access "TYPE" object_ in
CaseV ("REF", [ nonull; dt])
let ht =
if !Construct.version <= 3 then dt
else CaseV ("_HT", [ CaseV ("", [ some "EXACT"; dt ]) ])
in
CaseV ("REF", [ nonull; ht ])
(* extern *)
(* TODO: check null *)
| CaseV ("REF.EXTERN", [ _ ]) -> CaseV ("REF", [ nonull; nullary "EXTERN"])
Expand All @@ -44,7 +48,7 @@ let ref_ok =
| vs -> Numerics.error_values "$Ref_ok" vs

let module_ok v =
if !Construct.version <> 3 then failwith "This hardcoded function ($Module_ok) should be only called with test version 3.0";
if !Construct.version < 3 then failwith "This hardcoded function ($Module_ok) should be only called with test version >= 3.0";
match v with
| [ m ] ->
(try
Expand All @@ -68,7 +72,13 @@ let externaddr_ok = function
|> unwrap_listv_to_array
|> fun arr -> Array.get arr addr
|> strv_access "TYPE"
|> fun type_ -> CaseV (name, [type_])
|> fun type_ ->
let arg =
if name = "FUNC" && !Construct.version > 3 then
CaseV ("", [ some "EXACT"; type_ ])
else type_
in
CaseV (name, [ arg ])
|> Construct.al_to_externtype
in
let externtype = Construct.al_to_externtype t in
Expand Down
5 changes: 3 additions & 2 deletions spectec/src/backend-interpreter/runner.ml
Original file line number Diff line number Diff line change
Expand Up @@ -200,14 +200,14 @@ let test_assertion assertion =
| exception Exception.Throw -> success
| _ -> Assert.error assertion.at "expected exception"
)
| AssertInvalid (def, re) when !Construct.version = 3 ->
| AssertInvalid (def, re) when !Construct.version >= 3 ->
(match def |> module_of_def |> instantiate |> ignore with
| exception Exception.Invalid _ -> success
| _ ->
Run.assert_message assertion.at "validation" "module instance" re;
fail
)
| AssertInvalidCustom (def, re) when !Construct.version = 3 ->
| AssertInvalidCustom (def, re) when !Construct.version >= 3 ->
(match def |> module_of_def |> instantiate |> ignore with
| exception Exception.Invalid _ -> success
| _ ->
Expand Down Expand Up @@ -371,6 +371,7 @@ and run_dir path =
path
|> Sys.readdir
|> Array.to_list
|> List.filter (fun filename -> not (!Construct.version <= 3 && filename = "custom-descriptors"))

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a bit of a hack. wasm-latest still mirrors wasm-3.0 and they use the same test directory, but wasm-3.0 cannot run the custom descriptors tests. Maybe we need to start mirroring the tests into a separate "latest" directory that proposals can update, similar to what we do for the .spectec sources.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, good point. Though unlike with the specs, we do not keep the old versions of the test suite around (maybe we should?). So it's less clear what should happen when merging the feature.

Alternatively, instead of hard-coding a single test name inline here, perhaps add some kind of blacklist that is easier to update?

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll land this for now, but I'm happy to adopt a different scheme here if you decide on one. I don't have a strong feeling about what is best. I guess it's not the end of the world if each new proposal just adds this line to skip its own tests if necessary.

|> List.sort compare
|> List.map (fun filename -> run_file (Filename.concat path filename) [])
|> sum_results_with_time
Expand Down
2 changes: 1 addition & 1 deletion spectec/src/exe-spectec/main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@ let argspec = Arg.align (
] @ List.map pass_argspec all_passes @ [
"--all-passes", Arg.Unit (fun () -> List.iter enable_pass all_passes)," Run all passes";

"--test-version", Arg.Int (fun i -> Backend_interpreter.Construct.version := i; Il2al.Translate.version := i), " Wasm version to assume for tests (default: 3)";
"--test-version", Arg.Int (fun i -> Backend_interpreter.Construct.version := i; Il2al.Translate.version := i), " Wasm version to assume for tests (default: 4)";

"-help", Arg.Unit ignore, "";
"--help", Arg.Unit ignore, "";
Expand Down
9 changes: 8 additions & 1 deletion spectec/src/il2al/postprocess.ml
Original file line number Diff line number Diff line change
Expand Up @@ -93,9 +93,16 @@ let split_iter s =
String.sub s 0 last, String.sub s last (len - last)

let replace_name old_name new_name algo =
let replace_name' walker e =
let replace_name' (walker: Walk.walker) e =

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AI explanation of why this change is necessary:

simplify_var_name in postprocess.ml renames suffixed variables (such as dcs_0 -> dcs in $subst_desctype) across an AL algorithm using replace_name. Previously, replace_name relied solely on Walk.base_walker.walk_expr, which for IterE (inner_e, (iter, xes)) walks inner_e and the RHS expressions in xes : (id * expr) list, but not the LHS bound variable string x ("dcs_0"), leaving dcs?{dcs_0 <- dcs?}. When backend-interpreter executed that IterE, it bound "dcs_0" in the environment and then evaluated inner_e (VarE "dcs"), failing with an unbound variable error. Updating replace_name to also rename matching keys x in xes fixes this.

Someone with more context will have to say whether that makes sense.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds plausible at least.

match e.it with
| VarE x when x = old_name -> {e with it = VarE new_name}
| IterE (inner_e, (iter, xes)) ->
let xes' =
List.map
(fun (x, e) -> (if x = old_name then new_name else x), walker.walk_expr walker e)
xes
in
{e with it = IterE (walker.walk_expr walker inner_e, (walker.walk_iter walker iter, xes'))}
| _ -> Walk.base_walker.walk_expr walker e
in
let walker = {Walk.base_walker with walk_expr = replace_name'} in
Expand Down
2 changes: 1 addition & 1 deletion spectec/src/il2al/translate.ml
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ struct
include Print
end

let version = ref 3
let version = ref 4


(* Errors *)
Expand Down
Loading
Loading