tweaks symbolization and function start identification facilities (#1355)

We remove the dependency on the Bap.Std.Image and instead use the
image specification directly. These gives us strictly more symbols,
as image imposes extra constraints, which my hide functions starts
and their names.

More information is not always better, as we now have more chances to
get the conflicting knowledge. To ensure that we're able to preserve
as much information as possible without compromising correctness we
leverage our agent-based conflict resolution system. We push all names
in which we're not completely sure into possible aliases and use a new
agent, `bap:gossiper` to propse names from that set.

To make everything work fine, we pushed down the reliability of the
objdump symbolizer (as we want bap to have the final word).

The improved symbolization facility uncovered a small bug in the way
how the x86 lock intrinsic was implemented, it was named just
`"lock"`, which obviously may conflict with a normal function with the
same name (which was uncovered by our testsuite). This commit adds
the `x86` prefix to the intrinsic, e.g., `x86:lock` as well as
properly delimits the locked code with the corresponding `x86:unlock`
intrinsic.

Author: ivg

lib/bap/bap_project.ml

@@ -39,6 +39,182 @@ let memory_slot = KB.Class.property Theory.Unit.cls "unit-memory"
     ~desc:"annotated memory regions of the unit"
     Memmap.domain
 
+module Symbols = struct
+  open KB.Let
+  open KB.Syntax
+
+  module Addr = struct
+    include Bitvec
+    include Bitvec_order
+    include Bitvec_binprot.Functions
+    include Bitvec_sexp.Functions
+  end
+
+  type table = {
+    roots : Set.M(Addr).t;
+    names : string Map.M(Addr).t;
+    aliases : Set.M(String).t Map.M(Addr).t;
+  } [@@deriving compare, equal, bin_io, sexp]
+
+  let empty = {
+    roots = Set.empty (module Addr);
+    names = Map.empty (module Addr);
+    aliases = Map.empty (module Addr);
+  }
+
+  let slot = KB.Class.property Theory.Unit.cls
+      ~package:"bap" "symbol-table"
+      ~persistent:(KB.Persistent.of_binable (module struct
+                     type t = table [@@deriving bin_io]
+                   end)) @@
+    KB.Domain.flat ~empty ~equal:equal_table "symbols"
+
+  let is_ident s =
+    String.length s > 0 &&
+    (Char.is_alpha s.[0] || Char.equal s.[0] '_') &&
+    String.for_all s ~f:(fun c -> Char.is_alphanum c ||
+                                  Char.equal c '_')
+
+  let from_spec t =
+    let collect fld = Ogre.collect Ogre.Query.(select @@ from fld) in
+    let open Ogre.Let in
+    let to_addr =
+      let m = Bitvec.modulus (Theory.Target.code_addr_size t) in
+      let n = Theory.Target.code_alignment t / Theory.Target.byte t in
+      let mask = Int64.(lnot (of_int n - 1L)) in
+      fun x ->
+        let x = Int64.(x land mask) in
+        Bitvec.(int64 x mod m) in
+    let add_alias aliases addr alias = Map.update aliases addr ~f:(function
+        | None -> Set.singleton (module String) alias
+        | Some names -> Set.add names alias) in
+    let pp_comma ppf () = Format.pp_print_string ppf ", " in
+    let pp_addrs =
+      Format.pp_print_list ~pp_sep:pp_comma Bitvec.pp
+    and pp_names =
+      Format.pp_print_list ~pp_sep:pp_comma Format.pp_print_string in
+    let* roots =
+      let+ roots =
+        let* starts = collect Image.Scheme.code_start in
+        let* values = collect Image.Scheme.symbol_value in
+        let+ entry = Ogre.request Image.Scheme.entry_point in
+        let roots = Seq.append starts (Seq.map ~f:fst values) in
+        match entry with
+        | None -> roots
+        | Some entry -> Seq.cons entry roots in
+      Seq.fold roots ~init:(Set.empty (module Bitvec_order))
+        ~f:(fun xs x -> Set.add xs (to_addr x)) in
+    let+ named_symbols = collect Image.Scheme.named_symbol in
+    let init = Bap_relation.empty Bitvec.compare String.compare in
+    Seq.fold named_symbols ~init ~f:(fun rel (data,name) ->
+        let addr = to_addr data in
+        if Set.mem roots addr && is_ident name
+        then Bap_relation.add rel (to_addr data) name
+        else rel) |> fun rel ->
+    Bap_relation.matching rel {empty with roots}
+      ~saturated:(fun k v t -> {
+            t with names = Map.add_exn t.names k v
+          })
+      ~unmatched:(fun reason t -> {
+            t with aliases = match reason with
+          | Non_injective_fwd (addrs,name) ->
+            info "the symbol %s has ambiguous addresses: %a@\n"
+              name pp_addrs addrs;
+            List.fold addrs ~init:t.aliases ~f:(fun aliases addr ->
+                add_alias aliases addr name)
+          | Non_injective_bwd (names,addr) ->
+            info "the symbol at %a has ambiguous names: %a@\n"
+              Bitvec.pp addr pp_names names;
+            List.fold names ~init:t.aliases ~f:(fun aliases name ->
+                add_alias aliases addr name)
+          })
+
+  let build_table t spec = match Ogre.eval (from_spec t) spec with
+    | Ok x -> x
+    | Error err ->
+      invalid_argf "Malformed ogre specification: %s"
+        (Error.to_string_hum err) ()
+
+  let collect_inputs from obj f =
+    KB.collect Theory.Label.unit obj >>=? fun unit ->
+    KB.collect Theory.Label.addr obj >>=? fun addr ->
+    let+ data = KB.collect from unit in
+    f data addr
+
+  let promised_table : unit =
+    KB.promise slot @@ fun unit ->
+    let* t = KB.collect Theory.Unit.target unit in
+    let+ s = KB.collect Image.Spec.slot unit in
+    build_table t s
+
+  let promised_roots : unit =
+    KB.Rule.(begin
+        declare "provides roots" |>
+        require Image.Spec.slot |>
+        provide Theory.Label.is_subroutine |>
+        comment "computes roots from spec";
+      end);
+    KB.promise Theory.Label.is_subroutine @@ fun obj ->
+    collect_inputs slot obj @@ fun {roots} addr ->
+    Option.some_if (Set.mem roots addr) true
+
+
+  let names_agent = KB.Agent.register
+      ~package:"bap" "specification-provider"
+      ~desc:"provides names obtained from the image specification."
+
+  let promised_names : unit =
+    KB.Rule.(begin
+        declare "provides names" |>
+        require Image.Spec.slot |>
+        provide Theory.Label.possible_name |>
+        comment "computes symbol names from spec";
+      end);
+    KB.propose names_agent Theory.Label.possible_name @@ fun obj ->
+    collect_inputs slot obj @@ fun {names} addr ->
+    Map.find names addr
+
+
+  let promised_aliases : unit =
+    KB.Rule.(begin
+        declare "provides aliases" |>
+        require Image.Spec.slot |>
+        provide Theory.Label.possible_name |>
+        comment "computes symbol aliases (names) from spec";
+      end);
+    KB.promise Theory.Label.aliases @@ fun obj ->
+    let* unit = KB.collect Theory.Label.unit obj in
+    let* addr = KB.collect Theory.Label.addr obj in
+    match unit,addr with
+    | None,_|_,None -> KB.return (Set.empty (module String))
+    | Some unit, Some addr ->
+      let+ {aliases} = KB.collect slot unit in
+      match Map.find aliases addr with
+      | None -> Set.empty (module String)
+      | Some aliases -> aliases
+
+  let gossiper = KB.Agent.register
+      ~package:"bap" "symbols-gossiper"
+      ~desc:"propses an alias as a possible name"
+      ~reliability:KB.Agent.unreliable
+
+  let gossiped_aliases : unit =
+    KB.Rule.(begin
+        declare "provides aliases as names" |>
+        require Image.Spec.slot |>
+        provide Theory.Label.possible_name |>
+        comment "uses aliases as an unreliable source of symbol names";
+      end);
+    KB.propose gossiper Theory.Label.possible_name @@ fun obj ->
+    let+ aliases = KB.collect Theory.Label.aliases obj in
+    match Set.find aliases ~f:is_ident with
+    | None -> Set.max_elt aliases
+    | ident -> ident
+end
+
+
+
+
 let with_filename spec target _code memory path f =
   let open KB.Syntax in
   let width = Theory.Target.code_addr_size target in
@@ -237,27 +413,11 @@ module Input = struct
     target = compute_target ?target (Image.spec img);
   }
 
