Stream: git-wasmtime

Topic: wasmtime / PR #7231 PCC: check facts on loaded and stored...

Wasmtime GitHub notifications bot (Oct 12 2023 at 19:24):

cfallin requested abrown for a review on PR #7231.

Wasmtime GitHub notifications bot (Oct 12 2023 at 19:24):

cfallin requested wasmtime-compiler-reviewers for a review on PR #7231.

Wasmtime GitHub notifications bot (Oct 12 2023 at 19:24):

cfallin opened PR #7231 from cfallin:pcc-memtypes-load to bytecodealliance:main:

This PR incorporates a few more steps in PCC's development:

• We now check that the fact, if any, provided for a field in a memory type supports (subsumes) the claimed fact on the result of a load from that field. Likewise, we check that the fact on any value stored to a field supports the field's fact.
• We check that facts are preserved across control-flow edges by validating that branch arguments' facts subsume blockparams' facts.
• For integer-typed values, when no other fact is present and one is needed during validation, we infer a minimal fact based on the type's full range.

With all of these together, we can validate a simple "mock vmctx" example that looks a lot like what static memory accesses in Wasmtime do:

test compile
set enable_pcc=true
target aarch64

;; Equivalent to a Wasm `i64.load` from a static memory.
function %f0(i64, i32) -> i64 {
    ;; mock vmctx struct:
    mt0 = struct 8 { 0: i64 readonly ! mem(mt1, 0) }
    ;; mock static memory: 4GiB range, plus 2GiB guard
    mt1 = memory 0x1_8000_0000

block0(v0 ! mem(mt0, 0): i64, v1: i32):
    ;; Compute the address: base + offset. Guard region (2GiB) is
    ;; sufficient for an 8-byte I64 load.
    v2 ! mem(mt1, 0) = load.i64 checked v0+0    ;; base pointer
    v3 ! max(64, 0xffff_ffff) = uextend.i64 v1  ;; offset
    v4 ! mem(mt1, 0xffff_ffff) = iadd.i64 v2, v3
    v5 = load.i64 checked v4
    return v5
}

In theory, once we propagate facts during aegraph rewriting (we don't currently; opts are off in all tests), this should be enough for end-to-end checking of static memories by emitting the right facts in cranelift-wasm. Those two steps (opts, then Wasm frontend) are next!

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

Wasmtime GitHub notifications bot (Oct 12 2023 at 19:24):

cfallin requested fitzgen for a review on PR #7231.

Wasmtime GitHub notifications bot (Oct 12 2023 at 20:19):

fitzgen submitted PR review:

Nice!

Wasmtime GitHub notifications bot (Oct 12 2023 at 20:19):

fitzgen submitted PR review:

Nice!

Wasmtime GitHub notifications bot (Oct 12 2023 at 20:19):

fitzgen created PR review comment:

Missing trailing newline

Wasmtime GitHub notifications bot (Oct 12 2023 at 20:19):

fitzgen created PR review comment:

ditto

Wasmtime GitHub notifications bot (Oct 12 2023 at 20:32):

cfallin updated PR #7231.

Wasmtime GitHub notifications bot (Oct 12 2023 at 20:34):

cfallin has enabled auto merge for PR #7231.

Wasmtime GitHub notifications bot (Oct 13 2023 at 00:12):

cfallin updated PR #7231.

Wasmtime GitHub notifications bot (Oct 13 2023 at 01:36):

cfallin merged PR #7231.

Wasmtime GitHub notifications bot (Oct 13 2023 at 17:22):

fitzgen submitted PR review.

Wasmtime GitHub notifications bot (Oct 13 2023 at 17:22):

fitzgen submitted PR review.

Wasmtime GitHub notifications bot (Oct 13 2023 at 17:22):

fitzgen created PR review comment:

I don't think this is technically wrong but it feels like a footgun to allow a Mem fact to subsume a minimal ValueMax fact.

Would it be a problem to limit this to ValueMax LHSes? I guess that is what would happen if this case wasn't here, due to the match arm just below this one. Can you explain in more detail why we need this kind of cross-fact-kind subsumption then?

Wasmtime GitHub notifications bot (Oct 13 2023 at 18:48):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 13 2023 at 18:48):

cfallin created PR review comment:

It seems that that narrower rule is indeed sufficient, at least for our test cases. The new rule is still necessary (not covered by the rule below) because of the remaining difference: it doesn't require matching bit-widths.

All of this is a bit of awkward fallout of the way default facts are working now though, so I'm going to see if I can try again to eliminate them and make subsume take the type instead. If not, I'll update as you suggest!

Last updated: Dec 23 2024 at 12:05 UTC