Length matching error when using the `and` bit operation on two conditional expressions
Opened this issue · 1 comments
Description
I use two conditional expressions to execute &
bit arithmetic operation. But failed in length check.
│ /home/squ/Projects/self-proj/Warden/src/see/engine.py:382 in exec_branch │
│ │
│ 379 │ │ │ elif op == const.opcode.AND: │
│ 380 │ │ │ │ [s0, s1] = state.stack_pop(2) │
│ 381 │ │ │ │ # fix for python10 claripy │
│ ❱ 382 │ │ │ │ state.stack_push(s0 & s1) │
│ 383 │ │ │ │ # state.stack_push( │
│ 384 │ │ │ │ # claripy.If( │
│ 385 │ │ │ │ # claripy.And((s0 != BVV0), (s1 != BVV0)), │
│ │
│ ╭─────────────────────────────────────────── locals ───────────────────────────────────────────╮ │
│ │ bps = [] │ │
│ │ curinst = <Instruction name=AND address=0x6ea size=1 > │ │
│ │ depth = 3 │ │
│ │ op = 22 │ │
│ │ pushnum = 32 │ │
│ │ s0 = <BV256 if input-uint256_2_256 != 0x0 then 0x1 else 0x0> │ │
│ │ s1 = <BV256 if 0x2 > 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff │ │
│ │ / input-uint256_2_256 then 0x1 else 0x0> │ │
│ │ self = <see.engine.SymExecEngine object at 0x7fb09f40ea70> │ │
│ │ state = State( │ │
│ │ selfdestruct_to = None │ │
│ │ pc = 6ea │ │
│ │ calls = [] │ │
│ │ storage = 1 <BV256 (0xff & LShR(LShR(LShR(input-uint256_3_256, 0x8), 0x8), 0x8)) * │ │
│ │ 0x1 | 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00 & (0x100 │ │
│ │ * (0x0 .. input-uint256_3_256[23:16]) | (0x10000 * (0x0 .. │ │
│ │ input-uint256_3_256[15:8])[255:16] | (0x1000000 * (0x0 .. │ │
│ │ input-uint256_3_256[7:0])[255:24] .. 0) .. 0x0))> │ │
│ │ │ │
│ │ solver = <claripy.solvers.Solver object at 0x7fb09ef79e40> │ │
│ │ ) │ │
│ │ txn = <evm.transaction.Transaction object at 0x7fb09ef7aaa0> │ │
│ ╰──────────────────────────────────────────────────────────────────────────────────────────────╯ │
│ │
│ /home/squ/.local/lib/python3.10/site-packages/claripy/operations.py:57 in _op │
│ │
│ 54 │ │ │ │ │ raise ClaripyOperationError(msg) │
│ 55 │ │ │
│ 56 │ │ # pylint:disable=too-many-nested-blocks │
│ ❱ 57 │ │ simp = _handle_annotations(simplifications.simpleton.simplify(name, fixed_args), │
│ 58 │ │ if simp is not None: │
│ 59 │ │ │ return simp │
│ 60 │
│ │
│ ╭─────────────────────────────────────────── locals ───────────────────────────────────────────╮ │
│ │ _type_fixer = <function op.<locals>._type_fixer at 0x7fb0a53765f0> │ │
│ │ args = ( │ │
│ │ │ <BV256 if input-uint256_2_256 != 0x0 then 0x1 else 0x0>, │ │
│ │ │ <BV256 if 0x2 > │ │
│ │ 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff / │ │
│ │ input-uint256_2_256 then 0x1 else 0x0> │ │
│ │ ) │ │
│ │ calc_length = <function basic_length_calc at 0x7fb0a559ff40> │ │
│ │ extra_check = <function length_same_check at 0x7fb0a559feb0> │ │
│ │ fixed_args = ( │ │
│ │ │ <BV256 if input-uint256_2_256 != 0x0 then 0x1 else 0x0>, │ │
│ │ │ <BV256 if 0x2 > │ │
│ │ 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff / │ │
│ │ input-uint256_2_256 then 0x1 else 0x0> │ │
│ │ ) │ │
│ │ i = <BV256 if 0x2 > │ │
│ │ 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff / │ │
│ │ input-uint256_2_256 then 0x1 else 0x0> │ │
│ │ msg = "args' length must all be equal" │ │
│ │ name = '__and__' │ │
│ │ return_type = <class 'claripy.ast.bv.BV'> │ │
│ │ success = True │ │
│ ╰──────────────────────────────────────────────────────────────────────────────────────────────╯ │
│ │
│ /home/squ/.local/lib/python3.10/site-packages/claripy/simplifications.py:43 in simplify │
│ │
│ 40 │ def simplify(self, op, args): │
│ 41 │ │ if op not in self._simplifiers: │
│ 42 │ │ │ return None │
│ ❱ 43 │ │ return self._simplifiers[op](*args) │
│ 44 │ │
│ 45 │ @staticmethod │
│ 46 │ def _deduplicate_filter(args): │
│ │
│ ╭─────────────────────────────────────────── locals ───────────────────────────────────────────╮ │
│ │ args = ( │ │
│ │ │ <BV256 if input-uint256_2_256 != 0x0 then 0x1 else 0x0>, │ │
│ │ │ <BV256 if 0x2 > │ │
│ │ 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff / │ │
│ │ input-uint256_2_256 then 0x1 else 0x0> │ │
│ │ ) │ │
│ │ op = '__and__' │ │
│ │ self = <claripy.simplifications.SimplificationManager object at 0x7fb0a55dc5b0> │ │
│ ╰──────────────────────────────────────────────────────────────────────────────────────────────╯ │
│ │
│ /home/squ/.local/lib/python3.10/site-packages/claripy/simplifications.py:734 in │
│ bitwise_and_simplifier │
│ │
│ 731 │ │ │ # if(cond0, 1, 0) & if(cond1, 1, 0) -> if(cond0 & cond1, 1, 0) │
│ 732 │ │ │ if a.op == "If" and b.op == "If": │
│ 733 │ │ │ │ if ( │
│ ❱ 734 │ │ │ │ │ (a.args[1] == ast.all_operations.BVV(1, 1)).is_true() │
│ 735 │ │ │ │ │ and (a.args[2] == ast.all_operations.BVV(0, 1)).is_true() │
│ 736 │ │ │ │ │ and (b.args[1] == ast.all_operations.BVV(1, 1)).is_true() │
│ 737 │ │ │ │ │ and (b.args[2] == ast.all_operations.BVV(0, 1)).is_true() │
│ │
│ ╭─────────────────────────────────────────── locals ───────────────────────────────────────────╮ │
│ │ a = <BV256 if input-uint256_2_256 != 0x0 then 0x1 else 0x0> │ │
│ │ args = () │ │
│ │ b = <BV256 if 0x2 > 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff / │ │
│ │ input-uint256_2_256 then 0x1 else 0x0> │ │
│ │ r = None │ │
│ ╰──────────────────────────────────────────────────────────────────────────────────────────────╯ │
│ │
│ /home/squ/.local/lib/python3.10/site-packages/claripy/operations.py:54 in _op │
│ │
│ 51 │ │ │ if extra_check is not None: │
│ 52 │ │ │ │ success, msg = extra_check(*fixed_args) │
│ 53 │ │ │ │ if not success: │
│ ❱ 54 │ │ │ │ │ raise ClaripyOperationError(msg) │
│ 55 │ │ │
│ 56 │ │ # pylint:disable=too-many-nested-blocks │
│ 57 │ │ simp = _handle_annotations(simplifications.simpleton.simplify(name, fixed_args), │
│ │
│ ╭────────────────────────────── locals ──────────────────────────────╮ │
│ │ _type_fixer = <function op.<locals>._type_fixer at 0x7fb0a5375360> │ │
│ │ args = (<BV256 0x1>, <BV1 1>) │ │
│ │ calc_length = None │ │
│ │ extra_check = <function length_same_check at 0x7fb0a559feb0> │ │
│ │ fixed_args = (<BV256 0x1>, <BV1 1>) │ │
│ │ i = <BV1 1> │ │
│ │ msg = "args' length must all be equal" │ │
│ │ name = '__eq__' │ │
│ │ return_type = <class 'claripy.ast.bool.Bool'> │ │
│ │ success = False │ │
│ ╰────────────────────────────────────────────────────────────────────╯ │
╰──────────────────────────────────────────────────────────────────────────────────────────────────╯
Steps to reproduce the bug
a = BVS("uint256-a", 256)
b = BVS("uint256-b", 256)
BVV0 = BVV(0, 256)
BVV1 = BVV(1, 256)
solver = Solver()
# solver.add(Not(a == 0))
c = If(a > 0, BVV(0xff, 256), BVV0)
d = If(b < 0xff, BVV(0xff, 256), BVV0)
e = (c ^ d)
print(e) # work
e = (c | d)
print(e) # work
e = (c & d)
print(e) # !!! raise ClaripyOperationError(claripy.errors.ClaripyOperationError: args' length must all be equal)
Environment
angr environment report
Date: 2023-12-25 19:30:05.904681
!!! running in global environment. Are you sure? !!!
Platform: linux-x86_64
Python version: 3.10.12 (main, Nov 20 2023, 15:14:05) [GCC 11.4.0]
######## angr #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/angr/init.py
Pip version angr 9.2.81
Couldn't find git info
######## ailment #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/ailment/init.py
Pip version ailment 9.2.81
Couldn't find git info
######## cle #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/cle/init.py
Pip version cle 9.2.81
Couldn't find git info
######## pyvex #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/pyvex/init.py
Pip version pyvex 9.2.81
Couldn't find git info
######## claripy #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/claripy/init.py
Pip version claripy 9.2.81
Couldn't find git info
######## archinfo #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/archinfo/init.py
Pip version archinfo 9.2.81
Couldn't find git info
######## z3 #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/z3/init.py
Pip version z3-solver 4.10.2.0
Couldn't find git info
######## unicorn #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/unicorn/init.py
Pip version unicorn 2.0.1.post1
Couldn't find git info
######### Native Module Info ##########
angr: <CDLL '/home/squ/.local/lib/python3.10/site-packages/angr/state_plugins/../lib/angr_native.so', handle 55c215f60590 at 0x7f463e041d80>
unicorn: <CDLL '/home/squ/.local/lib/python3.10/site-packages/unicorn/lib/libunicorn.so.2', handle 55c215a70b20 at 0x7f4640d21630>
pyvex: <cffi.api._make_ffi_library..FFILibrary object at 0x7f4641a1e320>
z3: <CDLL '/home/squ/.local/lib/python3.10/site-packages/z3/lib/libz3.so', handle 55c215737340 at 0x7f4643bfb7c0>
Additional context
No response
I encounter this issue locally when trying to decompile the main
function from the
Free Madame De Maintenon – CTF Challenge:
$ angr-management
(python:51985): dbind-WARNING **: 17:52:35.514: AT-SPI: Error retrieving accessibility bus address: org.freedesktop.DBus.Error.ServiceUnknown: The name org.a11y.Bus was not provided by any .service files
0.00s - Debugger warning: It seems that frozen modules are being used, which may
0.00s - make the debugger miss breakpoints. Please pass -Xfrozen_modules=off
0.00s - to python to disable frozen modules.
0.00s - Note: Debugging will proceed. Set PYDEVD_DISABLE_FILE_VALIDATION=1 to disable this validation.
INFO | 2024-01-17 17:52:54,455 | angrmanagement.data.jobs.job | Job "Loading file" started
WARNING | 2024-01-17 17:52:54,471 | cle.backends.backend | Unused kwargs for loading binary /home/jvoisin/Downloads/challenge: ignore_missing_arch
INFO | 2024-01-17 17:53:01,693 | angrmanagement.data.jobs.job | Job "Loading file" completed after 7.24 seconds
INFO | 2024-01-17 17:53:01,693 | angrmanagement.data.jobs.job | Job "CFG generation" started
INFO | 2024-01-17 17:53:02,067 | angrmanagement.data.jobs.job | Job "CFG generation" completed after 0.37 seconds
INFO | 2024-01-17 17:53:02,144 | angrmanagement.data.jobs.job | Job "Applying FLIRT signatures" started
WARNING | 2024-01-17 17:53:02,145 | angrmanagement.data.jobs.flirt_signature_recognition | No FLIRT signatures exist for architecture AMD64.
INFO | 2024-01-17 17:53:02,145 | angrmanagement.data.jobs.job | Job "Applying FLIRT signatures" completed after 0.00 seconds
INFO | 2024-01-17 17:53:02,166 | angrmanagement.data.jobs.job | Job "Function prototype finding" started
INFO | 2024-01-17 17:53:02,166 | angrmanagement.data.jobs.job | Job "Function prototype finding" completed after 0.00 seconds
INFO | 2024-01-17 17:53:02,207 | angrmanagement.data.jobs.job | Job "Variable Recovery" started
WARNING | 2024-01-17 17:53:02,225 | angr.analyses.variable_recovery.engine_vex.SimEngineVRVEX | Unsupported Binop Iop_MullU64.
WARNING | 2024-01-17 17:53:02,554 | angr.analyses.reaching_definitions.engine_vex.SimEngineRDVEX | Unsupported Binop Iop_64HLto128.
INFO | 2024-01-17 17:53:02,928 | angrmanagement.data.jobs.job | Job "Variable Recovery" completed after 0.72 seconds
INFO | 2024-01-17 17:53:14,888 | angrmanagement.data.jobs.job | Job "Variable Recovery" started
INFO | 2024-01-17 17:53:14,982 | angrmanagement.data.jobs.job | Job "Variable Recovery" completed after 0.09 seconds
INFO | 2024-01-17 17:53:14,995 | angrmanagement.data.jobs.job | Job "Decompiling" started
ERROR | 2024-01-17 17:53:15,116 | angrmanagement.data.instance | Exception while running job "Decompiling":
Traceback (most recent call last):
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angrmanagement/data/instance.py", line 343, in _worker
result = job.run(self)
^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angrmanagement/data/jobs/job.py", line 69, in run
r = self._run(inst)
^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angrmanagement/data/jobs/decompile_function.py", line 17, in _run
decompiler = inst.project.analyses.Decompiler(
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 216, in __call__
r = w(*args, **kwargs)
^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 201, in wrapper
oself.__init__(*args, **kwargs)
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/decompiler.py", line 97, in __init__
self._decompile()
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/decompiler.py", line 158, in _decompile
clinic = self.project.analyses.Clinic(
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 216, in __call__
r = w(*args, **kwargs)
^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 201, in wrapper
oself.__init__(*args, **kwargs)
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/clinic.py", line 142, in __init__
self._analyze_for_decompiling()
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/clinic.py", line 245, in _analyze_for_decompiling
self._simplify_function(
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/utils/timing.py", line 43, in timed_func
return func(*args, **kwargs)
^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/clinic.py", line 837, in _simplify_function
simplified = self._simplify_function_once(
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/utils/timing.py", line 43, in timed_func
return func(*args, **kwargs)
^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/clinic.py", line 867, in _simplify_function_once
simp = self.project.analyses.AILSimplifier(
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 216, in __call__
r = w(*args, **kwargs)
^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 201, in wrapper
oself.__init__(*args, **kwargs)
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/ail_simplifier.py", line 104, in __init__
self._simplify()
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/ail_simplifier.py", line 117, in _simplify
folded_exprs = self._fold_exprs()
^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/ail_simplifier.py", line 538, in _fold_exprs
propagator = self._compute_propagation(immediate_stmt_removal=True)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/ail_simplifier.py", line 198, in _compute_propagation
reaching_definitions=self._compute_reaching_definitions(),
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/ail_simplifier.py", line 178, in _compute_reaching_definitions
rd = self.project.analyses.ReachingDefinitions(
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 216, in __call__
r = w(*args, **kwargs)
^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 201, in wrapper
oself.__init__(*args, **kwargs)
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/reaching_definitions.py", line 202, in __init__
self._analyze()
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/forward_analysis/forward_analysis.py", line 252, in _analyze
self._analysis_core_graph()
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/forward_analysis/forward_analysis.py", line 269, in _analysis_core_graph
changed, output_state = self._run_on_node(n, job_state)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/reaching_definitions.py", line 524, in _run_on_node
state = engine.process(
^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 85, in process
self._process(
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/engines/light/engine.py", line 807, in _process
self._process_Stmt(whitelist=whitelist)
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 119, in _process_Stmt
super()._process_Stmt(whitelist=whitelist)
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/engines/light/engine.py", line 823, in _process_Stmt
self._handle_Stmt(stmt)
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 130, in _handle_Stmt
handler(stmt)
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 153, in _ail_handle_Assignment
src = self._expr(stmt.src)
^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 141, in _expr
return handler(expr)
^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 636, in _ail_handle_BinaryOp
r = super()._ail_handle_BinaryOp(expr)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/engines/light/engine.py", line 960, in _ail_handle_BinaryOp
return handler(expr)
^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 719, in _ail_handle_DivMod
return self._ail_handle_Div(expr)
^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 781, in _ail_handle_Div
r = MultiValues(offset_to_values={0: {expr0_v / expr1_v}})
~~~~~~~~^~~~~~~~~
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/claripy/utils/deprecated.py", line 16, in inner
return func(*args, **kwargs)
^^^^^^^^^^^^^^^^^^^^^
File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/claripy/operations.py", line 54, in _op
raise ClaripyOperationError(msg)
claripy.errors.ClaripyOperationError: args' length must all be equal
$