1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
"""Interpreter for claripy ASTs"""
from inspect import signature
from logging import debug
import claripy as cp
class SymbolResolver:
def __init__(self):
pass
def resolve(self, symbol_name: str) -> cp.ast.Base:
raise NotImplementedError()
class SymbolResolveError(Exception):
def __init__(self, symbol, reason: str = ""):
super().__init__(f'Unable to resolve symbol name \"{symbol}\" to a'
' concrete value'
+ f': {reason}' if len(reason) > 0 else '.')
def eval(resolver: SymbolResolver, expr) -> int:
"""Evaluate a claripy expression to a concrete value.
:param resolver: A `SymbolResolver` implementation that can resolve symbol
names to concrete values.
:param expr: The claripy AST to evaluate. Should be a subclass of
`claripy.ast.Base`.
:return: A concrete value if the expression was resolved successfully.
If `expr` is not a claripy AST, `expr` is returned immediately.
:raise NotImplementedError:
:raise SymbolResolveError: If `resolver` is not able to resolve a symbol.
"""
if not issubclass(type(expr), cp.ast.Base):
return expr
if expr.depth == 1:
if expr.symbolic:
name = expr._encoded_name.decode()
val = resolver.resolve(name)
if val is None:
raise SymbolResolveError(name)
return eval(resolver, val)
else: # if expr.concrete
assert(expr.concrete)
return expr.v
# Expression is a non-trivial AST, i.e. a function
return _eval_op(resolver, expr.op, *expr.args)
def _eval_op(resolver: SymbolResolver, op, *args) -> int:
"""Evaluate a claripy operator expression.
:param *args: Arguments to the function `op`. These are NOT evaluated yet!
"""
assert(type(op) is str)
def concat(*vals):
res = 0
for val in vals:
assert(type(val) is cp.ast.BV)
res = res << val.length
res = res | eval(resolver, val)
return res
# Handle claripy's operators
if op == 'Concat':
res = concat(*args)
debug(f'Concatenating {args} to {hex(res)}')
return res
if op == 'Extract':
assert(len(args) == 3)
start, end, val = (eval(resolver, arg) for arg in args)
size = start - end + 1
res = (val >> end) & ((1 << size) - 1)
debug(f'Extracing range [{start}, {end}] from {hex(val)}: {hex(res)}')
return res
if op == 'If':
assert(len(args) == 3)
cond, iftrue, iffalse = (eval(resolver, arg) for arg in args)
debug(f'Evaluated branch condition {args[0]} to {cond}')
return iftrue if bool(cond) else iffalse
if op == 'Reverse':
assert(len(args) == 1)
return concat(*reversed(args[0].chop(8)))
# `op` is not one of claripy's special operators, so treat it as the name
# of a python operator function (because that is how claripy names its OR,
# EQ, etc.)
# Convert some of the non-python names to magic names
# NOTE: We use python's signed comparison operators for unsigned
# comparisons. I'm not sure that this is legal.
if op in ['SGE', 'SGT', 'SLE', 'SLT', 'UGE', 'UGT', 'ULE', 'ULT']:
op = '__' + op[1:].lower() + '__'
if op in ['And', 'Or']:
op = '__' + op.lower() + '__'
resolved_args = [eval(resolver, arg) for arg in args]
try:
func = getattr(int, op)
except AttributeError:
raise NotImplementedError(op)
# Sometimes claripy doesn't build its AST in an arity-respecting way if
# adjacent operations are associative. For example, it might pass five
# arguments to an XOR function instead of nesting the AST deeper.
#
# That's why we have to check with the python function's signature for its
# number of arguments and manually apply parentheses.
sig = signature(func)
assert(len(args) >= len(sig.parameters))
debug(f'Trying to evaluate function {func} with arguments {resolved_args}')
if len(sig.parameters) == len(args):
return func(*resolved_args)
else:
# Fold parameters from left by successively applying `op` to a
# subset of them
return _eval_op(resolver,
op,
func(*resolved_args[0:len(sig.parameters)]),
*resolved_args[len(sig.parameters):]
)
|