123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262 |
- ((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)))))
|