about summary refs log tree commit diff stats
diff options
context:
space:
mode:
authorTheofilos Augoustis <theofilos.augoustis@gmail.com>2025-10-31 16:20:14 +0000
committerTheofilos Augoustis <theofilos.augoustis@gmail.com>2025-11-06 17:23:55 +0000
commit6236e4857c124e3b8d32d8c2ff018a88071b8c9c (patch)
tree1f7ea845a5925dc5077ab99335ebe4f17d245120
parentba2199f6d833d724c9dfa557476de8bdf2cd8f68 (diff)
downloadfocaccia-6236e4857c124e3b8d32d8c2ff018a88071b8c9c.tar.gz
focaccia-6236e4857c124e3b8d32d8c2ff018a88071b8c9c.zip
Do not deduplicate but handle post events
-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 fa20942..440e39c 100644
--- a/src/focaccia/symbolic.py
+++ b/src/focaccia/symbolic.py
@@ -782,15 +782,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)):
@@ -904,5 +909,8 @@ class SymbolicTracer:
 
             strace.append(transform)
 
+            if needs_step:
+                self.post_event()
+
         return Trace(strace, self.env)