def test_memset():
    l.info("concrete src, concrete dst, concrete len")
    s = SimState(arch="PPC32", mode="symbolic")
    dst = s.se.BitVecVal(0, 128)
    dst_addr = s.se.BitVecVal(0x1000, 32)
    char = s.se.BitVecVal(0x00000041, 32)
    char2 = s.se.BitVecVal(0x50505050, 32)
    length = s.BV("some_length", 32)

    s.memory.store(dst_addr, dst)
    memset(s, inline=True, arguments=[dst_addr, char, s.se.BitVecVal(3, 32)])
    nose.tools.assert_equals(s.se.any_int(s.memory.load(dst_addr, 4)), 0x41414100)

    l.debug("Symbolic length")
    s = SimState(arch="PPC32", mode="symbolic")
    s.memory.store(dst_addr, dst)
    length = s.BV("some_length", 32)
    memset(s, inline=True, arguments=[dst_addr, char2, length])

    l.debug("Trying 2")
    s_two = s.copy()
    s_two.add_constraints(length == 2)
    nose.tools.assert_equals(s_two.se.any_int(s_two.memory.load(dst_addr, 4)), 0x50500000)

    l.debug("Trying 0")
    s_zero = s.copy()
    s_zero.add_constraints(length == 0)
    nose.tools.assert_equals(s_zero.se.any_int(s_zero.memory.load(dst_addr, 4)), 0x00000000)

    l.debug("Trying 5")
    s_five = s.copy()
    s_five.add_constraints(length == 5)
    nose.tools.assert_equals(s_five.se.any_int(s_five.memory.load(dst_addr, 6)), 0x505050505000)

def test_inline_strlen():
    s = SimState(arch="AMD64", mode="symbolic")

    l.info("fully concrete string")
    a_str = s.se.BitVecVal(0x41414100, 32)
    a_addr = s.se.BitVecVal(0x10, 64)
    s.memory.store(a_addr, a_str, endness="Iend_BE")
    a_len = SimProcedures["libc.so.6"]["strlen"](s, inline=True, arguments=[a_addr]).ret_expr
    nose.tools.assert_true(s.se.unique(a_len))
    nose.tools.assert_equal(s.se.any_int(a_len), 3)

    l.info("concrete-terminated string")
    b_str = s.se.Concat(s.BV("mystring", 24), s.se.BitVecVal(0, 8))
    b_addr = s.se.BitVecVal(0x20, 64)
    s.memory.store(b_addr, b_str, endness="Iend_BE")
    b_len = SimProcedures["libc.so.6"]["strlen"](s, inline=True, arguments=[b_addr]).ret_expr
    nose.tools.assert_equal(s.se.max_int(b_len), 3)
    nose.tools.assert_items_equal(s.se.any_n_int(b_len, 10), (0, 1, 2, 3))

    l.info("fully unconstrained")
    u_addr = s.se.BitVecVal(0x50, 64)
    u_len_sp = SimProcedures["libc.so.6"]["strlen"](s, inline=True, arguments=[u_addr])
    u_len = u_len_sp.ret_expr
    nose.tools.assert_equal(len(s.se.any_n_int(u_len, 100)), s.libc.buf_symbolic_bytes)
    nose.tools.assert_equal(s.se.max_int(u_len), s.libc.buf_symbolic_bytes - 1)

    # print u_len_sp.se.maximum_null

    # s.add_constraints(u_len < 16)

    nose.tools.assert_equal(s.se.any_n_int(s.memory.load(0x50 + u_len, 1), 300), [0])

    #
    # This tests if a strlen can influence a symbolic str.
    #
    l.info("Trying to influence length.")
    s = SimState(arch="AMD64", mode="symbolic")
    str_c = s.BV("some_string", 8 * 16)
    c_addr = s.se.BitVecVal(0x10, 64)
    s.memory.store(c_addr, str_c, endness="Iend_BE")
    c_len = SimProcedures["libc.so.6"]["strlen"](s, inline=True, arguments=[c_addr]).ret_expr
    nose.tools.assert_equal(len(s.se.any_n_int(c_len, 100)), s.libc.buf_symbolic_bytes)
    nose.tools.assert_equal(s.se.max_int(c_len), s.libc.buf_symbolic_bytes - 1)

    one_s = s.copy()
    one_s.add_constraints(c_len == 1)
    nose.tools.assert_equal(one_s.se.any_str(str_c).index("\x00"), 1)
    str_test = one_s.memory.load(c_addr, 2, endness="Iend_BE")
    nose.tools.assert_equal(len(one_s.se.any_n_str(str_test, 300)), 255)

    for i in range(16):
        test_s = s.copy()
        test_s.add_constraints(c_len == i)
        str_test = test_s.memory.load(c_addr, i + 1, endness="Iend_BE")
        nose.tools.assert_equal(test_s.se.any_str(str_test).index("\x00"), i)
        for j in range(i):
            nose.tools.assert_false(test_s.se.unique(test_s.memory.load(c_addr + j, 1)))

def test_unsat_core():

    s = SimState(arch='AMD64', mode='symbolic', add_options={ simuvex.options.CONSTRAINT_TRACKING_IN_SOLVER })
    x = s.se.BVS('x', 32)
    s.add_constraints(s.se.BVV(0, 32) == x)
    s.add_constraints(s.se.BVV(1, 32) == x)

    nose.tools.assert_false(s.satisfiable())
    unsat_core = s.se.unsat_core()
    nose.tools.assert_equal(len(unsat_core), 2)

def test_state_merge_static():
    # With abstract memory
    # Aligned memory merging
    a = SimState(mode='static')
    se = a.se

    addr = a.se.ValueSet(region='global', bits=32, val=8)
    a.memory.store(addr, a.se.BitVecVal(42, 32))

    b = a.copy()
    c = a.copy()
    a.memory.store(addr, a.se.BitVecVal(50, 32), endness='Iend_LE')
    b.memory.store(addr, a.se.BitVecVal(60, 32), endness='Iend_LE')
    c.memory.store(addr, a.se.BitVecVal(70, 32), endness='Iend_LE')

    merged, _, _ = a.merge(b, c)
    nose.tools.assert_true(merged.memory.load(addr, 4).identical(a.se.SI(bits=32, stride=10, lower_bound=50, upper_bound=70)))

