diff options
| -rw-r--r-- | src/focaccia/_deterministic_impl.py | 11 | ||||
| -rw-r--r-- | src/focaccia/deterministic.py | 40 | ||||
| -rw-r--r-- | src/focaccia/symbolic.py | 51 |
3 files changed, 64 insertions, 38 deletions
diff --git a/src/focaccia/_deterministic_impl.py b/src/focaccia/_deterministic_impl.py index 1d784cb..fc99280 100644 --- a/src/focaccia/_deterministic_impl.py +++ b/src/focaccia/_deterministic_impl.py @@ -221,10 +221,17 @@ class DeterministicLog: arch = event.arch if arch == rr_trace.Arch.x8664: regs = parse_x64_registers(event.registers.raw) - return regs['rip'], regs + if event.event.which() == 'syscall': + regs['rip'] -= 2 + pc = regs['rip'] + return pc, regs if arch == rr_trace.Arch.aarch64: regs = parse_aarch64_registers(event.registers.raw) - return regs['pc'], regs + if event.event.which() == 'syscall': + regs['pc'] -= 4 + pc = regs['pc'] + return pc, regs + return pc, regs raise NotImplementedError(f'Unable to parse registers for architecture {arch}') def parse_memory_writes(event: Frame, reader: io.RawIOBase) -> list[MemoryWrite]: diff --git a/src/focaccia/deterministic.py b/src/focaccia/deterministic.py index 84fcace..7186f5d 100644 --- a/src/focaccia/deterministic.py +++ b/src/focaccia/deterministic.py @@ -47,14 +47,13 @@ class Event: self.mem_writes = memory_writes self.event_type = event_type - def match(self, pc: int, target: ReadableProgramState) -> bool: + def match(self, target) -> bool: # TODO: match the rest of the state to be sure - if self.pc == pc: + if self.pc == target.read_pc(): for reg, value in self.registers.items(): if value == self.pc: continue if target.read_register(reg) != value: - print(f'Failed match for {reg}: {hex(value)} != {hex(target.read_register(reg))}') return False return True return False @@ -293,4 +292,39 @@ except Exception: def events(self) -> list[Event]: return [] def tasks(self) -> list[Event]: return [] def mmaps(self) -> list[Event]: return [] +finally: + class DeterministicEventIterator: + def __init__(self, deterministic_log: DeterministicLog): + self._detlog = deterministic_log + self._events = self._detlog.events() + self._idx: int | None = 0 # None represents no current event + + def events(self) -> list[Event]: + return self._events + + def current_event(self) -> Event | None: + if self._idx and self._idx < len(self._events): + return self._events[self._idx] + return None + + def update(self, target: ReadableProgramState) -> Event | None: + if self._idx is None: + self._idx = 0 + + for idx in range(self._idx+1, len(self._events)): + if self._events[idx].match(target): + self._idx = idx + return self.current_event() + self._idx = None + return None + + def next(self) -> Event | None: + if self._idx is None: + return None + + self._idx += 1 + return self.current_event() + + def __bool__(self) -> bool: + return len(self.events()) > 0 diff --git a/src/focaccia/symbolic.py b/src/focaccia/symbolic.py index 2a66a26..7ff36e7 100644 --- a/src/focaccia/symbolic.py +++ b/src/focaccia/symbolic.py @@ -26,6 +26,7 @@ from .miasm_util import MiasmSymbolResolver, eval_expr, make_machine from .snapshot import ReadableProgramState, RegisterAccessError, MemoryAccessError from .trace import Trace, TraceEnvironment from .utils import timebound, TimeoutError +from .deterministic import DeterministicEventIterator logger = logging.getLogger('focaccia-symbolic') debug = logger.debug @@ -729,8 +730,7 @@ class SymbolicTracer: self.cross_validate = cross_validate self.target = SpeculativeTracer(self.create_debug_target()) - self.nondet_events = self.env.detlog.events() - self.next_event: int | None = None + self.nondet_events = DeterministicEventIterator(self.env.detlog) def create_debug_target(self) -> LLDBConcreteTarget: binary = self.env.binary_name @@ -784,33 +784,27 @@ class SymbolicTracer: f' mem[{hex(addr)}:{hex(addr+len(data))}] = {conc_data}.' f'\nFaulty transformation: {transform}') - 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) -> None: - if self.next_event: - if self.nondet_events[self.next_event].pc == 0: + current_event = self.nondet_events.current_event() + if current_event: + if current_event.pc == 0: # Exit sequence debug('Completed exit event') self.target.run() - debug(f'Completed handling event at index {self.next_event}') - self.progress_event() + debug(f'Completed handling event: {current_event}') + self.nondet_events.next() 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() - return True - else: - if self.target.arch.is_instr_syscall(str(instruction)): - return True + # if self.nondet_events: + print(f'{self.nondet_events.current_event()}') + if self.nondet_events.current_event(): + debug('Current instruction matches next event; stepping through it') + self.nondet_events.next() + return True + # else: + # if self.target.arch.is_instr_syscall(str(instruction)): + # return True return False def progress(self, new_pc, step: bool = False) -> int | None: @@ -832,21 +826,12 @@ class SymbolicTracer: if self.env.start_address is not None: self.target.run_until(self.env.start_address) - for i in range(len(self.nondet_events)): - if self.nondet_events[i].pc == self.target.read_pc(): - 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 - ctx = DisassemblyContext(self.target) arch = ctx.arch if logger.isEnabledFor(logging.DEBUG): debug('Tracing program with the following non-deterministic events') - for event in self.nondet_events: + for event in self.nondet_events.events(): debug(event) # Trace concolically @@ -857,7 +842,7 @@ class SymbolicTracer: if self.env.stop_address is not None and pc == self.env.stop_address: break - assert(pc != 0) + self.nondet_events.update(self.target) # Disassemble instruction at the current PC tid = self.target.get_current_tid() |