Re: [XEN PATCH][for-4.19] domain: add ASSERT to help static analysis tools

[Stefano Stabellini <sstabellini@xxxxxxxxxx>]

On Thu, 9 Nov 2023, Julien Grall wrote:
> On 09/11/2023 07:42, Jan Beulich wrote:
> > On 08.11.2023 14:33, Julien Grall wrote:
> > > Hi Jan,
> > > 
> > > On 08/11/2023 11:19, Jan Beulich wrote:
> > > > On 08.11.2023 12:03, Nicola Vetrini wrote:
> > > > > On 2023-11-08 09:24, Jan Beulich wrote:
> > > > > > On 03.11.2023 18:58, Nicola Vetrini wrote:
> > > > > > > Static analysis tools may detect a possible null
> > > > > > > pointer dereference at line 760 (the memcpy call)
> > > > > > > of xen/common/domain.c. This ASSERT helps them in
> > > > > > > detecting that such a condition is not possible
> > > > > > > and also provides a basic sanity check.
> > > > > > 
> > > > > > I disagree with this being a possible justification for adding such
> > > > > > a
> > > > > > redundant assertion. More detail is needed on what is actually
> > > > > > (suspected to be) confusing the tool. Plus it also needs explaining
> > > > > > why (a) adding such an assertion helps and (b) how that's going to
> > > > > > cover release builds.
> > > > > > 
> > > > > 
> > > > > How about:
> > > > > "Static analysis tools may detect a possible null pointer dereference
> > > > > at line 760 (config->handle) due to config possibly being NULL.
> > > > > 
> > > > > However, given that all system domains, including IDLE, have a NULL
> > > > > config and in the code path leading to the assertion only real domains
> > > > > (which have a non-NULL config) can be present."
> > > > > 
> > > > > On point b): this finding is a false positive, therefore even if the
> > > > > ASSERT is
> > > > > expanded to effectively a no-op, there is no inherent problem with
> > > > > Xen's
> > > > > code.
> > > > > The context in which the patch was suggested [1] hinted at avoiding
> > > > > inserting in
> > > > > the codebase false positive comments.
> > > > 
> > > > Which I largely agree with. What I don't agree with is adding an
> > > > assertion which is only papering over the issue, and only in debug
> > > > builds.
> > > 
> > > I expect that the number of issues will increase a lot as soon as we
> > > start to analyze production builds.
> > > 
> > > I don't think it will be a solution to either replace all the ASSERT()
> > > with runtime check in all configuration or even...
> > > 
> > > > So perhaps instead we need a different way of tracking
> > > > false positives (which need to be tied to specific checker versions
> > > > anyway).
> > > 
> > > ... documenting false positive.
> > > 
> > > IMHO, the only viable option would be to have a configuration to keep
> > > ASSERT in production build for scanning tools.
> > 
> > But wouldn't that then likely mean scanning to be done on builds not also
> > used in production? Would doing so even be permitted when certification
> > is a requirement? Or do you expect such production builds to be used with
> > the assertions left in place (increasing the risk of a crash; recall that
> > assertions themselves may also be wrong, and hence one triggering in rare
> > cases may not really be a reason to bring down the system)?
> 
> I will leave Stefano/Nicola to answer from the certification perspective. But
> I don't really see how we could get away unless we replace most of the
> ASSERT() with proper runtime check (which may not be desirable for ASSERT()s
> like this one).

For sure we don't want to replace ASSERTs with runtime checks.

Nicola, do we really need the ASSERT to be implemented as a check, or
would the presence of the ASSERT alone suffice as a tag, the same way we
would be using /* SAF-xx-safe */ or asmlinkage?

If we only need ASSERT as a deviation tag, then production builds vs.
debug build doesn't matter.

If ECLAIR actually needs ASSERT to be implemented as a check, could we
have a special #define to define ASSERT in a special way for static
analysis tools in production builds? For instance:

#ifdef STATIC_ANALYSIS
#define ASSERT(p) \
    do { if ( unlikely(!(p)) ) printk("ASSERT triggered %s:%d", 
__file__,__LINE__); } while (0)
#endif

Nicola, would that be enough?