-
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/precondition #101
Pzucker/precondition #101
Changes from 1 commit
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -127,6 +127,9 @@ val wp_rec_call : | |
typically a constant. *) | ||
val add_var : t -> Bap.Std.Var.t -> Constr.z3_expr -> t | ||
|
||
(** Remove a binding in the environment for a bap variable. *) | ||
val remove_var : t -> Bap.Std.Var.t -> t | ||
|
||
(** Add a precondition to be associated to a block b to the environment. *) | ||
val add_precond : t -> Bap.Std.Tid.t -> Constr.t -> t | ||
|
||
|
@@ -209,4 +212,20 @@ val mk_z3_expr : Z3.context -> name:string -> typ:Bap.Std.Type.t -> Constr.z3_ex | |
constant is "fresh" with the {!Environment.var_gen}. *) | ||
val new_z3_expr : ?name:string -> t -> Bap.Std.Type.t -> Constr.z3_expr | ||
|
||
|
||
(** [get_decls_and_symbols] builds from a the var_map in an environment | ||
a mapping of all Z3 func_decl to their symbol. This is a helper function for | ||
[mk_smtlib2] *) | ||
|
||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Just a little nitpick, but there are no blank lines between the ocamldoc comments and the function signatures in the other functions, and I think it would be great to be consistent. |
||
val get_decls_and_symbols : t -> ((Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list) | ||
|
||
|
||
(** [mk_smtlib2_single env smtlib_str] takes in a string representing a | ||
valid SMT-Lib-2 statement. | ||
The variables in the SMT-Lib statements need to appear in the | ||
environment. The intended purpose of this function is generating hypothesis | ||
and postconditions for single binary analysis *) | ||
val mk_smtlib2_single : t -> string -> Constr.t | ||
|
||
|
||
(*---------------------------------------------------*) |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -217,11 +217,10 @@ let exp_to_z3 (exp : Exp.t) (env : Env.t) : Constr.z3_expr * Constr.t list * Con | |
debug "Visiting let %s = %s in %s%!" | ||
(Var.to_string v) (Exp.to_string exp) (Exp.to_string body); | ||
let exp_val, env = exp_to_z3_body exp env in | ||
(* FIXME: we're handling this incorrectly! The variable should | ||
be removed from the context after leaving the scope of the | ||
Let! *) | ||
let env' = Env.add_var env v exp_val in | ||
exp_to_z3_body body env' | ||
let z3_expr, env = exp_to_z3_body body env' in | ||
let env = Env.remove_var env v in | ||
(z3_expr, env) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. If a variable in the let-binding shares a name with a variable that already existed in the There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Correct, this could conceivable occur if some pervert wanted to name a let-bound variable There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Hmm. That's an interesting point. We didn't implement this correctly basically. We should store the variable we're covering up. In practice it probably isn't a problem because the let bindings seem to use names like "$1", but should probably still be fixed for sanity There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is a really good catch There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think I fixed this |
||
| Unknown (str, typ) -> | ||
debug "Visiting unknown: %s Type:%s%!" str (Type.to_string typ); | ||
Env.new_z3_expr env ~name:("unknown_" ^ str) typ, env | ||
|
@@ -847,42 +846,6 @@ let non_null_assert : Env.exp_cond = fun env exp -> | |
else | ||
Some (Assume (Constr.mk_goal "assume" (Bool.mk_and ctx conds))) | ||
|
||
let mk_smtlib2_post (env : Env.t) (smt_post : string) : Constr.t = | ||
let ctx = Env.get_context env in | ||
let sort_symbols = [] in | ||
let sorts = [] in | ||
let fun_decls = | ||
Env.EnvMap.fold (Env.get_var_map env) ~init:[] | ||
~f:(fun ~key:_ ~data:z3_var decls -> | ||
assert (Z3.Expr.is_const z3_var); | ||
Z3.FuncDecl.mk_const_decl_s ctx | ||
(Z3.Expr.to_string z3_var) | ||
(Z3.Expr.get_sort z3_var) | ||
::decls | ||
) | ||
in | ||
let fun_symbols = | ||
Env.EnvMap.fold (Env.get_var_map env) ~init:[] | ||
~f:(fun ~key:_ ~data:z3_var decls -> | ||
assert (Z3.Expr.is_const z3_var); | ||
Z3.Symbol.mk_string ctx | ||
(Z3.Expr.to_string z3_var) | ||
::decls | ||
) | ||
in | ||
let asts = Z3.SMT.parse_smtlib2_string ctx smt_post | ||
sort_symbols | ||
sorts | ||
fun_symbols | ||
fun_decls | ||
in | ||
let goals = List.map (Z3.AST.ASTVector.to_expr_list asts) | ||
~f:(fun e -> | ||
e | ||
|> Constr.mk_goal (Expr.to_string e) | ||
|> Constr.mk_constr) | ||
in | ||
Constr.mk_clause [] goals | ||
|
||
let check ?refute:(refute = true) (solver : Solver.solver) (ctx : Z3.context) | ||
(pre : Constr.t) : Solver.status = | ||
|
@@ -895,6 +858,7 @@ let check ?refute:(refute = true) (solver : Solver.solver) (ctx : Z3.context) | |
else | ||
pre' | ||
in | ||
Printf.printf "Z3 Query:\n%s\n" (Z3.Expr.to_string (Z3.Expr.simplify is_correct None)); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Do you think we can make this an There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Seems reasonable. Or perhaps a command line flag. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'm not against having a flag for There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yea |
||
let () = Z3.Solver.add solver [is_correct] in | ||
Z3.Solver.check solver [] | ||
|
||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -123,7 +123,7 @@ let test_sub_pair_1 (test_ctx : test_ctxt) : unit = | |
let output_vars = Var.Set.singleton z in | ||
let compare_prop, _, _ = Comp.compare_subs_eq | ||
~input:input_vars ~output:output_vars | ||
~original:(sub1,env1) ~modified:(sub2,env2) in | ||
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_pre:"" in | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Should There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yeah. i debated this one. I just hated putting them as the first arguments, which optional seems to require. But it might be the right call There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I vote for There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Shouldn't the defaults both be There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes, I think you're right, actually. |
||
assert_z3_compare test_ctx ~orig:env1 ~modif:env2 | ||
(Sub.to_string sub1) (Sub.to_string sub2) | ||
compare_prop Z3.Solver.UNSATISFIABLE | ||
|
@@ -163,7 +163,7 @@ let test_sub_pair_2 (test_ctx : test_ctxt) : unit = | |
let output_vars = Var.Set.singleton z in | ||
let compare_prop, _, _ = Comp.compare_subs_eq | ||
~input:input_vars ~output:output_vars | ||
~original:(sub1,env1) ~modified:(sub2,env2) in | ||
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_pre:"" in | ||
assert_z3_compare test_ctx ~orig:env1 ~modif:env2 | ||
(Sub.to_string sub1) (Sub.to_string sub2) | ||
compare_prop Z3.Solver.SATISFIABLE | ||
|
@@ -197,7 +197,7 @@ let test_sub_pair_3 (test_ctx : test_ctxt) : unit = | |
let output_vars = Var.Set.singleton z in | ||
let compare_prop, _, _ = Comp.compare_subs_eq | ||
~input:input_vars ~output:output_vars | ||
~original:(sub1,env1) ~modified:(sub2,env2) in | ||
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_pre:"" in | ||
assert_z3_compare test_ctx ~orig:env1 ~modif:env2 | ||
(Sub.to_string sub1) (Sub.to_string sub2) | ||
compare_prop Z3.Solver.UNSATISFIABLE | ||
|
@@ -234,7 +234,7 @@ let test_sub_pair_4 (test_ctx : test_ctxt) : unit = | |
let output_vars = Var.Set.singleton y in | ||
let compare_prop, _, _ = Comp.compare_subs_eq | ||
~input:input_vars ~output:output_vars | ||
~original:(sub1,env1) ~modified:(sub2,env2) in | ||
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_pre:"" in | ||
assert_z3_compare test_ctx ~orig:env1 ~modif:env2 | ||
(Sub.to_string sub1) (Sub.to_string sub2) | ||
compare_prop Z3.Solver.UNSATISFIABLE | ||
|
@@ -271,7 +271,7 @@ let test_sub_pair_5 (test_ctx : test_ctxt) : unit = | |
let output_vars = Var.Set.singleton y in | ||
let compare_prop, _, _ = Comp.compare_subs_eq | ||
~input:input_vars ~output:output_vars | ||
~original:(sub1,env1) ~modified:(sub2,env2) in | ||
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_pre:"" in | ||
assert_z3_compare test_ctx ~orig:env1 ~modif:env2 | ||
(Sub.to_string sub1) (Sub.to_string sub2) | ||
compare_prop Z3.Solver.SATISFIABLE | ||
|
@@ -462,7 +462,7 @@ let test_fun_outputs_1 (test_ctx : test_ctxt) : unit = | |
let output_vars = Var.Set.singleton ret_var in | ||
let compare_prop, _, _ = Comp.compare_subs_eq | ||
~input:input_vars ~output:output_vars | ||
~original:(main_sub1, env1) ~modified:(main_sub2, env2) in | ||
~original:(main_sub1, env1) ~modified:(main_sub2, env2) ~smtlib_post:"" ~smtlib_pre:"" in | ||
assert_z3_compare test_ctx ~orig:env1 ~modif:env2 | ||
(Sub.to_string main_sub1) | ||
(Sub.to_string main_sub2) | ||
|
@@ -495,7 +495,7 @@ let test_fun_outputs_2 (test_ctx : test_ctxt) : unit = | |
let output_vars = Var.Set.singleton ret_var in | ||
let compare_prop, _, _ = Comp.compare_subs_eq | ||
~input:input_vars ~output:output_vars | ||
~original:(main_sub1, env1) ~modified:(main_sub2, env2) in | ||
~original:(main_sub1, env1) ~modified:(main_sub2, env2) ~smtlib_post:"" ~smtlib_pre:"" in | ||
assert_z3_compare test_ctx ~orig:env1 ~modif:env2 | ||
(Sub.to_string main_sub1) | ||
(Sub.to_string main_sub2) | ||
|
@@ -599,7 +599,7 @@ let test_sub_pair_mem_1 (test_ctx : test_ctxt) : unit = | |
let output_vars = Var.Set.singleton mem in | ||
let compare_prop, _, _ = Comp.compare_subs_eq | ||
~input:input_vars ~output:output_vars | ||
~original:(sub1,env1) ~modified:(sub2,env2) in | ||
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_pre:"" in | ||
assert_z3_compare test_ctx ~orig:env1 ~modif:env2 | ||
(Sub.to_string sub1) (Sub.to_string sub2) | ||
compare_prop Z3.Solver.SATISFIABLE | ||
|
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 agree, hypothesis might be a better name for this.
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.
So
smtlib_hyp
orsmtlib_hype
if we're trying to appeal to the youth.