[Cocci] [PATCH v2 0/3] coccinelle: add control flow docs and demos

[Cocci] [PATCH v2 0/3] coccinelle: add control flow docs and demos

[Luis R. Rodriguez]

This v2 addresses the typos and issues from the RFC. This also
adds some "depends on" documentation at the end of the control
flow section as well.

Luis R. Rodriguez (3):
  tests: add test to remove single statement from branch
  demos: add basic series of demos for exists and forall
  coccinelle: add control flow documentation

 demos/exists1.c                    |  20 +++
 demos/exists1.cocci                |   9 ++
 demos/exists1.res                  |  21 +++
 demos/exists2.c                    |  21 +++
 demos/exists2.cocci                |  13 ++
 demos/exists2.res                  |  23 ++++
 demos/exists3.c                    |  21 +++
 demos/exists3.cocci                |  12 ++
 demos/exists3.res                  |  23 ++++
 demos/exists4.c                    |  22 ++++
 demos/exists4.cocci                |  13 ++
 demos/exists4.res                  |  21 +++
 docs/manual/Makefile               |   6 +-
 docs/manual/cocci_syntax.tex       | 257 +++++++++++++++++++++++++++++++++++++
 docs/manual/flow1.c                |  10 ++
 docs/manual/flow2.c                |  11 ++
 tests/remove-code-in-branch1.c     |   7 +
 tests/remove-code-in-branch1.cocci |   4 +
 tests/remove-code-in-branch1.res   |   7 +
 19 files changed, 520 insertions(+), 1 deletion(-)
 create mode 100644 demos/exists1.c
 create mode 100644 demos/exists1.cocci
 create mode 100644 demos/exists1.res
 create mode 100644 demos/exists2.c
 create mode 100644 demos/exists2.cocci
 create mode 100644 demos/exists2.res
 create mode 100644 demos/exists3.c
 create mode 100644 demos/exists3.cocci
 create mode 100644 demos/exists3.res
 create mode 100644 demos/exists4.c
 create mode 100644 demos/exists4.cocci
 create mode 100644 demos/exists4.res
 create mode 100644 docs/manual/flow1.c
 create mode 100644 docs/manual/flow2.c
 create mode 100644 tests/remove-code-in-branch1.c
 create mode 100644 tests/remove-code-in-branch1.cocci
 create mode 100644 tests/remove-code-in-branch1.res

-- 
2.7.2

[Cocci] [PATCH v2 1/3] tests: add test to remove single statement from branch

[Luis R. Rodriguez]

At leaset with coccinelle 1.0.4 this test fails with
two issues, one is the return statement is shifted,
another is debatable -- an empty branch statement is
left. This is funtional however its debatable if this
is desirable by default.

v2: do not remove the if -- the if is needed as the items
    in the branch could consist of functional run time
    changes, for instance if (bar()).

Signed-off-by: Luis R. Rodriguez <mcgrof@kernel.org>
---
 tests/remove-code-in-branch1.c     | 7 +++++++
 tests/remove-code-in-branch1.cocci | 4 ++++
 tests/remove-code-in-branch1.res   | 7 +++++++
 3 files changed, 18 insertions(+)
 create mode 100644 tests/remove-code-in-branch1.c
 create mode 100644 tests/remove-code-in-branch1.cocci
 create mode 100644 tests/remove-code-in-branch1.res

diff --git a/tests/remove-code-in-branch1.c b/tests/remove-code-in-branch1.c
new file mode 100644
index 000000000000..83840bdd99ac
--- /dev/null
+++ b/tests/remove-code-in-branch1.c
@@ -0,0 +1,7 @@
+int main(void)
+{
+	if (a > 1)
+		c();
+
+	return 0;
+}
diff --git a/tests/remove-code-in-branch1.cocci b/tests/remove-code-in-branch1.cocci
new file mode 100644
index 000000000000..b3f03523ac92
--- /dev/null
+++ b/tests/remove-code-in-branch1.cocci
@@ -0,0 +1,4 @@
+ at r@
+@@
+
+-c();
diff --git a/tests/remove-code-in-branch1.res b/tests/remove-code-in-branch1.res
new file mode 100644
index 000000000000..eb7985f683a0
--- /dev/null
+++ b/tests/remove-code-in-branch1.res
@@ -0,0 +1,7 @@
+int main(void)
+{
+	if (a > 1)
+		{}
+
+	return 0;
+}
-- 
2.7.2

[Cocci] [PATCH v2 2/3] demos: add basic series of demos for exists and forall

[Luis R. Rodriguez]

This should not ony help test but also demo use of exists
and forall.

Signed-off-by: Luis R. Rodriguez <mcgrof@kernel.org>
---
 demos/exists1.c     | 20 ++++++++++++++++++++
 demos/exists1.cocci |  9 +++++++++
 demos/exists1.res   | 21 +++++++++++++++++++++
 demos/exists2.c     | 21 +++++++++++++++++++++
 demos/exists2.cocci | 13 +++++++++++++
 demos/exists2.res   | 23 +++++++++++++++++++++++
 demos/exists3.c     | 21 +++++++++++++++++++++
 demos/exists3.cocci | 12 ++++++++++++
 demos/exists3.res   | 23 +++++++++++++++++++++++
 demos/exists4.c     | 22 ++++++++++++++++++++++
 demos/exists4.cocci | 13 +++++++++++++
 demos/exists4.res   | 21 +++++++++++++++++++++
 12 files changed, 219 insertions(+)
 create mode 100644 demos/exists1.c
 create mode 100644 demos/exists1.cocci
 create mode 100644 demos/exists1.res
 create mode 100644 demos/exists2.c
 create mode 100644 demos/exists2.cocci
 create mode 100644 demos/exists2.res
 create mode 100644 demos/exists3.c
 create mode 100644 demos/exists3.cocci
 create mode 100644 demos/exists3.res
 create mode 100644 demos/exists4.c
 create mode 100644 demos/exists4.cocci
 create mode 100644 demos/exists4.res

