diff --git a/src/sindi/comparator.py b/src/sindi/comparator.py index ce4ed11..c98e528 100644 --- a/src/sindi/comparator.py +++ b/src/sindi/comparator.py @@ -7,6 +7,7 @@ from src.sindi.rewriter import Rewriter from src.sindi.utils import printer import z3 +import re class Comparator: @@ -51,16 +52,7 @@ def compare(self, predicate1: str, predicate2: str) -> str: # Convert ASTs to SymPy expressions expr1 = self._to_sympy_expr(ast1) expr2 = self._to_sympy_expr(ast2) - - - printer('*' * 140) - printer('*' * 140) - printer(f"expr1 this time is: {self.simplifier._to_sympy(ast1)}") - printer(f"expr2 this time is: {self.simplifier._to_sympy(ast2)}") - printer('*' * 140) - printer('*' * 140) - - + printer(f'> expr1: {expr1}') printer(f'> expr2: {expr2}') @@ -134,6 +126,19 @@ def _is_strict_vs_neq_same_operands(self, a, b): return False def _to_sympy_expr(self, ast): + def _sanitize_sym_name(s: str) -> str: + # keep alnum/underscore; collapse others to single '_' + s = re.sub(r"[^A-Za-z0-9_]", "_", str(s)) + s = re.sub(r"_+", "_", s).strip("_") + return s or "sym" + + def _symbol_from_call(func_name: str, arg_exprs): + # include args in the symbol name for disambiguation + parts = [_sanitize_sym_name(func_name)] + if arg_exprs: + parts.extend(_sanitize_sym_name(a) for a in arg_exprs) + return sp.Symbol("__".join(parts)) + if not ast.children: try: return sp.Number(float(ast.value)) if '.' in ast.value else sp.Number(int(ast.value)) @@ -145,20 +150,19 @@ def _to_sympy_expr(self, ast): return sp.false return sp.Symbol(ast.value.replace('.', '_')) - # Handle indexed attributes: a[b].c + + # Handle indexed attributes: a[b].c -> symbolic atom with args baked in if '[]' in ast.value and '.' in ast.value: - # Create a single function name from the complex expression - # e.g., "coinMap[].coinContract.balanceOf()" becomes a function call func_name = ast.value.replace('[]', '').replace('()', '').replace('.', '_') args = [self._to_sympy_expr(child) for child in ast.children] - return sp.Function(func_name)(*args) + return _symbol_from_call(func_name, args) # Handle indexing without attributes: a[b] if '[]' in ast.value: base_name = ast.value.replace('[]', '') base = sp.IndexedBase(base_name) index = self._to_sympy_expr(ast.children[0]) - return base[index] + return _symbol_from_call(base_name, [index]) args = [self._to_sympy_expr(child) for child in ast.children] @@ -198,8 +202,9 @@ def _to_sympy_expr(self, ast): elif ast.value == '*': return sp.Mul(*args) elif '()' in ast.value: - func_name = ast.value.replace('()', '') - return sp.Function(func_name)(*args) + # Treat calls as Boolean/unknown atoms so And/Or/Not accept them + func_name = ast.value.replace('()', '').replace('.', '_') + return _symbol_from_call(func_name, args) return sp.Symbol(ast.value.replace('.', '_')) diff --git a/src/sindi/rewriter.py b/src/sindi/rewriter.py index 6d4d98c..064067e 100644 --- a/src/sindi/rewriter.py +++ b/src/sindi/rewriter.py @@ -56,10 +56,10 @@ class Rewriter: _ETH_MULT = {"ether": 10**18, "gwei": 10**9, "wei": 1} - # ---------------- NEW: parenthesized assignment and finalization mask ---------------- + # ---------------- Parenthesized assignment and finalization mask ---------------- # Replace occurrences of '(var = expr)' with 'expr' (single '=' only). _PAREN_ASSIGN = re.compile( - r"\(\s*([A-Za-z_]\w*)\s*=\s*(.*?)\s*\)" + r"\(\s*([A-Za-z_]\w*)\s*=\s*(?![=])(.*?)\s*\)" ) # (X & MarketplaceLib.FLAG_MASK_FINALIZED) == 0 --> !MarketplaceLib.isFinalized(X) diff --git a/tests/comparator_test_set.json b/tests/comparator_test_set.json index d3ba558..0c16739 100644 --- a/tests/comparator_test_set.json +++ b/tests/comparator_test_set.json @@ -57,7 +57,8 @@ ["fee == 10**18 wei", "fee == 1000000000000000000"], ["x == 1e18 wei", "x == 1000000000000000000"], ["to != 0x0000000000000000000000000000000000000000", "to != address(0)"], - ["x == 0x80ac58cd", "x == type(IERC721).interfaceId"] + ["x == 0x80ac58cd", "x == type(IERC721).interfaceId"], + ["_msgSender() == owner || isApprovedForAll(owner, _msgSender())", "_msgSender() == owner || isApprovedForAll(owner, _msgSender())"] ], "The predicates are not equivalent and neither is stronger.": [ ["a > 0", "a < 0"],