Re: [XEN PATCH] docs/misra: document the C dialect and translation toolchain assumptions.

[Roberto Bagnara <roberto.bagnara@xxxxxxxxxxx>]

On 19/06/23 13:47, Jan Beulich wrote:
> On 19.06.2023 12:53, Roberto Bagnara wrote:
> > On 19/06/23 09:54, Jan Beulich wrote:
> > > On 16.06.2023 17:54, Roberto Bagnara wrote:
> > > > On 16/06/23 01:26, Stefano Stabellini wrote:
> > > > > On Thu, 15 Jun 2023, Roberto Bagnara wrote:
> > > > > > +       static function is used in an inline function with external linkage:
> > > > > > +          non-documented GCC extension.
> > > > > I am not sure if I follow about this one. Did you mean "static is used
> > > > > in an inline function with external linkage" ?
> > > > An inline function with external linkage can be inlined everywhere.
> > > > If that calls a static functions, which is not available everywhere,
> > > > the behavior is not defined.
> > > I guess I could do with an example where this leads to UB. What I'd expect
> > > is that it leads to a compilation error.
> > Here are the two occurrences we have in ARM64 code:
> >
> > violation for rule MC3R1.R1.1: (required) The program shall contain no 
> > violations of the standard C syntax and constraints, and shall not exceed the 
> > implementation's translation limits.
> > xen/common/spinlock.c:316.29-316.40: Loc #1 [culprit: static function 
> > `observe_head(spinlock_tickets_t*)' is used in an inline function with external linkage 
> > (ill-formed for the C99 standard, ISO/IEC 9899:1999: "An ill-formed source detected 
> > by the parser."
> > xen/common/spinlock.c:301.26-301.37: Loc #2 [evidence: 
> > `observe_head(spinlock_tickets_t*)' declared here]
> > xen/include/xen/spinlock.h:180.1-180.4: Loc #3 [evidence: use 'static' to give 
> > inline function `_spin_lock_cb(spinlock_t*, void(*)(void*), void*)' internal 
> > linkage]
> >
> > violation for rule MC3R1.R1.1: (required) The program shall contain no 
> > violations of the standard C syntax and constraints, and shall not exceed the 
> > implementation's translation limits.
> > xen/common/spinlock.c:324.5-324.12: Loc #1 [culprit: static function `got_lock(union 
> > lock_debug*)' is used in an inline function with external linkage (ill-formed for the C99 
> > standard, ISO/IEC 9899:1999: "An ill-formed source detected by the parser."
> > xen/common/spinlock.c:227.13-227.20: Loc #2 [evidence: `got_lock(union 
> > lock_debug*)' declared here]
> > xen/include/xen/spinlock.h:180.1-180.4: Loc #3 [evidence: use 'static' to give 
> > inline function `_spin_lock_cb(spinlock_t*, void(*)(void*), void*)' internal 
> > linkage]
> I know _spin_lock_cb() was an example of a violation (it isn't anymore),
> but this does not serve as an example for the UB you claim may occur.
> The "inline" there was in a .c file, and hence the function could only
> be inlined with its (static) helper also in scope.
This is a constraint violation according to C99 6.7.4p3: "An inline definition
of a function with external linkage shall not contain a definition of a 
modifiable
object with static storage duration, and shall not contain a reference to an 
identifier
with internal linkage."  A standard-compliant C compiler ought to diagnose all
constraint violations: when it does not, as is the case for GCC in these 
specific
examples, the behavior is implicitly undefined.