Skip to content

Verify most of the mid-end #105

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
avanhatt wants to merge 2 commits into
base: main
Choose a base branch
from
Draft

Verify most of the mid-end #105

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cb5eb04
Verify most of the mid-end
avanhatt Jul 15, 2026
b8ad93d
mbm feedback
avanhatt Jul 21, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .github/workflows/main.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1353,6 +1353,7 @@ jobs:
- uses: ./.github/actions/install-rust
- run: cargo run -p cranelift-isle-veri --bin veri -- --config cranelift/isle/veri/configs/aarch64-fast.args --skip-solver
- run: cargo run -p cranelift-isle-veri --bin veri -- --name x64 --rule iadd_base_case_32_or_64_lea --skip-solver
- run: cargo run -p cranelift-isle-veri --bin veri -- --name opt --only-root simplify --default-excludes --skip-solver

# Perform release builds of `wasmtime` and `libwasmtime.so`. Builds a variety
# of platforms and architectures and then uploads the release artifacts to
Expand Down
18 changes: 13 additions & 5 deletions cranelift/codegen/meta/src/isle.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,14 @@ pub fn get_isle_compilations(
inputs.extend(extra.iter().map(|f| spec_dir.join(f)));
inputs
};
let lower_spec_inputs = |extra: &[&str]| -> Vec<std::path::PathBuf> {
let mut inputs = spec_inputs(extra);
if cfg!(feature = "spec") {
let spec_dir = codegen_crate_dir.join("src").join("spec");
inputs.push(spec_dir.join("prelude_lower_spec.isle"));
}
inputs
};

