in addition, are there some symbolic implementations can do what I want?
On Sat, Jun 15, 2013 at 8:27 PM, Eric Lu <[email protected]> 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 < > [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
