Adds insn-code to the Theory.Semantics class

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
 

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

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
 

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" |>