Hi, Thanks for the additional information. You are right that if you don’t have the concrete values for symbolic data, the method that I proposed will not work. I was thinking that maybe you have something like seeds, where you can associate each index of symbolic array with the corresponding concrete value from the program input. ZESTI project has seeds functionality that makes it possible to replace symbolic values with the corresponding concrete values that you know from the program input. It evaluates expression and for every symbolic data that it knows the corresponding concrete value, it will replace it, so that the resulting expression may become a constant expression.
Hope that helps, Tomek > On 21 May 2015, at 15:46, Qixue Xiao <[email protected]> wrote: > > Hi, > > The failed situations, what I want to say, are timeout of solving a > query or a query (such as square root ) cannot be solved by current > solver. > when the solver cannot get a solution, it would return failed. and > KLEE will terminate the state early. > And what I want to do is make the state go on by replacing a concrete > value (from a seed). > >> If that is the case, one way to do it is to modify the >> Executor::executeMemoryOperation function in such a way that whenever you >> are about to read or write symbolic value, you replace it with a concrete >> one, so that in doesn’t further propagate into the program. > this method may not work, because when KLEE could not know which > symbolic value should be replace before solving. > or how to do it ? > > thanks > xqx > > > > > > > > > 2015-05-20 22:58 GMT+08:00 Kuchta, Tomasz <[email protected]>: >> Hi, >> >> When you say failed, do you mean that the branch was not feasible? >> If that is the case, it means that there are no such values in the program >> input that would make the program execute certain path. >> Or do you want to just replace symbolic data with concrete values? >> If that is the case, one way to do it is to modify the >> Executor::executeMemoryOperation function in such a way that whenever you >> are about to read or write symbolic value, you replace it with a concrete >> one, so that in doesn’t further propagate into the program. >> >> Hope that helps, >> Tomek >> >> >>> On 19 May 2015, at 16:48, Qixue Xiao <[email protected]> wrote: >>> >>> hi, >>> >>> when constraints are solved failed during symbolic execution, I want >>> to use concrete value (like seeds) to replace the related symbolic >>> value. So that the execution could continue. >>> >>> How could I use this feature in KLEE ? >>> >>> thanks. >>> >>> xqx >>> >>> _______________________________________________ >>> klee-dev mailing list >>> [email protected] >>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >>
<<attachment: winmail.dat>>
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