def test_concretization_strategies():
    initial_memory = {0: 'A', 1: 'B', 2: 'C', 3: 'D'}

    s = SimState(memory_backer=initial_memory)

    # sanity check
    nose.tools.assert_equal(s.se.any_n_str(s.memory.load(3, 1), 2), ['D'])

    x = s.se.BVS('x', s.arch.bits)
    s.add_constraints(x >= 1)

    ss = s.copy()
    nose.tools.assert_equal(ss.se.any_n_str(ss.memory.load(x, 1), 2), ['B'])

    ss = s.copy()
    ss.options.add(simuvex.o.CONSERVATIVE_READ_STRATEGY)
    nose.tools.assert_true('symbolic' in next(iter(ss.memory.load(x, 1).variables)))

def test_strchr():
    l.info("concrete haystack and needle")
    s = SimState(arch="AMD64", mode="symbolic")
    str_haystack = s.se.BitVecVal(0x41424300, 32)
    str_needle = s.se.BitVecVal(0x42, 64)
    addr_haystack = s.se.BitVecVal(0x10, 64)
    s.memory.store(addr_haystack, str_haystack, endness="Iend_BE")

    ss_res = strchr(s, inline=True, arguments=[addr_haystack, str_needle]).ret_expr
    nose.tools.assert_true(s.se.unique(ss_res))
    nose.tools.assert_equal(s.se.any_int(ss_res), 0x11)

    l.info("concrete haystack, symbolic needle")
    s = SimState(arch="AMD64", mode="symbolic")
    str_haystack = s.se.BitVecVal(0x41424300, 32)
    str_needle = s.BV("wtf", 64)
    chr_needle = str_needle[7:0]
    addr_haystack = s.se.BitVecVal(0x10, 64)
    s.memory.store(addr_haystack, str_haystack, endness="Iend_BE")

    ss_res = strchr(s, inline=True, arguments=[addr_haystack, str_needle]).ret_expr
    nose.tools.assert_false(s.se.unique(ss_res))
    nose.tools.assert_equal(len(s.se.any_n_int(ss_res, 10)), 4)

    s_match = s.copy()
    s_nomatch = s.copy()
    s_match.add_constraints(ss_res != 0)
    s_nomatch.add_constraints(ss_res == 0)

    nose.tools.assert_true(s_match.satisfiable())
    nose.tools.assert_true(s_nomatch.satisfiable())
    nose.tools.assert_equal(len(s_match.se.any_n_int(chr_needle, 300)), 3)
    nose.tools.assert_equal(len(s_nomatch.se.any_n_int(chr_needle, 300)), 253)
    nose.tools.assert_items_equal(s_match.se.any_n_int(ss_res, 300), [0x10, 0x11, 0x12])
    nose.tools.assert_items_equal(s_match.se.any_n_int(chr_needle, 300), [0x41, 0x42, 0x43])

    s_match.memory.store(ss_res, s_match.BVV(0x44, 8))
    nose.tools.assert_items_equal(s_match.se.any_n_int(s_match.memory.load(0x10, 1), 300), [0x41, 0x44])
    nose.tools.assert_items_equal(s_match.se.any_n_int(s_match.memory.load(0x11, 1), 300), [0x42, 0x44])
    nose.tools.assert_items_equal(s_match.se.any_n_int(s_match.memory.load(0x12, 1), 300), [0x43, 0x44])

    return

def test_state_merge_static():
    # With abstract memory
    # Aligned memory merging
    a = SimState(mode='static')

    addr = a.se.ValueSet(region='global', bits=32, val=8)
    a.memory.store(addr, a.se.BVV(42, 32))
    # Clear a_locs, so further writes will not try to merge with value 42
    a.memory.regions['global']._alocs = { }

    b = a.copy()
    c = a.copy()
    a.memory.store(addr, a.se.BVV(50, 32), endness='Iend_LE')
    b.memory.store(addr, a.se.BVV(60, 32), endness='Iend_LE')
    c.memory.store(addr, a.se.BVV(70, 32), endness='Iend_LE')

    merged, _, _ = a.merge(b, c)
    actual = claripy.backends.vsa.convert(merged.memory.load(addr, 4))
    expected = claripy.backends.vsa.convert(a.se.SI(bits=32, stride=10, lower_bound=50, upper_bound=70))
    nose.tools.assert_true(actual.identical(expected))

def test_state_merge_static():
    # With abstract memory
    # Aligned memory merging
    a = SimState(mode="static")
    se = a.se

    addr = a.se.ValueSet(region="global", bits=32, val=8)
    a.memory.store(addr, a.se.BitVecVal(42, 32))
    # Clear a_locs, so further writes will not try to merge with value 42
    a.memory.regions["global"]._alocs = {}

    b = a.copy()
    c = a.copy()
    a.memory.store(addr, a.se.BitVecVal(50, 32), endness="Iend_LE")
    b.memory.store(addr, a.se.BitVecVal(60, 32), endness="Iend_LE")
    c.memory.store(addr, a.se.BitVecVal(70, 32), endness="Iend_LE")

    merged, _, _ = a.merge(b, c)
    nose.tools.assert_true(
        merged.memory.load(addr, 4).identical(a.se.SI(bits=32, stride=10, lower_bound=50, upper_bound=70))
    )

