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

[avanhatt]

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.

[avanhatt]

Related to: #3059

[bjorn3]

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.

[sampsyo]

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. 🤪
• 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.

[bjorn3]

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]

Got it; thanks for clarifying!

[jameysharp]

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]

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]

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]

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

[avanhatt]

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.

[fitzgen]

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.

[jameysharp]

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.