User-provided space for patches (#138)

This adds a new config-file field for the user to provide us with information about regions in the binary that can be replaced with overflow patch code. It's threaded through to the patcher, which already had support for using that information.

Author: Chris Casinghino

bap-vibes/src/config.ml

@@ -27,6 +27,12 @@ type patch =
     patch_vars : Hvar.t list
   }
 
+(** A type to represent known regions that may be overwritten with patch code *)
+type patch_space = {
+    space_offset : int64;
+    space_size : int64
+  }
+
 (* The configuration for a run of the VIBES pipeline. *)
 type t = {
   exe : string; (* The filename (path) of the executable to patch. *)
@@ -35,6 +41,7 @@ type t = {
   max_tries : int option; (* Optional number of CEGIS iterations to allow *)
   minizinc_model_filepath : string; (* Path to a minizinc model file *)
   ogre : string option;
+  patch_spaces : patch_space list;
   wp_params : Wp_params.t;
 }
 
@@ -52,6 +59,7 @@ let patched_exe_filepath t : string option = t.patched_exe_filepath
 let max_tries t : int option = t.max_tries
 let minizinc_model_filepath t : string = t.minizinc_model_filepath
 let ogre t : string option = t.ogre
+let patch_spaces t : patch_space list = t.patch_spaces
 let wp_params t : Wp_params.t = t.wp_params
 
 (* For displaying a higher var. *)
@@ -94,6 +102,19 @@ let patch_to_string (p : patch) : string =
 let patches_to_string (ps : patch list) : string =
   String.concat ~sep:",\n" (List.map ~f:patch_to_string ps)
 
+(* For displaying a patch space. *)
+let patch_space_to_string (p : patch_space) : string =
+  String.concat ~sep:";\n" [
+      Printf.sprintf "  {";
+      Printf.sprintf "    Space_offset: %s" (Int64.to_string p.space_offset);
+      Printf.sprintf "    Space_size: %s" (Int64.to_string p.space_size);
+      Printf.sprintf "  }";
+    ]
+
+(* For displaying a list of patch spaces *)
+let patch_spaces_to_string (ps : patch_space list) : string =
+  String.concat ~sep:",\n" (List.map ~f:patch_space_to_string ps)
+
 (* For displaying WP params. *)
 let wp_params_to_string (wp_params : Wp_params.t) : string =
   let opt (s : string option) : string =
@@ -109,7 +130,7 @@ let wp_params_to_string (wp_params : Wp_params.t) : string =
   let triple_list (t_list : (string * string * string) list) : string =
     lst @@ List.map t_list ~f:triple
   in
-  let params = [ 
+  let params = [
       Printf.sprintf "func: %s" wp_params.func;
       Printf.sprintf "precond: %s" wp_params.precond;
       Printf.sprintf "postcond: %s" wp_params.postcond;
@@ -118,11 +139,11 @@ let wp_params_to_string (wp_params : Wp_params.t) : string =
       Printf.sprintf "show: %s" (lst wp_params.show);
       Printf.sprintf "use-fun-input-regs: %b" wp_params.use_fun_input_regs;
       Printf.sprintf "fun-specs: %s" (lst wp_params.fun_specs);
-      Printf.sprintf 
+      Printf.sprintf
         "user-fun-specs-orig: %s" (triple_list wp_params.user_func_specs_orig);
       Printf.sprintf
         "user-fun-specs-mod: %s" (triple_list wp_params.user_func_specs_mod);
-    ] 
+    ]
   in
   String.concat ~sep:"\n" params
 
@@ -132,9 +153,13 @@ let pp (ppf : Format.formatter) t : unit =
       Printf.sprintf "Exe: %s" t.exe;
       Printf.sprintf "Patches: %s" (patches_to_string t.patches);
       Printf.sprintf "Output filepath: %s"
-        (Option.value t.patched_exe_filepath ~default:"none provided");
+        (Option.value t.patched_exe_filepath ~default:"<none provided>");
       Printf.sprintf "Max tries: %d" (Option.value t.max_tries ~default:0);
       Printf.sprintf "Minizinc model: %s" t.minizinc_model_filepath;
+      Printf.sprintf "Ogre file: %s"
+        (Option.value t.ogre ~default:"<none provided>");
+      Printf.sprintf "Patch spaces: %s"
+        (patch_spaces_to_string t.patch_spaces);
       Printf.sprintf "WP-params: %s" (wp_params_to_string t.wp_params);
     ] in
   Format.fprintf ppf "@[%s@]@." info
