imm12neg_new.isle

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

(type MInst
  (enum
))

;; Imm12 modeled as the range of intermediates it can represent.
(model Imm12 (type (bv 24)))
(type Imm12 (primitive Imm12))

(type ALUOp
  (enum
    (Add)
))

;; Note that 4094 = 0xffe and 16773119 = 0xffefff
(spec (add_imm ty a b)
  (provide
    (= result
       (if (<= ty 32)
           (conv_to 64 (bvadd (extract 31 0 a) (zero_ext 32 b)))
           (bvadd a (zero_ext 64 b)))))
  (require  (or (<= (bv2int b) 4094)
               (and (<= (bv2int b) 16773119)
                   (= (extract 2 0 b) #b000)))))
(decl add_imm (Type Reg Imm12) Reg)
(rule (add_imm ty x y) (alu_rr_imm12 (ALUOp.Add) ty x y))

(decl alu_rr_imm12 (ALUOp Type Reg Imm12) Reg)
(extern constructor alu_rr_imm12 alu_rr_imm12)

(spec (imm12_from_negated_value arg)
    (provide (or (bvult (bvneg (sign_ext 64 arg)) #x0000000000000fff)
                    (and (bvult (bvneg (sign_ext 64 arg)) #x0000000000fff000)
                        (= (extract 2 0 (bvneg (sign_ext 64 arg))) #b000)))
                (= result (extract 23 0 (bvneg (sign_ext 64 arg))))))
(instantiate imm12_from_negated_value
    ((args (bv 8)) (ret (bv 24)) (canon (bv 8)))
    ((args (bv 16)) (ret (bv 24)) (canon (bv 16)))
    ((args (bv 32)) (ret (bv 24)) (canon (bv 32)))
    ((args (bv 64)) (ret (bv 24)) (canon (bv 64)))
)
(decl pure partial imm12_from_negated_value (Value) Imm12)
(extern extractor imm12_from_negated_value imm12_from_negated_value)

(rule isub_imm12_neg 2 (lower (has_type (fits_in_64 ty) (isub x y)))
      (if-let imm12_neg (imm12_from_negated_value y))
      (add_imm ty x imm12_neg))