Path: blob/main/cranelift/isle/veri/veri_engine/examples/broken/broken_uextend.isle
3149 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)))