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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
from snapshot import ProgramState
from utils import print_separator
def calc_transformation(previous: ProgramState, current: ProgramState):
"""Calculate the difference between two context blocks.
:return: A context block that contains in its registers the difference
between the corresponding input blocks' register values.
"""
assert(previous.arch == current.arch)
arch = previous.arch
transformation = ProgramState(arch)
for reg in arch.regnames:
prev_val, cur_val = previous.regs[reg], current.regs[reg]
if prev_val is not None and cur_val is not None:
transformation.regs[reg] = cur_val - prev_val
return transformation
def equivalent(val1, val2, transformation, previous_translation):
if val1 == val2:
return True
# TODO: maybe incorrect
return val1 - previous_translation == transformation
def verify(translation: ProgramState, reference: ProgramState,
transformation: ProgramState, previous_translation: ProgramState):
assert(translation.arch == reference.arch)
if translation.regs["PC"] != reference.regs["PC"]:
return 1
print_separator()
print(f'For PC={translation.as_repr("PC")}')
print_separator()
for reg in translation.arch.regnames:
if translation.regs[reg] is None:
print(f'Element not available in translation: {reg}')
elif reference.regs[reg] is None:
print(f'Element not available in reference: {reg}')
elif not equivalent(translation.regs[reg], reference.regs[reg],
transformation.regs[reg],
previous_translation.regs[reg]):
txl = translation.as_repr(reg)
ref = reference.as_repr(reg)
print(f'Difference for {reg}: {txl} != {ref}')
return 0
def compare(txl: list[ProgramState],
native: list[ProgramState],
progressive: bool = False,
stats: bool = False):
"""Compare two lists of snapshots and output the differences.
:param txl: The translated, and possibly faulty, state of the program.
:param native: The 'correct' reference state of the program.
:param progressive:
:param stats:
"""
if len(txl) != len(native):
print(f'Different numbers of blocks discovered: '
f'{len(txl)} in translation vs. {len(native)} in reference.')
previous_reference = native[0]
previous_translation = txl[0]
unmatched_pcs = {}
pc_to_skip = ""
if progressive:
i = 0
for translation in txl:
previous = i
while i < len(native):
reference = native[i]
transformation = calc_transformation(previous_reference, reference)
if verify(translation, reference, transformation, previous_translation) == 0:
reference.matched = True
break
i += 1
matched = True
# Didn't find anything
if i == len(native):
matched = False
# TODO: add verbose output
print_separator()
print(f'No match for PC {hex(translation.regs["PC"])}')
if translation.regs['PC'] not in unmatched_pcs:
unmatched_pcs[translation.regs['PC']] = 0
unmatched_pcs[translation.regs['PC']] += 1
i = previous
# Necessary since we may have run out of native BBs to check and
# previous becomes len(native)
#
# We continue checking to report unmatched translation PCs
if i < len(native):
previous_reference = native[i]
previous_translation = translation
# Skip next reference when there is a backwards branch
# NOTE: if a reference was skipped, don't skip it again
# necessary for loops which may have multiple backwards
# branches
if translation.has_backwards and translation.regs['PC'] != pc_to_skip:
pc_to_skip = translation.regs['PC']
i += 1
if matched:
i += 1
else:
txl = iter(txl)
native = iter(native)
for translation, reference in zip(txl, native):
transformation = calc_transformation(previous_reference, reference)
if verify(translation, reference, transformation, previous_translation) == 1:
# TODO: add verbose output
print_separator()
print(f'No match for PC {hex(translation.regs["PC"])}')
if translation.regs['PC'] not in unmatched_pcs:
unmatched_pcs[translation.regs['PC']] = 0
unmatched_pcs[translation.regs['PC']] += 1
else:
reference.matched = True
if translation.has_backwards:
next(native)
previous_reference = reference
previous_translation = translation
if stats:
print_separator()
print('Statistics:')
print_separator()
for pc in unmatched_pcs:
print(f'PC {hex(pc)} unmatched {unmatched_pcs[pc]} times')
# NOTE: currently doesn't handle mismatched due backward branches
current = ""
unmatched_count = 0
for ref in native:
ref_pc = ref.regs['PC']
if ref_pc != current:
if unmatched_count:
print(f'Reference PC {hex(current)} unmatched {unmatched_count} times')
current = ref_pc
if ref.matched == False:
unmatched_count += 1
return 0
|