Stream: git-wasmtime

Topic: wasmtime / PR #7389 PCC: verification primitives for dyna...

Wasmtime GitHub notifications bot (Oct 27 2023 at 06:37):

cfallin requested fitzgen for a review on PR #7389.

Wasmtime GitHub notifications bot (Oct 27 2023 at 06:37):

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

Wasmtime GitHub notifications bot (Oct 27 2023 at 06:37):

cfallin opened PR #7389 from cfallin:pcc-dynamic to bytecodealliance:main:

This PR adds new kinds of facts on value dynamic_range, dynamic_mem, and compare; a new kind of memory type dynamic_memory; and a notion of symbolic expressions (a sum of either an SSA value or global value and a static offset) for min and max values in those ranges that are just rich enough to express the expected CLIF sequence for Wasm dynamic memory bounds-checks with Spectre mitigations (cmp/select rather than control-flow-based). It is sufficient to validate the following

; Equivalent to a Wasm `i64.load` from a dynamic memory.
function %f0(i64 vmctx, i32) -> i64 {
    gv0 = vmctx
    gv1 = load.i64 notrap aligned checked gv0+0 ;; base
    gv2 = load.i64 notrap aligned checked gv0+8 ;; size

    ;; mock vmctx struct:
    mt0 = struct 16 {
        0: i64 readonly ! dynamic_mem(mt1, 0, 0),
        8: i64 readonly ! dynamic_range(64, gv2, gv2),
    }
    ;; mock dynamic memory: dynamic range, plus 2GiB guard
    mt1 = dynamic_memory gv2 + 0x8000_0000

block0(v0 ! mem(mt0, 0, 0): i64, v1 ! dynamic_range(32, v1, v1): i32):
    v2 ! dynamic_range(64, v1, v1)            = uextend.i64 v1       ;; extended Wasm offset
    v3 ! dynamic_mem(mt1, 0, 0)               = global_value.i64 gv1 ;; base
    v4 ! dynamic_range(64, gv2, gv2)          = global_value.i64 gv2 ;; size
    v5 ! compare(uge, v1, gv2)                = icmp.i64 uge v2, v4  ;; bounds-check compare of extended Wasm offset to size
    v6 ! dynamic_mem(mt1, v1, v1)              = iadd.i64 v3, v2      ;; compute access address: memory base plus extended Wasm offset
    v7 ! dynamic_mem(mt1, 0, 0, nullable)     = iconst.i64 0         ;; null pointer for speculative path
    v8 ! dynamic_mem(mt1, 0, gv2-1, nullable) = select_spectre_guard v5, v7, v6  ;; if OOB, pick null, otherwise the real address
    v9                                        = load.i64 checked v8
    return v9
}

on both x86-64 and aarch64.

The first half of this was:

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

Wasmtime GitHub notifications bot (Oct 27 2023 at 06:46):

cfallin updated PR #7389.

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen submitted PR review:

r=me with some comments below

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen submitted PR review:

r=me with some comments below

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

It seems potentially wrong that both union and intersection take the or of nullability. I guess I'd expect one to and or have guards on the match arm that they are both null or both not null. Intuitively, the or behavior makes sense to me for union, but not for intersection above. But I'm also not 100% sure that it is incorrect? It just feels funky.

Care to calm my nerves a bit by explaining why this is okay? And probably putting some part of that explanation in comments here?

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

Should this not return an Expr with BaseExpr::Max? I guess I'm not seeing (yet) what the point of that variant is if we aren't going to use it for something like this.

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

Maybe we can rename this to is_symbol or something? Because a constant value range is also a single value, but it is not symbolic. If I was just reading some code that called this method, I might assume that it would return true for things it does not check for.

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

Style nitpick: might be easier to read if the try_from expression was pulled out to its own variable, similar to how the end_offset is.

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

Above we have bw_lhs >= bw_rhs -- do we need that here? Or, even if we don't need it, is it still correct to have it here for the sake of consistency? And if not, then we should probably explain that rather than say "same as above" when it isn't the same as above.

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

Style nitpick: can move the *min == 0 && *max == 0 && *nullable from the guard to the pattern, and it will be a little easier to read, IMO.

            (
                Fact::Range {
                    bit_width,
                    min: 0,
                    max: 0,
                },
                Fact::DynamicMem {
                    nullable: true,
                    ..
                },
            ) if *bit_width == self.pointer_width => true,

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

Can we define an enum to replace the strict: bool parameter? This should both make this code easier to follow and make it more obvious what callers are doing vs just passing a random bool parameter or needing to do stuff like foo(/* strict = */ false).

Something like

enum InequalityKind {
    GreaterThanOrEqual,
    LessThan,
}

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

Let's either clean up these traces and give them more context to make them readable by general wasmtime/cranelift devs or remove them.

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

Oh also, maybe we can call this as_symbol since it returns something. Just got confused for a second when reading callers.

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

    v6 ! dynamic_mem(mt1, v1, v1)             = iadd.i64 v3, v2      ;; compute access address: memory base plus extended Wasm offset

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

Seems like maybe not the most useful trace long term.

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

Ditto regarding traces.

Wasmtime GitHub notifications bot (Oct 27 2023 at 16:39):

fitzgen created PR review comment:

Also, it seems like maybe the comment is incorrect and this is <= or <, not >= or <?

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:14):

cfallin updated PR #7389.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin created PR review comment:

Ah, good point! It arose out of a need for the other side of the lattice when defining min and max, but now that we have it we can saturate to it here too.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin created PR review comment:

Ah, yeah, intersect was wrong -- it should have been an AND. Fixed, thanks!

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin created PR review comment:

Done!

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin created PR review comment:

I was having some trouble convincing myself it works here... in the static case, we know that the concrete limit values are within the range provided by the bitwidth, so if the range gets bigger on the RHS (the subsuming case), and the bitwidth gets smaller, that implies that the claimed range values also fit within the bitwidth on the left, and so no claims are being made about upper bits. Whereas we don't know that about symbolic values. (It's still a little handwavy but that's the gist) I've added a comment to this effect.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin created PR review comment:

Done!

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin created PR review comment:

Done!

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin created PR review comment:

Done on both -- indeed, the comment was incorrect in the second case, thanks!

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin created PR review comment:

Removed; I neglected to go through and clean these up after getting things working, sorry!

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin created PR review comment:

Done

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin created PR review comment:

Done!

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:17):

cfallin created PR review comment:

Done!

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:18):

cfallin has enabled auto merge for PR #7389.

Wasmtime GitHub notifications bot (Oct 27 2023 at 21:21):

cfallin updated PR #7389.

Wasmtime GitHub notifications bot (Oct 27 2023 at 22:49):

cfallin merged PR #7389.

Last updated: Oct 23 2024 at 20:03 UTC