adds more thumb-specific instructions

lib/arm/arm_target.ml

@@ -381,8 +381,8 @@ let enable_arch () =
   | None -> `unknown
 
 
-let llvm_a32 = CT.Language.declare ~package "llvm-A32"
-let llvm_t32 = CT.Language.declare ~package "llvm-T32"
+let llvm_a32 = CT.Language.declare ~package "llvm-armv7"
+let llvm_t32 = CT.Language.declare ~package "llvm-thumbv7"
 let llvm_a64 = CT.Language.declare ~package "llvm-aarch64"
 
 module Dis = Disasm_expert.Basic

plugins/arm/semantics/aarch64.lisp

@@ -1,7 +1,8 @@
 (require bits)
+(require arm-bits)
 
 (declare (context (target armv8-a+le)))
-(defpackage aarch64 (:use core target))
+(defpackage aarch64 (:use core target arm))
 (defpackage llvm-aarch64 (:use aarch64))
 
 (in-package aarch64)
@@ -70,13 +71,6 @@
 (defun ADDWri (dst r1 imm s)
   (set$ (base-reg dst) (+ (base-reg r1) (lshift imm s))))
 
-(defun add-with-carry (rd x y c)
-  (let ((r (+ c y x)))
-    (set NF (msb r))
-    (set VF (overflow r x y))
-    (set ZF (is-zero r))
-    (set CF (carry r x y))
-    (set$ rd r)))
 
 (defun SUBXrx64 (rd rn rm off)
   (set$ rd (- rn (extended rm off))))

plugins/arm/semantics/arm-bits.lisp

@@ -0,0 +1,22 @@
+(defpackage arm (:use core target))
+(declare  (context (target armv4+le)))
+
+(in-package arm)
+
+(defun add-with-carry (rd x y c)
+  (let ((r (+ c y x)))
+    (set NF (msb r))
+    (set VF (overflow r x y))
+    (set ZF (is-zero r))
+    (set CF (carry r x y))
+    (set$ rd r)))
+
+(defun logandnot (rd rn)
+  (logand rd (lnot rn)))
+
+(defmacro shift-with-carry (shift rd rn rm)
+  (let ((r (cast-signed (word-width) rn)))
+    (set CF (msb r))
+    (set$ rd (shift r rm))
+    (set ZF (is-zero rd))
+    (set NF (msb rd))))

plugins/arm/semantics/thumb.lisp

@@ -0,0 +1,65 @@
+(require bits)
+(require arm-bits)
+
+(declare (context (target armv4+le)))
+
+(defpackage thumb (:use core target arm))
+(defpackage llvm-thumbv7 (:use thumb))
+
+(in-package thumb)
+
+(defmacro tLOGs (op rd rn rm)
+  (prog (set$ rd (op rn rm))
+     (set ZF (is-zero rd))
+     (set NF (msb rd))))
+
+(defun tEOR (rd _ rn rm _ _)
+  (tLOGs logxor rd rn rm))
+
+(defun tAND (rd _ rn rm _ _)
+  (tLOGs logand rd rn rm))
+
+(defun tBIC (rd _ rn rm _ _)
+  "bics rd, rn, rm ; with rn = rd"
+  (tLOGs logandnot rd rn rm))
+
+(defun tMVN (rd _ rn _ _)
+  (set$ rd (lnot rn))
+  (set ZF (is-zero rd))
+  (set NF (msb rd)))
+
+(defun tREV (rd rn _ _)
+  (set$ rd (concat
+            (extract 7 0 rn)
+            (extract 15 8 rn)
+            (extract 23 16 rn)
+            (extract 31 24 rn))))
+
+(defun tLSLrr (rd _ rn rm _ _)
+  "lsls rd, rn, rm"
+  (shift-with-carry lshift rd rn rm))
+
+(defun tLSRrr (rd _ rn rm _ _)
+  "lsrs rd, rn, rm"
+  (shift-with-carry rshift rd rn rm))
+
+(defun tTST (rn rm _ _)
+  "tst rn, rm"
+  (let ((rd (logand rn rm)))
+    (set ZF (is-zero rd))
+    (set NF (msb rd))))
+
+(defun tADDhirr (rd rn rm _ _)
+  (set$ rd (+ rn rm)))
+
+(defun tSBC (rd _ rn rm _ _)
+  (add-with-carry rd rn (- rm) CF))
+
+(defun tRSB (rd _ rn _ _)
+  "rsbs	r3, r2, #0"
+  (add-with-carry rd 0 (lnot rn) 1))
+
+(defun tMUL (rd _ rn rm _ _)
+  (set$ rd (* rn rm))
+  (set ZF (is-zero rd))
+  (set NF (msb rd)))

plugins/thumb/thumb_bits.mli

@@ -0,0 +1,8 @@
+open Bap_core_theory
+open Thumb_core
+
+module Make(CT : Theory.Core) : sig
+  open Theory
+  val sx : r32 reg -> _ reg -> unit eff
+  val ux : r32 reg -> _ reg -> unit eff
+end

plugins/thumb/thumb_main.ml

@@ -64,7 +64,7 @@ module Thumb(CT : Theory.Core) = struct
   let has_pc = List.exists ~f:is_pc
   let remove_pc = List.filter ~f:(Fn.non is_pc)
 
-  let lift_move _addr opcode insn =
+  let lift_move addr opcode insn =
     let module T = Thumb_mov.Make(CT) in
     let open T in
     match opcode, (MC.Insn.ops insn : Op.t array) with
@@ -74,6 +74,8 @@ module Thumb(CT : Theory.Core) = struct
       addi8 (reg rd) (imm x)
     | `tADDrr, [|Reg rd; _; Reg rn; Reg rm; _; _|] ->
       addrr (reg rd) (reg rn) (reg rm)
+    | `tADC, [|Reg rd; Reg _; Reg rn; Reg rm; _; _|] ->
+      adcs (reg rd) (reg rn) (reg rm)
     | `tADDrSPi, [|Reg rd; _; Imm x; _; _;|] ->
       addrspi (reg rd) (imm x * 4)
     | `tADDspi, [|_; _; Imm x; _; _|] ->
@@ -105,7 +107,7 @@ module Thumb(CT : Theory.Core) = struct
     | `tORR, [|Reg rd; _; _; Reg rm; _; _|] ->
       lorr (reg rd) (reg rm)
     | insn ->
-      info "unhandled move instruction: %a" pp_insn insn;
+      info "unhandled move instruction: %a: %a" Bitvec.pp addr pp_insn insn;
       !!Insn.empty
 
 

plugins/thumb/thumb_mov.ml

@@ -57,6 +57,15 @@ module Make(CT : Theory.Core) = struct
       vf := overflow_from_add (var r) (var rn) (var rm);
     ]
 
+
+  let adcs rd rn rm = with_result rd @@ fun r -> [
+      r := var rn + var rm + CT.unsigned s32 (var zf);
+      nf := msb (var r);
+      zf := is_zero (var r);
+      cf := carry_from_add (var r) (var rn);
+      vf := overflow_from_add (var r) (var rn) (var rm);
+    ]
+
   let addspi off = data [
       sp += const off;
     ]

plugins/thumb/thumb_mov.mli

@@ -19,6 +19,9 @@ module Make(CT : Theory.Core) : sig
   (** [add sp, #x] aka add(7)  *)
   val addspi : int -> unit eff
 
+  (** [adcs rd rn rm]  *)
+  val adcs : r32 reg -> r32 reg -> r32 reg -> unit eff
+
   (** [subs rd, rn, #x] aka sub(1) *)
   val subi3 : r32 reg -> r32 reg -> int -> unit eff