// Directory for mid-end optimizations.
let src_opts = codegen_crate_dir.join("src").join("opts");
Expand Down Expand Up @@ -166,7 +174,7 @@ pub fn get_isle_compilations(
output: gen_dir.join("isle_opt.rs"),
tracked_inputs: [
vec![prelude_isle.clone(), prelude_opt_isle],
spec_inputs(&[]),
spec_inputs(&["fpconst.isle", "opt.isle"]),
vec![
src_opts.join("arithmetic.isle"),
src_opts.join("bitops.isle"),
Expand All @@ -191,7 +199,7 @@ pub fn get_isle_compilations(
output: gen_dir.join("isle_x64.rs"),
tracked_inputs: [
vec![prelude_isle.clone(), prelude_lower_isle.clone()],
spec_inputs(&["state.isle"]),
lower_spec_inputs(&["fpconst.isle", "state.isle"]),
vec![
src_isa_x64.join("inst.isle"),
src_isa_x64.join("lower.isle"),
Expand All @@ -210,7 +218,7 @@ pub fn get_isle_compilations(
output: gen_dir.join("isle_aarch64.rs"),
tracked_inputs: [
vec![prelude_isle.clone(), prelude_lower_isle.clone()],
spec_inputs(&["fpconst.isle", "state.isle"]),
lower_spec_inputs(&["fpconst.isle", "state.isle"]),
vec![
src_isa_aarch64.join("inst.isle"),
src_isa_aarch64.join("inst_neon.isle"),
Expand All @@ -235,7 +243,7 @@ pub fn get_isle_compilations(
output: gen_dir.join("isle_s390x.rs"),
tracked_inputs: [
vec![prelude_isle.clone(), prelude_lower_isle.clone()],
spec_inputs(&[]),
lower_spec_inputs(&[]),
vec![
src_isa_s390x.join("inst.isle"),
src_isa_s390x.join("lower.isle"),
Expand All @@ -250,7 +258,7 @@ pub fn get_isle_compilations(
output: gen_dir.join("isle_riscv64.rs"),
tracked_inputs: [
vec![prelude_isle.clone(), prelude_lower_isle.clone()],
spec_inputs(&[]),
lower_spec_inputs(&[]),
vec![
src_isa_risc_v.join("inst.isle"),
src_isa_risc_v.join("inst_vector.isle"),
Expand Down
6 changes: 3 additions & 3 deletions cranelift/codegen/src/opts/arithmetic.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
;; the right, and thus only simplify patterns like `x+0`, not `0+x`.

;; x+0 == x.
(rule (simplify (iadd ty
(rule iadd_x_plus_zero (simplify (iadd ty
x
(iconst_u ty 0)))
(subsume x))
Expand Down Expand Up @@ -191,7 +191,7 @@

;; If both of the multiplied arguments to an `fmul` are negated then remove
;; both of them since they cancel out.
(rule (simplify (fmul ty (fneg ty x) (fneg ty y)))
(rule fmul_fneg_fneg (simplify (fmul ty (fneg ty x) (fneg ty y)))
(fmul ty x y))

;; Detect people open-coding `mulhi`: (x as big * y as big) >> bits
Expand Down Expand Up @@ -567,4 +567,4 @@
(rule (simplify (ult ty (umax ty y x) x)) (iconst_u ty 0))

;; (-X) * C = X * (-C)
(rule (simplify (imul (fits_in_64 ty) (ineg ty x) (iconst ty y))) (imul ty x (iconst ty (imm64_neg ty y))))
(rule imul_ineg_const (simplify (imul (fits_in_64 ty) (ineg ty x) (iconst ty y))) (imul ty x (iconst ty (imm64_neg ty y))))
4 changes: 4 additions & 0 deletions cranelift/codegen/src/prelude_opt.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -627,3 +627,7 @@
(isub $I64 numerator tt)))
(rule (apply_div_const_magic_s64_finish (Opcode.Sdiv) _numerator _divisor qf)
qf)

(model Inst (type (bv)))
(model ValueArray2 (type (bv)))
(model ValueArray3 (type (bv)))
75 changes: 53 additions & 22 deletions cranelift/codegen/src/spec/inst_specs.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

(model Imm64 (type (bv 64)))

(model Ieee16 (type (bv 16)))
(model Ieee32 (type (bv 32)))
(model Ieee64 (type (bv 64)))

Expand Down Expand Up @@ -61,6 +62,18 @@
(type Bool)
(default (not clif_trap)))

; Whether the value being rewritten is a nondeterministic arithmetic NaN,
; which loosens the mid-end `simplify` soundness contract from exact bitwise
; equality to `fp_equiv!` (see `opt.isle`). Relevant floating-point arithmetic
; instructions (`fadd`/`fmul`/...) set to true exactly when they produce a NaN;
; deterministic float bit-ops (`fneg`/`fabs`/`fcopysign`) leave it at the
; default `false`. Modeled as execution state (like `clif_trap`) so the relaxation
; is expressed declaratively in specs rather than special-cased in the verifier
; (because `simplify` does not consume the value type).
(state relax_nan
(type Bool)
(default (not relax_nan)))

;;;; Common Term Forms ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(form
Expand Down Expand Up @@ -367,16 +380,14 @@
((args (named Type) (bv 64)) (ret (bv 32))))

(form extend
((args (named Type) (bv 8)) (ret (bv 8)))
((args (named Type) (bv 8)) (ret (bv 16)))
((args (named Type) (bv 8)) (ret (bv 32)))
((args (named Type) (bv 8)) (ret (bv 64)))
((args (named Type) (bv 16)) (ret (bv 16)))
((args (named Type) (bv 16)) (ret (bv 32)))
((args (named Type) (bv 16)) (ret (bv 64)))
((args (named Type) (bv 32)) (ret (bv 32)))
((args (named Type) (bv 32)) (ret (bv 64))))
;; Note: (bv 64) -> (bv 64) not accepted in clif
;; Note: extends must strictly widen, so same-width instantiations
;; (8->8, 16->16, 32->32, 64->64) are not accepted in clif.

(spec (uextend ty x)
(provide (= result (zero_ext (widthof result) x))
Expand All @@ -388,16 +399,6 @@
(= (:bits ty) (widthof result))))
(instantiate sextend extend)

;; `maybe_uextend` "sees through" a `uextend`: given the outer value `result`,
;; it yields the inner value `value`. When `result` is defined by a `uextend`,
;; `value` is that uextend's argument; otherwise `value` is `result` itself. In
;; both cases the inner value is the low bits of the outer value, i.e. the outer
;; value is the zero-extension of the inner one to the outer width (in the
;; fall-through case the two widths are equal, so this is the identity). The
;; extractor is total (it always matches), so no `match` clause is needed.
(spec (maybe_uextend value)
(provide (= result (zero_ext (widthof result) value))))

(spec (smin ty x y)
(provide (= result (if (bvsle x y) x y))
(= (:bits ty) (widthof result))))
Expand Down Expand Up @@ -710,7 +711,10 @@
;
; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
(spec (fadd ty x y)
(modifies relax_nan produces_nan)
(provide
(= produces_nan (fp.isNaN result))
(=> produces_nan relax_nan)
(= (:bits ty) (widthof result))
(= result
; If either z1 or z2 is a NaN, then return an element of nans{z1,z2}.
Expand Down Expand Up @@ -751,7 +755,10 @@
;
; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
(spec (fsub ty x y)
(modifies relax_nan produces_nan)
(provide
(= produces_nan (fp.isNaN result))
(=> produces_nan relax_nan)
(= (:bits ty) (widthof result))
(= result
; If either z1 or z2 is a NaN, then return an element of nans{z1,z2}.
Expand Down Expand Up @@ -794,7 +801,10 @@
;
; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
(spec (fmul ty x y)
(modifies relax_nan produces_nan)
(provide
(= produces_nan (fp.isNaN result))
(=> produces_nan relax_nan)
(= (:bits ty) (widthof result))
(= result
; If either z1 or z2 is a NaN, then return an element of nans{z1,z2}.
Expand Down Expand Up @@ -837,7 +847,10 @@
;
; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
(spec (fdiv ty x y)
(modifies relax_nan produces_nan)
(provide
(= produces_nan (fp.isNaN result))
(=> produces_nan relax_nan)
(= (:bits ty) (widthof result))
(= result
; If either z1 or z2 is a NaN, then return an element of nans{z1,z2}.
Expand Down Expand Up @@ -884,7 +897,10 @@
;
; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
(spec (fmin ty x y)
(modifies relax_nan produces_nan)
(provide
(= produces_nan (fp.isNaN result))
(=> produces_nan relax_nan)
(= (:bits ty) (widthof result))
(= result
; If either z1 or z2 is a NaN, then return an element of nans{z1,z2}.
Expand All @@ -911,7 +927,10 @@
;
; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
(spec (fmax ty x y)
(modifies relax_nan produces_nan)
(provide
(= produces_nan (fp.isNaN result))
(=> produces_nan relax_nan)
(= (:bits ty) (widthof result))
(= result
; If either z1 or z2 is a NaN, then return an element of nans{z1,z2}.
Expand Down Expand Up @@ -967,14 +986,11 @@
(spec (fneg ty x)
(provide
(= (:bits ty) (widthof result))
(= result
; If z is a NaN, then return z with negated sign.
(if (fp.isNaN x)
(nan_neg! x)
; Else if z is an infinity, then return that infinity negated.
; Else if z is a zero, then return that zero negated.
; Else return z negated.
(fp.neg x))))) ; Remaining cases of the spec handled by SMT fp.neg
; IEEE-754 negation just toggles the sign bit for every input (normal,
; +/-0, +/-inf, NaN), so model it directly in the bit-vector theory: this
; is bit-exact and avoids an fp<->bv bridge that makes queries like
; `fmul_fneg_fneg` intractable.
(= result (bvxor x (fp_sign_bit_set! (widthof x))))))
(instantiate fneg
((args (named Type) (bv 32)) (ret (bv 32)))
((args (named Type) (bv 64)) (ret (bv 64))))
Expand All @@ -984,7 +1000,10 @@
;
; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
(spec (sqrt ty x)
(modifies relax_nan produces_nan)
(provide
(= produces_nan (fp.isNaN result))
(=> produces_nan relax_nan)
(= (:bits ty) (widthof result))
(= result
; If z is a NaN, then return an element of nans{z}.
Expand Down Expand Up @@ -1012,7 +1031,10 @@
;
; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
(spec (ceil ty x)
(modifies relax_nan produces_nan)
(provide
(= produces_nan (fp.isNaN result))
(=> produces_nan relax_nan)
(= (:bits ty) (widthof result))
(= result
; If z is a NaN, then return an element of nans{z}.
Expand All @@ -1037,7 +1059,10 @@
;
; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
(spec (floor ty x)
(modifies relax_nan produces_nan)
(provide
(= produces_nan (fp.isNaN result))
(=> produces_nan relax_nan)
(= (:bits ty) (widthof result))
(= result
; If z is a NaN, then return an element of nans{z}.
Expand All @@ -1062,7 +1087,10 @@
;
; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
(spec (trunc ty x)
(modifies relax_nan produces_nan)
(provide
(= produces_nan (fp.isNaN result))
(=> produces_nan relax_nan)
(= (:bits ty) (widthof result))
(= result
; If z is a NaN, then return an element of nans{z}.
Expand All @@ -1089,7 +1117,10 @@
;
; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
(spec (nearest ty x)
(modifies relax_nan produces_nan)
(provide
(= produces_nan (fp.isNaN result))
(=> produces_nan relax_nan)
(= (:bits ty) (widthof result))
(= result
; If z is a NaN, then return an element of nans{z}.
Expand Down
Loading