Pzucker/gdb

wp/lib/bap_wp/src/output.ml

@@ -0,0 +1,126 @@
+(***************************************************************************)
+(*                                                                         *)
+(*  Copyright (C) 2018/2019 The Charles Stark Draper Laboratory, Inc.      *)
+(*                                                                         *)
+(*  This file is provided under the license found in the LICENSE file in   *)
+(*  the top-level directory of this project.                               *)
+(*                                                                         *)
+(*  This work is funded in part by ONR/NAWC Contract N6833518C0107.  Its   *)
+(*  content does not necessarily reflect the position or policy of the US  *)
+(*  Government and no official endorsement should be inferred.             *)
+(*                                                                         *)
+(***************************************************************************)
+
+open !Core_kernel
+open Bap.Std
+
+include Self()
+
+module Expr = Z3.Expr
+module Arith = Z3.Arithmetic
+module BV = Z3.BitVector
+module Bool = Z3.Boolean
+module Array = Z3.Z3Array
+module Env = Environment
+module Constr = Constraint
+
+
+(** Implements {!Model}. *)
+
+open Core_kernel
+open Bap.Std
+
+type sign = Unsigned | Signed
+
+let string_of_sign s =
+  match s with
+  | Unsigned -> "u"
+  | Signed -> "s"
+
+exception NoValue of string
+
+let no_value_msg e m =
+  let e_str = Z3.Expr.to_string e in
+  let m_str = Z3.Model.to_string m in
+  Printf.sprintf "No value for symbol '%s' found in model: %s" e_str m_str
+
+let word_of_str s w sign =
+  let w_str = Printf.sprintf "%s:%d%s" s w (string_of_sign sign) in
+  Word.of_string w_str
+
+let z3_val_of e m =
+  match Z3.Model.eval m e true with
+  | Some v -> v
+  | None -> raise (NoValue (no_value_msg e m))
+
+let word_of_z3_bv bv =
+  let bits = Z3.BitVector.get_size (Z3.Expr.get_sort bv) in
+  let sign = Unsigned in
+  let s = Z3.Expr.to_string bv in
+  word_of_str (String.substr_replace_first s ~pattern:"#" ~with_:"0") bits sign
+
+let val_for_reg r m env =
+  let reg_var = Var.create r (Type.imm 64) in
+  let reg_value, _ = Environment.get_var env reg_var in
+  let v = z3_val_of reg_value m in
+  word_of_z3_bv v
+
+let strip_final_digits s =
+  let s' = List.rev (String.to_list s) in
+  let rec pop_digits l =
+    match l with
+    | [] -> l
+    | x :: xs ->
+      begin
+        match x with
+        | '0' .. '9' -> pop_digits xs
+        | _ -> l
+      end
+    in 
+  let s'' = List.rev (pop_digits s') in
+  String.of_char_list s''
+
+let reg_names m =
+  m |>
+  Z3.Model.get_decls |>
+  List.map ~f:Z3.FuncDecl.get_name |>
+  List.map ~f:Z3.Symbol.to_string |>
+  List.filter ~f:(fun s -> String.is_substring_at s 0 "R") |>
+  List.map ~f:strip_final_digits
+
+
+let print_result (solver : Z3.Solver.solver) (status : Z3.Solver.status)
+    (goals: Constr.t) (ctx : Z3.context) : unit =
+  match status with
+  | Z3.Solver.UNSATISFIABLE -> Format.printf "\nUNSAT!\n%!"
+  | Z3.Solver.UNKNOWN -> Format.printf "\nUNKNOWN!\n%!"
+  | Z3.Solver.SATISFIABLE ->
+    Format.printf "\nSAT!\n%!";
+    let model = Z3.Solver.get_model solver
+                |> Option.value_exn ?here:None ?error:None ?message:None in
+    Format.printf "\nModel:\n%s\n%!" (Z3.Model.to_string model);
+    let refuted_goals = Constr.get_refuted_goals goals solver ctx in
+    Format.printf "\nRefuted goals:\n%!";
+    Seq.iter refuted_goals ~f:(fun g ->
+        Format.printf "%s\n%!" (Constr.refuted_goal_to_string g model))
+
+(** [output_gdb] is similar to [print_result] except chews on the model and outputs a gdb script with a 
+    breakpoint at the subroutine and fills the appropriate registers *)
+
+let output_gdb (solver : Z3.Solver.solver) (status : Z3.Solver.status)
+               (env : Env.t) ~func:(func : string) ~filename:(gdb_filename : string) : unit =
+    match status with
+    | Z3.Solver.SATISFIABLE ->
+        let model = Z3.Solver.get_model solver
+                |> Option.value_exn ?here:None ?error:None ?message:None in
+        let regs = reg_names model in
+        Out_channel.with_file gdb_filename  ~f:(fun t -> 
+            Printf.fprintf t "break *%s\n" func; (* The "*" is necessary to break before some slight setup *)
+            Printf.fprintf t "start\n";
+            List.iter regs ~f:(fun r -> 
+                  let w = val_for_reg r model env in
+                  let s = Format.asprintf "set $%s = %a \n" (String.lowercase r) Bap.Std.Word.pp_hex w  in
+                  Printf.fprintf t "%s" s))   
+    | _ -> ()
+
+

wp/lib/bap_wp/src/output.mli

@@ -0,0 +1,40 @@
+(***************************************************************************)
+(*                                                                         *)
+(*  Copyright (C) 2018/2019 The Charles Stark Draper Laboratory, Inc.      *)
+(*                                                                         *)
+(*  This file is provided under the license found in the LICENSE file in   *)
+(*  the top-level directory of this project.                               *)
+(*                                                                         *)
+(*  This work is funded in part by ONR/NAWC Contract N6833518C0107.  Its   *)
+(*  content does not necessarily reflect the position or policy of the US  *)
+(*  Government and no official endorsement should be inferred.             *)
+(*                                                                         *)
+(***************************************************************************)
+
+(**
+
+   This module exports types and utilities to process and report results found uisng the wp plugin.
+
+*)
+
+module Expr = Z3.Expr
+
+module Arith = Z3.Arithmetic
+
+module BV = Z3.BitVector
+
+module Bool = Z3.Boolean
+
+module Array = Z3.Z3Array
+
+module Env = Environment
+
+module Constr = Constraint
+
+(** Prints out the result from check, and if the result is [SAT], generate a model that
+    represents the registers and memory values that lead to a specific program state. *)
+val print_result : Z3.Solver.solver -> Z3.Solver.status -> Constr.t -> Z3.context -> unit
+
+
+(** Prints to file a gdb script that will fill the appropriate registers with the countermodel *)
+val output_gdb : Z3.Solver.solver -> Z3.Solver.status -> Env.t -> func:string -> filename:string -> unit

wp/lib/bap_wp/src/precondition.ml

@@ -237,6 +237,7 @@ let set_fun_called (post : Constr.t) (env : Env.t) (tid : Tid.t) : Constr.t =
                                       Option.value_exn ?here:None ?error:None ?message:None) in
   Constr.substitute_one post fun_name (Bool.mk_true ctx)
 
