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

[Chaoqi Zhang]

Dear Martin,

Really thanks for your reply!

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.

Best wishes,
Chaoqi

> On Jun 27, 2022, at 22:19, Nowack, Martin <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 <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>

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