Length matching error when using the `and` bit operation on two conditional expressions
- Langage dominant
- Python
- Étoiles
- 334
- Forks
- 105
- Merge moyen
- 6 h 1 min
- PR mergées (30 j)
- 3
Description
### Description
I use two conditional expressions to execute `&` bit arithmetic operation. But failed in length check.
```shell
│ /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 = │ │
│ │ depth = 3 │ │
│ │ op = 22 │ │
│ │ pushnum = 32 │ │
│ │ s0 = │ │
│ │ s1 = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff │ │
│ │ / input-uint256_2_256 then 0x1 else 0x0> │ │
│ │ self = │ │
│ │ state = State( │ │
│ │ selfdestruct_to = None │ │
│ │ pc = 6ea │ │
│ │ calls = [] │ │
│ │ storage = 1 │ │
│ │ │ │
│ │ solver = │ │
│ │ ) │ │
│ │ txn = │ │
│ ╰──────────────────────────────────────────────────────────────────────────────────────────────╯ │
│ │
│ /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 = ._type_fixer at 0x7fb0a53765f0> │ │
│ │ args = ( │ │
│ │ │ , │ │
│ │ │ │ │
│ │ 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff / │ │
│ │ input-uint256_2_256 then 0x1 else 0x0> │ │
│ │ ) │ │
│ │ calc_length = │ │
│ │ extra_check = │ │
│ │ fixed_args = ( │ │
│ │ │ , │ │
│ │ │ │ │
│ │ 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff / │ │
│ │ input-uint256_2_256 then 0x1 else 0x0> │ │
│ │ ) │ │
│ │ i = │ │
│ │ 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff / │ │
│ │ input-uint256_2_256 then 0x1 else 0x0> │ │
│ │ msg = "args' length must all be equal" │ │
│ │ name = '__and__' │ │
│ │ return_type = │ │
│ │ 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 = ( │ │
│ │ │ , │ │
│ │ │ │ │
│ │ 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff / │ │
│ │ input-uint256_2_256 then 0x1 else 0x0> │ │
│ │ ) │ │
│ │ op = '__and__' │ │
│ │ self = │ │
│ ╰──────────────────────────────────────────────────────────────────────────────────────────────╯ │
│ │
│ /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 = │ │
│ │ args = () │ │
│ │ b = 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 = ._type_fixer at 0x7fb0a5375360> │ │
│ │ args = (, ) │ │
│ │ calc_length = None │ │
│ │ extra_check = │ │
│ │ fixed_args = (, ) │ │
│ │ i = │ │
│ │ msg = "args' length must all be equal" │ │
│ │ name = '__eq__' │ │
│ │ return_type = │ │
│ │ success = False │ │
│ ╰────────────────────────────────────────────────────────────────────╯ │
╰──────────────────────────────────────────────────────────────────────────────────────────────────╯
```
### Steps to reproduce the bug
```python
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:
unicorn:
pyvex: .FFILibrary object at 0x7f4641a1e320>
z3:
### Additional context
_No response_
Guide de contribution
Aucun guide de contribution indexé pour ce dépôt
Évaluation
Cette issue n'a pas encore été évaluée.