Module Bap_wp.Output

This module exports types and utilities to process and report results found using the WP plugin.

The report contains information about the result of the WP analysis, and in the case the result is SAT, prints out the model that contains the input register and memory values that result in the program refuting a goal, the path taken to the refuted goal, and the register values at each jump in the path.

module Env = Environment
module Constr = Constraint
val print_result : ?fmt:Stdlib.Format.formatter -> Z3.Solver.solver -> Z3.Solver.status -> Constr.t -> show:string list -> orig:Bap.Std.sub Compare.code -> modif:Bap.Std.sub Compare.code -> unit

Prints out the result from check, and if the result is SAT, generate a model that represents the registers and memory values that lead to a specific program state, a list of goals that have been refuted, and if specified, the paths that lead to the refuted goals.

val output_gdb : Z3.Solver.solver -> Z3.Solver.status -> Env.t -> func:string -> filename:string -> unit

Prints to file a gdb script that will fill the appropriate registers with the countermodel

val output_bildb : Z3.Solver.solver -> Z3.Solver.status -> Env.t -> string -> unit

output_bildb solver status env file prints to a YAML file that will fill the appropriate registers with the values found in the countermodel in the case the analysis returns SAT. This is used to initialize the BilDB plugin.

type mem_model = {
default : Constr.z3_expr;
model : (Constr.z3_expr * Constr.z3_expr) list;
}

mem_model The default value stores the final else branch of a memory model. The model holds an association list of addresses and values held at those adresses.

val extract_array : Constr.z3_expr -> mem_model

extract_array takes a z3 expression that is a sequence of stores and converts it into a mem_model, which consists of a key/value association list and a default value