def test_strcpy():
    l.info("concrete src, concrete dst")

    l.debug("... full copy")
    s = SimState(arch="AMD64", mode="symbolic")
    dst = s.se.BitVecVal(0x41414100, 32)
    dst_addr = s.se.BitVecVal(0x1000, 64)
    src = s.se.BitVecVal(0x42420000, 32)
    src_addr = s.se.BitVecVal(0x2000, 64)
    s.memory.store(dst_addr, dst)
    s.memory.store(src_addr, src)
    strcpy(s, inline=True, arguments=[dst_addr, src_addr])
    new_dst = s.memory.load(dst_addr, 4, endness="Iend_BE")
    nose.tools.assert_equal(s.se.any_str(new_dst), "BB\x00\x00")

    l.info("symbolic src, concrete dst")
    dst = s.se.BitVecVal(0x41414100, 32)
    dst_addr = s.se.BitVecVal(0x1000, 64)
    src = s.BV("src", 32)
    src_addr = s.se.BitVecVal(0x2000, 64)

    s = SimState(arch="AMD64", mode="symbolic")
    s.memory.store(dst_addr, dst)
    s.memory.store(src_addr, src)

    ln = strlen(s, inline=True, arguments=[src_addr]).ret_expr

    strcpy(s, inline=True, arguments=[dst_addr, src_addr])

    cm = strcmp(s, inline=True, arguments=[dst_addr, src_addr]).ret_expr

    s.add_constraints(cm == 0)

    s.add_constraints(ln == 15)

def broken_sprintf():
    l.info("concrete src, concrete dst, concrete len")
    s = SimState(mode="symbolic", arch="PPC32")
    format_str = s.se.BitVecVal(0x25640000, 32)
    format_addr = s.se.BitVecVal(0x2000, 32)
    # dst = s.se.BitVecVal("destination", 128)
    dst_addr = s.se.BitVecVal(0x1000, 32)
    arg = s.BV("some_number", 32)

    s.memory.store(format_addr, format_str)

    sprintf(s, inline=True, arguments=[dst_addr, format_addr, arg])

    for i in range(9):
        j = random.randint(10 ** i, 10 ** (i + 1))
        s2 = s.copy()
        s2.add_constraints(arg == j)
        # print s2.se.any_n_str(s2.memory.load(dst_addr, i+2), 2), repr("%d\x00" % j)
        nose.tools.assert_equal(s2.se.any_n_str(s2.memory.load(dst_addr, i + 2), 2), ["%d\x00" % j])

    s2 = s.copy()
    s2.add_constraints(arg == 0)
    # print s2.se.any_n_str(s2.memory.load(dst_addr, 2), 2), repr("%d\x00" % 0)
    nose.tools.assert_equal(s2.se.any_n_str(s2.memory.load(dst_addr, 2), 2), ["%d\x00" % 0])

def test_copy():
    s = SimState()
    s.memory.store(0x100, "ABCDEFGHIJKLMNOP")
    s.memory.store(0x200, "XXXXXXXXXXXXXXXX")
    x = s.se.BV('size', s.arch.bits)
    s.add_constraints(s.se.ULT(x, 10))
    s.memory.copy_contents(0x200, 0x100, x)

    nose.tools.assert_equals(sorted(s.se.any_n_int(x, 100)), range(10))
    result = s.memory.load(0x200, 5)
    nose.tools.assert_equals(sorted(s.se.any_n_str(result, 100)), [ "ABCDE", "ABCDX", "ABCXX", "ABXXX", "AXXXX", "XXXXX" ])
    nose.tools.assert_equals(sorted(s.se.any_n_str(result, 100, extra_constraints=[x==3])), [ "ABCXX" ])

    s = SimState()
    s.posix.write(0, "ABCDEFGHIJKLMNOP", len("ABCDEFGHIJKLMNOP"))
    s.posix.seek(0, 0)
    s.memory.store(0x200, "XXXXXXXXXXXXXXXX")
    x = s.se.BV('size', s.arch.bits)
    s.add_constraints(s.se.ULT(x, 10))

    s.posix.read(0, x, dst_addr=0x200)
    nose.tools.assert_equals(sorted(s.se.any_n_int(x, 100)), range(10))
    result = s.memory.load(0x200, 5)
    nose.tools.assert_equals(sorted(s.se.any_n_str(result, 100)), [ "ABCDE", "ABCDX", "ABCXX", "ABXXX", "AXXXX", "XXXXX" ])
    nose.tools.assert_equals(sorted(s.se.any_n_str(result, 100, extra_constraints=[x==3])), [ "ABCXX" ])

    s = SimState()
    s.posix.write(0, "ABCDEFGHIJKLMNOP", len("ABCDEFGHIJKLMNOP"))
    s.posix.seek(0, 0)
    s.memory.store(0x200, "XXXXXXXXXXXXXXXX")
    x = s.se.BV('size', s.arch.bits)
    s.add_constraints(s.se.ULT(x, 10))

    ret_x = SimProcedures['libc.so.6']['read'](s, inline=True, arguments=[0, 0x200, x]).ret_expr
    nose.tools.assert_equals(sorted(s.se.any_n_int(x, 100)), range(10))
    result = s.memory.load(0x200, 5)
    nose.tools.assert_equals(sorted(s.se.any_n_str(result, 100)), [ "ABCDE", "ABCDX", "ABCXX", "ABXXX", "AXXXX", "XXXXX" ])
    nose.tools.assert_equals(sorted(s.se.any_n_str(result, 100, extra_constraints=[x==3])), [ "ABCXX" ])

    nose.tools.assert_equals(sorted(s.se.any_n_int(ret_x, 100)), range(10))
    nose.tools.assert_equals(sorted(s.se.any_n_str(result, 100, extra_constraints=[ret_x==3])), [ "ABCXX" ])

