bytecodealliance / bytecodealliance/wasmtime

Cranelift/ISLE: precise semantics for narrow `iconst`s

Open
#5,700 12 comments 1 reaction 0 assignees View on GitHub
Dominant language
Rust
Stars
18.6k
Forks
1.8k
Avg merge
1d 18h
Merged PRs (30d)
126

Description

#### 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 (e.g., `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`:
```lisp
;; 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:
```rust
/// Compute a Imm12 from raw bits, if possible.
pub fn maybe_from_u64(val: u64) -> Option {
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](https://github.com/bytecodealliance/wasmtime/commit/244dce93f67b717cb6e77dc8d74d92052be165d8) 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](https://github.com/avanhatt/wasmtime/blob/cprop/cranelift/isle/veri/veri_engine/examples/midend/old_cprop.isle) 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.

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.