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
<[email protected] <mailto:[email protected]>>
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 <[email protected]
<mailto:[email protected]>> 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
[email protected] <mailto:[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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
