adds the missing ux*, sx*, s?bz instructions (#1297)

* adds the missing ux* and sx* instructions

We could use Primus Lisp for that but apparently we already have them
implemented but just forgot to update the code and to use it.

* adds cbz and cnbz instructions

Author: ivg

oasis/thumb

@@ -11,6 +11,7 @@ Library thumb_plugin
                     bap, bap-arm, bitvec
   FindlibName:      bap-plugin-thumb
   InternalModules:  Thumb_main,
+                    Thumb_bits,
                     Thumb_branch,
                     Thumb_core,
                     Thumb_mem,

plugins/thumb/thumb_bits.ml

@@ -1,36 +1,17 @@
 open Bap_core_theory
 open Base
 open KB.Syntax
+open Thumb_core
 
-module Env  = Thumb_env.Env
-module Defs = Thumb_defs
+module Make(CT : Theory.Core) = struct
+  open Thumb_core.Make(CT)
+  open Syntax
 
-module Bits(Core : Theory.Core) = struct
-  open Core
-
-  module Utils = Thumb_util.Utils(Core)
-  module DSL = Thumb_dsl.Make(Core)
-
-  open Utils
-
-  let sxtb dest src =
-    DSL.[
-      !$$dest := extend_to Env.byte !$src |> extend_signed
-    ]
-
-  let sxth dest src =
-    DSL.[
-      !$$dest := extend_to Env.half_word !$src |> extend_signed
-    ]
-
-  let uxtb dest src =
-    DSL.[
-      !$$dest := extend_to Env.byte !$src |> extend
+  let sx rd rm = data [
+      rd := CT.signed s32 (var rm)
     ]
 
-  let uxth dest src =
-    DSL.[
-      !$$dest := extend_to Env.half_word !$src |> extend
+  let ux rd rm = data [
+      rd := CT.unsigned s32 (var rm)
     ]
-
 end

plugins/thumb/thumb_branch.ml

@@ -78,4 +78,14 @@ module Make(CT : Theory.Core) = struct
     ]
 
   let blxr pc dst = blr pc dst
+
+  let cbnz pc rn dst =
+    CT.branch CT.(inv@@is_zero (var rn))
+      (goto (pc +> dst))
+      (seq [])
+
+  let cbz pc rn dst =
+    CT.branch CT.(inv@@is_zero (var rn))
+      (goto (pc +> dst))
+      (seq [])
 end

plugins/thumb/thumb_branch.mli

@@ -29,4 +29,10 @@ module Make(CT : Theory.Core) : sig
 
   (** [bl rm] or [blx rm]  *)
   val blr : Bitvec.t -> r32 reg -> eff
+
+  (** [cbnz rm <label>]  *)
+  val cbnz : Bitvec.t -> r32 reg -> int -> eff
+
+  (** [cbz rm <label>]  *)
+  val cbz : Bitvec.t -> r32 reg -> int -> eff
 end

plugins/thumb/thumb_main.ml

@@ -169,15 +169,17 @@ module Thumb(CT : Theory.Core) = struct
       info "unhandled memory operation: %a" pp_insn insn;
       !!Insn.empty
 
+  let lift_bits opcode insn =
+    let open Thumb_bits.Make(CT) in
+    match opcode, (MC.Insn.ops insn : Op.t array) with
+    | `tSXTB, [|Reg rd; Reg rm; _; _|] -> sx (reg rd) (reg rm)
+    | `tSXTH, [|Reg rd; Reg rm; _; _|] -> sx (reg rd) (reg rm)
+    | `tUXTB, [|Reg rd; Reg rm; _; _|] -> ux (reg rd) (reg rm)
+    | `tUXTH, [|Reg rd; Reg rm; _; _|] -> ux (reg rd) (reg rm)
+    | insn ->
+      info "unhandled bit-wise instruction: %a" pp_insn insn;
+      !!Insn.empty
 
-  (* let lift_bits insn ops =
-   *   let open Bits in
-   *   match insn, ops with
-   *   | `tSXTB, [|dest; src; _unknown; _|] -> sxtb dest src
-   *   | `tSXTH, [|dest; src; _unknown; _|] -> sxth dest src
-   *   | `tUXTB, [|dest; src; _unknown; _|] -> uxtb dest src
-   *   | `tUXTH, [|dest; src; _unknown; _|] -> uxth dest src
-   *   | _ -> [] *)
 
   (* these are not entirely complete *)
   let lift_branch pc opcode insn =
@@ -192,6 +194,8 @@ module Thumb(CT : Theory.Core) = struct
     | `tBLXr, [|_; _; Reg dst|]-> blxr pc (reg dst)
     | `tBX, [|Reg dst; _; _|]when is_pc (reg dst) -> bxi pc 0
     | `tBX, [|Reg dst;_;_|] -> bxr (reg dst)
+    | `tCBNZ, [|Reg rn; Imm c|] -> cbnz pc (reg rn) (imm c)
+    | `tCBZ, [|Reg rn; Imm c|] -> cbz pc (reg rn) (imm c)
     | insn ->
       info "unhandled branch: %a" pp_insn insn;
       !!Insn.empty
@@ -200,9 +204,7 @@ module Thumb(CT : Theory.Core) = struct
     | #opmem as op -> lift_mem addr op insn
     | #opmov as op -> lift_move addr op insn
     | #opbranch as op -> lift_branch addr op insn
-    | op ->
-      info "unsupported opcode: %s" (string_of_opcode op);
-      !!Insn.empty
+    | #opbit as op -> lift_bits op insn
 end
 
 
@@ -237,7 +239,8 @@ module Main = struct
       match decode_opcode (MC.Insn.name insn) with
       | None ->
         info "failed to decode MC instruction, unknown opcode: \
-              %s => %a"
+              %a: %s => %a"
+          Memory.pp mem
           (MC.Insn.asm insn)
           Sexp.pp_hum (MC.Insn.sexp_of_t insn);
         !!Insn.empty

plugins/thumb/thumb_opcodes.ml

@@ -89,6 +89,8 @@ type opbranch = [
   | `tBLXi
   | `tBLXr
   | `tBX
+  | `tCBNZ
+  | `tCBZ
 ] [@@deriving bin_io, compare, sexp, enumerate]
 
 type opcode = [