Pzucker/precondition #101

philzook58 · 2019-11-21T18:37:56Z

adds the ability the specify assumptions at the beginning of a program about the variables. Closes Add concrete values as preconditions #49 ? Does not address idea about soft constraints
It does a string find and replace on variables in smt-lib expressions given to convert them to the internal mangled names.
Contains bug fix for popping BIL Let bindings from the Env.var_map
bug fix for the returned environments from analyze_proj in wp.ml. Should fix Models are not being printed out #100
Moved smt-lib related functions out of precondition.ml
Adds the ability to create custom preconditions and postconditions in comparative analysis. The variables are referenced by appending "_orig" and "_mod" to variable names.

Example usage

bap resources/sample_binaries/dummy/hello_world.out --pass=wp --wp-compare=true --wp-file1=resources/sample_binaries/equiv_argc/main_1.bpj --wp-file2=resources/sample_binaries/equiv_argc/main_2.bpj --wp-function=main --wp-output-vars=RAX,EAX --wp-precond="(assert (= RDI_mod #x0000000000000003))  (assert (= RDI_orig #x0000000000000003))"

bap resources/sample_binaries/simple_wp/main --pass=wp --wp-precond="(assert (= RDI #x0000000000000002))"

TODO:

Does the naming make sense for precondition? Should it be called assumptions or hypotheses?
I'll also need to rebase off of Chloe's pull request
I still need to add tests
The placement of the new smt-lib code in compare.ml feels a bit ad hoc. Refactor it somewhere?

codyroux · 2019-11-22T00:17:33Z

Looking good other than the conflicts! I agree that the smtlib stuff should be in its own module maybe something like Z3_utils.ml. I'll take a closer look in the morning.

fortunac · 2019-11-22T15:21:06Z

wp/lib/bap_wp/src/environment.mli

+(** [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] *)
+


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.

fortunac · 2019-11-22T15:28:53Z

wp/lib/bap_wp/src/precondition.ml

-      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)


If a variable in the let-binding shares a name with a variable that already existed in the env, would removing it also remove the original variable? If so, it might be good to write a comment about that.

Correct, this could conceivable occur if some pervert wanted to name a let-bound variable RAX, or more pragmatically if an inner let shadows an outer let. This should cause a run-time error rather than a mysterious change in semantics. A comment might be appropriate though.

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

This is a really good catch

I think I fixed this

fortunac · 2019-11-22T15:43:50Z

wp/lib/bap_wp/src/compare.ml

 let compare_subs_eq
    ~input:(input : Var.Set.t)
    ~output:(output : Var.Set.t)
    ~original:(original : Sub.t * Env.t)
    ~modified:(modified : Sub.t * Env.t)
+    ~smtlib_post:(smtlib_post : string)
+    ~smtlib_pre:(smtlib_pre : string)


I agree, hypothesis might be a better name for this.

So smtlib_hyp or smtlib_hype if we're trying to appeal to the youth.

fortunac · 2019-11-22T15:49:02Z

wp/lib/bap_wp/tests/unit/test_compare.ml

@@ -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


Should smtlib_post and smtlib_pre be optional arguments defaulting to ""? This one is really up to you.

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

I vote for true and false as defaults, respectively.

Shouldn't the defaults both be true?

Yes, I think you're right, actually.

fortunac · 2019-11-22T15:51:57Z

wp/lib/bap_wp/src/precondition.ml

@@ -833,6 +796,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));


Do you think we can make this an info log or something so that it doesn't print out when we run the unit tests?

Seems reasonable. Or perhaps a command line flag.
Is there an insane amount of stuff in info? I would be of the opinion we also suppress the Constrain being printed by default and maybe the BIL.

I'm not against having a flag for verbose mode, but it's probably out of the scope for this PR. And there isn't too much stuff in info. From grepping, I can see we have 8 info logs.

Yea info seems reasonable... IDK.

fortunac · 2019-11-22T15:54:47Z

Looks super good! Just a few nitpicks. I agree, putting the smtlib functions in its own module and adding unit test(s) for the compare module is a great idea. Good work! 🎉

minor fixes to formatting and 1 silly bug

fortunac · 2019-12-05T18:18:01Z

wp/lib/bap_wp/src/z3_utils.mli

+
+(**
+
+   This module exports types and utilities to process and report results found


Can we update this comment to match the z3_utils module?

Fixed. Good catch.

fortunac reviewed Nov 22, 2019

View reviewed changes

Initial commit of precondition smtlib code

70dd0f4

minor fixes to formatting and 1 silly bug

philzook58 force-pushed the pzucker/precondition branch from baa4501 to 70dd0f4 Compare November 22, 2019 16:17

fortunac mentioned this pull request Dec 4, 2019

Add hooks to memory reads about memory offsets #104

Closed

Made suggested changes. Added tests. Make a z3_utils file

01e18a7

fortunac reviewed Dec 5, 2019

View reviewed changes

updated desciprtion on z3_utils.mli

2d64676

codyroux merged commit 6edf3be into master Dec 5, 2019

codyroux deleted the pzucker/precondition branch December 5, 2019 19:22

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Pzucker/precondition #101

Pzucker/precondition #101

philzook58 commented Nov 21, 2019 •

edited

codyroux commented Nov 22, 2019

fortunac Nov 22, 2019

fortunac Nov 22, 2019

codyroux Nov 22, 2019

philzook58 Nov 22, 2019

philzook58 Nov 22, 2019

philzook58 Dec 5, 2019

fortunac Nov 22, 2019

codyroux Nov 22, 2019

fortunac Nov 22, 2019

philzook58 Nov 22, 2019

codyroux Nov 22, 2019

philzook58 Dec 2, 2019

codyroux Dec 3, 2019

fortunac Nov 22, 2019

philzook58 Nov 22, 2019

fortunac Nov 22, 2019

codyroux Nov 22, 2019

fortunac commented Nov 22, 2019

fortunac Dec 5, 2019

philzook58 Dec 5, 2019


		(**

		This module exports types and utilities to process and report results found

Pzucker/precondition #101

Pzucker/precondition #101

Conversation

philzook58 commented Nov 21, 2019 • edited

codyroux commented Nov 22, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fortunac commented Nov 22, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

philzook58 commented Nov 21, 2019 •

edited