Skip to content

Commit a34d106

Browse files
committed
Fix AST optimizations incorrectly eliminating symbolic expressions
Three optimizations (A^A=0, A|A=A, A-A=0) were using equalTo() to detect identical operands. However, equalTo() compares concrete values rather than AST structure, causing different symbolic expressions with the same concrete value to be incorrectly identified as equal. This caused the optimizer to eliminate symbolic information: - bvxor: A^A=0 replaced symbolic XOR with concrete 0 - bvsub: A-A=0 replaced symbolic SUB with concrete 0 - bvor: A|A=A returned one operand, losing the other's dependency Example: In AArch64 cfSub_s(), the carry flag computation would lose symbolic status when symbolic operands evaluated to 0, breaking conditional branch symbolization (e.g., b.lo not recognized as symbolic). The fix adds isSymbolized() checks to ensure these optimizations only apply when both operands are concrete, preserving symbolic information. Note: bvand already had the correct check; this fix makes bvor, bvsub, and bvxor consistent with that pattern.
1 parent 8b43626 commit a34d106

File tree

1 file changed

+10
-3
lines changed

1 file changed

+10
-3
lines changed

src/libtriton/ast/astContext.cpp

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -353,7 +353,9 @@ namespace triton {
353353
return this->bv(expr2->getBitvectorMask(), expr2->getBitvectorSize());
354354

355355
/* Optimization: A | A = A */
356-
if (expr1->equalTo(expr2))
356+
/* Only apply when both operands are concrete. Two different symbolic expressions
357+
* may evaluate to the same value but represent distinct computations. */
358+
if (!expr1->isSymbolized() && !expr2->isSymbolized() && expr1->equalTo(expr2))
357359
return expr1;
358360
}
359361

@@ -603,7 +605,9 @@ namespace triton {
603605
return this->bvneg(expr2);
604606

605607
/* Optimization: A - A = 0 */
606-
if (expr1->equalTo(expr2))
608+
/* Only apply when both operands are concrete to preserve symbolic information.
609+
* Different symbolic expressions may evaluate equal but must remain distinct. */
610+
if (!expr1->isSymbolized() && !expr2->isSymbolized() && expr1->equalTo(expr2))
607611
return this->bv(0, expr1->getBitvectorSize());
608612
}
609613

@@ -732,7 +736,10 @@ namespace triton {
732736
return expr2;
733737

734738
/* Optimization: A ^ A = 0 */
735-
if (expr1->equalTo(expr2))
739+
/* Only apply when both operands are concrete to avoid losing symbolic information.
740+
* Two different symbolic expressions may have the same concrete value temporarily,
741+
* but they represent different symbolic computations that must be preserved. */
742+
if (!expr1->isSymbolized() && !expr2->isSymbolized() && expr1->equalTo(expr2))
736743
return this->bv(0, expr1->getBitvectorSize());
737744
}
738745

0 commit comments

Comments
 (0)