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

Breakup operations.py #516

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open
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
2 changes: 1 addition & 1 deletion claripy/ast/base.py
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@
from typing_extensions import Self

import claripy
from claripy import operations
from claripy.ast import operations
from claripy.errors import BackendError, ClaripyOperationError, ClaripyReplacementError
from claripy.fp import FSort

Expand Down
2 changes: 1 addition & 1 deletion claripy/ast/bool.py
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
from typing import TYPE_CHECKING, overload

import claripy
from claripy import operations
from claripy.ast import operations
from claripy.ast.base import ASTCacheKey, Base, _make_name
from claripy.errors import BackendError, ClaripyTypeError

Expand Down
2 changes: 1 addition & 1 deletion claripy/ast/bv.py
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
from typing_extensions import Self

import claripy
from claripy import operations
from claripy.ast import operations
from claripy.ast.base import _make_name
from claripy.errors import BackendError, ClaripyValueError
from claripy.util import deprecated
Expand Down
2 changes: 1 addition & 1 deletion claripy/ast/fp.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

import struct

from claripy import operations
from claripy.ast import operations
from claripy.ast.base import _make_name
from claripy.fp import FSORT_FLOAT, RM, FSort

Expand Down
229 changes: 7 additions & 222 deletions claripy/operations.py → claripy/ast/operations.py
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,8 @@

import claripy
import claripy.simplifications

from . import debug as _d
from .errors import ClaripyOperationError, ClaripyTypeError
from claripy import debug as _d
from claripy.errors import ClaripyOperationError, ClaripyTypeError


def op(name, arg_types, return_type, extra_check=None, calc_length=None):
Expand Down Expand Up @@ -177,172 +176,6 @@ def ext_length_calc(ext, orig):
# Operation lists
#

expression_arithmetic_operations = {
# arithmetic
"__add__",
"__radd__",
"__truediv__",
"__rtruediv__",
"__floordiv__",
"__rfloordiv__",
"__mul__",
"__rmul__",
"__sub__",
"__rsub__",
"__pow__",
"__rpow__",
"__mod__",
"__rmod__",
"SDiv",
"SMod",
"__neg__",
"__abs__",
}

bin_ops = {
"__add__",
"__radd__",
"__mul__",
"__rmul__",
"__or__",
"__ror__",
"__and__",
"__rand__",
"__xor__",
"__rxor__",
}

expression_comparator_operations = {
# comparisons
"__eq__",
"__ne__",
"__ge__",
"__le__",
"__gt__",
"__lt__",
}

# expression_comparator_operations = {
# 'Eq',
# 'Ne',
# 'Ge', 'Le',
# 'Gt', 'Lt',
# }

expression_bitwise_operations = {
# bitwise
"__invert__",
"__or__",
"__ror__",
"__and__",
"__rand__",
"__xor__",
"__rxor__",
"__lshift__",
"__rlshift__",
"__rshift__",
"__rrshift__",
}

expression_set_operations = {
# Set operations
"union",
"intersection",
"widen",
}

expression_operations = (
expression_arithmetic_operations
| expression_comparator_operations
| expression_bitwise_operations
| expression_set_operations
)

backend_comparator_operations = {
"SGE",
"SLE",
"SGT",
"SLT",
"UGE",
"ULE",
"UGT",
"ULT",
}

backend_bitwise_operations = {
"RotateLeft",
"RotateRight",
"LShR",
"Reverse",
}

backend_boolean_operations = {"And", "Or", "Not"}

backend_bitmod_operations = {"Concat", "Extract", "SignExt", "ZeroExt"}

backend_creation_operations = {"BoolV", "BVV", "FPV", "StringV"}

backend_symbol_creation_operations = {"BoolS", "BVS", "FPS", "StringS"}

backend_other_operations = {"If"}

backend_arithmetic_operations = {"SDiv", "SMod"}

backend_operations = (
backend_comparator_operations
| backend_bitwise_operations
| backend_boolean_operations
| backend_bitmod_operations
| backend_creation_operations
| backend_other_operations
| backend_arithmetic_operations
)
backend_operations_vsa_compliant = (
backend_bitwise_operations | backend_comparator_operations | backend_boolean_operations | backend_bitmod_operations
)
backend_operations_all = backend_operations | backend_operations_vsa_compliant

backend_fp_cmp_operations = {
"fpLT",
"fpLEQ",
"fpGT",
"fpGEQ",
"fpEQ",
}

