Adds more missing Thumb instructions (#1511)

* Adds more missing instructions

* `ADR` uses PC aligned by 4

* Fixes `UXT/SXT` bug in the Core Theory Thumb lifter

Co-authored-by: bmourad01 <bmourad@draper.com>

plugins/arm/semantics/arm-bits.lisp

@@ -95,3 +95,16 @@
   (let ((bitv-length (word-width bitv)))
     (assert-msg (= 0 (mod n bitv-length)) "replicate-to-fill n not multiple of len(bitv)")
     (replicate bitv (/ n bitv-length))))
+
+(defun i-shift (r simm)
+  "(i-shift r simm) shifts r according to the encoded shift simm.
+   The first three bits of simm indicate the shift type, and the
+   remaining bits indicate the shift amount."
+  (let ((amt (rshift simm 3)))
+    (case (extract 2 0 simm)
+      0b000 r ; none
+      0b001 (arshift r amt) ; asr
+      0b010 (lshift r amt) ; lsl
+      0b011 (rshift r amt) ; lsr
+      0b100 (logor (rshift r amt) (lshift r (- 32 amt))) ; ror
+      0b101 (logor (lshift (cast-unsigned 32 CF) 31) (rshift r 1))))) ; rrx

plugins/arm/semantics/thumb.lisp

@@ -11,6 +11,18 @@
 
 (in-package thumb)
 
+(defun tCMPhir (rn rm cnd _)
+  "cmp rn, rn"
+  (when (condition-holds cnd)
+    (let ((r (- rn rm)))
+      (set-nzcv-from-registers r rn rm))))
+
+(defun tADR (rd lbl cnd _)
+  "adr rd, lbl"
+  (when (condition-holds cnd)
+    (let ((pc (* 4 (/ (t2pc) 4))))
+      (set$ rd (+ pc (lshift lbl 2))))))
+
 (defmacro tLOGs (op rd rn rm cnd)
   (prog (set$ rd (op rn rm))
      (when (is-unconditional cnd)
@@ -20,6 +32,11 @@
 (defun tEOR (rd _ rn rm cnd _)
   (tLOGs logxor rd rn rm cnd))
 
+(defun t2EORrs (rd rn rm simm cnd _ _)
+  "eor.w rd, rn, rm, simm"
+  (when (condition-holds cnd)
+    (set$ rd (logxor rn (i-shift rm simm)))))
+
 (defun tAND (rd _ rn rm cnd _)
   (tLOGs logand rd rn rm cnd))
 
@@ -41,14 +58,33 @@
               (extract 23 16 rn)
               (extract 31 24 rn)))))
 
+(defun tREV16 (rd rm cnd _)
+  "rev16 rd rm"
+  (when (condition-holds cnd)
+    (set$ rd (concat
+              (extract 23 16 rm)
+              (extract 31 24 rm)
+              (extract 7 0 rm)
+              (extract 15 8 rm)))))
+
 (defun tLSLrr (rd _ rn rm cnd _)
   "lsls rd, rn, rm"
   (shift-with-carry lshift rd rn rm cnd))
 
+(defun t2LSLri (rd rm imm cnd _ _)
+  "lsl.w rd, rm, #imm"
+  (when (condition-holds cnd)
+    (set$ rd (lshift rm imm))))
+
 (defun tLSRrr (rd _ rn rm cnd _)
   "lsrs rd, rn, rm"
   (shift-with-carry rshift rd rn rm cnd))
 
