one + weird_nine, though. It is a type error to perform an operation on bitvectors of differing lengths. You can, however, extend
weird_nineso it has an appropriate number of bits:
zero_extendwill pad the bitvector on the left with the given number of zero bits. You can also use
sign_extendto pad with a duplicate of the highest bit, preserving the value of the bitvector under two's compliment signed integer semantics.
yare 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.
oneare 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.
.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
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_hundredwill raise an exception. Instead, you should use
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.
evalis a general purpose method to convert any bitvector into a python primitive while respecting the integrity of the state. This is why we use
evalto convert from concrete bitvectors to python ints, too!
solver.fpAddfor example) with a rounding mode (one of
solver.fp.RM_*) as the first argument.
evalreturning a floating point number:
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.
signedparameter, designating the signedness of the source or target bitvector.
evalwill 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_constraintscan be passed as a tuple of constraints.
cast_tocan be passed a data type to cast the result to.
bytes, which will cause the method to return the corresponding representation of the underlying data.
state.solver.eval(state.solver.BVV(0x41424344, 32), cast_to=bytes)will return