@@ -156,7 +181,8 @@ let create
     ~max_tries:(max_tries : int option)
     ~minizinc_model_filepath:(minizinc_model_filepath : string)
     ~ogre:(ogre : string option)
+    ~patch_spaces:(patch_spaces : patch_space list)
     ~wp_params:(wp_params : Wp_params.t)
   : t =
-  { exe; patches; patched_exe_filepath;
-    max_tries; minizinc_model_filepath; ogre; wp_params }
+  { exe; patches; patched_exe_filepath; max_tries;
+    minizinc_model_filepath; ogre; patch_spaces; wp_params }

bap-vibes/src/config.mli

@@ -15,6 +15,12 @@ type t
 (** A type to represent patch cody which may either be C or literal assembly *)
 type patch_code = CCode of Cabs.definition | ASMCode of string
 
+(** A type to represent known regions that may be overwritten with patch code *)
+type patch_space = {
+    space_offset : int64;
+    space_size : int64
+  }
+
 (** [patch_name p] returns the name of the patch [p]. *)
 val patch_name : patch -> string
 
@@ -53,6 +59,10 @@ val ogre : t -> string option
 (** [wp_params config] returns the input parameters for the invocation to WP *)
 val wp_params : t -> Wp_params.t
 
+(** [patch_spaces config] returns known dead regions suitable for patch
+   placement *)
+val patch_spaces : t -> patch_space list
+
 (** [pp ppf config] is a pretty printer for a configuration record. *)
 val pp : Format.formatter -> t -> unit
 
@@ -79,6 +89,8 @@ val create_patch :
     - [~max_tries] is the optional number of tries to allow
     - [~minizinc_model_filepath] is the minizinc model file location
     - [~ogre] is the optional filepath to an ogre file
+    - [~patch_spaces] is the list of known empty regions for patch code (which
+        may be empty)
     - [~wp_params] is the parameter struct for WP *)
 val create :
   exe:string
@@ -87,5 +99,6 @@ val create :
   -> max_tries : int option
   -> minizinc_model_filepath:string
   -> ogre:string option
+  -> patch_spaces:patch_space list
   -> wp_params:Wp_params.t
   -> t

bap-vibes/src/data.ml

@@ -28,6 +28,11 @@ let int_domain : int option KB.Domain.t = KB.Domain.optional
     ~equal:Int.(=)
     "int-domain"
 
+(* Optional int64 domain *)
+let int64_domain : int64 option KB.Domain.t = KB.Domain.optional
+    ~equal:Int64.(=)
+    "int64-domain"
+
 (* Optional bitvector domain *)
 let bitvec_domain : Bitvec.t option KB.Domain.t = KB.Domain.optional
     ~equal:Bitvec.equal
@@ -246,9 +251,60 @@ end
 (* Sets of patches *)
 module Patch_set = Set.Make (Patch)
 
