From 7808bccc6beea56b23d88890906d4ba2a031fe14 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Florian=20M=C3=A4rkl?= Date: Mon, 14 Feb 2022 19:54:53 +0100 Subject: [PATCH] adds mode events to traces 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 | 1 + lib/arm/arm_target.ml | 26 +++++++++++++++++++------ lib/bap_traces/bap_trace_event_types.ml | 10 ++++++++++ lib/bap_traces/bap_trace_events.ml | 10 ++++++++++ lib/bap_traces/bap_trace_events.mli | 3 +++ lib/bap_traces/bap_traces.ml | 1 + lib/bap_traces/bap_traces.mli | 16 +++++++++++++++ oasis/arm | 2 +- oasis/traces | 2 +- 9 files changed, 63 insertions(+), 8 deletions(-) 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