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 CLIFiconst
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 usingimm64
and notimm64_masked
. If usingimm64
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.
avanhatt commented on issue #5700:
Related to: https://github.com/bytecodealliance/wasmtime/issues/3059
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.
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 CLIFiconst
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 usingimm64
and notimm64_masked
. If usingimm64
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.
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
u64
s.- 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
u64
s. :zany_face:- So the question is about how ISLE rules (and other stuff that processes ISLE data structures) should treat these
u64
s. 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 theseu64
s.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.
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
u64
s.- 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
u64
s. :zany_face:- So the question is about how ISLE rules (and other stuff that processes ISLE data structures) should treat these
u64
s. 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 theseu64
s.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.
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
u64
s.- 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
u64
s. :zany_face:- So the question is about how ISLE rules (and other stuff that processes ISLE data structures) should treat these
u64
s. 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 theseu64
s.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.
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
u64
s.- 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
u64
s. :zany_face:- So the question is about how ISLE rules (and other stuff that processes ISLE data structures) should treat these
u64
s. 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 theseu64
s.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.
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.
sampsyo commented on issue #5700:
Got it; thanks for clarifying!
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?
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.
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.)
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
onaarch64
,simm32_from_value
onx64
) gives the sign-extended constant foriconst.i32 -1
:FAIL iconst.clif: panicked in worker #0: 0xffffffffffffffff
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 au64
, 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.
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
onaarch64
,simm32_from_value
onx64
):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
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 theImm64
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.
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: Dec 23 2024 at 12:05 UTC