adds is-executable and format attributes and fixes glibc rt check (#1198)

We are not using is-executable for the glibc runtime check though,
as we have a more precise check now - we can look for the name
reference of __libc_start_main and if it is there insert it.

fixes #1130

Author: ivg

lib/bap/bap.mli

@@ -5606,12 +5606,26 @@ module Std : sig
       val bits : (size, (size -> 'a) -> 'a) Ogre.attribute
 
 
-      (** [is_little_endian yes-or-no] is [true] if the target is
-          little endian.
+      (** [(format X)] defines the file format to be X.
+
+          Currently supported formats:
+          - ["elf"];
+          - ["macho"];
+          - ["coff"]
+      *)
+      val format : (string, (string -> 'a) -> 'a) Ogre.attribute
+
+
+      (** (is-little-endian FLAG)] is set for files with words encoded in the
+          little-endian order.
 
           @since 2.2.0  *)
       val is_little_endian : (bool, (bool -> 'a) -> 'a) Ogre.attribute
 
+      (** [(is-executable FLAG)] is set for binaries that executable.
+
+          @since 2.2.0 *)
+      val is_executable : (bool, (bool -> 'a) -> 'a) Ogre.attribute
 
       (** [bias offset] the value by which all addresses are biased
           wrt to the real addresses in the binary.
@@ -9342,6 +9356,12 @@ module Std : sig
     (** [arch project] reveals the architecture of a loaded file  *)
     val arch : t -> arch
 
+
+    (** [specification p] returns the specification of the binary.
+
+        @since 2.2.0*)
+    val specification : t -> Ogre.doc
+
     val state : t -> state
 
 

lib/bap/bap_project.ml

@@ -79,6 +79,7 @@ module Spec = struct
     let statements = Ogre.all [
         Ogre.provide Field.arch (Arch.to_string arch);
         Ogre.provide Field.bits bits;
+        Ogre.provide Field.format "raw";
         Ogre.provide Field.is_little_endian @@
         match Arch.endian arch with
         | LittleEndian -> true
@@ -168,6 +169,7 @@ type state = State.t [@@deriving bin_io]
 
 type t = {
   arch    : arch;
+  spec    : Ogre.doc;
   core    : State.t;
   disasm  : disasm;
   memory  : value memmap;
@@ -370,6 +372,7 @@ let create
     let cfg,symbols,core = State.Toplevel.run spec arch ~code ~data file state in
     Result.return @@ finish {
       core;
+      spec;
       disasm = Disasm.create cfg;
       program = Program.lift symbols;
       symbols;
@@ -386,6 +389,8 @@ let create
     Error (to_info msg)
   | exn -> Or_error.of_exn ~backtrace:`Get exn
 
+let specification = spec
+
 let restore_state _ =
   failwith "Project.restore_state: this function should no be used.
     Please use the Toplevel module to save/restore the state."

lib/bap/bap_project.mli

@@ -30,6 +30,7 @@ val create :
   input -> t Or_error.t
 
 val arch : t -> arch
+val specification : t -> Ogre.doc
 val program : t -> program term
 val with_program : t -> program term -> t
 val symbols : t -> symtab

lib/bap_core_theory/bap_core_theory.mli

@@ -1160,6 +1160,13 @@ module Theory : sig
     val path : (cls, string option) KB.slot
 
 
+    (** [format] the file format of the unit, e.g., ["elf"].*)
+    val format : (cls, string option) KB.slot
+
+    (** [is-executed] is true if the unit is an executable file ready
+        to be executed by the operating system. *)
+    val is_executable : (cls, bool option) KB.slot
+
     (** [bias] is the bias of all addresses in the unit.
 
         If a unit is biased, then all addresses in this unit have

lib/bap_core_theory/bap_core_theory_program.ml

@@ -26,6 +26,10 @@ let path = Knowledge.Domain.optional "path"
     ~equal:String.equal
     ~inspect:sexp_of_string
 
+let format = Knowledge.Domain.optional "path"
+    ~equal:String.equal
+    ~inspect:sexp_of_string
+
 let names = Knowledge.Domain.powerset (module String) "names"
     ~inspect:sexp_of_string
 
@@ -52,7 +56,20 @@ module Unit = struct
       ~desc:"a unit of code"
 
   let path = string_property ~domain:path cls "unit-path"
-      ~desc:"a filesytem name of the file that contains the program"
+      ~desc:"a filesystem name of the file that contains the program"
+
+  let format = string_property ~domain:format cls "unit-format"
+      ~desc:"the file format that used to encode the unit"
+
+  let is_executable =
+    Knowledge.Class.property ~package cls "unit-is-executable"
+      Knowledge.Domain.bool
+      ~persistent:(Knowledge.Persistent.of_binable (module struct
+                     type t = bool option [@@deriving bin_io]
+                   end))
+      ~public:true
+      ~desc:"whether the unit is ready to be executed by the OS"
+
 
   let bias = Knowledge.Class.property ~package cls "unit-bias" word
       ~persistent:(Knowledge.Persistent.of_binable (module struct

lib/bap_core_theory/bap_core_theory_program.mli

@@ -30,6 +30,8 @@ module Unit : sig
   val for_region : lower:Bitvec.t -> upper:Bitvec.t -> t knowledge
 
   val path : (cls, string option) slot
+  val format : (cls, string option) slot
+  val is_executable : (cls, bool option) slot
   val bias : (cls, Bitvec.t option) slot
 
   module Target : sig

lib/bap_image/bap_image.ml

@@ -356,9 +356,11 @@ module Scheme = struct
   let subarch    () = declare "subarch" (scheme name) ident
   let vendor    () = declare "vendor" (scheme name) ident
   let system    () = declare "system" (scheme name) ident
+  let format    () = declare "format" (scheme name) ident
   let abi    () = declare "abi" (scheme name) ident
   let bits    () = declare "bits" (scheme size) ident
-  let is_little_endian () = declare "is_little_endian" (scheme flag) ident
+  let is_little_endian () = declare "is-little-endian" (scheme flag) ident
+  let is_executable () = declare "is-executable" (scheme flag) ident
   let bias    () = declare "bias" (scheme off) ident
   let section () = declare "section" (location ()) void_region
   let code_start   () = declare "code-start" (scheme addr) ident

lib/bap_image/bap_image.mli

@@ -97,11 +97,13 @@ module Scheme : sig
 
   val arch : (string, (string -> 'a) -> 'a) Ogre.attribute
   val subarch : (string, (string -> 'a) -> 'a) Ogre.attribute
+  val format : (string, (string -> 'a) -> 'a)  Ogre.attribute
   val vendor : (string, (string -> 'a) -> 'a) Ogre.attribute
   val system : (string, (string -> 'a) -> 'a) Ogre.attribute
   val abi : (string, (string -> 'a) -> 'a) Ogre.attribute
   val bits : (size, (size -> 'a) -> 'a) Ogre.attribute
   val is_little_endian : (bool, (bool -> 'a) -> 'a) Ogre.attribute
+  val is_executable : (bool, (bool -> 'a) -> 'a) Ogre.attribute
 
   val bias : (off, (off -> 'a) -> 'a) Ogre.attribute
   val segment : ((bool * bool * bool) region,

lib/bap_llvm/bap_llvm_loader.ml

@@ -32,9 +32,6 @@ module LLVM = struct
 
   let at = "at" %: int
 
-  let file_type () =
-    Ogre.declare ~name:"llvm:file-type" (scheme name) ident
-
   (** entry point  *)
   let entry_point () =
     Ogre.declare ~name:"llvm:entry-point" (scheme addr) ident
@@ -293,7 +290,7 @@ let provide_coff_segmentation = [
 ]
 
 let overload file_type info =
-  Ogre.require LLVM.file_type >>= fun file ->
+  Ogre.require format >>= fun file ->
   Ogre.sequence @@
   provide_if (String.equal file file_type) info
 

lib/bap_llvm/llvm_coff_loader.hpp

@@ -57,13 +57,51 @@ void emit_base_address(const coff_obj &obj, ogre_doc &s) {
     s.entry("llvm:base-address") << obj.getImageBase();
 }
 
+#if LLVM_VERSION_MAJOR >= 10
+
+error_or<pe32_header> get_pe32_header(const COFFObjectFile &obj) {
+    const pe32_header *hdr = obj.getPE32Header();
+    if (!hdr) { return failure("PE header not found"); }
+    else return success(*hdr);
+}
+
+error_or<pe32plus_header> get_pe32plus_header(const COFFObjectFile &obj) {
+    const pe32plus_header *hdr = obj.getPE32PlusHeader();
+    if (!hdr) { return failure("PE+ header not found"); }
+    else return success(*hdr);
+}
+
+#else
+
+error_or<pe32_header> get_pe32_header(const COFFObjectFile &obj) {
+    const pe32_header *hdr = 0;
+    auto ec = obj.getPE32Header(hdr);
+    if (ec) return failure(ec.message());
+    else if (!hdr) { return failure("PE header not found"); }
+    else return success(*hdr);
+}
+
+error_or<pe32plus_header> get_pe32plus_header(const COFFObjectFile &obj) {
+    const pe32plus_header *hdr = 0;
+    auto ec = obj.getPE32PlusHeader(hdr);
+    if (ec) return failure(ec.message());
+    else if (!hdr) { return failure("PE+ header not found"); }
+    else return success(*hdr);
+}
+#endif
+
+bool is_executable(const COFFObjectFile &obj) {
+    return obj.getCharacteristics() & COFF::IMAGE_FILE_EXECUTABLE_IMAGE;
+}
+
+
 void emit_entry_point(const coff_obj &obj, ogre_doc &s) {
     auto entry = 0L;
     if (obj.getBytesInAddress() == 4) {
-        if (auto hdr = prim::get_pe32_header(obj))
+        if (auto hdr = get_pe32_header(obj))
             entry = hdr->AddressOfEntryPoint;
     } else {
-        if (auto hdr = prim::get_pe32plus_header(obj))
+        if (auto hdr = get_pe32plus_header(obj))
             entry = hdr->AddressOfEntryPoint;
     }
     s.entry("llvm:entry-point") << entry + obj.getImageBase();
@@ -268,7 +306,8 @@ error_or<uint64_t> symbol_file_offset(const coff_obj &obj, const SymbolRef &sym)
 
 error_or<std::string> load(ogre_doc &s, const llvm::object::COFFObjectFile &obj, const char* pdb_path) {
     using namespace coff_loader;
-    s.raw_entry("(llvm:file-type coff)");
+    s.raw_entry("(format coff)");
+    s.entry("is-executable") << is_executable(obj);
     emit_base_address(obj, s);
     emit_entry_point(obj, s);
     emit_sections(obj, s);