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 >