-  let symtab_agent =
-    let reliability = KB.Agent.authorative in
-    KB.Agent.register "symtab"
-      ~reliability
-      ~desc:"extracts symbols from symbol tables"
-      ~package:"bap"
-
-  let provide_image file image =
-    let image_symbols = Symbolizer.(set_path (of_image image) file) in
-    let image_roots = Rooter.(set_path (of_image image) file) in
-    info "providing rooter and symbolizer from image of %a"
-      Sexp.pp_hum ([%sexp_of : string option] (Image.filename image));
-    Symbolizer.provide symtab_agent image_symbols;
-    Rooter.provide image_roots
-
   let of_image ?target ?loader filename =
     Image.create ?backend:loader filename >>| fun (img,warns) ->
     List.iter warns ~f:(fun e -> warning "%a" Error.pp e);
     let spec = Image.spec img in
     Signal.send Info.got_img img;
-    provide_image filename img;
     let finish proj = {
       proj with
       storage = Dict.set proj.storage Image.specification spec;

lib/bap_relation/bap_relation.mli

@@ -6,7 +6,7 @@
     sets and computes their matching that defines bijections between
     the sets.
 
-    {2 Format Definition and Notation}
+    {2 Formal Definition and Notation}
 
     Given two sets [K] and [S], with meta-variables [x,y,z] ranging
     over [K] and meta-variables [r,s,t] ranging over [S] we will
@@ -77,7 +77,7 @@ val iter : ('k,'s) t -> f:('k -> 's -> unit) -> unit
       [Non_injective_bwd ([r;s],x);
 *)
 
-(** the reason why was the pair left unmatched  *)
+(** the reason why the pair was left unmatched  *)
 type ('k,'s) non_injective =
   | Non_injective_fwd of 'k list * 's (** Non-injective forward mapping.  *)
   | Non_injective_bwd of 's list * 'k (** Non-injective backward mapping.  *)

lib/bap_types/bap_stmt.ml

@@ -80,6 +80,11 @@ module Special = struct
 
   let pp_default ppf s = fprintf ppf "special@ @[<1>(%s)@]" s
 
+  let pp_cons ppf s =
+    pp_print_string ppf @@ match String.chop_prefix s ~prefix:"bap:" with
+    | None ->  s
+    | Some s -> s
+
   let pp ppf s = match String.chop_prefix ~prefix s with
     | None -> pp_default ppf s
     | Some data -> match Sexp.of_string data with
@@ -88,7 +93,7 @@ module Special = struct
         let pp_vals ppf xs = pp_print_list
             ~pp_sep:(fun ppf () -> pp_print_string ppf ", ")
             Sexp.pp_hum ppf xs in
-        fprintf ppf "%s(@[<hv2>%a@])" cons pp_vals vals
+        fprintf ppf "%a(@[<hv2>%a@])" pp_cons cons pp_vals vals
       | _ -> pp_default ppf s
 end
 

oasis/bap-std

@@ -17,12 +17,16 @@ Library bap
                    cmdliner,
                    bap-knowledge,
                    bap-core-theory,
+                   bap-relation,
                    graphlib,
                    regular,
                    core_kernel,
                    ppx_bap,
                    monads,
                    bitvec,
+                   bitvec-binprot,
+                   bitvec-order,
+                   bitvec-sexp,
                    ogre,
                    fileutils,
                    core_kernel.caml_unix

plugins/objdump/objdump_main.ml

@@ -101,6 +101,7 @@ let with_objdump_output demangler ~file ~f ~init =
 let agent =
   KB.Agent.register ~package:"bap" "objdump-symbolizer"
     ~desc:"extracts symbols objdump"
+    ~reliability:KB.Agent.doubtful
 
 module Repository : sig
   type t

plugins/relocatable/rel_symbolizer.ml

@@ -125,6 +125,7 @@ end
 let plt_agent = Knowledge.Agent.register
     ~package:"bap" "plt-symbolizer"
     ~desc:"extracts symbols from external relocations"
+    ~reliability:Knowledge.Agent.reliable
 
 open KB.Syntax
 

plugins/x86/x86_tools_prefix.ml

@@ -5,7 +5,10 @@ open X86_tools_types
 module Make (RR : RR) (FR : FR) (IV : IV) : PR = struct
   type t = X86_prefix.t [@@deriving sexp, compare]
 
-  let lock bil = Bil.(encode intrinsic "lock") :: bil
+  let lock bil =
+    Bil.(encode intrinsic "x86:lock") :: bil @ [
+      Bil.(encode intrinsic "x86:unlock")
+    ]
 
   module Rep = struct
     let rcx =