diff options
| -rw-r--r-- | src/focaccia/parser.py | 18 | ||||
| -rw-r--r-- | src/focaccia/qemu/_qemu_tool.py | 26 |
2 files changed, 34 insertions, 10 deletions
diff --git a/src/focaccia/parser.py b/src/focaccia/parser.py index 9c7b283..dd1223f 100644 --- a/src/focaccia/parser.py +++ b/src/focaccia/parser.py @@ -31,6 +31,21 @@ def parse_transformations(json_stream: TextIO) -> TraceContainer[SymbolicTransfo return TraceContainer(strace, env) +class SymbolicTransformStream: + def __init__(self, unpacker: msgpack.Unpacker): + self._unpacker = unpacker + + def __iter__(self): + return self + + def __next__(self) -> SymbolicTransform: + obj = next(self._unpacker) + return SymbolicTransform.from_json(obj['state']) + + def skip(self, n: int = 1) -> None: + for _ in range(n): + self._unpacker.skip() + def stream_transformation(stream) -> Trace[SymbolicTransform]: unpacker = msgpack.Unpacker(stream, raw=False) @@ -44,7 +59,8 @@ def stream_transformation(stream) -> Trace[SymbolicTransform]: t = SymbolicTransform.from_json(obj['state']) yield t - return Trace(state_iter(), addresses, env) + state_stream = SymbolicTransformStream(unpacker) + return Trace(iter(state_stream), addresses, env) def serialize_transformations(trace: Trace[SymbolicTransform], out_file: str, diff --git a/src/focaccia/qemu/_qemu_tool.py b/src/focaccia/qemu/_qemu_tool.py index c838f2b..c6d6c1c 100644 --- a/src/focaccia/qemu/_qemu_tool.py +++ b/src/focaccia/qemu/_qemu_tool.py @@ -175,7 +175,6 @@ def collect_conc_trace(gdb: GDBServerStateIterator, strace: Trace) \ break try: - symb_i += 1 transform = next(trace) except StopIteration: break @@ -185,7 +184,8 @@ def collect_conc_trace(gdb: GDBServerStateIterator, strace: Trace) \ next_i = None if pc in traced_address_set: - next_i = find_index(strace.addresses[symb_i:], pc) + next_i = find_index(strace.addresses[symb_i+1:], pc) + print(f'Next {next_i}, current {symb_i}') # Drop the concrete state if no address in the symbolic trace # matches @@ -198,13 +198,20 @@ def collect_conc_trace(gdb: GDBServerStateIterator, strace: Trace) \ continue # Otherwise, jump to the next matching symbolic state - for _ in range(next_i+1): - try: - symb_i += 1 - transform = next(trace) - except StopIteration: - warn(f'QEMU executed more states than native execution: {symb_i} vs {len(strace.addresses)-1}') - break + try: + trace.skip(next_i) + transform = next(trace) + symb_i += next_i+1 + except StopIteration: + warn(f'QEMU executed more states than native execution: {symb_i} vs {len(strace.addresses)-1}') + break + # for _ in range(next_i+1): + # try: + # symb_i += 1 + # transform = next(trace) + # except StopIteration: + # warn(f'QEMU executed more states than native execution: {symb_i} vs {len(strace.addresses)-1}') + # break assert(cur_state.read_pc() == transform.addr) info(f'Validating instruction at address {hex(pc)}') @@ -213,6 +220,7 @@ def collect_conc_trace(gdb: GDBServerStateIterator, strace: Trace) \ cur_state, matched_transforms[-1] if matched_transforms else transform, transform)) + symb_i += 1 matched_transforms.append(transform) cur_state = next(state_iter) except StopIteration: |