The when modifier on ”…” is normally used to indicate code that should not appear in the region matched by the ”…”. For example, the following pattern only matches if there is no call to xxx() between the calls to f and g:

f();
... when != xxx()
g();

It is also possible to use when forall or when exists, to specify that ”…” should match all paths or only a single one. Finally, there are when strict and when any, which are explained as follows.

In the pattern A … B, the ”…” matches any sequence of code that appears between A and B and that does not contain A or B; known as the “shortest path property”. Adding when any after ”…” lifts this shortest path restriction. For example,

A
... when any
B

can match:

1. A
2. A
3. B
4. B

in four different ways: 1-3, 1-4, 2-3, 2-4. On the other hand:

A
...
B

only matches 2-3.

As shown above, when using when any, a single piece of code can be part of multiple matches. If there are transformations associate with that code, this can cause problems, because the system finds a single piece of code that can be transformed in two different ways.

In the above case, when any can also be expressed using a nest. That is, the above rule is equivalent to the following:

@@
@@

a();
<...
 \(a\|b\)
...>
b();

A nest also has the shortest path property, but the pattern that is specified inside the nest overrides the implicit shortest path constraints.

It may be that this semantics of nest makes when any unnecessary. But when any is a bit more concise.

The sequence when strict is something that makes sense when spatch is considering all control-flow paths, which it does by default unless the “semantic matching” notation * (rather than - or +) is used. It also considers all control-flow paths when the rule header is annotated with forall, or when when forall is used on … In this case, suppose there is a rule:

a();
...
b();

In this case, we only have a successful match if there is a call to a() that is followed by a call to b() along all control flow paths. That is, the following code matches:

a();
if (x) b(); else b();

and the following code does not:

a();
if (x) b(); else foo();

But we have found that in Linux code, such function calls are often interspersed with error-handling code. For example, the code may be:

a();
x = c();
if (!x) return -1;
b();

But the pattern was somehow intending to match the normal flow of execution, and the error code return -1 is not really part of that. So by default, A … B considers all paths except paths that it considers to end in the reporting of an error, when such paths do not contain B. It considers the reporting of an error to be the then branch of a conditional that has no else branch and that ends in a return or goto, a heuristic that works fairly well, but not perfectly for Linux code.

When strict then says not to give special treatment to error paths and instead to require that b(); appear on all control-flow paths.