-
Notifications
You must be signed in to change notification settings - Fork 14
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Pzucker/gdb #70
Merged
Merged
Pzucker/gdb #70
Changes from all commits
Commits
Show all changes
63 commits
Select commit
Hold shift + click to select a range
90c4ad4
Add Unknown case when pattern matching BIR types
40f2a2e
Save a binary's program instead of a project
ac69020
Use last block to determine how much to increment stack pointer
3134645
Update README with BAP version number
2ce0faf
Upgrade value_set to BAP 2.0
ba87d76
Update BAP version number in wp README
3597cf3
Add makefile for all sample binaries in resources
cf6bcb7
Look for a jmp to a var with noreturn as return block
6cc3a85
Basic gdb output might work. It works on the simplest example anyway
philzook58 bad4c87
added documentation
philzook58 585e8e9
added labelled parater for filename
philzook58 906ccf0
fiexed merge conficts
philzook58 84ea864
Made some suggested fixes in pull request
philzook58 9ffa399
Use last block to determine how much to increment stack pointer
fcc4840
Look for a jmp to a var with noreturn as return block
35a61e4
Basic gdb output might work. It works on the simplest example anyway
philzook58 1eb8646
added documentation
philzook58 683fc03
added labelled parater for filename
philzook58 390248a
Made some suggested fixes in pull request
philzook58 fb98a4b
added labelled parameter. Moved aorund some comments. Renamed postpro…
philzook58 10aff45
fixed readme typo
philzook58 4d6855f
Rebased.
philzook58 7d8750d
fixed merge conflicts. Again.
philzook58 666c43e
removed postprocess modules
philzook58 354ba34
fixed readme
philzook58 a926039
fixed weird spacing
philzook58 9cb9cd1
Use last block to determine how much to increment stack pointer
ed6d6d6
Look for a jmp to a var with noreturn as return block
f362a3e
Basic gdb output might work. It works on the simplest example anyway
philzook58 d9833dd
added documentation
philzook58 c3fc7bc
added labelled parater for filename
philzook58 9022447
Made some suggested fixes in pull request
philzook58 6ad1e3a
added labelled parameter. Moved aorund some comments. Renamed postpro…
philzook58 a1f5e16
fixed readme typo
philzook58 71c11e7
Rebased.
philzook58 6afb96e
Look for a jmp to a var with noreturn as return block
0df653f
Basic gdb output might work. It works on the simplest example anyway
philzook58 5bb857a
added documentation
philzook58 14db1b1
Made some suggested fixes in pull request
philzook58 a7998f2
removed postprocess modules
philzook58 3c6f4f6
fixed readme
philzook58 468d426
fixed weird spacing
philzook58 348145f
Merge branch 'pzucker/gdb' of https://github.com/draperlaboratory/cba…
philzook58 5aeab89
Use last block to determine how much to increment stack pointer
f7fced3
Look for a jmp to a var with noreturn as return block
f171fb7
Basic gdb output might work. It works on the simplest example anyway
philzook58 93a184a
added documentation
philzook58 9660ee5
added labelled parater for filename
philzook58 f0e2e8b
Made some suggested fixes in pull request
philzook58 e7e34ef
added labelled parameter. Moved aorund some comments. Renamed postpro…
philzook58 85ea279
fixed readme typo
philzook58 f189730
Rebased.
philzook58 526fe04
Look for a jmp to a var with noreturn as return block
c1d8e37
Basic gdb output might work. It works on the simplest example anyway
philzook58 658ccfe
added documentation
philzook58 1e4d12c
Made some suggested fixes in pull request
philzook58 7855bbc
removed postprocess modules
philzook58 810bf14
fixed readme
philzook58 76171ab
fixed weird spacing
philzook58 b786424
Use last block to determine how much to increment stack pointer
b0fa7bd
Look for a jmp to a var with noreturn as return block
3a76268
Rebased.
philzook58 46f9ee2
Merge branch 'pzucker/gdb' of https://github.com/draperlaboratory/cba…
philzook58 File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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)) | ||
| _ -> () | ||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not super important, but I noticed we use both the
Printf
modules and theFormat
modules. What's the difference between these two and would it be a good idea to be uniform?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have not figured out how to get Format to actually print to a file. Me and jt scratched our heads about this one and couldn't figure it out.
outputs a blank file. Thoughts? Printf was a workaround.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Tried some various flush commands too.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That's super interesting. Flushing sounds like the intuitive answer to this. If that's the case, keeping it as
Printf
is all good with me.