T0b1/wasmtime
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update aarch64 backend's ISLE code to be rule-ordering-independent.

Browse Source 
In [this
comment](https://github.com/bytecodealliance/wasmtime/pull/3545#discussion_r756284757)
I noted a potential subtle issue with the way that a few rules were
written that is fine now but could cause some unexpected pain when we
get around to verification.

Specifically, a set of rules of the form

```
    (rule (A (B _)) (C))
    (rule (A _) (D))
```

should, under any reasonable "default" rule ordering scheme, fire the
more specific rule `(A (B _))` when applicable, in preference to the
second "fallback" rule.

However, for future verification-specific applications of ISLE, we want
to ensure the property that a rule's meaning/validity is not dependent
on being overridden by more specific rules. In other words, if a rule
specifies a rewrite, that rewrite should always be correct; and choosing
a more specific rule can give a *better* compilation (better generated
code) but should not be necessary for correctness.

This is an admittedly under-documented part of the language, though in the
pending #3560 I added a note about rule ordering being a heuristic that
should hopefully make this slightly clearer. Ultimately I want to have
tests that choose non-default rule orderings and differentially fuzz in
order to be sure that we're following this principle; and of course once
we're actually doing verification, we'll catch issues like this upfront.

Apologies for the subtle footgun here and hopefully the reasoning is
clear enough :-)
This commit is contained in:
Chris Fallin
2021-11-24 10:42:58 -08:00
parent ec43254292
commit bc0de464bc
3 changed files with 22 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files

27
cranelift/codegen/src/isa/aarch64/lower/isle/generated_code.rs generated
View File

@@ -2046,38 +2046,47 @@ pub fn constructor_lower<C: Context>(ctx: &mut C, arg0: Inst) -> Option<ValueReg
// Generated as internal constructor for term iadd_op.
pub fn constructor_iadd_op<C: Context>(ctx: &mut C, arg0: Type) -> Option<ALUOp> {
let pattern0_0 = arg0;
if pattern0_0 == I64 {
// Rule at src/isa/aarch64/lower.isle line 76.
let expr0_0 = ALUOp::Add64;
return Some(expr0_0);
}
if let Some(pattern1_0) = C::fits_in_32(ctx, pattern0_0) {
// Rule at src/isa/aarch64/lower.isle line 75.
let expr0_0 = ALUOp::Add32;
return Some(expr0_0);
}
// Rule at src/isa/aarch64/lower.isle line 76.
let expr0_0 = ALUOp::Add64;
return Some(expr0_0);
return None;
}
// Generated as internal constructor for term isub_op.
pub fn constructor_isub_op<C: Context>(ctx: &mut C, arg0: Type) -> Option<ALUOp> {
let pattern0_0 = arg0;
if pattern0_0 == I64 {
// Rule at src/isa/aarch64/lower.isle line 81.
let expr0_0 = ALUOp::Sub64;
return Some(expr0_0);
}
if let Some(pattern1_0) = C::fits_in_32(ctx, pattern0_0) {
// Rule at src/isa/aarch64/lower.isle line 80.
let expr0_0 = ALUOp::Sub32;
return Some(expr0_0);
}
// Rule at src/isa/aarch64/lower.isle line 81.
let expr0_0 = ALUOp::Sub64;
return Some(expr0_0);
return None;
}
// Generated as internal constructor for term madd_op.
pub fn constructor_madd_op<C: Context>(ctx: &mut C, arg0: Type) -> Option<ALUOp3> {
let pattern0_0 = arg0;
if pattern0_0 == I64 {
// Rule at src/isa/aarch64/lower.isle line 86.
let expr0_0 = ALUOp3::MAdd64;
return Some(expr0_0);
}
if let Some(pattern1_0) = C::fits_in_32(ctx, pattern0_0) {
// Rule at src/isa/aarch64/lower.isle line 85.
let expr0_0 = ALUOp3::MAdd32;
return Some(expr0_0);
}
// Rule at src/isa/aarch64/lower.isle line 86.
let expr0_0 = ALUOp3::MAdd64;
return Some(expr0_0);
return None;
}