value_analysis

value_reg_edge(EA:address, Reg:register, EA_reg1:address, Reg1:register, Multiplier:number, Offset:number)

This module performs a basic value analysis.

The value of a register at a point (ea) is expressed as the value of another at another point (EA_reg1) multiplied by a multiplier plus an offset:

val(Reg,EA) = val(Reg1,EA_reg1)* Multiplier+ Offset

In some cases we can obtain a term of the form:

  • val(Reg,EA) = Offset

If we can obtain that the register is assigned a constant

  • val(Reg,EA) = Unknown * Multiplier+ Offset

If we detect a loop where the register gets incremented ‘Multiplier’ in each iteration

The analysis first computes value_reg_edge which are facts of the form above defined for different instruction and using the def-use chains.

Then, we have a propagation phase where value_reg is computed. This phase chains individual value_reg_edge together. In addition to chaining edges together it takes care of cases such as two registers added together or substracted if it turns out that they can be expressed in terms of the same register. It also detects possible loops.

This propagation is limited in the number of steps using step_limit to ensure termination and efficiency.

As a result, we might obtain more than one ‘value’ for a certain register at a certain location. best_value_reg selects only one of these values prioritizing the two special cases from above (constant or loop) and considering the value with most steps.

value_reg(EA:address, Reg:register, EA_reg1:address, Reg1:reg_nullable, Multiplier:number, Offset:number, Steps:unsigned)

best_value_reg(EA:address, Reg:register, EA_from:address, Multiplier:number, Offset:number, type:symbol)

bshru_wrapper(Lhs:number, Rhs:number, Res:number)

For logical right shift in 32-bit ISA, the LHS value’s upper 32-bit needs to be masked out.

WARNING: Predicate not present in compiled Datalog program (Dead Code)

value_reg_unsupported(EA:address, Reg:register)

A register is defined using an unknown value This predicate is used to create trivial leaf edges in the value_reg graph step_limit .

step_limit(Limit:unsigned)

reg_reg_arithmetic_operation_defs(EA:address, Reg_def:register, EA_def1:address, Reg1:register, EA_def2:address, Reg2:register, Mult:number, Offset:number)

This is an auxiliary predicate used for computing value_reg. It captures an instruction at EA that defines register Reg_def by operating with two register Reg1 and Reg2 defined at EA_def1 and EA_def1.

The operation is Reg_def = Reg1 + Reg2 * Mult + Offset.

value_reg_max_mult(EA:address, Reg:register, MaxMult:number)

const_value_reg_used(UsedEA:address, EADef:address, EARegDef:address, Reg:register, Value:number)

A constant value is used in a data access.

EADef: The address where Value was originally defined (which may not necessarily be where Reg is defined, if that value is moved to a different register later).

EARegDef: The address where Reg is defined as Value. Often EADef = EARegDef.

value_reg_address_before(EA:address, Reg:register, AddrValue:number, Steps:unsigned)

AddrValue represents the value of register Reg before EA. The value should be an address.