[ValueError@z3_logic.py:107] ValueError: FOUND

[bugfinder-bot]

What happened?

  File "/opt/dewolf/decompiler/util/bugfinder/bugfinder.py", line 190, in iter_function_reports
    task_result = self.decompile(function, options)
  File "/opt/dewolf/decompile.py", line 51, in decompile
    pipeline.run(task)
  File "/opt/dewolf/decompiler/pipeline/pipeline.py", line 109, in run
    raise e
  File "/opt/dewolf/decompiler/pipeline/pipeline.py", line 102, in run
    instance.run(task)
  File "/opt/dewolf/decompiler/pipeline/controlflowanalysis/restructuring.py", line 46, in run
    self.asforest = AbstractSyntaxForest.generate_from_code_nodes([node.ast for node in self.t_cfg], self.t_cfg.condition_handler)
  File "/opt/dewolf/decompiler/structures/ast/syntaxforest.py", line 60, in generate_from_code_nodes
    asforest = AbstractSyntaxForest(condition_map)
  File "/opt/dewolf/decompiler/structures/ast/syntaxforest.py", line 41, in __init__
    self.switch_node_handler: SwitchNodeHandler = SwitchNodeHandler(condition_handler)
  File "/opt/dewolf/decompiler/structures/ast/switch_node_handler.py", line 70, in __init__
    self._initialize_case_node_properties_for_symbols()
  File "/opt/dewolf/decompiler/structures/ast/switch_node_handler.py", line 138, in _initialize_case_node_properties_for_symbols
    self._case_node_properties_of_symbol[symbol] = self.__get_case_node_property_of_symbol(symbol)
  File "/opt/dewolf/decompiler/structures/ast/switch_node_handler.py", line 151, in __get_case_node_property_of_symbol
    elif len(constants) == 0 and (zero_case_condition := self.__check_for_zero_case_condition(condition)):
  File "/opt/dewolf/decompiler/structures/ast/switch_node_handler.py", line 173, in __check_for_zero_case_condition
    ssa_condition = self.__get_z3_condition(ExpressionUsages(condition, tuple_ssa_usages))
  File "/opt/dewolf/decompiler/structures/ast/switch_node_handler.py", line 183, in __get_z3_condition
    z3_condition = self._z3_converter.convert(ssa_condition)
  File "/opt/dewolf/decompiler/structures/pseudo/logic.py", line 31, in convert
    return self._convert_condition(expression)
  File "/opt/dewolf/decompiler/structures/pseudo/z3_logic.py", line 91, in _convert_condition
    _operation = self._get_operation(condition)
  File "/opt/dewolf/decompiler/structures/pseudo/z3_logic.py", line 105, in _get_operation
    operands = self._ensure_same_sort([self.convert(operand) for operand in operation.operands])
  File "/opt/dewolf/decompiler/structures/pseudo/z3_logic.py", line 105, in <listcomp>
    operands = self._ensure_same_sort([self.convert(operand) for operand in operation.operands])
  File "/opt/dewolf/decompiler/structures/pseudo/logic.py", line 35, in convert
    return self._convert_operation(expression)
  File "/opt/dewolf/decompiler/structures/pseudo/z3_logic.py", line 100, in _convert_operation
    _operation = self._get_operation(operation)
  File "/opt/dewolf/decompiler/structures/pseudo/z3_logic.py", line 107, in _get_operation
    raise ValueError("FOUND")

Error class ValueError@z3_logic.py:107 contains 200 cases.

How to reproduce?

python decompile.py f46a41f3ee52bcaa4e63ddd083e1708a8e1d2f4aeba713652a83d99aa7d967ab sub_5400 --debug

sample: f46a41f3ee52bcaa4e63ddd083e1708a8e1d2f4aeba713652a83d99aa7d967ab case: https://bugfinder.seclab-bonn.de/case/1789/ dewolf commit: 1c34ffef Binaryninja version: 3.4.4271

[NeoQuix]

/cib

[github-actions[bot]]

Branch issue-273-_ValueError_z3_logic_py_107_ValueError_FOUND created!

[NeoQuix]

ValueError: Could not convert operation atoi(rax#1) into z3 logic. (ValueError@z3_logic.py:115) is a duplicate

[NeoQuix]

Solution: Ignore conditions which have calls in it