1;; This is a prelude of standard definitions for ISLE, the instruction-selector 2;; DSL, as we use it bound to our interfaces. 3;; 4;; Note that all `extern` functions here are typically defined in the 5;; `isle_prelude_methods` macro defined in `src/isa/isle.rs` 6 7;;;; Primitive and External Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 8 9;; `()` 10(type Unit (primitive Unit)) 11(model Unit (type Unit)) 12 13(decl pure unit () Unit) 14(extern constructor unit unit) 15 16(model bool (type Bool)) 17 18(model u8 (type (bv 8))) 19(model u16 (type (bv 16))) 20(model u32 (type (bv 32))) 21(model u64 (type (bv 64))) 22(model usize (type (bv))) 23 24(model i8 (type (bv 8))) 25(model i16 (type (bv 16))) 26(model i32 (type (bv 32))) 27(model i64 (type (bv 64))) 28 29;; `cranelift-entity`-based identifiers. 30(model Type (type Int)) 31(type Type (primitive Type)) 32(model Value (type (bv))) 33(type Value (primitive Value)) 34(type ValueList (primitive ValueList)) 35(type BlockCall (primitive BlockCall)) 36(type Inst (primitive Inst)) 37 38;; Match the instruction that defines the given value, if any. 39(spec (def_inst arg) (provide (= result arg))) 40(decl def_inst (Inst) Value) 41(extern extractor def_inst def_inst) 42 43;; ISLE representation of `&[Value]`. 44(type ValueSlice (primitive ValueSlice)) 45 46;; Extract the type of a `Value`. 47(spec (value_type arg) (provide (= arg (widthof result)))) 48(decl value_type (Type) Value) 49(extern extractor infallible value_type value_type) 50 51;; Extractor that matches a `u32` only if non-negative. 52(decl u32_nonnegative (u32) u32) 53(extern extractor u32_nonnegative u32_nonnegative) 54 55;; Extractor that pulls apart an Offset32 into a i32 with the raw 56;; signed-32-bit twos-complement bits. 57(decl offset32 (i32) Offset32) 58(extern extractor infallible offset32 offset32) 59 60;; Pure/fallible constructor that tests if one u32 is less than or 61;; equal to another. 62(spec (u32_lteq a b) 63 (provide (= result ())) 64 (require (<= a b) 65 (= (widthof a) 32) 66 (= (widthof b) 32))) 67(decl pure partial u32_lteq (u32 u32) Unit) 68(extern constructor u32_lteq u32_lteq) 69 70;; Pure/fallible constructor that tests if one u8 is less than or 71;; equal to another. 72(decl pure partial u8_lteq (u8 u8) Unit) 73(extern constructor u8_lteq u8_lteq) 74 75;; Pure/fallible constructor that tests if one u8 is strictly less 76;; than another. 77(decl pure partial u8_lt (u8 u8) Unit) 78(extern constructor u8_lt u8_lt) 79 80;;;; Primitive Type Conversions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 81 82(decl pure u8_as_i8 (u8) i8) 83(extern constructor u8_as_i8 u8_as_i8) 84 85(spec (u8_as_u32 arg) 86 (provide (= result (zero_ext 32 arg))) 87 (require 88 (= (widthof arg) 8) 89 (= (widthof result) 32))) 90(decl pure u8_as_u32 (u8) u32) 91(extern constructor u8_as_u32 u8_as_u32) 92(convert u8 u32 u8_as_u32) 93 94(decl pure u8_as_u64 (u8) u64) 95(extern constructor u8_as_u64 u8_as_u64) 96(convert u8 u64 u8_as_u64) 97 98(decl pure u16_as_i16 (u16) i16) 99(extern constructor u16_as_i16 u16_as_i16) 100 101(decl pure u16_as_u32 (u16) u32) 102(extern constructor u16_as_u32 u16_as_u32) 103(convert u16 u32 u16_as_u32) 104 105(decl pure u16_as_u64 (u16) u64) 106(extern constructor u16_as_u64 u16_as_u64) 107(convert u16 u64 u16_as_u64) 108 109(decl pure u64_as_u8 (u64) u8) 110(extern constructor u64_as_u8 u64_as_u8) 111 112(decl pure u64_as_u16 (u64) u16) 113(extern constructor u64_as_u16 u64_as_u16) 114 115(decl pure u64_as_u16_extractor (u16) u64) 116(extern extractor u64_as_u16_extractor u64_as_u16_extractor) 117 118(decl pure u64_as_i64 (u64) i64) 119(extern constructor u64_as_i64 u64_as_i64) 120 121(decl pure partial u8_try_from_u64 (u64) u8) 122(extern constructor u8_try_from_u64 u8_try_from_u64) 123 124(decl pure partial u8_try_from_u16 (u16) u8) 125(extern constructor u8_try_from_u16 u8_try_from_u16) 126 127(decl pure partial u8_try_from_i32 (i32) u8) 128(extern constructor u8_try_from_i32 u8_try_from_i32) 129 130(decl u16_try_from_i32 (u16) i32) 131(extern extractor u16_try_from_i32 u16_try_from_i32) 132 133(decl pure partial u16_try_from_u64 (u64) u16) 134(extern constructor u16_try_from_u64 u16_try_from_u64) 135 136(decl pure partial u32_try_from_u64 (u64) u32) 137(extern constructor u32_try_from_u64 u32_try_from_u64) 138 139(decl pure partial i32_try_from_i64 (i64) i32) 140(extern constructor i32_try_from_i64 i32_try_from_i64) 141 142(decl pure partial u64_try_from_i64 (i64) u64) 143(extern constructor u64_try_from_i64 u64_try_from_i64) 144 145(decl i8_try_from_i32 (i8) i32) 146(extern extractor i8_try_from_i32 i8_try_from_i32) 147 148(decl pure partial i8_try_from_i64 (i64) i8) 149(extern constructor i8_try_from_i64 i8_try_from_i64) 150 151(decl pure partial i8_try_from_u64 (u64) i8) 152(extern constructor i8_try_from_u64 i8_try_from_u64) 153 154(decl pure i16_as_u16 (i16) u16) 155(extern constructor i16_as_u16 i16_as_u16) 156 157(decl pure partial i16_try_from_u64 (u64) i16) 158(extern constructor i16_try_from_u64 i16_try_from_u64) 159 160(decl pure partial i16_try_from_i32 (i16) i32) 161(extern extractor i16_try_from_i32 i16_try_from_i32) 162 163(decl pure partial i32_try_from_u64 (u64) i32) 164(extern constructor i32_try_from_u64 i32_try_from_u64) 165 166(decl pure u32_as_u64 (u32) u64) 167(extern constructor u32_as_u64 u32_as_u64) 168(convert u32 u64 u32_as_u64) 169 170(decl pure i8_as_u8 (i8) u8) 171(extern constructor i8_as_u8 i8_as_u8) 172 173(decl pure i32_as_u32 (i32) u32) 174(extern constructor i32_as_u32 i32_as_u32) 175 176(decl pure i32_as_i64 (i32) i64) 177(extern constructor i32_as_i64 i32_as_i64) 178(convert i32 i64 i32_as_i64) 179 180(spec (i64_as_u64 arg) (provide (= arg result))) 181(decl pure i64_as_u64 (i64) u64) 182(extern constructor i64_as_u64 i64_as_u64) 183 184(spec (i64_neg x) (provide (= result (bvneg x)))) 185(decl pure i64_neg (i64) i64) 186(extern constructor i64_neg i64_neg) 187 188(decl pure i8_neg (i8) i8) 189(extern constructor i8_neg i8_neg) 190 191(decl u128_as_u64 (u64) u128) 192(extern extractor u128_as_u64 u128_as_u64) 193 194(decl u64_as_u32 (u32) u64) 195(extern extractor u64_as_u32 u64_as_u32) 196 197(decl u32_as_u16 (u16) u32) 198(extern extractor u32_as_u16 u32_as_u16) 199 200(decl i32_as_i8 (i8) i32) 201(extern extractor i32_as_i8 i32_as_i8) 202 203(decl pure u64_as_i32 (u64) i32) 204(extern constructor u64_as_i32 u64_as_i32) 205 206;;;; Primitive Arithmetic ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 207 208(decl pure u8_and (u8 u8) u8) 209(extern constructor u8_and u8_and) 210 211(decl pure u8_shl (u8 u8) u8) 212(extern constructor u8_shl u8_shl) 213 214(decl pure u8_shr (u8 u8) u8) 215(extern constructor u8_shr u8_shr) 216 217(decl pure u8_sub (u8 u8) u8) 218(extern constructor u8_sub u8_sub) 219 220(decl pure u32_add (u32 u32) u32) 221(extern constructor u32_add u32_add) 222 223(spec (u32_sub a b) (provide (= result (bvsub a b)))) 224(decl pure u32_sub (u32 u32) u32) 225(extern constructor u32_sub u32_sub) 226 227(decl pure u32_and (u32 u32) u32) 228(extern constructor u32_and u32_and) 229 230(decl pure u32_shl (u32 u32) u32) 231(extern constructor u32_shl u32_shl) 232 233;; Pure/fallible constructor that tries to add two `u32`s, interpreted 234;; as signed values, and fails to match on overflow. 235(spec (s32_add_fallible x y) 236 (provide (= result (bvadd x y))) 237 (require (not (bvsaddo x y)))) 238(decl pure partial s32_add_fallible (i32 i32) i32) 239(extern constructor s32_add_fallible s32_add_fallible) 240 241(decl pure partial checked_add_with_type (Type u64 u64) u64) 242(extern constructor checked_add_with_type checked_add_with_type) 243 244(decl pure add_overflows_with_type (Type u64 u64) bool) 245(extern constructor add_overflows_with_type add_overflows_with_type) 246 247(decl pure u64_add (u64 u64) u64) 248(extern constructor u64_add u64_add) 249 250(spec (u64_sub a b) 251 (provide (= result (bvsub a b)))) 252(decl pure u64_sub (u64 u64) u64) 253(extern constructor u64_sub u64_sub) 254 255(decl pure u64_mul (u64 u64) u64) 256(extern constructor u64_mul u64_mul) 257 258(decl pure partial u64_udiv (u64 u64) u64) 259(extern constructor u64_udiv u64_udiv) 260 261(decl pure u64_and (u64 u64) u64) 262(extern constructor u64_and u64_and) 263 264(decl pure u64_or (u64 u64) u64) 265(extern constructor u64_or u64_or) 266 267(decl pure u64_xor (u64 u64) u64) 268(extern constructor u64_xor u64_xor) 269 270(decl pure u64_shl (u64 u64) u64) 271(extern constructor u64_shl u64_shl) 272 273(decl pure partial imm64_sdiv (Type Imm64 Imm64) Imm64) 274(extern constructor imm64_sdiv imm64_sdiv) 275 276(decl pure imm64_shl (Type Imm64 Imm64) Imm64) 277(extern constructor imm64_shl imm64_shl) 278 279(decl pure imm64_ushr (Type Imm64 Imm64) Imm64) 280(extern constructor imm64_ushr imm64_ushr) 281 282(decl pure imm64_sshr (Type Imm64 Imm64) Imm64) 283(extern constructor imm64_sshr imm64_sshr) 284 285(decl pure u64_not (u64) u64) 286(extern constructor u64_not u64_not) 287 288(decl pure i64_not (i64) i64) 289(extern constructor i64_not i64_not) 290 291(decl pure u64_eq (u64 u64) bool) 292(extern constructor u64_eq u64_eq) 293 294(decl pure u64_le (u64 u64) bool) 295(extern constructor u64_le u64_le) 296 297(decl pure u64_lt (u64 u64) bool) 298(extern constructor u64_lt u64_lt) 299 300(decl pure i64_shr (i64 i64) i64) 301(extern constructor i64_shr i64_shr) 302 303(decl pure i64_ctz (i64) i64) 304(extern constructor i64_ctz i64_ctz) 305 306;; Sign extends a u64 from ty bits up to 64bits 307(decl pure i64_sextend_u64 (Type u64) i64) 308(extern constructor i64_sextend_u64 i64_sextend_u64) 309 310(spec (i64_sextend_imm64 ty a) (provide (= result (sign_ext 64 (conv_to ty a))))) 311(decl pure i64_sextend_imm64 (Type Imm64) i64) 312(extern constructor i64_sextend_imm64 i64_sextend_imm64) 313 314(decl pure u64_uextend_imm64 (Type Imm64) u64) 315(extern constructor u64_uextend_imm64 u64_uextend_imm64) 316 317(decl pure imm64_icmp (Type IntCC Imm64 Imm64) Imm64) 318(extern constructor imm64_icmp imm64_icmp) 319 320(decl u64_is_zero (bool) u64) 321(extern extractor infallible u64_is_zero u64_is_zero) 322 323(decl i64_is_zero (bool) i64) 324(extern extractor infallible i64_is_zero i64_is_zero) 325 326(decl u64_zero () u64) 327(extractor (u64_zero) (u64_is_zero true)) 328 329(decl u64_nonzero (u64) u64) 330(extractor (u64_nonzero x) (and (u64_is_zero false) x)) 331 332(decl i64_nonzero (i64) i64) 333(extractor (i64_nonzero x) (and (i64_is_zero false) x)) 334 335;; x & 1 == 1 336(spec (u64_is_odd arg) (provide (= result (= #b1 (extract 0 0 arg))))) 337(decl pure u64_is_odd (u64) bool) 338(extern constructor u64_is_odd u64_is_odd) 339 340;; Each of these extractors tests whether the upper half of the input equals the 341;; lower half of the input 342(decl u128_replicated_u64 (u64) u128) 343(extern extractor u128_replicated_u64 u128_replicated_u64) 344(decl u64_replicated_u32 (u64) u64) 345(extern extractor u64_replicated_u32 u64_replicated_u32) 346(decl u32_replicated_u16 (u64) u64) 347(extern extractor u32_replicated_u16 u32_replicated_u16) 348(decl u16_replicated_u8 (u8) u64) 349(extern extractor u16_replicated_u8 u16_replicated_u8) 350 351;; Get the low and high bits of a `u128` as `u64`s. 352(decl u128_low_bits (u128) u64) 353(extern constructor u128_low_bits u128_low_bits) 354(decl u128_high_bits (u128) u64) 355(extern constructor u128_high_bits u128_high_bits) 356 357;; Floating point operations 358 359(decl pure partial f16_min (Ieee16 Ieee16) Ieee16) 360(extern constructor f16_min f16_min) 361(decl pure partial f16_max (Ieee16 Ieee16) Ieee16) 362(extern constructor f16_max f16_max) 363(decl pure f16_neg (Ieee16) Ieee16) 364(extern constructor f16_neg f16_neg) 365(decl pure f16_abs (Ieee16) Ieee16) 366(extern constructor f16_abs f16_abs) 367(decl pure f16_copysign (Ieee16 Ieee16) Ieee16) 368(extern constructor f16_copysign f16_copysign) 369(decl pure partial f32_add (Ieee32 Ieee32) Ieee32) 370(extern constructor f32_add f32_add) 371(decl pure partial f32_sub (Ieee32 Ieee32) Ieee32) 372(extern constructor f32_sub f32_sub) 373(decl pure partial f32_mul (Ieee32 Ieee32) Ieee32) 374(extern constructor f32_mul f32_mul) 375(decl pure partial f32_div (Ieee32 Ieee32) Ieee32) 376(extern constructor f32_div f32_div) 377(decl pure partial f32_sqrt (Ieee32) Ieee32) 378(extern constructor f32_sqrt f32_sqrt) 379(decl pure partial f32_ceil (Ieee32) Ieee32) 380(extern constructor f32_ceil f32_ceil) 381(decl pure partial f32_floor (Ieee32) Ieee32) 382(extern constructor f32_floor f32_floor) 383(decl pure partial f32_trunc (Ieee32) Ieee32) 384(extern constructor f32_trunc f32_trunc) 385(decl pure partial f32_nearest (Ieee32) Ieee32) 386(extern constructor f32_nearest f32_nearest) 387(decl pure partial f32_min (Ieee32 Ieee32) Ieee32) 388(extern constructor f32_min f32_min) 389(decl pure partial f32_max (Ieee32 Ieee32) Ieee32) 390(extern constructor f32_max f32_max) 391(decl pure f32_neg (Ieee32) Ieee32) 392(extern constructor f32_neg f32_neg) 393(decl pure f32_abs (Ieee32) Ieee32) 394(extern constructor f32_abs f32_abs) 395(decl pure f32_copysign (Ieee32 Ieee32) Ieee32) 396(extern constructor f32_copysign f32_copysign) 397(decl pure partial f64_add (Ieee64 Ieee64) Ieee64) 398(extern constructor f64_add f64_add) 399(decl pure partial f64_sub (Ieee64 Ieee64) Ieee64) 400(extern constructor f64_sub f64_sub) 401(decl pure partial f64_mul (Ieee64 Ieee64) Ieee64) 402(extern constructor f64_mul f64_mul) 403(decl pure partial f64_div (Ieee64 Ieee64) Ieee64) 404(extern constructor f64_div f64_div) 405(decl pure partial f64_sqrt (Ieee64) Ieee64) 406(extern constructor f64_sqrt f64_sqrt) 407(decl pure partial f64_ceil (Ieee64) Ieee64) 408(extern constructor f64_ceil f64_ceil) 409(decl pure partial f64_floor (Ieee64) Ieee64) 410(extern constructor f64_floor f64_floor) 411(decl pure partial f64_trunc (Ieee64) Ieee64) 412(extern constructor f64_trunc f64_trunc) 413(decl pure partial f64_nearest (Ieee64) Ieee64) 414(extern constructor f64_nearest f64_nearest) 415(decl pure partial f64_min (Ieee64 Ieee64) Ieee64) 416(extern constructor f64_min f64_min) 417(decl pure partial f64_max (Ieee64 Ieee64) Ieee64) 418(extern constructor f64_max f64_max) 419(decl pure f64_neg (Ieee64) Ieee64) 420(extern constructor f64_neg f64_neg) 421(decl pure f64_abs (Ieee64) Ieee64) 422(extern constructor f64_abs f64_abs) 423(decl pure f64_copysign (Ieee64 Ieee64) Ieee64) 424(extern constructor f64_copysign f64_copysign) 425(decl pure partial f128_min (Ieee128 Ieee128) Ieee128) 426(extern constructor f128_min f128_min) 427(decl pure partial f128_max (Ieee128 Ieee128) Ieee128) 428(extern constructor f128_max f128_max) 429(decl pure f128_neg (Ieee128) Ieee128) 430(extern constructor f128_neg f128_neg) 431(decl pure f128_abs (Ieee128) Ieee128) 432(extern constructor f128_abs f128_abs) 433(decl pure f128_copysign (Ieee128 Ieee128) Ieee128) 434(extern constructor f128_copysign f128_copysign) 435(type Ieee128 (primitive Ieee128)) 436 437;;;; `cranelift_codegen::ir::Type` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 438 439(extern const $I8 Type) 440(extern const $I16 Type) 441(extern const $I32 Type) 442(extern const $I64 Type) 443(extern const $I128 Type) 444 445(extern const $F16 Type) 446(extern const $F32 Type) 447(extern const $F64 Type) 448(extern const $F128 Type) 449 450(extern const $I8X8 Type) 451(extern const $I8X16 Type) 452(extern const $I16X4 Type) 453(extern const $I16X8 Type) 454(extern const $I32X2 Type) 455(extern const $I32X4 Type) 456(extern const $I64X2 Type) 457 458(extern const $F16X8 Type) 459(extern const $F32X4 Type) 460(extern const $F64X2 Type) 461 462(extern const $I32X4XN Type) 463 464;; Get the unsigned minimum value for a given type. 465;; This always zero, but is included for completeness. 466(decl pure ty_umin (Type) u64) 467(extern constructor ty_umin ty_umin) 468 469;; Get the unsigned maximum value for a given type. 470(decl pure ty_umax (Type) u64) 471(extern constructor ty_umax ty_umax) 472 473;; Get the signed minimum value for a given type. 474(decl pure ty_smin (Type) u64) 475(extern constructor ty_smin ty_smin) 476 477;; Get the signed maximum value for a given type. 478(decl pure ty_smax (Type) u64) 479(extern constructor ty_smax ty_smax) 480 481;; Get the bit width of a given type. 482(spec (ty_bits x) (provide (= result (int2bv 8 x)))) 483(decl pure ty_bits (Type) u8) 484(extern constructor ty_bits ty_bits) 485 486;; Get the bit width of a given type. 487(spec (ty_bits_u16 x) 488 (provide (= result (int2bv 16 x)))) 489(decl pure ty_bits_u16 (Type) u16) 490(extern constructor ty_bits_u16 ty_bits_u16) 491 492;; Get the bit width of a given type. 493(decl pure ty_bits_u64 (Type) u64) 494(extern constructor ty_bits_u64 ty_bits_u64) 495 496;; Get a mask for the width of a given type. 497(decl pure ty_mask (Type) u64) 498(extern constructor ty_mask ty_mask) 499 500;; Get a mask that is set for each lane in a given type. 501(decl pure ty_lane_mask (Type) u64) 502(extern constructor ty_lane_mask ty_lane_mask) 503 504;; Get the number of lanes for a given type. 505(decl pure ty_lane_count (Type) u64) 506(extern constructor ty_lane_count ty_lane_count) 507 508;; Get the byte width of a given type. 509(decl pure ty_bytes (Type) u16) 510(extern constructor ty_bytes ty_bytes) 511 512;; Get the type of each lane in the given type. 513(decl pure lane_type (Type) Type) 514(extern constructor lane_type lane_type) 515 516;; Get a type with the same element type, but half the number of lanes. 517(decl pure partial ty_half_lanes (Type) Type) 518(extern constructor ty_half_lanes ty_half_lanes) 519 520;; Get a type with the same number of lanes but a lane type that is half as small. 521(decl pure partial ty_half_width (Type) Type) 522(extern constructor ty_half_width ty_half_width) 523 524;; Generate a mask for the maximum shift amount for a given type. i.e 31 for I32. 525(decl pure ty_shift_mask (Type) u64) 526(rule (ty_shift_mask ty) (u64_sub (ty_bits (lane_type ty)) 1)) 527 528;; Compare two types for equality. 529(decl pure ty_equal (Type Type) bool) 530(extern constructor ty_equal ty_equal) 531 532;;;; `cranelift_codegen::ir::MemFlags ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 533 534;; Provide model for the MemFlags type (declared in generated clif_lower.isle). 535(model MemFlags (type (bv 16))) 536 537;; `MemFlags::trusted` 538(spec (mem_flags_trusted) 539 (provide (= result #x0003))) 540(decl pure mem_flags_trusted () MemFlags) 541(extern constructor mem_flags_trusted mem_flags_trusted) 542 543;; Determine if flags specify little- or native-endian. 544(decl little_or_native_endian (MemFlags) MemFlags) 545(extern extractor little_or_native_endian little_or_native_endian) 546 547;;;; Helpers for Working with Flags ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 548 549;; Swap args of an IntCC flag. 550(decl intcc_swap_args (IntCC) IntCC) 551(extern constructor intcc_swap_args intcc_swap_args) 552 553;; Complement an IntCC flag. 554(decl intcc_complement (IntCC) IntCC) 555(extern constructor intcc_complement intcc_complement) 556 557;; This is a direct import of `IntCC::without_equal`. 558;; Get the corresponding IntCC with the equal component removed. 559;; For conditions without a zero component, this is a no-op. 560(decl pure intcc_without_eq (IntCC) IntCC) 561(extern constructor intcc_without_eq intcc_without_eq) 562 563;; Swap args of a FloatCC flag. 564(decl floatcc_swap_args (FloatCC) FloatCC) 565(extern constructor floatcc_swap_args floatcc_swap_args) 566 567;; Complement a FloatCC flag. 568(decl floatcc_complement (FloatCC) FloatCC) 569(extern constructor floatcc_complement floatcc_complement) 570 571;; True when this FloatCC involves an unordered comparison. 572(decl pure floatcc_unordered (FloatCC) bool) 573(extern constructor floatcc_unordered floatcc_unordered) 574 575;;;; Helper Clif Extractors ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 576 577;; An extractor that only matches types that can fit in 16 bits. 578(spec (fits_in_16 arg) 579 (provide (= result arg)) 580 (require (<= arg 16))) 581(decl fits_in_16 (Type) Type) 582(extern extractor fits_in_16 fits_in_16) 583 584;; An extractor that only matches types that can fit in 32 bits. 585(spec (fits_in_32 arg) 586 (provide (= result arg)) 587 (require (<= arg 32))) 588(decl fits_in_32 (Type) Type) 589(extern extractor fits_in_32 fits_in_32) 590 591;; An extractor that only matches types that can fit in 32 bits. 592(decl lane_fits_in_32 (Type) Type) 593(extern extractor lane_fits_in_32 lane_fits_in_32) 594 595;; An extractor that only matches types that can fit in 64 bits. 596(spec (fits_in_64 arg) 597 (provide (= result arg)) 598 (require (<= arg 64))) 599(decl fits_in_64 (Type) Type) 600(extern extractor fits_in_64 fits_in_64) 601 602;; An extractor that only matches types that fit in exactly 16 bits. 603(decl ty_16 (Type) Type) 604(extern extractor ty_16 ty_16) 605 606;; An extractor that only matches types that fit in exactly 32 bits. 607(decl ty_32 (Type) Type) 608(extern extractor ty_32 ty_32) 609 610;; An extractor that only matches types that fit in exactly 64 bits. 611(decl ty_64 (Type) Type) 612(extern extractor ty_64 ty_64) 613 614;; An extractor that only matches types that fit in exactly 128 bits. 615(decl ty_128 (Type) Type) 616(extern extractor ty_128 ty_128) 617 618;; A pure constructor/extractor that only matches scalar integers, and 619;; references that can fit in 64 bits. 620(spec (ty_int_ref_scalar_64 arg) 621 (provide (= result arg)) 622 (require (<= arg 64))) 623(decl pure partial ty_int_ref_scalar_64 (Type) Type) 624(extern constructor ty_int_ref_scalar_64 ty_int_ref_scalar_64) 625(extern extractor ty_int_ref_scalar_64 ty_int_ref_scalar_64_extract) 626 627;; An extractor that matches 32- and 64-bit types only. 628(spec (ty_32_or_64 arg) 629 (provide (= result arg)) 630 (require (or (= arg 32) (= arg 64)))) 631(decl ty_32_or_64 (Type) Type) 632(extern extractor ty_32_or_64 ty_32_or_64) 633 634;; An extractor that matches 8- and 16-bit types only. 635(decl ty_8_or_16 (Type) Type) 636(extern extractor ty_8_or_16 ty_8_or_16) 637 638;; An extractor that matches 16- and 32-bit types only. 639(decl ty_16_or_32 (Type) Type) 640(extern extractor ty_16_or_32 ty_16_or_32) 641 642;; An extractor that matches int types that fit in 32 bits. 643(decl int_fits_in_32 (Type) Type) 644(extern extractor int_fits_in_32 int_fits_in_32) 645 646;; An extractor that matches I64. 647(decl ty_int_ref_64 (Type) Type) 648(extern extractor ty_int_ref_64 ty_int_ref_64) 649 650;; An extractor that matches int or reference types bigger than 16 bits but at most 64 bits. 651(decl ty_int_ref_16_to_64 (Type) Type) 652(extern extractor ty_int_ref_16_to_64 ty_int_ref_16_to_64) 653 654;; An extractor that only matches integers. 655(spec (ty_int a) (provide (= result a))) 656(decl ty_int (Type) Type) 657(extern extractor ty_int ty_int) 658 659;; An extractor that only matches scalar types, float or int or ref's. 660(decl ty_scalar (Type) Type) 661(extern extractor ty_scalar ty_scalar) 662 663;; An extractor that only matches scalar floating-point types. 664(decl ty_scalar_float (Type) Type) 665(extern extractor ty_scalar_float ty_scalar_float) 666 667;; An extractor that matches scalar floating-point types or vector types. 668(decl ty_float_or_vec (Type) Type) 669(extern extractor ty_float_or_vec ty_float_or_vec) 670 671;; A pure constructor that only matches vector floating-point types. 672(decl pure partial ty_vector_float (Type) Type) 673(extern constructor ty_vector_float ty_vector_float) 674 675;; A pure constructor that only matches vector types with lanes which 676;; are not floating-point. 677(decl pure partial ty_vector_not_float (Type) Type) 678(extern constructor ty_vector_not_float ty_vector_not_float) 679 680;; A pure constructor/extractor that only matches 64-bit vector types. 681(decl pure partial ty_vec64 (Type) Type) 682(extern constructor ty_vec64 ty_vec64_ctor) 683(extern extractor ty_vec64 ty_vec64) 684 685;; An extractor that only matches 128-bit vector types. 686(decl ty_vec128 (Type) Type) 687(extern extractor ty_vec128 ty_vec128) 688 689;; An extractor that only matches dynamic vector types with a 64-bit 690;; base type. 691(decl ty_dyn_vec64 (Type) Type) 692(extern extractor ty_dyn_vec64 ty_dyn_vec64) 693 694;; An extractor that only matches dynamic vector types with a 128-bit 695;; base type. 696(decl ty_dyn_vec128 (Type) Type) 697(extern extractor ty_dyn_vec128 ty_dyn_vec128) 698 699;; An extractor that only matches 64-bit vector types with integer 700;; lanes (I8X8, I16X4, I32X2) 701(decl ty_vec64_int (Type) Type) 702(extern extractor ty_vec64_int ty_vec64_int) 703 704;; An extractor that only matches 128-bit vector types with integer 705;; lanes (I8X16, I16X8, I32X4, I64X2). 706(decl ty_vec128_int (Type) Type) 707(extern extractor ty_vec128_int ty_vec128_int) 708 709;; An extractor that only matches types that can be a 64-bit address. 710(decl ty_addr64 (Type) Type) 711(extern extractor ty_addr64 ty_addr64) 712 713;; A pure constructor that matches everything except vectors with size 32X2. 714(decl pure partial not_vec32x2 (Type) Type) 715(extern constructor not_vec32x2 not_vec32x2) 716 717;; An extractor that matches everything except I64X2 718(decl not_i64x2 () Type) 719(extern extractor not_i64x2 not_i64x2) 720 721;; Extract a `u8` from an `Uimm8`. 722(decl u8_from_uimm8 (u8) Uimm8) 723(extern extractor infallible u8_from_uimm8 u8_from_uimm8) 724 725;; Extract a `u64` from a `bool`. 726(decl u64_from_bool (u64) bool) 727(extern extractor infallible u64_from_bool u64_from_bool) 728 729;; Extract a `u64` from an `Imm64`. 730(spec (u64_from_imm64 arg) (provide (= arg result))) 731(decl u64_from_imm64 (u64) Imm64) 732(extern extractor infallible u64_from_imm64 u64_from_imm64) 733 734;; Extract a `u64` from an `Imm64` which is not zero. 735(decl nonzero_u64_from_imm64 (u64) Imm64) 736(extern extractor nonzero_u64_from_imm64 nonzero_u64_from_imm64) 737 738;; If the given `Imm64` is a power-of-two, extract its log2 value. 739(decl imm64_power_of_two (u64) Imm64) 740(extern extractor imm64_power_of_two imm64_power_of_two) 741 742;; Create a new Imm64. 743(decl pure imm64 (u64) Imm64) 744(extern constructor imm64 imm64) 745 746;; Create a new Imm64, masked to the width of the given type. 747(decl pure imm64_masked (Type u64) Imm64) 748(extern constructor imm64_masked imm64_masked) 749 750;; Extract a `u16` from an `Ieee16`. 751(decl u16_from_ieee16 (u16) Ieee16) 752(extern extractor infallible u16_from_ieee16 u16_from_ieee16) 753 754;; Extract a `u32` from an `Ieee32`. 755(decl u32_from_ieee32 (u32) Ieee32) 756(extern extractor infallible u32_from_ieee32 u32_from_ieee32) 757 758;; Extract a `u64` from an `Ieee64`. 759(decl u64_from_ieee64 (u64) Ieee64) 760(extern extractor infallible u64_from_ieee64 u64_from_ieee64) 761 762;; Match a multi-lane type, extracting (# bits per lane, # lanes) from the given 763;; type. Will only match when there is more than one lane. 764(decl multi_lane (u32 u32) Type) 765(extern extractor multi_lane multi_lane) 766 767;; Match a dynamic-lane type, extracting (# bits per lane) from the given 768;; type. 769(decl dynamic_lane (u32 u32) Type) 770(extern extractor dynamic_lane dynamic_lane) 771 772;; An extractor that only matches 64-bit dynamic vector types with integer 773;; lanes (I8X8XN, I16X4XN, I32X2XN) 774(decl ty_dyn64_int (Type) Type) 775(extern extractor ty_dyn64_int ty_dyn64_int) 776 777;; An extractor that only matches 128-bit dynamic vector types with integer 778;; lanes (I8X16XN, I16X8XN, I32X4XN, I64X2XN). 779(decl ty_dyn128_int (Type) Type) 780(extern extractor ty_dyn128_int ty_dyn128_int) 781 782;; Convert an `Offset32` to a primitive number. 783(spec (offset32_to_i32 offset) (provide (= result offset))) 784(decl pure offset32_to_i32 (Offset32) i32) 785(extern constructor offset32_to_i32 offset32_to_i32) 786 787;; Convert a number to an `Offset32` 788(spec (i32_to_offset32 x) (provide (= result x))) 789(decl pure i32_to_offset32 (i32) Offset32) 790(extern constructor i32_to_offset32 i32_to_offset32) 791 792;; This is a direct import of `IntCC::unsigned`. 793;; Get the corresponding IntCC with the signed component removed. 794;; For conditions without a signed component, this is a no-op. 795(decl pure intcc_unsigned (IntCC) IntCC) 796(extern constructor intcc_unsigned intcc_unsigned) 797 798;; Pure constructor that only matches signed integer cond codes. 799(spec (signed_cond_code c) 800 (provide (= result c)) 801 (require (and (bvuge c #x02) (bvule c #x05)))) 802(decl pure partial signed_cond_code (IntCC) IntCC) 803(extern constructor signed_cond_code signed_cond_code) 804 805;;;; Helpers for Working with TrapCode ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 806 807(decl pure trap_code_division_by_zero () TrapCode) 808(extern constructor trap_code_division_by_zero trap_code_division_by_zero) 809 810(decl pure trap_code_integer_overflow () TrapCode) 811(extern constructor trap_code_integer_overflow trap_code_integer_overflow) 812 813(decl pure trap_code_bad_conversion_to_integer () TrapCode) 814(extern constructor trap_code_bad_conversion_to_integer trap_code_bad_conversion_to_integer) 815 816;;;; Automatic conversions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 817 818(convert Offset32 i32 offset32_to_i32) 819(convert i32 Offset32 i32_to_offset32) 820 821;;;; Common Term Signatures ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 822 823(form 824 bv_unary_8_to_64 825 ((args (bv 8)) (ret (bv 8)) (canon (bv 8))) 826 ((args (bv 16)) (ret (bv 16)) (canon (bv 16))) 827 ((args (bv 32)) (ret (bv 32)) (canon (bv 32))) 828 ((args (bv 64)) (ret (bv 64)) (canon (bv 64))) 829) 830 831(form 832 bv_binary_8_to_64 833 ((args (bv 8) (bv 8)) (ret (bv 8)) (canon (bv 8))) 834 ((args (bv 16) (bv 16)) (ret (bv 16)) (canon (bv 16))) 835 ((args (bv 32) (bv 32)) (ret (bv 32)) (canon (bv 32))) 836 ((args (bv 64) (bv 64)) (ret (bv 64)) (canon (bv 64))) 837) 838 839(form 840 bv_ternary_8_to_64 841 ((args (bv 8) (bv 8) (bv 8)) (ret (bv 8)) (canon (bv 8))) 842 ((args (bv 16) (bv 16) (bv 16)) (ret (bv 16)) (canon (bv 16))) 843 ((args (bv 32) (bv 32) (bv 32)) (ret (bv 32)) (canon (bv 32))) 844 ((args (bv 64) (bv 64) (bv 64)) (ret (bv 64)) (canon (bv 64))) 845) 846