Secure your code as it's written. Use Snyk Code to scan source code in minutes - no build needed - and fix issues immediately.
def test_send_back_negative_signed(self):
self.state.calls.append(self.get_call(self.env.calldata.read(0, 32)))
self.state.solver.add(claripy.SLT(self.env.calldata.read(0, 32), 0))
self.assertFalse(self.check_state(self.state))
state.stack_pop(),
state.stack_pop(),
) # pylint:disable=invalid-name
state.stack_push(bool_to_bv(claripy.ULT(s0, s1)))
elif op == opcode_values.GT:
s0, s1 = (
state.stack_pop(),
state.stack_pop(),
) # pylint:disable=invalid-name
state.stack_push(bool_to_bv(claripy.UGT(s0, s1)))
elif op == opcode_values.SLT:
s0, s1 = (
state.stack_pop(),
state.stack_pop(),
) # pylint:disable=invalid-name
state.stack_push(bool_to_bv(claripy.SLT(s0, s1)))
elif op == opcode_values.SGT:
s0, s1 = (
state.stack_pop(),
state.stack_pop(),
) # pylint:disable=invalid-name
state.stack_push(bool_to_bv(claripy.SGT(s0, s1)))
elif op == opcode_values.SIGNEXTEND:
# TODO: Use Claripy's SignExt that should do exactly that.
s0, s1 = (
state.stack_pop(),
state.stack_pop(),
) # pylint:disable=invalid-name
# s0 is the number of bits. s1 the number we want to extend.
s0 = solution(s0)
if s0 <= 31:
sign_bit = 1 << (s0 * 8 + 7)
align = self.offsets[addr][2]
if align != 1:
solver.add(var.sym_addr % align == 0)
var.sym_link(solver, stack) # this hooks up the constrains to actual immediates
# also the top/bottom fixing happens in there
if i != 0:
prev_var = stack.variables[stack.addr_list[i-1]]
self.mark_boundaries(prev_var, var)
if i != len(stack.addr_list) - 1:
next_var = stack.variables[stack.addr_list[i+1]]
self.mark_boundaries(var, next_var)
# ew. ew ew ew ew ew ew!!!
diff = next_var.conc_addr - var.conc_addr
solver.add(claripy.SLT(var.sym_addr, var.sym_addr + diff))
if i == 0:
solver.add(claripy.SLE(-stack.sym_size, var.sym_addr))
i += 1
def amd64g_calculate_RCL(state, arg, rot_amt, eflags_in, sz):
if sz.op != 'BVV':
raise SimError('Hit a symbolic "sz" in an x86 rotate with carry instruction. Panic.')
want_flags = claripy.SLT(sz, 0).is_true()
if want_flags: sz = -sz
carry_bit_in = eflags_in[data['AMD64']['CondBitOffsets']['G_CC_SHIFT_C']]
carry_bit_out, overflow_bit_out, arg_out = generic_rotate_with_carry(state, True, arg, rot_amt, carry_bit_in, sz)
if want_flags:
cf = carry_bit_out.zero_extend(63)
of = overflow_bit_out.zero_extend(63)
eflags_out = eflags_in
eflags_out &= ~(data['AMD64']['CondBitMasks']['G_CC_MASK_C'] | data['AMD64']['CondBitMasks']['G_CC_MASK_O'])
eflags_out |= (cf << data['AMD64']['CondBitOffsets']['G_CC_SHIFT_C']) | \
(of << data['AMD64']['CondBitOffsets']['G_CC_SHIFT_O'])
return eflags_out
else:
return arg_out
def _op_generic_StoU_saturation(self, value, min_value, max_value): #pylint:disable=no-self-use
"""
Return unsigned saturated BV from signed BV.
Min and max value should be unsigned.
"""
return claripy.If(
claripy.SGT(value, max_value),
max_value,
claripy.If(claripy.SLT(value, min_value), min_value, value))
def pc_actions_cond_CondL(state, cc_expr):
return _cond_flag(state, claripy.SLT(cc_expr, 0))
sdata, _ = simfd.read_data(1, short_reads=False)
self.state.memory.store(args(argnum), sdata)
argnum += 1
else:
bits = component.size * 8
if component.spec_type == b'x':
base = 16
elif component.spec_type == b'o':
base = 8
else:
base = 10
# here's the variable representing the result of the parsing
target_variable = self.state.solver.BVS('scanf_' + component.string.decode(), bits,
key=('api', 'scanf', argnum - startpos, component.string))
negative = claripy.SLT(target_variable, 0)
# how many digits does it take to represent this variable fully?
max_digits = int(math.ceil(math.log(2**bits, base)))
# how many digits does the format specify?
spec_digits = component.length_spec
# how many bits can we specify as input?
available_bits = float('inf') if spec_digits is None else spec_digits * math.log(base, 2)
not_enough_bits = available_bits < bits
# how many digits will we model this input as?
digits = max_digits if spec_digits is None else spec_digits
# constrain target variable range explicitly if it can't take on all possible values
if not_enough_bits:
def amd64g_calculate_RCR(state, arg, rot_amt, eflags_in, sz):
if sz.op != 'BVV':
raise SimError('Hit a symbolic "sz" in an x86 rotate with carry instruction. Panic.')
want_flags = claripy.SLT(sz, 0).is_true()
if want_flags: sz = -sz
carry_bit_in = eflags_in[data['AMD64']['CondBitOffsets']['G_CC_SHIFT_C']]
carry_bit_out, overflow_bit_out, arg_out = generic_rotate_with_carry(state, False, arg, rot_amt, carry_bit_in, sz)
if want_flags:
cf = carry_bit_out.zero_extend(63)
of = overflow_bit_out.zero_extend(63)
eflags_out = eflags_in
eflags_out &= ~(data['AMD64']['CondBitMasks']['G_CC_MASK_C'] | data['AMD64']['CondBitMasks']['G_CC_MASK_O'])
eflags_out |= (cf << data['AMD64']['CondBitOffsets']['G_CC_SHIFT_C']) | \
(of << data['AMD64']['CondBitOffsets']['G_CC_SHIFT_O'])
return eflags_out
else:
return arg_out