Handle exit in post-event hook

2 files changed, 22 insertions, 13 deletions

diff --git a/src/focaccia/deterministic.py b/src/focaccia/deterministic.py
index 3396797..f60b3ba 100644
--- a/src/focaccia/deterministic.py
+++ b/src/focaccia/deterministic.py
@@ -171,9 +171,6 @@ class DeterministicLog:
             pc, registers = parse_registers(raw_event)
             mem_writes = parse_memory_writes(raw_event)
 
-            if pc == 0:
-                pc = events[-1].pc
-
             event = Event(pc,
                           raw_event.tid,
                           raw_event.arch,
diff --git a/src/focaccia/symbolic.py b/src/focaccia/symbolic.py
index 49e0259..ef7723a 100644
--- a/src/focaccia/symbolic.py
+++ b/src/focaccia/symbolic.py
@@ -780,17 +780,26 @@ class SymbolicTracer:
                                       f' mem[{hex(addr)}:{hex(addr+len(data))}] = {conc_data}.'
                                       f'\nFaulty transformation: {transform}')
 
-    def progress_event(self):
-        if self.next_event < len(self.nondet_events):
+    def progress_event(self) -> None:
+        if (self.next_event + 1) < len(self.nondet_events):
             self.next_event += 1
+            debug(f'Next event to handle at index {self.next_event}')
         else:
             self.next_event = None
 
-    def post_event(self):
-        self.progress_event()
+    def post_event(self) -> None:
+        if self.next_event:
+            if self.nondet_events[self.next_event].pc == 0:
+                # Exit sequence
+                debug('Completed exit event')
+                self.target.run()
 
-    def is_stepping_instr(self, pc: int, instruction: Instruction):
+            debug(f'Completed handling event at index {self.next_event}')
+            self.progress_event()
+
+    def is_stepping_instr(self, pc: int, instruction: Instruction) -> bool:
         if self.nondet_events:
+            pc = pc + instruction.length # detlog reports next pc for each event
             if self.next_event and self.nondet_events[self.next_event].match(pc, self.target):
                 debug('Current instruction matches next event; stepping through it')
                 self.progress_event()
@@ -824,7 +833,10 @@ class SymbolicTracer:
 
         for i in range(len(self.nondet_events)):
             if self.nondet_events[i].pc == self.target.read_pc():
-                self.next_event = i
+                self.next_event = i+1
+                if self.next_event >= len(self.nondet_events):
+                    break
+
                 debug(f'Starting from event {self.nondet_events[i]} onwards')
                 break
 
@@ -872,7 +884,7 @@ class SymbolicTracer:
                         continue
                     raise # forward exception
 
-            needs_step = self.is_stepping_instr(pc, instruction)
+            is_event = self.is_stepping_instr(pc, instruction)
 
             # Run instruction
             conc_state = MiasmSymbolResolver(self.target, ctx.loc_db)
@@ -890,7 +902,7 @@ class SymbolicTracer:
                 new_pc = int(new_pc)
                 transform = SymbolicTransform(modified, [instruction], arch, pc, new_pc)
                 pred_regs, pred_mems = self.predict_next_state(instruction, transform)
-                self.progress(new_pc, step=needs_step)
+                self.progress(new_pc, step=is_event)
 
                 try:
                     self.validate(instruction, transform, pred_regs, pred_mems)
@@ -900,14 +912,14 @@ class SymbolicTracer:
                         continue
                     raise
             else:
-                new_pc = self.progress(new_pc, step=needs_step)
+                new_pc = self.progress(new_pc, step=is_event)
                 if new_pc is None:
                     continue # we're done
                 transform = SymbolicTransform(modified, [instruction], arch, pc, new_pc)
 
             strace.append(transform)
 
-            if needs_step:
+            if is_event:
                 self.post_event()
 
         return Trace(strace, self.env)