Module Bap_wp.Environment

This module represents the environment of a BIR program and is used when determining pre-conditions.

It contains a Z3 context, a var_gen, the association between BIR variables and Z3 constants, preconditions for previously visited blocks, a mapping of Z3 variables to function calls during runtime, subroutine summaries, a handler for loop unrolling, and expression verification conditions.

module EnvMap = Bap.Std.Var.Map
module Constr = Constraint
module ExprSet : Core.Set.S with type Elt.t = Constr.z3_expr
module Unroll_depth = Bap.Std.Blk.Map
type t

The state type which is maintained when creating preconditions. It contains, among other things, summaries for subroutines, the associations between BIR variables and Z3 constants, and preconditions for already visited blocks, if relevant.

type var_gen

This type is used to create fresh variables when needed. It's internals should be irrelevant.

type fun_spec_type =
| Summary of t -> Constr.t -> Bap.Std.Tid.t -> Constr.t * t
| Inline

The type that specifies whether a fun_spec should calculate the precondition based off a summary or by inlining the function and visiting it with Precondition.visit_sub.

type fun_spec = {
spec_name : string;
spec : fun_spec_type;
}

Type that specifies what rules should be used when calculating the precondition of a subroutine.

type indirect_spec = t -> Constr.t -> Bap.Std.Exp.t -> bool -> Constr.t * t

Type that specifies what rules should be used when encountering an indirect call

type jmp_spec = t -> Constr.t -> Bap.Std.Tid.t -> Bap.Std.Jmp.t -> (Constr.t * t) option

Type that specifies what rules should be used when visiting a jump in a BIR program.

type int_spec = t -> Constr.t -> int -> Constr.t * t

Type that specifies what rules should be used when calculating the precondition of an interrupt.

type loop_handler = t -> Constr.t -> start:Bap.Std.Graphs.Ir.Node.t -> Bap.Std.Graphs.Ir.t -> t

The loop handling procedure for the appropriate blocks.

type cond =
| BeforeExec of Constr.goal
| AfterExec of Constr.goal

Condition generated when exploring an expression: BeforeExec will generate a Constr.goal to be added to the postcondition before any substitution is made, and AfterExec will generate the goal to be added after all substitutions are completed.

type cond_type =
| Verify of cond
| Assume of cond

Conditions generated when exploring an expression: if it is a Verify, this represents an additional proof obligation, an Assume represents an assumption, typically about the definedness of the expression.

type exp_cond = t -> Bap.Std.Exp.t -> cond_type option

Type that generates a Verification Condition on encountering a given pattern, typically a correctness constraint, like no overflow or no null dereference.

type mem_range = {
base_addr : int;
size : int;
}
type unroll_depth = int Unroll_depth.t

A map containing the current depth for a block when unrolling a loop.

type loop_invariants = string Bap.Std.Tid.Map.t
val init_loop_handler : default:loop_handler -> ( Bap.Std.Tid.t -> loop_handler option ) list -> loop_handler

init_loop_handler default handlers takes in a list of handlers that will be used when visiting a loop in the subroutine. The handler used is based off of the loop's tid.

val mk_env : subs:Bap.Std.Sub.t Bap.Std.Seq.t -> specs: ( Bap.Std.Sub.t -> Bap_core_theory.Theory.target -> fun_spec option ) list -> default_spec:( Bap.Std.Sub.t -> Bap_core_theory.Theory.target -> fun_spec ) -> indirect_spec:indirect_spec -> jmp_spec:jmp_spec -> int_spec:int_spec -> exp_conds:exp_cond list -> loop_handlers:( Bap.Std.Tid.t -> loop_handler option ) list -> default_loop_handler:loop_handler -> target:Bap_core_theory.Theory.target -> freshen_vars:bool -> use_fun_input_regs:bool -> stack_range:mem_range -> data_section_range:mem_range -> func_name_map:string Core.String.Map.t -> smtlib_compat:bool -> Z3.context -> var_gen -> t

