error handling and performance tweaks (#1375)

* error handling and performance tweaks

Sorry for a little bit dirty pull request featuring several
independent changes, but it is really tedious to split it into several
PRs.

The most important and controversial change is that we now capture
conflicts when disassemble. The conflict is reported, the instruction
is marked as invalid and the whole chain instructions that led to it,
is rejected. The previous behavior was terminating the program with
an error message, which to my taste is more correct, but is
unsatisfying from the user-perspective. We might return the old
behavior after the release, in the development version of bap, as most
of the conflicts are programmers' errors. The motivation for
capturing conflicts was introducing pattern-based instruction
encoding identification, which naturally can have false
positives (which we occasionally see in some ARM interworked
binaries).

The other changes concern how our lifters report and handle
errors. Since we can now have multiple lifters each supplying
semantics for a subset of the instruction set, we no longer assume
that an unhandled instruction is an error (it might be handled by some
other lifter). We still report errors on instructions that a lifter
claim to lift but failed to lift.

And since the log file is now much cleaner, I was able to detect some
missing cases, mostly for thumb2 (via arm) instructions, which are now
handled.

Finally, this PR removes the `is-valid` promise from thumb, which
wasn't necessary but was introducing a little bit of slowdown.

* fixes the empty instruction BIL intrinsic

Author: ivg

lib/arm/arm_lifter.ml

@@ -357,13 +357,15 @@ let lift_bits mem ops (insn : bits_insn ) =
 let lift_mult ops insn =
   let open Mul in
   match insn,ops with
-  | `MUL, [|`Reg dest; src1; src2; cond; _rflag; wflag|] ->
+  | `MUL, [|`Reg dest; src1; src2; cond; _; wflag|]
+  | `MUL, [|`Reg dest; src1; src2; cond; wflag|] ->
     let flags = Flags.set_nzf Bil.(var (Env.of_reg dest)) reg32_t in
     exec [
       assn (Env.of_reg dest) Bil.(exp_of_op src1 * exp_of_op src2)
     ] ~flags ~wflag cond
 
-  | `MLA, [|`Reg dest; src1; src2; addend; cond; _rflag; wflag|] ->
+  | `MLA, [|`Reg dest; src1; src2; addend; cond; _; wflag|]
+  | `MLA, [|`Reg dest; src1; src2; addend; cond; wflag|] ->
     let flags = Flags.set_nzf Bil.(var Bil.(Env.of_reg dest)) reg32_t in
     exec [
       assn (Env.of_reg dest)
@@ -376,18 +378,24 @@ let lift_mult ops insn =
         Bil.(exp_of_op addend - exp_of_op src1 * exp_of_op src2)
     ] cond
 
-  | `UMULL, [|lodest; hidest; src1; src2; cond; _rflag; wflag|] ->
+  | `UMULL, [|lodest; hidest; src1; src2; cond; _; wflag|]
+  | `UMULL, [|lodest; hidest; src1; src2; cond; wflag|] ->
     lift_mull ~lodest ~hidest ~src1 ~src2 Unsigned ~wflag cond
 
-  | `SMULL, [|lodest; hidest; src1; src2; cond; _rflag; wflag|] ->
+  | `SMULL, [|lodest; hidest; src1; src2; cond; _; wflag|]
+  | `SMULL, [|lodest; hidest; src1; src2; cond; wflag|] ->
     lift_mull ~lodest ~hidest ~src1 ~src2 Signed ~wflag cond
 
   | `UMLAL, [|lodest; hidest; src1; src2;
-              _loadd; _hiadd; cond; _rflag; wflag|] ->
+              _loadd; _hiadd; cond; _; wflag|]
+  | `UMLAL, [|lodest; hidest; src1; src2;
+              _loadd; _hiadd; cond; wflag|] ->
     lift_mull ~lodest ~hidest ~src1 ~src2 Unsigned ~addend:true ~wflag cond
 
   | `SMLAL, [|lodest; hidest; src1; src2;
-              _loadd; _hiadd; cond; _rflag; wflag|] ->
+              _loadd; _hiadd; cond; _; wflag|]
+  | `SMLAL, [|lodest; hidest; src1; src2;
+              _loadd; _hiadd; cond; wflag|] ->
     lift_mull ~lodest ~hidest ~src1 ~src2 Signed ~addend:true ~wflag cond
 
   (* signed 16bit mul plus a 32bit bit accum, Q *)
