diff --git a/.merlin b/.merlin index 89aa7e875..f41d6e92d 100644 --- a/.merlin +++ b/.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 diff --git a/lib/arm/arm_target.ml b/lib/arm/arm_target.ml index f68e217d2..4fdfbd396 100644 --- a/lib/arm/arm_target.ml +++ b/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 (); diff --git a/lib/bap_traces/bap_trace_event_types.ml b/lib/bap_traces/bap_trace_event_types.ml index f923615ab..3ae393e22 100644 --- a/lib/bap_traces/bap_trace_event_types.ml +++ b/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,6 +66,11 @@ 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] @@ -69,3 +78,4 @@ 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] diff --git a/lib/bap_traces/bap_trace_events.ml b/lib/bap_traces/bap_trace_events.ml index ecef5f552..6971e7cbf 100644 --- a/lib/bap_traces/bap_trace_events.ml +++ b/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" diff --git a/lib/bap_traces/bap_trace_events.mli b/lib/bap_traces/bap_trace_events.mli index 829818149..1b141cd49 100644 --- a/lib/bap_traces/bap_trace_events.mli +++ b/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 diff --git a/lib/bap_traces/bap_traces.ml b/lib/bap_traces/bap_traces.ml index 1eeec2ee3..500c47eba 100644 --- a/lib/bap_traces/bap_traces.ml +++ b/lib/bap_traces/bap_traces.ml @@ -1,2 +1,3 @@ module Unix = Caml_unix module Std = Bap_trace_std +module KB = Bap_knowledge.Knowledge diff --git a/lib/bap_traces/bap_traces.mli b/lib/bap_traces/bap_traces.mli index 83acc0138..9a6e3763d 100644 --- a/lib/bap_traces/bap_traces.mli +++ b/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,6 +361,14 @@ 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] @@ -364,6 +376,7 @@ module Std : sig 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 diff --git a/oasis/arm b/oasis/arm index 358452a6a..e29af8a04 100644 --- a/oasis/arm +++ b/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, diff --git a/oasis/traces b/oasis/traces index 94b79a073..06772b05c 100644 --- a/oasis/traces +++ b/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