From 39b0ceac8e553b2326be19c324cd94702bc893a3 Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Mon, 2 Sep 2024 16:05:00 -0700 Subject: [PATCH] Fold EvalStringToAstsMixin into Frontend (#463) * Fold EvalStringToAstsMixin into Frontend * Whoops * Clean it up a little * Fix length calculation * Better length calculation --- claripy/frontend.py | 10 +++++++++- claripy/frontend_mixins/__init__.py | 1 - .../frontend_mixins/eval_string_to_ast_mixin.py | 16 ---------------- claripy/solvers.py | 1 - 4 files changed, 9 insertions(+), 19 deletions(-) delete mode 100644 claripy/frontend_mixins/eval_string_to_ast_mixin.py diff --git a/claripy/frontend.py b/claripy/frontend.py index 8cc3fbb27..c3c287dd0 100644 --- a/claripy/frontend.py +++ b/claripy/frontend.py @@ -52,7 +52,15 @@ def eval_to_ast(self, e, n, extra_constraints=(), exact=None): :return: list of concrete ASTs """ - return [ast.bv.BVV(v, e.size()) for v in self.eval(e, n, extra_constraints=extra_constraints, exact=exact)] + values = self.eval(e, n, extra_constraints=extra_constraints, exact=exact) + + if isinstance(e, ast.BV): + return [ast.bv.BVV(v, e.size()) for v in values] + if isinstance(e, ast.String): + return [ast.strings.StringV(v, length=e.string_length) for v in values] + + # TODO: Implement support for other types + raise NotImplementedError def finalize(self): raise NotImplementedError("finalize() is not implemented") diff --git a/claripy/frontend_mixins/__init__.py b/claripy/frontend_mixins/__init__.py index 1b8573426..ae18e1d13 100644 --- a/claripy/frontend_mixins/__init__.py +++ b/claripy/frontend_mixins/__init__.py @@ -11,4 +11,3 @@ from .simplify_skipper_mixin import SimplifySkipperMixin from .composited_cache_mixin import CompositedCacheMixin from .sat_cache_mixin import SatCacheMixin -from .eval_string_to_ast_mixin import EvalStringsToASTsMixin diff --git a/claripy/frontend_mixins/eval_string_to_ast_mixin.py b/claripy/frontend_mixins/eval_string_to_ast_mixin.py deleted file mode 100644 index afac137f7..000000000 --- a/claripy/frontend_mixins/eval_string_to_ast_mixin.py +++ /dev/null @@ -1,16 +0,0 @@ -from __future__ import annotations - -from claripy import String, StringV - - -class EvalStringsToASTsMixin: - def eval_to_ast(self, e, n, extra_constraints=(), exact=None): - if type(e) is String: - return [ - StringV( - v, - ) - for v in self.eval(e, n, extra_constraints=extra_constraints, exact=exact) - ] - - return super().eval_to_ast(e, n, extra_constraints=extra_constraints, exact=None) diff --git a/claripy/solvers.py b/claripy/solvers.py index 79b596b96..7bcd27f9a 100644 --- a/claripy/solvers.py +++ b/claripy/solvers.py @@ -109,7 +109,6 @@ class SolverStrings( frontend_mixins.ConstraintFilterMixin, frontend_mixins.ConstraintDeduplicatorMixin, frontend_mixins.EagerResolutionMixin, - frontend_mixins.EvalStringsToASTsMixin, frontends.FullFrontend, ): """SolverStrings is a frontend that uses Z3 to solve string constraints."""