angr / angr/claripy

Length matching error when using the `and` bit operation on two conditional expressions

Đang mở
#383 1 bình luận 0 reaction 0 người được giao Xem trên GitHub
bug needs-triage
Ngôn ngữ chính
Python
Star
334
Fork
105
Merge trung bình
6 giờ 1 phút
Pull request đã merge (30 ngày)
3

Mô tả

### 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_

Hướng dẫn đóng góp

Chưa lập chỉ mục được hướng dẫn đóng góp cho kho mã nguồn này

Đánh giá

Issue này chưa được đánh giá.

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.