You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The following is quoted from @zardus in the Slack channel. We should put them in the documentation.
generally speaking:
claripy abstracts expressions using claripy.AST objects
Frontends provide different paradigms for handling those expressions. The FullFrontend (should really be named SolverFrontend or something) handles them using something like an SMT solver, LightFrontend (should really be named ApproximationFrontend or something) handles them by using an abstract (and approximating) data domain.
each Frontend needs to, at some point, do actual operation and evaluations on the AST. ASTs don't support this on their own. Instead, Backends translate ASTs into BackendObjects (i.e., python primitives, Z3 expressions, strided intervals for VSA, etc) and also handle the appropriate state-tracking objects (such as Z3 solvers)
Frontends take ASTs as inputs and use Backends to backend.convert() those ASTs into BackendObjects that can be evaluated and otherwise reasoned about
FrontendMixins customize the operation of Frontends. For example, ModelCacheMixin caches solutions from an SMT solver
The text was updated successfully, but these errors were encountered:
The following is quoted from @zardus in the Slack channel. We should put them in the documentation.
generally speaking:
claripy.AST
objectsFrontend
s provide different paradigms for handling those expressions. TheFullFrontend
(should really be namedSolverFrontend
or something) handles them using something like an SMT solver,LightFrontend
(should really be namedApproximationFrontend
or something) handles them by using an abstract (and approximating) data domain.Frontend
needs to, at some point, do actual operation and evaluations on theAST
.AST
s don't support this on their own. Instead,Backend
s translateAST
s intoBackendObject
s (i.e., python primitives, Z3 expressions, strided intervals for VSA, etc) and also handle the appropriate state-tracking objects (such as Z3 solvers)Frontend
s takeAST
s as inputs and useBackend
s tobackend.convert()
thoseAST
s intoBackendObjects
that can be evaluated and otherwise reasoned aboutFrontendMixin
s customize the operation ofFrontend
s. For example,ModelCacheMixin
caches solutions from an SMT solverThe text was updated successfully, but these errors were encountered: