angr / claripy

An abstraction layer for constraint solvers.
BSD 2-Clause "Simplified" License
284 stars 93 forks source link

Over-design for `BackendManager`? #353

Closed syheliel closed 2 weeks ago

syheliel commented 1 year ago

Description

claripy.backends is originally a submodule of claripy, but in claripy/__init__.py, backends is reassigned by _backend_manager.BackendManager() and used to register other backend.

from . import backend_manager as _backend_manager
backends = _backend_manager.BackendManager()
backends._register_backend(_backends_module.BackendConcrete(), "concrete", True, True)
backends._register_backend(_backends_module.BackendVSA(), "vsa", False, False)

I know that it's for the flexibility to add backends by users themselves, but this name collision between backends:Module and backends:BackendManager really causes some problems in type infering. The language server typically mark it as module other than BackendManager. image

There is a simple fix without BackendManager:

  1. remove all BackendManager
  2. move class Backend from claripy/backends/__init__.py to claripy/backends/backend.py( avoid recursive import)
  3. In claripy/backends/__init__.py, use from .backend_z3 import BackendZ3 to import correct class
  4. In claripy/backends/__init__.py, use z3 = BackendZ3 , __all__ = ["z3"] to create alias

Alternatives

No response

Additional context

No response

zardus commented 1 year ago

I agree that it's over-engineered. Would you be willing to send a PR with this plan executed?

On Mon, May 15, 2023 at 9:02 AM syheliel @.***> wrote:

Description

claripy.backends is originally a submodule of claripy, but in claripy/init.py, backends is reassigned by _backend_manager.BackendManager() and used to register other backend.

from . import backend_manager as _backend_manager backends = _backend_manager.BackendManager() backends._register_backend(_backends_module.BackendConcrete(), "concrete", True, True) backends._register_backend(_backends_module.BackendVSA(), "vsa", False, False)

I know that it's for the flexibility to add backends by users themselves, but this name collision between backends:Module and backends:BackendManager really causes some problems in type infering. The language server typically mark it as module other than BackendManager. [image: image] https://urldefense.com/v3/__https://user-images.githubusercontent.com/45957390/238404102-31f2d87a-2915-44de-9207-3fe28cd310af.png__;!!IKRxdwAv5BmarQ!afXT7Vr6FF_RCH2fkgXFpPNaQlqYxePFIHVP4uu5f7b4NF5xvATa7zWmQ6oPJrkeyly8W7npwWbShQEf9BzR$

There is a simple fix without BackendManager:

  1. remove all BackendManager
  2. move class Backend from claripy/backends/init.py to claripy/backends/backend.py( avoid recursive import)
  3. In claripy/backends/init.py, use from .backend_z3 import BackendZ3 to import correct class
  4. In claripy/backends/init.py, use z3 = BackendZ3 , all = ["z3"] to create alias

Alternatives

No response Additional context

No response

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/angr/claripy/issues/353__;!!IKRxdwAv5BmarQ!afXT7Vr6FF_RCH2fkgXFpPNaQlqYxePFIHVP4uu5f7b4NF5xvATa7zWmQ6oPJrkeyly8W7npwWbShYH5cUPo$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AA2LHF62WWH37VEMRVNIRHTXGJHPNANCNFSM6AAAAAAYCM6JGU__;!!IKRxdwAv5BmarQ!afXT7Vr6FF_RCH2fkgXFpPNaQlqYxePFIHVP4uu5f7b4NF5xvATa7zWmQ6oPJrkeyly8W7npwWbShQ_pQqUo$ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

syheliel commented 1 year ago

I'm planning to add it. Since the modification overlaps with some part in #352 , so I will do this PR when #352 is merged.

twizmwazin commented 1 year ago

@syheliel I would advise you do it in a separate parallel PR instead of waiting for that one to be merged, as this is a much smaller change that can be reviewed and merged more quickly.

twizmwazin commented 2 months ago

Trying to tackle this now. I think BackendManager is somewhat necessary currently to support dynamically importing backends (not even just custom backends, this is the included smtlib backends). If #418 can be merged, then the backends list can just be a finite set and removing BackendManager should be straightforward.