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 <[email protected]> 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 <[email protected] > > <mailto:[email protected]>> wrote: > > > > Hi Martin, Manuel, > > > > Thanks for your answer :) ! > > > > On Thu, Jun 16, 2022 at 1:19 PM Nowack, Martin > > <[email protected] <mailto:[email protected]>> 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 > >> <[email protected] <mailto:[email protected]>> > >> 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:*[email protected] > >> <mailto:[email protected]> > >> <[email protected] > >> <mailto:[email protected]>> on behalf of Marco > >> Vanotti <[email protected] <mailto:[email protected]>> > >> *Sent:*16 June 2022 18:55 > >> *To:*klee-dev <[email protected] > >> <mailto:[email protected]>> > >> *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 > >> [email protected] <mailto:[email protected]> > >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> > > > > > > _______________________________________________ > > klee-dev mailing list > > [email protected] > > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