Creates a new environment with

  • a sequence of subroutines in the program used to initialize function specs
  • a list of fun_specs that each summarize the precondition for its mapped function
  • the default fun_spec in the case a function does not satisfy the requirements of the other fun_specs
  • a indirect_spec for handling indirect calls
  • a jmp_spec for handling branches
  • an int_spec for handling interrupts
  • a list of exp_conds to satisfy
  • the number of times to unroll a loop
  • a loop handler that can unroll a loop or check a loop invariant
  • the target architecture of the binary
  • the option to freshen variable names
  • the option to use all input registers when generating function symbols at a call site
  • the concrete range of addresses of the stack
  • the concrete range of addresses of the data section
  • a Z3 context
  • and a variable generator.
val env_to_string : t -> string

Creates a string representation of the environment.

val mk_ctx : unit -> Z3.context

Create a Z3 context, used to generate every Z3 expression. Simply defined as Z3.mk_context [].

val mk_var_gen : unit -> var_gen

Create a new variable generator. Two fresh variables created with the same generator will be distinct.

val get_fresh : ?name:string -> var_gen -> string

Get a fresh variable name, possibly prefixed by a given name string.

val set_freshen : t -> bool -> t

Set variable freshening, which will cause constraint generation to create fresh variables.

val freshen : ?name:( string -> string ) -> Constr.t -> t -> Bap.Std.Var.Set.t -> Constr.t * t

freshen ~name constr env vars creates fresh names for vars found in constr. Optionally takes in name, which is a function that maps the original variable name to the fresh name. Defaults to fresh_var.

val add_call_pred : t -> Constr.z3_expr -> t

Add a z3 expression representing a function call predicate generated during the analysis to the environment.

val clear_call_preds : t -> t

Removes all z3 expressions representing function call predicates from the environment. This is used because the initial pass through a binary generates predicates that are not used during precondition computation.

val add_var : t -> Bap.Std.Var.t -> Constr.z3_expr -> t

Add a new binding to the environment for a bap variable to a Z3 expression, typically a constant.

val remove_var : t -> Bap.Std.Var.t -> t

Remove a binding in the environment for a bap variable.

val find_var : t -> Bap.Std.Var.t -> Constr.z3_expr option

Looks up the Z3 variable that represents a BIR variable.

val add_precond : t -> Bap.Std.Tid.t -> Constr.t -> t

Add a precondition to be associated to a block b to the environment.

val mk_exp_conds : t -> Bap.Std.Exp.t -> cond_type list

Creates a list of assumptions and verification conditions as hooks on an expression being visited during analysis.

val get_context : t -> Z3.context

Obtains the Z3 context within a given environment.

val get_var_gen : t -> var_gen

Obtains the var_gen used to create fresh variables within a given environment.

val get_subs : t -> Bap.Std.Sub.t Bap.Std.Seq.t

Obtains the sequence of subroutines that belongs to a BIR program.

val get_var_map : t -> Constr.z3_expr EnvMap.t

Obtains the var_map containing a mapping of BIR variables to Z3 variables.

val get_init_var_map : t -> Constr.z3_expr EnvMap.t

Obtains the var_map containing a mapping of BIR variables to the Z3 variables that represent their initial states.

val get_var : t -> Bap.Std.Var.t -> Constr.z3_expr * t

Looks up the Z3 variable that represents a BIR variable. Produces fresh z3_expr if not found.

val get_precondition : t -> Bap.Std.Tid.t -> Constr.t option

Looks up the precondition for a given block in the environment. Currently returns True if the block is not yet visited.

val get_sub_name : t -> Bap.Std.Tid.t -> string option

Looks up the subroutine's name given its tid.

val get_fun_name_tid : t -> string -> Bap.Std.Tid.t option

Finds the tid of a function in the environment.

val get_called : t -> Bap.Std.tid -> string option

Look up the string name for the variable which represents a call made to a subroutine with a given tid.

val get_sub_handler : t -> Bap.Std.Tid.t -> fun_spec_type option

Looks up the specification of a subroutine that is used to calculate the precondition of a function call.

val get_indirect_handler : t -> Bap.Std.Exp.t -> indirect_spec

Looks up the indirect call spec for an expression. Used to calculate the precondition of an indirect call.

val get_jmp_handler : t -> jmp_spec

Looks up the list of jmp_specs that is used to calculate the precondition of jumps in a BIR program.

val set_jmp_handler : t -> jmp_spec -> t

Updates the list of jmp_specs used to calculate the precondition of jumps in a BIR program.

val get_int_handler : t -> int_spec

Looks up the specification of calculating the precondition of an interrupt.