diff --git a/demos/exists1.c b/demos/exists1.c
new file mode 100644
index 000000000000..5cc37415bfef
--- /dev/null
+++ b/demos/exists1.c
@@ -0,0 +1,20 @@
+void bar(void)
+{
+	int a;
+
+	a = 300;
+	b();
+}
+
+int main(void)
+{
+	int a;
+
+	a = 10;
+	b();
+
+	c = 400;
+	c();
+
+	return 0;
+}
diff --git a/demos/exists1.cocci b/demos/exists1.cocci
new file mode 100644
index 000000000000..af95363de18f
--- /dev/null
+++ b/demos/exists1.cocci
@@ -0,0 +1,9 @@
+// this rule lacks exists, without exists, all control flows possible
+// must match the rule when + or - is used. In the case of exists1.c only
+// one possible control flow exists, the flow is completely linear.
+ at r@
+@@
+
+b();
+...
+-c();
diff --git a/demos/exists1.res b/demos/exists1.res
new file mode 100644
index 000000000000..cd83e4b2b6b1
--- /dev/null
+++ b/demos/exists1.res
@@ -0,0 +1,21 @@
+#include <stdio.h>
+
+int bar(void)
+{
+	int a;
+
+	a = 300;
+	b();
+}
+
+int main(void)
+{
+	int a;
+
+	a = 10;
+	b();
+
+	c = 400;
+
+	return 0;
+}
diff --git a/demos/exists2.c b/demos/exists2.c
new file mode 100644
index 000000000000..486a8f5633d9
--- /dev/null
+++ b/demos/exists2.c
@@ -0,0 +1,21 @@
+void bar(void)
+{
+	int a;
+
+	a = 300;
+	b();
+}
+
+int main(void)
+{
+	int a;
+
+	a = 10;
+	b();
+
+	c = 400;
+	if (a > 5)
+		c();
+
+	return 0;
+}
diff --git a/demos/exists2.cocci b/demos/exists2.cocci
new file mode 100644
index 000000000000..576b3cd3af24
--- /dev/null
+++ b/demos/exists2.cocci
@@ -0,0 +1,13 @@
+// this rule lacks exists, without exists, all control flows possible
+// must match the rule. In the case of exists2.c two possible control
+// flows exists on main():
+// 1. b() --> a > 5 --> c();
+// 2. b() --> a <= 5 ---> no c();
+// Not all control flows match, so no changes are made.
+// To visualize the control graph use: spatch --control-flow exists2.c
+ at r@
+@@
+
+b();
+...
+-c();
diff --git a/demos/exists2.res b/demos/exists2.res
new file mode 100644
index 000000000000..9d6401eb7d05
--- /dev/null
+++ b/demos/exists2.res
@@ -0,0 +1,23 @@
+#include <stdio.h>
+
+int bar(void)
+{
+	int a;
+
+	a = 300;
+	b();
+}
+
+int main(void)
+{
+	int a;
+
+	a = 10;
+	b();
+
+	c = 400;
+	if (a > 5)
+		c();
+
+	return 0;
+}
diff --git a/demos/exists3.c b/demos/exists3.c
new file mode 100644
index 000000000000..486a8f5633d9
--- /dev/null
+++ b/demos/exists3.c
@@ -0,0 +1,21 @@
+void bar(void)
+{
+	int a;
+
+	a = 300;
+	b();
+}
+
+int main(void)
+{
+	int a;
+
+	a = 10;
+	b();
+
+	c = 400;
+	if (a > 5)
+		c();
+
+	return 0;
+}
diff --git a/demos/exists3.cocci b/demos/exists3.cocci
new file mode 100644
index 000000000000..64cb43aa8ec4
--- /dev/null
+++ b/demos/exists3.cocci
@@ -0,0 +1,12 @@
+// this rule uses exists, with it, the rule is successful if at least
+// one of the possible control flows possible match.
+// exists3.c has two possible control flows on main():
+// 1. b() --> a > 5 --> c();
+// 2. b() --> a <= 5 ---> no c();
+// The match on 1. enables the changes to take place.
+ at r exists @
+@@
+
+b();
+...
+-c();
diff --git a/demos/exists3.res b/demos/exists3.res
new file mode 100644
index 000000000000..f6b53c361fa5
--- /dev/null
+++ b/demos/exists3.res
@@ -0,0 +1,23 @@
+#include <stdio.h>
+
+int bar(void)
+{
+	int a;
+
+	a = 300;
+	b();
+}
+
+int main(void)
+{
+	int a;
+
+	a = 10;
+	b();
+
+	c = 400;
+	if (a > 5)
+		{}
+
+	return 0;
+}
diff --git a/demos/exists4.c b/demos/exists4.c
new file mode 100644
index 000000000000..0b3dab08e6e1
--- /dev/null
+++ b/demos/exists4.c
@@ -0,0 +1,22 @@
+void bar(void)
+{
+	int a;
+
+	a = 300;
+	b();
+	c();
+}
+
+int main(void)
+{
+	int a;
+
+	a = 10;
+	b();
+
+	c = 400;
+	if (a > 5)
+		c();
+
+	return 0;
+}
diff --git a/demos/exists4.cocci b/demos/exists4.cocci
new file mode 100644
index 000000000000..d80c71a9d3f3
--- /dev/null
+++ b/demos/exists4.cocci
@@ -0,0 +1,13 @@
+// this rule uses forall, with it, all control flows must match.
+//
+// The exists4.c was extended to add a c() in comparison to exists2.c
+// this is done to show that using forall will still have an effect
+// on bar() even though it does not match on main()
+//
+// This is the default behaviour when + or - is used as well.
+ at r forall@
+@@
+
+b();
+...
+-c();
diff --git a/demos/exists4.res b/demos/exists4.res
new file mode 100644
index 000000000000..486a8f5633d9
--- /dev/null
+++ b/demos/exists4.res
@@ -0,0 +1,21 @@
+void bar(void)
+{
+	int a;
+
+	a = 300;
+	b();
+}
+
+int main(void)
+{
+	int a;
+
+	a = 10;
+	b();
+
+	c = 400;
+	if (a > 5)
+		c();
+
+	return 0;
+}
-- 
2.7.2

[Cocci] [PATCH v2 3/3] coccinelle: add control flow documentation

[Luis R. Rodriguez]

From: "Luis R. Rodriguez" <mcgrof@suse.com>

Add control flow documentation.

v2: fix typos, add "depends on" documentation in control flow
    section as well.

Signed-off-by: Luis R. Rodriguez <mcgrof@suse.com>
---
 docs/manual/Makefile         |   6 +-
 docs/manual/cocci_syntax.tex | 257 +++++++++++++++++++++++++++++++++++++++++++
 docs/manual/flow1.c          |  10 ++
 docs/manual/flow2.c          |  11 ++
 4 files changed, 283 insertions(+), 1 deletion(-)
 create mode 100644 docs/manual/flow1.c
 create mode 100644 docs/manual/flow2.c

