[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