allows target overriding (#1515)

BinaryAnalysisPlatform · Jun 29, 2022 · f07b270 · f07b270
1 parent 6ef5e3d
commit f07b270
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 18 deletions.
diff --git a/lib/bap/bap.mli b/lib/bap/bap.mli
@@ -10524,10 +10524,17 @@ module Std : sig
           and the information from the is merged, otherwise only the
           selected loaded is used. See {!Image.available_backend}.
 
-          The [target] could be used to specialize the target
-          information retrieved from the file. If it is less specific,
-          then it will be ignored, if it contradicts the information
-          in the file then the project creation will fail.
+          The [target] could be used to override the target
+          information derived from the input file.
+
+          @since 2.5.0 if [target] is specified then it is used
+          instead of the derived target, and the derivation itself is
+          not performed.
+
+          @before 2.5.0 if [target] is specified and is less specific,
+          then the derived target it will be ignored, if it
+          contradicts the information in the file then the project
+          creation will fail.
 
           @since 2.2.0 *)
       val load : ?target:Theory.Target.t -> ?loader:string -> string -> t

diff --git a/lib/bap/bap_project.ml b/lib/bap/bap_project.ml
@@ -227,15 +227,10 @@ module Input = struct
     | None -> false
     | Some s -> not (Image.Segment.is_executable s)
 
-  let compute_target ?file ?(target=Theory.Target.unknown) spec =
-    let target' = State.Toplevel.compute_target ?file spec in
-    match (Theory.Target.order target target' : KB.Order.partial) with
-    | LT | EQ -> target'
-    | GT -> target
-    | NC -> invalid_argf "the derived target %s is incompatible \
-                          with the user-specified target %s."
-              (Theory.Target.to_string target')
-              (Theory.Target.to_string target) ()
+  let compute_target ?file ?target spec =
+    match target with
+    | Some t when not (Theory.Target.is_unknown t) -> t
+    | _ -> State.Toplevel.compute_target ?file spec
 
   let result_of_image ?target finish file img = {
     arch = Image.arch img;

diff --git a/plugins/disassemble/disassemble_main.ml b/plugins/disassemble/disassemble_main.ml
@@ -376,7 +376,10 @@ let loader =
 let target =
   let t = Extension.Type.define Theory.Target.unknown
       ~name:"NAME"
-      ~digest:(fun t -> Caml.Digest.string@@Theory.Target.to_string t)
+      ~digest:(fun t ->
+          let r = Caml.Digest.string@@Theory.Target.to_string t in
+          Format.eprintf "target digest = %s@\n" (Caml.Digest.to_hex r);
+          r)
       ~parse:(fun s -> match Theory.Target.lookup ~package:"bap" s with
           | Some t -> t
           | None ->
@@ -385,10 +388,8 @@ let target =
                           of targets" s ())
       ~print:Theory.Target.to_string in
   Extension.Command.parameter t "target"
-    ~doc:"Refines the target architecture of the binary. \
-          See `bap list targets` for the full hierarchy of targets. \
-          The specified target must be a refinement of the actual \
-          target stored in the binary, otherwise an error is signaled."
+    ~doc:"Sets the target architecture of the binary. \
+          See `bap list targets` for the full hierarchy of targets."
 
 let validate_input file =
   Result.ok_if_true (Sys.file_exists file)
@@ -494,6 +495,7 @@ let create_and_process input outputs passes loader target update
   let digest = make_digest [
       Extension.Configuration.digest ctxt;
       Caml.Digest.file input;
+      Theory.Target.to_string target;
       if uses_file_loader then Caml.Digest.file loader else loader;
     ] in
   let had_knowledge = load_knowledge print_missing digest kb in