Re: [klee-dev] Working with fixed memory locations.

2022-06-20 Thread Marco Vanotti
;> > 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
>> >> 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>
>> >> > >> <mailto:klee-dev-boun...@imperial.ac.uk>> on behalf of Marco
>> >> Vanotti mailto:mvano...@dc.uba.ar>>
>> >> *Sent:*16 June 2022 18:55
>> >> *To:*klee-dev > >> <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:
>> >>
>> >> 

Re: [klee-dev] Working with fixed memory locations.

2022-06-19 Thread Daniel Schemmel
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>
>>         >         <mailto:klee-dev-boun...@imperial.ac.uk>> on behalf of
Marco
>>         Vanotti mailto:mvano...@dc.uba.ar>>
>>         *Sent:*16 June 2022 18:55
>>         *To:*klee-dev >         <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


___
klee-dev mailing list
klee-dev@imperial.ac.uk
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


Re: [klee-dev] Working with fixed memory locations.

2022-06-17 Thread Marco Vanotti
Hi Manuel,

On Fri, Jun 17, 2022 at 3:29 AM Carrasco, Manuel G <
m.carra...@imperial.ac.uk> wrote:

> Hi Marco,
>
> I wasn't aware of the klee_define_fixed_object intrinsic.
>
> This is a question on my side regarding KLEE. If an array is always
> read/written using constant accesses,  are the "getArrayForUpdate" calls
> strictly necessary? However, I'm not sure if this description fits your
> blob. Is it a constant buffer after its initialization? Is it symbolically
> indexed? How is it initialized?
>

No, the blob is not constant. It represents a virtual machine which holds
the instructions, memory and registers. My program is just an emulator. I
point it to the entry point inside the memory region and it starts
executing.

I've heard that KLEE, and symbolic execution in general, are not that great
in this scenario. However, the machine that I am interpreting is extremely
simple.

Best,
Marco


> Best,
> Manuel.
> --
> *From:* klee-dev-boun...@imperial.ac.uk 
> on behalf of Cristian Cadar 
> *Sent:* 17 June 2022 10:53
> *To:* mvano...@dc.uba.ar ; Nowack, Martin <
> m.now...@imperial.ac.uk>
> *Cc:* klee-dev 
> *Subject:* Re: [klee-dev] Working with fixed memory locations.
>
> 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  > <mailto:mvano...@dc.uba.ar >> wrote:
> >
> > Hi Martin, Manuel,
> >
> > Thanks for your answer :) !
> >
> > On Thu, Jun 16, 2022 at 1:19 PM Nowack, Martin
> > 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
> >> 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 KLEE

Re: [klee-dev] Working with fixed memory locations.

2022-06-17 Thread Marco Vanotti
ter/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>
> >>  >> <mailto:klee-dev-boun...@imperial.ac.uk>> on behalf of Marco
> >> Vanotti mailto:mvano...@dc.uba.ar>>
> >> *Sent:*16 June 2022 18:55
> >> *To:*klee-dev  >> <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
>
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


Re: [klee-dev] Working with fixed memory locations.

2022-06-17 Thread Carrasco, Manuel G
Hi Marco,

I wasn't aware of the klee_define_fixed_object intrinsic.

This is a question on my side regarding KLEE. If an array is always 
read/written using constant accesses,  are the "getArrayForUpdate" calls 
strictly necessary? However, I'm not sure if this description fits your blob. 
Is it a constant buffer after its initialization? Is it symbolically indexed? 
How is it initialized?

Best,
Manuel.

From: klee-dev-boun...@imperial.ac.uk  on 
behalf of Cristian Cadar 
Sent: 17 June 2022 10:53
To: mvano...@dc.uba.ar ; Nowack, Martin 

Cc: klee-dev 
Subject: Re: [klee-dev] Working with fixed memory locations.

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  <mailto:mvano...@dc.uba.ar>> wrote:
>
> Hi Martin, Manuel,
>
> Thanks for your answer :) !
>
> On Thu, Jun 16, 2022 at 1:19 PM Nowack, Martin
> 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
>> 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 

Re: [klee-dev] Working with fixed memory locations.

2022-06-17 Thread Cristian Cadar
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 <mailto:mvano...@dc.uba.ar>> wrote:


Hi Martin, Manuel,

Thanks for your answer :) !

On Thu, Jun 16, 2022 at 1:19 PM Nowack, Martin
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
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>
mailto:klee-dev-boun...@imperial.ac.uk>> on behalf of Marco
Vanotti mailto:mvano...@dc.uba.ar>>
*Sent:*16 June 2022 18:55
    *To:*klee-dev 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 aro

Re: [klee-dev] Working with fixed memory locations.

2022-06-16 Thread Marco Vanotti
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

Best Regards,
Marco

On Thu, Jun 16, 2022 at 3:48 PM Marco Vanotti  wrote:

> Hi Martin, Manuel,
>
> Thanks for your answer :) !
>
> On Thu, Jun 16, 2022 at 1:19 PM Nowack, Martin 
> wrote:
>
>> Hi Marco,
>>
>> Maybe the following helps you:
>>
>> 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 
>> 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 KLEE executes a LLVM-IR load instruction
>> <https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L2722>,
>> it will try to find
>> <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 this function
>> <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 
>> on behalf of Marco Vanotti 
>> *Sent:* 16 June 2022 18:55
>> *To:* klee-dev 
>> *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.
>>
>&g

Re: [klee-dev] Working with fixed memory locations.

2022-06-16 Thread Marco Vanotti
Hi Martin, Manuel,

Thanks for your answer :) !

On Thu, Jun 16, 2022 at 1:19 PM Nowack, Martin 
wrote:

> Hi Marco,
>
> Maybe the following helps you:
>
> 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 
> 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 KLEE executes a LLVM-IR load instruction
> <https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L2722>,
> it will try to find
> <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 this function
> <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 
> on behalf of Marco Vanotti 
> *Sent:* 16 June 2022 18:55
> *To:* klee-dev 
> *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 

Re: [klee-dev] Working with fixed memory locations.

2022-06-16 Thread Nowack, Martin
Hi Marco,

Maybe the following helps you:
https://github.com/klee/klee/blob/292600cf54d5fd73278f67a4f98c2f955cbdaa10/test/Feature/DefineFixedObject.c

Best,
Martin

On 16. Jun 2022, at 20:43, Carrasco, Manuel G 
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.

As far as I understand, when KLEE executes a LLVM-IR load 
instruction<https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L2722>,
 it will try to 
find<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 this 
function<https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L648> 
and addExternalObject perhaps as well.

I apologise if you already know this!

Best regards,
Manuel.


From: klee-dev-boun...@imperial.ac.uk<mailto:klee-dev-boun...@imperial.ac.uk> 
mailto:klee-dev-boun...@imperial.ac.uk>> on 
behalf of Marco Vanotti mailto:mvano...@dc.uba.ar>>
Sent: 16 June 2022 18:55
To: klee-dev 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

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


Re: [klee-dev] Working with fixed memory locations.

2022-06-16 Thread Carrasco, Manuel G
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.

As far as I understand, when KLEE executes a LLVM-IR load 
instruction<https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L2722>,
 it will try to 
find<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 this 
function<https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L648> 
and addExternalObject perhaps as well.

I apologise if you already know this!

Best regards,
Manuel.


From: klee-dev-boun...@imperial.ac.uk  on 
behalf of Marco Vanotti 
Sent: 16 June 2022 18:55
To: klee-dev 
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


[klee-dev] Working with fixed memory locations.

2022-06-16 Thread Marco Vanotti
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev