Concrete Execution

Concrete execution evaluates lifted LowUIR with concrete BitVector values.

Sources:

• B2R2/src/MiddleEnd/ConcEval/ConcExecutor.fs
• B2R2/src/MiddleEnd/ConcEval/ConcStateAccessor.fs

ConcExecutor

API	Meaning
ConcExecutor(hdl)	Create a concrete executor for a binary.
CreateState()	Create an EvalState with BinSectionBackedMemory and no initial registers.
CreateState(options)	Create an EvalState with explicit StateCreationOptions<IMemory, BitVector>.
Run(start, state, options)	Run with ConcRunOptions<EvalState>.
Run(start, state, stopCondition)	Run with default options plus one stop condition.

State Creation

CreateState(options) accepts StateCreationOptions<IMemory, BitVector>.

type StateCreationOptions<'Memory, 'Value> =
  { Memory: InitialMemory<'Memory>
    Registers: (RegisterID * 'Value)[] }

Initial memory	Meaning
EmptyMemory	Start from an empty memory object.
PreinitializedMemory memory	Start from a caller-provided memory object.
BinSectionBackedMemory	Back memory reads with loaded binary sections.

Initial registers are passed as (RegisterID * BitVector)[].

Stop Conditions

Condition	Meaning
StopAtAddress addr	Stop before executing addr.
StopAfterAddress addr	Stop after executing addr.
StopAtReturn	Stop before a return instruction is evaluated.
StopAfterReturn	Stop after a return instruction is evaluated.
StopAtCall	Stop when a call instruction is observed.
StopAtSideEffect	Stop when a LowUIR side-effect statement is observed.
StopAfterInstructionCount count	Stop after count machine instructions.
StopOnEvaluationError	Present in the API. The current executor stops on evaluation errors regardless of whether this condition is supplied.
StopWhen predicate	Stop when a predicate over ConcStopPoint<'State> returns true.

Run Options

Field	Values
Calls	StopAtCalls, FollowDirectInternalCalls, UseCallHooks
UndefinedValues	StopOnUndefinedValue, IgnoreUndefinedWrites
UninitializedRegisters	StopOnUninitializedRegister, ZeroCallerContext, ZeroAnyRegister
StopConditions	ConcStopCondition<EvalState> list

ConcRunOptions.Default stopCondition and ConcRunOptions.Default stopConditions create bounded defaults. The default follows direct internal calls, ignores undefined writes, zeroes caller-context registers on first read, and adds StopAfterInstructionCount 50000.

Caution

ConcStopCondition.StopOnEvaluationError is present in the API, but the current ConcExecutor stops on expression or statement evaluation failure even when this condition is not supplied.

Caution

ConcCallPolicy.UseCallHooks is present in the API, but call-hook dispatch is not implemented yet in the current ConcExecutor source. Use StopAtCalls or FollowDirectInternalCalls for concrete workflows.

Run Result

Field or member	Meaning
StopReasons	One or more ConcStopReason values.
FinalAddress	Final instruction address or PC.
InstructionCount	Executed machine instruction count.
State	Final EvalState.
IsStoppedAtAddress addr	Convenience check for StoppedAtAddress addr.

Stop reasons include StoppedAtAddress, StoppedAfterAddress, StoppedAtReturn, StoppedAfterReturn, StoppedAtCall, StoppedAtSideEffect, UndefinedValue, InstructionLimitReached, EvaluationError, UserStopConditionMet, and InvalidInstructionAddress.

ConcStateAccessor

API	Meaning
ConcStateAccessor(hdl, state)	Linux ABI accessor.
ConcStateAccessor(hdl, state, os)	Accessor for a specific OS.
DefaultStackTop	Default stack top: 0x7fffffffe000UL.
State	Underlying EvalState.
WordType / WordBytes	Target word type and byte width.
StackPointer	Current stack pointer value.
WordValue(value)	Create a word-sized BitVector.
InitializeDefaultStack()	Set the stack pointer to DefaultStackTop.
PushPointer(value) / PopPointer()	Push or pop an address-sized pointer.
WritePointer(addr, value) / ReadPointer(addr)	Write or read an address-sized pointer in target endian.
WriteInteger(addr, value, typ)	Store an integer with an explicit RegType.
WriteBytes(addr, bytes) / ReadBytes(addr, length)	Write or read concrete bytes.
ReadCString(addr, maxLength)	Read a null-terminated ASCII string from executor memory.

Shared State Accessor Members

ConcStateAccessor also exposes common state-accessor members for registers, arguments, return values, and stack buffers.

API	Meaning
SetStackPointer(addr)	Set the stack pointer register.
InitializeStack(stackTop)	Initialize the stack pointer to an explicit address.
InitializeFramePointer()	Initialize the frame pointer from the current stack pointer.
SetRegister(name, value) / GetRegister(name)	Write or read a register value by architecture register name.
SetRegister(rid, value) / GetRegister(rid)	Write or read a register value by RegisterID.
ZeroRegisters(names: string[]) / ZeroRegisters(rids: RegisterID[])	Clear selected registers to zero values.
SetArgument(index, value)	Set the ABI argument register at index.
GetReturnValue()	Read the ABI return register.
AllocateStackBuffer(size)	Reserve stack space and return its address.
PushToStack(value) / PopFromStack()	Push or pop a word-sized value.

Register-name helpers are useful for architecture-specific setup, such as setting R0/LR for ARM or A0/RA/NPC for MIPS.

accessor.SetRegister("A0", accessor.WordValue buf)
accessor.SetRegister("RA", accessor.WordValue endAddr)

Example

let executor = ConcExecutor hdl
let state = executor.CreateState()
let accessor = ConcStateAccessor(hdl, state)

accessor.InitializeDefaultStack()
accessor.SetArgument(0, accessor.WordValue 0x1234UL)

let result =
  executor.Run(0x401000UL, state,
               ConcRunOptions.Default [ StopAfterReturn ])

printfn "stopped at 0x%x after %d instructions"
  result.FinalAddress result.InstructionCount

let resultAccessor = ConcStateAccessor(hdl, result.State)
printfn "return value = %A"
  (resultAccessor.GetReturnValue())