Hi Heinz,
You may find our paper "Execution Synthesis: A Technique for Automated Software
Debugging" http://dslab.epfl.ch/pubs/esd of interest in this regard.
From what I understand, in your case you may be able to statically decide if a
given execution state is still able to reach a given line in the code. Once you
find an execution with property #1, you may be able to use some simple control
flow static analysis to discard all other states from which property #1 is
reachable, assuming that the properties are mutually exclusive.
Cristi
On May 15, 2010, at 7:27 PM, Daniel Dunbar wrote:
> Unfortunately no. KLEE has no way to limit it's search to paths which (will
> eventually) satisfy the predicates.
>
> Ideally a very smart search strategy would handle this automatically as part
> of trying to get code coverage, but it is a very hard problem.
>
> - Daniel
>
>
> On Apr 28, 2010, at 6:02, Heinz Riener <hriener at student.tugraz.at> wrote:
>
>> Dear all,
>>
>> Currently I'm using KLEE to check whether a program fulfills certain
>> properties. Consider the following pseudo code example, where f is a
>> function and p1, p2, and p3 are predicates using global variables or
>> values returned from f.
>>
>> // a very large program
>> f(/* symbolic args */);
>>
>> // predicate checks
>> if (p1) {
>> printf("Property #1 satisfied.");
>> }
>> if (p2) {
>> printf("Property #2 satisfied.");
>> }
>> if (p3) {
>> printf("Property #3 satisfied.");
>> }
>>
>> The properties are exclusive such that only one property is true at a
>> time. I'm only interested if there is one path that fulfills property
>> p1, one path that fulfills property p2 and one path that fulfills
>> property p3. However, KLEE searches for all feasible execution paths
>> and thus fulfills each property multiple times, which is a huge
>> computational waste in my case. I'm looking for a way to tell KLEE that
>> each property should be checked only once.
>>
>> Is there some kind of KLEE instrumentation trick that could assist me?
>> Can you give me some other advice to make my search task more efficient?
>>
>> Regards,
>> Heinz
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at keeda.stanford.edu
>> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
