James,
I don't see how you would do this without modifying KLEE because all path
constraints get passed to the solver. The FastCexSolver can simplify some
queries but it won't handle everything.
There is more than one way to solve this. The easiest seems to be creating a
new intrinsic to annotate the mutually exclusive ifs (plus the default) and
then in KLEE stop adding any constraints on the else paths of the annotated
code.
Paul
On 01/02/12 01:55, James Hongyi Zeng wrote:
> Thanks, Paul! In the example you given, a default rule can be added to
> catch !(c==1) && !(c==2). But it is a waste to consider !(c==1) in the
> (c==2) case since they can not be true at the same time.
>
> Here is a longer version: I have a long list of if-statements. Each
> statement contains a very complex expression. What I know is that at a
> given time, only one of them can be true (think of it as a switch
> statement). If I write it like this
>
> if(rule<1>) {Do 1}
> if(rule<2>)) {Do 2}
> ...
> if(rule<n>)) {Do n}
> {Do n+1}
>
> The generated STP queries will be
> 1: (rule<1>)
> 2: (rule<2>))&&(!rule<1>)
> ...
> n: (rule<n>)&&(!rule<1>)&&(!rule<2>)&&(!rule<3>)...&&(!rule<n-1>)
> default: (!rule<1>)&&(!rule<2>)&&(!rule<3>)...&&(!rule<n-1>)&&(!rule<n>)
>
> If fact, because they're mutually exclusive, hence no priority is
> implied. The STP queries can be
> 1: (rule<1>)
> 2: (rule<2>)
> ...
> n: (rule<n>)
> default: (!rule<1>)&&(!rule<2>)&&(!rule<3>)...&&(!rule<n-1>)&&(!rule<n>)
>
> The latter case will generate much shorter queries.
>
> Regards,
> James
>
>
> On Tue, Jan 31, 2012 at 5:38 PM, Paul Marinescu
> <[email protected] <mailto:[email protected]>>
> wrote:
>
> Hi James,
> It doesn't seem like what you're trying to do is sound. Take this
> slightly modified example:
>
> #include <klee/klee.h>
>
> void f(int c) {
> if(c==1) {printf("Do A\n");}
> if(c==2) {printf("Do B\n");}
> }
>
> int main() {
> int c;
> klee_make_symbolic(&c, sizeof(c), "input");
> klee_assume(c == 1 || c == 2);
> f(c);
> }
>
> If you don't consider !(c==1), you'll end up saying that a path
> which doesn't print anything is feasible. Perhaps you need to
> explain in more detail what you want to do.
>
> Paul
>
> On 31 Jan 2012, at 02:06, James Hongyi Zeng wrote:
>
> > Hi all,
> >
> > I am wondering whether I can explicitly tell KLEE that a set of
> if-statements are mutually exclusive. In the following example, KLEE
> generates 3 STP queries. Since c==2 and c==1 are mutually exclusive,
> I would like klee not to include !(c==1) in c==2 STP query. Is it
> possible?
> >
> > Thanks,
> > James
> >
> > #include <klee/klee.h>
> >
> > void f(int c) {
> > if(c==1) {printf("Do A\n");}
> > if(c==2) {printf("Do B\n");}
> > }
> >
> > int main() {
> > int c;
> > klee_make_symbolic(&c, sizeof(c), "input");
> > f(c);
> > }
> >
> >
> >
> > _______________________________________________
> > klee-dev mailing list
> > [email protected] <mailto:[email protected]>
> > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
>
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
