Stream: git-wasmtime

Topic: wasmtime / issue #5700 Cranlift/ISLE: precise semantics f...

Wasmtime GitHub notifications bot (Feb 03 2023 at 18:43):

avanhatt opened issue #5700:

Feature

In verification conversations, it’s come up that we don’t have a precise semantics for the underlying u64 when a CLIF iconst has a narrow type (i.e., i8). Should the narrow constant be sign-extended, should it be zero-extended, or should the upper bits be semantically unspecified?

For example, for rules that use Imm12:

;; Helper to go directly from a `Value`, when it's an `iconst`, to an `Imm12`.
(decl imm12_from_value (Imm12) Value)
(extractor
  (imm12_from_value n)
  (def_inst (iconst (u64_from_imm64 (imm12_from_u64 n)))))

This external extractor is called:

  /// Compute a Imm12 from raw bits, if possible.
    pub fn maybe_from_u64(val: u64) -> Option<Imm12> {
        if val == 0 {
            // …
        } else if val < 0xfff {
            // …
        } else if val < 0xfff_000 && (val & 0xfff == 0) {
            // …
        } else {
            None
        }
    }

This seems to assume that constants are sign-extended, since we're comparing against 64-wide constants and because immediate arithmetic instructions do not sign extend (or, at minimum, this assumes the upper bits are not unspecified).

However, this bug fix for constant propagation in the midend implies that upper bits are unspecified and that bugs can occur from interpreting them: “this was producing iconsts with set high bits beyond their types' width, which is not legal.”

Because the verifier essentially models these iconsts as zero-extended, the verifier _does not_ find a bug on the code before the bug fix for #5405. That is, this code verifies successfully even using imm64 and not imm64_masked . If using imm64 here without masking is a bug, we need to update our the verifier's modeling to find it.

Benefit

We need precise semantics for verification. :)

We can also use this as a chance to audit for other bugs where there might be missing masking behavior.

Implementation

This doesn’t strictly need to change the implementation; but might be wise to add assertions of this behavior.

Alternatives

iconst could have a more complicated backing Rust type where different widths are modeled with the correct type (e.g., u8), this is probably infeasible for performance reasons.

Last updated: Nov 22 2024 at 16:03 UTC