fixes some T32 instructions that are accessing to PC (#1357)

The PC register wasn't handled correctly and slipped into the IR. Some
of the affected instructions were lifted in the OCaml-written part of
lifter and are now rewritten in Primus Lisp (with corrected and extended
semantics).

There are also a few instruction in the ARM lifter (i.e., A32
encoding) that although treat PC correctly but do not initiate the
interworking branch. It might be that handling them correctly might
let us to discover more code in the interworked binaries, see E1-4253
in ARMv8 Architecture reference manual,

```
In A32 state only, ADC, ADD, ADR, AND, ASR (immediate), BIC, EOR, LSL (immediate), LSR (immediate), MOV, MVN, ORR, ROR (immediate), RRX, RSB, RSC, SBC, and SUB instructions with <Rd> equal to the PC and without flag-setting specified
```

Author: ivg

lib/arm/arm_lifter.ml

@@ -1092,14 +1092,18 @@ module CPU = struct
   let is_mem = is mem
 end
 
-
 (** Substitute PC with its value  *)
 let resolve_pc mem = Stmt.map (object
     inherit Stmt.mapper as super
     method! map_var var =
       if Var.(equal var CPU.pc) then
         Bil.int (CPU.addr_of_pc mem)
       else super#map_var var
+
+    method! map_move v x =
+      if Var.(equal v CPU.pc)
+      then super#map_jmp x
+      else super#map_move v x
   end)
 
 let insn_exn mem insn : bil Or_error.t =

plugins/arm/semantics/thumb.lisp

@@ -53,7 +53,7 @@
     (set NF (msb rd))))
 
 (defun tADDhirr (rd rn rm _ _)
-  (set$ rd (+ rn rm)))
+  (set$ rd (+ rn (t2reg rm))))
 
 (defun tSBC (rd _ rn rm _ _)
   (add-with-carry rd rn (lnot rm) CF))
@@ -87,4 +87,24 @@
 (defun t2B (off pre _)
   "b.w imm; A7-207, T3"
   (when (condition-holds pre)
-    (exec-addr (+ (get-program-counter) off 4))))
+    (exec-addr (+ (t2pc) off))))
+
+(defun t2LDRs (rt rn rm imm pre _)
+  (when (condition-holds pre)
+    (t2set rt (load-word (+ rn (lshift rm imm))))))
+
+(defun tMOVr (rt rn pre _)
+  (when (condition-holds pre)
+    (t2set rt rn)))
+
+(defun t2pc () (+ (get-program-counter) 4))
+
+(defun is-pc (r) (= (symbol r) 'PC))
+
+(defun t2reg (r)
+  (if (is-pc r) (t2pc) r))
+
+(defun t2set (reg val)
+  (if (is-pc reg)
+      (exec-addr val)
+    (set$ reg val)))

plugins/thumb/thumb_main.ml

@@ -94,8 +94,6 @@ module Thumb(CT : Theory.Core) = struct
       movi8 (reg rd) (imm x)
     | `tMOVSr, [|Reg rd; Reg rn|] ->
       movsr (reg rd) (reg rn)
-    | `tMOVr, [|Reg rd; Reg rn; _; _|] ->
-      movr (reg rd) (reg rn)
     | `tASRri, [|Reg rd; _; Reg rm; Imm x; _; _|] ->
       asri (reg rd) (reg rm) (imm x)
     | `tLSRri, [|Reg rd; _; Reg rm; Imm x; _; _|] ->
@@ -120,8 +118,7 @@ module Thumb(CT : Theory.Core) = struct
     | `tLDRi,   [|Reg rd; Reg rm; Imm i; _; _|]
     | `tLDRspi, [|Reg rd; Reg rm; Imm i; _; _|] ->
       ldri (reg rd) (reg rm) (imm i * 4)
-    | `tLDRr, [|Reg rd; Reg rm; Reg rn; _; _|]
-    | `t2LDRs, [|Reg rd; Reg rm; Reg rn; _; _; _|] ->
+    | `tLDRr, [|Reg rd; Reg rm; Reg rn; _; _|] ->
       ldrr (reg rd) (reg rm) (reg rn)
     | `tLDRpci, [|Reg rd; Imm i; _; _|] ->
       ldrpci (reg rd) W32.(pc + int 2) (imm i)

plugins/thumb/thumb_mov.ml

@@ -29,10 +29,6 @@ module Make(CT : Theory.Core) = struct
       zf := is_zero (var rd);
     ]
 
-  let movr rd rn = data [
-      rd := var rn
-    ]
-
   let addi3 rd rn x = with_result rd @@ fun r -> [
       r := var rn + const x;
       nf := msb (var r);

plugins/thumb/thumb_mov.mli

@@ -40,9 +40,6 @@ module Make(CT : Theory.Core) : sig
   (** [movs rd, rn]  *)
   val movsr : r32 reg -> r32 reg -> unit eff
 
-  (** [mov rd, rn] with [d] or [n] greater than 7.  *)
-  val movr  : r32 reg -> r32 reg -> unit eff
-
   (** [asrs rd, rn, #i]  *)
   val asri : r32 reg -> r32 reg -> int -> unit eff
 

plugins/thumb/thumb_opcodes.ml

@@ -4,7 +4,6 @@ open Bap.Std
 (* all the `mov` series, registers marked with `e` means extended *)
 type opmov = [
   | `tMOVi8 (* Rd imm8 *)
-  | `tMOVr (* Rde Rse *)
   | `tMOVSr (* Rd Rm affect CSPR *)
   | `tMVN (* Rd Rm *)
   | `tADC (* Rd Rn Rm *)
@@ -63,7 +62,7 @@ type opmem_multi = [
 
 type opmem = [
   | `tLDRi
-  | `tLDRr   | `t2LDRs
+  | `tLDRr
   | `tLDRpci | `t2LDRpci
   | `tLDRspi
   | `tLDRBi