broken_imul.isle

(spec (lower arg)
    (provide (= result arg)))
(decl lower (Inst) InstOutput)

;; Instruction formats.
(type MInst
  (enum
    ;; An ALU operation with two register sources and a register destination.
    (AluRRR
      (alu_op ALUOp)
      (size OperandSize)
)))

;; An ALU operation. This can be paired with several instruction formats
;; below (see `Inst`) in any combination.
(type ALUOp
  (enum
    (Add)
))

(type ALUOp3
  (enum
    ;; Multiply-add
    (MAdd)
))

(type OperandSize extern
      (enum Size32
            Size64))

(decl alu_rrr (ALUOp Type Reg Reg) Reg)
(extern constructor alu_rrr alu_rrr)

(decl alu_rrrr (ALUOp3 Type Reg Reg Reg) Reg)
(extern constructor alu_rrrr alu_rrrr)

(spec (zero_reg)
    (provide (= (zero_ext 64 #x0000000000000000) result)))
(decl zero_reg () Reg)
(extern constructor zero_reg zero_reg)

;; Helper for calculating the `OperandSize` corresponding to a type
(decl operand_size (Type) OperandSize)
(rule (operand_size (fits_in_32 _ty)) (OperandSize.Size32))
(rule (operand_size (fits_in_64 _ty)) (OperandSize.Size64))

;; Helpers for generating `madd` instructions.
(spec (madd ty a b c) 
  (provide 
    (= result 
       (if (<= ty 32) 
           (conv_to 64 (bvadd (extract 31 0 c) (bvmul (extract 31 0 a) (extract 31 0 b))))
           (bvadd c (bvmul a b))))))
(decl madd (Type Reg Reg Reg) Reg)
(rule (madd ty x y z) (alu_rrrr (ALUOp3.MAdd) ty x y z))

;; `i64` and smaller.
(rule (lower (has_type (fits_in_64 ty) (imul x y)))
      (madd ty y y (zero_reg)))