Angr + Claripy Cheatsheet
===

Also available at: https://pad.sec.in.tum.de/V1nxhCWqRM2FWski2iHysg#

To be completed

# Angr

 - Read/Write Register: `state.regs.<regname>`
 - Write memory: `state.mem[addr].uintX_t = value`
 - Read memory: `value = state.mem[addr].uintX_t.resolved.args[0]`
 - Add constraint/condition: `state.solver.add(constraint)`
 - Get possible value of symbolic expression in state: `state.solver.eval(expr)`
 - Read stdin/stdout/stderr in found state: `state.posix.dumps(<fd>)`

 - Single-Step: `next_states = project.factory.successors(state, num_inst=1)`

 - Increase libc symbolic buffer max size: `state.libc.buf_symbolic_bytes = 0x100`

 - Provide stdin: In state initializer, add `stdin=flag_bvv`


## Concretization hacks:

 - hooking:
    - `state.inspect.b('address_concretization', when=angr.BP_BEFORE, action=func)`
    - `state.inspect.b('address_concretization', when=angr.BP_AFTER, action=func)`



# Claripy
Note: In general, bit vectors are **big-endian**!

Values:
 - Create symbolic variable: `claripy.BVS('sym_arg', bitsize)`
 - Create constant value: `claripy.BVV(value, bitsize)`
 - Create constant value from bytes: `claripy.BVV(bytes)`
 - Combine multiple values: `flag = claripy.Concat(*flag_bytes)`

Expressions:
 - Check if expression is constant `expr.op == 'BVV'`
 - Access expression children: `expr.args`
 - Split bitvector into smaller bitvectors (big-endian!), e.g. bytes: `expr.chop(8)`
 - If-then-else: `claripy.If(cond, then, else)
 - Normal arithmetic: Use python operators; generally mimics `z3` behavior


API-Reference: https://docs.angr.io/projects/claripy/en/latest/api.html