diff --git a/docs/manual/Makefile b/docs/manual/Makefile
index 98e397ac5b69..0cfe817cdc4e 100644
--- a/docs/manual/Makefile
+++ b/docs/manual/Makefile
@@ -36,7 +36,11 @@ manual.pdf: $(SRC)
 	$(PDFLATEX_CMD) manual.tex
 	$(PDFLATEX_CMD) manual.tex
 
-main_grammar.pdf: main_grammar.tex cocci_syntax.tex  macros_listing_cocci.tex macros_grammar.tex macros_common.tex examples.tex tips.tex
+main_grammar.pdf: main_grammar.tex cocci_syntax.tex flow1.c flow2.c macros_listing_cocci.tex macros_grammar.tex macros_common.tex examples.tex tips.tex
+	#spatch --control-flow-to-file flow1.c
+	#spatch --control-flow-to-file flow2.c
+	#dot -Gsize="0.5,0.5" -Tpdf flow1:main.dot > flow1.pdf
+	#dot -Gsize="0.5,0.5" -Tpdf flow2:main.dot > flow2.pdf
 	$(PDFLATEX_CMD) main_grammar.tex
 	$(PDFLATEX_CMD) main_grammar.tex
 
diff --git a/docs/manual/cocci_syntax.tex b/docs/manual/cocci_syntax.tex
index 2c0f622251f6..b62540da7093 100644
--- a/docs/manual/cocci_syntax.tex
+++ b/docs/manual/cocci_syntax.tex
@@ -584,6 +584,263 @@ rule is only applied if all of the metavariables for which there are no
 default values have values.  See demos/defaultscript.cocci for examples of
 the use of this feature.
 