+
 let get_stack_ptr_offset (sub : Sub.t) (arch : Arch.t) : Exp.t =
   let module Target = (val target_of_arch arch) in
   let blks = Term.to_sequence ~rev:true blk_t sub in
@@ -854,20 +855,7 @@ let check ?refute:(refute = true) (solver : Z3.Solver.solver) (ctx : Z3.context)
   in
   Z3.Solver.check solver [is_correct]
 
-let print_result (solver : Z3.Solver.solver) (status : Z3.Solver.status)
-    (goals: Constr.t) (ctx : Z3.context) : unit =
-  match status with
-  | Z3.Solver.UNSATISFIABLE -> Format.printf "\nUNSAT!\n%!"
-  | Z3.Solver.UNKNOWN -> Format.printf "\nUNKNOWN!\n%!"
-  | Z3.Solver.SATISFIABLE ->
-    Format.printf "\nSAT!\n%!";
-    let model = Z3.Solver.get_model solver
-                |> Option.value_exn ?here:None ?error:None ?message:None in
-    Format.printf "\nModel:\n%s\n%!" (Z3.Model.to_string model);
-    let refuted_goals = Constr.get_refuted_goals goals solver ctx in
-    Format.printf "\nRefuted goals:\n%!";
-    Seq.iter refuted_goals ~f:(fun g ->
-        Format.printf "%s\n%!" (Constr.refuted_goal_to_string g model))
+
 
 let exclude (solver : Z3.Solver.solver) (ctx : Z3.context) ~var:(var : Constr.z3_expr)
     ~pre:(pre : Constr.t) : Z3.Solver.status =

wp/lib/bap_wp/src/precondition.mli

@@ -198,9 +198,6 @@ val visit_sub : Env.t -> Constr.t -> Bap.Std.Sub.t -> Constr.t * Env.t
     refute is set to false, it checks for a model instead. *)
 val check : ?refute:bool -> Z3.Solver.solver -> Z3.context -> Constr.t -> Z3.Solver.status
 
