Hi Oleg, Ah - yeah there is. The name is `klee::findSymbolicObjects` but it’s a bit hidden: https://github.com/klee/klee/blob/fc83f06b17221bf5ef20e30d9da1ccff927beb17/include/klee/Expr/ExprUtil.h#L38 and https://github.com/klee/klee/blob/fc83f06b17221bf5ef20e30d9da1ccff927beb17/lib/Expr/ExprUtil.cpp#L123
In a nutshell, it’s a tree traversal and returns all used arrays. This functionality is only really required in KLEE’s current implementation when a solver is called to generate assignments for expressions, e.g.: https://github.com/klee/klee/blob/fc83f06b17221bf5ef20e30d9da1ccff927beb17/lib/Solver/STPSolver.cpp#L233. Therefore, it’s not really visible. Best, Martin > On 12. Dec 2023, at 14:23, Oleg Sokolsky <sokol...@cis.upenn.edu> wrote: > > Hi Martin, > > Thanks for the quick response. Our question was slightly different, let me > clarify. Given an instance of the Expr object, we want to obtain the set of > symbolic names used in that instance. ExprPPrinter does it, for example, but > in a very specific way and, frankly, we struggled to understand how it works. > We were wondering if there is a generic way to do it. I was expecting a > visitor in the Expr hierarchy, or something similar, but could not find it. > > Thanks again, > Oleg > > On 12/12/23 05:42, Nowack, Martin wrote: >> Hi Haozhi Fan, >> >> The symbolic names are generated using the call `klee_make_symbolic` >> indirectly or directly in your software under test. >> KLEE tracks the memory object that have been associated with these calls >> (https://github.com/klee/klee/blob/fc83f06b17221bf5ef20e30d9da1ccff927beb17/lib/Core/Executor.cpp*L4435) >> and assigns it an array that has the same name or similar name that is >> unique. >> Reading from this memory will result in read expressions that reference this >> array and are later used as part of the solver calls. >> >> Best, >> Martin >> >>> On 11. Dec 2023, at 20:07, Haozhi Fan <h3...@seas.upenn.edu> wrote: >>> >>> Dear klee-dev members, >>> >>> I was wondering if you could share some insight into how KLEE collects the >>> set of symbolic names from an expression? Namely, how does KLEE generate >>> the kquery for a specific path condition and from which files should I be >>> looking for the details of such implementation? Thank you! >>> >>> Best regards, >>> Haozhi Fan >>> _______________________________________________ >>> klee-dev mailing list >>> klee-dev@imperial.ac.uk >>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> _______________________________________________ >> klee-dev mailing list >> klee-dev@imperial.ac.uk >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > _______________________________________________ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
