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

[Paul Marinescu]

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 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>
>>     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
>