adds mode events to traces (#1433)

A mode event expresses a switch of some processor mode affecting the
execution of all following instructions. The possible values and their
meanings depend on the target. At the moment, the only one that uses
modes is arm, where the mode indicates whether or not thumb mode is
used.

In order to make use of it, it can be provided in `Mode.slot` of
`Theory.program`, such that the computation `Theory.Label.encoding`
can access it, if available.

.merlin

@@ -64,6 +64,7 @@ B lib/bap_sema
 B lib/bap_strings
 B lib/bap_types
 B lib/bap_core_theory
+B lib/bap_traces
 B lib/graphlib
 B lib/monads
 B lib/ogre

lib/arm/arm_target.ml

@@ -7,6 +7,7 @@ open KB.Syntax
 open Poly
 
 module CT = Theory
+module Mode = Bap_trace_event_types.Mode
 
 type r128 and r80 and r64 and r32 and r16 and r8
 
@@ -581,6 +582,11 @@ module Encodings = struct
     provide_primitive ()
 end
 
+module Modes = struct
+  let a32 = Mode.declare ~package:"arm" "a32"
+  let t32 = Mode.declare ~package:"arm" "t32"
+end
+
 let has_t32 label =
   KB.collect CT.Label.unit label >>= function
   | None -> !!false
@@ -639,15 +645,22 @@ let enable_pcode () =
   if is_arm t then pcode
   else Theory.Language.unknown
 
-let guess_encoding interworking label target =
+let guess_encoding interworking label target mode =
   if is_arm target then
     if is_64bit target then !!llvm_a64 else
     if is_thumb_only target
     then !!llvm_t32
-    else match interworking with
-      | Some true -> compute_encoding_from_symbol_table label
+    else
+      let from_mode_or fallback =
+        if Mode.equal mode Modes.t32 then !!llvm_t32
+        else if Mode.equal mode Modes.a32 then !!llvm_a32
+        else fallback () in
+      match interworking with
+      | Some true -> from_mode_or @@ fun () ->
+        compute_encoding_from_symbol_table label
       | Some false -> !!llvm_a32
-      | None -> has_t32 label >>= function
+      | None -> from_mode_or @@ fun () ->
+        has_t32 label >>= function
         | true -> compute_encoding_from_symbol_table label
         | false -> !!llvm_a32
   else !!CT.Language.unknown
@@ -658,8 +671,9 @@ let enable_llvm ?interworking () =
   register llvm_t32 "thumbv7" ~attrs:"+thumb2";
   register llvm_a64 "aarch64";
   KB.promise CT.Label.encoding @@ fun label ->
-  CT.Label.target label >>= guess_encoding interworking label
-
+  let* target = CT.Label.target label in
+  let* mode = KB.collect Mode.slot label in
+  guess_encoding interworking label target mode
 
 let load ?interworking ?(backend="llvm") () =
   enable_loader ();

lib/bap_traces/bap_trace_event_types.ml

@@ -1,5 +1,9 @@
 open Bap.Std
 open Core_kernel
+open Bap_knowledge
+open Bap_core_theory
+
+module KB = Knowledge
 
 module Move = struct
   type 'a t = {
@@ -62,10 +66,16 @@ module Modload = struct
   } [@@deriving bin_io, compare, fields, sexp]
 end
 
+module Mode = struct
+  include KB.Enum.Make()
+  let slot = KB.Class.property ~package:"bap" Theory.Program.cls "mode" domain
+end
+
 type 'a move = 'a Move.t [@@deriving bin_io, compare, sexp]
 type chunk = Chunk.t [@@deriving bin_io, compare, sexp]
 type syscall = Syscall.t [@@deriving bin_io, compare, sexp]
 type exn = Exn.t [@@deriving bin_io, compare, sexp]
 type call = Call.t [@@deriving bin_io, compare, sexp]
 type return = Return.t [@@deriving bin_io, compare, sexp]
 type modload = Modload.t [@@deriving bin_io, compare, sexp]
