Pzucker/gdb mem #89
Pzucker/gdb mem #89
Conversation
wp/lib/bap_wp/src/output.mli
Outdated
| @@ -39,3 +39,10 @@ val print_result : Z3.Solver.solver -> Z3.Solver.status -> Constr.t | |||
|
|
|||
| (** 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 | |||
|
|
|||
| type mem_model = {default : Z3.Expr.expr ; model : (Z3.Expr.expr * Z3.Expr.expr) list} | |||
There was a problem hiding this comment.
Can you add a comment describing what default and model is supposed to be?
wp/lib/bap_wp/src/output.ml
Outdated
| @@ -60,6 +60,48 @@ let format_model (model : Model.model) (env1 : Env.t) (_env2 : Env.t) : string = | |||
| Format.flush_str_formatter () | |||
|
|
|||
|
|
|||
| type mem_model = {default : Z3.Expr.expr ; model : (Z3.Expr.expr * Z3.Expr.expr) list} | |||
There was a problem hiding this comment.
Not super important, but we've been using Constr.z3_expr instead of Z3.Expr.expr and I think it would be good to be consistent.
wp/lib/bap_wp/src/output.ml
Outdated
| extract_array' [] e | ||
|
|
||
|
|
||
| module F = Z3.Model.FuncInterp |
There was a problem hiding this comment.
Do we need to have this module redefined here if it was defined earlier as module FInterp = Model.FuncInterp?
There was a problem hiding this comment.
I should move this definition up. I don't see the FInterp definition?
There was a problem hiding this comment.
It actually looks like I don't even use F
There was a problem hiding this comment.
Might be a good idea to remove the definition if we don't use it
wp/lib/bap_wp/src/output.ml
Outdated
| { default = key; model = List.rev partial_map} | ||
| end | ||
| else begin | ||
| Printf.printf "Unpexpected case destructing Z3 array: %s" f_name; |
There was a problem hiding this comment.
Might want to make this a warning statement:
warning "Unexpected ... %s\n" f_name;
wp/lib/bap_wp/src/output.ml
Outdated
| let get_mem (m : Z3.Model.model) : mem_model option = | ||
| let decls = Z3.Model.get_decls m |> List.filter ~f:(fun decl -> (Z3.Symbol.to_string (Z3.FuncDecl.get_name decl)) = "mem0") in | ||
| match (List.hd decls) with | ||
| | None -> Printf.printf "No mem0 found."; |
There was a problem hiding this comment.
Also might want to make this a warning.
|
Looks good to me. Great work! |
wp/lib/bap_wp/src/output.ml
Outdated
| let get_mem (m : Z3.Model.model) : mem_model option = | ||
| let decls = Z3.Model.get_decls m |> List.filter ~f:(fun decl -> (Z3.Symbol.to_string (Z3.FuncDecl.get_name decl)) = "mem0") in | ||
| match (List.hd decls) with | ||
| | None -> warning "No mem0 found."; |
There was a problem hiding this comment.
I wonder if there's a way to be more agnostic about the name of the mem variable, e.g. by traipsing around a CPU or Target instance to be able to call CPU.mem from here: http://binaryanalysisplatform.github.io/bap/api/v1.6.0/Bap.Std.CPU.html
And get the name for the memory variable.
There was a problem hiding this comment.
See e.g. what we do here:
cbat_tools/wp/lib/bap_wp/src/precondition.ml
Line 260 in 9f1180b
wp/lib/bap_wp/tests/unit/test.ml
Outdated
| @@ -15,9 +15,10 @@ open OUnit2 | |||
|
|
|||
| let suite = | |||
| "Unit Tests" >::: [ | |||
| "Precondition" >::: Test_precondition.suite; | |||
| "Precondition" >::: Test_precondition.suite; | |||
There was a problem hiding this comment.
Any reason there's an extra space here?
| @@ -106,7 +106,7 @@ let analyze_proj (proj : project) (var_gen : Env.var_gen) (ctx : Z3.context) | |||
| 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, env', env) | |||
| (pre, env, env') | |||
|
|
|||
There was a problem hiding this comment.
I'm a bit disturbed by this bug. Is there any way we can return more structured output to avoid these kinds of shenanigans in the future? This is probably a task for myself.
|
Looks good Phil! My comments are quite minor, as usual. If you want to make fixes, great, otherwise I can rebase as soon as the merge conflicts are resolved. |
philzook58
force-pushed
the
pzucker/gdb-mem
branch
from
fe4d9c5
to
fab352a
Compare
After a long journey of Z3 build troubles and api confusion, adds the ability to extract memory models for gdb-output. Having said that, they are totally faulty and case gdb to fail immediately when they try to write to memory locations it has no access to.
I am concerned about what it will do if it encounters a lambda model, but it is profitable to open a pull review at this point I think.