These may be enabled by passing mode=xxx to a state constructor.
| Mode name | Description |
|---|---|
symbolic |
The default mode. Useful for most emulation and analysis tasks. |
symbolic_approximating |
Symbolic mode, but enables approximations for constraint solving. |
static |
A preset useful for static analysis. The memory model becomes an abstract region-mapping system, "fake return" successors skipping calls are added, and more. |
fastpath |
A preset for extremely lightweight static analysis. Executing will skip all intensive processing to give a quick view of the behavior of code. |
tracing |
A preset for attempting to execute concretely through a program with a given input. Enables unicorn, enables resilience options, and will attempt to emulate access violations correctly. |
These are sets of options, found as angr.options.xxx.
| Set name | Description |
|---|---|
common_options |
Options necessary for basic execution |
symbolic |
Options necessary for basic symbolic execution |
resilience |
Options that harden angr's emulation against unsupported operations, attempting to carry on by treating the result as an unconstrained symbolic value and logging the occasion to state.history.events. |
refs |
Options that cause angr to keep a log of all the memory, register, and temporary references complete with dependency information in history.actions. This option consumes a lot of memory, so be careful! |
approximation |
Options that enable approximations of constraint solves via value-set analysis instead of calling into z3 |
simplification |
Options that cause data to be run through z3's simplifiers before it reaches memory or register storage |
unicorn |
Options that enable the unicorn engine for executing on concrete data |
These are individual option objects, found as angr.options.XXX.
| Option name | Description | Sets | Modes | Implicit adds |
|---|---|---|---|---|
ABSTRACT_MEMORY |
Use SimAbstractMemory to model memory as discrete regions |
static |
||
ABSTRACT_SOLVER |
Allow splitting constraint sets during simplification | static |
||
ACTION_DEPS |
Track dependencies in SimActions | |||
APPROXIMATE_GUARDS |
Use VSA when evaluating guard conditions | |||
APPROXIMATE_MEMORY_INDICES |
Use VSA when evaluating memory indices | approximation |
symbolic_approximating |
|
APPROXIMATE_MEMORY_SIZES |
Use VSA when evaluating memory load/store sizes | approximation |
symbolic_approximating |
|
APPROXIMATE_SATISFIABILITY |
Use VSA when evaluating state satisfiability | approximation |
symbolic_approximating |
|
AST_DEPS |
Enables dependency tracking for all claripy ASTs | During execution | ||
AUTO_REFS |
An internal option used to track dependencies in SimProcedures | During execution | ||
AVOID_MULTIVALUED_READS |
Return a symbolic value without touching memory for any read that has a symbolic address | fastpath |
||
AVOID_MULTIVALUED_WRITES |
Do not perfrom any write that has a symbolic address | fastpath |
||
BEST_EFFORT_MEMORY_STORING |
Handle huge writes of symbolic size by pretending they are actually smaller | static, fastpath |
||
BREAK_SIRSB_END |
Debug: trigger a breakpoint at the end of each block | |||
BREAK_SIRSB_START |
Debug: trigger a breakpoint at the start of each block | |||
BREAK_SIRSTMT_END |
Debug: trigger a breakpoint at the end of each IR statement | |||
BREAK_SIRSTMT_START |
Debug: trigger a breakpoint at the start of each IR statement | |||
BYPASS_ERRORED_IRCCALL |
Treat clean helpers that fail with errors as returning unconstrained symbolic values | resilience |
fastpath, tracing |
|
BYPASS_ERRORED_IROP |
Treat operations that fail with errors as returning unconstrained symbolic values | resilience |
fastpath, tracing |
|
BYPASS_UNSUPPORTED_IRCCALL |
Treat unsupported clean helpers as returning unconstrained symbolic values | resilience |
fastpath, tracing |
|
BYPASS_UNSUPPORTED_IRDIRTY |
Treat unsupported dirty helpers as returning unconstrained symbolic values | resilience |
fastpath, tracing |
|
BYPASS_UNSUPPORTED_IREXPR |
Treat unsupported IR expressions as returning unconstrained symbolic values | resilience |
fastpath, tracing |
|
BYPASS_UNSUPPORTED_IROP |
Treat unsupported operations as returning unconstrained symbolic values | resilience |
fastpath, tracing |
|
BYPASS_UNSUPPORTED_IRSTMT |
Treat unsupported IR statements as returning unconstrained symbolic values | resilience |
fastpath, tracing |
|
BYPASS_UNSUPPORTED_SYSCALL |
Treat unsupported syscalls as returning unconstrained symbolic values | resilience |
fastpath, tracing |
|
BYPASS_VERITESTING_EXCEPTIONS |
Discard emulation errors during veritesting | resilience |
fastpath, tracing |
|
CACHELESS_SOLVER |
enable SolverCacheless |
|||
CALLLESS |
Emulate call instructions as an unconstraining of the return value register | |||
CGC_ENFORCE_FD |
CGC: make sure all reads and writes go to stdin and stdout, respectively | |||
CGC_NON_BLOCKING_FDS |
CGC: always report "data available" in fdwait | |||
CGC_NO_SYMBOLIC_RECEIVE_LENGTH |
CGC: always read the maximum amount of data requested in the receive syscall | |||
COMPOSITE_SOLVER |
Enable SolverComposite for independent constraint set optimization |
symbolic |
all except static |
|
CONCRETIZE |
Concretize all symbolic expressions encountered during emulation | |||
CONCRETIZE_SYMBOLIC_FILE_READ_SIZES |
Concreteize the sizes of file reads | |||
CONCRETIZE_SYMBOLIC_WRITE_SIZES |
Concretize the sizes of symbolic writes to memory | |||
CONSERVATIVE_READ_STRATEGY |
Do not use SimConcretizationStrategyAny for reads; in case of read address concretization failures, return an unconstrained symbolic value | |||
CONSERVATIVE_WRITE_STRATEGY |
Do not use SimConcretizationStrategyAny for writes; in case of write address concretization failures, treat the store as a no-op | |||
CONSTRAINT_TRACKING_IN_SOLVER |
Set track=True for making claripy Solvers; enable use of unsat_core |
|||
COW_STATES |
Copy states instead of mutating the initial state directly | common_options |
all | |
DOWNSIZE_Z3 |
Downsize the claripy solver whenever possible to save memory | |||
DO_CCALLS |
Perform IR clean calls | symbolic |
all except fastpath |
|
DO_GETS |
Perform IR register reads | common_options |
all | |
DO_LOADS |
Perform IR memory loads | common_options |
all | |
DO_OPS |
Perform IR computation operations | common_options |
all | |
DO_PUTS |
Perform IR register writes | common_options |
all | |
DO_RET_EMULATION |
For each Ijk_Call successor, add a corresponding Ijk_FakeRet successor |
static, fastpath |
||
DO_STORES |
Perform IR memory stores | common_options |
all | |
EFFICIENT_STATE_MERGING |
Keep in memory any state that might be a common ancestor in a merge | Veritesting | ||
ENABLE_NX |
When in conjunction with STRICT_PAGE_ACCESS, raise a SimSegfaultException on executing non-executable memory |
Automatically if supported | ||
EXCEPTION_HANDLING |
Ask all SimExceptions raised during execution to be handled by the SimOS | tracing |
||
FAST_MEMORY |
Use SimFastMemory for memory storage |
|||
FAST_REGISTERS |
Use SimFastMemory for register storage |
fastpath |
||
INITIALIZE_ZERO_REGISTERS |
Treat the initial value of registers as zero instead of unconstrained symbolic | unicorn |
tracing |
|
KEEP_IP_SYMBOLIC |
Don't try to concretize successor states with symbolic instruction pointers | |||
KEEP_MEMORY_READS_DISCRETE |
In abstract memory, handle failed loads by returning a DCIS? | |||
LAZY_SOLVES |
Don't check satisfiability until absolutely necessary | |||
MEMORY_SYMBOLIC_BYTES_MAP |
Maintain a mapping of symbolic variable to which memory address it "really" corresponds to, at the paged memory level? | |||
NO_SYMBOLIC_JUMP_RESOLUTION |
Do not attempt to flatten symbolic-ip successors into discrete targets | fastpath |
||
NO_SYMBOLIC_SYSCALL_RESOLUTION |
Do not attempt to flatten symbolic-syscall-number successors into discrete targets | fastpath |
||
OPTIMIZE_IR |
Use LibVEX's optimization | common_options |
all | |
REGION_MAPPING |
Maintain a mapping of symbolic variable to which memory region it corresponds to, at the abstract memory level | static |
||
REPLACEMENT_SOLVER |
Enable SolverReplacement |
|||
REVERSE_MEMORY_HASH_MAP |
Maintain a mapping from AST hash to which addresses it is present in | |||
REVERSE_MEMORY_NAME_MAP |
Maintain a mapping from symbolic variable name to which addresses it is present in, required for memory.replace_all |
static |
||
SIMPLIFY_CONSTRAINTS |
Run added constraints through z3's simplifcation | |||
SIMPLIFY_EXIT_GUARD |
Run branch guards through z3's simplification | |||
SIMPLIFY_EXIT_STATE |
Perform simplification on all successor states generated | |||
SIMPLIFY_EXIT_TARGET |
Run jump/call/branch targets through z3's simplification | |||
SIMPLIFY_EXPRS |
Run the results of IR expressions through z3's simplification | |||
SIMPLIFY_MEMORY_READS |
Run the results of memory reads through z3's simplification | |||
SIMPLIFY_MEMORY_WRITES |
Run values stored to memory through z3's simplification | simplification, common_options |
symbolic, symbolic_approximating, tracing |
|
SIMPLIFY_REGISTER_READS |
Run values read from registers through z3's simplification | |||
SIMPLIFY_REGISTER_WRITES |
Run values written to registers through z3's simplification | simplification, common_options |
symbolic, symbolic_approximating, tracing |
|
SIMPLIFY_RETS |
Run values returned from SimProcedures through z3's simplification | |||
STRICT_PAGE_ACCESS |
Raise a SimSegfaultException when attempting to interact with memory in a way not permitted by the current permissions | tracing |
||
SUPER_FASTPATH |
Only execute the last four instructions of each block | |||
SUPPORT_FLOATING_POINT |
When disabled, throw an UnsupportedIROpError when encountering floating point operations | common_options |
all | |
SYMBOLIC |
Enable constraint solving? | symbolic |
symbolic, symbolic_approximating, fastpath |
|
SYMBOLIC_INITIAL_VALUES |
make state.solver.Unconstrained return a symbolic value instead of zero |
symbolic |
all | |
SYMBOLIC_TEMPS |
Treat each IR temporary as a symbolic variable; treat stores to them as constraint addition | |||
SYMBOLIC_WRITE_ADDRESSES |
Allow writes with symbolic addresses to be processed by concretization strategies; when disabled, only allow for variables annotated with the "multiwrite" annotation | |||
TRACK_CONSTRAINTS |
When disabled, don't keep any constraints added to the state | symbolic |
all | |
TRACK_CONSTRAINT_ACTIONS |
Keep a SimAction for each constraint added | refs |
||
TRACK_JMP_ACTIONS |
Keep a SimAction for each jump or branch | refs |
||
TRACK_MEMORY_ACTIONS |
Keep a SimAction for each memory read and write | refs |
||
TRACK_MEMORY_MAPPING |
Keep track of which pages are mapped into memory and which are not | common_options |
all | |
TRACK_OP_ACTIONS |
Keep a SimAction for each IR operation | fastpath |
||
TRACK_REGISTER_ACTIONS |
Keep a SimAction for each register read and write | refs |
||
TRACK_SOLVER_VARIABLES |
Maintain a listing of all the variables in all the constraints in the solver | |||
TRACK_TMP_ACTIONS |
Keep a SimAction for each temporary variable read and write | refs |
||
TRUE_RET_EMULATION_GUARD |
With DO_RET_EMULATION, add fake returns with guard condition true instead of false |
static |
||
UNDER_CONSTRAINED_SYMEXEC |
Enable under-constrained symbolic execution | |||
UNICORN |
Use unicorn engine to execute symbolically when data is concrete | unicorn |
tracing |
Oppologist |
UNICORN_AGGRESSIVE_CONCRETIZATION |
Concretize any register variable unicorn tries to access | Oppologist | ||
UNICORN_HANDLE_TRANSMIT_SYSCALL |
CGC: handle the transmit syscall without leaving unicorn | unicorn |
tracing |
|
UNICORN_SYM_REGS_SUPPORT |
Attempt to stay in unicorn even in the presence of symbolic registers by checking that the tainted registers are unused at every step | unicorn |
tracing |
|
UNICORN_THRESHOLD_CONCRETIZATION |
Concretize variables if they prevent unicorn from executing too often | |||
UNICORN_TRACK_BBL_ADDRS |
Keep state.history.bbl_addrs up to date when using unicorn |
unicorn |
tracing |
|
UNICORN_TRACK_STACK_POINTERS |
Track a list of the stack pointer's value at each block in state.scratch.stack_pointer_list |
unicorn |
||
UNICORN_ZEROPAGE_GUARD |
Prevent unicorn from mapping the zero page into memory | |||
UNINITIALIZED_ACCESS_AWARENESS |
Broken/unused? | |||
UNSUPPORTED_BYPASS_ZERO_DEFAULT |
When using the resilience options, return zero instead of an unconstrained symbol | |||
USE_SIMPLIFIED_CCALLS |
Use a "simplified" set of ccalls optimized for specific cases | static |
||
USE_SYSTEM_TIMES |
In library functions and syscalls and hardware instructions accessing clock data, retrieve the real value from the host system. | tracing |
||
VALIDATE_APPROXIMATIONS |
Debug: When performing approximations, ensure that the approximation is sound by calling into z3 | |||
ZERO_FILL_UNCONSTRAINED_MEMORY |
Make the value of memory read from an uninitialized address zero instead of an unconstrained symbol | tracing |