dewolf-logic fix (#11)

Co-authored-by: Niklas Bergmann <[email protected]> Co-authored-by: Eva-Maria Hols <[email protected]> Co-authored-by: Steffen Enders <[email protected]>
fkie-cad · Jul 29, 2022 · be51ee0 · be51ee0
1 parent 075c54e
commit be51ee0
Show file tree

Hide file tree

Showing 11 changed files with 1,630 additions and 54 deletions.
diff --git a/decompiler/pipeline/controlflowanalysis/restructuring_commons/ast_processor.py b/decompiler/pipeline/controlflowanalysis/restructuring_commons/ast_processor.py
@@ -154,7 +154,7 @@ def _simplify_reaching_conditions(self) -> None:
         This helps to remove unnecessary conditions for finding switches.
         """
         for node in self.asforest.post_order(self.asforest.current_root):
-            node.simplify_reaching_condition(self.asforest.condition_handler.get_z3_condition_map())
+            node.simplify_reaching_condition(self.asforest.condition_handler)
 
     def _combine_nodes_with_same_reaching_conditions(self) -> None:
         """

diff --git a/...structuring_commons/condition_aware_refinement_commons/initial_switch_node_constructer.py b/...structuring_commons/condition_aware_refinement_commons/initial_switch_node_constructer.py
@@ -268,7 +268,9 @@ def _update_reaching_condition_of(self, case_node: CaseNode, considered_conditio
             else:
                 exception_condition &= ~literal
         case_node.reaching_condition = (
-            LogicCondition.disjunction_of(literals_of_case_node) if literals_of_case_node else self.condition_handler.get_false_value()
+            LogicCondition.disjunction_of(list(literals_of_case_node))
+            if literals_of_case_node
+            else self.condition_handler.get_false_value()
         )
         if not exception_condition.is_true:
             case_node.child.reaching_condition = case_node.child.reaching_condition & exception_condition

diff --git a/decompiler/structures/ast/ast_nodes.py b/decompiler/structures/ast/ast_nodes.py
@@ -5,6 +5,7 @@
 from enum import Enum
 from typing import TYPE_CHECKING, Dict, Iterable, List, Literal, Optional, Tuple, TypeVar, Union
 
+from decompiler.structures.ast.condition_symbol import ConditionHandler
 from decompiler.structures.ast.reachability_graph import CaseDependencyGraph, SiblingReachability
 from decompiler.structures.graphs.interface import GraphNodeInterface
 from decompiler.structures.logic.logic_condition import LogicCondition, PseudoLogicCondition
@@ -163,10 +164,10 @@ def clean(self) -> None:
         """Makes clean ups, depending on the node. This helps to standardize the AST."""
         pass
 
-    def simplify_reaching_condition(self, z3_condition_of: Dict[LogicCondition, PseudoLogicCondition]):
+    def simplify_reaching_condition(self, condition_handler: ConditionHandler):
         """Simplify the reaching condition. If it is false we remove the subtree of this node."""
         if not self.reaching_condition.is_true:
-            self.reaching_condition.remove_redundancy(z3_condition_of)
+            self.reaching_condition.remove_redundancy(condition_handler)
         if self.reaching_condition.is_false:
             logging.warning(f"The CFG node {self} has reaching condition false, therefore, we remove it.")
             self._ast.remove_subtree(self)
@@ -534,16 +535,16 @@ def get_possible_case_candidate_condition(self) -> Optional[LogicCondition]:
             return self.reaching_condition & self.condition
         return None
 
-    def simplify_reaching_condition(self, z3_condition_of: Dict[LogicCondition, PseudoLogicCondition]):
+    def simplify_reaching_condition(self, condition_handler: ConditionHandler):
         """
         Add the reaching condition to the condition of the condition node if the false-branch does not exist. Otherwise, only simplify it.
         """
         self.clean()
         if self.false_branch is None and not self.reaching_condition.is_true:
             self.condition &= self.reaching_condition
-            self.condition.remove_redundancy(z3_condition_of)
+            self.condition.remove_redundancy(condition_handler)
             self.reaching_condition = LogicCondition.initialize_true(self.reaching_condition.context)
-        super().simplify_reaching_condition(z3_condition_of)
+        super().simplify_reaching_condition(condition_handler)
 
     def switch_branches(self):
         """Switch the true-branch and false-branch, this includes negating the condition."""

diff --git a/decompiler/structures/ast/syntaxforest.py b/decompiler/structures/ast/syntaxforest.py
@@ -395,7 +395,7 @@ def combine_cascading_single_branch_conditions(self, root: Optional[AbstractSynt
                     & condition_node.reaching_condition
                     & nested_condition_node.reaching_condition
                 )
-                condition_node.condition = new_condition.remove_redundancy(self.condition_handler.get_z3_condition_map())
+                condition_node.condition = new_condition.remove_redundancy(self.condition_handler)
                 condition_node.reaching_condition = self.condition_handler.get_true_value()
 
                 self.replace_condition_node_by_single_branch(nested_condition_node)