Update wp option flags

wp/lib/bap_wp/bap_wp.opam

@@ -11,11 +11,12 @@ authors: [
   "Chloe Fortuna <cfortuna@draper.com>"
   "Chris Casinghino <ccasinghino@draper.com>"
   "JT Paasch <jpaasch@draper.com>"
+  "Philip Zucker <pzucker@draper.com>"
 ]
 license: "MIT"
-homepage: "https://github.com/draperlaboratory/CBAT-internal"
-bug-reports: "https://github.com/draperlaboratory/CBAT-internal"
-dev-repo: "git+https://github.com/draperlaboratory/CBAT-internal"
+homepage: "https://github.com/draperlaboratory/cbat_tools"
+bug-reports: "https://github.com/draperlaboratory/cbat_tools"
+dev-repo: "git+https://github.com/draperlaboratory/cbat_tools"
 depends: [
   "bap" {>= "master"}
   "core" {>= "0.11"}

wp/plugin/Makefile

@@ -12,7 +12,7 @@ build:
 	bapbuild -use-ocamlfind -pkgs 'z3,bap_wp' -tag 'warn(A-48-44)' $(PASS_NAME).plugin
 
 install: build verifier save_project
-	bapbundle update -desc 'Computes the weakest precondition of a subroutine given a postcondition' $(PASS_NAME).plugin
+	bapbundle update -desc 'Computes the weakest precondition of a subroutine given a postcondition.' $(PASS_NAME).plugin
 	bapbundle install $(PASS_NAME).plugin
 
 test: install save_project dummy

wp/plugin/README.md

@@ -277,61 +277,73 @@ nothing else is causing those changes.
 
 Use the bap CLI:
 
+To view the man page:
+
+    bap --wp-help
+
 To find the precondition of a subroutine:
 
     bap /path/to/exec --pass=wp \
       [--wp-function=function_name] \
-      [--wp-inline=bool] \
-      [--wp-postcond=smt-lib-string] \
-      [--wp-num-unroll=int] \
-      [--log-dir=directory]
+      [OPTIONS]
 
 To compare two binaries:
 
     bap /path/to/dummy/exec --pass=wp \
       --wp-compare=true \
       --wp-file1=/path/to/main1.bpj \
       --wp-file2=/path/to/main2.bpj \
-      [--wp-function=function_name] \
-      [--wp-check-calls=bool] \
-      [--wp-inline=bool] \
-      [--wp-num-unroll=int] \
-      [--log-dir=directory]
+      [OPTIONS]
 
 The various options are:
 
 - `--wp-compare=[true|false]`. This flag determines whether or
   not to analyze a single function. If enabled, you will need to
   specify the `file1` and `file2` options as well. `false` by default.
-- `--wp-function=function_name`. Determines which function to
-  verify. `wp` verifies a single function, though calling it on
-  the `main` function along with the `inline` option will analyze the
-  whole program. Has value `main` by default.
+
 - `--wp-file1=file_name.bpj`. Determines the location of the
   first file in the case of a comparative analysis.
+
 - `--wp-file2=file_name.bpj`. Determines the location of the
   second file in the case of a comparative analysis.
-- `--wp-inline=[true|false]`. Determines whether to inline a
-  function call for the purpose of computing the semantics. By default
-  we simply build a summary, which is a heuristic representation of
-  the function call semantics. `false` by default.
+
+- `--wp-function=function_name`. Determines which function to
+  verify. `wp` verifies a single function, though calling it on
+  the `main` function along with the `inline` option will analyze the
+  whole program. Has value `main` by default.
+
 - `--wp-check-calls=[true|false]`. Determines whether to compare
   the semantics of two programs by examining the return values of the
   function to be compared, or whether to compare which sub-routines
   are invoked in the body of the function. `false` by default.
+
+- `--wp-inline=[true|false]`. Determines whether to inline a
+  function call for the purpose of computing the semantics. By default
+  we simply build a summary, which is a heuristic representation of
+  the function call semantics. `false` by default.
+
+- `--wp-inline-funcs=funcs,list`. Determines which function calls to inline
+  when used in conjunction with `inline-funcs`. If `inline` is set without
+  specifying function calls, all functions in the binary will be inlined.
+
 - `--wp-postcond=smt-lib-string`. If present, replaces the
   default post-condition by the user-specified one, using the
   [smt-lib2] format. At the moment, the names of variables
   representing memory and registers are a bit magical, so consider
   this to be an experimental feature.
+
 - `--wp-num-unroll=num`. If present, replaces the default number of
   times to unroll each loop. The number of loop unrollings is 5 by default.
+
 - `--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.
-
+  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.
+
+- `--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/save_project/Makefile

@@ -9,6 +9,7 @@ build: $(PASS_NAME).ml
 
 install: $(PASS_NAME).ml
 	bapbuild $(PASS_NAME).plugin
+	bapbundle update -desc "Saves a binary's program data structure to disk." $(PASS_NAME).plugin
 	bapbundle install $(PASS_NAME).plugin
 
 clean:

wp/plugin/tests/test_wp.ml

@@ -100,28 +100,38 @@ let test_update_num_unroll (new_unroll : int option) (test_ctx : test_ctxt) : un
     assert_equal ~ctxt:test_ctx ~cmp:Int.equal ~msg:fail_msg updated original
 
 let suite = [
-  "Equiv Null Check"           >:: test_compare_elf "equiv_null_check" "SAT!";
-  "Equiv Argc"                 >:: test_compare_elf "equiv_argc" "SAT!";
-  "Diff Ret Val"               >:: test_compare_elf "diff_ret_val" "SAT!";
-  "Diff Pointer Val"           >:: test_compare_elf "diff_pointer_val" "SAT!";
-  "Switch Case Assignments"    >:: test_compare_elf "switch_case_assignments" "SAT!" ~func:"process_status";
-  "Switch Cases"               >:: test_compare_elf "switch_cases" "SAT!" ~func:"process_message" ~check_calls:true;
-  "Remove Stack Protector"     >:: test_compare_elf "no_stack_protection" "SAT!" ~output_vars:"RSI,RAX";
-  "Caller-saved registers"     >:: test_compare_elf "retrowrite_stub" "UNSAT!"
+  "Equiv Null Check"              >:: test_compare_elf "equiv_null_check" "SAT!";
+  "Equiv Argc"                    >:: test_compare_elf "equiv_argc" "SAT!";
+  "Diff Ret Val"                  >:: test_compare_elf "diff_ret_val" "SAT!";
+  "Diff Pointer Val"              >:: test_compare_elf "diff_pointer_val" "SAT!";
+  "Switch Case Assignments"       >:: test_compare_elf "switch_case_assignments" "SAT!" ~func:"process_status";
+  "Switch Cases"                  >:: test_compare_elf "switch_cases" "SAT!" ~func:"process_message" ~check_calls:true;
+  "No Stack Protection"           >:: test_compare_elf "no_stack_protection" "SAT!" ~output_vars:"RSI,RAX";
+  "Retrowrite Stub"               >:: test_compare_elf "retrowrite_stub" "UNSAT!"
     ~inline:true ~to_inline:"__afl_maybe_log";
-  "Pop RSP in Summary"         >:: test_compare_elf "retrowrite_stub" "UNSAT!";
-  "Simple WP"                  >:: test_single_elf "simple_wp" "main" "SAT!";
-  "Verifier Assume SAT"        >:: test_single_elf "verifier_calls" "verifier_assume_sat" "SAT!";
-  "Verifier Assume UNSAT"      >:: test_single_elf "verifier_calls" "verifier_assume_unsat" "UNSAT!";
-  "Verifier Nondet"            >:: test_single_elf "verifier_calls" "verifier_nondet" "SAT!";
-  "Function Call"              >:: test_single_elf "function_call" "main" "SAT!"
+  "Retrowrite Stub: imply inline" >:: test_compare_elf "retrowrite_stub" "UNSAT!" ~to_inline:"__afl_maybe_log";
+  "Retrowrite Stub: inline all"   >:: test_compare_elf "retrowrite_stub" "UNSAT!" ~inline:true;
+  "Retrowrite Stub: Pop RSP"      >:: test_compare_elf "retrowrite_stub" "UNSAT!";
+
+  "Simple WP"                     >:: test_single_elf "simple_wp" "main" "SAT!";
+  "Verifier Assume SAT"           >:: test_single_elf "verifier_calls" "verifier_assume_sat" "SAT!";
+  "Verifier Assume UNSAT"         >:: test_single_elf "verifier_calls" "verifier_assume_unsat" "UNSAT!";
+  "Verifier Nondet"               >:: test_single_elf "verifier_calls" "verifier_nondet" "SAT!";
+  "Function Call"                 >:: test_single_elf "function_call" "main" "SAT!"
     ~inline:true ~to_inline:"foo";
-  "Function Specs"             >:: test_single_elf "function_spec" "main" "UNSAT!"
+  "Function Call: imply inline"   >:: test_single_elf "function_call" "main" "SAT!" ~to_inline:"foo";
+  "Function Call: inline all"     >:: test_single_elf "function_call" "main" "SAT!" ~inline:true;
+  "Function Spec"                 >:: test_single_elf "function_spec" "main" "UNSAT!"
     ~inline:true ~to_inline:"foo";
-  "Function Specs"             >:: test_single_elf "function_spec" "main" "SAT!" ~inline:false;
-  "Nested Function Calls"      >:: test_single_elf "nested_function_calls" "main" "SAT!"
+  "Function Spec: imply inline"   >:: test_single_elf "function_spec" "main" "UNSAT!" ~to_inline:"foo";
+  "Function Spec: inline all "    >:: test_single_elf "function_spec" "main" "UNSAT!" ~inline:true;
+  "Function Spec: no inlining"    >:: test_single_elf "function_spec" "main" "SAT!" ~inline:false;
+  "Nested Function Calls"         >:: test_single_elf "nested_function_calls" "main" "SAT!"
     ~inline:true ~to_inline:"foo,bar";
-  "User Defined Postcondition" >:: test_single_elf "return_argc" "main" "SAT!" ~post:"(assert (= RAX0 #x0000000000000000))";
-  "Update Number of Unrolls"   >:: test_update_num_unroll (Some 3);
-  "Original Number of Unrolls" >:: test_update_num_unroll None;
+  "Nested Calls: imply inline"    >:: test_single_elf "nested_function_calls" "main" "SAT!" ~to_inline:"foo,bar";
+  "Nested Calls: inline all"      >:: test_single_elf "nested_function_calls" "main" "SAT!" ~inline:true;
+  "User Defined Postcondition"    >:: test_single_elf "return_argc" "main" "SAT!" ~post:"(assert (= RAX0 #x0000000000000000))";
+
+  "Update Number of Unrolls"      >:: test_update_num_unroll (Some 3);
+  "Original Number of Unrolls"    >:: test_update_num_unroll None;
 ]

wp/plugin/wp.ml

@@ -33,11 +33,39 @@ let find_func_err (subs : Sub.t Seq.t) (func : string) : Sub.t =
   | None -> failwith (missing_func_msg func)
   | Some f -> f
 
+(* Not efficient, but easier to read *)
+let find_func_in_one_of (f : string) ~to_find:(to_find : Sub.t Seq.t)
+    ~to_check:(to_check : Sub.t Seq.t) : Sub.t list =
+  match Seq.find ~f:(fun s -> String.equal (Sub.name s) f) to_find with
+  | None -> if Option.is_some (Seq.find ~f:(fun s -> String.equal (Sub.name s) f) to_check)
+    then []
+    else failwith (missing_func_msg f)
+  | Some f -> [f]
+
 let update_default_num_unroll (num_unroll : int option) : unit =
   match num_unroll with
   | Some n -> Pre.num_unroll := n
   | None -> ()
 
+let has_inline_funcs (to_inline : string list) : bool =
+  not (List.is_empty to_inline)
+
+let find_inline_funcs (inline_funcs : string list) ~to_find:(to_find : Sub.t Seq.t)
+    ~to_check:(to_check : Sub.t Seq.t) : Sub.t Seq.t =
+  if List.is_empty inline_funcs then
+    to_find
+  else
+    inline_funcs
+    |> List.map ~f:(find_func_in_one_of ~to_find ~to_check)
+    |> List.concat
+    |> Seq.of_list
+
+let varset_to_string (vs : Var.Set.t) : string =
+  vs
+  |> Var.Set.to_sequence
+  |> Seq.to_list
+  |> List.to_string ~f:Var.to_string
+
 let analyze_proj (proj : project) (var_gen : Env.var_gen) (ctx : Z3.context)
     ~func:(func : string)
     ~inline:(inline : bool)
@@ -48,10 +76,14 @@ let analyze_proj (proj : project) (var_gen : Env.var_gen) (ctx : Z3.context)
   let subs = proj |> Project.program |> Term.enum sub_t in
   let main_sub = find_func_err subs func in
   let env =
-    if inline then
-      let to_inline = to_inline
-                      |> List.map ~f:(find_func_err subs)
-                      |> Seq.of_list
+    if inline || has_inline_funcs to_inline then
+      let to_inline =
+        if List.is_empty to_inline then
+          subs
+        else
+          to_inline
+          |> List.map ~f:(find_func_err subs)
+          |> Seq.of_list
       in
       Pre.mk_inline_env ctx var_gen ~subs ~arch ~to_inline:to_inline
     else
@@ -93,24 +125,10 @@ let compare_projs (proj : project) (file1: string) (file2 : string)
   let subs2 = Term.enum sub_t prog2 in
   let main_sub1 = find_func_err subs1 func in
   let main_sub2 = find_func_err subs2 func in
-  (* Not efficient, but easier to read *)
-  let find_func_in_one_of f ~to_find ~to_check =
-    match Seq.find ~f:(fun s -> String.equal (Sub.name s) f) to_find with
-    | None -> if Option.is_some (Seq.find ~f:(fun s -> String.equal (Sub.name s) f) to_check)
-      then []
-      else failwith (missing_func_msg func)
-    | Some f -> [f]
-  in
   let env1, env2 =
-    if inline then
-      let to_inline1 = to_inline
-                       |> List.map ~f:(find_func_in_one_of ~to_find:subs1 ~to_check:subs2)
-                       |> List.concat
-                       |> Seq.of_list in
-      let to_inline2 = to_inline
-                       |> List.map ~f:(find_func_in_one_of ~to_find:subs2 ~to_check:subs1)
-                       |> List.concat
-                       |> Seq.of_list in
+    if inline || has_inline_funcs to_inline then
+      let to_inline1 = find_inline_funcs to_inline ~to_find:subs1 ~to_check:subs2 in
+      let to_inline2 = find_inline_funcs to_inline ~to_find:subs2 ~to_check:subs1 in
       Pre.mk_inline_env ctx var_gen ~subs:subs1 ~arch:arch ~to_inline:to_inline1,
       Pre.mk_inline_env ctx var_gen ~subs:subs2 ~arch:arch ~to_inline:to_inline2
     else
@@ -125,10 +143,8 @@ let compare_projs (proj : project) (file1: string) (file2 : string)
         let output_vars = Var.Set.union
             (Pre.get_output_vars main_sub1 output_vars)
             (Pre.get_output_vars main_sub2 output_vars) in
-        let input_vars = Var.Set.union_list
-            [Pre.get_vars main_sub1; Pre.get_vars main_sub2; output_vars] in
-        let varset_to_string vs =
-          vs |> Var.Set.to_sequence |> Seq.to_list |> List.to_string ~f:Var.to_string in
+        let input_vars = Var.Set.union
+            (Pre.get_vars main_sub1) (Pre.get_vars main_sub2) in
         debug "Input: %s%!" (varset_to_string input_vars);
         debug "Output: %s%!" (varset_to_string output_vars);
         Comp.compare_subs_eq ~input:input_vars ~output:output_vars
@@ -155,60 +171,80 @@ let main (file1 : string) (file2 : string)
   let var_gen = Env.mk_var_gen () in
   let solver = Z3.Solver.mk_simple_solver ctx in
   update_default_num_unroll num_unroll;
+  let has_files_to_compare = String.(file1 <> "" && file2 <> "") in
   let pre, env' =
-    if compare then
+    if compare || has_files_to_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
   let () = match gdb_filename with
           | None -> ()
-          | Some f -> 
+          | Some f ->
                 Printf.printf "Dumping gdb script to file: %s\n" f;
-                Output.output_gdb solver result env' ~func:func ~filename:f in 
+                Output.output_gdb solver result env' ~func:func ~filename:f in
   Output.print_result solver result pre ctx
 
 
 module Cmdline = struct
   open Config
 
-  let file1 = param string "file1" ~doc:"Project file location for first binary"
-      ~default:""
+  let compare = param bool "compare" ~as_flag:true ~default:false
+      ~doc:"Determines whether to analyze a single function or compare the same \
+            function across two binaries. If enabled, project files must be specified \
+            with the `file1' and `file2' options."
 
-  let file2 = param string "file2" ~doc:"Project file location for second binary"
-      ~default:""
+  let file1 = param string "file1" ~default:""
+      ~doc:"Project file location of the first binary for comparative analysis, \
+            which can be generated via the save-project plugin. If both `file1' and \
+            `file2' are specified, wp will automatically run the comparative analysis."
 
-  let func = param string "function" ~doc:"Function in both binaries to compare"
-      ~default:"main"
+  let file2 = param string "file2" ~default:""
+      ~doc:"Project file location of the second binary for comparative analysis, \
+            which can be generated via the save-project plugin. If both `file1' and \
+            `file2' are specified, wp will automatically run the comparative analysis."
 
-  let check_calls = param bool "check-calls" ~doc:"Check conservation of function calls"
-      ~as_flag:true ~default:false
+  let func = param string "function" ~default:"main"
+      ~doc:"Function to run the wp analysis on. `main' by default. If the function \
+            cannot be found in the binary or both binaries in the comparison \
+            case, wp analysis should fail."
 
-  let compare = param bool "compare" ~doc:"Compare the subroutines of two binaries"
-      ~as_flag:true ~default:false
+  let check_calls = param bool "check-calls" ~as_flag:true ~default:false
+      ~doc:"If set, compares which subroutines are invoked in the body of the \
+            function. Otherwise, compares the return values computed in the function \
+            body."
 
   let inline = param bool "inline" ~as_flag:true ~default:false
-      ~doc:"Inline function calls. Use in conjunction with inline-funcs to \
+      ~doc:"Inline function calls. Use in conjunction with `inline-funcs' to \
             specify which functions should be replaced by their bodies for purposes \
-            of analysis"
+            of analysis. If not set, function summaries are used at function call \
+            time."
 
-  let to_inline = param (list string) "inline-funcs" ~doc:"List of functions to inline. Use in "
+  let to_inline = param (list string) "inline-funcs"
+      ~doc:"List of functions to inline separated by `,'. By default, if `inline' \
+            is set without specifying `inline-funcs', all functions in the binary \
+            will be inlined."
       ~default:[]
 
-  let post_cond = param string "postcond" ~doc:"Post condition in SMT-LIB format"
-      ~default:""
+  let post_cond = param string "postcond" ~default:""
+      ~doc:"Post condition in SMT-LIB format used when analyzing a single binary. \
+            If no post condition is specified, a trivial post condition (`true') \
+            will be used."
 
-  let num_unroll = param (some int) "num-unroll" ~doc:"Amount of times to unroll each loop"
+  let num_unroll = param (some int) "num-unroll"
+      ~doc:"Amount of times to unroll each loop. By default, wp will unroll each \
+            loop 5 times."
       ~default:None
 
   let output_vars = param (list string) "output-vars" ~default:["RAX"; "EAX"]
-      ~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` \
+      ~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' @@
       main !!file1 !!file2
@@ -225,7 +261,6 @@ module Cmdline = struct
 
   let () = manpage [
       `S "DESCRIPTION";
-      `P
-        ("Compute the weakest precondition of a subroutine given a postcondition")
+      `P "Computes the weakest precondition of a subroutine given a postcondition."
     ]
 end