+(* Properties pertaining to space for patches *)
+module Patch_space = struct
+
+  (* Declare patche spaces as a KB class.  A patch space is a KB object of its
+     own corresponding to a single region of space available for patch code.  We
+     may know of multiple such regions. *)
+  type patch_space_cls
+  let patch_space : (patch_space_cls, unit) KB.cls =
+    KB.Class.declare ~package "patch-space" ()
+
+  (* This provides equality / comparisons for objects of this class *)
+  include (val KB.Object.derive patch_space)
+
+  let offset : (patch_space_cls, int64 option) KB.slot =
+    KB.Class.property ~package patch_space "patch-space-offset" int64_domain
+
+  let size : (patch_space_cls, int64 option) KB.slot =
+    KB.Class.property ~package patch_space "patch-space-size" int64_domain
+
+  let set_offset (obj : t) (data : int64 option) : unit KB.t =
+    KB.provide offset obj data
+
+  let get_offset (obj : t) : int64 option KB.t =
+    KB.collect offset obj
+
+  let get_offset_exn (obj : t) : int64 KB.t =
+    get_offset obj >>= fun result ->
+    match result with
+    | None -> Kb_error.fail Kb_error.Missing_patch_space_offset
+    | Some value -> KB.return value
+
+  let set_size (obj : t) (data : int64 option) : unit KB.t =
+    KB.provide size obj data
+
+  let get_size (obj : t) : int64 option KB.t =
+    KB.collect size obj
+
+  let get_size_exn (obj : t) : int64 KB.t =
+    get_size obj >>= fun result ->
+    match result with
+    | None -> Kb_error.fail Kb_error.Missing_patch_space_size
+    | Some value -> KB.return value
+end
+
+(* Sets of patch spaces *)
+module Patch_space_set = Set.Make (Patch_space)
+
 (* Properties pertaining to the original executable *)
 module Original_exe = struct
 
+  let patch_spaces_domain : Patch_space_set.t KB.domain =
+    KB.Domain.flat ~empty:Patch_space_set.empty ~equal:Patch_space_set.equal
+      "patch-spaces"
+
   let filepath : (cls, string option) KB.slot =
     KB.Class.property ~package cls "original-exe-filepath"
       string_domain
@@ -257,6 +313,10 @@ module Original_exe = struct
     KB.Class.property ~package cls "original-exe-target"
       Theory.Target.domain
 
+  let patch_spaces : (cls, Patch_space_set.t) KB.slot =
+    KB.Class.property ~package cls "original-exe-patch-spaces"
+      patch_spaces_domain
+
   let set_filepath (obj : t) (data : string option) : unit KB.t =
     KB.provide filepath obj data
 
@@ -282,6 +342,12 @@ module Original_exe = struct
     else
       KB.return tgt
 
+  let set_patch_spaces (obj : t) (data : Patch_space_set.t) : unit KB.t =
+    KB.provide patch_spaces obj data
+
+  let get_patch_spaces (obj : t) : Patch_space_set.t KB.t =
+    KB.collect patch_spaces obj
+
 end
 
 (* Properties pertaining to the patched executable *)

bap-vibes/src/data.mli

@@ -11,6 +11,7 @@ module Hvar = Higher_var
 (** We define "domains" for the types used in our properties. *)
 val string_domain    : string option KB.Domain.t
 val int_domain       : int option KB.Domain.t
+val int64_domain     : int64 option KB.Domain.t
 val bitvec_domain    : Bitvec.t option KB.Domain.t
 val sexp_domain      : Sexp.t option KB.Domain.t
 val source_domain    : Cabs.definition option KB.Domain.t
@@ -113,10 +114,40 @@ end
 (** Sets of patches *)
 module Patch_set : Set.S with type Elt.t = Patch.t
 
+(** The Patch_space module defines an additional class holding all properties
+   related to regions in the original binary that can be used for the patch
+   (e.g., dead code).  *)
+module Patch_space : sig
+
+  (* The KB infrastructure *)
+  type patch_space_cls
+  type t = patch_space_cls KB.obj
+  val patch_space : (patch_space_cls, unit) KB.cls
+
+  (* equal, compare, and other things for patch spaces *)
+  include Knowledge.Object.S with type t := t
+
+  val offset : (patch_space_cls, int64 option) KB.slot
+  val size : (patch_space_cls, int64 option) KB.slot
+
+  val set_offset : t -> int64 option -> unit KB.t
+  val get_offset : t -> int64 option KB.t
+  val get_offset_exn : t -> int64 KB.t
+
+  val set_size : t -> int64 option -> unit KB.t
+  val get_size : t -> int64 option KB.t
+  val get_size_exn : t -> int64 KB.t
+end
+
+(** Sets of patch spaces *)
+
+module Patch_space_set : Set.S with type Elt.t = Patch_space.t
+
 (** Properties pertaining to the original executable *)
 module Original_exe : sig
   val filepath : (cls, string option) KB.slot
   val target : (cls, Theory.target) KB.slot
