The solver plugin (SimSolver) is the primary interface for creating and manipulating symbolic variables and solving constraints in angr. It’s accessible via state.solver.
Overview The solver plugin wraps the Claripy constraint solver and provides methods for:
Creating symbolic variables
Adding constraints
Evaluating expressions
Checking satisfiability
Finding min/max values
Creating Symbolic Variables BVS BVS(name, size, min = None , max = None , stride = None , uninitialized = False , explicit_name = False , key = None , eternal = False , inspect = True , events = True , ** kwargs)
Create a bit-vector symbol (symbolic variable).
The name of the symbolic variable.
The size in bits of the bitvector.
Minimum value (VSA only).
Maximum value (VSA only).
Stride/step value (VSA only).
Whether to mark this as an uninitialized value for analysis.
If True, don’t append a unique identifier to the name.
Tracking key for variable registration (e.g., ('mem', 0x1000)).
If True with a key, all states with the same ancestry retrieve the same symbol.
# Create 32-bit symbolic variable x = state.solver.BVS( 'x' , 32 ) # Create with explicit name (no unique suffix) y = state.solver.BVS( 'input' , 64 , explicit_name = True ) # Create tracked variable buf = state.solver.BVS( 'buf' , 256 , key = ( 'mem' , 0x 1000 ), eternal = True ) # VSA: Create with value constraints port = state.solver.BVS( 'port' , 16 , min = 1024 , max = 65535 )
Unconstrained Unconstrained(name, bits, uninitialized = True , inspect = True , events = True , key = None , eternal = False , ** kwargs)
Create an unconstrained symbol or concrete zero based on state options.
A symbolic bitvector if SYMBOLIC_INITIAL_VALUES is set, otherwise concrete 0.
# Creates symbolic if SYMBOLIC_INITIAL_VALUES is in state.options val = state.solver.Unconstrained( 'uninit_var' , 32 )
Adding Constraints add Add constraints to the solver state.
Boolean constraint expressions to add. Pass multiple constraints as separate arguments.
# Add single constraint state.solver.add(x > 10 ) # Add multiple constraints state.solver.add(x > 10 , x < 100 , y == 42 ) # Add complex constraint state.solver.add(x + y == z * 2 )
Constraints must be boolean expressions (comparisons, logical operations)
Adding conflicting constraints makes the state unsatisfiable
Constraints are permanent and affect all future solver operations
Use state.solver.satisfiable() to check if constraints are consistent
Evaluating Expressions eval eval (e, cast_to = None , ** kwargs)
Get one possible solution for an expression.
The expression to evaluate.
Type to cast result to (int, bytes, etc.).
Additional temporary constraints for this evaluation only.
One possible value satisfying the constraints.
# Evaluate to integer value = state.solver.eval(x) print (value) # e.g., 42 # Evaluate to bytes string = state.solver.eval(buf, cast_to = bytes ) print (string) # e.g., b'hello' # Evaluate with extra constraints value = state.solver.eval(x, extra_constraints = (x > 100 ,))
eval_one eval_one(e, cast_to = None , ** kwargs)
Get the only possible solution. Raises an error if there are zero or multiple solutions.
state.solver.add(x == 42 ) value = state.solver.eval_one(x) # Returns 42 # With default on failure value = state.solver.eval_one(x, default = 0 ) # Returns 0 if multiple solutions
eval_upto eval_upto(e, n, cast_to = None , ** kwargs)
Get up to n possible solutions.
Maximum number of solutions to return.
List of solutions (length 1 to n).
# Get up to 10 solutions values = state.solver.eval_upto(x, 10 ) print (values) # e.g., [1, 2, 3, 4, 5, 6, 7, 8, 9, 10] # Check if variable has limited solutions if len (state.solver.eval_upto(x, 2 )) == 1 : print ( "x is concrete" )
eval_exact eval_exact(e, n, cast_to = None , ** kwargs)
Get exactly n solutions. Raises error if there are more or fewer.
state.solver.add(x < 5 , x >= 0 ) values = state.solver.eval_exact(x, 5 ) # [0, 1, 2, 3, 4]
eval_atleast / eval_atmost eval_atleast(e, n, cast_to = None , ** kwargs) eval_atmost(e, n, cast_to = None , ** kwargs)
Get at least/at most n solutions. Raises error if requirement not met.
# Ensure at least 5 solutions exist values = state.solver.eval_atleast(x, 5 ) # Ensure at most 3 solutions exist values = state.solver.eval_atmost(x, 3 )
Min/Max Values min / max min (e, extra_constraints = (), exact = None , signed = False ) max (e, extra_constraints = (), exact = None , signed = False )
Find the minimum or maximum possible value of an expression.
The expression to evaluate.
Whether to treat the expression as signed.
The minimum or maximum value.
state.solver.add(x > 10 , x < 100 ) min_val = state.solver.min(x) # 11 max_val = state.solver.max(x) # 99 # Signed min/max state.solver.add(y < 0 ) min_val = state.solver.min(y, signed = True ) # Negative value
Satisfiability Checking satisfiable satisfiable( extra_constraints = (), exact = None )
Check if the current constraints are satisfiable.
Additional temporary constraints to check.
True if satisfiable, False if unsatisfiable.
# Check if constraints are consistent if state.solver.satisfiable(): print ( "State is feasible" ) # Check with extra constraints if state.solver.satisfiable( extra_constraints = (x == 42 ,)): print ( "x can be 42" )
is_true / is_false is_true(e, extra_constraints = (), exact = None ) is_false(e, extra_constraints = (), exact = None )
Check if an expression is definitely true or false.
True if the expression is definitely true/false under current constraints.
state.solver.add(x > 10 ) if state.solver.is_true(x > 5 ): print ( "x is definitely > 5" ) if state.solver.is_false(x < 5 ): print ( "x is definitely >= 5" )
solution solution(e, v, extra_constraints = (), exact = None )
Check if v is a valid solution for expression e.
True if v is a valid solution.
state.solver.add(x > 10 , x < 20 ) print (state.solver.solution(x, 15 )) # True print (state.solver.solution(x, 5 )) # False
Constraint Management constraints Property that returns the current constraint list.
all_constraints = state.solver.constraints print ( f "State has { len (all_constraints) } constraints" ) for constraint in all_constraints: print (constraint)
unsat_core unsat_core( extra_constraints = ())
Get the unsatisfiable core (minimal set of conflicting constraints).
Tuple of constraints that form an unsatisfiable core.
# Requires CONSTRAINT_TRACKING_IN_SOLVER option state.options.add( 'CONSTRAINT_TRACKING_IN_SOLVER' ) state.solver.add(x > 10 ) state.solver.add(x < 5 ) # Conflict! try : state.solver.eval(x) except : core = state.solver.unsat_core() print ( f "Conflicting constraints: { core } " )
reload_solver reload_solver( constraints = None )
Reload the solver, useful when changing solver options.
# Change solver options state.options.add( 'REPLACEMENT_SOLVER' ) state.solver.reload_solver()
Variable Management register_variable register_variable(v, key, eternal = True )
Register a variable with the tracking system.
The variable to register.
Tracking key tuple (e.g., ('mem', 0x1000)).
If True, variable persists across state copies.
buf = state.solver.BVS( 'buffer' , 256 ) state.solver.register_variable(buf, ( 'mem' , 0x 1000 ), eternal = True )
get_variables Iterate over tracked variables matching the given key prefix.
Variable-length key prefix to filter by.
Iterator of (key, variable) tuples.
# Get all memory variables for key, var in state.solver.get_variables( 'mem' ): print ( f "Memory at { key } : { var } " ) # Get specific file variables for key, var in state.solver.get_variables( 'file' , 2 ): print ( f "File 2 variable: { key } = { var } " ) # Get all tracked variables for key, var in state.solver.get_variables(): print ( f " { key } : { var } " )
describe_variables Get the tracking keys for all registered variables in an AST.
An expression containing variables.
Iterator of tracking keys.
expr = x + y + z for key in state.solver.describe_variables(expr): print ( f "Expression contains variable: { key } " )
Utility Methods symbolic Check if an expression is symbolic (contains variables).
True if symbolic, False if concrete.
if state.solver.symbolic(x): print ( "x is symbolic" ) else : print ( "x is concrete" )
unique Check if expression has exactly one solution, and add that constraint.
True if unique, False if multiple solutions exist.
if state.solver.unique(x): print ( f "x must be { state.solver.eval(x) } " )
single_valued Check if expression is concrete or has only one possible value (without querying solver).
if state.solver.single_valued(x): print ( "x has a single value" )
simplify Simplify an expression or the current constraint set.
Expression to simplify. If None, simplifies all constraints.
# Simplify expression simple = state.solver.simplify(x + x + 0 ) # simple might be 2*x # Simplify all constraints state.solver.simplify()
variables Get the set of variable names in an expression.
Set of variable name strings.
vars = state.solver.variables(x + y * 2 ) print ( vars ) # {'x', 'y'}
Claripy Interoperability The solver provides access to all Claripy module functions as properties:
# These are equivalent: state.solver.BVV( 0x 1234 , 32 ) claripy.BVV( 0x 1234 , 32 ) # Boolean operations state.solver.And(cond1, cond2) state.solver.Or(cond1, cond2) state.solver.Not(cond) # Arithmetic state.solver.ULT(x, y) # Unsigned less than state.solver.SLT(x, y) # Signed less than # Bit operations state.solver.Extract( 63 , 32 , x) # Get bits 63-32 state.solver.Concat(x, y) # Concatenate
Examples import angr project = angr.Project( '/bin/example' ) state = project.factory.entry_state() # Create symbolic input input_size = 64 sym_input = state.solver.BVS( 'input' , input_size * 8 ) state.memory.store( 0x 1000 , sym_input) # Run and add constraints simgr = project.factory.simulation_manager(state) simgr.explore( find = 0x 401234 ) if simgr.found: found = simgr.found[ 0 ] # Get valid input solution = found.solver.eval(sym_input, cast_to = bytes ) print ( f "Valid input: { solution } " )
Password Cracking # Symbolic password password = state.solver.BVS( 'password' , 32 * 8 ) # 32 bytes state.memory.store(password_addr, password) # Run to password check simgr.explore( find = success_addr, avoid = failure_addr) if simgr.found: found = simgr.found[ 0 ] pwd = found.solver.eval(password, cast_to = bytes ) print ( f "Password: { pwd.decode() } " )
Constraint-Based Analysis # Add application constraints state.solver.add(x >= 0 ) state.solver.add(x <= 1000 ) state.solver.add(y == x * 2 + 5 ) # Find values if state.solver.satisfiable(): x_val = state.solver.eval(x) y_val = state.solver.eval(y) print ( f "x= { x_val } , y= { y_val } " ) # Check properties if state.solver.is_true(y > x): print ( "y is always greater than x" )
See Also