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 < [email protected]> 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 >> <[email protected] >> <mailto:paul.marinescu@**imperial.ac.uk<[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].**uk<[email protected]> >>> > >>> >>> https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> >>> >> >> >> >> >> >> ______________________________**_________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> >> >> > > > ______________________________**_________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
