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

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

[Evan Zhao]

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?
Thanks in advance.

Best regards,
Evan
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

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

[Julia Lawall]

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

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

[Evan Zhao]

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

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

[Julia Lawall]

On Wed, 9 Jan 2019, Evan Zhao wrote:

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

free variables would be all metavariables referenced by a rule.
minus_free_vars would be the ones used in the matching part of the rule (-
annotated code or unannotated code).
nc means no constraint.  One can put a constraint on a metavariable, for
example to say that one position should be different than a previously
identified position.  The no constraint variables are the ones thatare
found directly on the matching code, and not in the constraints.

julia

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

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

[Evan Zhao]

Thank you for the clarification.

On Wed, Jan 9, 2019 at 4:50 PM Julia Lawall <julia.lawall@lip6.fr> wrote:
>
>
>
> On Wed, 9 Jan 2019, Evan Zhao wrote:
>
> > 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?
>
> free variables would be all metavariables referenced by a rule.
> minus_free_vars would be the ones used in the matching part of the rule (-
> annotated code or unannotated code).
> nc means no constraint.  One can put a constraint on a metavariable, for
> example to say that one position should be different than a previously
> identified position.  The no constraint variables are the ones thatare
> found directly on the matching code, and not in the constraints.
>
> julia
>
> >
> > 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