Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow simplifications to handle annotations #548

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions claripy/ast/base.py
Original file line number Diff line number Diff line change
Expand Up @@ -246,7 +246,7 @@ def make_like(
length: int | None = None,
) -> Self:
# Try to simplify the expression again
simplified = claripy.simplifications.simplify(op, args) if simplify else None
simplified, annotated = claripy.simplifications.simplify(op, args) if simplify else (None, False)
if simplified is not None:
op = simplified.op
if ( # fast path
Expand Down Expand Up @@ -294,7 +294,10 @@ def make_like(
# special case: if self is one of the args, we do not copy annotations over from self since child
# annotations will be re-processed during AST creation.
if annotations is None:
annotations = self.annotations if not args or not any(self is arg for arg in args) else ()
if not annotated:
annotations = self.annotations if not args or not any(self is arg for arg in args) else ()
else:
annotations = simplified.annotations
if variables is None and op in all_operations:
variables = self.variables
if uninitialized is None:
Expand Down
10 changes: 5 additions & 5 deletions claripy/operations.py
Original file line number Diff line number Diff line change
Expand Up @@ -54,9 +54,12 @@ def _op(*args):
raise ClaripyOperationError(msg)

# pylint:disable=too-many-nested-blocks
simp = _handle_annotations(claripy.simplifications.simplify(name, fixed_args), args)
simp, annotated = claripy.simplifications.simplify(name, fixed_args)
if simp is not None:
return simp
if not annotated:
simp = _handle_annotations(simp, fixed_args)
if simp is not None:
return simp

kwargs = {}
if calc_length is not None:
Expand All @@ -73,9 +76,6 @@ def _op(*args):


def _handle_annotations(simp, args):
if simp is None:
return None

# pylint:disable=isinstance-second-argument-not-valid-type
ast_args = tuple(a for a in args if isinstance(a, claripy.ast.Base))
preserved_relocatable = frozenset(simp._relocatable_annotations)
Expand Down
34 changes: 20 additions & 14 deletions claripy/simplifications.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,14 @@
import itertools
import operator
from functools import reduce
from typing import TYPE_CHECKING

import claripy
from claripy.fp import FSORT_DOUBLE, FSORT_FLOAT

if TYPE_CHECKING:
from claripy.ast.base import Base

SIMPLE_OPS = ("Concat", "SignExt", "ZeroExt")

extract_distributable = {
Expand Down Expand Up @@ -829,7 +833,7 @@ def extract_simplifier(high, low, val):

# avoid extracting if we need the full value
if new_high == result.length - 1 and low_loc == 0:
return result
return result, True

# else extract the part we need
return result[new_high:low_loc]
Expand Down Expand Up @@ -1110,13 +1114,10 @@ def zeroext_comparing_against_simplifier(op, a, b):
return None


_simple_bool_simplifiers = {
_all_simplifiers = {
"And": boolean_and_simplifier,
"Or": boolean_or_simplifier,
"Not": boolean_not_simplifier,
}

_all_simplifiers = _simple_bool_simplifiers | {
"Reverse": bv_reverse_simplifier,
"Extract": extract_simplifier,
"Concat": concat_simplifier,
Expand All @@ -1141,16 +1142,21 @@ def zeroext_comparing_against_simplifier(op, a, b):
"__invert__": invert_simplifier,
}

# the actual functions
# the actual function


def simplify_bool_condition(op, args):
if op not in _simple_bool_simplifiers:
return None
return _simple_bool_simplifiers[op](*args)

def simplify(op, args) -> tuple[Base | None, bool]:
"""Simplifies the given operation with the given arguments. Returns the
simplified result if possible, along with a boolean representing whether
annotations were handled by the simplifier.
"""

def simplify(op, args):
if op not in _all_simplifiers:
return None
return _all_simplifiers[op](*args)
return None, False

simplified = _all_simplifiers[op](*args)

if isinstance(simplified, tuple):
return simplified[0], simplified[1]

return simplified, False