Adds insn-code to the Theory.Semantics class (BinaryAnalysisPlatf…

…orm#1389) * Adds `label-bytes` slot to the `Theory.program` objects The `Memory.slot` property is not serialized, which is a bummer. This change aims to provide a more lightweight version which can be serialized. It may be of interest to analyst to observe the memory contents of a particular instruction (or simply to know its physical length). * Runs `make indent` * Uses a nicer `inspect` function for `bytes` domain * Moves the property to the `Theory.Semantics.cls` Co-authored-by: bmourad01 <bmourad@draper.com>
thestr4ng3r · Jan 5, 2022 · 5be8fef · 5be8fef
1 parent 3d90994
commit 5be8fef
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 1 deletion.
diff --git a/lib/bap_core_theory/bap_core_theory.mli b/lib/bap_core_theory/bap_core_theory.mli
@@ -1303,6 +1303,9 @@ module Theory : sig
         @since 2.3.0 *)
     val value : (cls, unit Value.t) Knowledge.slot
 
+    (** the memory contents of the program. *)
+    val code : (cls, string option) Knowledge.slot
+
     include Knowledge.Value.S with type t := t
   end
 
@@ -1798,7 +1801,6 @@ module Theory : sig
     (** the address of the label.  *)
     val addr : (program, Bitvec.t option) KB.slot
 
-
     (** the linkage name of the label  *)
     val name : (program, string option) KB.slot
 

diff --git a/lib/bap_core_theory/bap_core_theory_program.ml b/lib/bap_core_theory/bap_core_theory_program.ml
@@ -20,6 +20,12 @@ let word = Knowledge.Domain.optional "word"
     ~equal:Bitvec.equal
     ~inspect:Bitvec_sexp.sexp_of_t
 
+let hexcode = Knowledge.Domain.optional "hexcode"
+    ~equal:String.equal
+    ~inspect:(Fn.compose sexp_of_string @@
+              String.concat_map ~sep:" " ~f:(fun c ->
+                  Format.sprintf "%02x" @@ Char.to_int c))
+
 let name = Knowledge.Domain.optional "name"
     ~equal:String.equal
     ~inspect:sexp_of_string
@@ -296,6 +302,13 @@ module Semantics = struct
       ~persistent:(Knowledge.Persistent.of_binable (module Value.Top))
       ~public:true
       ~desc:"the program semantics"
+  let code = Knowledge.Class.property ~package cls "insn-code" hexcode
+      ~persistent:(Knowledge.Persistent.of_binable (module struct
+                     type t = string option
+                     [@@deriving bin_io]
+                   end))
+      ~public:true
+      ~desc:"the program memory contents"
 
   include Self
 end

diff --git a/lib/bap_core_theory/bap_core_theory_program.mli b/lib/bap_core_theory/bap_core_theory_program.mli
@@ -19,6 +19,7 @@ module Semantics : sig
   val cls : (cls, unit Effect.sort) Knowledge.cls
   val slot : (program, t) Knowledge.slot
   val value : (cls, unit Value.t) Knowledge.slot
+  val code : (cls, string option) Knowledge.slot
   include Knowledge.Value.S with type t := t
 end
 

diff --git a/lib/bap_image/bap_memory.ml b/lib/bap_image/bap_memory.ml
@@ -464,6 +464,14 @@ let () =
   KB.collect slot label >>|? fun mem ->
   Some (Addr.to_bitvec (min_addr mem))
 
+let () =
+  let open KB.Syntax in
+  KB.promise Theory.Semantics.slot @@ fun label ->
+  let+ {data; off; size} = label-->?slot in
+  let empty = KB.Value.empty Theory.Semantics.cls in
+  KB.Value.put Theory.Semantics.code empty @@
+  Some (Bigstring.to_string ~pos:off ~len:size data)
+
 let () =
   let open KB.Rule in
   declare ~package:"bap" "addr-of-mem" |>