Valstack Bug

[QianyangPeng]

I have a test case:

(module
  (func (export "unmatch") (result i32) (i64.const 700))
)

(invoke "unmatch")
#assertTopStackExactly < i32 > 123 "dummy test 1"
#assertTopStack < i32 > 456 "dummy test 1"

#clearConfig

The return type of function "unmatch" is not matched with the top of stack, so instead of returning a value, it will keep a #take ( i32 .ValTypes , < i64 > 700 : .ValStack ) ++ .ValStack on the <valstack>.

The interesting thing is that when using Java backend if the <valstack> is at the state above, any stack assertion will pass no matter what value you assert, therefore all assertions becomes useless.

Also, the output of the program above with Ocaml backend is also abnormal. All it outputs is:

#take ( i32  .ValTypes , < i64 > 700 : .ValStack )

, but I think it should output the whole configuration.

[hjorthjort]

It's not really a bug since the module is invalid, and we only deal with valid modules. If we decide to deal with this, we should go over the "Validation" chapter of the spec and figure out how to integrate it with our semantics. But I prefer if we assume we only deal with valid modules.

The way the Ocaml backend stops here is what it always does for functions with unmatched patterns. I don't like it either, but I don't know if it's easy/worth fixing. My guess is that it's because it's called as a function, with no configuration getting passed to the function, so when it halts there the configuration isn't available.

The fact that the Java backend passes all assertions is weird and more serious. I'd be interested if you could figure out why. The Java backend is still used for proving. Don't know if it's deprecated, though.

[QianyangPeng]

@hjorthjort Well, It is not a bug if you can make sure that all your semantics are bug-free, which means a type un-match error can never happen in a valid program. But can we really assume that? The bug is that current assertion does not work correctly.

For example if you have a valid program:

(module
  (func (export "unmatch") (result i32) (i32.wrap_i64 (i64.const 700)))
)

(invoke "unmatch")
#assertTopStackExactly < i32 > 700 "dummy test 1"

#clearConfig

If our implementation for i32.wrap_i64 is buggy, and it just returns the parameter itself without doing any conversion. The problem is that our test case cannot detect this bug and just returns a clean configuration.

[hjorthjort]

Hmm, I see your point. The problem is that the semantics are written in a way that assumes the module is valid. In the example you gave, the ad-hoc typechecking in #take will mean that you get stuck in the way you described, for example, which is fine, because we are free to do whatever when the module is invalid.

The second example you gave is important, and indeed, it would be a problem if we passed the assertion there. But if I understand you correctly, we get stuck on #take, right? Getting stuck on a function (or getting stuck anywhere) is sort of like the program "crashing", which is okay behavior for invalid modules, and bad behavior for valid modules (meaning there's a bug in the semantics).

So if I understand correctly, if you change the rule i32.wrap_i64 to just do nothing, we still pass the tests? Is that just in the Java backend or in the OCaml backend as well?

[QianyangPeng]

Only Java backend has this problem. If the top of stack is #take, any stack related assertion will pass.
For Ocaml it will not pass.

[hjorthjort]

Still reproducing this. I changed the implementation of i32.wrap_i64 so that it's an identity function, then ran this program:

(module
  (func (export "unmatch") (result i32) (i32.wrap_i64 (i64.const 700)))
)

(invoke "unmatch")
#assertTopStackExactly < i32 > 700 "dummy test 1"

The output is:

<wasm>        
  <k>       
    .            
  </k>          
  <valstack>      
    #take ( i32  .ValTypes , < i64 > 700 : .ValStack ) ++ .ValStack
  </valstack> 
  <curFrame>  
    <locals>      
      .Map      
    </locals>      
    <localIds>   
      .Map                   
    </localIds>
    <curModIdx>               
      0            
    </curModIdx>
    <labelDepth>    
      0            
    </labelDepth>                                                                                                                 
    <labelIds>                                                   
      .Map
    </labelIds>
  </curFrame>
  <moduleRegistry>
    .Map
  </moduleRegistry>
  <moduleIds>
    .Map
  </moduleIds>
  <moduleInstances>
    <modIdx>
      0
    </modIdx> |-> <moduleInst>
      <modIdx>
        0
      </modIdx>
      <exports>
        "unmatch" |-> #freshId ( 0 )
      </exports>
      <typeIds>
        .Map
      </typeIds>
      <types>
        0 |-> [ .ValTypes ] -> [ i32  .ValTypes ]
      </types>
      <nextTypeIdx>
        1
      </nextTypeIdx>
      <funcIds>
        #freshId ( 0 ) |-> 0
      </funcIds>
      <funcAddrs>
        0 |-> 0
      </funcAddrs>
      <nextFuncIdx>
        1
      </nextFuncIdx>
      <tabIds>
        .Map
      </tabIds>
      <tabAddrs>
        .Map
      </tabAddrs>
      <memIds>
        .Map
      </memIds>
      <memAddrs>
        .Map
      </memAddrs>
      <globIds>
        .Map
      </globIds>
      <globalAddrs>
        .Map
      </globalAddrs>
      <nextGlobIdx>
        0
      </nextGlobIdx>
    </moduleInst>
  </moduleInstances>
  <nextModuleIdx>
    1
  </nextModuleIdx>
  <mainStore>
    <funcs>
      <fAddr>
        0
      </fAddr> |-> <funcDef>
        <fAddr>
          0
        </fAddr>
        <fCode>
          ( i32 . wrap_i64 ( i64 . const 700 )  .EmptyStmts )  .EmptyStmts
        </fCode>
        <fType>
          [ .ValTypes ] -> [ i32  .ValTypes ]
        </fType>
        <fLocal>
          [ .ValTypes ]
        </fLocal>
        <fModInst>
          0
        </fModInst>
      </funcDef>
    </funcs>
    <nextFuncAddr>
      1
    </nextFuncAddr>
    <tabs>
      .Map
    </tabs>
    <nextTabAddr>
      0
    </nextTabAddr>
    <mems>
      .Map
    </mems>
    <nextMemAddr>
      0
    </nextMemAddr>
    <globals>
      .Map
    </globals>
    <nextGlobAddr>
      0
    </nextGlobAddr>
  </mainStore>
  <deterministicMemoryGrowth>
    true
  </deterministicMemoryGrowth>
  <nextFreshId>
    1
  </nextFreshId>
</wasm>