Thanks David. I've been working around and hooking into some parts of KLEE. Seems like KLEE randomizes the symbolic string from the start of execution. At each function call, all arguments are concrete, for example what I got from strcmp(x, y) operator (x is symbolic): strcmp
ARGUMENT 0/2 = 54242560 Type = Constant Width = 64 ZExtValue Value = 54242560 ARGUMENT 1/2 = 54209552 Type = Constant Width = 64 ZExtValue Value = 54209552 Of course for Integer variable, KLEE maintains the symbolic property. For the function get_sign(int a): get_sign ARGUMENT 0/1 = (ReadLSB w32 0 a) So what I want now is to track the symbolic property of each variable. For example, if we have x is symbolic string and s = x + "123", then s is marked as symbolic and I want to store the relationship s = x + "123" also. Which part of KLEE should I start working on? Thank you, On Tue, Oct 29, 2013 at 6:06 PM, DAVID LIGHTSTONE < [email protected]> wrote: > I suspect not always. The reason being that the involving call may not be > on the stack. > Quite likely the library call will be somewhere between two KLEE branch > fork invocations. > > For your example where the involving call is in the conditional, the > answer is yes. > > This suggests that the library will need to be modified so as to output to > a trace file the argument lists that you wish to capture ; A lot of work. > The effort has a definite recursion to avoid; the various print procedures > use the library also > > There are code translation systems such as ROSE which probably can > automate the modification effort, but there is a nontrivial effort needed > to learn them. > > Dave Lightstone > > ------------------------------ > * From: * Loi Luu <[email protected]>; > * To: * DAVID LIGHTSTONE <[email protected]>; > * Cc: * klee-dev <[email protected]>; > * Subject: * Re: [klee-dev] Collect functions and values of parameters > * Sent: * Tue, Oct 29, 2013 2:20:27 AM > > Thank you David. Are we able to query the values of parameters in each > function call by KLEE? Using the line numbers generated by KLEE to identify > the invokes tree is easy, but to get the parameter values parsed into each > function I'm not sure. > > Regards, > > > On Tue, Oct 29, 2013 at 2:29 AM, DAVID LIGHTSTONE < > [email protected]> wrote: > >> Sorry, I used the wrong nomenclature >> >> It's not a call tree, rather it is the tree created when Klee invokes fork >> >> ------------------------------ >> * From: * DAVID LIGHTSTONE <[email protected]>; >> * To: * Loi Luu <[email protected]>; <[email protected]>; >> * Subject: * Re: [klee-dev] Collect functions and values of parameters >> * Sent: * Mon, Oct 28, 2013 6:01:09 PM >> >> Take a look at your favorite debugger. Ask the question - how does it >> figure the call tree? >> >> When KLEE writes out the test case, walk the call tree in the same >> fashion as the debugger until you get to main. >> >> You probably need a debug version of the code to get the symbols needed >> to play this game, but it should work. Use the line numbers to identify the >> branch locations, there may not be symbols at those locations >> >> Dave Lightstone >> >> ------------------------------ >> * From: * Loi Luu <[email protected]>; >> * To: * klee-dev <[email protected]>; >> * Subject: * Re: [klee-dev] Collect functions and values of parameters >> * Sent: * Mon, Oct 28, 2013 4:34:20 PM >> >> I posted this question on StackOverflow with an illustrating example >> http://stackoverflow.com/questions/19634022/program-analysis-with-given-input >> >> Thanks, >> >> >> On Mon, Oct 28, 2013 at 6:54 PM, Loi Luu <[email protected]> wrote: >> >>> Hi, >>> >>> Given a program path, I wanna track all libc functions (in path >>> condition) with their corresponding parameters in each execution path. For >>> example, given the branch condition if (strcmp(s, s1)) in which s is >>> symbolic, s1 is concrete; I wanna get the function name (strcmp), the value >>> of s1 and the return value of this function. Which part of KLEE should I >>> modify to get it stored in each execution state and printed in somewhere >>> like .pc file. >>> >>> Thanks, >>> >>> -- >>> Loi, Luu The (Mr.) >>> RA at Security Lab, SoC, NUS >>> >> >> >> >> -- >> Loi, Luu The (Mr.) >> RA at Security Lab, SoC, NUS >> > > > > -- > Loi, Luu The (Mr.) > RA at Security Lab, SoC, NUS > -- Loi, Luu The (Mr.) RA at Security Lab, SoC, NUS
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
