Migrate to nix flakes, uv and pyproject toml for builds

1 files changed, 0 insertions, 222 deletions

diff --git a/focaccia.py b/focaccia.py
deleted file mode 100755
index f0c6efe..0000000
--- a/focaccia.py
+++ /dev/null
@@ -1,222 +0,0 @@
-#!/usr/bin/env python3
-
-import argparse
-import platform
-from typing import Callable, Iterable
-
-import focaccia.parser as parser
-from focaccia.arch import supported_architectures, Arch
-from focaccia.compare import compare_simple, compare_symbolic, ErrorTypes
-from focaccia.lldb_target import LLDBConcreteTarget
-from focaccia.match import fold_traces, match_traces
-from focaccia.snapshot import ProgramState
-from focaccia.symbolic import collect_symbolic_trace, SymbolicTransform
-from focaccia.utils import print_result, get_envp
-from focaccia.reproducer import Reproducer
-from focaccia.compare import ErrorSeverity
-from focaccia.trace import Trace, TraceEnvironment
-
-verbosity = {
-    'info':    ErrorTypes.INFO,
-    'warning': ErrorTypes.POSSIBLE,
-    'error':   ErrorTypes.CONFIRMED,
-}
-
-concrete_trace_parsers = {
-    'focaccia': lambda f, _: parser.parse_snapshots(f),
-    'qemu':     parser.parse_qemu,
-    'arancini': parser.parse_arancini,
-}
-
-_MatchingAlgorithm = Callable[
-    [list[ProgramState], list[SymbolicTransform]],
-    tuple[list[ProgramState], list[SymbolicTransform]]
-]
-
-matching_algorithms: dict[str, _MatchingAlgorithm] = {
-    'none':   lambda c, s: (c, s),
-    'simple': match_traces,
-    'fold':   fold_traces,
-}
-
-def collect_concrete_trace(env: TraceEnvironment, breakpoints: Iterable[int]) \
-        -> list[ProgramState]:
-    """Gather snapshots from a native execution via an external debugger.
-
-    :param env: Program to execute and the environment in which to execute it.
-    :param breakpoints: List of addresses at which to break and record the
-                        program's state.
-
-    :return: A list of snapshots gathered from the execution.
-    """
-    target = LLDBConcreteTarget(env.binary_name, env.argv, env.envp)
-
-    # Set breakpoints
-    for address in breakpoints:
-        target.set_breakpoint(address)
-
-    # Execute the native program
-    snapshots = []
-    while not target.is_exited():
-        snapshots.append(target.record_snapshot())
-        target.run()
-
-    return snapshots
-
-def parse_arguments():
-    parser = argparse.ArgumentParser()
-    parser.description = '''An emulator tester and verifier.
-
-You can pre-record symbolic traces with `tools/capture_transforms.py`, then pass
-them to the verifier with the --oracle-trace argument.
-'''
-
-    # Specification of the symbolic truth trace
-    symb_trace = parser.add_mutually_exclusive_group(required=True)
-    symb_trace.add_argument('-p', '--oracle-program',
-                            help='A program from which a symbolic truth will be'
-                                 ' recorded.')
-    symb_trace.add_argument('-o', '--oracle-trace', '--symb-trace',
-                            help='A symbolic trace that serves as a truth state'
-                                 ' for comparison.')
-    parser.add_argument('-a', '--oracle-args',
-                        nargs='*',
-                        default=[],
-                        help='Arguments to the oracle program.')
-    parser.add_argument('-e', '--oracle-env',
-                        nargs='*',
-                        help='Override the oracle program\'s environment during'
-                             ' symbolic and concrete execution.')
-
-    # Specification of the concrete test trace
-    parser.add_argument('-t', '--test-trace',
-                        required=True,
-                        help='The concrete test states to test against the'
-                             ' symbolic truth.')
-    parser.add_argument('--test-trace-type',
-                        default='focaccia',
-                        choices=list(concrete_trace_parsers.keys()),
-                        help='Log file format of the tested program trace.'
-                             ' [Default: focaccia]')
-
-    # Algorithm and output control
-    parser.add_argument('--match',
-                        choices=list(matching_algorithms.keys()),
-                        default='simple',
-                        help='Select an algorithm to match the test trace to'
-                             ' the truth trace. Only applicable if --symbolic'
-                             ' is enabled.'
-                             ' [Default: simple]')
-    parser.add_argument('--symbolic',
-                        action='store_true',
-                        default=False,
-                        help='Use an advanced algorithm that uses symbolic'
-                             ' execution to determine accurate data'
-                             ' transformations. This improves the quality of'
-                             ' generated errors significantly, but will take'
-                             ' more time to complete.')
-    parser.add_argument('--error-level',
-                        default='warning',
-                        choices=list(verbosity.keys()),
-                        help='Verbosity of reported errors. \'error\' only'
-                             ' reports mismatches that have been detected as'
-                             ' errors in the translation with certainty.'
-                             ' \'warning\' will report possible errors that'
-                             ' may as well stem from incomplete input data.'
-                             ' \'info\' will report absolutely everything.'
-                             ' [Default: warning]')
-    parser.add_argument('--no-verifier',
-                        action='store_true',
-                        default=False,
-                        help='Don\'t print verifier output.')
-
-    # Reproducer
-    parser.add_argument('--reproducer',
-                        action='store_true',
-                        default=False,
-                        help='Generate repoducer executables for detected'
-                             ' errors.')
-
-    return parser.parse_args()
-
-def print_reproducer(result, min_severity: ErrorSeverity, oracle, oracle_args):
-    for res in result:
-        errs = [e for e in res['errors'] if e.severity >= min_severity]
-        #breakpoint()
-        if errs:
-            rep = Reproducer(oracle, oracle_args, res['snap'], res['ref'])
-            print(rep.asm())
-            return
-
-def get_test_trace(args, arch: Arch) -> Trace[ProgramState]:
-    path = args.test_trace
-    parser = concrete_trace_parsers[args.test_trace_type]
-    with open(path, 'r') as txl_file:
-        return parser(txl_file, arch)
-
-def get_truth_env(args) -> TraceEnvironment:
-    oracle = args.oracle_program
-    oracle_args = args.oracle_args
-    if args.oracle_env:
-        oracle_env = args.oracle_env
-    else:
-        oracle_env = get_envp()
-    return TraceEnvironment(oracle, oracle_args, oracle_env)
-
-def get_symbolic_trace(args):
-    if args.oracle_program:
-        env = get_truth_env(args)
-        print('Tracing', env)
-        return collect_symbolic_trace(env)
-    elif args.oracle_trace:
-        with open(args.oracle_trace, 'r') as file:
-            return parser.parse_transformations(file)
-    raise AssertionError()
-
-def main():
-    args = parse_arguments()
-
-    # Determine the current machine's architecture. The log type must match the
-    # architecture on which focaccia is executed because focaccia wants to
-    # execute the reference program concretely.
-    if platform.machine() not in supported_architectures:
-        print(f'Machine {platform.machine()} is not supported! Exiting.')
-        exit(1)
-    arch = supported_architectures[platform.machine()]
-
-    # Parse reference trace
-    test_trace = get_test_trace(args, arch)
-
-    # Compare reference trace to a truth
-    if args.symbolic:
-        symb_trace = get_symbolic_trace(args)
-        match = matching_algorithms[args.match]
-        conc, symb = match(test_trace.states, symb_trace.states)
-
-        result = compare_symbolic(conc, symb)
-        oracle_env = symb_trace.env
-    else:
-        if not args.oracle_program:
-            print('Argument --oracle-program is required for non-symbolic'
-                  ' verification!')
-            exit(1)
-
-        # Record truth states from a concrete execution of the oracle
-        breakpoints = [state.read_register('PC') for state in test_trace]
-        env = get_truth_env(args)
-        truth_trace = collect_concrete_trace(env, breakpoints)
-
-        result = compare_simple(test_trace.states, truth_trace)
-        oracle_env = env
-
-    if not args.no_verifier:
-        print_result(result, verbosity[args.error_level])
-
-    if args.reproducer:
-        print_reproducer(result,
-                         verbosity[args.error_level],
-                         oracle_env.binary_name,
-                         oracle_env.argv)
-
-if __name__ == '__main__':
-    main()