[klee-dev] How can I use shared memory correctly in KLEE?

[Nowack, Martin]

Hi Chaoqi,



On 27. Jun 2022, at 15:53, Chaoqi Zhang <prncoprs at 163.com<mailto:prncoprs at 163.com>> wrote:

I want to communicate with the KLEE process itself, not the tested software.

I insert the `shm_*` code into the executor.cpp, so that the Executor in KLEE can communicate with other process.

Just a guess. Depending on where exactly you insert the call,  by any chance is the call executed multiple times?
(Maybe cross-check it with a dirty but useful `llvm::errs() << “shm_open has been called\n”;` or `klee_warning(“...")`)

Best,
Martin



Best wishes,
Chaoqi

On Jun 27, 2022, at 22:19, Nowack, Martin <m.nowack at imperial.ac.uk<mailto:m.nowack at imperial.ac.uk>> wrote:

Hi Chaoqi,

Can you clarify: Do you want to test software that uses `shm_*` or do you want communicate with the KLEE process itself?

KLEE should not modify any `shm` allocated objects.

The only unintended modification that could happen is if your tested application uses external function calls that somehow manipulate that memory.

Best,
Martin

On 25. Jun 2022, at 18:40, prncoprs at 163.com<mailto:prncoprs at 163.com> wrote:

Dear all,

I want to use shared memory in klee, so that I can expose some info of the klee to other processes in the same operate system.

I use the POSIX `shm_open()` to get a shared memory fd `shm_fd`, after I use `ftruncate()` to set the size, then I use `mmap()` to get the shared memory address `(int *)shm_region` in the klee program. However, I find that the value and content of `(int *)shm_region` changes. For example, when I first got the value of `shm_region`, it is 0x7f8892da0000, and I set the content of the `shm_region` to 0. But after a while, I found the value of `shm_region` was changed to 0x55658e481eb4, the content of `shm_region[0]` is 267633609, without any my manually modified.

After I checked the mailing list, I found that klee did not support multi-processes. However, I think this is just an inter-processes communication issue rather the multi-processes. Could someone tell me why the shared memory address changes in klee?

I also tried other IPC methods, like shared files and PIPE, and they work correctly. Does this mean that I cannot use shared memory in klee to do the IPC?

Thanks!

Best wishes,
Chaoqi
_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



-------------- next part --------------
HTML attachment scrubbed and removed