about summary refs log tree commit diff stats
diff options
context:
space:
mode:
-rw-r--r--src/focaccia/deterministic.py17
-rw-r--r--src/focaccia/symbolic.py18
2 files changed, 18 insertions, 17 deletions
diff --git a/src/focaccia/deterministic.py b/src/focaccia/deterministic.py
index 635a573..3396797 100644
--- a/src/focaccia/deterministic.py
+++ b/src/focaccia/deterministic.py
@@ -170,6 +170,10 @@ class DeterministicLog:
         for raw_event in raw_events:
             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,
@@ -177,16 +181,5 @@ class DeterministicLog:
                           registers, mem_writes)
             events.append(event)
 
-        # deduplicate
-        deduped_events = []
-        for i in range(0, len(events), 2):
-            if events[i].event_type == 'syscall':
-                if events[i+1].pc == 0:
-                    deduped_events.append(events[i])
-                    break
-                if events[i+1].event_type != 'syscall':
-                    raise Exception(f'Event {events[i+1]} should follow {events[i]} but does not')
-                deduped_events.append(events[i+1])
-
-        return deduped_events
+        return events
 
diff --git a/src/focaccia/symbolic.py b/src/focaccia/symbolic.py
index 186f18e..49e0259 100644
--- a/src/focaccia/symbolic.py
+++ b/src/focaccia/symbolic.py
@@ -780,15 +780,20 @@ 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):
+            self.next_event += 1
+        else:
+            self.next_event = None
+
+    def post_event(self):
+        self.progress_event()
+
     def is_stepping_instr(self, pc: int, instruction: Instruction):
         if self.nondet_events:
             if self.next_event and self.nondet_events[self.next_event].match(pc, self.target):
                 debug('Current instruction matches next event; stepping through it')
-                if self.next_event < len(self.nondet_events):
-                    self.next_event += 1
-                else:
-                    self.next_event = None
-
+                self.progress_event()
                 return True
         else:
             if self.target.arch.is_instr_syscall(str(instruction)):
@@ -902,5 +907,8 @@ class SymbolicTracer:
 
             strace.append(transform)
 
+            if needs_step:
+                self.post_event()
+
         return Trace(strace, self.env)