angr文档摘要1———Symbolic Expressions and COnstraint Solving

几个月前入门angr，很久没用了，重新看文档，记一些笔记

Symbolic Expressions and COnstraint Solving

angr's solver engine is called Claripy

Working with bitvectors

bitvector is a sequence bits

BVV: bitvector value, BVV是值
BVS: bitvector symbol，BVS是符号

创建BVV方法

one=state.solver.BVV(1,64)#value=1, num of bits=64
# or
one=clarypy.BVV(1,64)

创建BVS

x=state.solver.BVS("x",64)
y=clarypy.BVS('x',64)

在运算时bitvector长度必须相同

Symbolic Constrains

BVS op BVV :<Bool x_n_m == value>
BVV op BVV :<Bool True or False>

用state.solver.is_true(exp)来判断真假，而不是if one > hundred 来判断

约束求解

state.solver.add(exp1)# add constrains
state.solver.add(exp2)# add constrains
print state.solver.eval(xs) # get results

solver.eval(exp):give one possible expression
solver.max(exp):get max possible expression
solver.min(exp):get mix possible expression

cast_to:passed as a data type