Frontend
s provide different paradigms for evaluating these expressions. For example, the FullFrontend
solves expressions using something like an SMT solver backend, while LightFrontend
handles them by using an abstract (and approximating) data domain backend.Frontend
needs to, at some point, do actual operation and evaluations on an AST. ASTs don't support this on their own. Instead, Backend
s 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.FrontendMixin
s customize the operation of Frontend
s. For example, ModelCacheMixin
caches solutions from an SMT solver.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.BVS('x', 32)
0xc001b3475
: claripy.BVV(0xc001b3a75, 32)
claripy.SI(name='x', bits=32, lower_bound=1000, upper_bound=2000, stride=10)
claripy.fp.FSORT_DOUBLE
symbolic floating point "b": claripy.FPS('b', claripy.fp.FSORT_DOUBLE)
claripy.fp.FSORT_FLOAT
floating point with value 3.2
: claripy.FPV(3.2, claripy.fp.FSORT_FLOAT)
claripy.BoolV(True)
, or claripy.true
or claripy.false
, or by comparing two ASTs (i.e., claripy.BVS('x', 32) < claripy.BVS('y', 32)
claripy.LShR(x, 10)
claripy.SignExt(32, x)
or x.sign_extend(32)
claripy.ZeroExt(32, x)
or x.zero_extend(32)
claripy.Extract(7, 0, x)
or x[7:0]
claripy.Concat(x, y, z)
claripy.RotateLeft(x, 8)
claripy.RotateRight(x, 8)
claripy.Reverse(x)
or x.reversed
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)
claripy.ULE(x, y)
claripy.ULT(x, y)
claripy.UGE(x, y)
claripy.UGT(x, y)
claripy.SLE(x, y)
claripy.SLT(x, y)
claripy.SGE(x, y)
claripy.SGT(x, y)
>
, <
, >=
, and <=
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()
or _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 Backend
abstract class that currently raise NotImplementedError()
.convert()
and _convert()
, as Claripy can try to stuff anything it feels like into _convert() to see if the backend can handle that type of object.BackendObject
is 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.