+  val patch_spaces : (cls, Patch_space_set.t) KB.slot
 
   val set_filepath : t -> string option -> unit KB.t
   val get_filepath : t -> string option KB.t
@@ -128,6 +159,9 @@ module Original_exe : sig
   (** Raises if the target is empty *)
   val get_target_exn : t -> Theory.target KB.t
 
+  val set_patch_spaces : t -> Patch_space_set.t -> unit KB.t
+  val get_patch_spaces : t -> Patch_space_set.t KB.t
+
 end
 
 (** Properties pertaining to the patched executable *)

bap-vibes/src/kb_error.ml

@@ -20,6 +20,8 @@ type t =
   | Missing_patch_size
   | Missing_lower_patch_code
   | Missing_patch_vars
+  | Missing_patch_space_offset
+  | Missing_patch_space_size
   | Missing_func
   | Missing_property
   | Missing_raw_ir
@@ -57,6 +59,8 @@ let pp ppf (e : t) =
     | Missing_patch_size -> "No patch size was stashed in KB"
     | Missing_lower_patch_code -> "No lower patch code was stashed in KB"
     | Missing_patch_vars -> "No patch vars were stashed in KB"
+    | Missing_patch_space_offset -> "No patch space offset was stashed in KB"
+    | Missing_patch_space_size -> "No patch space size was stashed in KB"
     | Missing_func -> "No function name to verify was stashed in KB"
     | Missing_property -> "No correctness property was stashed in KB"
     | Missing_raw_ir -> "Raw Ir compiled from core_theory not found in KB"

bap-vibes/src/kb_error.mli

@@ -22,6 +22,8 @@ type t =
   | Missing_patch_size
   | Missing_lower_patch_code
   | Missing_patch_vars
+  | Missing_patch_space_offset
+  | Missing_patch_space_size
   | Missing_func
   | Missing_property
   | Missing_raw_ir

bap-vibes/src/patcher.ml

@@ -351,6 +351,26 @@ let reify_patch
               orig_loc = patch_file_offset;
               orig_size = Int64.of_int patch_size}
 
+(* Turn a KB patch space into a patch site (the type used by this module to
+   represent the same information *)
+let reify_patch_site (obj : Data.Patch_space.t) : patch_site KB.t =
+  let open KB.Let in
+  let* location = Data.Patch_space.get_offset_exn obj in
+  let* size = Data.Patch_space.get_size_exn obj in
+  KB.return {location; size}
+
+(* Get the patch_spaces out of the kb monad and into the form used by this
+   module *)
+let reify_patch_sites (obj : Data.t) : patch_site list KB.t =
+  let open KB.Let in
+  let* patch_space_set : Data.Patch_space_set.t =
+    Data.Original_exe.get_patch_spaces obj
+  in
+  let patch_spaces : Data.Patch_space.t list =
+    Data.Patch_space_set.to_list patch_space_set
+  in
+  KB.List.map ~f:reify_patch_site patch_spaces
+
 (* Patches the original exe, to produce a patched exe. *)
 let patch
     ?compute_region:(compute_region=ogre_compute_region)
@@ -369,7 +389,9 @@ let patch
   let reify_patch = reify_patch
     ~compute_region:compute_region ~exe_unit:original_exe_unit in
   let* patch_list = KB.List.map ~f:reify_patch patch_list in
-  let patch_sites = naive_find_patch_sites original_exe_filename in
+  let naive_patch_sites = naive_find_patch_sites original_exe_filename in
+  let* provided_patch_sites = reify_patch_sites obj in
+  let patch_sites = naive_patch_sites @ provided_patch_sites in
   let* lang =
     let patch = Data.Patch_set.choose_exn patches in
     Data.Patch.get_lang patch