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
