[klee-dev] Working with fixed memory locations.
Daniel Schemmel
d.schemmel at imperial.ac.uk
Sun Jun 19 19:04:09 BST 2022
Hi Marco,
I had a look at your stack trace, and the crash might have been caused
by KLEE when building the solver query before passing it to the actual
solver. Could you check out https://github.com/klee/klee/pull/1523 and
see if that changes anything for you?
Best,
Daniel
On 2022-06-18 01:12, Marco Vanotti wrote:
> 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
>
>
> _______________________________________________
> 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