Add TID marker to collected symbolic transforms

1 files changed, 11 insertions, 7 deletions

diff --git a/src/focaccia/symbolic.py b/src/focaccia/symbolic.py
index 058efe8..b46d9e2 100644
--- a/src/focaccia/symbolic.py
+++ b/src/focaccia/symbolic.py
@@ -127,21 +127,24 @@ class Instruction:
 class SymbolicTransform:
     """A symbolic transformation mapping one program state to another."""
     def __init__(self,
+                 tid: int, 
                  transform: dict[Expr, Expr],
                  instrs: list[Instruction],
                  arch: Arch,
                  from_addr: int,
                  to_addr: int):
         """
+        :param tid: The thread ID that executed the instructions effecting the transformation.
         :param transform: A map of input symbolic expressions and output symbolic expressions.
         :param instrs: A list of instructions. The transformation
                        represents the collective modifications to the program state
                        performed by these instructions.
-        :param arch: The architecture of the symbolic transformaion.
+        :param arch: The architecture of the symbolic transformation.
         :param from_addr: The starting address of the instruction effecting the symbolic
                           transformation.
         :param to_addr: The final address of the last instruction in the instructions list.
         """
+        self.tid = tid
         self.arch = arch
 
         self.addr = from_addr
@@ -394,11 +397,12 @@ class SymbolicTransform:
                 raise ValueError(f'[In SymbolicTransform.from_json] Unable to parse'
                                  f' instruction string "{text}": {err}.') from None
 
+        tid = int(data['tid'])
         arch = supported_architectures[data['arch']]
         start_addr = int(data['from_addr'])
         end_addr = int(data['to_addr'])
 
-        t = SymbolicTransform({}, [], arch, start_addr, end_addr)
+        t = SymbolicTransform(tid, {}, [], arch, start_addr, end_addr)
         t.changed_regs = { name: parse(val) for name, val in data['regs'].items() }
         t.changed_mem = { parse(addr): parse(val) for addr, val in data['mem'].items() }
         instrs = [decode_inst(b, arch) for b in data['instructions']]
@@ -420,13 +424,13 @@ class SymbolicTransform:
             except Exception as err:
                 # Note: from None disables chaining in traceback
                 raise Exception(f'[In SymbolicTransform.to_json] Unable to serialize'
-                                f' "{inst}" as string: {err}. This instruction will not'
-                                f' be serialized.') from None
+                                f' "{inst}" as string: {err}') from None
 
         instrs = [encode_inst(inst) for inst in self.instructions]
         instrs = [inst for inst in instrs if inst is not None]
         return {
             'arch': self.arch.archname,
+            'tid': self.tid,
             'from_addr': self.range[0],
             'to_addr': self.range[1],
             'instructions': instrs,
@@ -436,7 +440,7 @@ class SymbolicTransform:
 
     def __repr__(self) -> str:
         start, end = self.range
-        res = f'Symbolic state transformation {start} -> {end}:\n'
+        res = f'Symbolic state transformation [{self.tid}] {start} -> {end}:\n'
         res += '  [Symbols]\n'
         for reg, expr in self.changed_regs.items():
             res += f'    {reg:6s} = {expr}\n'
@@ -900,7 +904,7 @@ class SymbolicTracer:
                 # We verify the symbolic execution backend on the fly for some
                 # additional protection from bugs in the backend.
                 new_pc = int(new_pc)
-                transform = SymbolicTransform(modified, [instruction], arch, pc, new_pc)
+                transform = SymbolicTransform(tid, modified, [instruction], arch, pc, new_pc)
                 pred_regs, pred_mems = self.predict_next_state(instruction, transform)
                 self.progress(new_pc, step=is_event)
 
@@ -917,7 +921,7 @@ class SymbolicTracer:
                     transform = SymbolicTransform(tid, modified, [instruction], arch, pc, 0)
                     strace.append(transform)
                     continue # we're done
-                transform = SymbolicTransform(modified, [instruction], arch, pc, new_pc)
+                transform = SymbolicTransform(tid, modified, [instruction], arch, pc, new_pc)
 
             strace.append(transform)