((operands
((rD . 'GPR)
(setcc . 'Cc_out)
(predBits . 'Pred)
(rM . 'GPR)
(rN . 'GPR)))
(in (setcc rN rM 'CPSR 'PC))
(defs
(('PC
(ite
((_ call "arm.is_r15") rD)
(ite
(bveq
#b0
((_ extract 0 0)
((_ extract 31 0)
(bvadd
(bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001)))))
(bvand
#xfffffffe
((_ extract 31 0)
(bvadd
(bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001))))
(ite
(bveq
#b0
((_ extract 1 1)
((_ extract 31 0)
(bvadd
(bvadd
((_ zero_extend 1) rN)
((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001)))))
(bvand
#xfffffffd
((_ extract 31 0)
(bvadd
(bvadd
((_ zero_extend 1) rN)
((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001))))
((_ extract 31 0)
(bvadd
(bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001)))))
(bvadd 'PC #x00000004)))
('CPSR
(ite
(ite
(andp (bveq #b1 ((_ extract 0 0) predBits)) (bvne predBits #xf))
(notp
(ite
(bveq ((_ extract 3 1) predBits) #b000)
(bveq #b1 ((_ extract 30 30) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b001)
(bveq #b1 ((_ extract 29 29) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b010)
(bveq #b1 ((_ extract 31 31) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b011)
(bveq #b1 ((_ extract 28 28) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b100)
(andp
(bveq #b1 ((_ extract 29 29) 'CPSR))
(notp (bveq #b1 ((_ extract 30 30) 'CPSR))))
(ite
(bveq ((_ extract 3 1) predBits) #b101)
(bveq
((_ extract 31 31) 'CPSR)
((_ extract 28 28) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b110)
(andp
(bveq
((_ extract 31 31) 'CPSR)
((_ extract 28 28) 'CPSR))
(notp (bveq #b1 ((_ extract 30 30) 'CPSR))))
(bveq #b0 #b0)))))))))
(ite
(bveq ((_ extract 3 1) predBits) #b000)
(bveq #b1 ((_ extract 30 30) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b001)
(bveq #b1 ((_ extract 29 29) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b010)
(bveq #b1 ((_ extract 31 31) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b011)
(bveq #b1 ((_ extract 28 28) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b100)
(andp
(bveq #b1 ((_ extract 29 29) 'CPSR))
(notp (bveq #b1 ((_ extract 30 30) 'CPSR))))
(ite
(bveq ((_ extract 3 1) predBits) #b101)
(bveq
((_ extract 31 31) 'CPSR)
((_ extract 28 28) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b110)
(andp
(bveq
((_ extract 31 31) 'CPSR)
((_ extract 28 28) 'CPSR))
(notp (bveq #b1 ((_ extract 30 30) 'CPSR))))
(bveq #b0 #b0)))))))))
(ite
(andp (bveq setcc #b1) (notp ((_ call "arm.is_r15") rD)))
(concat
(concat
((_ extract 31 31)
((_ extract 31 0)
(bvadd
(bvadd
((_ zero_extend 1) rN)
((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001))))
(concat
(ite
(bveq
((_ extract 31 0)
(bvadd
(bvadd
((_ zero_extend 1) rN)
((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001)))
#x00000000)
#b1
#b0)
(concat
((_ extract 32 32)
(bvadd
(bvadd
((_ zero_extend 1) rN)
((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001)))
(bvand
((_ extract 31 31)
((_ extract 31 0)
(bvadd
(bvadd
((_ zero_extend 1) rN)
((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001))))
((_ extract 32 32)
(bvadd
(bvadd
((_ zero_extend 1) rN)
((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001)))))))
((_ extract 27 0)
(ite
((_ call "arm.is_r15") rD)
(ite
(bveq
#b0
((_ extract 0 0)
((_ extract 31 0)
(bvadd
(bvadd
((_ zero_extend 1) rN)
((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001)))))
(bvand #xfeffffff (bvor #x00000020 'CPSR))
'CPSR)
'CPSR)))
(ite
((_ call "arm.is_r15") rD)
(ite
(bveq
#b0
((_ extract 0 0)
((_ extract 31 0)
(bvadd
(bvadd
((_ zero_extend 1) rN)
((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001)))))
(bvand #xfeffffff (bvor #x00000020 'CPSR))
'CPSR)
'CPSR))
'CPSR))
(rD
(ite
(ite
(andp (bveq #b1 ((_ extract 0 0) predBits)) (bvne predBits #xf))
(notp
(ite
(bveq ((_ extract 3 1) predBits) #b000)
(bveq #b1 ((_ extract 30 30) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b001)
(bveq #b1 ((_ extract 29 29) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b010)
(bveq #b1 ((_ extract 31 31) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b011)
(bveq #b1 ((_ extract 28 28) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b100)
(andp
(bveq #b1 ((_ extract 29 29) 'CPSR))
(notp (bveq #b1 ((_ extract 30 30) 'CPSR))))
(ite
(bveq ((_ extract 3 1) predBits) #b101)
(bveq
((_ extract 31 31) 'CPSR)
((_ extract 28 28) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b110)
(andp
(bveq
((_ extract 31 31) 'CPSR)
((_ extract 28 28) 'CPSR))
(notp (bveq #b1 ((_ extract 30 30) 'CPSR))))
(bveq #b0 #b0)))))))))
(ite
(bveq ((_ extract 3 1) predBits) #b000)
(bveq #b1 ((_ extract 30 30) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b001)
(bveq #b1 ((_ extract 29 29) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b010)
(bveq #b1 ((_ extract 31 31) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b011)
(bveq #b1 ((_ extract 28 28) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b100)
(andp
(bveq #b1 ((_ extract 29 29) 'CPSR))
(notp (bveq #b1 ((_ extract 30 30) 'CPSR))))
(ite
(bveq ((_ extract 3 1) predBits) #b101)
(bveq
((_ extract 31 31) 'CPSR)
((_ extract 28 28) 'CPSR))
(ite
(bveq ((_ extract 3 1) predBits) #b110)
(andp
(bveq
((_ extract 31 31) 'CPSR)
((_ extract 28 28) 'CPSR))
(notp (bveq #b1 ((_ extract 30 30) 'CPSR))))
(bveq #b0 #b0)))))))))
(ite
((_ call "arm.is_r15") rD)
rD
((_ extract 31 0)
(bvadd
(bvadd ((_ zero_extend 1) rN) ((_ zero_extend 1) (bvnot rM)))
((_ zero_extend 1) #x00000001))))
rD)))))