diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/focaccia/miasm_util.py | 21 | ||||
| -rw-r--r-- | src/focaccia/tools/_qemu_tool.py | 25 |
2 files changed, 44 insertions, 2 deletions
diff --git a/src/focaccia/miasm_util.py b/src/focaccia/miasm_util.py index cacc6e8..c9dc4e5 100644 --- a/src/focaccia/miasm_util.py +++ b/src/focaccia/miasm_util.py @@ -86,10 +86,29 @@ def simp_fsub(expr_simp, expr: ExprOp): return expr_simp(ExprInt(res, expr.size)) return expr +def simp_fpconvert_fp64(expr_simp, expr: ExprOp): + from .utils import float_bits_to_uint, uint_bits_to_float, \ + double_bits_to_uint, uint_bits_to_double + + if expr.op != 'fpconvert_fp64': + return expr + + if not len(expr.args) == 1: + raise NotImplementedError(f'fpconvert_fp64 on number of arguments not in 1: {expr.args}') + + operand = expr.args[0] + if operand.is_int(): + if not operand.size == 32: + raise NotImplementedError(f'fpconvert_fp64 on values of size not in 64: {operand.size}') + + res = double_bits_to_uint(uint_bits_to_double(float_bits_to_uint(operand.arg))) + return expr_simp(ExprInt(res, 64)) + return expr + # The expression simplifier used in this module expr_simp = expr_simp_explicit expr_simp.enable_passes({ - ExprOp: [simp_segm, simp_fadd, simp_fsub], + ExprOp: [simp_segm, simp_fadd, simp_fsub, simp_fpconvert_fp64], }) class MiasmSymbolResolver: diff --git a/src/focaccia/tools/_qemu_tool.py b/src/focaccia/tools/_qemu_tool.py index cc97c95..02d150b 100644 --- a/src/focaccia/tools/_qemu_tool.py +++ b/src/focaccia/tools/_qemu_tool.py @@ -13,7 +13,7 @@ from typing import Iterable import focaccia.parser as parser from focaccia.arch import supported_architectures, Arch -from focaccia.compare import compare_symbolic +from focaccia.compare import compare_symbolic, Error, ErrorTypes from focaccia.snapshot import ProgramState, ReadableProgramState, \ RegisterAccessError, MemoryAccessError from focaccia.symbolic import SymbolicTransform, eval_symbol, ExprMem @@ -27,6 +27,15 @@ debug = logger.debug info = logger.info warn = logger.warning +qemu_crash = { + "crashed": False, + "pc": None, + 'txl': None, + 'ref': None, + 'errors': [Error(ErrorTypes.CONFIRMED, "QEMU crashed")], + 'snap': None, +} + class GDBProgramState(ReadableProgramState): from focaccia.arch import aarch64, x86 @@ -315,9 +324,15 @@ def collect_conc_trace(gdb: GDBServerStateIterator, \ if symb_i >= len(strace): break except StopIteration: + # TODO: The conditions may test for the same if stop_addr and pc != stop_addr: raise Exception(f'QEMU stopped at {hex(pc)} before reaching the stop address' f' {hex(stop_addr)}') + if symb_i+1 < len(strace): + qemu_crash["crashed"] = True + qemu_crash["pc"] = strace[symb_i].addr + qemu_crash["ref"] = strace[symb_i] + qemu_crash["snap"] = states[-1] break except Exception as e: print(traceback.format_exc()) @@ -374,6 +389,14 @@ def main(): if not args.quiet: try: res = compare_symbolic(conc_states, matched_transforms) + if qemu_crash["crashed"]: + res.append({ + 'pc': qemu_crash["pc"], + 'txl': None, + 'ref': qemu_crash["ref"], + 'errors': qemu_crash["errors"], + 'snap': qemu_crash["snap"], + }) print_result(res, verbosity[args.error_level]) except Exception as e: raise Exception('Error occured when comparing with symbolic equations: {e}') |