one + weird_nine
, though. It is a type error to perform an operation on bitvectors of differing lengths. You can, however, extend weird_nine
so it has an appropriate number of bits:zero_extend
will pad the bitvector on the left with the given number of zero bits. You can also use sign_extend
to pad with a duplicate of the highest bit, preserving the value of the bitvector under two's compliment signed integer semantics.x
and y
are now symbolic variables, which are kind of like the variables you learned to work with in 7th grade algebra. Notice that the name you provided has been been mangled by appending an incrementing counter and You can do as much arithmetic as you want with them, but you won't get a number back, you'll get an AST instead.x
and y
and even one
are also ASTs - any bitvector is a tree of operations, even if that tree is only one layer deep. To understand this, let's learn how to process ASTs..op
and a .args
. The op is a string naming the operation being performed, and the args are the values the operation takes as input. Unless the op is BVV
or BVS
(or a few others...), the args are all other ASTs, the tree eventually terminating with BVVs or BVSs.<BV64 0xfffffffffffffffb>
, which is definitely not less than one hundred. If you want the comparison to be signed, you can say one_hundred.SGT(-5)
(that's "signed greater-than"). A full list of operations can be found at the end of this chapter.if one > one_hundred
will raise an exception. Instead, you should use solver.is_true
and solver.is_false
, which test for concrete truthyness/falsiness without performing a constraint solve.state.solver.eval(y)
, you'll get a value of y which is consistent with the value of x that you got. If you don't add any constraints between two queries, the results will be consistent with each other.state.satisfiable()
.eval
is a general purpose method to convert any bitvector into a Python primitive while respecting the integrity of the state. This is why we use eval
to convert from concrete bitvectors to Python ints, too!FPV
and FPS
.solver.fpAdd
for example) with a rounding mode (one of solver.fp.RM_*
) as the first argument.eval
returning a floating point number:raw_to_bv
and raw_to_fp
:val_to_fp
and val_to_bv
. These methods must take the size or sort of the target value as a parameter, due to the floating-point nature of floats.signed
parameter, designating the signedness of the source or target bitvector.eval
will give you one possible solution to an expression, but what if you want several? What if you want to ensure that the solution is unique? The solver provides you with several methods for common solving patterns:solver.eval(expression)
will give you one possible solution to the given expression.solver.eval_one(expression)
will give you the solution to the given expression, or throw an error if more than one solution is possible.solver.eval_upto(expression, n)
will give you up to n solutions to the given expression, returning fewer than n if fewer than n are possible.solver.eval_atleast(expression, n)
will give you n solutions to the given expression, throwing an error if fewer than n are possible.solver.eval_exact(expression, n)
will give you n solutions to the given expression, throwing an error if fewer or more than are possible.solver.min(expression)
will give you the minimum possible solution to the given expression.solver.max(expression)
will give you the maximum possible solution to the given expression.extra_constraints
can be passed as a tuple of constraints. These constraints will be taken into account for this evaluation, but will not be added to the state.cast_to
can be passed a data type to cast the result to. Currently, this can only be int
and bytes
, which will cause the method to return the corresponding representation of the underlying data. For example, state.solver.eval(state.solver.BVV(0x41424344, 32), cast_to=bytes)
will return b'ABCD'
.