fix(z3): catch edge case with regex with nested XORs

bliutech · Jul 19, 2024 · da4e1e5 · da4e1e5
1 parent 030c08d
commit da4e1e5
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/solver/passes/z3_pass.py b/solver/passes/z3_pass.py
@@ -34,11 +34,12 @@ def run_pass(ast: Expr) -> Expr:
     # this is a hack to fix that
 
     # Pattern to match "Xor(A, B)"
-    pattern = r"Xor\((\w+), (\w+)\)"
+    pattern = r"Xor\(([A-Z \|&\^\(\)]+), ([A-Z \|&\^\(\)]+)\)"
     # Replacement string using backreferences to capture groups
     replacement = r"\1 ^ \2"
-    # Performing the replacement
-    simplifiedStr = re.sub(pattern, replacement, simplifiedStr)
+    # Performing the replacement. Loop to catch nested Xor calls
+    while re.match(pattern, simplifiedStr):
+        simplifiedStr = re.sub(pattern, replacement, simplifiedStr)
 
     l: Lexer = Lexer()
     l.lex(simplifiedStr)