Hello Henning, Your observations are correct about possible side effects if two routines are executed in the same address space. As we describe a bit in our CAV paper, we avoided this problem in UC-KLEE by using independent address spaces (within a single execution state) for executing each function. That is, we maintain the path constraints imposed on the path through the first function, but we discard all of its writes and use a clean address space for executing the second function. Our equivalence checking algorithm then compares pairs of reachable objects across these two address spaces.
Let's take further discussion offline since this mailing list is for the base open source KLEE project, not the various research extensions. Thanks, -David On Jul 19, 2011, at 9:24 AM, Henning Femmer wrote: > Hello, > > let me first congratulate again on your good work here. From your answers and > my experience with KLEE, your tool seems to be based upon lots of experience > and deep analysis of the domain. > > I’m working on comparing different implementations of functions, but in my > case, each function has a whole “state” in their back (global variables, > different data types and variables, etc.). As far as I understood, there is > only one state for each path in KLEE. That means, however, that functional > equivalence checking, as proposed in your paper, operates on the same memory, > which might cause some nasty side effects. > > It would be good to fork the whole state for each implementation and then > join again and check the differences in the two branches. Does KLEE offer a > functionality to join or to compare different states? > > Keep up the good work, > Henning > > _______________________________________________ > klee-dev mailing list > [email protected] > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
