[klee-dev] Working with fixed memory locations.
Marco Vanotti
mvanotti at dc.uba.ar
Sat Jun 18 01:12:31 BST 2022
Hi Cristian,
Thanks for your answer. I have tried *--optimize-array=all*, but that
didn't fix the problem :(.
It would be a better user experience to get an error message instead of a
segfault. In any case, if this is stopping because it's running out of
memory, is there a way to remove that restriction? My server still had a
few GiB to spare 😅.
On Fri, Jun 17, 2022 at 2:53 AM Cristian Cadar <c.cadar at imperial.ac.uk>
wrote:
> Hi Marco, you seem to be reaching an issue with the solver, which is
> having trouble reasoning about the huge symbolic array (requiring
> excessive time and memory). You should try to shrink that array if
> possible. You can also try --optimize-array=all, but it might not help
> in your case.
>
> Best,
> Cristian
>
> On 17/06/2022 05:02, Marco Vanotti wrote:
> > 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 <mvanotti at dc.uba.ar
> > <mailto:mvanotti at dc.uba.ar>> wrote:
> >
> > Hi Martin, Manuel,
> >
> > Thanks for your answer :) !
> >
> > On Thu, Jun 16, 2022 at 1:19 PM Nowack, Martin
> > <m.nowack at imperial.ac.uk <mailto:m.nowack at 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.carrasco at imperial.ac.uk <mailto:m.carrasco at 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-bounces at imperial.ac.uk
> >> <mailto:klee-dev-bounces at imperial.ac.uk>
> >> <klee-dev-bounces at imperial.ac.uk
> >> <mailto:klee-dev-bounces at imperial.ac.uk>> on behalf of Marco
> >> Vanotti <mvanotti at dc.uba.ar <mailto:mvanotti at dc.uba.ar>>
> >> *Sent:*16 June 2022 18:55
> >> *To:*klee-dev <klee-dev at imperial.ac.uk
> >> <mailto:klee-dev at 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 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>
> >
> >
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at imperial.ac.uk
> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list