def test_strstr_inconsistency(n=2):
    l.info("symbolic haystack, symbolic needle")
    s = SimState(arch="AMD64", mode="symbolic")
    s.libc.buf_symbolic_bytes = n
    addr_haystack = s.se.BitVecVal(0x10, 64)
    addr_needle = s.se.BitVecVal(0xB0, 64)
    # len_needle = strlen(s, inline=True, arguments=[addr_needle])

    ss_res = strstr(s, inline=True, arguments=[addr_haystack, addr_needle]).ret_expr

    # slh_res = strlen(s, inline=True, arguments=[addr_haystack]).ret_expr
    # sln_res = strlen(s, inline=True, arguments=[addr_needle]).ret_expr
    # print "LENH:", s.se.any_n_int(slh_res, 100)
    # print "LENN:", s.se.any_n_int(sln_res, 100)

    nose.tools.assert_false(s.se.unique(ss_res))
    nose.tools.assert_items_equal(s.se.any_n_int(ss_res, 100), [0] + range(0x10, 0x10 + s.libc.buf_symbolic_bytes - 1))

    s.add_constraints(ss_res != 0)
    ss2 = strstr(s, inline=True, arguments=[addr_haystack, addr_needle]).ret_expr
    s.add_constraints(ss2 == 0)
    nose.tools.assert_false(s.satisfiable())

def test_memcpy():
    l.info("concrete src, concrete dst, concrete len")
    l.debug("... full copy")
    s = SimState(arch="AMD64", mode="symbolic")
    dst = s.se.BitVecVal(0x41414141, 32)
    dst_addr = s.se.BitVecVal(0x1000, 64)
    src = s.se.BitVecVal(0x42424242, 32)
    src_addr = s.se.BitVecVal(0x2000, 64)

    s.memory.store(dst_addr, dst)
    s.memory.store(src_addr, src)
    memcpy(s, inline=True, arguments=[dst_addr, src_addr, s.se.BitVecVal(4, 64)])
    new_dst = s.memory.load(dst_addr, 4, endness="Iend_BE")
    nose.tools.assert_equal(s.se.any_n_str(new_dst, 2), ["BBBB"])

    l.debug("... partial copy")
    s = SimState(arch="AMD64", mode="symbolic")
    s.memory.store(dst_addr, dst)
    s.memory.store(src_addr, src)
    memcpy(s, inline=True, arguments=[dst_addr, src_addr, s.se.BitVecVal(2, 64)])
    new_dst = s.memory.load(dst_addr, 4, endness="Iend_BE")
    nose.tools.assert_equal(s.se.any_n_str(new_dst, 2), ["BBAA"])

    l.info("symbolic src, concrete dst, concrete len")
    s = SimState(arch="AMD64", mode="symbolic")
    dst = s.se.BitVecVal(0x41414141, 32)
    dst_addr = s.se.BitVecVal(0x1000, 64)
    src = s.BV("src", 32)
    src_addr = s.se.BitVecVal(0x2000, 64)

    s.memory.store(dst_addr, dst)
    s.memory.store(src_addr, src)

    # make sure it copies it all
    memcpy(s, inline=True, arguments=[dst_addr, src_addr, s.se.BitVecVal(4, 64)])
    nose.tools.assert_true(s.satisfiable())
    s.add_constraints(src != s.memory.load(dst_addr, 4))
    nose.tools.assert_false(s.satisfiable())

    l.info("symbolic src, concrete dst, symbolic len")
    s = SimState(arch="AMD64", mode="symbolic")
    dst = s.se.BitVecVal(0x41414141, 32)
    dst_addr = s.se.BitVecVal(0x1000, 64)
    src = s.BV("src", 32)
    src_addr = s.se.BitVecVal(0x2000, 64)
    cpylen = s.BV("len", 64)

    s.memory.store(dst_addr, dst)
    s.memory.store(src_addr, src)
    memcpy(s, inline=True, arguments=[dst_addr, src_addr, cpylen])
    result = s.memory.load(dst_addr, 4, endness="Iend_BE")

    # make sure it copies it all
    s1 = s.copy()
    s1.add_constraints(cpylen == 1)
    nose.tools.assert_true(s1.se.unique(s1.memory.load(dst_addr + 1, 3)))
    nose.tools.assert_equals(len(s1.se.any_n_int(s1.memory.load(dst_addr, 1), 300)), 256)

    s2 = s.copy()
    s2.add_constraints(cpylen == 2)
    nose.tools.assert_equals(len(s2.se.any_n_int(result[31:24], 300)), 256)
    nose.tools.assert_equals(len(s2.se.any_n_int(result[23:16], 300)), 256)
    nose.tools.assert_equals(s2.se.any_n_str(result[15:0], 300), ["AA"])

    l.info("concrete src, concrete dst, symbolic len")
    dst = s2.se.BitVecVal(0x41414141, 32)
    dst_addr = s2.se.BitVecVal(0x1000, 64)
    src = s2.se.BitVecVal(0x42424242, 32)
    src_addr = s2.se.BitVecVal(0x2000, 64)

    s = SimState(arch="AMD64", mode="symbolic")
    s.memory.store(dst_addr, dst)
    s.memory.store(src_addr, src)
    cpylen = s.BV("len", 64)

    s.add_constraints(s.se.ULE(cpylen, 4))
    memcpy(s, inline=True, arguments=[dst_addr, src_addr, cpylen])
    new_dst = s.memory.load(dst_addr, 4, endness="Iend_BE")
    nose.tools.assert_items_equal(s.se.any_n_str(new_dst, 300), ["AAAA", "BAAA", "BBAA", "BBBA", "BBBB"])

