Repository navigation
Expand file tree
/
Copy pathutils.py
More file actions
133 lines (107 loc) · 3.98 KB
/
Copy pathutils.py
File metadata and controls
133 lines (107 loc) · 3.98 KB
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
126
127
128
129
130
131
132
133
#!/usr/bin/python3
# -*- coding: utf-8 -*-
"""
The utils module includes functions to help symbolic execution, such as transformation function
for transform truly value to symbolic value and versa.
"""
import ctypes
from typing import Union
import six
import z3
import bin_format
def is_int(value: int) -> bool:
return isinstance(value, six.integer_types)
def is_float(value: float) -> bool:
return isinstance(value, float)
def is_symbolic(value: Union[float, int, z3.BitVecNumRef]) -> bool:
return not isinstance(value, six.integer_types) and not isinstance(value, float)
def is_all_real(*args) -> bool:
for elem in args:
if is_symbolic(elem):
return False
return True
def to_symbolic(number: int, length: int) -> z3.BitVecVal:
if is_int(number) or is_float(number):
return z3.BitVecVal(number, length)
return number
def to_signed(number: int, length: int) -> int:
if number > 2**(length - 1):
return (2 ** length - number) * (-1)
else:
return number
def to_unsigned(number: int, length: int) -> int:
if number < 0:
return number + 2 ** length
else:
return number
def sym_abs(x):
return z3.If(x >= 0, x, -x)
def check_sat(solver: z3.Solver, pop_if_exception: bool = True) -> z3.CheckSatResult:
try:
ret = solver.check()
if ret == z3.unknown:
raise z3.Z3Exception(solver.reason_unknown())
except Exception as e:
if pop_if_exception:
solver.pop()
raise e
return ret
def eos_abi_to_int(abi_name: str) -> int:
try:
if len(abi_name) > 13:
raise Exception('string is too long to be a valid name')
if not abi_name:
return 0
value = 0
n = min(len(abi_name), 12)
for i in range(n):
value <<= 5
value |= _char_to_value(abi_name[i])
value <<= (4 + 5*(12-n))
if len(abi_name) == 13:
v = _char_to_value(abi_name[12])
if v > 0x0F:
raise Exception('13th character in name cannot be a letter that comes after j')
value |= v
return ctypes.c_int64(value).value
except Exception as e:
return 0
def _char_to_value(c: str) -> int:
if c == '.':
return 0
elif '1' <= c <= '5':
return (ord(c) - ord('1')) + 1
elif 'a' <= c <= 'z':
return (ord(c) - ord('a')) + 6
else:
raise Exception('character is not in allowed character set for names')
def gen_symbolic_args(func: 'instance.FunctionInstance'):
symbolic_params = list()
for i, e in enumerate(func.functype.args):
if e == bin_format.i32:
symbolic_params.append(z3.BitVec(f'i32_bv_{i}', 32))
elif e == bin_format.i64:
symbolic_params.append(z3.BitVec(f'i64_bv_{i}', 64))
elif e == bin_format.f32:
# The first approach is bit-vector based
# f32_bv = z3.BitVec(f'f32_bv_{i}', 32)
# symbolic_params.append(z3.fpBVToFP(f32_bv, z3.Float32()))
# The second approach is float-point based
symbolic_params.append(z3.FP(f'f32_{i}', z3.Float32()))
else:
# The first approach is bit-vector based
# f64_bv = z3.BitVec(f'f64_bv_{i}', 64)
# symbolic_params.append(z3.fpBVToFP(f64_bv, z3.Float64()))
# The second approach is float-point based
symbolic_params.append(z3.FP(f'f64_{i}', z3.Float64()))
return symbolic_params
def gen_symbolic_value(var_type, name):
if var_type == bin_format.i32:
return z3.BitVec(name, 32)
if var_type == bin_format.i64:
return z3.BitVec(name, 64)
if var_type == bin_format.f32:
return z3.FP(f'f32_{i}', z3.Float32())
if var_type == bin_format.f64:
return z3.FP(name, z3.Float64())
raise TypeError('Unsupported variable type')