val get_loop_handler : t -> t -> Constr.t -> start:Bap.Std.Graphs.Ir.Node.t -> Bap.Std.Graphs.Ir.t -> t

Finds the loop_handler that is used to unroll loops when it is visited in the BIR program.

val get_target : t -> Bap_core_theory.Theory.target

Obtains the target architecture of the program.

val get_gprs : t -> Bap.Std.Var.Set.t

Obtains the general purpose registers of the target architecture of the program.

val get_sp : t -> Bap.Std.Var.t

Obtains the name of the program's stack pointer

val get_mem : t -> Bap.Std.Var.t

Obtains the BAP variable representing a program's memory.

val get_all_target_vars : t -> Bap.Std.Var.Set.t

Obtain the set of all registers and memories for the target.

val get_call_preds : t -> ExprSet.t

Obtains a list of all the Constr.z3_exprs that represents function call predicates that were generated during analysis.

val fold_fun_tids : t -> init:'a -> f:( key:string -> data:Bap.Std.Tid.t -> 'a -> 'a ) -> 'a

Performs a fold on the map of of function names to tids to generate a Constr.z3_expr.

val is_x86 : Bap_core_theory.Theory.target -> bool

Checks if the target is part of the x86 family.

val use_input_regs : t -> bool

Checks to see if the environment supports using all possible input registers when generating symbols in the function specs at a function call site.

val get_smtlib_compat : t -> bool

Determine whether to generate constraints that are smtlib compatible or using optimizations that are Z3 specific. Put to true if using external smt solver

val in_stack : t -> Constr.z3_expr -> Constr.z3_expr

in_stack env addr is the constraint STACK_MIN < addr <= STACK_MAX as defined by the concrete range of the stack in the env.

val get_stack_end : t -> int

get_stack_end retrieves the address of the largest address that the top of the stack can take. It is assumed the stack grows downwards, from high addresss to low address. The top and start of the stack is defined as stack_base and is the largest address in the stack. The stack end (retrieved by this function) is the smallest value that the stack pointer can take.

val in_data_section : t -> Constr.z3_expr -> Constr.z3_expr

in_data_section env addr is the constraint DATA_MIN <= addr < DATA_MAX as defined by the concrete range of the data section in the env.

val init_stack_ptr : t -> Constr.z3_expr -> Constr.z3_expr

init_stack_ptr env ptr initializes the constraint STACK_MIN + 128 < sp <= STACK_MAX which is the region of the stack that the stack pointer may point to at the beginning of a subroutine. The 128 is based off of the 128 bytes of red zone underneath the stack pointer in x86_64.

val update_stack_base : mem_range -> int -> mem_range

update_stack_base range base updates the highest address of the stack to be the same value as base.

val update_stack_size : mem_range -> int -> mem_range

update_stack_size range size updates the size of the stack to be the same value as size.

val mk_init_var : t -> Bap.Std.Var.t -> Constr.z3_expr * t

mk_init_var env var creates a fresh Z3 variable that represents the initial state of variable var. Adds a new binding to env for the bap variable to is generated init variable.

val get_init_var : t -> Bap.Std.Var.t -> Constr.z3_expr option

get_init_var var obtains the Z3 expression that represents the initial state of a bap variable var.

val map_sub_name : t -> string -> string

map_sub_name env name_mod obtains the name of the subroutine in the original binary based off its name in the modified binary. In the case there is no mapping for the subroutine, get_sub_name will return name_mod (when calling this function from the original binary.

val get_unroll_depth : t -> Bap.Std.Blk.t -> int option

get_unroll_depth env node obtains the unroll depth for node when unrolling a loop.

val set_unroll_depth : t -> Bap.Std.Blk.t -> f:( int option -> int ) -> t

set_unroll_depth env node depth updates the map with the new unroll depth for node.

val mk_z3_expr : Z3.context -> name:string -> typ:Bap.Std.Type.t -> Constr.z3_expr

Create a constant Z3 expression of a type that corresponds to a bap type, where the correspondence is as follows:

  • BitVector of width w -> BitVector of width w
  • Memory value with address size a and word size w -> Functional array from BitVector a to BitVector w.
val new_z3_expr : ?name:string -> t -> Bap.Std.Type.t -> Constr.z3_expr

Create a Z3 constant of the appropriate name and type, but ensure that the constant is "fresh" with the Environment.var_gen.