Implement skip() mechanism for unmatch symbolic transformations

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: