Symbolic Execution

Symbolic execution explores lifted LowUIR with SymbExpr values and optional solver-backed reachability or satisfiability queries.

Sources:

• B2R2/src/MiddleEnd/SymbEval/SymbExecutor.fs
• B2R2/src/MiddleEnd/SymbEval/SymbStateAccessor.fs
• B2R2/src/MiddleEnd/SymbEval/SymbExpr.fs
• B2R2/src/MiddleEnd/SymbEval/ISolver.fs
• B2R2/src/MiddleEnd/SymbEval/SymbModel.fs
• B2R2/src/MiddleEnd/SymbEval/SymbCallHook.fs

SymbExecutor

API	Meaning
SymbExecutor(hdl)	Create a symbolic executor for a binary.
CreateState()	Create a SymbState with BinSectionBackedMemory and no initial registers.
CreateState(options)	Create a state with explicit StateCreationOptions<ISymbMemory, SymbExpr>.
Run(start, state, options)	Run with SymbRunOptions.
Run(start, state, calls, query, solver)	Convenience overload using call policy, query request, and solver.

State Creation

CreateState(options) accepts StateCreationOptions<ISymbMemory, SymbExpr>.

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

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

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

Queries and Avoids

API	Meaning
ReachAddress target	Ask if execution can reach an address.
ReachState predicate	Ask if execution can reach a state predicate.
SatisfyAddress target	Ask for concrete symbolic-input values reaching an address.
SatisfyState predicate	Ask for concrete symbolic-input values reaching a state predicate.
AvoidAddresses addrs	Discard states whose PC reaches any address in the set.
AvoidState predicate	Discard states matching a predicate.
NoSolver	Run without solver support.
CustomSolver solver	Use an ISolver implementation.

Use SymbQueryRequest when the query also needs model values. This is the form used by the loginme solution to ask the solver for concrete bytes of a symbolic input buffer.

type SymbQueryRequest =
  { Query: SymbQuery
    QueryValues: IQueryExpr }

Field	Meaning
Query	Reachability or satisfiability query, such as SatisfyAddress endAddr.
QueryValues	Symbolic expressions or buffers to extract from the solver model.

QueryValues accepts any IQueryExpr. SymbByteBuffer implements IQueryExpr, so a buffer returned by SetArgumentSymbolicString can be used directly.

let buf = accessor.SetArgumentSymbolicString(0, "password")

let query =
  { Query = SatisfyAddress endAddr
    QueryValues = buf }

Run Options

SymbRunOptions.Default(query) creates a bounded default with no solver. SymbRunOptions.Default(query, solver) uses a solver. Defaults are FollowDirectInternalCalls, MaxDepth = 500, MaxStates = 4096, LoopBound = 1, RunTimeout = 30000, path pruning disabled, and stop at first answer enabled.

Member	Meaning
AddQueryValue value / AddQueryValues values	Add symbolic values to model extraction.
WithQueryValues values	Replace model extraction values with a sequence or IQueryExpr.
AddQueryBuffer buffer / AddQueryBuffers buffers	Add symbolic byte buffers to model extraction.
AddAvoidAddress addr / AddAvoidAddresses addrs	Add addresses to avoid.
WithAvoidAddresses addrs	Replace the avoid set.
WithAvoid avoid / AddAvoid avoid	Set or combine avoid conditions.
AddAvoidState predicate	Add a predicate-based avoid condition.
StopAtCalls()	Stop before calls.
FollowDirectInternalCalls()	Follow direct internal calls.
WithCallHooks hooks	Use a prepared hook registry.
RegisterCallHook(target, hook) / RegisterCallHooks hooks	Register symbolic call hooks.
WithSolver solver	Replace the solver backend.
EnablePathPruning() / DisablePathPruning()	Toggle solver-backed path pruning.
EnableStopAtFirstAnswer() / DisableStopAtFirstAnswer()	Toggle early stop after an answer.
WithWarmUpRanges ranges	Pre-lift half-open address ranges [start, finish).

Run Result

Result	Meaning
Reachable answers	One or more states reached the target.
Unreachable	No explored state reached the target.
Satisfiable answers	One or more concrete assignments satisfy the query.
Unsatisfiable	No explored assignment satisfies the query.
Unknown failures	Execution stopped or pruned before a complete answer.
TimedOut(timeout, result)	Timeout with a partial result.

SymbSatisfiabilityAnswer.Model wraps solver values in SymbModel. SymbRunResult.GetSatisfiabilityAnswer() returns the first satisfiability answer or raises if none is available.

Common stop reasons are StoppedAtCall, DepthLimitReached, StateLimitReached, InvalidInstructionStopped, SideEffectStopped, EvaluationFailed, MissingSolverForQuery, SolverQueryFailed, and RunTimeoutReached. Common prune reasons are AvoidedAddress, AvoidedState, LoopBoundReached, InfeasiblePath, and SolverPruningFailed.

SymbStateAccessor

