* [Cocci] A question about a part of a CTL formula @ 2019-01-09 8:02 Evan Zhao 2019-01-09 8:06 ` Julia Lawall 0 siblings, 1 reply; 5+ messages in thread From: Evan Zhao @ 2019-01-09 8:02 UTC (permalink / raw) To: cocci 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 ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [Cocci] A question about a part of a CTL formula 2019-01-09 8:02 [Cocci] A question about a part of a CTL formula Evan Zhao @ 2019-01-09 8:06 ` Julia Lawall 2019-01-09 8:44 ` Evan Zhao 0 siblings, 1 reply; 5+ messages in thread From: Julia Lawall @ 2019-01-09 8:06 UTC (permalink / raw) To: Evan Zhao; +Cc: cocci 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 ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [Cocci] A question about a part of a CTL formula 2019-01-09 8:06 ` Julia Lawall @ 2019-01-09 8:44 ` Evan Zhao 2019-01-09 8:50 ` Julia Lawall 0 siblings, 1 reply; 5+ messages in thread From: Evan Zhao @ 2019-01-09 8:44 UTC (permalink / raw) To: Julia Lawall; +Cc: cocci 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 ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [Cocci] A question about a part of a CTL formula 2019-01-09 8:44 ` Evan Zhao @ 2019-01-09 8:50 ` Julia Lawall 2019-01-09 8:58 ` Evan Zhao 0 siblings, 1 reply; 5+ messages in thread From: Julia Lawall @ 2019-01-09 8:50 UTC (permalink / raw) To: Evan Zhao; +Cc: cocci 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 ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [Cocci] A question about a part of a CTL formula 2019-01-09 8:50 ` Julia Lawall @ 2019-01-09 8:58 ` Evan Zhao 0 siblings, 0 replies; 5+ messages in thread From: Evan Zhao @ 2019-01-09 8:58 UTC (permalink / raw) To: Julia Lawall; +Cc: cocci 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 ^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2019-01-09 8:58 UTC | newest] Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2019-01-09 8:02 [Cocci] A question about a part of a CTL formula Evan Zhao 2019-01-09 8:06 ` Julia Lawall 2019-01-09 8:44 ` Evan Zhao 2019-01-09 8:50 ` Julia Lawall 2019-01-09 8:58 ` Evan Zhao
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).