backend_fp_operations = {
"FPS",
"fpToFP",
"fpToFPUnsigned",
"fpToIEEEBV",
"fpFP",
"fpToSBV",
"fpToUBV",
"fpNeg",
"fpSub",
"fpAdd",
"fpMul",
"fpDiv",
"fpAbs",
"fpIsNaN",
"fpIsInf",
"fpSqrt",
} | backend_fp_cmp_operations

backend_strings_operations = {
"StrSubstr",
"StrReplace",
"StrConcat",
"StrLen",
"StrContains",
"StrPrefixOf",
"StrSuffixOf",
"StrIndexOf",
"StrToInt",
"StrIsDigit",
"IntToStr",
}

opposites = {
"__add__": "__radd__",
"__radd__": "__add__",
Expand Down Expand Up @@ -402,45 +235,14 @@ def ext_length_calc(ext, orig):
"__rxor__": "__xor__",
}

inverse_operations = {
"__eq__": "__ne__",
"__ne__": "__eq__",
"__gt__": "__le__",
"__lt__": "__ge__",
"__ge__": "__lt__",
"__le__": "__gt__",
"ULT": "UGE",
"UGE": "ULT",
"UGT": "ULE",
"ULE": "UGT",
"SLT": "SGE",
"SGE": "SLT",
"SLE": "SGT",
"SGT": "SLE",
}
value_creation_operations = {"BoolV", "BVV", "FPV", "StringV"}
symbol_creation_operations = {"BoolS", "BVS", "FPS", "StringS"}

leaf_operations = backend_symbol_creation_operations | backend_creation_operations
leaf_operations_concrete = backend_creation_operations
leaf_operations_symbolic = backend_symbol_creation_operations
leaf_operations = symbol_creation_operations | value_creation_operations
leaf_operations_concrete = value_creation_operations
leaf_operations_symbolic = symbol_creation_operations
leaf_operations_symbolic_with_union = leaf_operations_symbolic | {"union"}

#
# Reversibility
#

not_invertible = {"union"}
reverse_distributable = {
"widen",
"union",
"intersection",
"__invert__",
"__or__",
"__ror__",
"__and__",
"__rand__",
"__xor__",
"__rxor__",
}

infix = {
"__add__": "+",
Expand Down Expand Up @@ -529,20 +331,3 @@ def ext_length_calc(ext, orig):
"Or": 12,
# 'Concat': '..',
}

commutative_operations = {
"__and__",
"__or__",
"__xor__",
"__add__",
"__mul__",
"And",
"Or",
"Xor",
}

bound_ops = {
"Not": "__invert__",
"And": "__and__",
"Or": "__or__",
}
2 changes: 1 addition & 1 deletion claripy/ast/strings.py
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
from __future__ import annotations

from claripy import operations
from claripy.ast import operations

from .base import Base, _make_name
from .bool import Bool
Expand Down
2 changes: 1 addition & 1 deletion claripy/backends/backend_concrete/backend_concrete.py
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,8 @@
from claripy.ast.strings import StringV
from claripy.backends.backend import Backend
from claripy.backends.backend_concrete import bv, fp, strings
from claripy.backends.operations import backend_fp_operations, backend_operations, backend_strings_operations
from claripy.errors import BackendError, UnsatError
from claripy.operations import backend_fp_operations, backend_operations, backend_strings_operations

log = logging.getLogger(__name__)

Expand Down
2 changes: 1 addition & 1 deletion claripy/backends/backend_vsa/backend_vsa.py
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,9 @@
from claripy.ast.base import Base
from claripy.ast.bv import ESI, SI, TSI
from claripy.backends.backend import Backend
from claripy.backends.operations import backend_operations_vsa_compliant, expression_set_operations
from claripy.balancer import Balancer
from claripy.errors import BackendError
from claripy.operations import backend_operations_vsa_compliant, expression_set_operations

from .bool_result import BoolResult, FalseResult, TrueResult
from .discrete_strided_interval_set import DiscreteStridedIntervalSet
Expand Down
2 changes: 1 addition & 1 deletion claripy/backends/backend_z3.py
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
from claripy.ast.fp import FP, FPV
from claripy.ast.strings import StringV
from claripy.backends.backend import Backend
from claripy.backends.operations import backend_fp_operations, backend_operations, backend_strings_operations, bound_ops
from claripy.errors import (
BackendError,
ClaripyError,
Expand All @@ -29,7 +30,6 @@
ClaripyZ3Error,
)
from claripy.fp import RM, FSort
from claripy.operations import backend_fp_operations, backend_operations, backend_strings_operations, bound_ops

log = logging.getLogger(__name__)

Expand Down
Loading
Loading