wasmtime / issue #5700 Cranelift/ISLE: precise semantics ... · git-wasmtime

Stream: git-wasmtime

Topic: wasmtime / issue #5700 Cranelift/ISLE: precise semantics ...

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

avanhatt edited 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.

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

avanhatt commented on issue #5700:

Related to: https://github.com/bytecodealliance/wasmtime/issues/3059

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

bjorn3 commented on issue #5700:

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.”

Indeed. This is the case both at clif ir level and machine code level.

Wasmtime GitHub notifications bot (Feb 03 2023 at 19:19):

avanhatt edited 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 (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:
;; 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.

Wasmtime GitHub notifications bot (Feb 06 2023 at 19:37):

sampsyo commented on issue #5700:

Just to distill some super-high-level facts:

In CLIF data structures, all constants of any size and sightedness are recorded as u64s.

To state the obvious, all these actual physical bits are all either 1 or 0! There is no such things as a "don't care" bit in Rust u64s. :zany_face:

So the question is about how ISLE rules (and other stuff that processes ISLE data structures) should treat these u64s. It seems like there are 3 options:
1. You can rely on the upper (out-of-range) bits being 0.
2. You can rely on those upper bits being the sign bit (i.e., sign-extended from the highest "real" bit).
3. You cannot rely on those bits being anything in particular, and you must expect there to be random junk up there. Which means you should probably mask off the upper bits before you do anything nontrivial with these u64s.

It seems like most of the evidence we have (including stuff linked in this thread) points toward option 2. But we are taking something like option 3 in the verifier, which is "conservative" in the sense that it at least doesn't mistakenly reject correct rules that adhere to 1 or 2. But it also limits it from finding bugs in rules that make incorrect assumptions about out-of-range bits.

So therefore, if we think the truth is actually option 1 or 2 above, we should probably "tighten down" the verifier to match those so we can find more bugs.

Wasmtime GitHub notifications bot (Feb 06 2023 at 19:38):

sampsyo edited a comment on issue #5700:

Just to distill some super-high-level facts:

In CLIF data structures, all constants of any size and sightedness are recorded as u64s.

To state the obvious, all these actual physical bits are all either 1 or 0! There is no such things as a "don't care" bit in Rust u64s. :zany_face:

So the question is about how ISLE rules (and other stuff that processes ISLE data structures) should treat these u64s. It seems like there are 3 options:
1. You can rely on the upper (out-of-range) bits being 0.
2. You can rely on those upper bits being the sign bit (i.e., sign-extended from the highest "real" bit).
3. You cannot rely on those bits being anything in particular, and you must expect there to be random junk up there. Which means you should probably mask off the upper bits before you do anything nontrivial with these u64s.

It seems like most of the evidence we have (including stuff linked in this thread) points toward option "ii". But we are taking something like option "iii" in the verifier, which is "conservative" in the sense that it at least doesn't mistakenly reject correct rules that adhere to "i" or "ii". But it also limits it from finding bugs in rules that make incorrect assumptions about out-of-range bits.

So therefore, if we think the truth is actually option "i" or "ii" above, we should probably "tighten down" the verifier to match those so we can find more bugs.

Wasmtime GitHub notifications bot (Feb 06 2023 at 19:39):

sampsyo edited a comment on issue #5700:

Just to distill some super-high-level facts:

In CLIF data structures, all constants of any size and sightedness are recorded as u64s.

To state the obvious, all these actual physical bits are all either 1 or 0! There is no such things as a "don't care" bit in Rust u64s. :zany_face:

So the question is about how ISLE rules (and other stuff that processes ISLE data structures) should treat these u64s. It seems like there are 3 options:
1. You can rely on the upper (out-of-range) bits being 0.
2. You can rely on those upper bits being copies of the sign bit (i.e., sign-extended from the highest "real" bit).
3. You cannot rely on those bits being anything in particular, and you must expect there to be random junk up there. Which means you should probably mask off the upper bits before you do anything nontrivial with these u64s.

It seems like most of the evidence we have (including stuff linked in this thread) points toward option "ii". But we are taking something like option "iii" in the verifier, which is "conservative" in the sense that it at least doesn't mistakenly reject correct rules that adhere to "i" or "ii". But it also limits it from finding bugs in rules that make incorrect assumptions about out-of-range bits.

So therefore, if we think the truth is actually option "i" or "ii" above, we should probably "tighten down" the verifier to match those so we can find more bugs.

Wasmtime GitHub notifications bot (Feb 06 2023 at 19:39):

sampsyo edited a comment on issue #5700:

Just to distill some super-high-level facts:

In CLIF data structures, all constants of any size and sightedness are recorded as u64s.

To state the obvious, all these actual physical bits are all either 1 or 0! There is no such thing as a "don't care" bit in Rust u64s. :zany_face:

So the question is about how ISLE rules (and other stuff that processes ISLE data structures) should treat these u64s. It seems like there are 3 options:
1. You can rely on the upper (out-of-range) bits being 0.
2. You can rely on those upper bits being copies of the sign bit (i.e., sign-extended from the highest "real" bit).
3. You cannot rely on those bits being anything in particular, and you must expect there to be random junk up there. Which means you should probably mask off the upper bits before you do anything nontrivial with these u64s.

It seems like most of the evidence we have (including stuff linked in this thread) points toward option "ii". But we are taking something like option "iii" in the verifier, which is "conservative" in the sense that it at least doesn't mistakenly reject correct rules that adhere to "i" or "ii". But it also limits it from finding bugs in rules that make incorrect assumptions about out-of-range bits.

So therefore, if we think the truth is actually option "i" or "ii" above, we should probably "tighten down" the verifier to match those so we can find more bugs.

Wasmtime GitHub notifications bot (Feb 06 2023 at 19:58):

bjorn3 commented on issue #5700:

In CLIF data structures, all constants of any size and sightedness are recorded as u64s.

Actually we use i64 (Imm64) and sometimes sign extend and sometimes zero extend, we currently require masking of the high bits in the backend. I would personallt like it to be changed to u64 + requiring zero extension using a clif verifier rule.

Wasmtime GitHub notifications bot (Feb 06 2023 at 19:59):

sampsyo commented on issue #5700:

Got it; thanks for clarifying!

Wasmtime GitHub notifications bot (Feb 06 2023 at 20:26):

jameysharp commented on issue #5700:

Right now my opinion is that we want to follow option 1: unused bits should be 0. I think that's what we've been moving toward producing in the mid-end optimization rules.

But we don't verify that whoever produced the CLIF we're compiling followed that rule, and in that sense we're currently following option 3.

But we are taking something like option "iii" in the verifier, which is "conservative" in the sense that it at least doesn't mistakenly reject correct rules that adhere to "i" or "ii". But it also limits it from finding bugs in rules that make incorrect assumptions about out-of-range bits.

I don't understand this. If a backend "cannot rely on those bits being anything in particular", then any rule which does rely on those bits (being all-zero in case 1, or all-sign in case 2, or making some other unspecified assumption) should be rejected by the verifier, right?

Wasmtime GitHub notifications bot (Feb 06 2023 at 21:15):

cfallin commented on issue #5700:

I'd also say that option 1 seems most reasonable to me. Elsewhere when we have a variable-width payload we generally try to zero-extend.

Re: current verifier assumptions: I imagine what's going on here is that the verifier is providing the assumption that the upper bits are initialized (sign-extended? zero-extended?) so rules that assume this invariant will work, but is not checking the same assumption at the output side? I guess a consistent approach at either extreme would be better -- either provide and check the bit status, or leave as don't-care on the input (as @jameysharp suggests) and don't verify on output. Former would be consistent with taking option 1 or 2 I guess.

Wasmtime GitHub notifications bot (Feb 06 2023 at 21:49):

sampsyo commented on issue #5700:

Right; I kinda realized while typing that summary of the verifier's current assumptions that it was a little nonsensical. Its current policy does not _model_ rule semantics under the regime of policy 3; instead, it does the masking/truncation like policy 3 on behalf of the rules. So, in the verifier's world, rules effectively "see" narrow values and never even interact with the out-of-range bits. Therefore, according to the verifier, they can never have bugs that arise from treating the out-of-range bits incorrectly. (As ever, @avanhatt may correct me about this.)

Wasmtime GitHub notifications bot (Feb 07 2023 at 04:47):

avanhatt commented on issue #5700:

Part of my initial confusion stemmed from that in working from .clif files, the frontend seems to sign extend.

For example running this test:
test run
target aarch64
target x86_64

function %a(i32) -> i32 {
block0(v0: i32):
    v2 = iconst.i32 -1
    v3 = iadd v0, v2
    return v3
}
; run: %a(50) == 49
And dumping (via a panic for simplicity) the resulting u64 of external extractors triggered by immediate checks (Imm12::maybe_from_u64 on aarch64, simm32_from_value on x64) gives the sign-extended constant for iconst.i32 -1:
FAIL iconst.clif: panicked in worker #0: 0xffffffffffffffff

Wasmtime GitHub notifications bot (Feb 07 2023 at 04:50):

avanhatt commented on issue #5700:

And yes, essentially what Adrian said: an iconst is modeled as only the narrow value where possible. When it needs to be used as a u64, our current annotations and inference do masking/truncation as necessary, so we don't find bugs in rules that set the upper bits but shouldn't.

Wasmtime GitHub notifications bot (Feb 07 2023 at 04:51):

avanhatt edited a comment on issue #5700:

Part of my initial confusion stemmed from that in working from .clif files, the frontend seems to sign extend.

For example running this test:
test run
target aarch64
target x86_64

function %a(i32) -> i32 {
block0(v0: i32):
    v2 = iconst.i32 -1
    v3 = iadd v0, v2
    return v3
}
; run: %a(50) == 49
And dumping (via a panic for simplicity) the resulting u64 of external extractors triggered by immediate checks (Imm12::maybe_from_u64 on aarch64, simm32_from_value on x64):
fn simm32_from_value(&mut self, val: Value) -> Option<GprMemImm> {
        let inst = self.lower_ctx.dfg().value_def(val).inst()?;
        let constant: u64 = self.lower_ctx.get_constant(inst)?;
        panic!("{:#x}", constant);
        // ...
    }
Gives the sign-extended constant for iconst.i32 -1:
FAIL iconst.clif: panicked in worker #0: 0xffffffffffffffff

Wasmtime GitHub notifications bot (Feb 07 2023 at 18:30):

fitzgen commented on issue #5700:

Ideally we would encapsulate Imm64's internal value such that you couldn't get/set it without supplying the type of the Imm64 and it would handle this however we choose in that one place, and this wouldn't be something we have to uphold all throughout Cranelift.

Wasmtime GitHub notifications bot (Feb 08 2023 at 01:54):

jameysharp commented on issue #5700:

Part of my initial confusion stemmed from that in working from .clif files, the frontend seems to sign extend.

At the least, we should make cranelift-reader mask constants after parsing them, and maybe also verify that a constant's value doesn't change after narrowing it.

Nick's suggestion of encapsulating Imm64 internally is a better and more comprehensive plan, but I think we'd still get a long way just by fixing the parser.

Last updated: Nov 22 2024 at 16:03 UTC