def test_inline_strcmp():
    s = SimState(arch="AMD64", mode="symbolic")
    str_a = s.se.BitVecVal(0x41414100, 32)
    str_b = s.BV("mystring", 32)

    a_addr = s.se.BitVecVal(0x10, 64)
    b_addr = s.se.BitVecVal(0xB0, 64)

    s.memory.store(a_addr, str_a, endness="Iend_BE")
    s.memory.store(b_addr, str_b, endness="Iend_BE")

    s_cmp = s.copy()
    cmpres = SimProcedures["libc.so.6"]["strcmp"](s_cmp, inline=True, arguments=[a_addr, b_addr]).ret_expr
    s_match = s_cmp.copy()
    s_nomatch = s_cmp.copy()
    s_match.add_constraints(cmpres == 0)
    s_nomatch.add_constraints(cmpres != 0)

    nose.tools.assert_true(s_match.se.unique(str_b))
    nose.tools.assert_false(s_nomatch.se.unique(str_b))
    nose.tools.assert_equal(s_match.se.any_str(str_b), "AAA\x00")

    s_ncmp = s.copy()
    ncmpres = SimProcedures["libc.so.6"]["strncmp"](
        s_ncmp, inline=True, arguments=[a_addr, b_addr, s.se.BitVecVal(2, s.arch.bits)]
    ).ret_expr
    s_match = s_ncmp.copy()
    s_nomatch = s_ncmp.copy()
    s_match.add_constraints(ncmpres == 0)
    s_nomatch.add_constraints(ncmpres != 0)

    nose.tools.assert_false(s_match.se.unique(str_b))
    nose.tools.assert_true(s_match.se.unique(s_match.memory.load(b_addr, 2)))
    nose.tools.assert_equal(len(s_match.se.any_n_int(s_match.memory.load(b_addr, 3), 300)), 256)
    nose.tools.assert_false(s_nomatch.se.unique(str_b))

    l.info("concrete a, symbolic b")
    s = SimState(arch="AMD64", mode="symbolic")
    str_a = s.se.BitVecVal(0x41424300, 32)
    str_b = s.BV("mystring", 32)
    a_addr = s.se.BitVecVal(0x10, 64)
    b_addr = s.se.BitVecVal(0xB0, 64)
    s.memory.store(a_addr, str_a, endness="Iend_BE")
    s.memory.store(b_addr, str_b, endness="Iend_BE")

    s_cmp = s.copy()
    cmpres = strncmp(s_cmp, inline=True, arguments=[a_addr, b_addr, s.se.BitVecVal(2, s_cmp.arch.bits)]).ret_expr
    s_match = s_cmp.copy()
    s_nomatch = s_cmp.copy()
    s_match.add_constraints(cmpres == 0)
    s_nomatch.add_constraints(cmpres != 0)

    nose.tools.assert_true(s_match.se.solution(str_b, 0x41420000))
    nose.tools.assert_true(s_match.se.solution(str_b, 0x41421234))
    nose.tools.assert_true(s_match.se.solution(str_b, 0x41424300))
    nose.tools.assert_false(s_nomatch.se.solution(str_b, 0x41420000))
    nose.tools.assert_false(s_nomatch.se.solution(str_b, 0x41421234))
    nose.tools.assert_false(s_nomatch.se.solution(str_b, 0x41424300))

    l.info("symbolic a, symbolic b")
    s = SimState(arch="AMD64", mode="symbolic")
    a_addr = s.se.BitVecVal(0x10, 64)
    b_addr = s.se.BitVecVal(0xB0, 64)

    s_cmp = s.copy()
    cmpres = strcmp(s_cmp, inline=True, arguments=[a_addr, b_addr]).ret_expr
    s_match = s_cmp.copy()
    s_nomatch = s_cmp.copy()
    s_match.add_constraints(cmpres == 0)
    s_nomatch.add_constraints(cmpres != 0)

    m_res = strcmp(s_match, inline=True, arguments=[a_addr, b_addr]).ret_expr
    s_match.add_constraints(m_res != 0)
    nm_res = strcmp(s_nomatch, inline=True, arguments=[a_addr, b_addr]).ret_expr
    s_nomatch.add_constraints(nm_res == 0)

    nose.tools.assert_false(s_match.satisfiable())
    nose.tools.assert_false(s_match.satisfiable())