API	Meaning
SymbStateAccessor(hdl, state)	Linux ABI accessor.
SymbStateAccessor(hdl, state, os)	Accessor for a specific OS.
DefaultStringBound	Default symbolic C-string payload length: 64.
DefaultStackTop	Default stack top: 0x7fffffffe000UL.
State	Underlying SymbState.
WordType / WordBytes	Target word type and byte width.
StackPointer	Current concrete stack pointer value.
WordValue(addr)	Create a concrete word-sized SymbExpr.
CreateSymbolicBytes(name, length)	Create symbolic byte variables without writing memory.
TryGetConcreteRegister rid	Read a register as a concrete address, returning Result.
TryGetStackPointer() / TrySetStackPointer addr	Stack pointer access without throwing when unavailable.
TryPushToStack value / TryPopFromStack()	Stack operations returning Result.
WriteSymbolicBuffer(name, addr, length)	Write symbolic bytes at addr.
WriteSymbolicBuffer(name, addr, length, nullTerminate)	Write symbolic bytes and optionally append a null byte.
AllocateSymbolicBuffer(name, length)	Allocate stack space and write symbolic bytes.
AllocateSymbolicBuffer(name, length, nullTerminate)	Allocate symbolic bytes with optional null termination.
SetArgumentBuffer(idx, buffer)	Set an argument register to the buffer address.
AllocateSymbolicString(name) / AllocateSymbolicString(name, maxLength)	Allocate a null-terminated symbolic string.
SetArgumentSymbolicString(idx, name) / SetArgumentSymbolicString(idx, name, maxLength)	Allocate a symbolic string and pass it as an argument.

Shared State Accessor Members

SymbStateAccessor 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 symbolic register value by architecture register name.
SetRegister(rid, value) / GetRegister(rid)	Write or read a symbolic 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.

SymbByteBuffer

Field or member	Meaning
Name	Prefix used for byte variable names.
Address	Concrete start address.
Bytes	Symbolic bytes in address order.
NullTerminated	True when a null byte was written after the symbolic bytes.
Values	Same bytes, ready for query extraction.

SymbByteBuffer implements IQueryExpr, so it can be passed through AddQueryBuffer or combined with other query expressions.

Symbolic Expressions and Query Values

API	Meaning
SymbExpr	Symbolic bit-vector expression: Const, Var, UnOp, BinOp, RelOp, Load, Ite, Cast, Extract, FuncApp, or Undef.
SymbExpr.zero typ / one typ	Concrete zero/one symbolic expressions.
SymbExpr.trueExpr / falseExpr	1-bit LowUIR condition constants.
SymbExpr.relop op lhs rhs	Build a relational path-condition expression.
IQueryExpr.QueryValues	Expressions requested from a solver model.
QueryExpr.Empty	Request no model values.
QueryExpr.Value expr	Request one symbolic expression value.
QueryExpr.Values exprs	Combine multiple query expressions.

SymbRunOptions.Default(queryRequest, solver) copies queryRequest.QueryValues into the run options. The convenience overload executor.Run(start, state, calls, queryRequest, solver) uses the same request shape.

Solvers and Models

API	Meaning
ISolver.CheckSat smt2	Run a satisfiability check over an SMT-LIB2 assertion script.
ISolver.GetModels smt2	Return a raw solver model for an SMT-LIB2 assertion script.
SolverStatus	Parsed solver status: Sat, Unsat, or Unknown.
SolverValue	One named BitVector value returned by a solver.
SymbModel.Values	Raw solver values.
SymbModel.TryGetValue name / GetValue name	Read a named model value.
SymbModel.GetByte name / GetByte expr	Read a model value as a byte.
SymbModel.ReadBytes values / ReadBytes buffer	Materialize symbolic bytes.
SymbModel.ReadCString values / ReadCString buffer	Materialize a null-terminated ASCII string.

Call Hooks

API	Meaning
SymbCallContext	Hook context: call site, target, return address, word type, endian, argument registers, and return register.
SymbCallHook	Function type: SymbCallContext -> SymbState -> Result<SymbState list, SymbEvalError>.
SymbCallHookRegistry()	Empty hook registry.
SymbCallHookRegistry(hooks)	Registry initialized from target-hook pairs.
Register(target, hook)	Return a registry with one hook added.
RegisterMany hooks	Return a registry with many hooks added.
TryFind target	Look up a hook by concrete target address.
SymbCallHooks.strlen	Built-in bounded symbolic model for strlen.
SymbCallHooks.strlenBounded maxScan	Same model with an explicit scan bound.

Example

let executor = SymbExecutor hdl
let state = executor.CreateState()
let accessor = SymbStateAccessor(hdl, state)

accessor.InitializeDefaultStack()
accessor.SetArgumentSymbolicString(0, "input", 16) |> ignore

let options =
  SymbRunOptions.Default(ReachAddress 0x401080UL)
    .WithAvoidAddresses [ 0x401050UL ]

match executor.Run(0x401000UL, state, options) with
| Reachable answers ->
  answers
  |> List.iter (fun answer ->
    printfn "reachable at 0x%x" answer.Target)
| result ->
  printfn "%A" result