Model of strncpy_from_user: could we create an object with a given address?

[zhangzhenghsy]

long strncpy_from_user(char *dst, const char __user *src, long count)
(https://elixir.bootlin.com/linux/v5.5-rc5/source/lib/strncpy_from_user.c#L104)
copies a buf from userspace to a given address dst
the buf can be tail of a struct ( struct file_name for example, https://elixir.bootlin.com/linux/v5.5-rc5/source/include/linux/fs.h#L2517)
we symbolize the struct but the size of buf is not counted, thus the dst address doesn't belong to any object

I want to model it
It seems that when we create an object in UCKLEE (Executor::create_mo, memory->allocate), we cannot control the address of the object
How could we solve it?

My current thinking is that if the address is adjacent to an existing object (struct file_name in the above example), we found it can extend the size of it
if we cannot find such a object, then we make a mapping between the given concrete address and real object address?

test case: /home/zzhan173/repos/Linux_kernel_UC_KLEE/configs/getname_flags_cover_func.json

[zhangzhenghsy]

After discussion, currently, we plan to:

1. For strncpy_from_user, we just do a standard copy_from_user(). First, try to find the corresponding allocated object of the dst pointer. Then write symbolic values to the given size memory.
2. To solve this specific issue when we need to allocate a memory object for a struct with a size 0 final field (implies that it's a non-fixed length buffer), we allocate (sizeofstruct + 8192) bytes. In other words, we prepare an 8192 bytes buffer for the final field. 8192 can be changed to a larger value if necessary later.

[ZHYfeng]

7d607ff

e86ba45