cfallin requested fitzgen for a review on PR #7389.
cfallin requested wasmtime-compiler-reviewers for a review on PR #7389.
cfallin opened PR #7389 from cfallin:pcc-dynamic
to bytecodealliance:main
:
This PR adds new kinds of facts on value
dynamic_range
,dynamic_mem
, andcompare
; a new kind of memory typedynamic_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>
cfallin updated PR #7389.
fitzgen submitted PR review:
r=me with some comments below
fitzgen submitted PR review:
r=me with some comments below
fitzgen created PR review comment:
It seems potentially wrong that both
union
andintersection
take theor
of nullability. I guess I'd expect one toand
or have guards on the match arm that they are both null or both not null. Intuitively, theor
behavior makes sense to me forunion
, 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?
fitzgen created PR review comment:
Should this not return an
Expr
withBaseExpr::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.
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 returntrue
for things it does not check for.
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 theend_offset
is.
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.
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,
fitzgen created PR review comment:
Can we define an
enum
to replace thestrict: 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 likefoo(/* strict = */ false)
.Something like
enum InequalityKind { GreaterThanOrEqual, LessThan, }
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.
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.
fitzgen created PR review comment:
v6 ! dynamic_mem(mt1, v1, v1) = iadd.i64 v3, v2 ;; compute access address: memory base plus extended Wasm offset
fitzgen created PR review comment:
Seems like maybe not the most useful trace long term.
fitzgen created PR review comment:
Ditto regarding traces.
fitzgen created PR review comment:
Also, it seems like maybe the comment is incorrect and this is
<=
or<
, not>=
or<
?
cfallin updated PR #7389.
cfallin submitted PR review.
cfallin created PR review comment:
Ah, good point! It arose out of a need for the other side of the lattice when defining
min
andmax
, but now that we have it we can saturate to it here too.
cfallin submitted PR review.
cfallin created PR review comment:
Ah, yeah, intersect was wrong -- it should have been an AND. Fixed, thanks!
cfallin submitted PR review.
cfallin created PR review comment:
Done!
cfallin submitted PR review.
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.
cfallin submitted PR review.
cfallin created PR review comment:
Done!
cfallin submitted PR review.
cfallin created PR review comment:
Done!
cfallin submitted PR review.
cfallin created PR review comment:
Done on both -- indeed, the comment was incorrect in the second case, thanks!
cfallin submitted PR review.
cfallin created PR review comment:
Removed; I neglected to go through and clean these up after getting things working, sorry!
cfallin submitted PR review.
cfallin created PR review comment:
Done
cfallin submitted PR review.
cfallin created PR review comment:
Done!
cfallin submitted PR review.
cfallin created PR review comment:
Done!
cfallin has enabled auto merge for PR #7389.
cfallin updated PR #7389.
cfallin merged PR #7389.
Last updated: Dec 23 2024 at 12:05 UTC