+type mode = Mode.t [@@deriving bin_io, compare, sexp]

lib/bap_traces/bap_trace_events.ml

@@ -104,6 +104,11 @@ module Pc_update = struct
   let pp = ppv "pc-update" Word.pp
 end
 
+module Mode = struct
+  include Mode
+  let pp = ppv "mode" pp
+end
+
 let memory_load =
   Value.Tag.register (module Load)
     ~name:"memory-load"
@@ -168,3 +173,8 @@ let modload =
   Value.Tag.register (module Modload)
     ~name:"modload"
     ~uuid:"7f842d03-6c9f-4745-af39-002f468f7fc8"
+
+let mode =
+  Value.Tag.register (module Mode)
+    ~name:"mode"
+    ~uuid:"f7ba0979-c3a9-4509-ba14-01faf577d478"

lib/bap_traces/bap_trace_events.mli

@@ -65,3 +65,6 @@ val return : return tag
 
 (** represent an executable module being loaded *)
 val modload : modload tag
+
+(** the CPU mode used for future instructions has changed  *)
+val mode : mode tag

lib/bap_traces/bap_traces.ml

@@ -1,2 +1,3 @@
 module Unix = Caml_unix
 module Std = Bap_trace_std
+module KB = Bap_knowledge.Knowledge

lib/bap_traces/bap_traces.mli

@@ -1,7 +1,11 @@
 open Core_kernel
 open Regular.Std
 open Bap.Std
+open Bap_knowledge
+open Bap_core_theory
+
 module Unix = Caml_unix
+module KB = Knowledge
 
 (** Traces of execution. *)
 module Std : sig
@@ -357,13 +361,22 @@ module Std : sig
     } [@@deriving bin_io, compare, fields, sexp]
   end
 
+
+  (** change of CPU mode (e.g. switch to thumb)  *)
+  module Mode : sig
+    include KB.Enum.S
+    val slot: (Theory.program, t) KB.slot
+  end
+
+
   type 'a move = 'a Move.t [@@deriving bin_io, compare, sexp]
   type chunk = Chunk.t [@@deriving bin_io, compare, sexp]
   type syscall = Syscall.t [@@deriving bin_io, compare, sexp]
   type exn = Exn.t [@@deriving bin_io, compare, sexp]
   type call = Call.t [@@deriving bin_io, compare, sexp]
   type return = Return.t [@@deriving bin_io, compare, sexp]
   type modload = Modload.t [@@deriving bin_io, compare, sexp]
+  type mode = Mode.t [@@deriving bin_io, compare, sexp]
 
   (** Types of events.  *)
   module Event : sig
@@ -409,6 +422,9 @@ module Std : sig
 
     (** a module (shared library) is dynamically linked into a host program. *)
     val modload : modload tag
+
+    (** the CPU mode used for future instructions has changed  *)
+    val mode : mode tag
   end
 
 

oasis/arm

@@ -8,7 +8,7 @@ Library "bap-arm"
  Build$:           flag(everything) || flag(arm)
  BuildDepends:     bap, core_kernel, ppx_bap, regular,
                    bap-core-theory, bap-knowledge, ogre,
-                   bitvec, bitvec-order, bap-primus
+                   bitvec, bitvec-order, bap-primus, bap-traces
  FindlibName:      bap-arm
  Modules:
                  ARM,

oasis/traces

@@ -18,7 +18,7 @@ Library traces
                    Bap_trace_std,
                    Bap_trace_traces,
                    Bap_trace
-  BuildDepends:    bap, core_kernel, uri, uuidm, regular, ppx_bap, core_kernel.caml_unix
+  BuildDepends:    bap, core_kernel, bap-core-theory, bap-knowledge, uri, uuidm, regular, ppx_bap, core_kernel.caml_unix
 
 Library traces_test
   Path:            lib_test/bap_traces