def broken_strtok_r():
    l.debug("CONCRETE MODE")
    s = SimState(arch="AMD64", mode="symbolic")
    s.memory.store(100, s.se.BitVecVal(0x4141414241414241424300, 88), endness="Iend_BE")
    s.memory.store(200, s.se.BitVecVal(0x4200, 16), endness="Iend_BE")
    str_ptr = s.se.BitVecVal(100, s.arch.bits)
    delim_ptr = s.se.BitVecVal(200, s.arch.bits)
    state_ptr = s.se.BitVecVal(300, s.arch.bits)

    st1 = strtok_r(s, inline=True, arguments=[str_ptr, delim_ptr, state_ptr])
    nose.tools.assert_equal(s.se.any_n_int(st1.ret_expr, 10), [104])
    nose.tools.assert_equal(s.se.any_n_int(s.memory.load(st1.ret_expr - 1, 1), 10), [0])
    nose.tools.assert_equal(s.se.any_n_int(s.memory.load(200, 2), 10), [0x4200])

    st2 = strtok_r(s, inline=True, arguments=[s.se.BitVecVal(0, s.arch.bits), delim_ptr, state_ptr])
    nose.tools.assert_equal(s.se.any_n_int(st2.ret_expr, 10), [107])
    nose.tools.assert_equal(s.se.any_n_int(s.memory.load(st2.ret_expr - 1, 1), 10), [0])

    st3 = strtok_r(s, inline=True, arguments=[s.se.BitVecVal(0, s.arch.bits), delim_ptr, state_ptr])
    nose.tools.assert_equal(s.se.any_n_int(st3.ret_expr, 10), [109])
    nose.tools.assert_equal(s.se.any_n_int(s.memory.load(st3.ret_expr - 1, 1), 10), [0])

    st4 = strtok_r(s, inline=True, arguments=[s.se.BitVecVal(0, s.arch.bits), delim_ptr, state_ptr])
    nose.tools.assert_equal(s.se.any_n_int(st4.ret_expr, 10), [0])
    nose.tools.assert_equal(s.se.any_n_int(s.memory.load(300, s.arch.bytes, endness=s.arch.memory_endness), 10), [109])

    st5 = strtok_r(s, inline=True, arguments=[s.se.BitVecVal(0, s.arch.bits), delim_ptr, state_ptr])
    nose.tools.assert_equal(s.se.any_n_int(st5.ret_expr, 10), [0])
    nose.tools.assert_equal(s.se.any_n_int(s.memory.load(300, s.arch.bytes, endness=s.arch.memory_endness), 10), [109])

    s.memory.store(1000, s.se.BitVecVal(0x4141414241414241424300, 88), endness="Iend_BE")
    s.memory.store(2000, s.se.BitVecVal(0x4200, 16), endness="Iend_BE")
    str_ptr = s.se.BitVecVal(1000, s.arch.bits)
    delim_ptr = s.se.BitVecVal(2000, s.arch.bits)
    state_ptr = s.se.BitVecVal(3000, s.arch.bits)

    st1 = strtok_r(s, inline=True, arguments=[str_ptr, delim_ptr, state_ptr])
    nose.tools.assert_equal(s.se.any_n_int(st1.ret_expr, 10), [1004])
    nose.tools.assert_equal(s.se.any_n_int(s.memory.load(st1.ret_expr - 1, 1), 10), [0])
    nose.tools.assert_equal(s.se.any_n_int(s.memory.load(2000, 2), 10), [0x4200])

    st2 = strtok_r(s, inline=True, arguments=[s.se.BitVecVal(0, s.arch.bits), delim_ptr, state_ptr])
    nose.tools.assert_equal(s.se.any_n_int(st2.ret_expr, 10), [1007])
    nose.tools.assert_equal(s.se.any_n_int(s.memory.load(st2.ret_expr - 1, 1), 10), [0])

    st3 = strtok_r(s, inline=True, arguments=[s.se.BitVecVal(0, s.arch.bits), delim_ptr, state_ptr])
    nose.tools.assert_equal(s.se.any_n_int(st3.ret_expr, 10), [1009])
    nose.tools.assert_equal(s.se.any_n_int(s.memory.load(st3.ret_expr - 1, 1), 10), [0])

    st4 = strtok_r(s, inline=True, arguments=[s.se.BitVecVal(0, s.arch.bits), delim_ptr, state_ptr])
    nose.tools.assert_equal(s.se.any_n_int(st4.ret_expr, 10), [0])
    nose.tools.assert_equal(
        s.se.any_n_int(s.memory.load(3000, s.arch.bytes, endness=s.arch.memory_endness), 10), [1009]
    )

    st5 = strtok_r(s, inline=True, arguments=[s.se.BitVecVal(0, s.arch.bits), delim_ptr, state_ptr])
    nose.tools.assert_equal(s.se.any_n_int(st5.ret_expr, 10), [0])
    nose.tools.assert_equal(
        s.se.any_n_int(s.memory.load(3000, s.arch.bytes, endness=s.arch.memory_endness), 10), [1009]
    )

    print "LIGHT FULLY SYMBOLIC TEST"
    s = SimState(arch="AMD64", mode="symbolic")
    str_ptr = s.se.BitVecVal(100, s.arch.bits)
    delim_ptr = s.se.BitVecVal(200, s.arch.bits)
    state_ptr = s.se.BitVecVal(300, s.arch.bits)

    s.add_constraints(s.memory.load(delim_ptr, 1) != 0)

    st1 = strtok_r(s, inline=True, arguments=[str_ptr, delim_ptr, state_ptr])
    s.add_constraints(st1.ret_expr != 0)
    nose.tools.assert_equal(s.se.any_n_int(s.memory.load(st1.ret_expr - 1, 1), 10), [0])

def test_state_merge():
    a = SimState(mode='symbolic')
    a.memory.store(1, a.se.BVV(42, 8))

    b = a.copy()
    c = b.copy()
    a.memory.store(2, a.memory.load(1, 1)+1)
    b.memory.store(2, b.memory.load(1, 1)*2)
    c.memory.store(2, c.memory.load(1, 1)/2)

    # make sure the byte at 1 is right
    nose.tools.assert_equal(a.se.any_int(a.memory.load(1, 1)), 42)
    nose.tools.assert_equal(b.se.any_int(b.memory.load(1, 1)), 42)
    nose.tools.assert_equal(c.se.any_int(c.memory.load(1, 1)), 42)

    # make sure the byte at 2 is right
    nose.tools.assert_equal(a.se.any_int(a.memory.load(2, 1)), 43)
    nose.tools.assert_equal(b.se.any_int(b.memory.load(2, 1)), 84)
    nose.tools.assert_equal(c.se.any_int(c.memory.load(2, 1)), 21)

    # the byte at 2 should be unique for all before the merge
    nose.tools.assert_true(a.se.unique(a.memory.load(2, 1)))
    nose.tools.assert_true(b.se.unique(b.memory.load(2, 1)))
    nose.tools.assert_true(c.se.unique(c.memory.load(2, 1)))

    logging.getLogger('simuvex.plugins.symbolic_memory').setLevel(logging.DEBUG)
    m, merge_flag, merging_occurred = a.merge(b, c)
    logging.getLogger('simuvex.plugins.symbolic_memory').setLevel(logging.WARNING)

    nose.tools.assert_true(merging_occurred)
    nose.tools.assert_equals(sorted(m.se.any_n_int(merge_flag, 10)), [ 0,1,2 ])

    # the byte at 2 should now *not* be unique for a
    nose.tools.assert_false(m.se.unique(m.memory.load(2, 1)))
    nose.tools.assert_true(a.se.unique(a.memory.load(2, 1)))
    nose.tools.assert_true(b.se.unique(b.memory.load(2, 1)))
    nose.tools.assert_true(c.se.unique(c.memory.load(2, 1)))

    # the byte at 2 should have the three values
    nose.tools.assert_items_equal(m.se.any_n_int(m.memory.load(2, 1), 10), (43, 84, 21))

    # we should be able to select them by adding constraints
    a_a = m.copy()
    a_a.add_constraints(merge_flag == 0)
    nose.tools.assert_true(a_a.se.unique(a_a.memory.load(2, 1)))
    nose.tools.assert_equal(a_a.se.any_int(a_a.memory.load(2, 1)), 43)

    a_b = m.copy()
    a_b.add_constraints(merge_flag == 1)
    nose.tools.assert_true(a_b.se.unique(a_b.memory.load(2, 1)))
    nose.tools.assert_equal(a_b.se.any_int(a_b.memory.load(2, 1)), 84)

    a_c = m.copy()
    a_c.add_constraints(merge_flag == 2)
    nose.tools.assert_true(a_c.se.unique(a_c.memory.load(2, 1)))
    nose.tools.assert_equal(a_c.se.any_int(a_c.memory.load(2, 1)), 21)

    # test different sets of plugins
    a = SimState(mode='symbolic')
    nose.tools.assert_true(a.has_plugin('memory'))
    nose.tools.assert_true(a.has_plugin('registers'))
    nose.tools.assert_false(a.has_plugin('libc'))

    b = a.copy()
    a.get_plugin('libc')
    nose.tools.assert_true(a.has_plugin('libc'))
    nose.tools.assert_false(b.has_plugin('libc'))
    c = a.copy().merge(b.copy())[0]
    d = b.copy().merge(a.copy())[0]
    nose.tools.assert_true(c.has_plugin('libc'))
    nose.tools.assert_true(d.has_plugin('libc'))

    # test merging posix with different open files
    a = SimState(mode='symbolic')
    b = a.copy()
    a.posix.get_file(3)
    nose.tools.assert_equal(len(a.posix.files), 4)
    nose.tools.assert_equal(len(b.posix.files), 3)
    c = a.copy().merge(b.copy())[0]
    d = b.copy().merge(a.copy())[0]
    nose.tools.assert_equal(len(c.posix.files), 4)
    nose.tools.assert_equal(len(d.posix.files), 4)