@@ -876,6 +884,13 @@ let lift_mem ops insn =
     in
     exec insns cond
 
+  | `LDREX, [|dest1; `Reg _ as dest2; base; cond; _|] ->
+    let insns =
+      Mem_shift.lift_r_op ~dest1 ~dest2 ~base ~offset:(`Imm (word 0))
+        Offset Unsigned W Ld
+    in
+    exec insns cond
+
   | `LDREXB, [|dest1; base; cond; _|] ->
     let insns =
       Mem_shift.lift_r_op ~dest1 ~base ~offset:(`Imm (word 0))
@@ -905,6 +920,13 @@ let lift_mem ops insn =
     let result = [Bil.move (Env.of_reg dest1) (int32 0)] in
     exec (insns @ result) cond
 
+  | `STREX, [|`Reg dest1; src1; `Reg _ as src2; base; cond; _|] ->
+    let insns =
+      Mem_shift.lift_r_op ~dest1:src1 ~dest2:src2 ~base ~offset:(`Imm (word 0))
+        Offset Unsigned W St in
+    let result = [Bil.move (Env.of_reg dest1) (int32 0)] in
+    exec (insns @ result) cond
+
   | `STREXB, [|`Reg dest1; src1; base; cond; _|] ->
     let insns =
       Mem_shift.lift_r_op ~dest1:src1 ~base ~offset:(`Imm (word 0))
@@ -1108,13 +1130,12 @@ let resolve_pc mem = Stmt.map (object
   end)
 
 let insn_exn mem insn : bil Or_error.t =
-  let name = Basic.Insn.name insn in
   let encoding = Theory.Language.read ~package:"bap" (Basic.Insn.encoding insn) in
   Memory.(Addr.Int_err.(!$(max_addr mem) - !$(min_addr mem)))
   >>= Word.to_int >>= fun s -> Size.of_int ((s+1) * 8) >>= fun scale ->
   Memory.get ~scale mem >>= fun word ->
   match Arm_insn.of_basic insn with
-  | None -> errorf "unsupported opcode: %s" name
+  | None -> Ok []
   | Some arm_insn -> match arm_ops (Basic.Insn.ops insn) with
     | Error _ as fail -> fail
     | Ok ops -> Result.return @@ match arm_insn with

lib/bap_disasm/bap_disasm_driver.ml

@@ -3,6 +3,8 @@ open Bap_types.Std
 open Bap_core_theory
 open Bap_image_std
 
+include Bap_main.Loggers()
+
 open KB.Syntax
 
 module Dis = Bap_disasm_basic
@@ -422,6 +424,7 @@ let disassemble ~code ~data ~funs debt base : Machine.state KB.t =
       else f state current mem
     else f state encoding mem
   and skip state addr f =
+    info "encoding for %a is unknown, skipping" Addr.pp addr;
     Machine.view (Machine.skipped state addr) base
       ~empty:KB.return
       ~ready:(fun state current mem ->
@@ -446,17 +449,25 @@ let disassemble ~code ~data ~funs debt base : Machine.state KB.t =
             ~return:KB.return ~init:(Machine.switch init encoding)
             ~stopped:(fun d s -> step d (Machine.stopped s encoding))
             ~hit:(fun d mem insn s ->
-                new_insn mem insn >>= fun label ->
-                let encoding = Machine.encoding s in
-                KB.provide Theory.Label.encoding label encoding.coding >>= fun () ->
-                collect_dests encoding label >>= fun dests ->
-                if Set.is_empty dests.resolved &&
-                   not dests.indirect then
-                  step d @@ Machine.moved s encoding mem
-                else
-                  delay mem insn >>= fun delay ->
-                  step d @@ Machine.jumped s encoding mem dests delay)
-            ~invalid:(fun d _ s ->
+                KB.catch begin
+                  new_insn mem insn >>= fun label ->
+                  let encoding = Machine.encoding s in
+                  KB.provide Theory.Label.encoding label encoding.coding >>= fun () ->
+                  collect_dests encoding label >>= fun dests ->
+                  if Set.is_empty dests.resolved &&
+                     not dests.indirect then
+                    step d @@ Machine.moved s encoding mem
+                  else
+                    delay mem insn >>= fun delay ->
+                    step d @@ Machine.jumped s encoding mem dests
+                      delay
+                end @@ fun problem ->
+                warning "rejecting %a due to a conflict %a"
+                  Memory.pp mem KB.Conflict.pp problem;
+                step d (Machine.failed s encoding s.addr))
+            ~invalid:(fun d mem s ->
+                info "rejecting %a as an invalid instruction"
+                  Memory.pp mem;
                 step d (Machine.failed s encoding s.addr)))
     ~empty:KB.return
 

lib/bap_disasm/bap_disasm_target_factory.ml

@@ -5,7 +5,7 @@ include Bap_disasm_target_intf
 
 let create_stub_target arch =
   let module Lifter = struct
-    let lift _ _ = Or_error.error_string "not implemented"
+    let lift _ _ = Ok []
     let addr_size = Arch.addr_size arch
 
     module CPU = struct

plugins/bil/bil_lifter.ml

@@ -274,10 +274,8 @@ let lift ~enable_intrinsics:{for_all; for_unk; for_special; predicates}
   else
     let module Target = (val target_of_arch arch) in
     match Target.lift mem insn with
-    | Error _ as err ->
-      if for_unk
-      then Ok (create_intrinsic target mem insn)
-      else err
+    | Error _ as err -> err
+    | Ok [] when for_unk -> Ok (create_intrinsic target mem insn)
     | Ok bil ->
       if for_special && has_special bil
       then Ok (create_intrinsic target mem insn)
@@ -297,7 +295,7 @@ let provide_bil ~enable_intrinsics () =
   let* insn = obj-->?Disasm_expert.Basic.Insn.slot in
   match lift ~enable_intrinsics target arch mem insn with
   | Error err ->
-    info "BIL: the BIL lifter failed with %a" Error.pp err;
+    warning "BIL: the BIL lifter failed with %a" Error.pp err;
     KB.return []
   | Ok [] -> KB.return []
   | Ok bil ->
@@ -327,12 +325,12 @@ let provide_lifter ~with_fp () =
     else base_context in
   let is_empty = KB.Domain.is_empty Bil.domain in
   let lifter obj =
-    Theory.Label.target obj >>= fun target ->
-    Theory.instance ~context:(context target) () >>=
-    Theory.require >>= fun (module Core) ->
     KB.collect Bil.code obj >>= fun bil ->
     if is_empty bil then !!Insn.empty
     else
+      Theory.Label.target obj >>= fun target ->
+      Theory.instance ~context:(context target) () >>=
+      Theory.require >>= fun (module Core) ->
       let module Lifter = Theory.Parser.Make(Core) in
       Lifter.run Bil.Theory.parser bil in
   KB.Rule.(declare ~package "bil-semantics" |>

plugins/radare2/radare2_main.ml

@@ -34,7 +34,6 @@ let provide_roots file funcs =
           Bitvec.((addr - bias) mod modulus bits) in
         Option.some_if (Hashtbl.mem funcs addr) true
       else None in
-  promise_property Theory.Label.is_valid;
   promise_property Theory.Label.is_subroutine
 
 let strip str =

plugins/thumb/thumb_main.ml

@@ -106,7 +106,7 @@ module Thumb(CT : Theory.Core) = struct
       cmpr (reg rn) (reg rm)
     | `tORR, [|Reg rd; _; _; Reg rm; Imm c; _|] ->
       lorr (reg rd) (reg rm) (cnd c)
-    | insn ->
+    | #opmov,_ as insn ->
       info "unhandled move instruction: %a: %a" Bitvec.pp addr pp_insn insn;
       !!Insn.empty
 
@@ -151,7 +151,8 @@ module Thumb(CT : Theory.Core) = struct
       strhr (reg rd) (reg rm) (reg rn) (cnd c)
     | #opmem_multi as op,ops ->
       begin match op, Array.to_list ops with
-        | `tSTMIA_UPD, Reg rd :: Imm c :: _ :: ar ->
+        | `tSTMIA_UPD, Reg rd :: Imm c :: _ :: ar
+        | `tSTMIA_UPD, Reg rd :: Reg _ :: Imm c :: _ :: ar ->
           stm (reg rd) (regs ar) (cnd c)
         | `tLDMIA, Reg rd :: Imm c :: _ :: ar ->
           ldm (reg rd) (regs ar) (cnd c)
@@ -166,7 +167,7 @@ module Thumb(CT : Theory.Core) = struct
           info "unhandled multi-reg instruction: %a" pp_insn (op,ops);
           !!Insn.empty
       end
-    | insn ->
+    | #opmem,_ as insn ->
       info "unhandled memory operation: %a" pp_insn insn;
       !!Insn.empty
 
@@ -177,7 +178,7 @@ module Thumb(CT : Theory.Core) = struct
     | `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)
-    | insn ->
+    | #opbit,_ as insn ->
       info "unhandled bit-wise instruction: %a" pp_insn insn;
       !!Insn.empty
 
@@ -192,7 +193,8 @@ module Thumb(CT : Theory.Core) = struct
     | `tB, [|Imm dst; _; _|] -> b pc (imm dst)
     | `tBcc, [|Imm dst; Imm c; _|] -> bcc pc (cnd c) (imm dst)
     | `tBL,   [|_; _; Imm dst; _|]
-    | `tBLXi, [|_; _; Imm dst|] -> bli pc (imm dst)
+    | `tBLXi, ([|_; _; Imm dst|] | [|_; _; Imm dst; _|] )  ->
+      bli pc (imm dst)
     | `tBLXr, [|_; _; Reg dst|]when is_pc (reg dst) ->
       (* blx pc is unpredictable in all versions of ARM *)
       Thumb.ctrl unpredictable
@@ -201,7 +203,7 @@ module Thumb(CT : Theory.Core) = struct
     | `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 ->
+    | #opbranch,_ as insn ->
       info "unhandled branch: %a" pp_insn insn;
       !!Insn.empty
 
@@ -216,22 +218,6 @@ end
 module Main = struct
   open Bap.Std
 
-  let cmnz_opcode = Word.of_int 10 0x10b
-
-  (* this is a temporary fix since bap-mc disassembler couldn't recognize CMN *)
-  let fix_cmnz insn mem = match insn with
-    | Some insn -> Some insn
-    | None ->
-      let opcode =
-        let open Or_error.Monad_infix in
-        let scale = Size.of_int_exn 16 in
-        Memory.get ~scale mem >>=
-        Word.extract ~hi:15 ~lo:6 in
-      match opcode with
-      | Ok opcode when Word.equal opcode cmnz_opcode ->
-        Some `tCMNz
-      | _ -> None
-
   let load () =
     KB.promise Theory.Semantics.slot @@ fun label ->
     KB.collect Theory.Label.encoding label >>= fun encoding ->
@@ -242,13 +228,7 @@ module Main = struct
       let module Thumb = Thumb(Core) in
       let addr = Word.to_bitvec@@Memory.min_addr mem in
       match decode_opcode (MC.Insn.name insn) with
-      | None ->
-        info "failed to decode MC instruction, unknown opcode: \
-              %a: %s => %a"
-          Memory.pp mem
-          (MC.Insn.asm insn)
-          Sexp.pp_hum (MC.Insn.sexp_of_t insn);
-        !!Insn.empty
+      | None -> !!Insn.empty
       | Some opcode ->
         try
           Thumb.lift_insn addr opcode insn >>| fun sema ->

plugins/thumb/thumb_opcodes.ml

@@ -3,43 +3,24 @@ open Bap.Std
 
 (* all the `mov` series, registers marked with `e` means extended *)
 type opmov = [
-  | `tMOVi8 (* Rd imm8 *)
-  | `tMOVSr (* Rd Rm affect CSPR *)
-  | `tMVN (* Rd Rm *)
-  | `tADC (* Rd Rn Rm *)
-  | `tADDi3 (* Rd Rs imm *)
-  | `tADDi8 (* Rd imm *)
-  | `tADDrr (* Rd Rn Rm *)
-  | `tADDhirr (* Rde Rse *)
-  | `tADR (* Rd imm *)
-  | `tADDrSPi (* Rd imm *)
-  | `tADDspi (* imm *)
-  | `tAND
+  |  `tADC
+  | `tADDi3
+  | `tADDi8
+  | `tADDrSPi
+  | `tADDrr
+  | `tADDspi
   | `tASRri
-  | `tASRrr
-  | `tBIC
-  | `tCMNz
   | `tCMPi8
   | `tCMPr
-  | `tCMPhir
-  | `tEOR
   | `tLSLri
-  | `tLSLrr
   | `tLSRri
-  | `tLSRrr
+  | `tMOVSr
+  | `tMOVi8
   | `tORR
-  | `tRSB (* NEG *)
-  | `tREV
-  | `tREV16
-  | `tREVSH
-  | `tROR
-  | `tSBC (* Rd Rm *)
-  | `tSUBi3 (* See the corresponding ADD insns. *)
+  | `tSUBi3
   | `tSUBi8
   | `tSUBrr
   | `tSUBspi
-  | `tTST
-  | `tMUL (* Rd Rn *)
 ] [@@deriving bin_io, compare, sexp, enumerate]
 
 type opbit = [
@@ -61,36 +42,29 @@ type opmem_multi = [
 
 
 type opmem = [
-  | `tLDRi
-  | `tLDRr
-  | `tLDRpci | `t2LDRpci
-  | `tLDRspi
+  | opmem_multi
+  | `t2LDRpci
   | `tLDRBi
   | `tLDRBr
   | `tLDRHi
   | `tLDRHr
   | `tLDRSB
   | `tLDRSH
-  | `tSTRi
-  | `tSTRr
-  | `tSTRspi
+  | `tLDRi
+  | `tLDRpci
+  | `tLDRr
+  | `tLDRspi
   | `tSTRBi
   | `tSTRBr
   | `tSTRHi
   | `tSTRHr
-  | opmem_multi
+  | `tSTRi
+  | `tSTRr
+  | `tSTRspi
 ] [@@deriving bin_io, compare, sexp, enumerate]
 
-type opbranch = [
-  | `tBcc
-  | `tB
-  | `tBL
-  | `tBLXi
-  | `tBLXr
-  | `tBX
-  | `tCBNZ
-  | `tCBZ
-] [@@deriving bin_io, compare, sexp, enumerate]
+type opbranch = [ `tB | `tBL | `tBLXi | `tBLXr | `tBX | `tBcc | `tCBNZ | `tCBZ ]
+[@@deriving bin_io, compare, sexp, enumerate]
 
 type opcode = [
   | opmov