Joseph (Mar 06 2025 at 19:57): Joseph (Mar 06 2025 at 19:57):I'm working on formally verifying that winch specific code (codegen context, masm, asm) is panic free. Is this something that anyone else has worked on/interested in working on?
Joseph (Mar 06 2025 at 19:58):Through this exercise, I've noticed that some properties have a run time check while others do not. For example, when adding two values, there is a check that ensures the dst register is different from the lhs register. However, there isn't a check to ensure that the operand size and the register size are compatible. What is the thinking behind this?
Saúl Cabrera (Mar 06 2025 at 20:58):Hi @Joseph , I did an initial pass on ensuring that the error reporting infrastructure is recoverable in certain scenarios e.g, returning a recoverable error when reaching an unsupported Wasm instruction for example rather than panicking. That said though, there are cases in which a panic is probably the right thing to do, like when a compilation or register allocation invariant is broken (here's the PR for reference https://github.com/bytecodealliance/wasmtime/pull/9851)
For example, when adding two values, there is a check that ensures the dst register is different from the lhs register. However, there isn't a check to ensure that the operand size and the register size are compatible. What is the thinking behind this?
The main motivation for this is the design behind the MacroAssembler (assuming that this is what you're referring to); we have a design that makes it relatively easy to accommodate architectures that use three-argument-form (e.g., RISC-V, ARM64, etc), so we have those checks to ensure that the callers aren't mistakenly passing wrong argument forms, however, those checks are pretty currently specific to x64 IIRC.
Regarding the relationship between operand size and registers, a couple of things to take into account: (i) it's the operand size that drives how a particular instruction will use the bits of a given register (ii) registers don't have a explicit notion of size, generally speaking the number of bits available will be determined by the architecture type, in this case it's assumed to be 64-bits/128-bits but in the future this could as well be 32-bits, but all those details are encapsulated at the MacroAssembler level, which is meant to be ISA-specific and not something to be dictated by the MacroAssembler consumers (iii) Winch has a notion of TypedReg which is ISA-agnostic and helps validate the semantics of certain operations (e.g., extend, wrap'), but this concept doesn't reach and should probably never reach the MacroAssembler layer.
Saúl Cabrera (Mar 06 2025 at 21:06):One thing worth clarifying though: my work on improving the error infrastructure is not "formal" by any means. It came mostly from a need for a better integration story with our testing and fuzzing infrastructure.
Joseph (Mar 06 2025 at 21:08):I can understand that. Would the cases where a signed division, for example, is expected to operate on 64bit TypedRegisters and returns a 32bit TypedReg be detected at the parser level?
Joseph (Mar 06 2025 at 21:11):The logic behind the encapsulation and separation of concerns makes sense. I'm looking at things from the perspective of formally verifying the sequence of calls, hence the specific questions! Your distinction between internal and external errors, for example, is an interesting starting point since it helps build an intuition for the expected behaviour of winch
Saúl Cabrera (Mar 06 2025 at 21:17):for example, is expected to operate on 64bit TypedRegisters and returns a 32bit TypedReg be detected at the parser level?
Since Winch is very specific to Wasm ( and not a general purpose code generator), our lowering rules are pretty much tied to the Wasm semantics, and many of the concepts introduced at the MacroAssembler layer try to accommodate those semantics through an ISA-agnostic interface. For example the case of division: in some architectures, division requires specific registers to be used, so in order to meet that requirement without potentially affecting the lowering of other architectures that don't have such constraint you'll notice that the signature doesn't match one-to-one to the instruction and instead we pass in the register allocation infrastructure so that each ISA implementation can decide with what registers they'd like to work with to lower a particular Wasm instruction.
Graydon Hoare (Apr 12 2025 at 06:22):hey @Saúl Cabrera I've been helping @Joseph here a bit with his work on formal verification of properties of winch (initially fairly shallow ones like "panic freedom", but the structure of the "unit proofs" is fairly general and anything you can write as an assert is potentially fair game) .. and we've been wondering if the work would ultimately be of any interest to y'all upstream.
there's a little bit of adaptation work required to make the codebase amenable to the tool he's using -- finitizing and hard-wiring some stuff, swapping in mocks / stubs or compiling-out areas not under investigation, probably mostly changes that could be gated by a separate --feature flag and/or some extra targets -- but .. in theory it seems like it could be an interesting or valuable addition to your CI / QA processes. if you're interested!
Saúl Cabrera (Apr 14 2025 at 12:43):Hi @Graydon Hoare from a correctness and robustness point of view I agree that some form of verification sounds appealing and I think it might make sense to explore what would it take to potentially upstream this work. That said, I think that as a first step, it would be beneficial to discuss more concretely, ideally through an issue, the main changes that you're proposing (if the changes are major, we could as well consider creating an RFC https://github.com/bytecodealliance/rfcs). Personally, I'd like to understand a bit more how these changes will play with the current architecture of the compiler, mainly around the maintainability and performance aspects.
Last updated: Dec 06 2025 at 06:05 UTC