Commit 1420e2a
committed
Fix bvxor A^A=0 optimization incorrectly eliminating symbolic expressions
The A^A=0 optimization in bvxor() was using equalTo() to detect when
both operands are the same expression. However, equalTo() compares
concrete values, hash, size, and level - not AST structure.
This caused a bug where two different symbolic expressions that
happened to evaluate to the same concrete value (e.g., both evaluating
to 0) would be incorrectly identified as equal, causing the optimizer
to replace the symbolic XOR with a concrete 0.
Example scenario:
- op1: symbolic register w8, evaluates to 0
- op2: bvxor(concrete_val, symbolic_result), also evaluates to 0
- bvxor(op1, op2) incorrectly returns concrete 0 instead of
preserving the symbolic computation
This broke symbolic execution of AArch64 conditional branches where
the carry flag (computed via XOR operations in cfSub_s) would lose
its symbolic status, causing branches like b.lo to not be recognized
as symbolized.
The fix adds isSymbolized() checks to ensure the A^A=0 optimization
only applies when both operands are concrete. When either operand is
symbolic, the full XOR node is preserved to maintain symbolic
information flow.1 parent 8b43626 commit 1420e2a
1 file changed
+4
-1
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
732 | 732 | | |
733 | 733 | | |
734 | 734 | | |
735 | | - | |
| 735 | + | |
| 736 | + | |
| 737 | + | |
| 738 | + | |
736 | 739 | | |
737 | 740 | | |
738 | 741 | | |
| |||
0 commit comments