[Pipeline] Add option to use dewolf-logic engine in dead path/loop el…

…imination (#72)

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()

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

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

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,22 +68,22 @@ 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
         for edge in graph.get_out_edges(block):
             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

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

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

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),
+    }