как применить ограничения к побочным эффектам кучи в angr

Question

Я пытаюсь использовать angr для проверки поведения функции, получая правильный ввод для данного результата. Функция изменяет буфер, в данном случае она просто копирует в него входные данные, поэтому я устанавливаю символические переменные в куче, к которой применяю ограничение равенства. Затем я создаю символическую переменную для ввода функции. То, что я намеревался сделать, это то, что angr, по сути, запускает функцию до тех пор, пока не будет найден вход, который при копировании в буфер удовлетворяет наложенному на него ограничению. Однако, когда он запускается, я получаю только одну тупиковую ветвь, где вывод имеет правильное значение, а ввод — нет. Ниже я прикрепил решатель и исходный код тестовой программы. Это провал моей реализации? Или такой подход к решению проблемы некорректен

решатель

      import angr
import claripy
import angr.sim_type as T

if __name__ == '__main__':
    path = './test'
    target = 'test_fn' 
    target_buf = 'buffer' 


    word = b'hello\0'


    program = angr.Project(path)
    fn = program.loader.find_symbol(target)
    buf = program.loader.find_symbol(target_buf)

    fn_addr = fn.rebased_addr
    buf_addr = buf.rebased_addr

    cc = program.factory.cc(func_ty=T.SimTypeFunction(
        args=[T.parse_type('char*')],
        returnty=T.parse_type('void')
        ))

    str_in = claripy.BVS('input', 8 * len(word))
    fn_call_state = program.factory.call_state(fn_addr, angr.calling_conventions.PointerWrapper(str_in), cc=cc)
    ptr_out = fn_call_state.heap.allocate(len(word))

    chars = []
    for i, v in enumerate(word):
        ch = claripy.BVS('char_{}'.format(i), 8)
        chars.append(ch)
        fn_call_state.solver.add(ch == int(v))
    word_sym = claripy.Concat(*chars)
    fn_call_state.memory.store(buf_addr, ptr_out)
    fn_call_state.memory.store(ptr_out, word_sym)

    simgr = program.factory.simgr(fn_call_state, save_unsat=True)
    simgr.run()
    print(simgr)
    for s in simgr.deadended:
        print(s.solver.eval(str_in, cast_to=bytes))
        print(s.solver.eval(word_sym, cast_to=bytes))

тестовая программа

      #include <string.h>
#include <stdlib.h>
#include <stdio.h>

char* buffer;

void test_fn(char* input) {
        strcpy(buffer, input);
        return;
}

int main(int argc, char** argv) {
        buffer = (char*) malloc(100);
        test_fn("hello");
}

когда я запускаю решатель, я получаю вывод, подобный следующему, хотя первое значение, входное значение, изменяется, по-видимому, случайным образом. Есть ли способ применить это ограничение, чтобы побочные эффекты программы имели приоритет? Я не понимаю, как эти два значения различаются. Это ошибка в том, как я подготавливаю память?

      b'\x01\x01\x01\x04\x01\x02'
b'hello\x00'