diff options
| m--------- | miasm | 0 | ||||
| -rw-r--r-- | src/focaccia/arch/arch.py | 15 | ||||
| -rw-r--r-- | src/focaccia/arch/x86.py | 6 | ||||
| -rw-r--r-- | src/focaccia/compare.py | 34 | ||||
| -rw-r--r-- | src/focaccia/symbolic.py | 13 |
5 files changed, 56 insertions, 12 deletions
diff --git a/miasm b/miasm -Subproject 2aee2e1313847cfbf88acd07143456e51989860 +Subproject 083c88f096d1b654069eff874356df7b2ecd460 diff --git a/src/focaccia/arch/arch.py b/src/focaccia/arch/arch.py index 234b0d9..a1b0671 100644 --- a/src/focaccia/arch/arch.py +++ b/src/focaccia/arch/arch.py @@ -80,7 +80,7 @@ class Arch(): return self._accessors.get(_regname, None) def get_reg_reader(self, regname: str) -> Callable[[], int] | None: - """Read a register directly from Focaccia + """Read a register directly from Focaccia. :param name: The register to read. :return: The register value. @@ -90,6 +90,19 @@ class Arch(): """ return None + def is_instr_uarch_dep(self, instr: str) -> bool: + """Returns true when an instruction is microarchitecturally-dependent. + + :param name: The instruction. + :return: True if microarchitecturally-dependent. + + Microarchitecturally-dependent instructions may have different output on different + microarchitectures, without it representing an error. Such instructions usually denote feature + support, output differences are representative of an error only if a program relies on the + particular microarchitectural features. + """ + return False + def __eq__(self, other): return self.archname == other.archname diff --git a/src/focaccia/arch/x86.py b/src/focaccia/arch/x86.py index 809055e..9ec5c51 100644 --- a/src/focaccia/arch/x86.py +++ b/src/focaccia/arch/x86.py @@ -202,3 +202,9 @@ class ArchX86(Arch): # Apply custom register alias rules return regname_aliases.get(name.upper(), None) + + def is_instr_uarch_dep(self, instr: str) -> bool: + if "XGETBV" in instr.upper(): + return True + return False + diff --git a/src/focaccia/compare.py b/src/focaccia/compare.py index 13f965c..4fea451 100644 --- a/src/focaccia/compare.py +++ b/src/focaccia/compare.py @@ -131,7 +131,8 @@ def compare_simple(test_states: list[ProgramState], def _find_register_errors(txl_from: ProgramState, txl_to: ProgramState, - transform_truth: SymbolicTransform) \ + transform_truth: SymbolicTransform, + is_uarch_dep: bool = False) \ -> list[Error]: """Find errors in register values. @@ -155,6 +156,14 @@ def _find_register_errors(txl_from: ProgramState, )] except RegisterAccessError as err: s, e = transform_truth.range + if is_uarch_dep: + return [Error(ErrorTypes.INCOMPLETE, + f'Register transformations {hex(s)} -> {hex(e)} depend' + f' on the value of microarchitecturally-dependent register {err.regname}, which is not' + f' set in the tested state. Incorrect or missing values for such registers' + f'are errors only if the program relies on them. Such registers generally' + f'denote microarchitectural feature support and not all programs depend on' + f'all features exposed by a microarchitecture')] return [Error(ErrorTypes.INCOMPLETE, f'Register transformations {hex(s)} -> {hex(e)} depend' f' on the value of register {err.regname}, which is not' @@ -172,10 +181,21 @@ def _find_register_errors(txl_from: ProgramState, continue if txl_val != truth_val: - errors.append(Error(ErrorTypes.CONFIRMED, - f'Content of register {regname} is false.' - f' Expected value: {hex(truth_val)}, actual' - f' value in the translation: {hex(txl_val)}.')) + if is_uarch_dep: + errors.append( + Error( + ErrorTypes.POSSIBLE, + f"Content of microarchitecture-specific register {regname} is different." + f"This denotes an error only when relied upon" + f" Expected value: {hex(truth_val)}, actual" + f" value in the translation: {hex(txl_val)}.", + ) + ) + else: + errors.append(Error(ErrorTypes.CONFIRMED, + f'Content of register {regname} is false.' + f' Expected value: {hex(truth_val)}, actual' + f' value in the translation: {hex(txl_val)}.')) return errors def _find_memory_errors(txl_from: ProgramState, @@ -252,8 +272,10 @@ def _find_errors_symbolic(txl_from: ProgramState, to_pc = txl_to.read_register('PC') assert((from_pc, to_pc) == transform_truth.range) + is_uarch_dep = txl_from.arch.is_instr_uarch_dep(transform_truth.instructions[0].to_string()) + errors = [] - errors.extend(_find_register_errors(txl_from, txl_to, transform_truth)) + errors.extend(_find_register_errors(txl_from, txl_to, transform_truth, is_uarch_dep)) errors.extend(_find_memory_errors(txl_from, txl_to, transform_truth)) return errors diff --git a/src/focaccia/symbolic.py b/src/focaccia/symbolic.py index 7b6098e..6ede2c1 100644 --- a/src/focaccia/symbolic.py +++ b/src/focaccia/symbolic.py @@ -122,11 +122,14 @@ class SymbolicTransform: from_addr: int, to_addr: int): """ - :param state: The symbolic transformation in the form of a SimState - object. - :param first_inst: An instruction address. The transformation - represents the modifications to the program state - performed by this instruction. + :param transform: A map of input symbolic expressions and output symbolic expressions. + :param instrs: A list of instructions. The transformation + represents the collective modifications to the program state + performed by these instructions. + :param arch: The architecture of the symbolic transformaion. + :param from_addr: The starting address of the instruction effecting the symbolic + transformation. + :param to_addr: The final address of the last instruction in the instructions list. """ self.arch = arch |