Extended equivalence condition simplifier for latest target 7 result …

…(issue #415).
GaloisInc · Jun 27, 2024 · 44cae29 · 44cae29
1 parent c5778f5
commit 44cae29
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/pate_binja/pate.py b/pate_binja/pate.py
@@ -1313,6 +1313,7 @@ def acons(k: Any, v: Any, alist: list[list]) -> list[list]:
     'bvsle': 'bvsgt',
     'bvsgt': 'bvsle',
     'bvsge': 'bvslt',
+    'intle': 'intgt',
     '=': '!=',
     '!=': '='
 }
@@ -1326,6 +1327,10 @@ def acons(k: Any, v: Any, alist: list[list]) -> list[list]:
     'bvsle': '<=',
     'bvsgt': '>',
     'bvsge': '>=',
+    'intlt': '<',
+    'intle': '<=',
+    'intgt': '>',
+    'intge': '>=',
     'andp': '&',
     'orp': '|',
     'LTs' : '<',
@@ -1369,6 +1374,10 @@ def simplify_sexp(sexp, env=None):
     if re.fullmatch(r'read(?:LE|GE)\d+', op) and len(arg) == 2 and arg[0] == 'memory':
         return [op, arg[1]]
 
+    # Simplify sbvToInteger(x) => x
+    if op == 'sbvToInteger' and len(arg) == 1:
+        return arg[0]
+
     # Simplify multiply by 1
     if op == 'bvmul' and len(arg) == 2:
         if re.fullmatch(r'#x0*1', arg[0]):