Path: blob/main/cranelift/isle/veri/veri_engine/examples/broken/broken_uextend.isle
1693 views
(spec (lower arg) (provide (= result arg))) (decl lower (Inst) InstOutput) ;; Instruction formats. (type MInst (enum ;; A sign- or zero-extend operation. (Extend (rd WritableReg) (rn Reg) (signed bool) (from_bits u8) (to_bits u8)) )) ;; Helper for emitting `MInst.Extend` instructions. ;; BROKEN: zero_ext and sign_ext swapped (spec (extend a b c d) (provide (if b (= result (zero_ext (bv2int d) (conv_to (bv2int c) a))) (= result (sign_ext (bv2int d) (conv_to (bv2int c) a)))))) (decl extend (Reg bool u8 u8) Reg) (rule (extend rn signed from_bits to_bits) (let ((dst WritableReg (temp_writable_reg $I64)) (_ Unit (emit (MInst.Extend dst rn signed from_bits to_bits)))) dst)) ;; General rule for extending input to an output which fits in a single ;; register. (rule (lower (has_type (fits_in_64 out) (uextend x @ (value_type in)))) (extend x false (ty_bits in) (ty_bits out)))