Stream: general

Topic: Loop validation

BC (Apr 26 2020 at 00:15):

Hello. I was surprised that this program validates because it adds one i32 to the stack on every iteration. I had assumed that the conditional branch to the start of the loop would be disallowed with that i32 on the stack. I thought I might be able to reach a stack limit by running the program with a large initial counter, but wasmtime ran it successfully. I am still trying to decipher the spec's validation formalism. Could anyone confirm that this program is OK, and whether the runtime optimizes away the extra i32 on the stack or something else happens? TIA

(module
 (func $start (export "_start") (result i32)
   (local $counter i32)
   (local.set $counter (i32.const 0xFFFFFFFF))
   loop $repeat (result i32)
     (local.get $counter)
     (local.set $counter (i32.sub (local.get $counter) (i32.const 1)))
     (br_if $repeat (local.get $counter))
   end
 )
)

Dan Gohman (Apr 26 2020 at 01:39):

when br_if takes the branch, it implicitly pops values off the stack to reset it to the depth it was at when the loop was entered

Dan Gohman (Apr 26 2020 at 01:39):

when it falls through, it doesn't, and that extra value on the stack becomes the loop result value

BC (Apr 26 2020 at 01:44):

Great, thank you! I see the execution semantics for br_if / br now.

Dan Gohman (Apr 26 2020 at 01:45):

Wasm's stack is constrained such that you can always match a push to its corresponding pop at compile time. At every instruction, the depth of the stack and the types of all the elements are known at compile time.

BC (Apr 26 2020 at 01:53):

Thanks, yes. A long time ago I was familiar with JVM bytecode verification (but I can't remember whether it allowed a reset like that).

Last updated: Dec 23 2024 at 13:07 UTC