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

[Qixue Xiao]

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