Refactor comparison and user-facing logic

Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>

1 files changed, 45 insertions, 45 deletions

diff --git a/focaccia.py b/focaccia.py
index bbd1317..032615b 100755
--- a/focaccia.py
+++ b/focaccia.py
@@ -1,19 +1,25 @@
-#! /bin/python3
+#! /usr/bin/env python3
 
 import argparse
 import platform
 from typing import Iterable
 
-from focaccia.arch import x86
-from focaccia.compare import compare_simple, compare_symbolic, \
-                             ErrorSeverity, ErrorTypes
+from focaccia.arch import supported_architectures
+from focaccia.compare import compare_simple, compare_symbolic, ErrorTypes
 from focaccia.lldb_target import LLDBConcreteTarget
 from focaccia.parser import parse_arancini
 from focaccia.snapshot import ProgramState
 from focaccia.symbolic import SymbolicTransform, collect_symbolic_trace
 from focaccia.utils import print_result
 
-def run_native_execution(oracle_program: str, breakpoints: Iterable[int]):
+verbosity = {
+    'info':    ErrorTypes.INFO,
+    'warning': ErrorTypes.POSSIBLE,
+    'error':   ErrorTypes.CONFIRMED,
+}
+
+def collect_concrete_trace(oracle_program: str, breakpoints: Iterable[int]) \
+        -> list[ProgramState]:
     """Gather snapshots from a native execution via an external debugger.
 
     :param oracle_program: Program to execute.
@@ -22,8 +28,6 @@ def run_native_execution(oracle_program: str, breakpoints: Iterable[int]):
 
     :return: A list of snapshots gathered from the execution.
     """
-    assert(platform.machine() == "x86_64")
-
     target = LLDBConcreteTarget(oracle_program)
 
     # Set breakpoints
@@ -75,19 +79,6 @@ def match_traces(test: list[ProgramState], truth: list[SymbolicTransform]):
 
     return test, truth
 
-def parse_inputs(txl_path, program):
-    # Our architecture
-    arch = x86.ArchX86()
-
-    with open(txl_path, "r") as txl_file:
-        txl = parse_arancini(txl_file, arch)
-
-    with open(txl_path, "r") as txl_file:
-        breakpoints = [state.read_register('PC') for state in txl]
-        ref = run_native_execution(program, breakpoints)
-
-    return txl, ref
-
 def parse_arguments():
     parser = argparse.ArgumentParser(description='Comparator for emulator logs to reference')
     parser.add_argument('-p', '--program',
@@ -96,7 +87,6 @@ def parse_arguments():
                         help='Path to oracle program')
     parser.add_argument('-a', '--program-arg',
                         type=str,
-                        required=False,
                         default=[],
                         action='append',
                         help='Arguments to the program specified with --program.')
@@ -110,42 +100,52 @@ def parse_arguments():
                         help='Use an advanced algorithm that uses symbolic'
                              ' execution to determine accurate data'
                              ' transformations. This improves the quality of'
-                             ' generated errors significantly, but may take'
-                             ' more time to run.')
+                             ' generated errors significantly, but will take'
+                             ' more time to complete.')
     parser.add_argument('--error-level',
                         type=str,
-                        default='verbose',
-                        choices=['verbose', 'errors', 'restricted'],
-                        help='Verbosity of reported errors. \'errors\' reports'
-                             ' everything that might be an error in the'
-                             ' translation, while \'verbose\' may report'
-                             ' additional errors from incomplete input'
-                             ' data, etc. [Default: verbose]')
+                        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]')
     args = parser.parse_args()
     return args
 
 def main():
-    verbosity = {
-        'verbose': ErrorTypes.INFO,
-        'errors': ErrorTypes.POSSIBLE,
-        'restricted': ErrorTypes.CONFIRMED,
-    }
     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()]
+
     txl_path = args.txl
-    program = args.program
-    prog_args = args.program_arg
-    txl, ref = parse_inputs(txl_path, program)
+    oracle = args.program
+    oracle_args = args.program_arg
 
-    if args.symbolic:
-        assert(program is not None)
+    # Parse reference trace
+    with open(txl_path, "r") as txl_file:
+        test_states = parse_arancini(txl_file, arch)
 
-        print(f'Tracing {program} symbolically with arguments {prog_args}...')
-        transforms = collect_symbolic_trace(program, prog_args)
-        txl, transforms = match_traces(txl, transforms)
-        result = compare_symbolic(txl, transforms)
+    # Compare reference trace to a truth
+    if args.symbolic:
+        print(f'Tracing {oracle} symbolically with arguments {oracle_args}...')
+        transforms = collect_symbolic_trace(oracle, oracle_args)
+        test_states, transforms = match_traces(test_states, transforms)
+        result = compare_symbolic(test_states, transforms)
     else:
-        result = compare_simple(txl, ref)
+        # Record truth states from a concrete execution of the oracle
+        breakpoints = [state.read_register('PC') for state in test_states]
+        truth = collect_concrete_trace(oracle, breakpoints)
+        result = compare_simple(test_states, truth)
 
     print_result(result, verbosity[args.error_level])