def test_inline_strncmp():
    l.info("symbolic left, symbolic right, symbolic len")
    s = SimState(arch="AMD64", mode="symbolic")
    left = s.BV("left", 32)
    left_addr = s.se.BitVecVal(0x1000, 64)
    right = s.BV("right", 32)
    right_addr = s.se.BitVecVal(0x2000, 64)
    maxlen = s.BV("len", 64)

    s.memory.store(left_addr, left)
    s.memory.store(right_addr, right)

    s.add_constraints(strlen(s, inline=True, arguments=[left_addr]).ret_expr == 3)
    s.add_constraints(strlen(s, inline=True, arguments=[right_addr]).ret_expr == 0)

    s.add_constraints(maxlen != 0)
    c = strncmp(s, inline=True, arguments=[left_addr, right_addr, maxlen]).ret_expr

    s_match = s.copy()
    s_match.add_constraints(c == 0)
    nose.tools.assert_false(s_match.satisfiable())
    # nose.tools.assert_equals(s_match.se.min_int(maxlen), 3)

    s_nomatch = s.copy()
    s_nomatch.add_constraints(c != 0)
    nose.tools.assert_true(s_nomatch.satisfiable())
    # nose.tools.assert_equals(s_nomatch.se.max_int(maxlen), 2)

    l.info("zero-length")
    s = SimState(arch="AMD64", mode="symbolic")
    left = s.BV("left", 32)
    left_addr = s.se.BitVecVal(0x1000, 64)
    right = s.BV("right", 32)
    right_addr = s.se.BitVecVal(0x2000, 64)
    maxlen = s.BV("len", 64)
    left_len = strlen(s, inline=True, arguments=[left_addr]).ret_expr
    right_len = strlen(s, inline=True, arguments=[right_addr]).ret_expr
    c = strncmp(s, inline=True, arguments=[left_addr, right_addr, maxlen]).ret_expr

    s.add_constraints(right_len == 0)
    s.add_constraints(left_len == 0)
    # s.add_constraints(c == 0)
    s.add_constraints(maxlen == 0)
    nose.tools.assert_true(s.satisfiable())

def broken_inline_strstr():
    l.info("concrete haystack and needle")
    s = SimState(arch="AMD64", mode="symbolic")
    str_haystack = s.se.BitVecVal(0x41424300, 32)
    str_needle = s.se.BitVecVal(0x42430000, 32)
    addr_haystack = s.se.BitVecVal(0x10, 64)
    addr_needle = s.se.BitVecVal(0xB0, 64)
    s.memory.store(addr_haystack, str_haystack, endness="Iend_BE")
    s.memory.store(addr_needle, str_needle, endness="Iend_BE")

    ss_res = strstr(s, inline=True, arguments=[addr_haystack, addr_needle]).ret_expr
    nose.tools.assert_true(s.se.unique(ss_res))
    nose.tools.assert_equal(s.se.any_int(ss_res), 0x11)

    l.info("concrete haystack, symbolic needle")
    s = SimState(arch="AMD64", mode="symbolic")
    str_haystack = s.se.BitVecVal(0x41424300, 32)
    str_needle = s.BV("wtf", 32)
    addr_haystack = s.se.BitVecVal(0x10, 64)
    addr_needle = s.se.BitVecVal(0xB0, 64)
    s.memory.store(addr_haystack, str_haystack, endness="Iend_BE")
    s.memory.store(addr_needle, str_needle, endness="Iend_BE")

    ss_res = strstr(s, inline=True, arguments=[addr_haystack, addr_needle]).ret_expr
    nose.tools.assert_false(s.se.unique(ss_res))
    nose.tools.assert_equal(len(s.se.any_n_int(ss_res, 10)), 4)

    s_match = s.copy()
    s_nomatch = s.copy()
    s_match.add_constraints(ss_res != 0)
    s_nomatch.add_constraints(ss_res == 0)

    match_needle = str_needle[31:16]
    nose.tools.assert_equal(len(s_match.se.any_n_int(match_needle, 300)), 259)
    nose.tools.assert_equal(len(s_match.se.any_n_int(str_needle, 10)), 10)

    l.info("symbolic haystack, symbolic needle")
    s = SimState(arch="AMD64", mode="symbolic")
    s.libc.buf_symbolic_bytes = 5
    addr_haystack = s.se.BitVecVal(0x10, 64)
    addr_needle = s.se.BitVecVal(0xB0, 64)
    len_needle = strlen(s, inline=True, arguments=[addr_needle])

    ss_res = strstr(s, inline=True, arguments=[addr_haystack, addr_needle]).ret_expr
    nose.tools.assert_false(s.se.unique(ss_res))
    nose.tools.assert_equal(len(s.se.any_n_int(ss_res, 100)), s.libc.buf_symbolic_bytes)

    s_match = s.copy()
    s_nomatch = s.copy()
    s_match.add_constraints(ss_res != 0)
    s_nomatch.add_constraints(ss_res == 0)

    match_cmp = strncmp(s_match, inline=True, arguments=[ss_res, addr_needle, len_needle.ret_expr]).ret_expr
    nose.tools.assert_items_equal(s_match.se.any_n_int(match_cmp, 10), [0])

    r_mm = strstr(s_match, inline=True, arguments=[addr_haystack, addr_needle]).ret_expr
    s_match.add_constraints(r_mm == 0)
    nose.tools.assert_false(s_match.satisfiable())

    nose.tools.assert_true(s_nomatch.satisfiable())
    s_nss = s_nomatch.copy()
    nomatch_ss = strstr(s_nss, inline=True, arguments=[addr_haystack, addr_needle]).ret_expr
    s_nss.add_constraints(nomatch_ss != 0)
    nose.tools.assert_false(s_nss.satisfiable())

