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 <
Post by Paul MarinescuHi,
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
Post by Eric LuHi, 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;
}
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
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
Hello,
Post by Eric LuI 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
https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
______________________________**_________________
klee-dev mailing list
https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
______________________________**_________________
klee-dev mailing list
https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>