|
|
|
Host Functions Invoking a has non-deterministic behavior. It may either terminate with a or return regularly. However, in the latter case, it must consume and produce the right number and types of WebAssembly on the stack, according to its A host function may also modify the . However, all store modifications must result in an of the original store, i.e., they must only modify mutable contents and must not have instances removed. Furthermore, the resulting store must be , i.e., all data and code in it is well-typed. 𝑆 𝑎 ) 𝑆 ′ ( if 𝑆. 𝑎 ] = [ 𝑡 𝑛 1 [ 𝑡 𝑚 2 ] hf } ∧ ( 𝑆 ′ ∈ hf ( 𝑆 )) 𝑆 𝑎 ) 𝑆 𝑎 ) ( if 𝑆. 𝑎 ] = [ 𝑡 𝑛 1 [ 𝑡 𝑚 2 ] hf } ∧ ⊥ ∈ hf ( 𝑆 )) Here, hf ( 𝑆 ) denotes the implementation-defined execution of host function hf in current store 𝑆 with argu- ments . It yields a set of possible outcomes, where each element is either a pair of a modified store 𝑆 ′ and a or the special value ⊥ indicating divergence. A host function is non-deterministic if there is at least one argument for which the set of outcomes is not singular. in the presence of host functions, every must be , which means that it adheres to suitable pre- and post-conditions: under a 𝑆 , and given arguments matching the ascribed parameter types 𝑡 𝑛 1 , executing the host function must yield a non-empty set of possible outcomes each of which is either divergence or consists of a valid store 𝑆 ′ that is an of 𝑆 and a result matching the ascribed return types 𝑡 𝑚 2 . All these notions are made precise in the Note: A host function can call back into WebAssembly by a function from a . However, the effects of any such call are subsumed by the non-deterministic behavior allowed for the host function. 4.4.11 Expressions An is evaluated relative to a pointing to its containing 1. Jump to the start of the instruction sequence of the expression. 2. Execute the instruction sequence. , the top of the stack contains a 4. Pop the from the stack. The value is the result of the evaluation. 𝑆 ; 𝐹 𝑆 ′ ; 𝐹 ′ ( if 𝑆 ; 𝐹 𝑆 ′ ; 𝐹 ′ Note: Evaluation iterates this reduction rule until reaching a value. Expressions constituting bodies are executed during function 4.4. Instructions 119 |