+\section{Control Flow}
+
+Rules describe a property which Coccinelle must match, when the property
+described is matched the rule is considered successful. Program control
+flows vary, a control flow describes a possible run time path taken by
+a program.
+
+When using Coccinelle you often want to be able to express certain code
+within certain types of control flows. Typically you will use ellipses
+("...") to indicate to Coccinelle anything can be present between
+consecutive statements. For instance the following SmPL patch tells Coccinelle
+that rule r0 wishes to remove call calls to function c().
+
+\begin{center}
+\begin{tabular}{c}
+\begin{lstlisting}[language=Cocci]
+ at r0@
+@@
+
+-c();
+
+\end{lstlisting}\\
+\end{tabular}
+\end{center}
+
+The context of the rule provides no other guidlines to Coccinelle to hint
+about any possible control flow other than this is a statement, and that
+c() must be called. We can modify the required control flow required for
+this rule by providing additional requirements and using ellipses in between.
+For instance, if we only wanted to remove call calls to c() but which also
+had a prior call to foo() we'd use the following SmPL patch:
+
+\begin{center}
+\begin{tabular}{c}
+\begin{lstlisting}[language=Cocci]
+ at r1@
+@@
+
+foo()
+...
+-c();
+\end{lstlisting}\\
+\end{tabular}
+\end{center}
+
+There are two possible modifiers to the control flow for ellipses, one
+is to annotate that statements in between ellipses are optional (<... ...>),
+or that the statements in between must be present at least once (<+... ...+).
+For instance the following SmPL patch tells Coccinelle to remove all
+calls to c() but foo() must be present at least once.
+
+\begin{center}
+\begin{tabular}{c}
+\begin{lstlisting}[language=Cocci]
+@r2@
+@@
+
+<+...
+foo()
+...+>
+-c();
+
+\end{lstlisting}\\
+\end{tabular}
+\end{center}
+
+Alternatively, if you wanted to be explicit that foo() was optional,
+you could use the following SmPL rule.
+
+\begin{center}
+\begin{tabular}{c}
+\begin{lstlisting}[language=Cocci]
+ at r3@
+@@
+
+<...
+foo()
+...>
+-c();
+
+\end{lstlisting}\\
+\end{tabular}
+\end{center}
+
+Let's consider some sample code to review, this is flow1.c.
+
+\begin{center}
+\begin{tabular}{c}
+\begin{lstlisting}[language=C]
+
+int main(void)
+{
+	int ret, a = 2;
+
+	a = foo(a);
+	ret = bar(a);
+	c();
+
+	return ret;
+}
+\end{lstlisting}\\
+\end{tabular}
+\end{center}
+
+Applying the SmPL rule r0 to flow1.c would remove the c() line as the control
+flow provides no specific context requirements. Applying rule r1 would also
+succeed as the call to foo() is present. Likewise rules r2 and r3 would also
+succeed. If the foo() call is removed from flow1.c only rules r0 and r3 would
+succeed, as foo() would not be present and only rules r0 and r3 allow for
+foo() to not be present.
+
+The program flow1.1 has a linear control flow, it has no branches. The main
+routine has a McCabe cyclomatic complexity of 1. The McCabe cyclomatic
+complexity can be computed using
+{\tt pmccabe} (https://www.gnu.org/software/complexity/manual/html\_node/pmccabe-parsing.html).
+
+\begin{center}
+\begin{tabular}{c}
+\begin{lstlisting}[language=C]
+pmccabe /flow1.c
+1       1       5       1       10      flow1.c(1): main
+\end{lstlisting}\\
+\end{tabular}
+\end{center}
+
+Since programs can use branches, often times you may also wish to annotate
+requirements for control flows in consideration for branches, for when
+the McCabe cyclomatic complexity is > 1. The following program, flow2.c,
+enables the control flow to diverge on line 7 due to the branch, if (a) --
+one control flow possible is if (a) is true, another when if (a) is false.
+
+\begin{center}
+\begin{tabular}{c}
+\begin{lstlisting}[language=C]
+int main(void)
+{
+	int ret, a = 2;
+
+	a = foo(a);
+	ret = bar(a);
+	if (a)
+		c();
+
+	return ret;
+}
+\end{lstlisting}\\
+\end{tabular}
+\end{center}
+
+This program has a McCabe cyclomatic complexity of 2.
+
+\begin{center}
+\begin{tabular}{c}
+\begin{lstlisting}[language=C]
+pmccabe flow2.c
+2       2       6       1       11      flow2.c(1): main
+\end{lstlisting}\\
+\end{tabular}
+\end{center}
+
+Using the McCabe cyclomatic complexity is one way to get an idea of
+the complexity of the control graph for a function, another way is
+to visualize all possible paths. Coccinelle provides a way to visualize
+control flows of programs, this however requires {\tt dot}
+(http://www.graphviz.org/) and {\tt gv} to be installed (typically provided
+by a package called graphviz). To visualize control flow or a program
+using Coccinelle you use:
+
+\begin{center}
+\begin{tabular}{c}
+spatch --control-flow-to-file flow1.c
+spatch --control-flow-to-file flow2.c
+\end{tabular}
+\end{center}
+
+%Below are the two generated control flow graphs for flow1.c and flow2.c
+%respectively.
+
+%\begin{figure}
+%	\[\includegraphics[width=\linewidth]{flow1.pdf}\]
+%	\caption{Linear flow example}
+%	\label{devmodel}
+%\end{figure}
+
+%\begin{figure}
+%	\[\includegraphics[width=\linewidth]{flow2.pdf}\]
+%	\caption{Linear flow example}
+%	\label{devmodel}
+%\end{figure}
+
+Behind the scenes this generates a dot file and uses gv to generate
+a PDF file for viewing. To generate and inspect these manually you
+can use the following:
+
+\begin{center}
+\begin{tabular}{c}
+spatch --control-flow-to-file flow2.c
+dot -Tpdf flow1:main.dot > flow1.pdf
+\end{tabular}
+\end{center}
+
+By default properties described in a rule must match all control
+flows possible within a code section being inspected by Coccinelle.
+So for instance, in the following SmPL patch rule r1 would match all
+the control flow possible on flow1.c as its linear, however it would
+not match the control possible on flow2.c. The rule r1 would not
+be successful in flow2.c
+
+\begin{center}
+\begin{tabular}{c}
+\begin{lstlisting}[language=Cocci]
+ at r1@
+@@
+
+foo()
+...
+-c();
+
+\end{lstlisting}\\
+\end{tabular}
+\end{center}
+
+The default control flow can be modified by using the keyword "exists"
+following the rule name. In the following SmPL patch the rule r2 would
+be successful on both flow1.c and flow2.c
+
+\begin{center}
+\begin{tabular}{c}
+\begin{lstlisting}[language=Cocci]
+ at r2 exists@
+@@
+
+foo()
+...
+-c();
+
+\end{lstlisting}\\
+\end{tabular}
+\end{center}
+
+If the rule is followed by the "forall" keyword, then all control flow
+paths must match in order for the rule to succeed. By default when one
+has "-" and "+", or when one has no annotations at all and only script
+code, ellipses ("...") uses the forall semantics.  And when one uses
+context annotation ("*"), the ellipses ("...") uses the exists semantics.
+Using the keyword "forall" or "exists" in the rule header affects
+all ellipses ("...") uses in the rule. You can also annotate each
+ellipses ("...") with "when exists" or "when forall" individually.
+
+Rules can also be not be successful if requirements do not match
+when a rule name is followed by "depends on XXX". When "depends on is used
+it means the rule should only apply if rule XXX matched with the current
+metavariable environment. Alternatively, "depends on ever XXX" can be used
+as well, this means this rule should apply if rule XXX was ever matched at
+all. A counter to this use is "depends on never XXX", which means that this
+rule should apply if rule XXX was never matched at all.
+
 \section{Transformation}
 
 The transformation specification essentially has the form of C code, except
diff --git a/docs/manual/flow1.c b/docs/manual/flow1.c
new file mode 100644
index 000000000000..43e45ed32843
--- /dev/null
+++ b/docs/manual/flow1.c
@@ -0,0 +1,10 @@
+int main(void)
+{
+	int ret, a = 2;
+
+	a = foo(a);
+	ret = bar(a);
+	c();
+
+	return ret;
+}
diff --git a/docs/manual/flow2.c b/docs/manual/flow2.c
new file mode 100644
index 000000000000..bb0d95e4c310
--- /dev/null
+++ b/docs/manual/flow2.c
@@ -0,0 +1,11 @@
+int main(void)
+{
+	int ret, a = 2;
+
+	a = foo(a);
+	ret = bar(a);
+	if (a)
+		c();
+
+	return ret;
+}
-- 
2.7.2

[Cocci] [PATCH v2 3/3] coccinelle: add control flow documentation

[SF Markus Elfring]

> +	#spatch --control-flow-to-file flow1.c

Do you really want to add such commands as comment lines of this make file?


> +Rules describe a property which Coccinelle must match, when the property
> +described is matched the rule is considered successful. Program control
> +flows vary, a control flow describes a possible run time path taken by
> +a program.

How do you think about an other wording?

+ ? match.
+ A rule is considered successful when the described property is matched.
+ Properties belong to varying program control flows.
+ A control flow describes a possible run time path taken by a program.


> +When using Coccinelle you often want to be able to express certain code
> +within certain types of control flows. Typically you will use ellipses
> +("...") to indicate to Coccinelle anything can be present between
> +consecutive statements.

Another alternative?

+ ? flows.
+ You would like to use placeholders at some places usually.
+ Typically you will use ellipses ("...") for the indication
+ that any source code can be present between consecutive statements.


> +The context of the rule provides no other guidlines to Coccinelle to hint

Do involved guidelines need another fix?


> +For instance, if we only wanted to remove call calls to c() but which also

Is the "call" mentioned too often here?


> +There are two possible modifiers to the control flow for ellipses, one
> +is to annotate that statements in between ellipses are optional (<... ...>),

Will it be better to use an enumeration (with bullet points)?


> +or that the statements in between must be present at least once (<+... ...+).

Would you like to add a closing angle bracket here?


> +The program flow1.1 has a linear control flow, it has no branches. The main
> +routine has a McCabe cyclomatic complexity of 1. The McCabe cyclomatic
> +complexity can be computed using

Another description approach?

+ ? branches.
+ Each flow can also be categorised by the metric "McCabe cyclomatic complexity"
+ which can be computed ? .


> +Rules can also be not be successful if requirements do not match
> +when a rule name is followed by "depends on XXX". When "depends on is used

More fine-tuning?

+ The match success is also affected by the rule dependency specification.
+ When "depends on" is used


> +it means the rule should only apply if rule XXX matched with the current
> +metavariable environment. Alternatively, "depends on ever XXX" can be used
> +as well, this means this rule should apply if rule XXX was ever matched at
> +all. A counter to this use is "depends on never XXX", which means that this
> +rule should apply if rule XXX was never matched at all.

Other enumeration format?

Regards,
Markus

[Cocci] [PATCH v2 2/3] demos: add basic series of demos for exists and forall

[SF Markus Elfring]

> +int main(void)
> +{
> +	int a;
> +
> +	a = 10;

Is it nicer to write such a variable initialisation in a single line?

+    int a = 10;


> +	c = 400;
> +	c();

Can such source code trigger understanding difficulties?
How do you think about to specify a function implementation (or pointer)
before its assignment?

Regards,
Markus

[Cocci] [PATCH v2 1/3] tests: add test to remove single statement from branch

[Julia Lawall]

On Thu, 19 May 2016, Luis R. Rodriguez wrote:

> At leaset with coccinelle 1.0.4 this test fails with
> two issues, one is the return statement is shifted,
> another is debatable -- an empty branch statement is
> left. This is funtional however its debatable if this
> is desirable by default.
>
> v2: do not remove the if -- the if is needed as the items
>     in the branch could consist of functional run time
>     changes, for instance if (bar()).
>
> Signed-off-by: Luis R. Rodriguez <mcgrof@kernel.org>

Applied

> ---
>  tests/remove-code-in-branch1.c     | 7 +++++++
>  tests/remove-code-in-branch1.cocci | 4 ++++
>  tests/remove-code-in-branch1.res   | 7 +++++++
>  3 files changed, 18 insertions(+)
>  create mode 100644 tests/remove-code-in-branch1.c
>  create mode 100644 tests/remove-code-in-branch1.cocci
>  create mode 100644 tests/remove-code-in-branch1.res
>
> diff --git a/tests/remove-code-in-branch1.c b/tests/remove-code-in-branch1.c
> new file mode 100644
> index 000000000000..83840bdd99ac
> --- /dev/null
> +++ b/tests/remove-code-in-branch1.c
> @@ -0,0 +1,7 @@
> +int main(void)
> +{
> +	if (a > 1)
> +		c();
> +
> +	return 0;
> +}
> diff --git a/tests/remove-code-in-branch1.cocci b/tests/remove-code-in-branch1.cocci
> new file mode 100644
> index 000000000000..b3f03523ac92
> --- /dev/null
> +++ b/tests/remove-code-in-branch1.cocci
> @@ -0,0 +1,4 @@
> + at r@
> +@@
> +
> +-c();
> diff --git a/tests/remove-code-in-branch1.res b/tests/remove-code-in-branch1.res
> new file mode 100644
> index 000000000000..eb7985f683a0
> --- /dev/null
> +++ b/tests/remove-code-in-branch1.res
> @@ -0,0 +1,7 @@
> +int main(void)
> +{
> +	if (a > 1)
> +		{}
> +
> +	return 0;
> +}
> --
> 2.7.2
>
> _______________________________________________
> Cocci mailing list
> Cocci at systeme.lip6.fr
> https://systeme.lip6.fr/mailman/listinfo/cocci
>

[Cocci] [PATCH v2 2/3] demos: add basic series of demos for exists and forall

[Julia Lawall]

On Thu, 19 May 2016, Luis R. Rodriguez wrote:

> This should not ony help test but also demo use of exists
> and forall.
>
> Signed-off-by: Luis R. Rodriguez <mcgrof@kernel.org>

Applied.  I got rid of the assignments of c to 400, which could be
confusing.

julia

> ---
>  demos/exists1.c     | 20 ++++++++++++++++++++
>  demos/exists1.cocci |  9 +++++++++
>  demos/exists1.res   | 21 +++++++++++++++++++++
>  demos/exists2.c     | 21 +++++++++++++++++++++
>  demos/exists2.cocci | 13 +++++++++++++
>  demos/exists2.res   | 23 +++++++++++++++++++++++
>  demos/exists3.c     | 21 +++++++++++++++++++++
>  demos/exists3.cocci | 12 ++++++++++++
>  demos/exists3.res   | 23 +++++++++++++++++++++++
>  demos/exists4.c     | 22 ++++++++++++++++++++++
>  demos/exists4.cocci | 13 +++++++++++++
>  demos/exists4.res   | 21 +++++++++++++++++++++
>  12 files changed, 219 insertions(+)
>  create mode 100644 demos/exists1.c
>  create mode 100644 demos/exists1.cocci
>  create mode 100644 demos/exists1.res
>  create mode 100644 demos/exists2.c
>  create mode 100644 demos/exists2.cocci
>  create mode 100644 demos/exists2.res
>  create mode 100644 demos/exists3.c
>  create mode 100644 demos/exists3.cocci
>  create mode 100644 demos/exists3.res
>  create mode 100644 demos/exists4.c
>  create mode 100644 demos/exists4.cocci
>  create mode 100644 demos/exists4.res
>
> diff --git a/demos/exists1.c b/demos/exists1.c
> new file mode 100644
> index 000000000000..5cc37415bfef
> --- /dev/null
> +++ b/demos/exists1.c
> @@ -0,0 +1,20 @@
> +void bar(void)
> +{
> +	int a;
> +
> +	a = 300;
> +	b();
> +}
> +
> +int main(void)
> +{
> +	int a;
> +
> +	a = 10;
> +	b();
> +
> +	c = 400;
> +	c();
> +
> +	return 0;
> +}
> diff --git a/demos/exists1.cocci b/demos/exists1.cocci
> new file mode 100644
> index 000000000000..af95363de18f
> --- /dev/null
> +++ b/demos/exists1.cocci
> @@ -0,0 +1,9 @@
> +// this rule lacks exists, without exists, all control flows possible
> +// must match the rule when + or - is used. In the case of exists1.c only
> +// one possible control flow exists, the flow is completely linear.
> + at r@
> +@@
> +
> +b();
> +...
> +-c();
> diff --git a/demos/exists1.res b/demos/exists1.res
> new file mode 100644
> index 000000000000..cd83e4b2b6b1
> --- /dev/null
> +++ b/demos/exists1.res
> @@ -0,0 +1,21 @@
> +#include <stdio.h>
> +
> +int bar(void)
> +{
> +	int a;
> +
> +	a = 300;
> +	b();
> +}
> +
> +int main(void)
> +{
> +	int a;
> +
> +	a = 10;
> +	b();
> +
> +	c = 400;
> +
> +	return 0;
> +}
> diff --git a/demos/exists2.c b/demos/exists2.c
> new file mode 100644
> index 000000000000..486a8f5633d9
> --- /dev/null
> +++ b/demos/exists2.c
> @@ -0,0 +1,21 @@
> +void bar(void)
> +{
> +	int a;
> +
> +	a = 300;
> +	b();
> +}
> +
> +int main(void)
> +{
> +	int a;
> +
> +	a = 10;
> +	b();
> +
> +	c = 400;
> +	if (a > 5)
> +		c();
> +
> +	return 0;
> +}
> diff --git a/demos/exists2.cocci b/demos/exists2.cocci
> new file mode 100644
> index 000000000000..576b3cd3af24
> --- /dev/null
> +++ b/demos/exists2.cocci
> @@ -0,0 +1,13 @@
> +// this rule lacks exists, without exists, all control flows possible
> +// must match the rule. In the case of exists2.c two possible control
> +// flows exists on main():
> +// 1. b() --> a > 5 --> c();
> +// 2. b() --> a <= 5 ---> no c();
> +// Not all control flows match, so no changes are made.
> +// To visualize the control graph use: spatch --control-flow exists2.c
> + at r@
> +@@
> +
> +b();
> +...
> +-c();
> diff --git a/demos/exists2.res b/demos/exists2.res
> new file mode 100644
> index 000000000000..9d6401eb7d05
> --- /dev/null
> +++ b/demos/exists2.res
> @@ -0,0 +1,23 @@
> +#include <stdio.h>
> +
> +int bar(void)
> +{
> +	int a;
> +
> +	a = 300;
> +	b();
> +}
> +
> +int main(void)
> +{
> +	int a;
> +
> +	a = 10;
> +	b();
> +
> +	c = 400;
> +	if (a > 5)
> +		c();
> +
> +	return 0;
> +}
> diff --git a/demos/exists3.c b/demos/exists3.c
> new file mode 100644
> index 000000000000..486a8f5633d9
> --- /dev/null
> +++ b/demos/exists3.c
> @@ -0,0 +1,21 @@
> +void bar(void)
> +{
> +	int a;
> +
> +	a = 300;
> +	b();
> +}
> +
> +int main(void)
> +{
> +	int a;
> +
> +	a = 10;
> +	b();
> +
> +	c = 400;
> +	if (a > 5)
> +		c();
> +
> +	return 0;
> +}
> diff --git a/demos/exists3.cocci b/demos/exists3.cocci
> new file mode 100644
> index 000000000000..64cb43aa8ec4
> --- /dev/null
> +++ b/demos/exists3.cocci
> @@ -0,0 +1,12 @@
> +// this rule uses exists, with it, the rule is successful if at least
> +// one of the possible control flows possible match.
> +// exists3.c has two possible control flows on main():
> +// 1. b() --> a > 5 --> c();
> +// 2. b() --> a <= 5 ---> no c();
> +// The match on 1. enables the changes to take place.
> + at r exists @
> +@@
> +
> +b();
> +...
> +-c();
> diff --git a/demos/exists3.res b/demos/exists3.res
> new file mode 100644
> index 000000000000..f6b53c361fa5
> --- /dev/null
> +++ b/demos/exists3.res
> @@ -0,0 +1,23 @@
> +#include <stdio.h>
> +
> +int bar(void)
> +{
> +	int a;
> +
> +	a = 300;
> +	b();
> +}
> +
> +int main(void)
> +{
> +	int a;
> +
> +	a = 10;
> +	b();
> +
> +	c = 400;
> +	if (a > 5)
> +		{}
> +
> +	return 0;
> +}
> diff --git a/demos/exists4.c b/demos/exists4.c
> new file mode 100644
> index 000000000000..0b3dab08e6e1
> --- /dev/null
> +++ b/demos/exists4.c
> @@ -0,0 +1,22 @@
> +void bar(void)
> +{
> +	int a;
> +
> +	a = 300;
> +	b();
> +	c();
> +}
> +
> +int main(void)
> +{
> +	int a;
> +
> +	a = 10;
> +	b();
> +
> +	c = 400;
> +	if (a > 5)
> +		c();
> +
> +	return 0;
> +}
> diff --git a/demos/exists4.cocci b/demos/exists4.cocci
> new file mode 100644
> index 000000000000..d80c71a9d3f3
> --- /dev/null
> +++ b/demos/exists4.cocci
> @@ -0,0 +1,13 @@
> +// this rule uses forall, with it, all control flows must match.
> +//
> +// The exists4.c was extended to add a c() in comparison to exists2.c
> +// this is done to show that using forall will still have an effect
> +// on bar() even though it does not match on main()
> +//
> +// This is the default behaviour when + or - is used as well.
> + at r forall@
> +@@
> +
> +b();
> +...
> +-c();
> diff --git a/demos/exists4.res b/demos/exists4.res
> new file mode 100644
> index 000000000000..486a8f5633d9
> --- /dev/null
> +++ b/demos/exists4.res
> @@ -0,0 +1,21 @@
> +void bar(void)
> +{
> +	int a;
> +
> +	a = 300;
> +	b();
> +}
> +
> +int main(void)
> +{
> +	int a;
> +
> +	a = 10;
> +	b();
> +
> +	c = 400;
> +	if (a > 5)
> +		c();
> +
> +	return 0;
> +}
> --
> 2.7.2
>
> _______________________________________________
> Cocci mailing list
> Cocci at systeme.lip6.fr
> https://systeme.lip6.fr/mailman/listinfo/cocci
>

[Cocci] [PATCH v2 3/3] coccinelle: add control flow documentation

[Julia Lawall]

On Thu, 19 May 2016, Luis R. Rodriguez wrote:

> From: "Luis R. Rodriguez" <mcgrof@suse.com>

Applied

>
> Add control flow documentation.
>
> v2: fix typos, add "depends on" documentation in control flow
>     section as well.
>
> Signed-off-by: Luis R. Rodriguez <mcgrof@suse.com>
> ---
>  docs/manual/Makefile         |   6 +-
>  docs/manual/cocci_syntax.tex | 257 +++++++++++++++++++++++++++++++++++++++++++
>  docs/manual/flow1.c          |  10 ++
>  docs/manual/flow2.c          |  11 ++
>  4 files changed, 283 insertions(+), 1 deletion(-)
>  create mode 100644 docs/manual/flow1.c
>  create mode 100644 docs/manual/flow2.c
>
> diff --git a/docs/manual/Makefile b/docs/manual/Makefile
> index 98e397ac5b69..0cfe817cdc4e 100644
> --- a/docs/manual/Makefile
> +++ b/docs/manual/Makefile
> @@ -36,7 +36,11 @@ manual.pdf: $(SRC)
>  	$(PDFLATEX_CMD) manual.tex
>  	$(PDFLATEX_CMD) manual.tex
>
> -main_grammar.pdf: main_grammar.tex cocci_syntax.tex  macros_listing_cocci.tex macros_grammar.tex macros_common.tex examples.tex tips.tex
> +main_grammar.pdf: main_grammar.tex cocci_syntax.tex flow1.c flow2.c macros_listing_cocci.tex macros_grammar.tex macros_common.tex examples.tex tips.tex
> +	#spatch --control-flow-to-file flow1.c
> +	#spatch --control-flow-to-file flow2.c
> +	#dot -Gsize="0.5,0.5" -Tpdf flow1:main.dot > flow1.pdf
> +	#dot -Gsize="0.5,0.5" -Tpdf flow2:main.dot > flow2.pdf
>  	$(PDFLATEX_CMD) main_grammar.tex
>  	$(PDFLATEX_CMD) main_grammar.tex
>
> diff --git a/docs/manual/cocci_syntax.tex b/docs/manual/cocci_syntax.tex
> index 2c0f622251f6..b62540da7093 100644
> --- a/docs/manual/cocci_syntax.tex
> +++ b/docs/manual/cocci_syntax.tex
> @@ -584,6 +584,263 @@ rule is only applied if all of the metavariables for which there are no
>  default values have values.  See demos/defaultscript.cocci for examples of
>  the use of this feature.
>
> +\section{Control Flow}
> +
> +Rules describe a property which Coccinelle must match, when the property
> +described is matched the rule is considered successful. Program control
> +flows vary, a control flow describes a possible run time path taken by
> +a program.
> +
> +When using Coccinelle you often want to be able to express certain code
> +within certain types of control flows. Typically you will use ellipses
> +("...") to indicate to Coccinelle anything can be present between
> +consecutive statements. For instance the following SmPL patch tells Coccinelle
> +that rule r0 wishes to remove call calls to function c().
> +
> +\begin{center}
> +\begin{tabular}{c}
> +\begin{lstlisting}[language=Cocci]
> + at r0@
> +@@
> +
> +-c();
> +
> +\end{lstlisting}\\
> +\end{tabular}
> +\end{center}
> +
> +The context of the rule provides no other guidlines to Coccinelle to hint
> +about any possible control flow other than this is a statement, and that
> +c() must be called. We can modify the required control flow required for
> +this rule by providing additional requirements and using ellipses in between.
> +For instance, if we only wanted to remove call calls to c() but which also
> +had a prior call to foo() we'd use the following SmPL patch:
> +
> +\begin{center}
> +\begin{tabular}{c}
> +\begin{lstlisting}[language=Cocci]
> + at r1@
> +@@
> +
> +foo()
> +...
> +-c();
> +\end{lstlisting}\\
> +\end{tabular}
> +\end{center}
> +
> +There are two possible modifiers to the control flow for ellipses, one
> +is to annotate that statements in between ellipses are optional (<... ...>),
> +or that the statements in between must be present at least once (<+... ...+).
> +For instance the following SmPL patch tells Coccinelle to remove all
> +calls to c() but foo() must be present at least once.
> +
> +\begin{center}
> +\begin{tabular}{c}
> +\begin{lstlisting}[language=Cocci]
> + at r2@
> +@@
> +
> +<+...
> +foo()
> +...+>
> +-c();
> +
> +\end{lstlisting}\\
> +\end{tabular}
> +\end{center}
> +
> +Alternatively, if you wanted to be explicit that foo() was optional,
> +you could use the following SmPL rule.
> +
> +\begin{center}
> +\begin{tabular}{c}
> +\begin{lstlisting}[language=Cocci]
> + at r3@
> +@@
> +
> +<...
> +foo()
> +...>
> +-c();
> +
> +\end{lstlisting}\\
> +\end{tabular}
> +\end{center}
> +
> +Let's consider some sample code to review, this is flow1.c.
> +
> +\begin{center}
> +\begin{tabular}{c}
> +\begin{lstlisting}[language=C]
> +
> +int main(void)
> +{
> +	int ret, a = 2;
> +
> +	a = foo(a);
> +	ret = bar(a);
> +	c();
> +
> +	return ret;
> +}
> +\end{lstlisting}\\
> +\end{tabular}
> +\end{center}
> +
> +Applying the SmPL rule r0 to flow1.c would remove the c() line as the control
> +flow provides no specific context requirements. Applying rule r1 would also
> +succeed as the call to foo() is present. Likewise rules r2 and r3 would also
> +succeed. If the foo() call is removed from flow1.c only rules r0 and r3 would
> +succeed, as foo() would not be present and only rules r0 and r3 allow for
> +foo() to not be present.
> +
> +The program flow1.1 has a linear control flow, it has no branches. The main
> +routine has a McCabe cyclomatic complexity of 1. The McCabe cyclomatic
> +complexity can be computed using
> +{\tt pmccabe} (https://www.gnu.org/software/complexity/manual/html\_node/pmccabe-parsing.html).
> +
> +\begin{center}
> +\begin{tabular}{c}
> +\begin{lstlisting}[language=C]
> +pmccabe /flow1.c
> +1       1       5       1       10      flow1.c(1): main
> +\end{lstlisting}\\
> +\end{tabular}
> +\end{center}
> +
> +Since programs can use branches, often times you may also wish to annotate
> +requirements for control flows in consideration for branches, for when
> +the McCabe cyclomatic complexity is > 1. The following program, flow2.c,
> +enables the control flow to diverge on line 7 due to the branch, if (a) --
> +one control flow possible is if (a) is true, another when if (a) is false.
> +
> +\begin{center}
> +\begin{tabular}{c}
> +\begin{lstlisting}[language=C]
> +int main(void)
> +{
> +	int ret, a = 2;
> +
> +	a = foo(a);
> +	ret = bar(a);
> +	if (a)
> +		c();
> +
> +	return ret;
> +}
> +\end{lstlisting}\\
> +\end{tabular}
> +\end{center}
> +
> +This program has a McCabe cyclomatic complexity of 2.
> +
> +\begin{center}
> +\begin{tabular}{c}
> +\begin{lstlisting}[language=C]
> +pmccabe flow2.c
> +2       2       6       1       11      flow2.c(1): main
> +\end{lstlisting}\\
> +\end{tabular}
> +\end{center}
> +
> +Using the McCabe cyclomatic complexity is one way to get an idea of
> +the complexity of the control graph for a function, another way is
> +to visualize all possible paths. Coccinelle provides a way to visualize
> +control flows of programs, this however requires {\tt dot}
> +(http://www.graphviz.org/) and {\tt gv} to be installed (typically provided
> +by a package called graphviz). To visualize control flow or a program
> +using Coccinelle you use:
> +
> +\begin{center}
> +\begin{tabular}{c}
> +spatch --control-flow-to-file flow1.c
> +spatch --control-flow-to-file flow2.c
> +\end{tabular}
> +\end{center}
> +
> +%Below are the two generated control flow graphs for flow1.c and flow2.c
> +%respectively.
> +
> +%\begin{figure}
> +%	\[\includegraphics[width=\linewidth]{flow1.pdf}\]
> +%	\caption{Linear flow example}
> +%	\label{devmodel}
> +%\end{figure}
> +
> +%\begin{figure}
> +%	\[\includegraphics[width=\linewidth]{flow2.pdf}\]
> +%	\caption{Linear flow example}
> +%	\label{devmodel}
> +%\end{figure}
> +
> +Behind the scenes this generates a dot file and uses gv to generate
> +a PDF file for viewing. To generate and inspect these manually you
> +can use the following:
> +
> +\begin{center}
> +\begin{tabular}{c}
> +spatch --control-flow-to-file flow2.c
> +dot -Tpdf flow1:main.dot > flow1.pdf
> +\end{tabular}
> +\end{center}
> +
> +By default properties described in a rule must match all control
> +flows possible within a code section being inspected by Coccinelle.
> +So for instance, in the following SmPL patch rule r1 would match all
> +the control flow possible on flow1.c as its linear, however it would
> +not match the control possible on flow2.c. The rule r1 would not
> +be successful in flow2.c
> +
> +\begin{center}
> +\begin{tabular}{c}
> +\begin{lstlisting}[language=Cocci]
> + at r1@
> +@@
> +
> +foo()
> +...
> +-c();
> +
> +\end{lstlisting}\\
> +\end{tabular}
> +\end{center}
> +
> +The default control flow can be modified by using the keyword "exists"
> +following the rule name. In the following SmPL patch the rule r2 would
> +be successful on both flow1.c and flow2.c
> +
> +\begin{center}
> +\begin{tabular}{c}
> +\begin{lstlisting}[language=Cocci]
> + at r2 exists@
> +@@
> +
> +foo()
> +...
> +-c();
> +
> +\end{lstlisting}\\
> +\end{tabular}
> +\end{center}
> +
> +If the rule is followed by the "forall" keyword, then all control flow
> +paths must match in order for the rule to succeed. By default when one
> +has "-" and "+", or when one has no annotations at all and only script
> +code, ellipses ("...") uses the forall semantics.  And when one uses
> +context annotation ("*"), the ellipses ("...") uses the exists semantics.
> +Using the keyword "forall" or "exists" in the rule header affects
> +all ellipses ("...") uses in the rule. You can also annotate each
> +ellipses ("...") with "when exists" or "when forall" individually.
> +
> +Rules can also be not be successful if requirements do not match
> +when a rule name is followed by "depends on XXX". When "depends on is used
> +it means the rule should only apply if rule XXX matched with the current
> +metavariable environment. Alternatively, "depends on ever XXX" can be used
> +as well, this means this rule should apply if rule XXX was ever matched at
> +all. A counter to this use is "depends on never XXX", which means that this
> +rule should apply if rule XXX was never matched at all.
> +
>  \section{Transformation}
>
>  The transformation specification essentially has the form of C code, except
> diff --git a/docs/manual/flow1.c b/docs/manual/flow1.c
> new file mode 100644
> index 000000000000..43e45ed32843
> --- /dev/null
> +++ b/docs/manual/flow1.c
> @@ -0,0 +1,10 @@
> +int main(void)
> +{
> +	int ret, a = 2;
> +
> +	a = foo(a);
> +	ret = bar(a);
> +	c();
> +
> +	return ret;
> +}
> diff --git a/docs/manual/flow2.c b/docs/manual/flow2.c
> new file mode 100644
> index 000000000000..bb0d95e4c310
> --- /dev/null
> +++ b/docs/manual/flow2.c
> @@ -0,0 +1,11 @@
> +int main(void)
> +{
> +	int ret, a = 2;
> +
> +	a = foo(a);
> +	ret = bar(a);
> +	if (a)
> +		c();
> +
> +	return ret;
> +}
> --
> 2.7.2
>
> _______________________________________________
> Cocci mailing list
> Cocci at systeme.lip6.fr
> https://systeme.lip6.fr/mailman/listinfo/cocci
>

[Cocci] [PATCH v2 3/3] coccinelle: add control flow documentation

[SF Markus Elfring]

> Applied

Did you fix the remaining open issues (like typos) in this update
suggestion?

Regards,
Markus

[Cocci] [PATCH v2 3/3] coccinelle: add control flow documentation

[SF Markus Elfring]

>> Did you fix the remaining open issues (like typos) in this update
>> suggestion?
> I edited the text somewhat.

Can corresponding commits be viewed in a public repository in the near
future?

Regards,
Markus

[Cocci] [PATCH v2 3/3] coccinelle: add control flow documentation

[Julia Lawall]

On Sat, 21 May 2016, SF Markus Elfring wrote:

> > Applied
>
> Did you fix the remaining open issues (like typos) in this update
> suggestion?

I edited the text somewhat.  Questions like "Do you want to rephrase
this?" I don't really know what to do with.

julia

[Cocci] [PATCH v2 3/3] coccinelle: add control flow documentation

[SF Markus Elfring]

> I edited the text somewhat.  Questions like "Do you want to rephrase
> this?" I don't really know what to do with.

I find a commit with a subject like "adjust the control flow discussion
a little" also interesting for this issue.
https://github.com/coccinelle/coccinelle/commit/c182a2eed0310c2e0203c817b02d46bfbe5f1453

Regards,
Markus