After letting it run for a few hours I've observed that klee spawns a
subprocess that keeps growing on memory until it reaches ~100GiB and
then it stops and restarts again.
Nothing is being printed indicating an error, but I'm not sure if the
behavior is normal. This is with KLEE from the docker container.
I've tried building KLEE from source, both with STP and Z3 support, and
running my program makes it crash with a segfault :(
Here is the backtrace for the crash with the STP solver:
https://pastebin.com/raw/xpf9D9VD <https://pastebin.com/raw/xpf9D9VD>
Best Regards,
Marco
On Thu, Jun 16, 2022 at 3:48 PM Marco Vanotti <mvano...@dc.uba.ar
<mailto:mvano...@dc.uba.ar>> wrote:
Hi Martin, Manuel,
Thanks for your answer :) !
On Thu, Jun 16, 2022 at 1:19 PM Nowack, Martin
<m.now...@imperial.ac.uk <mailto:m.now...@imperial.ac.uk>> wrote:
Hi Marco,
Maybe the following helps you:
https://github.com/klee/klee/blob/292600cf54d5fd73278f67a4f98c2f955cbdaa10/test/Feature/DefineFixedObject.c
<https://github.com/klee/klee/blob/292600cf54d5fd73278f67a4f98c2f955cbdaa10/test/Feature/DefineFixedObject.c>
This seems to be what I am looking for, thanks!. I tried using it
for small variables and it works. However, for a big object
(0x256000 bytes) it shows the following warning:
*KLEE: WARNING ONCE*: flushing 2449408 bytes on read, may be slow
and/or crash: MO195[2449408] allocated at main(): call void
@klee_define_fixed_object(i8* inttoptr (i64 8404992 to i8*), i64
2449408), !dbg !171
KLEE is still running, so maybe it just means it is slow.
I went with the approach of having my blob as a global variable, and
then `memcpy` it into the address after calling define_fixed_object.
Best,
Martin
On 16. Jun 2022, at 20:43, Carrasco, Manuel G
<m.carra...@imperial.ac.uk <mailto:m.carra...@imperial.ac.uk>>
wrote:
Hi Marco!
I have a program that when compiled, adds a program header
that loads a data blob into a fixed memory location.
I'm sorry to ask, but could you explain a bit more how this
works? At first glance, I'd say that if any of this happens on
a stage later than LLVM-IR, it may be hard to mimic in KLEE.
I have a bunch of files that I add as .incbin into a section, and
then my linker scripts put them in a fixed address when it links the
program altogether. I think there is no way this would work with
LLVM IR.
As far as I understand, when KLEEexecutes a LLVM-IR load
instruction
<https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L2722>,
it will try tofind
<https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L4191>the
MemoryObjects (more than one if it is a symbolic pointer) that
contain the address. Conceptually, you want KLEE to somehow
have a MemoryObject at the hardcoded address.
One way to go could be modelling this as a LLVM-IR
GlobalVariable at your fixed address with the content of your
blob. If this makes sense, you may want to check thisfunction
<https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L648>and
addExternalObject perhaps as well.
Thanks! This looks interesting, but I am a bit puzzled about how to
go with this. Should I recompile KLEE to add support for my use
case? I checked on the MemoryManager class and it seems like it just
allocates stuff at whatever place is available.
I apologise if you already know this!
I did not know any of that :) This is the second time I am using
KLEE, and the first one was a big failure :P
Thanks!
Marco
Best regards,
Manuel.
------------------------------------------------------------------------
*From:*klee-dev-boun...@imperial.ac.uk
<mailto:klee-dev-boun...@imperial.ac.uk>
<klee-dev-boun...@imperial.ac.uk
<mailto:klee-dev-boun...@imperial.ac.uk>> on behalf of Marco
Vanotti <mvano...@dc.uba.ar <mailto:mvano...@dc.uba.ar>>
*Sent:*16 June 2022 18:55
*To:*klee-dev <klee-dev@imperial.ac.uk
<mailto:klee-dev@imperial.ac.uk>>
*Subject:*[klee-dev] Working with fixed memory locations.
Hi klee-dev!
I am new to KLEE, and have a question about using it with one
of my programs.
I have a program that when compiled, adds a program header
that loads a data blob into a fixed memory location.
This means that my program has this fixed memory location
hardcoded all around the place (also this blob has references
to itself).
I would like to load my program in KLEE to get a better
understanding of how it works. The problem I am facing is that
I have no idea how to make KLEE understand that I need this
blob mapped in that address.
This are the things I've tried:
* Using wllvm/gclang to get the full program linked together,
following my link script, then extracting the bc and running
that with KLEE. This didn't work. KLEE complains that the
pointers are invalid.
* Manually embedding the blob into my program as an array,
then calling `mmap` with `MAP_FIXED` to map the area that I
want and copying over the blob.
The issue here is that MAP_FIXED returns EPERM because
probably the address range I am trying to map is already mapped.
* Setting the KLEE deterministic allocations to encompass the
range that I care about, then doing a big `malloc` and making
sure that my range is inside that malloc chunk.
For this last one, I am using flags like:
--allocate-determ --allocate-determ-start-address=8404992
--allocate-determ-size=3145728
One of the things that I see is that KLEE fails to mmap big
chunks (in the order of 100MiB). But even if I decrease the
size, I still get failures when I try to assert things like:
uintptr_t malloc_addr = (uintptr_t) malloc(malloc_size);
klee_assert(BASE_ADDR >= malloc_addr);
klee_assert(BASE_ADDR < malloc_addr + malloc_size);
------
Something that might be relevant is that in reality I need two
of these blobs loaded into different regions of memory, but so
far I can't even get to load one. And they are not too far
apart from each other, so if, for example, the malloc approach
works, I could just increase the size and make the two
allocations.
One thing that might complicate things, is that these
addresses might collide with where KLEE tries to load the
program. I don't know how to deal with that either.
Any advice on how to tune KLEE for this use case?
Best Regards,
Marco
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
