Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
bytecodealliance
GitHub Repository: bytecodealliance/wasmtime
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)))