Frontends provide different paradigms for evaluating these expressions. For example, the
FullFrontendsolves expressions using something like an SMT solver backend, while
LightFrontendhandles them by using an abstract (and approximating) data domain backend.
Frontendneeds to, at some point, do actual operation and evaluations on an AST. ASTs don't support this on their own. Instead,
Backends translate ASTs into backend objects (i.e., Python primitives for
BackendConcrete, Z3 expressions for
BackendZ3, strided intervals for
BackendVSA, etc) and handle any appropriate state-tracking objects (such as tracking the solver state in the case of
BackendZ3). Roughly speaking, frontends take ASTs as inputs and use backends to
backend.convert()those ASTs into backend objects that can be evaluated and otherwise reasoned about.
FrontendMixins customize the operation of
Frontends. For example,
ModelCacheMixincaches solutions from an SMT solver.
(a + b) / c)on any type of underlying data. Claripy handles the application of these operations on the underlying objects themselves by dispatching requests to the backends.
claripy.SI(name='x', bits=32, lower_bound=1000, upper_bound=2000, stride=10)
claripy.fp.FSORT_DOUBLEsymbolic floating point "b":
claripy.fp.FSORT_FLOATfloating point with value
claripy.false, or by comparing two ASTs (i.e.,
claripy.BVS('x', 32) < claripy.BVS('y', 32)
claripy.Extract(7, 0, x)or
claripy.Concat(x, y, z)
claripy.And(x == y, x > 0)
claripy.Or(x == y, y < 10)
claripy.Not(x == y)is the same as
x != y
claripy.If(x > y, x, y)
<=are unsigned in Claripy. This is different than their behavior in Z3, because it seems more natural in binary analysis.
z3.Solver(). It is a solver that tracks constraints on symbolic variables and uses a constraint solver (currently, Z3) to evaluate symbolic expressions.
convert()function. This function receives a claripy AST and should return an object that the backend can handle in its private methods. Backends should also implement a
_convert()method, which will receive anything that is not a claripy AST object (i.e., an integer or an object from a different backend). If
_convert()receives something that the backend can't translate to a format that is usable internally, the backend should raise BackendError, and thus won't be used for that object. All backends must also implement any functions of the base
Backendabstract class that currently raise
_convert(), as Claripy can try to stuff anything it feels like into _convert() to see if the backend can handle that type of object.
BackendObjectis a result of the operation represented by the AST. Claripy expects these objects to be returned from their respective backends, and will pass such objects into that backend's other functions.