Fix AST optimization bug incorrectly eliminating symbolic expressions

[JexAmro]

AST Optimization Bug

Three AST optimizations (A^A=0, A-A=0, A|A=A) use equalTo() to detect when both operands
are identical. However, equalTo() compares concrete evaluation values rather than AST structure:

bool AbstractNode::equalTo(const SharedAbstractNode& other) const {
  return (this->evaluate() == other->evaluate()) &&
         (this->getBitvectorSize() == other->getBitvectorSize()) &&
         (this->getHash() == other->getHash()) &&
         (this->getLevel() == other->getLevel());
}

This causes different symbolic expressions to be considered "equal" if they happen to have the same
concrete value, hash, size, and level at evaluation time, leading to incorrect symbolic
information elimination.

Affected Operations

Function	Optimization	Behavior	Impact
bvxor	A ^ A = 0	Returns concrete 0	Loses ALL symbolic info
bvsub	A - A = 0	Returns concrete 0	Loses ALL symbolic info
bvor	A | A = A	Returns one operand	Loses other operand's dependency

Note: bvand already had the correct check (!expr1->isSymbolized() && !expr2->isSymbolized()). This
fix makes the other three operations consistent with that pattern.

Impact

When symbolic expressions are incorrectly replaced with concrete values or have dependencies
removed, downstream symbolic analysis breaks.

Real-World Reproduction (AArch64)

ldr w8, [sp, #4]     ; w8 = symbolic value (happens to evaluate to 0)
ldr w9, [sp, #0xc]   ; w9 = concrete 0
subs w8, w8, w9      ; should set symbolic carry flag
b.lo #target         ; should be symbolized, but isn't

In the cfSub_s() semantics for the carry flag computation:
cf = (MSB(((op1 ^ op2 ^ result) ^ ((op1 ^ result) & (op1 ^ op2))))) ^ 1

When op1 (symbolic, eval=0) is XORed with other expressions that also evaluate to 0, the A^A=0
optimization incorrectly triggers:

• [bvxor] Optimization A^A=0 triggered
• [bvxor] expr1 sym=1 eval=0
• [bvxor] expr2 sym=1 eval=0

Result: The carry flag becomes concrete instead of symbolic, causing the conditional branch b.lo to
not be recognized as symbolized, breaking path exploration.

Solution

Add isSymbolized() checks to ensure these optimizations only apply when both operands are concrete:

/* bvxor - A ^ A = 0 */
if (!expr1->isSymbolized() && !expr2->isSymbolized() && expr1->equalTo(expr2))
  return this->bv(0, expr1->getBitvectorSize());

/* bvsub - A - A = 0 */
if (!expr1->isSymbolized() && !expr2->isSymbolized() && expr1->equalTo(expr2))
  return this->bv(0, expr1->getBitvectorSize());

/* bvor - A | A = A */
if (!expr1->isSymbolized() && !expr2->isSymbolized() && expr1->equalTo(expr2))
  return expr1;

This preserves symbolic information while still allowing optimizations for concrete expressions.

Systematic Fix

This PR fixes a systematic bug across three AST operations. The pattern was:

• bvand - already correct (had the symbolized checks)
• bvor - fixed by adding symbolized checks
• bvsub - fixed by adding symbolized checks
• bvxor - fixed by adding symbolized checks

All three now follow the same safe pattern as bvand.

Testing

• Verified fix resolves the AArch64 conditional branch symbolization issue
• All three optimizations now preserve symbolic information correctly
• Concrete-only optimization paths still function as expected

[JonathanSalwan]

Thx a lot for this reporting! Do we have to apply this patch also for these two ones?

• A | A = A
• A - A = 0

[JexAmro]

Yes should patch both! I have just tested and confirmed that "A - A = 0" is an identical issue and it occurs a lot in Arch64.
"A | A = A" has less impact but obviously significantly reduces exploration and constraint solving.

[JonathanSalwan]

Can you add those two in your patch and then I will merge :)

[JexAmro]

Yes, already planning to do but after testing. Will test and update the patch first thing tomorrow. Thanks for your fast response on this!

[JexAmro]

Done!