def test_cased_store():
    initial_memory = { 0: 'A', 1: 'A', 2: 'A', 3: 'A' }
    so = SimState(arch="AMD64", memory_backer=initial_memory)

    # sanity check
    nose.tools.assert_equal(so.se.any_n_str(so.memory.load(0, 4), 2), ['AAAA'])

    # the values
    values = [
        None,
        so.BVV('B'),
        so.BVV('CC'),
        so.BVV('DDD'),
        so.BVV('EEEE')
    ]

    # try the write
    s = so.copy()
    x = s.se.BV('x', 32)
    s.memory.store_cases(0, values, [ x == i for i in range(len(values)) ])
    for i,v in enumerate(values):
        v = '' if v is None else s.se.any_str(v)
        w = s.se.any_n_str(s.memory.load(0, 4), 2, extra_constraints=[x==i])
        nose.tools.assert_equal(w, [v.ljust(4, 'A')])

    # and now with a fallback
    y = s.se.BV('y', 32)
    s.memory.store_cases(0, values, [ y == i for i in range(len(values)) ], fallback=s.BVV('XXXX'))
    for i,v in enumerate(values):
        v = '' if v is None else s.se.any_str(v)
        w = s.se.any_n_str(s.memory.load(0, 4), 2, extra_constraints=[y==i])
        nose.tools.assert_equal(w, [v.ljust(4, 'X')])

    # and now with endness
    y = s.se.BV('y', 32)
    s.memory.store_cases(0, values, [ y == i for i in range(len(values)) ], fallback=s.BVV('XXXX'), endness="Iend_LE")
    for i,v in enumerate(values):
        v = '' if v is None else s.se.any_str(v)
        w = s.se.any_n_str(s.memory.load(0, 4), 2, extra_constraints=[y==i])
        print w, v.rjust(4, 'X')
        nose.tools.assert_equal(w, [v.rjust(4, 'X')])

    # and write all Nones
    s = so.copy()
    z = s.se.BV('z', 32)
    s.memory.store_cases(0, [ None, None, None ], [ z == 0, z == 1, z == 2])
    for i in range(len(values)):
        w = s.se.any_n_str(s.memory.load(0, 4), 2, extra_constraints=[z==i])
        nose.tools.assert_equal(w, ['AAAA'])

    # and all Nones with a fallback
    u = s.se.BV('w', 32)
    s.memory.store_cases(0, [ None, None, None ], [ u == 0, u == 1, u == 2], fallback=s.BVV('WWWW'))
    for i,v in enumerate(values):
        w = s.se.any_n_str(s.memory.load(0, 4), 2, extra_constraints=[u==i])
        nose.tools.assert_equal(w, ['WWWW'])

    # and all identical values
    s = so.copy()
    #t = s.se.BV('t', 32)
    s.memory.store_cases(0, [ s.BVV('AA'), s.BVV('AA'), s.BVV('AA') ], [ u == 0, u == 1, u == 2], fallback=s.BVV('AA'))
    r = s.memory.load(0, 2)
    nose.tools.assert_equal(r.op, 'I')
    nose.tools.assert_equal(s.se.any_n_str(r, 2), ['AA'])

    # and all identical values, with varying fallback
    s = so.copy()
    #t = s.se.BV('t', 32)
    s.memory.store_cases(0, [ s.BVV('AA'), s.BVV('AA'), s.BVV('AA') ], [ u == 0, u == 1, u == 2], fallback=s.BVV('XX'))
    r = s.memory.load(0, 2)
    nose.tools.assert_equal(s.se.any_n_str(r, 3), ['AA', 'XX'])

    # and some identical values
    s = so.copy()
    #q = s.se.BV('q', 32)
    values = [ 'AA', 'BB', 'AA' ]
    s.memory.store_cases(0, [ s.BVV(v) for v in values ], [ u == i for i in range(len(values))], fallback=s.BVV('XX'))
    r = s.memory.load(0, 2)
    for i,v in enumerate(values + ['XX']):
        w = s.se.any_n_str(s.memory.load(0, 2), 2, extra_constraints=[u==i])
        nose.tools.assert_equal(w, [(values+['XX'])[i]])