diff --git a/decompiler/backend/cexpressiongenerator.py b/decompiler/backend/cexpressiongenerator.py index 30b6553bd..7adf47399 100644 --- a/decompiler/backend/cexpressiongenerator.py +++ b/decompiler/backend/cexpressiongenerator.py @@ -307,11 +307,11 @@ def _get_integer_literal_value(self, literal: expressions.Constant[Integer]) -> def _interpret_integer_literal_type(value: int) -> Integer: """Return the type that a C compiler would use for a literal of this value.""" # Precedence: int -> uint -> long -> ulong -> ll -> ull (i32, u32, i64, u64) - if -(2 ** 31) <= value < 2 ** 31: + if -(2**31) <= value < 2**31: return Integer.int32_t() - elif 0 <= value < 2 ** 32: + elif 0 <= value < 2**32: return Integer.uint32_t() - elif -(2 ** 63) <= value < 2 ** 63: # i64 + elif -(2**63) <= value < 2**63: # i64 return Integer.int64_t() else: return Integer.uint64_t() diff --git a/decompiler/pipeline/dataflowanalysis/array_access_detection.py b/decompiler/pipeline/dataflowanalysis/array_access_detection.py index 68f6d518d..f4be4eca0 100644 --- a/decompiler/pipeline/dataflowanalysis/array_access_detection.py +++ b/decompiler/pipeline/dataflowanalysis/array_access_detection.py @@ -219,7 +219,7 @@ def _parse_offset(self, offset: Expression) -> Optional[Tuple[str, Variable, int var = vars[0] if isinstance(vars[0], Variable) else vars[0].operand if self._is_left_shift(offset) and offset.right == constant: - return "mul", var, 2 ** constant.value + return "mul", var, 2**constant.value if self._is_multiplication(offset) and constant.value % 2 == 0: # test % 2 for array of structs return "mul", var, constant.value return None diff --git a/decompiler/pipeline/dataflowanalysis/dead_loop_elimination.py b/decompiler/pipeline/dataflowanalysis/dead_loop_elimination.py index 91aa1550f..f821f336d 100644 --- a/decompiler/pipeline/dataflowanalysis/dead_loop_elimination.py +++ b/decompiler/pipeline/dataflowanalysis/dead_loop_elimination.py @@ -7,10 +7,12 @@ from decompiler.structures.graphs.cfg import BasicBlock, ControlFlowGraph, GraphEdgeInterface from decompiler.structures.graphs.interface import GraphInterface from decompiler.structures.maps import DefMap, UseMap +from decompiler.structures.pseudo.delogic_logic import DelogicConverter from decompiler.structures.pseudo.expressions import Constant, Variable from decompiler.structures.pseudo.instructions import Branch, GenericBranch, IndirectBranch, Phi -from decompiler.structures.pseudo.logic import Z3Converter +from decompiler.structures.pseudo.logic import BaseConverter from decompiler.structures.pseudo.operations import Condition +from decompiler.structures.pseudo.z3_logic import Z3Converter from decompiler.task import DecompilerTask from .dead_path_elimination import DeadPathElimination @@ -26,7 +28,7 @@ class DeadLoopElimination(DeadPathElimination, PipelineStage): def __init__(self): """Initialize a new loop elimination.""" - self._logic_converter: Z3Converter = Z3Converter() + self._logic_converter: BaseConverter = Z3Converter() self._use_map: Optional[UseMap] = None self._def_map: Optional[DefMap] = None self._bb_of_def: Optional[Dict[Variable, BasicBlock]] = None @@ -36,6 +38,9 @@ def __init__(self): def run(self, task: DecompilerTask) -> None: """Run dead loop elimination on the given task object.""" self._timeout = task.options.getint(f"{self.name}.timeout_satisfiable") + self.engine = task.options.getstring("logic-engine.engine") # choice of z3 or delogic + if self.engine == "delogic": + self._logic_converter = DelogicConverter() if not task.graph.root: warning(f"[{self.__class__.__name__}] Can not detect dead blocks because the cfg has no head.") return @@ -87,7 +92,7 @@ def _evaluate_branch_condition( Evaluate Branch.condition with z3 and return (satisfiable edge, unsatisfiable edge) if one edge is unsatisfiable. """ try: - condition = self._logic_converter.convert(condition) + condition = self._logic_converter.convert(condition, define_expr=True) except ValueError as value_error: warning(f"[{self.__class__.__name__}] {str(value_error)}") return None diff --git a/decompiler/pipeline/dataflowanalysis/dead_path_elimination.py b/decompiler/pipeline/dataflowanalysis/dead_path_elimination.py index af03341b0..db62dfcf3 100644 --- a/decompiler/pipeline/dataflowanalysis/dead_path_elimination.py +++ b/decompiler/pipeline/dataflowanalysis/dead_path_elimination.py @@ -1,13 +1,16 @@ """Module implementing the DeadPathElimination pipeline stage.""" from logging import info, warning -from typing import Iterator, Optional, Set +from typing import Iterator, Optional, Set, Union from decompiler.pipeline.stage import PipelineStage from decompiler.structures.graphs.cfg import BasicBlock, BasicBlockEdge, ControlFlowGraph, FalseCase, UnconditionalEdge +from decompiler.structures.pseudo.delogic_logic import DelogicConverter from decompiler.structures.pseudo.instructions import Branch, GenericBranch, IndirectBranch, Phi -from decompiler.structures.pseudo.logic import Z3Converter +from decompiler.structures.pseudo.logic import BaseConverter +from decompiler.structures.pseudo.z3_logic import Z3Converter from decompiler.task import DecompilerTask -from z3 import BoolRef, Not +from simplifier.world.nodes import WorldObject +from z3 import BoolRef class DeadPathElimination(PipelineStage): @@ -17,12 +20,15 @@ class DeadPathElimination(PipelineStage): def __init__(self): """Initialize a new path elimination.""" - self._logic_converter: Z3Converter = Z3Converter() + self._logic_converter: BaseConverter = Z3Converter() self._timeout: Optional[int] = None def run(self, task: DecompilerTask) -> None: """Run dead path elimination on the given task object.""" self._timeout = task.options.getint(f"{self.name}.timeout_satisfiable") + self.engine = task.options.getstring("logic-engine.engine") # choice of z3 or delogic + if self.engine == "delogic": + self._logic_converter = DelogicConverter() if task.graph.root is None: warning(f"[{self.__class__.__name__}] Can not detect dead blocks because the cfg has no head.") return @@ -62,7 +68,7 @@ def find_unsatisfyable_edges(self, graph: ControlFlowGraph) -> Iterator[BasicBlo def _get_invalid_branch_edge(self, graph: ControlFlowGraph, block: BasicBlock, instruction: Branch) -> Optional[BasicBlockEdge]: """Check the edges of the given branch for unsatisfyable branch conditions, returning a dead edge if any.""" try: - condition = self._logic_converter.convert(instruction) + condition = self._logic_converter.convert(instruction, define_expr=True) except ValueError as value_error: warning(f"[{self.__class__.__name__}] {str(value_error)}") return @@ -70,14 +76,14 @@ def _get_invalid_branch_edge(self, graph: ControlFlowGraph, block: BasicBlock, i if self._is_invalid_edge(edge, condition): return edge - def _is_invalid_edge(self, edge: BasicBlockEdge, condition: BoolRef) -> bool: + def _is_invalid_edge(self, edge: BasicBlockEdge, condition: Union[BoolRef, WorldObject]) -> bool: """ Check whether the condition of the given branch is satisfyable or not. Returns a tuple of bools indicating the viability of the true and false branches. """ if isinstance(edge, FalseCase): - condition = Not(condition) + condition = self._logic_converter.negate(condition) return self._logic_converter.is_not_satisfiable(condition, timeout=self._timeout) @staticmethod diff --git a/decompiler/pipeline/preprocessing/register_pair_handling.py b/decompiler/pipeline/preprocessing/register_pair_handling.py index cb2f2e4f9..6bdb968f5 100644 --- a/decompiler/pipeline/preprocessing/register_pair_handling.py +++ b/decompiler/pipeline/preprocessing/register_pair_handling.py @@ -179,7 +179,7 @@ def _get_lower_register_definition_value(var: Variable, register_size_in_bits: i ... var_64_bit // represents x1:x2 of size 64 bits, x1 and x2 are 32 bits x2 = var_64_bit & 0xffffffff // 0xffffffff == 2**32-1 """ - register_size_mask = 2 ** register_size_in_bits - 1 + register_size_mask = 2**register_size_in_bits - 1 return BinaryOperation(OperationType.bitwise_and, [var, Constant(register_size_mask, vartype=Integer(register_size_in_bits, True))]) @staticmethod diff --git a/decompiler/structures/pseudo/__init__.py b/decompiler/structures/pseudo/__init__.py index 97c0c6796..c5408b7b9 100644 --- a/decompiler/structures/pseudo/__init__.py +++ b/decompiler/structures/pseudo/__init__.py @@ -1,3 +1,4 @@ +from .delogic_logic import DelogicConverter from .expressions import ( Constant, DataflowObject, @@ -29,6 +30,6 @@ Relation, Return, ) -from .logic import Z3Converter from .operations import BinaryOperation, Call, Condition, ListOperation, Operation, OperationType, TernaryExpression, UnaryOperation from .typing import CustomType, Float, Integer, Pointer, Type, TypeParser, UnknownType +from .z3_logic import Z3Converter diff --git a/decompiler/structures/pseudo/delogic_logic.py b/decompiler/structures/pseudo/delogic_logic.py new file mode 100644 index 000000000..e78f40d1e --- /dev/null +++ b/decompiler/structures/pseudo/delogic_logic.py @@ -0,0 +1,142 @@ +"""Implements translating pseudo instructions into delogic statements.""" +from __future__ import annotations + +from typing import Generic, Union + +from simplifier.world.nodes import Operation as WorldOperation +from simplifier.world.nodes import Variable as WorldVariable +from simplifier.world.nodes import WorldObject +from simplifier.world.world import World + +from .expressions import Constant, Expression, Variable +from .instructions import Branch +from .logic import BaseConverter +from .operations import Condition, Operation, OperationType + + +class DelogicConverter(BaseConverter): + """Class in charge of converting psudo expressions into Logic statements""" + + def __init__(self): + self._world = World() + self._var_count = 0 + + def convert(self, expression: Union[Expression, Branch], define_expr: bool = False) -> WorldObject: + """Convert a given expression or branch into a logic statement of type WorldObject.""" + converted_expr = super().convert(expression) + if define_expr: + return self.define_expression(converted_expr) + return converted_expr + + def define_expression(self, expr: WorldObject) -> WorldVariable: + """Bind an expression to a WorldVariable.""" + var_name = f"delogic_var_{self._var_count}" + self._var_count += 1 + var = self._world.variable(var_name, expr.size) + self._world.define(var, expr) + return var + + def compare(self, a: WorldObject, b: WorldObject): + """Compare two world objects with each other.""" + return self._world.compare(a, b) + + def false(self) -> WorldObject: + """Return False in Delogic.""" + return self._world.constant(0, 1) + + def negate(self, expr: WorldObject) -> WorldObject: + """Negate a given expression.""" + if isinstance(expr, WorldVariable) and (formula := self._world.get_definition(expr)): + return self._world.bool_negate(formula) + return self._world.bool_negate(expr) + + def check(self, *condition: WorldObject, timeout: int = 2000) -> str: + """Return a string describing whether the given terms are satisfiable.""" + simplified_expr = self._full_simplification(condition[0], timeout) + if self.compare(simplified_expr, self.false()): + return BaseConverter.UNSAT + return BaseConverter.SAT + + def _full_simplification(self, condition: WorldObject, timeout: int = 2000) -> WorldObject: + """Return the full simplification of a condition.""" + result = condition.copy_tree() if isinstance(condition, WorldVariable) else self.define_expression(condition.copy_tree()) + # simplify to fixpoint, stop at timeout so we don't accidentally iterate forever. + for _ in range(timeout): + result_copy = result.copy_tree() + result.simplify() + if self.compare(result_copy, result): + break + return result + + def _convert_variable(self, variable: Variable, default_size: int = 32) -> WorldObject: + """Represent the given variable as a WorldObject.""" + return self._world.from_string(f"{variable.name}@{variable.type.size or default_size}") + + def _convert_constant(self, constant: Constant, default_size: int = 32) -> WorldObject: + """Represent the given constant as a WorldObject.""" + return self._world.from_string(f"{constant.value}@{constant.type.size or default_size}") + + def _convert_branch(self, branch: Branch) -> WorldObject: + """ + Convert the given branch into a WorldObject. + + Condition type Branches can be converted as a BinaryOperation. + When the condition is a single variable or an expression, the condition becomes a check != 0. + """ + if isinstance(branch.condition, Condition): + return self._convert_condition(branch.condition) + return self._convert_condition(Condition(OperationType.not_equal, [branch.condition, Constant(0, branch.condition.type)])) + + def _convert_condition(self, condition: Condition) -> WorldObject: + """ + Convert the given condition into a WorldObject. + + Please note conditions are a special kind of operation returning a boolean value. + """ + return self._get_operation(condition) + + def _convert_operation(self, operation: Operation) -> WorldObject: + """ + Convert the given operation into a WorldObject. + """ + return self._get_operation(operation) + + def _get_operation(self, operation: Operation) -> WorldObject: + """Convert the given operation into a WorldObject expression utilizing the handler functions.""" + converter = self.OPERATIONS.get(operation.operation, None) + if not converter: + raise ValueError(f"Could not convert operation {operation} into World Logic.") + operands = [self.convert(operand) for operand in operation.operands] + + return converter(self._world, *operands) + + OPERATIONS = { + OperationType.plus: lambda w, a, b: w.signed_add(a, b), + OperationType.minus: lambda w, a, b: w.signed_sub(a, b), + OperationType.multiply: lambda w, a, b: w.signed_mul(a, b), + OperationType.divide: lambda w, a, b: w.signed_div(a, b), + OperationType.modulo: lambda w, a, b: w.signed_mod(a, b), + OperationType.bitwise_xor: lambda w, a, b: w.bitwise_xor(a, b), + OperationType.bitwise_or: lambda w, a, b: w.bitwise_or(a, b), + OperationType.bitwise_and: lambda w, a, b: w.bitwise_and(a, b), + OperationType.left_shift: lambda w, a, b: w.shift_left(a, b), + OperationType.right_shift: lambda w, a, b: w.shift_right(a, b), + OperationType.left_rotate: lambda w, a, b: w.rotate_left(a, b), + OperationType.right_rotate: lambda w, a, b: w.rotate_right(a, b), + OperationType.equal: lambda w, a, b: w.bool_equal(a, b), + OperationType.not_equal: lambda w, a, b: w.bool_unequal(a, b), + OperationType.less: lambda w, a, b: w.signed_lt(a, b), + OperationType.less_or_equal: lambda w, a, b: w.signed_le(a, b), + OperationType.greater: lambda w, a, b: w.signed_gt(a, b), + OperationType.greater_or_equal: lambda w, a, b: w.signed_ge(a, b), + OperationType.cast: lambda w, a: a, + OperationType.negate: lambda w, a: w.bitwise_negate(a), + OperationType.logical_not: lambda w, a: w.bool_negate(a), + # unsigned operations + OperationType.divide_us: lambda w, a, b: w.unsigned_div(a, b), + OperationType.modulo_us: lambda w, a, b: w.unsigned_mod(a, b), + OperationType.greater_us: lambda w, a, b: w.unsigned_gt(a, b), + OperationType.less_us: lambda w, a, b: w.unsigned_lt(a, b), + OperationType.greater_or_equal_us: lambda w, a, b: w.unsigned_ge(a, b), + OperationType.less_or_equal_us: lambda w, a, b: w.unsigned_le(a, b), + } diff --git a/decompiler/structures/pseudo/logic.py b/decompiler/structures/pseudo/logic.py index 65568292f..1bfbeccde 100644 --- a/decompiler/structures/pseudo/logic.py +++ b/decompiler/structures/pseudo/logic.py @@ -1,54 +1,26 @@ """Implements translating psuedo instructions into logic statements.""" from __future__ import annotations -import logging -from typing import Iterator, List, Union - -from z3 import ( - UGE, - UGT, - ULE, - ULT, - And, - BitVec, - BitVecRef, - BitVecVal, - BoolRef, - Context, - ExprRef, - Extract, - If, - Not, - Or, - RotateLeft, - RotateRight, - Solver, - UDiv, - URem, - Xor, - ZeroExt, - is_bool, - is_bv, -) +from abc import ABC, abstractmethod +from enum import Enum +from typing import Generic, TypeVar, Union from .expressions import Constant, Expression, Variable -from .instructions import Branch -from .operations import Condition, Operation, OperationType +from .instructions import Branch, GenericBranch +from .operations import Condition, Operation +T = TypeVar("T") -class Z3Converter: - """Class in charge of converting pseudo expressions into z3 logic statements.""" - def __init__(self): - self._context = Context() +class BaseConverter(ABC, Generic[T]): + """Interface for converting pseudo expressions to Logic statements""" - @property - def context(self) -> Context: - """Return the current z3 context.""" - return self._context + SAT = "sat" + UNSAT = "unsat" + UNKNOWN = "unknown" - def convert(self, expression: Union[Expression, Branch]) -> BitVecRef: - """Convert the given expression or Branch into a z3 logic statement.""" + def convert(self, expression: Union[Expression, Branch], **kwargs: T) -> T: + """Convert a given expression or branch into a logic statement of type T.""" if isinstance(expression, Variable): return self._convert_variable(expression) if isinstance(expression, Constant) and (isinstance(expression.value, int) or isinstance(expression.value, float)): @@ -59,157 +31,47 @@ def convert(self, expression: Union[Expression, Branch]) -> BitVecRef: return self._convert_condition(expression) if isinstance(expression, Operation): return self._convert_operation(expression) - raise ValueError(f"Could not convert {expression} into z3 logic.") + raise ValueError(f"Could not convert {expression} into a logic statement.") - def _convert_variable(self, variable: Variable) -> BitVecRef: - """Represent the given Variable as a BitVector in z3.""" - return BitVec(variable.name, variable.type.size if variable.type.size else 32, ctx=self._context) + @abstractmethod + def check(self, *condition: T, timeout: int) -> str: + """Return a string describing whether the given terms are satisfiable.""" + + def is_not_satisfiable(self, *condition: T, timeout: int = 2000) -> bool: + """Check whether a given set of terms is not satisfiable.""" + return self.check(*condition, timeout=timeout) == BaseConverter.UNSAT - def _convert_constant(self, constant: Constant) -> BitVecRef: - """Represent the given variable as a BitVector (no types).""" - return BitVecVal(constant.value, constant.type.size if constant.type.size else 32, ctx=self._context) + def is_satisfiable(self, *condition: T, timeout: int = 2000) -> bool: + """Check whether a given set of terms is satisfiable.""" + return self.check(*condition, timeout=timeout) == BaseConverter.SAT - def _convert_branch(self, branch: Branch) -> BitVecRef: + @abstractmethod + def _convert_variable(self, variable: Variable, **kwargs: T) -> T: + """Represent the given Variable as type T.""" + + @abstractmethod + def _convert_constant(self, constant: Constant, **kwargs: T) -> T: + """Represent the given constant as type T.""" + + @abstractmethod + def _convert_branch(self, branch: Branch, **kwargs: T) -> T: """ - Convert the given branch into z3 logic. + Convert the given branch into type T. Condition type Branches can be converted as a BinaryOperation. When the condition is a single variable or an expression, the condition becomes a check != 0. """ - if isinstance(branch.condition, Condition): - return self._convert_condition(branch.condition) - return self._convert_condition(Condition(OperationType.not_equal, [branch.condition, Constant(0, branch.condition.type)])) - def _convert_condition(self, condition: Condition) -> BitVecRef: + @abstractmethod + def _convert_condition(self, condition: Condition, **kwargs: T) -> T: """ - Convert the given condition into z3 logic. + Convert the given condition into type T. Please note conditions are a special kind of operation returning a boolean value. """ - _operation = self._get_operation(condition) - return self._ensure_bool_sort(_operation) - - def _convert_operation(self, operation: Operation) -> BitVecRef: - """ - Convert the given operation into a z3 logic. - Operations should always be of BitvecRef type. - """ - _operation = self._get_operation(operation) - return self._ensure_bitvec_sort(_operation) - - def _get_operation(self, operation: Operation) -> Union[BoolRef, BitVecRef]: - """Convert the given operation into a z3 expression utilizing the handler functions.""" - operands = self._ensure_same_sort([self.convert(operand) for operand in operation.operands]) - if isinstance(operands[0], BoolRef) and operation.operation in self.OPERATIONS_BOOLREF: - converter = self.OPERATIONS_BOOLREF.get(operation.operation, None) - else: - converter = self.OPERATIONS.get(operation.operation, None) - if not converter: - raise ValueError(f"Could not convert operation {operation} into z3 logic.") - return converter(*operands) - - def _ensure_same_sort(self, operands: List[ExprRef]) -> List[ExprRef]: + @abstractmethod + def _convert_operation(self, operation: Operation, **kwargs: T) -> T: """ - Complicated function ensuring the given operand list has a common sort. - - Converts bv and bool into each other and tries to even out size differences for bit vectors. + Convert the given operation into type T. """ - if any(is_bv(op) for op in operands): - operands = [self._ensure_bitvec_sort(operand) for operand in operands] - operands = list(self._ensure_bv_size(operands)) - elif any(is_bool(op) for op in operands): - operands = [self._ensure_bool_sort(operand) for operand in operands] - return operands - - def _ensure_bitvec_sort(self, expression: ExprRef) -> BitVecRef: - """Ensure that the sort of the given expression is BitVec.""" - if is_bv(expression): - return expression - if is_bool(expression): - return If(expression, BitVecVal(1, 1, ctx=self._context), BitVecVal(0, 1, ctx=self._context), ctx=self._context) - raise ValueError(f"Can not convert {expression}") - - def _ensure_bool_sort(self, expression: ExprRef) -> BitVecRef: - """Ensure that the sort of the given expression is BitVec.""" - if is_bool(expression): - return expression - if is_bv(expression): - return expression != BitVecVal(1, expression.size(), ctx=self._context) - raise ValueError(f"Can not convert {expression}") - - def _ensure_bv_size(self, operands: List[BitVecRef]) -> Iterator[BitVecRef]: - """Ensure all bitvecors given as operands have the same size.""" - desired_size = operands[0].size() - for operand in operands: - operand_size = operand.size() - if operand_size == desired_size: - yield operand - else: - if desired_size > operand_size: - yield ZeroExt(desired_size - operand_size, operand) - else: - yield Extract(desired_size - 1, 0, operand) - - def check(self, *terms: BoolRef, timeout: int = 2000) -> str: - """Return a string describing whether the given terms are satisfiable.""" - solver = Solver(ctx=self._context) - solver.set("timeout", timeout) - for term in terms: - solver.add(term) - result = repr(solver.check()) - if result == "unknown": - logging.warning(f"It could be that z3 was not able to check satisfiability for the given terms in {timeout}ms") - return result - - def is_not_satisfiable(self, *terms: BoolRef, timeout: int = 2000) -> bool: - """Check whether a given set of terms is not satisfiable.""" - return self.check(*terms, timeout=timeout) == "unsat" - - def is_satisfiable(self, *terms: BoolRef, timeout: int = 2000) -> bool: - """Check whether a given set of terms is satisfiable.""" - return self.check(*terms, timeout=timeout) == "sat" - - LOGIC_OPERATIONS = { - OperationType.bitwise_or, - OperationType.bitwise_and, - } - - OPERATIONS = { - OperationType.plus: lambda a, b: a + b, - OperationType.minus: lambda a, b: a - b, - OperationType.multiply: lambda a, b: a * b, - OperationType.divide: lambda a, b: a / b, - OperationType.modulo: lambda a, b: a % b, - OperationType.bitwise_xor: lambda a, b: a ^ b, - OperationType.bitwise_or: lambda a, b: a | b, - OperationType.bitwise_and: lambda a, b: a & b, - OperationType.left_shift: lambda a, b: a << b, - OperationType.right_shift: lambda a, b: a >> b, - OperationType.left_rotate: RotateLeft, - OperationType.right_rotate: RotateRight, - OperationType.equal: lambda a, b: a == b, - OperationType.not_equal: lambda a, b: a != b, - OperationType.less: lambda a, b: a < b, - OperationType.less_or_equal: lambda a, b: a <= b, - OperationType.greater: lambda a, b: a > b, - OperationType.greater_or_equal: lambda a, b: a >= b, - OperationType.cast: lambda a: a, - OperationType.negate: lambda a: -a, - OperationType.logical_not: lambda a: ~a, - # unsigned operations - OperationType.divide_us: UDiv, - OperationType.modulo_us: URem, - OperationType.greater_us: UGT, - OperationType.less_us: ULT, - OperationType.greater_or_equal_us: UGE, - OperationType.less_or_equal_us: ULE, - } - - OPERATIONS_BOOLREF = { - OperationType.bitwise_and: And, - OperationType.bitwise_xor: Xor, - OperationType.bitwise_or: Or, - OperationType.logical_not: Not, - OperationType.negate: Not, - } diff --git a/decompiler/structures/pseudo/z3_logic.py b/decompiler/structures/pseudo/z3_logic.py new file mode 100644 index 000000000..0f8c6cf23 --- /dev/null +++ b/decompiler/structures/pseudo/z3_logic.py @@ -0,0 +1,201 @@ +"""Implements translating psuedo instructions into logic statements.""" +from __future__ import annotations + +import logging +from typing import Iterator, List, Union + +from z3 import ( + UGE, + UGT, + ULE, + ULT, + And, + BitVec, + BitVecRef, + BitVecVal, + BoolRef, + Context, + ExprRef, + Extract, + If, + Not, + Or, + RotateLeft, + RotateRight, + Solver, + UDiv, + URem, + Xor, + ZeroExt, + is_bool, + is_bv, +) + +from .expressions import Constant, Expression, Variable +from .instructions import Branch +from .logic import BaseConverter +from .operations import Condition, Operation, OperationType + + +class Z3Converter(BaseConverter): + """Class in charge of converting pseudo expressions into z3 logic statements.""" + + def __init__(self): + self._context = Context() + + @property + def context(self) -> Context: + """Return the current z3 context.""" + return self._context + + def negate(self, expr: BoolRef) -> BitVecRef: + """Negate a given expression.""" + return Not(expr) + + def _convert_variable(self, variable: Variable) -> BitVecRef: + """Represent the given Variable as a BitVector in z3.""" + return BitVec(variable.name, variable.type.size if variable.type.size else 32, ctx=self._context) + + def _convert_constant(self, constant: Constant) -> BitVecRef: + """Represent the given variable as a BitVector (no types).""" + return BitVecVal(constant.value, constant.type.size if constant.type.size else 32, ctx=self._context) + + def _convert_branch(self, branch: Branch) -> BitVecRef: + """ + Convert the given branch into z3 logic. + + Condition type Branches can be converted as a BinaryOperation. + When the condition is a single variable or an expression, the condition becomes a check != 0. + """ + if isinstance(branch.condition, Condition): + return self._convert_condition(branch.condition) + return self._convert_condition(Condition(OperationType.not_equal, [branch.condition, Constant(0, branch.condition.type)])) + + def _convert_condition(self, condition: Condition) -> BitVecRef: + """ + Convert the given condition into z3 logic. + + Please note conditions are a special kind of operation returning a boolean value. + """ + _operation = self._get_operation(condition) + return self._ensure_bool_sort(_operation) + + def _convert_operation(self, operation: Operation) -> BitVecRef: + """ + Convert the given operation into a z3 logic. + + Operations should always be of BitvecRef type. + """ + _operation = self._get_operation(operation) + return self._ensure_bitvec_sort(_operation) + + def _get_operation(self, operation: Operation) -> Union[BoolRef, BitVecRef]: + """Convert the given operation into a z3 expression utilizing the handler functions.""" + operands = self._ensure_same_sort([self.convert(operand) for operand in operation.operands]) + if isinstance(operands[0], BoolRef) and operation.operation in self.OPERATIONS_BOOLREF: + converter = self.OPERATIONS_BOOLREF.get(operation.operation, None) + else: + converter = self.OPERATIONS.get(operation.operation, None) + if not converter: + raise ValueError(f"Could not convert operation {operation} into z3 logic.") + return converter(*operands) + + def _ensure_same_sort(self, operands: List[ExprRef]) -> List[ExprRef]: + """ + Complicated function ensuring the given operand list has a common sort. + + Converts bv and bool into each other and tries to even out size differences for bit vectors. + """ + if any(is_bv(op) for op in operands): + operands = [self._ensure_bitvec_sort(operand) for operand in operands] + operands = list(self._ensure_bv_size(operands)) + elif any(is_bool(op) for op in operands): + operands = [self._ensure_bool_sort(operand) for operand in operands] + return operands + + def _ensure_bitvec_sort(self, expression: ExprRef) -> BitVecRef: + """Ensure that the sort of the given expression is BitVec.""" + if is_bv(expression): + return expression + if is_bool(expression): + return If(expression, BitVecVal(1, 1, ctx=self._context), BitVecVal(0, 1, ctx=self._context), ctx=self._context) + raise ValueError(f"Can not convert {expression}") + + def _ensure_bool_sort(self, expression: ExprRef) -> BitVecRef: + """Ensure that the sort of the given expression is BitVec.""" + if is_bool(expression): + return expression + if is_bv(expression): + return expression != BitVecVal(1, expression.size(), ctx=self._context) + raise ValueError(f"Can not convert {expression}") + + def _ensure_bv_size(self, operands: List[BitVecRef]) -> Iterator[BitVecRef]: + """Ensure all bitvecors given as operands have the same size.""" + desired_size = operands[0].size() + for operand in operands: + operand_size = operand.size() + if operand_size == desired_size: + yield operand + else: + if desired_size > operand_size: + yield ZeroExt(desired_size - operand_size, operand) + else: + yield Extract(desired_size - 1, 0, operand) + + def check(self, *condition: BoolRef, timeout: int = 2000) -> str: + """Return a string describing whether the given terms are satisfiable.""" + solver = Solver(ctx=self._context) + solver.set("timeout", timeout) + for term in condition: + solver.add(term) + result = repr(solver.check()) + if result == "unknown": + logging.warning(f"It could be that z3 was not able to check satisfiability for the given terms in {timeout}ms") + return BaseConverter.UNKNOWN + elif result == "unsat": + return BaseConverter.UNSAT + return BaseConverter.SAT + + LOGIC_OPERATIONS = { + OperationType.bitwise_or, + OperationType.bitwise_and, + } + + OPERATIONS = { + OperationType.plus: lambda a, b: a + b, + OperationType.minus: lambda a, b: a - b, + OperationType.multiply: lambda a, b: a * b, + OperationType.divide: lambda a, b: a / b, + OperationType.modulo: lambda a, b: a % b, + OperationType.bitwise_xor: lambda a, b: a ^ b, + OperationType.bitwise_or: lambda a, b: a | b, + OperationType.bitwise_and: lambda a, b: a & b, + OperationType.left_shift: lambda a, b: a << b, + OperationType.right_shift: lambda a, b: a >> b, + OperationType.left_rotate: RotateLeft, + OperationType.right_rotate: RotateRight, + OperationType.equal: lambda a, b: a == b, + OperationType.not_equal: lambda a, b: a != b, + OperationType.less: lambda a, b: a < b, + OperationType.less_or_equal: lambda a, b: a <= b, + OperationType.greater: lambda a, b: a > b, + OperationType.greater_or_equal: lambda a, b: a >= b, + OperationType.cast: lambda a: a, + OperationType.negate: lambda a: -a, + OperationType.logical_not: lambda a: ~a, + # unsigned operations + OperationType.divide_us: UDiv, + OperationType.modulo_us: URem, + OperationType.greater_us: UGT, + OperationType.less_us: ULT, + OperationType.greater_or_equal_us: UGE, + OperationType.less_or_equal_us: ULE, + } + + OPERATIONS_BOOLREF = { + OperationType.bitwise_and: And, + OperationType.bitwise_xor: Xor, + OperationType.bitwise_or: Or, + OperationType.logical_not: Not, + OperationType.negate: Not, + } diff --git a/decompiler/util/default.json b/decompiler/util/default.json index 42978c434..a8933a8ac 100644 --- a/decompiler/util/default.json +++ b/decompiler/util/default.json @@ -123,6 +123,15 @@ "is_hidden_from_gui": true } }, + "logic-engine": { + "engine": { + "default": "z3", + "title": "Logic Engine for simplifying conditions", + "type": "string", + "description": "Pick between delogic or z3 for simplifying conditions.", + "is_hidden_from_gui": true + } + }, "dead-path-elimination": { "timeout_satisfiable": { "default": 1000, diff --git a/tests/pipeline/SSA/test_phi_dependency_graph.py b/tests/pipeline/SSA/test_phi_dependency_graph.py index 368a64df1..9bf8ded58 100644 --- a/tests/pipeline/SSA/test_phi_dependency_graph.py +++ b/tests/pipeline/SSA/test_phi_dependency_graph.py @@ -77,16 +77,12 @@ def test_dependency_init(dependency_phi_functions): list_of_phi_functions = dependency_phi_functions graph = PhiDependencyGraph(list_of_phi_functions) - assert ( - set(graph.edges) - == { - (list_of_phi_functions[0], list_of_phi_functions[1]), - (list_of_phi_functions[4], list_of_phi_functions[3]), - (list_of_phi_functions[4], list_of_phi_functions[2]), - (list_of_phi_functions[3], list_of_phi_functions[2]), - } - and set(graph.nodes) == set(list_of_phi_functions) - ) + assert set(graph.edges) == { + (list_of_phi_functions[0], list_of_phi_functions[1]), + (list_of_phi_functions[4], list_of_phi_functions[3]), + (list_of_phi_functions[4], list_of_phi_functions[2]), + (list_of_phi_functions[3], list_of_phi_functions[2]), + } and set(graph.nodes) == set(list_of_phi_functions) def test_dependency_dfvs(dependency_phi_functions): @@ -103,15 +99,11 @@ def test_dependency_update(dependency_phi_functions, variable_x, variable_v): graph.update_dependency_graph(list_of_phi_functions[3], new_phi_function) - assert ( - set(graph.edges) - == { - (list_of_phi_functions[0], list_of_phi_functions[1]), - (list_of_phi_functions[4], list_of_phi_functions[2]), - (new_phi_function, list_of_phi_functions[2]), - } - and set(graph.nodes) == set(list_of_phi_functions[:3] + [list_of_phi_functions[4], new_phi_function]) - ) + assert set(graph.edges) == { + (list_of_phi_functions[0], list_of_phi_functions[1]), + (list_of_phi_functions[4], list_of_phi_functions[2]), + (new_phi_function, list_of_phi_functions[2]), + } and set(graph.nodes) == set(list_of_phi_functions[:3] + [list_of_phi_functions[4], new_phi_function]) @pytest.fixture() @@ -134,20 +126,16 @@ def test_circular_dependency_init(circular_dependency_phi_functions): list_of_phi_functions = circular_dependency_phi_functions graph = PhiDependencyGraph(list_of_phi_functions) - assert ( - set(graph.edges) - == { - (list_of_phi_functions[1], list_of_phi_functions[0]), - (list_of_phi_functions[0], list_of_phi_functions[1]), - (list_of_phi_functions[4], list_of_phi_functions[3]), - (list_of_phi_functions[5], list_of_phi_functions[3]), - (list_of_phi_functions[2], list_of_phi_functions[4]), - (list_of_phi_functions[5], list_of_phi_functions[4]), - (list_of_phi_functions[7], list_of_phi_functions[6]), - (list_of_phi_functions[3], list_of_phi_functions[7]), - } - and set(graph.nodes) == set(list_of_phi_functions) - ) + assert set(graph.edges) == { + (list_of_phi_functions[1], list_of_phi_functions[0]), + (list_of_phi_functions[0], list_of_phi_functions[1]), + (list_of_phi_functions[4], list_of_phi_functions[3]), + (list_of_phi_functions[5], list_of_phi_functions[3]), + (list_of_phi_functions[2], list_of_phi_functions[4]), + (list_of_phi_functions[5], list_of_phi_functions[4]), + (list_of_phi_functions[7], list_of_phi_functions[6]), + (list_of_phi_functions[3], list_of_phi_functions[7]), + } and set(graph.nodes) == set(list_of_phi_functions) def test_circular_dependency_dfvs(circular_dependency_phi_functions): @@ -168,35 +156,27 @@ def test_circular_dependency_update(circular_dependency_phi_functions, variable_ graph.update_dependency_graph(list_of_phi_functions[0], new_phi_function_1) - assert ( - set(graph.edges) - == { - (new_phi_function_1, list_of_phi_functions[1]), - (list_of_phi_functions[4], list_of_phi_functions[3]), - (list_of_phi_functions[5], list_of_phi_functions[3]), - (list_of_phi_functions[2], list_of_phi_functions[4]), - (list_of_phi_functions[5], list_of_phi_functions[4]), - (list_of_phi_functions[7], list_of_phi_functions[6]), - (list_of_phi_functions[3], list_of_phi_functions[7]), - } - and set(graph.nodes) == set(list_of_phi_functions[1:] + [new_phi_function_1]) - ) + assert set(graph.edges) == { + (new_phi_function_1, list_of_phi_functions[1]), + (list_of_phi_functions[4], list_of_phi_functions[3]), + (list_of_phi_functions[5], list_of_phi_functions[3]), + (list_of_phi_functions[2], list_of_phi_functions[4]), + (list_of_phi_functions[5], list_of_phi_functions[4]), + (list_of_phi_functions[7], list_of_phi_functions[6]), + (list_of_phi_functions[3], list_of_phi_functions[7]), + } and set(graph.nodes) == set(list_of_phi_functions[1:] + [new_phi_function_1]) graph.update_dependency_graph(list_of_phi_functions[5], new_phi_function_2) - assert ( - set(graph.edges) - == { - (new_phi_function_1, list_of_phi_functions[1]), - (list_of_phi_functions[4], list_of_phi_functions[3]), - (new_phi_function_2, list_of_phi_functions[3]), - (list_of_phi_functions[2], list_of_phi_functions[4]), - (new_phi_function_2, list_of_phi_functions[4]), - (list_of_phi_functions[7], list_of_phi_functions[6]), - (list_of_phi_functions[3], list_of_phi_functions[7]), - } - and set(graph.nodes) == set(list_of_phi_functions[1:5] + list_of_phi_functions[6:] + [new_phi_function_1, new_phi_function_2]) - ) + assert set(graph.edges) == { + (new_phi_function_1, list_of_phi_functions[1]), + (list_of_phi_functions[4], list_of_phi_functions[3]), + (new_phi_function_2, list_of_phi_functions[3]), + (list_of_phi_functions[2], list_of_phi_functions[4]), + (new_phi_function_2, list_of_phi_functions[4]), + (list_of_phi_functions[7], list_of_phi_functions[6]), + (list_of_phi_functions[3], list_of_phi_functions[7]), + } and set(graph.nodes) == set(list_of_phi_functions[1:5] + list_of_phi_functions[6:] + [new_phi_function_1, new_phi_function_2]) def test_circular_dependency_2_init(circular_dependency_phi_functions, variable_v, variable_u): @@ -204,21 +184,17 @@ def test_circular_dependency_2_init(circular_dependency_phi_functions, variable_ list_of_phi_functions[6].substitute(variable_v[6], variable_u[5]) graph = PhiDependencyGraph(list_of_phi_functions) - assert ( - set(graph.edges) - == { - (list_of_phi_functions[1], list_of_phi_functions[0]), - (list_of_phi_functions[0], list_of_phi_functions[1]), - (list_of_phi_functions[4], list_of_phi_functions[3]), - (list_of_phi_functions[5], list_of_phi_functions[3]), - (list_of_phi_functions[2], list_of_phi_functions[4]), - (list_of_phi_functions[5], list_of_phi_functions[4]), - (list_of_phi_functions[6], list_of_phi_functions[5]), - (list_of_phi_functions[7], list_of_phi_functions[6]), - (list_of_phi_functions[3], list_of_phi_functions[7]), - } - and set(graph.nodes) == set(list_of_phi_functions) - ) + assert set(graph.edges) == { + (list_of_phi_functions[1], list_of_phi_functions[0]), + (list_of_phi_functions[0], list_of_phi_functions[1]), + (list_of_phi_functions[4], list_of_phi_functions[3]), + (list_of_phi_functions[5], list_of_phi_functions[3]), + (list_of_phi_functions[2], list_of_phi_functions[4]), + (list_of_phi_functions[5], list_of_phi_functions[4]), + (list_of_phi_functions[6], list_of_phi_functions[5]), + (list_of_phi_functions[7], list_of_phi_functions[6]), + (list_of_phi_functions[3], list_of_phi_functions[7]), + } and set(graph.nodes) == set(list_of_phi_functions) def test_circular_dependency_dfvs_2(circular_dependency_phi_functions, variable_v, variable_u): @@ -239,36 +215,28 @@ def test_circular_dependency_update_2(circular_dependency_phi_functions, variabl graph.update_dependency_graph(list_of_phi_functions[0], new_phi_function_1) - assert ( - set(graph.edges) - == { - (new_phi_function_1, list_of_phi_functions[1]), - (list_of_phi_functions[4], list_of_phi_functions[3]), - (list_of_phi_functions[5], list_of_phi_functions[3]), - (list_of_phi_functions[2], list_of_phi_functions[4]), - (list_of_phi_functions[5], list_of_phi_functions[4]), - (list_of_phi_functions[6], list_of_phi_functions[5]), - (list_of_phi_functions[7], list_of_phi_functions[6]), - (list_of_phi_functions[3], list_of_phi_functions[7]), - } - and set(graph.nodes) == set(list_of_phi_functions[1:] + [new_phi_function_1]) - ) + assert set(graph.edges) == { + (new_phi_function_1, list_of_phi_functions[1]), + (list_of_phi_functions[4], list_of_phi_functions[3]), + (list_of_phi_functions[5], list_of_phi_functions[3]), + (list_of_phi_functions[2], list_of_phi_functions[4]), + (list_of_phi_functions[5], list_of_phi_functions[4]), + (list_of_phi_functions[6], list_of_phi_functions[5]), + (list_of_phi_functions[7], list_of_phi_functions[6]), + (list_of_phi_functions[3], list_of_phi_functions[7]), + } and set(graph.nodes) == set(list_of_phi_functions[1:] + [new_phi_function_1]) graph.update_dependency_graph(list_of_phi_functions[5], new_phi_function_2) - assert ( - set(graph.edges) - == { - (new_phi_function_1, list_of_phi_functions[1]), - (list_of_phi_functions[4], list_of_phi_functions[3]), - (new_phi_function_2, list_of_phi_functions[3]), - (list_of_phi_functions[2], list_of_phi_functions[4]), - (new_phi_function_2, list_of_phi_functions[4]), - (list_of_phi_functions[7], list_of_phi_functions[6]), - (list_of_phi_functions[3], list_of_phi_functions[7]), - } - and set(graph.nodes) == set(list_of_phi_functions[1:5] + list_of_phi_functions[6:] + [new_phi_function_1, new_phi_function_2]) - ) + assert set(graph.edges) == { + (new_phi_function_1, list_of_phi_functions[1]), + (list_of_phi_functions[4], list_of_phi_functions[3]), + (new_phi_function_2, list_of_phi_functions[3]), + (list_of_phi_functions[2], list_of_phi_functions[4]), + (new_phi_function_2, list_of_phi_functions[4]), + (list_of_phi_functions[7], list_of_phi_functions[6]), + (list_of_phi_functions[3], list_of_phi_functions[7]), + } and set(graph.nodes) == set(list_of_phi_functions[1:5] + list_of_phi_functions[6:] + [new_phi_function_1, new_phi_function_2]) def test_no_input_dependency_graph(): diff --git a/tests/pipeline/dataflowanalysis/test-delogic_dead_loop_elimination.py b/tests/pipeline/dataflowanalysis/test-delogic_dead_loop_elimination.py new file mode 100644 index 000000000..b5d2397cb --- /dev/null +++ b/tests/pipeline/dataflowanalysis/test-delogic_dead_loop_elimination.py @@ -0,0 +1,476 @@ +from decompiler.pipeline.dataflowanalysis import DeadLoopElimination, ExpressionPropagation +from decompiler.structures.graphs.cfg import BasicBlock, ControlFlowGraph, FalseCase, TrueCase, UnconditionalEdge +from decompiler.structures.pseudo.expressions import Constant, Variable +from decompiler.structures.pseudo.instructions import Assignment, Branch, Phi, Return +from decompiler.structures.pseudo.operations import Condition, OperationType +from decompiler.structures.pseudo.typing import Integer +from decompiler.task import DecompilerTask +from decompiler.util.options import Options + +a = Variable("a", Integer.int32_t(), 0) +b = Variable("b", Integer.int32_t(), 1) +c = Variable("c", Integer.int32_t(), 2) +x = Variable("x", Integer.int32_t(), 3) +x1 = Variable("x", Integer.int32_t(), 1) +x2 = Variable("x", Integer.int32_t(), 2) +x3 = Variable("x", Integer.int32_t(), 3) + + +def _run_dead_loop_elimination(cfg: ControlFlowGraph): + options = Options() + options.set("dead-loop-elimination.timeout_satisfiable", 1000) + options.set("logic-engine.engine", "delogic") + DeadLoopElimination().run(DecompilerTask("test", cfg, options=options)) + + +def _run_expression_propagation(cfg: ControlFlowGraph): + options = Options() + options.set("expression-propagation.maximum_instruction_complexity", 10) + options.set("expression-propagation.maximum_branch_complexity", 10) + options.set("expression-propagation.maximum_call_complexity", 10) + options.set("expression-propagation.maximum_assignment_complexity", 10) + ExpressionPropagation().run(DecompilerTask("test", cfg, options=options)) + + +def test_no_propagation_no_change(): + """ + Simple case where no branch will be removed: + No Constant in Phi. + + +----+ +---------------+ + | 2. | | 0. | + | |<----+ a = 0x0 |<---+ + +-+--+ f | x = phi(a, b) | | + | | if(x == 0x0) | | + | +---------------+ | + | |t | + | | | + | V | + | +--------------+ | + | | 1. | | + | | b = 0x1 | f | + | | if(b == 0x0) |-----+ + | +--------------+ + | |t + | | + | V + | +------------+ + | | 3. | + +------> | return 0x1 | + +------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + n0 := BasicBlock( + 0, instructions=[phi := Phi(x, [a, b]), branch := Branch(Condition(OperationType.equal, [phi.destination, Constant(0x0)]))] + ), + n1 := BasicBlock( + 1, instructions=[Assignment(b, Constant(0x1)), back_edge := Branch(Condition(OperationType.equal, [b, Constant(0x0)]))] + ), + n2 := BasicBlock(2, instructions=[]), + n3 := BasicBlock(3, instructions=[Return([Constant(1)])]), + ] + ) + cfg.add_edges_from( + [ + TrueCase(n0, n1), + FalseCase(n0, n2), + UnconditionalEdge(n2, n3), + TrueCase(n1, n3), + FalseCase(n1, n0), + ] + ) + origin_blocks = {n0: a, n1: b} + phi.update_phi_function(origin_blocks) + _run_dead_loop_elimination(cfg) + assert set(cfg) == {n0, n1, n2, n3} + assert n0.instructions == [phi, branch] + assert isinstance(cfg.get_edge(n0, n1), TrueCase) + assert isinstance(cfg.get_edge(n0, n2), FalseCase) + assert isinstance(cfg.get_edge(n2, n3), UnconditionalEdge) + assert isinstance(cfg.get_edge(n1, n3), TrueCase) + assert isinstance(cfg.get_edge(n1, n0), FalseCase) + + +def test_backedge_no_change(): + """ + Simple case where no branch will be removed: + Backedge prevents pruning. + + +----+ +------------------+ + | 2. | | 0. | + | |<----+ a = 0x0 |<--+ + +-+--+ f | x = phi(0x0, b) | | + | | if(x == 0x0) | | + | +------------------+ | + | |t | + | | | + | V | + | +--------------+ | + | | 1. | | + | | b = 0x1 | f | + | | if(b == 0x0) |-------+ + | +--------------+ + | |t + | | + | V + | +------------+ + | | 3. | + +------> | return 0x1 | + +------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + n0 := BasicBlock( + 0, + instructions=[ + phi := Phi(x, [const := Constant(0x0), b]), + branch := Branch(Condition(OperationType.equal, [phi.destination, Constant(0x0)])), + ], + ), + n1 := BasicBlock( + 1, instructions=[Assignment(b, Constant(0x1)), back_edge := Branch(Condition(OperationType.equal, [b, Constant(0x0)]))] + ), + n2 := BasicBlock(2, instructions=[]), + n3 := BasicBlock(3, instructions=[Return([Constant(1)])]), + ] + ) + origin_blocks = {n0: const, n1: b} + phi.update_phi_function(origin_blocks) + cfg.add_edges_from( + [ + TrueCase(n0, n1), + FalseCase(n0, n2), + UnconditionalEdge(n2, n3), + TrueCase(n1, n3), + FalseCase(n1, n0), + ] + ) + _run_dead_loop_elimination(cfg) + assert set(cfg) == {n0, n1, n2, n3} + assert n0.instructions == [phi, branch] + assert isinstance(cfg.get_edge(n0, n1), TrueCase) + assert isinstance(cfg.get_edge(n0, n2), FalseCase) + assert isinstance(cfg.get_edge(n2, n3), UnconditionalEdge) + assert isinstance(cfg.get_edge(n1, n3), TrueCase) + assert isinstance(cfg.get_edge(n1, n0), FalseCase) + + +def test_not_dominated_no_change(): + """ + Simple case where no branch will be removed: + Variables in phi-function not dominated by current block. + + +-----------------+ + | 4. | + | b = 0x1 | + +-+---------------+ + | + | + v + +----+ +--+---------------+ + | 2. | | 0. | + | +<----+ a = 0x0 +<--+ + +-+--+ f | x = phi(0x0, b) | | + | | if(x != 0x0) | | + | +------------------+ | + | |t | + | + | + | V | + | +--------------+ | + | | 1. | | + | | if(b == 0x0) | f | + | | +-------+ + | +--------------+ + | |t + | + + | V + | +------------+ + | | 3. | + +------> | return 0x1 | + +------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + n0 := BasicBlock( + 0, + instructions=[ + phi := Phi(x, [const := Constant(0x0), b]), + branch := Branch(Condition(OperationType.not_equal, [phi.destination, Constant(0x0)])), + ], + ), + n1 := BasicBlock(1, instructions=[back_edge := Branch(Condition(OperationType.equal, [b, Constant(0x0)]))]), + n2 := BasicBlock(2, instructions=[]), + n3 := BasicBlock(3, instructions=[Return([Constant(1)])]), + n4 := BasicBlock(4, instructions=[Assignment(b, Constant(0x1))]), + ] + ) + variable_of_block = {n0: const, n4: b} + phi.update_phi_function(variable_of_block) + cfg.add_edges_from( + [ + UnconditionalEdge(n4, n0), + TrueCase(n0, n1), + FalseCase(n0, n2), + UnconditionalEdge(n2, n3), + TrueCase(n1, n3), + FalseCase(n1, n0), + ] + ) + _run_dead_loop_elimination(cfg) + assert set(cfg) == {n0, n1, n2, n3, n4} + assert n0.instructions == [phi, branch] + assert isinstance(cfg.get_edge(n4, n0), UnconditionalEdge) + assert isinstance(cfg.get_edge(n0, n1), TrueCase) + assert isinstance(cfg.get_edge(n0, n2), FalseCase) + assert isinstance(cfg.get_edge(n2, n3), UnconditionalEdge) + assert isinstance(cfg.get_edge(n1, n3), TrueCase) + assert isinstance(cfg.get_edge(n1, n0), FalseCase) + + +def test_false_branch_without_back_edge(): + """ + Simple case where block 1 will be removed: + +----+ +------------------+ + | | | 0. | + | 2. | | x#3 = ϕ(0x0,b#1) | + | | <-- | if(x#3 != 0x0) | <+ + +----+ +------------------+ | + | | | + | | | + | v | + | +------------------+ | + | | 1. | | + | | b#1 = 0x1 | | + | | if(b#1 == 0x0) | -+ + | +------------------+ + | | + | | + | v + | +------------------+ + | | 3. | + +------> | return 0x1 | + +------------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + n0 := BasicBlock( + 0, + instructions=[ + phi := Phi(x, [const := Constant(0x0), b]), + branch := Branch(Condition(OperationType.not_equal, [phi.destination, Constant(0x0)])), + ], + ), + n1 := BasicBlock( + 1, instructions=[Assignment(b, Constant(0x1)), back_edge := Branch(Condition(OperationType.equal, [b, Constant(0x0)]))] + ), + n2 := BasicBlock(2, instructions=[]), + n3 := BasicBlock(3, instructions=[Return([Constant(1)])]), + ] + ) + variable_of_block = {n0: const, n1: b} + phi.update_phi_function(variable_of_block) + cfg.add_edges_from( + [ + TrueCase(n0, n1), + FalseCase(n0, n2), + UnconditionalEdge(n2, n3), + TrueCase(n1, n3), + FalseCase(n1, n0), + ] + ) + _run_dead_loop_elimination(cfg) + assert set(cfg) == {n0, n2, n3} + assert n0.instructions == [phi] + assert isinstance(cfg.get_edge(n0, n2), UnconditionalEdge) + assert isinstance(cfg.get_edge(n2, n3), UnconditionalEdge) + + +def test_variable_in_phi(): + """ + if (a == 0 || b !=0) where b = Phi(a, c) + case where block 1 will be removed: + + +----+ +----------------------------------+ + | | | 0. | + | 2. | | b#1 = ϕ(a#0,c#2) | + | | <-- | if((a#0 == 0x0) || (b#1 != 0x0)) | <+ + +----+ +----------------------------------+ | + | | | + | | | + | v | + | +----------------------------------+ | + | | 1. | | + | | c#2 = 0x1 | | + | | if(b#1 == 0x0) | -+ + | +----------------------------------+ + | | + | | + | v + | +----------------------------------+ + | | 3. | + +------> | return 0x1 | + +----------------------------------+ + + """ + phi = Phi(b, [a, c]) + cond1 = Condition(OperationType.equal, [a, Constant(0x0)]) + cond2 = Condition(OperationType.not_equal, [phi.destination, Constant(0x0)]) + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + n0 := BasicBlock( + 0, + instructions=[ + phi, + branch := Branch(Condition(OperationType.bitwise_or, [cond1, cond2])), + ], + ), + n1 := BasicBlock( + 1, instructions=[Assignment(c, Constant(0x1)), back_edge := Branch(Condition(OperationType.equal, [b, Constant(0x0)]))] + ), + n2 := BasicBlock(2, instructions=[]), + n3 := BasicBlock(3, instructions=[Return([Constant(1)])]), + ] + ) + variable_of_block = {n0: a, n1: c} + phi.update_phi_function(variable_of_block) + cfg.add_edges_from( + [ + FalseCase(n0, n1), + TrueCase(n0, n2), + UnconditionalEdge(n2, n3), + TrueCase(n1, n3), + FalseCase(n1, n0), + ] + ) + _run_dead_loop_elimination(cfg) + assert set(cfg.nodes) == {n0, n2, n3} + assert n0.instructions == [phi] + assert isinstance(cfg.get_edge(n0, n2), UnconditionalEdge) + assert isinstance(cfg.get_edge(n2, n3), UnconditionalEdge) + + +def test_multiple_upstream_const_in_phi(): + """ + No block will be removed. + After expression propagation: + +-----------+ +---------------+ + | 2. | | 0. | + | x#2 = 0x2 | <-- | if(a#0 < 0x0) | + +-----------+ +---------------+ + | | + | | + | v + | +---------------+ + | | 1. | + | | x#1 = 0x1 | + | +---------------+ + | | + | | + | v + | +----------------------+ +------------+ + | | 3. | | 5. | + | | b#1 = ϕ(0x1,0x2,0x5) | | return 0x0 | + +-------------> | if(b#1 == 0x5) | --> | | + +----------------------+ +------------+ + | ^ + | | + v | + +---------------+ | + | 4. | | + | x#3 = 0x5 | -+ + +---------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + n0 := BasicBlock( + 0, + instructions=[Branch(Condition(OperationType.less, [a, Constant(0x0)]))], + ), + n1 := BasicBlock(1, instructions=[Assignment(x1, Constant(0x1))]), + n2 := BasicBlock(2, instructions=[Assignment(x2, Constant(0x2))]), + n3 := BasicBlock(3, instructions=[phi := Phi(b, [x1, x2, x3]), Branch(Condition(OperationType.equal, [b, Constant(0x5)]))]), + n4 := BasicBlock(4, instructions=[Assignment(x3, Constant(0x5))]), + n5 := BasicBlock(5, instructions=[Return([Constant(0)])]), + ] + ) + variable_of_block = {n1: x1, n2: x2, n4: x3} + phi.update_phi_function(variable_of_block) + cfg.add_edges_from( + [ + TrueCase(n0, n1), + FalseCase(n0, n2), + UnconditionalEdge(n1, n3), + UnconditionalEdge(n2, n3), + UnconditionalEdge(n4, n3), + FalseCase(n3, n4), + TrueCase(n3, n5), + ] + ) + _run_expression_propagation(cfg) + _run_dead_loop_elimination(cfg) + assert set(cfg.nodes) == {n0, n1, n2, n3, n4, n5} + assert isinstance(cfg.get_edge(n0, n1), TrueCase) + assert isinstance(cfg.get_edge(n0, n2), FalseCase) + assert isinstance(cfg.get_edge(n1, n3), UnconditionalEdge) + assert isinstance(cfg.get_edge(n2, n3), UnconditionalEdge) + assert isinstance(cfg.get_edge(n4, n3), UnconditionalEdge) + assert isinstance(cfg.get_edge(n3, n4), FalseCase) + assert isinstance(cfg.get_edge(n3, n5), TrueCase) + + +def test_two_const_one_upstream_in_phi(): + """ + Block 2 will be removed. + After expression propagation: + +------------------+ + | 0. | + | x#1 = 0x1 | + +------------------+ + | + | + v + +------------+ +------------------+ + | 3. | | 1. | + | return 0x0 | | b#1 = ϕ(0x1,0x5) | + | | <-- | if(b#1 == 0x1) | <+ + +------------+ +------------------+ | + | | + | | + v | + +------------------+ | + | 2. | | + | x#3 = 0x5 | -+ + +------------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + n0 := BasicBlock(0, instructions=[Assignment(x1, Constant(0x1))]), + n1 := BasicBlock(1, instructions=[phi := Phi(b, [x1, x3]), Branch(Condition(OperationType.equal, [b, Constant(0x1)]))]), + n2 := BasicBlock(2, instructions=[Assignment(x3, Constant(0x5))]), + n3 := BasicBlock(3, instructions=[Return([Constant(0)])]), + ] + ) + variable_of_block = {n0: x1, n2: x3} + phi.update_phi_function(variable_of_block) + cfg.add_edges_from( + [ + UnconditionalEdge(n0, n1), + FalseCase(n1, n2), + TrueCase(n1, n3), + UnconditionalEdge(n2, n1), + ] + ) + _run_expression_propagation(cfg) + _run_dead_loop_elimination(cfg) + assert set(cfg.nodes) == {n0, n1, n3} + assert len(n1.instructions) == 1 + assert isinstance(cfg.get_edge(n0, n1), UnconditionalEdge) + assert isinstance(cfg.get_edge(n1, n3), UnconditionalEdge) diff --git a/tests/pipeline/dataflowanalysis/test-delogic_dead_path_elimination.py b/tests/pipeline/dataflowanalysis/test-delogic_dead_path_elimination.py new file mode 100644 index 000000000..51868d35f --- /dev/null +++ b/tests/pipeline/dataflowanalysis/test-delogic_dead_path_elimination.py @@ -0,0 +1,513 @@ +from decompiler.pipeline.dataflowanalysis import DeadPathElimination +from decompiler.structures.graphs.cfg import BasicBlock, BasicBlockEdgeCondition, ControlFlowGraph, FalseCase, TrueCase, UnconditionalEdge +from decompiler.structures.pseudo.expressions import Constant, Variable +from decompiler.structures.pseudo.instructions import Assignment, Branch, Phi, Return +from decompiler.structures.pseudo.operations import Condition, ListOperation, OperationType +from decompiler.task import DecompilerTask +from decompiler.util.options import Options + + +def run_dead_path_elimination(cfg): + options = Options() + options.set("dead-path-elimination.timeout_satisfiable", 1000) + options.set("logic-engine.engine", "delogic") + DeadPathElimination().run(DecompilerTask("test", cfg, options=options)) + + +def test_trivial_no_change(): + """ + Simple case where no branch can be removed. + + +----+ +----------------+ + | 2. | | 0. | + | | <-- | if(x < y) | + +----+ +----------------+ + | | + | | + | v + | +----------------+ + | | 1. | + | +----------------+ + | | + | | + | v + | +----------------+ + | | 3. | + +------> | return 0x1 | + +----------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + n0 := BasicBlock(0, instructions=[branch := Branch(Condition(OperationType.less, [Variable("x"), Variable("y")]))]), + n1 := BasicBlock(1, instructions=[]), + n2 := BasicBlock(2, instructions=[]), + n3 := BasicBlock(3, instructions=[Return([Constant(1)])]), + ] + ) + cfg.add_edges_from( + [ + TrueCase(n0, n1), + FalseCase(n0, n2), + UnconditionalEdge(n1, n3), + UnconditionalEdge(n2, n3), + ] + ) + run_dead_path_elimination(cfg) + assert set(cfg) == {n0, n1, n2, n3} + assert n0.instructions == [branch] + assert isinstance(cfg.get_edge(n0, n1), TrueCase) + assert isinstance(cfg.get_edge(n0, n2), FalseCase) + assert isinstance(cfg.get_edge(n1, n3), UnconditionalEdge) + assert isinstance(cfg.get_edge(n2, n3), UnconditionalEdge) + + +def test_trivial_true(): + """ + Simple case where the true branch is dead. + + +----+ +----------------+ + | 2. | | 0. | + | | <-- | if(0x0 == 0x1) | + +----+ +----------------+ + | | + | | + | v + | +----------------+ + | | 1. | + | +----------------+ + | | + | | + | v + | +----------------+ + | | 3. | + +------> | return 0x1 | + +----------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + n0 := BasicBlock(0, instructions=[Branch(Condition(OperationType.equal, [Constant(0), Constant(1)]))]), + n1 := BasicBlock(1, instructions=[]), + n2 := BasicBlock(2, instructions=[]), + n3 := BasicBlock(3, instructions=[Return([Constant(1)])]), + ] + ) + cfg.add_edges_from( + [ + TrueCase(n0, n1), + FalseCase(n0, n2), + UnconditionalEdge(n1, n3), + UnconditionalEdge(n2, n3), + ] + ) + run_dead_path_elimination(cfg) + assert set(cfg.nodes) == {n0, n2, n3} + assert n0.instructions == [] + assert isinstance(cfg.get_edge(n0, n2), UnconditionalEdge) + assert isinstance(cfg.get_edge(n2, n3), UnconditionalEdge) + + +def test_trivial_false(): + """ + Simple case where the false branch is dead. + + +----+ +----------------+ + | 2. | | 0. | + | | <-- | if(0x0 == 0x0) | + +----+ +----------------+ + | | + | | + | v + | +----------------+ + | | 1. | + | +----------------+ + | | + | | + | v + | +----------------+ + | | 3. | + +------> | return 0x1 | + +----------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + n0 := BasicBlock(0, instructions=[Branch(Condition(OperationType.equal, [Constant(0), Constant(0)]))]), + n1 := BasicBlock(1, instructions=[]), + n2 := BasicBlock(2, instructions=[]), + n3 := BasicBlock(3, instructions=[Return([Constant(1)])]), + ] + ) + cfg.add_edges_from( + [ + TrueCase(n0, n1), + FalseCase(n0, n2), + UnconditionalEdge(n1, n3), + UnconditionalEdge(n2, n3), + ] + ) + run_dead_path_elimination(cfg) + assert set(cfg.nodes) == {n0, n1, n3} + assert n0.instructions == [] + assert [cfg.get_edge(n0, n1).condition_type, cfg.get_edge(n1, n3).condition_type] == [ + BasicBlockEdgeCondition.unconditional, + BasicBlockEdgeCondition.unconditional, + ] + + +def test_trivial_mixed(): + """ + Trivial test with mixed dead true and false branches. + + +----+ +----------------+ +----------------+ + | 5. | | 2. | | 0. | + | | <-- | if(0x0 == 0x0) | <-- | if(x == 0x0) | + +----+ +----------------+ +----------------+ + | | | + | | | + | v v + | +----------------+ +----------------+ + | | 4. | | 1. | + | | | | if(0x0 == 0x1) | -+ + | +----------------+ +----------------+ | + | | | | + | | | | + | | v | + | | +----------------+ | + | | | 3. | | + | | +----------------+ | + | | | | + | | | | + | | v v + | | +---------------------+ + | | | 6. | + | +------------------> | return 0x1 | + | +---------------------+ + | ^ + +---------------------------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + start := BasicBlock(0, instructions=[Branch(Condition(OperationType.equal, [Variable("x"), Constant(0)]))]), + n1 := BasicBlock(1, instructions=[Branch(Condition(OperationType.equal, [Constant(0), Constant(1)]))]), + n2 := BasicBlock(2, instructions=[Branch(Condition(OperationType.equal, [Constant(0), Constant(0)]))]), + n3 := BasicBlock(3, instructions=[]), + n4 := BasicBlock(4, instructions=[]), + n5 := BasicBlock(5, instructions=[]), + end := BasicBlock(6, instructions=[Return([Constant(1)])]), + ] + ) + cfg.add_edges_from( + [ + TrueCase(start, n1), + FalseCase(start, n2), + TrueCase(n1, n3), + FalseCase(n1, end), + UnconditionalEdge(n3, end), + TrueCase(n2, n4), + FalseCase(n2, n5), + UnconditionalEdge(n4, end), + UnconditionalEdge(n5, end), + ] + ) + run_dead_path_elimination(cfg) + assert set(cfg.nodes) == {start, n1, n2, n4, end} + assert len(cfg.edges) == 5 + assert n1.instructions == n2.instructions == [] + assert [ + cfg.get_edge(start, n1).condition_type, + cfg.get_edge(start, n2).condition_type, + cfg.get_edge(n1, end).condition_type, + cfg.get_edge(n2, n4).condition_type, + cfg.get_edge(n4, end).condition_type, + ] == [ + BasicBlockEdgeCondition.true, + BasicBlockEdgeCondition.false, + BasicBlockEdgeCondition.unconditional, + BasicBlockEdgeCondition.unconditional, + BasicBlockEdgeCondition.unconditional, + ] + + +def test_dead_loop(): + """ + Check if a while-loop with an unsatisfyable condition is removed completely. + + +----------------+ + | 0. | + +----------------+ + | + | + v + +------------+ +----------------+ + | 3. | | 1. | + | return 0x1 | <-- | if(0x2a < 0x0) | <+ + +------------+ +----------------+ | + | | + | | + v | + +----------------+ | + | 2. | -+ + +----------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + start := BasicBlock(0, instructions=[]), + loop_condition := BasicBlock(1, instructions=[Branch(Condition(OperationType.less, [Constant(42), Constant(0)]))]), + loop_body := BasicBlock(2, instructions=[]), + end := BasicBlock(3, instructions=[Return([Constant(1)])]), + ] + ) + cfg.add_edges_from( + [ + UnconditionalEdge(start, loop_condition), + TrueCase(loop_condition, loop_body), + FalseCase(loop_condition, end), + UnconditionalEdge(loop_body, loop_condition), + ] + ) + run_dead_path_elimination(cfg) + assert set(cfg.nodes) == {start, loop_condition, end} + assert loop_condition.instructions == [] + assert len(cfg.edges) == 2 + assert [cfg.get_edge(start, loop_condition).condition_type, cfg.get_edge(loop_condition, end).condition_type] == [ + BasicBlockEdgeCondition.unconditional, + BasicBlockEdgeCondition.unconditional, + ] + + +def test_nested_loop(): + """ + Simple test with one dead branch with a nested loop inside. + + +----+ +----------------+ + | 1. | | 0. | + | | <-- | if(0x0 == 0x0) | + +----+ +----------------+ + | | + | | + | v + | +----------------+ + | | 2. | + | +----------------+ + | | + | | + | v + | +----------------+ +----+ + | | 3. | | 4. | + +----+------> | if(x == 0x0) | --> | | + | | +----------------+ +----+ + | | | | + | | | | + | | v | + | | +----------------+ | + | | | 5. | | + | +------> | return 0x1 | | + | +----------------+ | + | | + +--------------------------------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + start := BasicBlock(0, instructions=[Branch(Condition(OperationType.equal, [Constant(0), Constant(0)]))]), + true := BasicBlock(1, instructions=[]), + false := BasicBlock(2, instructions=[]), + loop_branch := BasicBlock(3, instructions=[Branch(Condition(OperationType.equal, [Variable("x"), Constant(0)]))]), + loop_body := BasicBlock(4, instructions=[]), + end := BasicBlock(5, instructions=[Return([Constant(1)])]), + ] + ) + cfg.add_edges_from( + [ + TrueCase(start, true), + FalseCase(start, false), + UnconditionalEdge(true, end), + UnconditionalEdge(false, loop_branch), + TrueCase(loop_branch, loop_body), + FalseCase(loop_branch, end), + UnconditionalEdge(loop_body, loop_branch), + ] + ) + run_dead_path_elimination(cfg) + assert set(cfg.nodes) == {start, true, end} + assert start.instructions == [] + assert [cfg.get_edge(start, true).condition_type, cfg.get_edge(true, end).condition_type] == [ + BasicBlockEdgeCondition.unconditional, + BasicBlockEdgeCondition.unconditional, + ] + + +def test_branch_block_remains(): + """ + Test that the block with the branch is not removed. + + +----+ +----------------+ + | 1. | | 0. | + | | <-- | if(0x0 == 0x0) | + +----+ +----------------+ + | | + | | + | v + | +----------------+ + | | 2. | + | +----------------+ + | | + | | + | v + | +----------------+ +----+ + | | 3. | | 4. | + +----+------> | if(x == 0x0) | --> | | + | | +----------------+ +----+ + | | | | + | | | | + | | v | + | | +----------------+ | + | | | 5. | | + | +------> | return 0x1 | | + | +----------------+ | + | | + +--------------------------------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + start := BasicBlock(0, instructions=[]), + dead_branch_block := BasicBlock(1, instructions=[Branch(Condition(OperationType.not_equal, [Variable("x"), Variable("x")]))]), + dead_loop_block := BasicBlock(2, instructions=[]), + loop_branch_block := BasicBlock(3, instructions=[Branch(Condition(OperationType.less, [Variable("x"), Constant(2)]))]), + end := BasicBlock(4, instructions=[Return([Variable("x")])]), + ] + ) + cfg.add_edges_from( + [ + UnconditionalEdge(start, dead_branch_block), + TrueCase(dead_branch_block, dead_loop_block), + UnconditionalEdge(dead_loop_block, dead_branch_block), + TrueCase(dead_branch_block, loop_branch_block), + FalseCase(loop_branch_block, dead_branch_block), + TrueCase(loop_branch_block, end), + ] + ) + run_dead_path_elimination(cfg) + assert set(cfg.nodes) == {start, dead_branch_block, loop_branch_block, end} + assert dead_branch_block.instructions == [] + + +def test_two_edges_one_node(): + """ + Test whether a block pointed to by two different dead edges is removed correctly. + + +------------+ +-------------+ + | 2. | | 0. | + +- | if(a != a) | <-- | if(a < 0xa) | + | +------------+ +-------------+ + | | | + | | | + | | v + | | +-------------+ +----+ + | | | 1. | | 4. | + | | | if(a != a) | --> | | + | | +-------------+ +----+ + | | | | + | | | | + | | v | + | | +-------------+ | + | +--------------> | 3. | | + | +-------------+ | + | | | + | | | + | v | + | +-------------+ | + | | 5. | | + +-------------------> | return a | <-----+ + +-------------+ + """ + cfg = ControlFlowGraph() + cfg.add_nodes_from( + [ + start := BasicBlock(0, instructions=[Branch(Condition(OperationType.less, [Variable("a"), Constant(10)]))]), + dead_branch_block1 := BasicBlock(1, instructions=[Branch(Condition(OperationType.not_equal, [Variable("a"), Variable("a")]))]), + dead_branch_block2 := BasicBlock(2, instructions=[Branch(Condition(OperationType.not_equal, [Variable("a"), Variable("a")]))]), + shared_block := BasicBlock(3), + exclusive_block := BasicBlock(4), + end := BasicBlock(5, instructions=[Return(ListOperation([Variable("a")]))]), + ] + ) + cfg.add_edges_from( + [ + TrueCase(start, dead_branch_block1), + FalseCase(start, dead_branch_block2), + TrueCase(dead_branch_block1, shared_block), + TrueCase(dead_branch_block2, shared_block), + UnconditionalEdge(shared_block, end), + FalseCase(dead_branch_block1, exclusive_block), + FalseCase(dead_branch_block2, end), + UnconditionalEdge(exclusive_block, end), + ] + ) + run_dead_path_elimination(cfg) + assert list(cfg.nodes) == [start, dead_branch_block1, dead_branch_block2, exclusive_block, end] + + +def test_phi_function_gets_updated(): + """ + Simple case where the true branch is dead and Phi dependency of true branch gets removed. + +----+ +----------------+ + | | | 0. | + | 2. | | a | + | | <-- | if(0x0 == 0x1) | + +----+ +----------------+ + | | + | | + | v + | +----------------+ + | | 1. | + | | b | + | +----------------+ + | | + | | + | v + | +----------------+ + | | 3. | + | | x = ϕ(a,b) | + +------> | return 0x1 | + +----------------+ + """ + cfg = ControlFlowGraph() + a = Variable("a") + b = Variable("b") + cfg.add_nodes_from( + [ + n0 := BasicBlock( + 0, + instructions=[ + assign_a := Assignment(a, Constant(0x42)), + Branch(Condition(OperationType.equal, [Constant(0), Constant(1)])), + ], + ), + n1 := BasicBlock(1, instructions=[Assignment(b, Constant(0x1))]), + n2 := BasicBlock(2, instructions=[]), + n3 := BasicBlock(3, instructions=[phi := Phi(Variable("x"), [a, b]), Return([Constant(1)])]), + ] + ) + cfg.add_edges_from( + [ + TrueCase(n0, n1), + FalseCase(n0, n2), + UnconditionalEdge(n1, n3), + UnconditionalEdge(n2, n3), + ] + ) + origin_block = {n0: a, n1: b} + phi.update_phi_function(origin_block) + assert phi.origin_block == origin_block + run_dead_path_elimination(cfg) + assert phi.origin_block == {n0: a} + assert set(cfg.nodes) == {n0, n2, n3} + assert n0.instructions == [assign_a] + assert isinstance(cfg.get_edge(n0, n2), UnconditionalEdge) + assert isinstance(cfg.get_edge(n2, n3), UnconditionalEdge) diff --git a/tests/pipeline/dataflowanalysis/test-dead_loop_elimination.py b/tests/pipeline/dataflowanalysis/test-z3_dead_loop_elimination.py similarity index 99% rename from tests/pipeline/dataflowanalysis/test-dead_loop_elimination.py rename to tests/pipeline/dataflowanalysis/test-z3_dead_loop_elimination.py index f93e31ac7..da60673fb 100644 --- a/tests/pipeline/dataflowanalysis/test-dead_loop_elimination.py +++ b/tests/pipeline/dataflowanalysis/test-z3_dead_loop_elimination.py @@ -19,6 +19,7 @@ def _run_dead_loop_elimination(cfg: ControlFlowGraph): options = Options() options.set("dead-loop-elimination.timeout_satisfiable", 1000) + options.set("logic-engine.engine", "z3") DeadLoopElimination().run(DecompilerTask("test", cfg, options=options)) diff --git a/tests/pipeline/dataflowanalysis/test-dead_path_elimination.py b/tests/pipeline/dataflowanalysis/test-z3_dead_path_elimination.py similarity index 99% rename from tests/pipeline/dataflowanalysis/test-dead_path_elimination.py rename to tests/pipeline/dataflowanalysis/test-z3_dead_path_elimination.py index c94331828..968031c23 100644 --- a/tests/pipeline/dataflowanalysis/test-dead_path_elimination.py +++ b/tests/pipeline/dataflowanalysis/test-z3_dead_path_elimination.py @@ -10,6 +10,7 @@ def run_dead_path_elimination(cfg): options = Options() options.set("dead-path-elimination.timeout_satisfiable", 1000) + options.set("logic-engine.engine", "z3") DeadPathElimination().run(DecompilerTask("test", cfg, options=options)) diff --git a/tests/structures/pseudo/test_delogic_converter.py b/tests/structures/pseudo/test_delogic_converter.py new file mode 100644 index 000000000..8ce0301fe --- /dev/null +++ b/tests/structures/pseudo/test_delogic_converter.py @@ -0,0 +1,154 @@ +import pytest +from decompiler.structures.pseudo.delogic_logic import DelogicConverter +from decompiler.structures.pseudo.expressions import Constant, Variable +from decompiler.structures.pseudo.instructions import Branch, Return +from decompiler.structures.pseudo.logic import BaseConverter +from decompiler.structures.pseudo.operations import BinaryOperation, Condition, OperationType, UnaryOperation +from decompiler.structures.pseudo.typing import Float, Integer, Pointer + +var_a = Variable("a", Integer.int32_t()) +var_b = Variable("b", Integer.int32_t()) +var_x = Variable("x", Integer.int32_t()) +var_y = Variable("y", Integer.int32_t()) +const_1 = Constant(1, Integer.int32_t()) + + +@pytest.fixture +def converter(): + return DelogicConverter() + + +def test_unsupported(converter): + with pytest.raises(ValueError): + converter.convert(Return([Variable("x")])) + with pytest.raises(ValueError): + converter.convert(UnaryOperation(OperationType.dereference, [Variable("x")])) + with pytest.raises(ValueError): + converter.convert(UnaryOperation(OperationType.address, [Variable("x")])) + + +def test_constant(converter): + w = converter._world + assert converter.convert(Constant(6, Integer.int32_t())) == w.constant(6, 32) + assert converter.convert(Constant(7.2, Float.float())) == w.constant(7.2, 32) + with pytest.raises(ValueError): + converter.convert(Constant("hello", Pointer(Integer.uint8_t()))) + + +@pytest.mark.parametrize( + "to_parse, output", + [ + (Variable("x", Integer.int32_t(), ssa_label=0), "x@32"), + (Variable("x", Integer.int32_t(), ssa_label=1), "x@32"), + (Variable("x", Float.float(), ssa_label=1), "x@32"), + ], +) +def test_variable(converter, to_parse, output): + """When generating a variable, we can not transpose ssa labels or type information.""" + w = converter._world + assert converter.convert(to_parse) == w.from_string(output) + + +@pytest.mark.parametrize( + "to_parse, output", + [ + (UnaryOperation(OperationType.negate, [var_x.copy()]), "(~ x@32)"), + (UnaryOperation(OperationType.cast, [var_x.copy()]), "x@32"), + (UnaryOperation(OperationType.logical_not, [Variable("x", Integer(1))]), "(! x@1)"), + ], +) +def test_unary_operation(converter, to_parse, output): + w = converter._world + assert converter.convert(to_parse) == w.from_string(output) + + +@pytest.mark.parametrize( + "to_parse, output", + [ + ("(!= 0@32 0@32)", BaseConverter.UNSAT), + ("(== 0@32 0@32)", BaseConverter.SAT), + ], +) +def test_check(converter, to_parse, output): + """Test the check() function.""" + w = converter._world + condition = w.from_string(to_parse) + assert converter.check(condition) == output + + +def test_binary_operation(converter): + w = converter._world + a = w.variable("a", 32) + b = w.variable("b", 32) + assert converter.convert(BinaryOperation(OperationType.plus, [var_a.copy(), var_b.copy()])) == w.signed_add(a, b) + assert converter.convert(BinaryOperation(OperationType.minus, [var_a.copy(), var_b.copy()])) == w.signed_sub(a, b) + assert converter.convert(BinaryOperation(OperationType.multiply, [var_a.copy(), var_b.copy()])) == w.signed_mul(a, b) + assert converter.convert(BinaryOperation(OperationType.bitwise_xor, [var_a.copy(), var_b.copy()])) == w.bitwise_xor(a, b) + assert converter.convert(BinaryOperation(OperationType.bitwise_or, [var_a.copy(), var_b.copy()])) == w.bitwise_or(a, b) + assert converter.convert(BinaryOperation(OperationType.bitwise_and, [var_a.copy(), var_b.copy()])) == w.bitwise_and(a, b) + assert converter.convert(BinaryOperation(OperationType.divide, [var_a.copy(), var_b.copy()])) == w.signed_div(a, b) + assert converter.convert(BinaryOperation(OperationType.modulo, [var_a.copy(), var_b.copy()])) == w.signed_mod(a, b) + assert converter.convert(BinaryOperation(OperationType.left_shift, [var_a.copy(), var_b.copy()])) == w.shift_left(a, b) + assert converter.convert(BinaryOperation(OperationType.right_shift, [var_a.copy(), var_b.copy()])) == w.shift_right(a, b) + assert converter.convert(BinaryOperation(OperationType.left_rotate, [var_a.copy(), var_b.copy()])) == w.rotate_left(a, b) + assert converter.convert(BinaryOperation(OperationType.right_rotate, [var_a.copy(), var_b.copy()])) == w.rotate_right(a, b) + + +def test_branch(converter): + """Check that all possible branch types (BinaryOperation, Expression, Variable) are handled correctly.""" + w = converter._world + x = w.variable("x", 32) + one = w.constant(1, 32) + + branch1 = converter.convert(Branch(Condition(OperationType.equal, [var_x.copy(), const_1.copy()]))) + branch2 = converter.convert(Branch(Condition(OperationType.not_equal, [var_x.copy(), const_1.copy()]))) + branch3 = converter.convert(Branch(Condition(OperationType.less, [var_x.copy(), const_1.copy()]))) + branch4 = converter.convert(Branch(Condition(OperationType.less_or_equal, [var_x.copy(), const_1.copy()]))) + branch5 = converter.convert(Branch(Condition(OperationType.greater, [var_x.copy(), const_1.copy()]))) + branch6 = converter.convert(Branch(Condition(OperationType.greater_or_equal, [var_x.copy(), const_1.copy()]))) + + assert branch1 == w.bool_equal(x, one) + assert branch2 == w.bool_unequal(x, one) + assert branch3 == w.signed_lt(x, one) + assert branch4 == w.signed_le(x, one) + assert branch5 == w.signed_gt(x, one) + assert branch6 == w.signed_ge(x, one) + + +def test_multiple_ops(converter): + w = converter._world + x = w.variable("x", 32) + y = w.variable("y", 32) + one = w.constant(1, 32) + + condition1 = converter.convert( + Condition( + OperationType.bitwise_and, + [ + Condition(OperationType.equal, [var_x.copy(), const_1.copy()]), + Condition(OperationType.not_equal, [var_y.copy(), const_1.copy()]), + ], + ), + ) + condition2 = converter.convert( + Condition( + OperationType.bitwise_xor, + [ + Condition(OperationType.equal, [var_x.copy(), const_1.copy()]), + Condition(OperationType.not_equal, [var_y.copy(), const_1.copy()]), + ], + ), + ) + condition3 = converter.convert( + Condition( + OperationType.bitwise_or, + [ + Condition(OperationType.equal, [var_x.copy(), const_1.copy()]), + Condition(OperationType.not_equal, [var_y.copy(), const_1.copy()]), + ], + ), + ) + + assert condition1 == w.bitwise_and(w.bool_equal(x, one), w.bool_unequal(y, one)) + assert condition2 == w.bitwise_xor(w.bool_equal(one, x), w.bool_unequal(one, y)) + assert condition3 == w.bitwise_or(w.bool_equal(x, one), w.bool_unequal(one, y)) diff --git a/tests/structures/pseudo/test_logic.py b/tests/structures/pseudo/test_z3_converter.py similarity index 98% rename from tests/structures/pseudo/test_logic.py rename to tests/structures/pseudo/test_z3_converter.py index d886b711f..d30f3c11b 100644 --- a/tests/structures/pseudo/test_logic.py +++ b/tests/structures/pseudo/test_z3_converter.py @@ -1,9 +1,9 @@ import pytest from decompiler.structures.pseudo.expressions import Constant, Variable from decompiler.structures.pseudo.instructions import Branch, Return -from decompiler.structures.pseudo.logic import Z3Converter from decompiler.structures.pseudo.operations import BinaryOperation, Condition, OperationType, UnaryOperation from decompiler.structures.pseudo.typing import Float, Integer, Pointer +from decompiler.structures.pseudo.z3_logic import Z3Converter from z3 import And, BitVec, BitVecVal, Bool, BoolRef, Not, Or, Real, RotateLeft, RotateRight var_a = Variable("a", Integer.int32_t()) @@ -165,7 +165,7 @@ class TestSatisfiability: ([And(x[1], x[2]), Or(Not(x[1]), Not(x[2]))], False), ([a < const[20], a == const[20]], False), ([a < const[20], a == const[15]], True), - ([2 ** b == 3], False), + ([2**b == 3], False), ], ) def test_is_satisfiable(self, term: BoolRef, is_sat: bool): @@ -178,7 +178,7 @@ def test_is_satisfiable(self, term: BoolRef, is_sat: bool): ([And(x[1], x[2]), Or(Not(x[1]), Not(x[2]))], True), ([a < const[20], a == const[20]], True), ([a < const[20], a == const[15]], False), - ([2 ** b == 3], False), + ([2**b == 3], False), ], ) def test_is_not_satisfiable(self, term: BoolRef, is_unsat: bool):