[klee-dev] Fwd: create ponter/array access bounds expressions with klee

[Eric Lu]

Hi, Paul

  My descriptions in the previous mail is ambiguous for you.  "a" is array.

   In fact, What I want to do is something like below:
1) generate expressions to define the accessed memory regions of some
variables in some code scope(a basic block or loop);
2) collect the memory trace in the first iterations.
3)the OPT: if  execution of  some other iteration has the same memory
regions according the    generated expressions in 1), then we don't to
collect the memory trace again.

I think this method will save space and time.

I think KLEE cannot satisfy the demand of the project. because:
1) KLEE cannot merge multi continuous objects into one memory objects. I.E.
 ptr++;
2) it does not support symbolic size for array as you have pointed.
3) It cannot execute the whole loops to get the formula as you have
pointed.

Am I right on this issue?

Thanks!

Eric


On Fri, Jun 14, 2013 at 9:14 PM, Paul Marinescu <
paul.marinescu at imperial.ac.uk> wrote:

> Hi,
> As a high-level answer, KLEE's analysis works on a per-path basis. This
> means that symbolic expressions are valid only for the particular path on
> which they're generated, not for the program as a whole, which is what you
> seem to be looking for.
>
> I'm not sure if I understand your example since you use ambiguous
> constructs (is N a literal? a symbolic parameter? can't multiply a pointer
> by a scalar (a+1)*N . a == array?). However,
>
> 1. To use KLEE you need to compile the program, so all statically
> allocated objects (a and b if N is a literal) will have a fixed size and a
> straightforward 'region expression'
>
> 2. KLEE doesn't support objects of symbolic size anyway
>
> 3. Even if it would, you wouldn't get a formula for ptr which summarizes
> all possible executions, because of the for loop.
>
> Best,
> Paul
>
>
> On 14/06/13 12:48, Eric Lu wrote:
>
>>
>> Hi, Paul
>> Thanks for your reply.
>>
>> What I want to generate a expression for pointers to express the memory
>> space. I.E.
>>      int *ptr;
>>      int a[N], b[(a+1)*N];
>>      for( i = 0; i < N; i++){
>>        ptr++;
>>        array[i] += i + 2;
>>        ptr++;
>>        b[a*i+1] = i;
>>     }
>>
>>     We get the access region expression for each variable:
>>     1)  ptr: (start_address: ptr, upbound:2*N, lowerbound: 0 )
>>     2) a: ( &a[0], N, 0);
>>    3) b:  (&b[1], a*N, 1);
>>
>> Can klee do this? I have look through the mail list, there seems no
>> subject related to this case.
>>
>>
>> On Fri, Jun 14, 2013 at 4:46 PM, Paul Marinescu
>> <paul.marinescu at imperial.ac.uk <mailto:paul.marinescu@**imperial.ac.uk<paul.marinescu at imperial.ac.uk>
>> >>
>>
>> wrote:
>>
>>     Hi,
>>     KLEE does generate symbolic expressions to check for out-of-bounds
>>     memory access. If you are looking for something specific, you may
>>     get more answers if you explain it in a few sentences, rather than
>>     expect people to read the whole paper.
>>
>>     Best,
>>     Paul
>>
>>     On 14 Jun 2013, at 08:31, Eric Lu <eirc.lew at gmail.com
>>     <mailto:eirc.lew at gmail.com>> wrote:
>>
>>      Hello,
>>>       I want to generate pointer/array access bounds expressions with
>>>     KLEE in LLVM. I am new to symbolic execution and KLEE, and I am
>>>     not sure if  some body have done this before?
>>>       What I need is something like symbolic execution in [1]， is it
>>>     possible to implement [1] based KLEE?
>>>
>>>        Or are there some better ways to do this?  Any advice is welcome!
>>>
>>>
>>>     [1] Symbolic Bounds Analysis of Pointers, Array Indices, and
>>>     Accessed Memory Regions
>>>
>>>
>>>     Thanks!
>>>
>>>     Eric
>>>     ______________________________**_________________
>>>     klee-dev mailing list
>>>     klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.**uk<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<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<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
-------------- next part --------------
HTML attachment scrubbed and removed