Using angr to solve "recurse"

output.txt

(angr) moyix@lorenzo:~$ time python recurse_solve.py recurse.bin
WARNING | 2018-02-22 19:00:58,557 | angr.analyses.disassembly_utils | Your verison of capstone does not support MIPS instruction groups.
a = 13
b = 37

real    0m1.397s
user    0m1.340s
sys     0m0.052s

recurse_solve.py

#!/usr/bin/env python
  
import sys
import angr
import claripy

# Start of the "recurse" function
RECURSE_START = 0x400749
# Address of the "return true" branch
SUCCESS_ADDR = 0x400774

# Load the binary. We use auto_load_libs = False so that it doesn't
# try to load libc (we're only going to execute one function)
proj = angr.Project(sys.argv[1],
        load_options={'auto_load_libs': False})

# Set up an initial state to start from. "addr" tells it what to set
# the program counter to (i.e. where to start executing)
initial_state = proj.factory.blank_state(addr=RECURSE_START)

# Set the inputs to the function.
#   BVS is a symbolic bit vector.
#   BVV is a concrete bit vector.
a = claripy.BVS('a', 64)
b = claripy.BVS('b', 64)
initial_state.regs.rdi = a
initial_state.regs.rsi = b
initial_state.regs.rdx = claripy.BVV(0, 64)

# Constrain a and b to reasonable values
# "se" is the "solver engine" for our state
initial_state.se.add(a > 0)
initial_state.se.add(b > 0)
initial_state.se.add(a < 10000)
initial_state.se.add(b < 10000)

# Create a "simulation manager" that will track the various paths
# as we symbolically execute the function. We give it the state
# we constructed as its starting point.
sim = proj.factory.simulation_manager(initial_state)

# Explore, looking for our success condition
sim.explore(find=SUCCESS_ADDR)

# When we reach here we're done! Just print out a and b.
# angr will put all paths that reached SUCCESS_ADDR into sim.found
found = sim.found[0]
print "a =", found.state.se.eval(a)
print "b =", found.state.se.eval(b)