Hi， Thanks for your detailed reply. I have done some tests with ZESTI some time ago, but I found it also can not work well when solving some complex queries. I think that it would evaluates expression before solving, but the evaluation maybe not work.
I am not sure it and I have some questions about ZESTI. first, ZESTI use "(seedinfo)->assignment.evaluate(expr)" to evaluate an expr in ZESTEvaluate, which is called before solving. But It also returns an expression . What the difference between the expression before calling ZESTEvaluate? second, I found there two methods to fill the concrete value: using memset or klee_assume. I thought the first one would use the concrete value directly, and the second one would add an expression in query, such as "symdata==A". Why it provides 2 methods? I think the first method is better in theory. third, I find KLEE is of a seed mode, and Does it use its seed mode to do the work like ZESTI? Thanks again. xqx 2015-05-21 23:12 GMT+08:00 Kuchta, Tomasz <[email protected]>: > 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 >>> > _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