+(defun t2LSRri (rd rm imm cnd _ _)
+  "lsr.w rd, rm, #imm"
+  (when (condition-holds cnd)
+    (set$ rd (rshift rm imm))))
+
 (defun tTST (rn rm _ _)
   "tst rn, rm"
   (let ((rd (logand rn rm)))
@@ -59,26 +95,47 @@
   (when (condition-holds cnd)
     (set$ rd (+ rn (t2reg rm)))))
 
+(defun t2ADDrs (rd rn rm simm cnd _ _)
+  "add.w rd, rn, rm, simm"
+  (when (condition-holds cnd)
+    (set$ rd (+ rn (i-shift rn simm)))))
+
 (defun tSBC (rd _ rn rm cnd _)
   (add-with-carry/it-block rd rn (lnot rm) CF cnd))
 
 (defun tRSB (rd _ rn cnd _)
   "rsbs	r3, r2, #0"
   (add-with-carry/it-block rd 0 (lnot rn) 1 cnd))
 
+(defun t2RSBrs (rd rn rm simm cnd _ _)
+  "rsb rd, rn, rm, simm"
+  (when (condition-holds cnd)
+    (set$ rd (- (i-shift rm simm) rn))))
+
 (defun tMUL (rd _ rn rm cnd _)
   (when (condition-holds cnd)
     (set$ rd (* rn rm))
     (when (is-unconditional cnd)
       (set ZF (is-zero rd))
       (set NF (msb rd)))))
 
+(defun t2STR_PRE (_ rt rn off cnd _)
+  "str rt [rn, #off]!"
+  (when (condition-holds cnd)
+    (set$ rn (+ rn off))
+    (store-word rn rt)))
+
 (defun t2STRDi8 (rt1 rt2 rn imm pre _)
   "strd rt1, rt2, [rn, off]"
   (when (condition-holds pre)
     (store-word (+ rn imm) rt1)
     (store-word (+ rn imm (sizeof word-width)) rt2)))
 
+(defun t2STRs (rt rn rm imm cnd _)
+  "str.w rt [rn, rm, lsl imm]"
+  (when (condition-holds cnd)
+    (store-word (+ rn (lshift rm imm)) rt)))
+
 (defun t2ADDri12 (rd rn imm pre _)
   "addw rd, rn, imm; A7-189, T4 "
   (when (condition-holds pre)
@@ -115,6 +172,30 @@
   (when (condition-holds pre)
     (t2set rt (load-word (+ rn (lshift rm imm))))))
 
+(defun t2LDRi8 (rt rn imm cnd _)
+  "ldr rt, [rn, #-imm]"
+  (when (condition-holds cnd)
+    (set$ rt (load-word (+ rn imm)))))
+
+(defun t2LDRDi8 (rt rt2 rn imm cnd _)
+  "ldrd rt, rt2, [rn, #imm]"
+  (when (condition-holds cnd)
+    (set$ rt (load-word (+ rn imm)))
+    (set$ rt2 (load-word (+ rn imm 4)))))
+
+(defun t2LDR_POST (rt _ rn off cnd _)
+  "ldr rt, [rn], #imm"
+  (when (condition-holds cnd)
+    (let ((tmp rn))
+      (set$ rn (+ rn off))
+      (t2set rt (load-word tmp)))))
+
+(defun t2LDRB_PRE (rt _ rn off cnd _)
+  "ldrb rt, [rn, #off]!"
+  (when (condition-holds cnd)
+    (set$ rn (+ rn off))
+    (set$ rt (cast-unsigned 32 (load-bits 8 rn)))))
+
 (defun t2LDRSBi12 (rt rn imm pre _)
   "ldrsb.w rt, [rn, imm]"
   (when (condition-holds pre)

plugins/thumb/thumb_bits.ml

@@ -7,9 +7,9 @@ module Make(CT : Theory.Core) = struct
   open Thumb_core.Make(CT)
   open Syntax
 
-  let sx rd rm =
-    rd <-? CT.signed s32 (var rm)
+  let sx s rd rm =
+    rd <-? CT.signed s32 (CT.low s (var rm))
 
-  let ux rd rm =
-    rd <-? CT.unsigned s32 (var rm)
+  let ux s rd rm =
+    rd <-? CT.unsigned s32 (CT.low s (var rm))
 end

plugins/thumb/thumb_bits.mli

@@ -2,8 +2,8 @@ open Bap_core_theory
 open Thumb_core
 open Thumb_opcodes
 
-module Make(CT : Theory.Core) : sig
+module Make(_ : Theory.Core) : sig
   open Theory
-  val sx : r32 reg -> _ reg -> cond -> unit eff
-  val ux : r32 reg -> _ reg -> cond -> unit eff
+  val sx : 'a Bitv.t Value.sort -> r32 reg -> _ reg -> cond -> unit eff
+  val ux : 'a Bitv.t Value.sort -> r32 reg -> _ reg -> cond -> unit eff
 end

plugins/thumb/thumb_main.ml

@@ -174,11 +174,12 @@ module Thumb(CT : Theory.Core) = struct
 
   let lift_bits opcode insn =
     let open Thumb_bits.Make(CT) in
+    let open Thumb_core in
     match opcode, (MC.Insn.ops insn : Op.t array) with
-    | `tSXTB, [|Reg rd; Reg rm; Imm c; _|] -> sx (reg rd) (reg rm) (cnd c)
-    | `tSXTH, [|Reg rd; Reg rm; Imm c; _|] -> sx (reg rd) (reg rm) (cnd c)
-    | `tUXTB, [|Reg rd; Reg rm; Imm c; _|] -> ux (reg rd) (reg rm) (cnd c)
-    | `tUXTH, [|Reg rd; Reg rm; Imm c; _|] -> ux (reg rd) (reg rm) (cnd c)
+    | `tSXTB, [|Reg rd; Reg rm; Imm c; _|] -> sx s8 (reg rd) (reg rm) (cnd c)
+    | `tSXTH, [|Reg rd; Reg rm; Imm c; _|] -> sx s16 (reg rd) (reg rm) (cnd c)
+    | `tUXTB, [|Reg rd; Reg rm; Imm c; _|] -> ux s8 (reg rd) (reg rm) (cnd c)
+    | `tUXTH, [|Reg rd; Reg rm; Imm c; _|] -> ux s16 (reg rd) (reg rm) (cnd c)
     | #opbit,_ as insn ->
       info "unhandled bit-wise instruction: %a" pp_insn insn;
       !!Insn.empty