Ahh, I was thinking the constraints passed to the solver held per-line information rather than per-CFG block information. I was wondering why there weren't constraints for the contents of each variable in the constraint vector but I see now that would be unnecessary.
Thanks, Jonathan Daniel Dunbar wrote: > On Thu, Mar 11, 2010 at 11:38 AM, Jonathan Cooke <jdcooke at andrew.cmu.edu> > wrote: > >> Hello, >> >> I'm attempting to modify the constraints KLEE adds to states in hopes of >> getting better path merging. I noticed when KLEE comes across an >> assignment, rather than adding a constraint about the variable being >> assigned to, KLEE updates the state's stack information to reflect this >> assignment. I'm trying to figure out how the solver uses this >> information when solving constraints, but I couldn't find the stack >> being passed to the solver at any point. It looks like the TimingSolver >> only passes the constraints and the expression to the Solver. Where >> does KLEE's Solver take variable information into account? >> > > Right. Every state has a (byte addressable) stack and a heap, and each > byte maps to a symbolic expression. Loads and stores read and write > those symbolic expressions. In the case of arrays, the memory object > containing the array now becomes a list of writes (indices and values) > -- this may be what you are thinking of when you say assignment? > > I'm not exactly sure how to explain this better, but here is an > pseudo-example: > -- > // state -- x -> undef, y -> [undef, undef, undef, undef] > char x, y[4]; > x = 1; // x -> 1 > x = klee_int(); // x -> var_0 > x = x + 1; // x-> var_0 + 1 (the read of x evaluates to var_0) > y[0] = x; // y -> [var_0 + 1, undef, undef, undef] > y[klee_int()] = 2; // y -> [var_0 + 1, undef, undef, undef] with var_1 = 2 > -- > > Given this, the solver never sees the stack or heap values; it only > sees the path constraints (the expressions from taken branches) and > the evaluated contents of expressions. > > Does that clarify things at all? > > - Daniel > > >> Thanks, >> Jonathan >> _______________________________________________ >> klee-dev mailing list >> klee-dev at keeda.stanford.edu >> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >> >> > >
