Make cross-validation of results with native execution optional

3 files changed, 34 insertions, 21 deletions

diff --git a/src/focaccia/symbolic.py b/src/focaccia/symbolic.py
index 444145f..321b39d 100644
--- a/src/focaccia/symbolic.py
+++ b/src/focaccia/symbolic.py
@@ -663,8 +663,9 @@ def collect_symbolic_trace(env: TraceEnvironment,
         # Predict next concrete state.
         # We verify the symbolic execution backend on the fly for some
         # additional protection from bugs in the backend.
-        predicted_regs = transform.eval_register_transforms(lldb_state)
-        predicted_mems = transform.eval_memory_transforms(lldb_state)
+        if env.cross_validate:
+            predicted_regs = transform.eval_register_transforms(lldb_state)
+            predicted_mems = transform.eval_memory_transforms(lldb_state)
 
         # Step forward
         target.step()
@@ -674,23 +675,25 @@ def collect_symbolic_trace(env: TraceEnvironment,
         # Verify last generated transform by comparing concrete state against
         # predicted values.
         assert(len(strace) > 0)
-        for reg, val in predicted_regs.items():
-            conc_val = lldb_state.read_register(reg)
-            if conc_val != val:
-                warn(f'Symbolic execution backend generated false equation for'
-                     f' [{hex(instruction.addr)}]: {instruction}:'
-                     f' Predicted {reg} = {hex(val)}, but the'
-                     f' concrete state has value {reg} = {hex(conc_val)}.'
-                     f'\nFaulty transformation: {transform}')
-        for addr, data in predicted_mems.items():
-            conc_data = lldb_state.read_memory(addr, len(data))
-            if conc_data != data:
-                warn(f'Symbolic execution backend generated false equation for'
-                     f' [{hex(instruction.addr)}]: {instruction}: Predicted'
-                     f' mem[{hex(addr)}:{hex(addr+len(data))}] = {data},'
-                     f' but the concrete state has value'
-                     f' mem[{hex(addr)}:{hex(addr+len(data))}] = {conc_data}.'
-                     f'\nFaulty transformation: {transform}')
-                raise Exception()
+        if env.cross_validate:
+            for reg, val in predicted_regs.items():
+                conc_val = lldb_state.read_register(reg)
+                if conc_val != val:
+                    warn(f'Symbolic execution backend generated false equation for'
+                         f' [{hex(instruction.addr)}]: {instruction}:'
+                         f' Predicted {reg} = {hex(val)}, but the'
+                         f' concrete state has value {reg} = {hex(conc_val)}.'
+                         f'\nFaulty transformation: {transform}')
+            for addr, data in predicted_mems.items():
+                conc_data = lldb_state.read_memory(addr, len(data))
+                if conc_data != data:
+                    warn(f'Symbolic execution backend generated false equation for'
+                         f' [{hex(instruction.addr)}]: {instruction}: Predicted'
+                         f' mem[{hex(addr)}:{hex(addr+len(data))}] = {data},'
+                         f' but the concrete state has value'
+                         f' mem[{hex(addr)}:{hex(addr+len(data))}] = {conc_data}.'
+                         f'\nFaulty transformation: {transform}')
+                    raise Exception()
 
     return Trace(strace, env)
+
diff --git a/src/focaccia/tools/capture_transforms.py b/src/focaccia/tools/capture_transforms.py
index 552b855..0b084da 100755
--- a/src/focaccia/tools/capture_transforms.py
+++ b/src/focaccia/tools/capture_transforms.py
@@ -16,9 +16,12 @@ def main():
     prog.add_argument('-o', '--output',
                       default='trace.out',
                       help='Name of output file. (default: trace.out)')
+    prog.add_argument('-c', '--cross-validate',
+                      default=False,
+                      help='Cross-validate symbolic equations with concrete values')
     args = prog.parse_args()
 
-    env = TraceEnvironment(args.binary, args.args, utils.get_envp())
+    env = TraceEnvironment(args.binary, args.args, args.cross_validate, utils.get_envp())
     trace = collect_symbolic_trace(env, None)
     with open(args.output, 'w') as file:
         parser.serialize_transformations(trace, file)
diff --git a/src/focaccia/trace.py b/src/focaccia/trace.py
index 094358f..c72d90f 100644
--- a/src/focaccia/trace.py
+++ b/src/focaccia/trace.py
@@ -10,11 +10,13 @@ class TraceEnvironment:
     def __init__(self,
                  binary: str,
                  argv: list[str],
+                 cross_validate: bool,
                  envp: list[str],
                  binary_hash: str | None = None):
         self.argv = argv
         self.envp = envp
         self.binary_name = binary
+        self.cross_validate = cross_validate
         if binary_hash is None:
             self.binary_hash = file_hash(binary)
         else:
@@ -26,6 +28,7 @@ class TraceEnvironment:
         return cls(
             json['binary_name'],
             json['argv'],
+            json['cross_validate'],
             json['envp'],
             json['binary_hash'],
         )
@@ -36,6 +39,7 @@ class TraceEnvironment:
             'binary_name': self.binary_name,
             'binary_hash': self.binary_hash,
             'argv': self.argv,
+            'cross_validate': self.cross_validate,
             'envp': self.envp,
         }
 
@@ -46,11 +50,13 @@ class TraceEnvironment:
         return self.binary_name == other.binary_name \
             and self.binary_hash == other.binary_hash \
             and self.argv == other.argv \
+            and self.cross_validate == other.cross_validate \
             and self.envp == other.envp
 
     def __repr__(self) -> str:
         return f'{self.binary_name} {" ".join(self.argv)}' \
                f'\n   bin-hash={self.binary_hash}' \
+               f'\n   options=cross-validate' \
                f'\n   envp={repr(self.envp)}'
 
 class Trace(Generic[T]):
@@ -72,3 +78,4 @@ class Trace(Generic[T]):
     def __repr__(self) -> str:
         return f'Trace with {len(self.states)} trace points.' \
                f' Environment: {repr(self.env)}'
+