To view the man page:
$ bap wp --help
--func=<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. If no function is specified or the function cannot be found in the binary/binaries, WP will exit with an error message.--inline=<posix-regexp> — Functions specified by the provided POSIX regular expression will inlined. When functions are not inlined, heuristic function summaries are used at function call sites. For example, if you want to inline the functions foo and bar, you can write --inline=foo|bar. To inline everything, use --inline=.* (not generally recommended).--pointer-reg-list=<reg-list> — This flag specifies a comma delimited list of input registers to be treated as pointers at the start of program execution. This means that these registers are restricted in value to point to memory known to be initialized at the start of the function. For example, RSI,RDI would specify that RSI and RDI's values should be restricted to initialized memory at the start of execution. --num-unroll=<num> — Specifies the number of times to unroll each loop. WP will unroll each loop 5 times by default.--gdb-output=<filename.gdb> — When WP results in SAT, outputs a gdb script to file filename.gdb. From within gdb, run source filename.gdb to set a breakpoint at the function given by --func and fill the appropriate registers with the values found in the countermodel. In the case WP returns UNSAT or UNKNOWN, no script will be outputted.--bildb-output=<filename.yml> — When WP results in SAT, outputs a BILDB initialization script to file filename.yml. This YAML file sets the registers and memory to the values found in the countermodel, allowing BILDB to follow the same execution trace. In the case the analysis returns UNSAT or UNKNOWN, no script will be outputted.--use-fun-input-regs — At a function call site, uses all possible input registers as arguments to a function symbol generated for an output register. If this flag is not present, no registers will be used.--stack-base=<address> — Sets the location of the stack frame for the function under analysis. By default, WP assumes the stack frame for the current function is between 0x40000000 and 0x3F800080.--stack-size=<size> — Sets the size of the stack. size should be denoted in bytes. By default, the size of the stack is 0x800000, which is 8MB.--ext-solver-path=</bin/boolector> — Allows the usage of an external SMT solver. This option has only been tested with Boolector version 3.2.1. For other solvers, results may vary.--show=[bir|refuted-goals|paths|precond-internal|precond-smtlib] — A list of details to print out from the analysis. Multiple options can be specified as a comma-separated list. For example: --show=bir,refuted-goals. The options are:
bir: The code of the binary/binaries in BAP Intermediate Representation.refuted-goals: In the case WP results in SAT, a list of goals refuted in the model that contains their tagged names, their concrete values, and their Z3 representation.paths: The execution path of the binary that results in a refuted goal. The path contains information about the jumps taken, their addresses, and the values of the registers at each jump. This option automatically prints out the refuted goals. It also writes files that contain control-flow graphs (CFGs) for the functions being analyzed. In each CFG, the execution path that results in a refuted goal is highlighted. The files are called <f>_orig.dot and <f>_mod.dot, where <f> is the name of the function being analyzed. CFGs are written in Graphviz DOT syntax so that they can be rendered with any DOT viewing tool.precond-smtlib: The precondition printed out in Z3's SMT-LIB2 format.precond-internal: The precondition printed out in WP's internal format for the Constr.t type.--debug=[z3-solver-stats|z3-verbose|constraint-stats|eval-constraint-stats] — A list of debugging statistics to display. Multiple statistics may be specified in a comma-separated list. For example: --debug=z3-solver-stats,z3-verbose. The options are:
z3-solver-stats: Information and statistics about Z3's solver. It includes information such as the maximum amount of memory used and the number of allocations.z3-verbose: Z3's verbosity level. It outputs information such as the tactics the Z3 solver used.constraint-stats: Statistics regarding the internal Constr.t data structure, including the number of goals, ITEs, clauses, and substitutions.eval-constraint-stats: Statistics regarding the internal expression lists during evaluation of the Constr.t data type.--user-func-specs=<user-spec-list> — List of user-defined subroutine specifications. For each subroutine, it creates the weakest precondition given the name of the subroutine and its pre and post-conditions. Usage: --user-func-specs="<sub name>,<precondition>,<postcondition>". For example, --user-func-specs="foo,(assert (= RAX RDI)),(assert (= RAX init_RDI))" means "for subroutine named foo, specify that its precondition is RAX = RDI and its postcondition is RAX = init_RDI". Multiple subroutine specifications are delimited with ';'s, i.e.: --user-func-specs="foo,(assert (= RAX RDI)),(assert (= RAX init_RDI));bar,(assert (= RAX RDI)),(assert (= RAX init_RDI))".
--fun-specs=<spec-list> — List of built-in function summaries to be used at a function call site in order of precedence. A target function will be mapped to a function spec if it fulfills the spec's requirements. All function specs set the target function as called and update the stack pointer. The default specs set are verifier-assume, varifier-nondet, empty, and chaos-caller-saved. Note that if a function is set to be inlined, it will not use any of the following function specs. Available built-in specs:
verifier-error: Used for calls to __VERIFIER_error and __assert_fail. Looks for inputs that would cause execution to reach these functions.verifier-assume: Used for calls to __VERIFIER_assume. Adds an assumption to the precondition based on the argument to the function call.verifier-nondet: Used for calls to nondeterministic functions such as __VERIFIER_nondet_*, calloc, and malloc. Chaoses the output to the function call representing an arbitrary pointer.afl-maybe-log: Used for calls to __afl_maybe_log. Chaoses the registers RAX, RCX, and RDX.arg-terms: Used when BAP's uplifter returns a nonempty list of input and output registers for the target function. Chaoses this list of output registers.chaos-caller-saved: Used for the x86 architecture. Chaoses the caller-saved registers.rax-out: Chaos RAX if it can be found on the left-hand side of an assignment in the target function.chaos-rax: Chaos RAX regardless if it has been used on the left-hand side of an assignment in the target function.empty: Used for empty subroutines. Performs no actions.To analyze a single program, the command you want to invoke has this basic form:
$ bap wp \ <-- The command is wp
--func=FUNC \ <-- The function to examine
[options] \ <-- Any extra options
/path/to/exe <-- The path to a binary program
The following options select or adjust the property that will be checked for the function FUNC in the case of single-program analysis.
--trip-asserts — Looks for inputs to the subroutine that would cause an __assert_fail or __VERIFIER_error to be reached.--check-null-derefs — Checks for inputs that would result in dereferencing a NULL address during a memory read or write. This flag can also be used in comparative analysis; see below.--precond=<smt-lib-string> — Allows you to specify an assertion that WP will assume is true at the beginning of the function it is analyzing. Assertions are specified in the smt-lib2 format. If no precondition is specified, a trivial precondition of true will be used. This flag can also be used in comparative analysis; see below.--postcond=<smt-lib-string> — Allows you to specify an assertion that WP will assume is true at the end of the function it is analyzing, using the smt-lib2 format. If no postcondition is specified, a trivial postcondition of true will be used. This flag can also be used in comparative analysis; see below.--loop-invariant=<s-expression> — Usage: (((address <addr>) (invariant <smtlib>)) (...)). Assumes the subroutine contains unnested while loops with one entry point and one exit each. Checks the loop invariant written in smt-lib2 format for the loop with its header at the given address. The address should be written in BAP's bitvector string format. Only supported for a single binary analysis.To analyze two programs,the command you want to invoke has this basic form:
$ bap wp \ <-- The command is wp
--func=FUNC \ <-- The function to examine in both programs
[options] \ <-- Any extra options
/path/to/exe1 \ <-- The path to the first program
/path/to/exe2 <-- The path to the second program
--check-null-derefs — Checks that the modified binary has no additional paths with null dereferences in comparison with the original binary.--check-invalid-derefs — Checks that the modified binary has no additional paths that result in dereferences to invalid memory locations. That is, all memory dereferences are either on the stack or heap. The stack is defined as the memory region above the current stack pointer, and the heap is defined as the memory region 0x256 bytes below the lowest address of the stack.--compare-func-calls — Checks that function calls do not occur in the modified binary if they have not occurred in the original binary.--compare-post-reg-values=<reg-list> — Compares the values stored in the registers specified in reg-list at the end of the function's execution. For example, RAX,RDI compares the values of RAX and RDI at the end of execution. If unsure about which registers to compare, check the architecture's ABI. x86_64 architectures place their output in RAX and ARM architectures place their output in R0.--user-func-specs-orig=<user-spec-list> — List of user-defined subroutine specifications to be used only for the original binary in comparative analysis. Usage: See --user-func-specs.
--user-func-specs-mod=<user-spec-list> — List of user-defined subroutine specifications to be used only for the modified binary in comparative analysis. Usage: See --user-func-specs.
--mem-offset — Maps the symbols in the data and bss sections from their addresses in the original binary to their addresses in the modified binary. If this flag is not present, WP assumes that memory between both binaries start at the same offsets.--rewrite-addresses — This flag is only used in a comparative analysis. Rewrites the concrete addresses in the modified binary to the same address in the original binary if they point to the same symbol. This flag should not be used in conjunction with the --mem-offset flag.--precond=<smt-lib-string> — Allows you to specify an assertion that WP will assume is true at the beginning of the function it is analyzing, using the smt-lib2 format. For comparative predicates, one may refer to variables in the original and modified programs by appending the suffix _orig and _mod to variable names in the smt-lib expression. For example, --precond="(assert (= RDI_mod #x0000000000000003)) (assert (= RDI_orig #x0000000000000003))". If no precondition is specified, a trivial precondition of true will be used.--postcond=<smt-lib-string> — Allows you to specify an assertion that WP will assume is true at the end of the function it is analyzing, using the smt-lib2 format. Similar to --precond, one may create comparative postconditions on variables by appending _orig and _mod to variable names. If no postcondition is specified, a trivial postcondition of true will be used.--func-name-map=<regex-orig>,<regex-mod> — Maps the subroutine names from the original binary to their names in the modified binary based on the regex from the user. Usage: --func-name-map="<regex for original name>,<regex for modified name>". For example: --func-name-map="\(.*\),foo_\1" means that all subroutines in the original binary have foo_ prepended in the modified binary. Multiple patterns can be used to map function names and are delimited with ';'s (i.e. <reg1_orig>,<reg1_mod>;<reg2_orig>,<reg2_mod>"). By default, WP assumes subroutines have the same names between the two binaries.smt-lib2 format. Here we provide a quick reference to commonly used features.
In the following, let E1, E2, and so on refer to SMTLIB expressions.
(assert E1)(and E1 E2)(or E1 E2)(=> E1 E2)(not E1)(= E1 E2)(not (= E1 E2))(+ E1 E2)(- E1 E2)(* E1 E2)(< E1 E2)(<= E1 E2)(> E1 E2)(>= E1 E2)(bvadd E1 E2)(bvsub E1 E2)(bvult E1 E2)(bvule E1 E2)(bvugt E1 E2)(bvuge E1 E2)(bvslt E1 E2)(bvsle E1 E2)(bvsgt E1 E2)(bvsge E1 E2)