Re: [Cocci] A question about a part of a CTL formula

[Evan Zhao <tacingiht@gmail.com>]

Thank you for your quick response,

I am a beginner for model checking.
I having been reading your papers and implement code for a while,
there are some more questions, will you please to answer them too?

there are three free vars type, free_vars, minus_free_vars, and
minus_nc_free_vars.
By reading your paper, I know that free vars are used to manage the
metavariables, but
what does those three do respectively?

Thank you again.

On Wed, Jan 9, 2019 at 4:09 PM Julia Lawall <julia.lawall@lip6.fr> wrote:
>
>
>
> On Wed, 9 Jan 2019, Evan Zhao wrote:
>
> > Hi there,
> >
> > I am looking at a CTL formula generated by spatch with "--show-ctl-text",
> >
> > for example, for a cocci file like
> > @@
> > expression e,e1,e2;
> > @@
> >
> > if (e)
> > - GOTO(e1);
> > -else GOTO(e2);
> > + e1;
> > +else e2;
> >
> > it corresponding CTL formula is:
> >
> > CTL =
> > Let _r_0 = (EX^((TrueBranch v InLoop)) v EX^(EX^(FalseBranch))) in
> > ((_r_0 &
> > (Ex e1 .
> > ((Ex_ e . (Ex _v . if (e) )) &,
> > ((EX(FalseBranch) &, EX(After)) &,
> > ((EX((TrueBranch &, AX((Ex _v . GOTO(e1);)))) &,
> > EX((FalseBranch &,
> > AX(((Ex _v . else ) &, AX((Ex e2 . (Ex _v . GOTO(e2);))))))))
> > &, EX((After &, EX((Ex _v . _S1)))))))))
> > v
> > (!_r_0 &
> > (Ex e1 .
> > ((Ex_ e . if (e) ) &,
> > (EX(FalseBranch) &,
> > ((EX((TrueBranch &, AX((Ex _v . GOTO(e1);)))) &,
> > EX((FalseBranch &,
> > AX(((Ex _v . else ) &, AX((Ex e2 . (Ex _v . GOTO(e2);))))))))
> > &, EX(After)))))))
> >
> > and I noticed that
> > Let _r_0 = (EX^((TrueBranch v InLoop)) v EX^(EX^(FalseBranch))) in
> > is a fixed pattern, and I can track it at somewhere around the function of
> > do_between_dots in the module Asttoctl2, but I don't what it stands for.
> >
> > Cloud someone tell me what purpose it serves for?
>
> I think it is checking whether the added code is in an if branch in which
> case it wants to add {}.  I think that in your semantic patch it is not
> detecting that the then is just a replacement.  If this is what led you to
> look at the CTL in the first place, you may get a better result with
>
> if (e)
> - GOTO(
>   e1
> - )
>   ;
> else
> - GOTO(
>   e2
> - )
>   ;
>
> Then it should be able to see that the changes are just inside the
> existing branches, and so no {} adjustment is needed.
>
> julia
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci