[klee-dev] how to use concrete value to replace symbolic value when solving failed

[Kuchta, Tomasz]

Hi,

> On 21 May 2015, at 16:48, Qixue Xiao <s2exqx at gmail.com> wrote:
> 
> 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?
> 

The expression that’s returned by ZESTEvaluate will have all the reads from symbolic data replaced by concrete values, whenever
the corresponding value can be found in seeds. For example if the program is called with an input value x = 5 and then
x is made symbolic, in the expression we can still replace reads from x with the corresponding concrete value. It is used in the context of concolic 
execution: you run the program and make the input symbolic, but also try to follow the path that would have been executed if the input was concrete. 
To sum up, the potential difference between the expressions going into ZESTEvaluate and resulting from ZESTEvaluate is that the 
resulting expression might be constant, which means that we would not need to call solver.
An example of a situation when the resulting expression is not constant is when we don’t have seeds to replace reads from symbolic arrays.

> 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.
> 

If you use memset, what will happen is that if symdata was symbolic before calling memset on it, it will become concrete afterwards, if you
set the memory with concrete values.
Using klee_assume does not modify the memory contents - symdata is still symbolic, but in the path condition you will have these equality constraints
added (so if you ask the solver, it will be constrained when returning a value for symdata).


> third, I find KLEE is of a seed mode, and Does it use its seed mode to
> do the work like ZESTI?

Unfortunately I’m not familiar with seed mode in KLEE. As far as I know, ZESTI functionality is not available in the mainline KLEE.

> 
> Thanks again.
> 
> xqx
> 
> 

Best regards,
Tomek

> 
> 
> 
> 
> 2015-05-21 23:12 GMT+08:00 Kuchta, Tomasz <t.kuchta12 at imperial.ac.uk>:
>> 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 <s2exqx at gmail.com> 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 <t.kuchta12 at imperial.ac.uk>:
>>>> 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 <s2exqx at gmail.com> 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
>>>>> klee-dev at imperial.ac.uk
>>>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>>> 
>> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 6919 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150521/bfc1e83d/attachment.bin>