Closed tiedaoxiaotubie closed 3 years ago
Hi,
interesting thanks for helping improving SymCC !
Is this for when you use SymCC with SYMCC_INPUT_FILE
and the program mmaps that file? It would be nice to have a minimal test case to reproduce. More generally, it would be nice at some point to have a more generic way to make memory symbolic (like klee or S2E have).
I imagine the main problem in your code comes from the fact that mmap
will map the file to memory and it will be accessed out of order, so a shadow memory for the the whole file should be created. If I understand well, now you copied the code from read
which copies one word from the current file offset (inputOffset
) and it does not make much sense to use the file offset to the input file for mmap
. I think you should use the offset passed as parameter to mmap
instead, the off
parameter?
Interesting question is what to do when the same file is mapped at multiple addresses.
I assume the type error may be a consequence of that. Diagnosing it would require to log the generated constraints and see where the type mismatch happens.
I have changed to use off
to replace inputOffset
, but still got the same error message.
What do you mean now you copied the code from read which copies *one word* from the current file offset
?
I am using len
when I create shadow memory in my code: ReadWriteShadow shadow(result, len);
, so I will map the whole file to memory IMO, am I right?
Hi, I noticed that
mmap()
andmmap64()
didn't create symbolic expression in their libc wrapper. However,mmap
sometimes will be used as a read function, since symbolic expression will be created inread()
wrapper https://github.com/eurecom-s3/symcc/blob/master/runtime/LibcWrappers.cpp#L140, I also add these code inmmap64()
wrapper, so that we can create symbolic expression inside it too. Here is my implementation:I can compile it successfully, however, I got error message when I tried to run target program:
Any idea about how to fix it?