-(** Prints out the result from check, and if the result is [SAT], generate a model that
-    represents the registers and memory values that lead to a specific program state. *)
-val print_result : Z3.Solver.solver -> Z3.Solver.status -> Constr.t -> Z3.context -> unit
 
 (** Adds a constraint to the Z3 solver in which var does not equal its value from
     the original Z3 model, then runs the Z3 solver again.

wp/plugin/README.md

@@ -329,6 +329,9 @@ The various options are:
 - `--wp-output-vars=var_list`. List of output variables for equivalence checking
   by `,` given the same input variables in the case of a comparative analysis.
   Defaults to `RAX,EAX` which are the 64- and 32-bit output registers for x86.
+- `--wp-gdb-filename=my_exec.gdb` output a gdb script to file `my_exec.gdb`. From
+  within gdb, run `source my_exec.gdb` to set a breakpoint at the function given by `--wp-function` and fill the appropriate registers with a found counter-model.
+
 
 ## C checking API
 

wp/plugin/wp.ml

@@ -43,7 +43,7 @@ let analyze_proj (proj : project) (var_gen : Env.var_gen) (ctx : Z3.context)
     ~inline:(inline : bool)
     ~to_inline:(to_inline : string list)
     ~post_cond:(post_cond : string)
-  : Constr.t =
+  : Constr.t * Env.t =
   let arch = Project.arch proj in
   let subs = proj |> Project.program |> Term.enum sub_t in
   let main_sub = find_func_err subs func in
@@ -71,10 +71,10 @@ let analyze_proj (proj : project) (var_gen : Env.var_gen) (ctx : Z3.context)
         Pre.mk_smtlib2_post env post_cond
       end
   in
-  let pre, _ = Pre.visit_sub env post main_sub in
+  let pre, env' = Pre.visit_sub env post main_sub in
   Format.printf "\nSub:\n%s\nPre:\n%a\n%!"
     (Sub.to_string main_sub) Constr.pp_constr pre;
-  pre
+  (pre, env')
 
 let compare_projs (proj : project) (file1: string) (file2 : string)
     (var_gen : Env.var_gen) (ctx : Z3.context)
@@ -83,7 +83,7 @@ let compare_projs (proj : project) (file1: string) (file2 : string)
     ~inline:(inline : bool)
     ~to_inline:(to_inline : string list)
     ~output_vars:(output_vars : string list)
-  : Constr.t =
+  : Constr.t * Env.t =
   let prog1 = In_channel.with_file file1 ~f:Program.Io.load in
   let prog2 = In_channel.with_file file2 ~f:Program.Io.load in
   (* Currently using the dummy binary's project to determine the architecture
@@ -117,7 +117,7 @@ let compare_projs (proj : project) (file1: string) (file2 : string)
       Pre.mk_default_env ctx var_gen ~subs:subs1 ~arch:arch,
       Pre.mk_default_env ctx var_gen ~subs:subs2 ~arch:arch
   in
-  let pre, _ =
+  let pre, env' =
     if check_calls then
       Comp.compare_subs_fun ~original:(main_sub1,env1) ~modified:(main_sub2,env2)
     else
@@ -137,7 +137,7 @@ let compare_projs (proj : project) (file1: string) (file2 : string)
   in
   Format.printf "\nComparing\n\n%s\nand\n\n%s\n%!"
     (Sub.to_string main_sub1) (Sub.to_string main_sub2);
-  pre
+  (pre, env')
 
 let main (file1 : string) (file2 : string)
     ~func:(func : string)
@@ -148,20 +148,27 @@ let main (file1 : string) (file2 : string)
     ~post_cond:(post_cond : string)
     ~num_unroll:(num_unroll : int option)
     ~output_vars:(output_vars : string list)
+    ~gdb_filename:(gdb_filename : string option)
     (proj : project) : unit =
   Log.start ~logdir:"/dev/stdout" ();
   let ctx = Env.mk_ctx () in
   let var_gen = Env.mk_var_gen () in
   let solver = Z3.Solver.mk_simple_solver ctx in
   update_default_num_unroll num_unroll;
-  let pre =
+  let pre, env' =
     if compare then
       compare_projs proj file1 file2 var_gen ctx ~func ~check_calls ~inline ~to_inline ~output_vars
     else
       analyze_proj proj var_gen ctx ~func ~inline ~to_inline ~post_cond
   in
   let result = Pre.check solver ctx pre in
-  Pre.print_result solver result pre ctx
+  let () = match gdb_filename with
+          | None -> ()
+          | Some f -> 
+                Printf.printf "Dumping gdb script to file: %s\n" f;
+                Output.output_gdb solver result env' ~func:func ~filename:f in 
+  Output.print_result solver result pre ctx
+
 
 module Cmdline = struct
   open Config
@@ -199,6 +206,8 @@ module Cmdline = struct
       ~doc:"List of output variables to compare separated by ',' given the same \
             input variables in the case of a comparative analysis. Defaults to `RAX,EAX` \
             which are the 64- and 32-bit output registers for x86."
+  let gdb_filename = param (some string) "gdb-filename" ~doc:"Output gdb script file for counterexample"
+      ~default:None
 
   let () = when_ready (fun {get=(!!)} ->
       Project.register_pass' @@
@@ -211,6 +220,7 @@ module Cmdline = struct
         ~post_cond:!!post_cond
         ~num_unroll:!!num_unroll
         ~output_vars:!!output_vars
+        ~gdb_filename:!!gdb_filename
     )
 
   let () = manpage [