diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/focaccia/symbolic.py | 9 | ||||
| -rwxr-xr-x | src/focaccia/tools/capture_transforms.py | 11 | ||||
| -rw-r--r-- | src/focaccia/utils.py | 4 |
3 files changed, 22 insertions, 2 deletions
diff --git a/src/focaccia/symbolic.py b/src/focaccia/symbolic.py index 45bbc22..e6c919a 100644 --- a/src/focaccia/symbolic.py +++ b/src/focaccia/symbolic.py @@ -751,11 +751,14 @@ class SymbolicTracer: return None return self.target.read_pc() - def trace(self, start_addr: int | None = None) -> Trace[SymbolicTransform]: + def trace(self, + start_addr: int | None = None, + stop_addr: int | None = None) -> Trace[SymbolicTransform]: """Execute a program and compute state transformations between executed instructions. :param start_addr: Address from which to start tracing. + :param stop_addr: Address until which to trace. """ # Set up concrete reference state if start_addr is not None: @@ -773,6 +776,10 @@ class SymbolicTracer: strace: list[SymbolicTransform] = [] while not self.target.is_exited(): pc = self.target.read_pc() + + if stop_addr is not None and pc == stop_addr: + break + assert(pc != 0) # Disassemble instruction at the current PC diff --git a/src/focaccia/tools/capture_transforms.py b/src/focaccia/tools/capture_transforms.py index 7e28ed3..d742994 100755 --- a/src/focaccia/tools/capture_transforms.py +++ b/src/focaccia/tools/capture_transforms.py @@ -37,6 +37,14 @@ def main(): default=False, action='store_true', help='Capture transforms in debug mode to identify errors in Focaccia itself') + prog.add_argument('--start-address', + default=None, + type=utils.to_int, + help='Set a starting address from which to collect the symoblic trace') + prog.add_argument('--stop-address', + default=None, + type=utils.to_int, + help='Set a final address up until which to collect the symoblic trace') args = prog.parse_args() if args.debug: @@ -67,7 +75,8 @@ def main(): env = TraceEnvironment(args.binary, args.args, utils.get_envp(), nondeterminism_log=detlog) tracer = SymbolicTracer(env, remote=args.remote, cross_validate=args.cross_validate, force=args.force) - trace = tracer.trace() + + trace = tracer.trace(start_addr=args.start_address, stop_addr=args.stop_address) with open(args.output, 'w') as file: parser.serialize_transformations(trace, file) diff --git a/src/focaccia/utils.py b/src/focaccia/utils.py index c4f6a74..efbb6b2 100644 --- a/src/focaccia/utils.py +++ b/src/focaccia/utils.py @@ -114,3 +114,7 @@ def print_result(result, min_severity: ErrorSeverity): f' (showing {min_severity} and higher).') print('#' * 60) print() + +def to_int(value: str) -> int: + return int(value, 0) + |