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

[Eric Lu]

in addition, are there some symbolic implementations can do what I want?


On Sat, Jun 15, 2013 at 8:27 PM, Eric Lu <eirc.lew at gmail.com> wrote:

> 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