[cocci] [RFC] Choosing “semantics” better for SmPL script parts?

[cocci] [RFC] Choosing “semantics” better for SmPL script parts?

[Markus Elfring]

Hello,

A bit of information is provided about special “semantics” (also in the manual
for the semantic patch language).
https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/face14907c0791b93397d5788d2a94c7c6a4b886/docs/manual/cocci_syntax.tex#L1007-1014

Usage possibilities are indicated for the key words “exists” and “forall”.

* Would any more software users like to discuss and clarify safer applications
  of these system configuration parameters?

* Would you be looking for better “connections” according to computation tree
  logic (or linear temporal logic) variations?


Regards,
Markus

Re: [cocci] [RFC] Choosing “semantics” better for SmPL script parts?

[Markus Elfring]

> A bit of information is provided about special “semantics” (also in the manual
> for the semantic patch language).

The usage of the semantic match functionality influences which default semantics
should be applied for the evaluation of an SmPL rule.
I imagine that the corresponding data processing can become more interesting
when the needed semantics would actually be the opposite setting.

* Do you tend to look for the existence of selected implementation details
  more than that source code variants can occur on all executions paths
  according to evolving control flows?

* Would you expect to use the source code search parameter “exists” more often
  then “forall”?


Regards,
Markus

Re: [cocci] [RFC] Choosing “semantics” better for SmPL script parts?

[Julia Lawall]

[-- Attachment #1: Type: text/plain, Size: 1069 bytes --]



On Mon, 25 Aug 2025, Markus Elfring wrote:

> > A bit of information is provided about special “semantics” (also in the manual
> > for the semantic patch language).
>
> The usage of the semantic match functionality influences which default semantics
> should be applied for the evaluation of an SmPL rule.
> I imagine that the corresponding data processing can become more interesting
> when the needed semantics would actually be the opposite setting.
>
> * Do you tend to look for the existence of selected implementation details
>   more than that source code variants can occur on all executions paths
>   according to evolving control flows?
>
> * Would you expect to use the source code search parameter “exists” more often
>   then “forall”?

The default is exists for use with * and forall with transformation, with
the reasoning for the latter being that when transformation occurs the
trasformed code should be consistent.  But there are cases where something
else is desired, so this is controlled by the user.

julia

>
>
> Regards,
> Markus
>

Re: [cocci] [RFC] Choosing “semantics” better for SmPL script parts?

[Markus Elfring]

> The default is exists for use with * and forall with transformation, with
> the reasoning for the latter being that when transformation occurs the
> trasformed code should be consistent.  But there are cases where something
> else is desired, so this is controlled by the user.

Can SmPL script developers occasionally get any indications that they would expect
an opposite system setting?

Will the usage incidence become more interesting for the mentioned source code
search parameter?

Regards,
Markus

Re: [cocci] [RFC] Choosing “semantics” better for SmPL script parts?

[Markus Elfring]

> The default is exists for use with * and forall with transformation, with
> the reasoning for the latter being that when transformation occurs the
> trasformed code should be consistent.

Will corresponding development concerns be reconsidered in more detail?

Would you understand the source code search parameter “forall” in the way
that it expresses a stronger data processing requirement (than the setting
alternative “exists”)?
https://en.wikipedia.org/wiki/Universal_quantification

Is it known if such a quantification difference would influence software
run time characteristics in significant ways?

Regards,
Markus