Fix spec #50
Fix spec #50
Conversation
| @@ -116,8 +116,7 @@ rule Step_read/call: | |||
| rule Step_read/call_indirect-call: | |||
| z; (CONST I32 i) (CALL_INDIRECT x) ~> (CALL_ADDR a) | |||
| -- if $table(z, 0).ELEM[i] = a | |||
| -- if $funcinst(z)[a].CODE = FUNC x' (LOCAL t)* instr* | |||
| -- if $type(z, x) = $type(z, x') | |||
There was a problem hiding this comment.
This is problematic when the function instance is an imported function.
In that case, x' is a type index for the imported module, but $type(z, x') returns a x'th type in the current module.
|
|
||
| def $instantiate(store, module, externval*) : config | ||
| def $instantiate(s, module, externval*) = s'; f; (CALL x')? | ||
| def $instantiate(s, module, externval*) = s'''; f; (CALL x')? |
There was a problem hiding this comment.
The store should be propagated through initializing elems and datas, thus s''' here.
(Perhaps s_3 will be better?)
There was a problem hiding this comment.
I'm fine with changing this to s_N.
| -- if f_init = { LOCAL epsilon, MODULE mm_init } | ||
| -- if z = s; f_init | ||
| -- (Eval_expr : z; expr_G ~>* z; val)* | ||
| -- (Eval_expr : z; expr_E ~>* z; (CONST I32 i_E))* | ||
| -- (Eval_expr : z; expr_D ~>* z; (CONST I32 i_D))* | ||
| -- if (s', mm) = $allocmodule(s, module, externval*, val*) | ||
| -- if s'' = $initelem(s', mm.TABLE[0], i_E*, mm.FUNC[x]**) | ||
| -- if s''' = $initdata(s'', mm.MEM[0], i_D*, b**) |
There was a problem hiding this comment.
mm.TABLE[0] (or mm.MEM[0]) may result in out-of-index error, especially if elem* (or data*) is empty. I had to pass the entire module instance mm as an argument to the initelem (or initdata), but perhaps there might be a better way?
There was a problem hiding this comment.
That was working as intended: it is an error to define a segment when no memory/table is present, even if the segment's length is 0. (And it's actually a validation error already.)
There was a problem hiding this comment.
The problem here is that, the premise
-- if s'' = $initelem(s', mm.TABLE[0], i_E*, mm.FUNC[x]**)
implies the side condition |mm.TABLE| > 0, regardless of whether element is present or not.
In other words, the result of the function $instantiate would not be defined for the given module
(module)
In contrast, in the changed version, the side condition |mm.TABLE| > 0 is implied only if element is present.
There was a problem hiding this comment.
Oh, I see! Yeah, I don't know how to do it more elegantly than your change then.
| -- if f_init = { LOCAL epsilon, MODULE mm_init } | ||
| -- if z = s; f_init | ||
| -- (Eval_expr : z; expr_G ~>* z; val)* | ||
| -- (Eval_expr : z; expr_E ~>* z; (CONST I32 i_E))* | ||
| -- (Eval_expr : z; expr_D ~>* z; (CONST I32 i_D))* | ||
| -- if (s', mm) = $allocmodule(s, module, externval*, val*) | ||
| -- if s'' = $initelem(s', mm.TABLE[0], i_E*, mm.FUNC[x]**) | ||
| -- if s''' = $initdata(s'', mm.MEM[0], i_D*, b**) |
There was a problem hiding this comment.
That was working as intended: it is an error to define a segment when no memory/table is present, even if the segment's length is 0. (And it's actually a validation error already.)
|
|
||
| def $instantiate(store, module, externval*) : config | ||
| def $instantiate(s, module, externval*) = s'; f; (CALL x')? | ||
| def $instantiate(s, module, externval*) = s'''; f; (CALL x')? |
There was a problem hiding this comment.
I'm fine with changing this to s_N.
| @@ -116,8 +116,7 @@ rule Step_read/call: | |||
| rule Step_read/call_indirect-call: | |||
| z; (CONST I32 i) (CALL_INDIRECT x) ~> (CALL_ADDR a) | |||
| -- if $table(z, 0).ELEM[i] = a | |||
| -- if $funcinst(z)[a].CODE = FUNC x' (LOCAL t)* instr* | |||
| -- if $type(z, x) = $type(z, x') | |||
Update readme to link to the two active stack-switching proposals
This PR fixes spec for Wasm 1 and 2, especially regarding module instantiation and
call_indirect.