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

[Stefano Stabellini <sstabellini@xxxxxxxxxx>]

On Fri, 10 Nov 2023, Nicola Vetrini wrote:
> Hi everyone,
> 
> I trimmed the thread a bit, to make this more readable.
> 
> > > > > > 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
> > 
> > Just to make 100% clear, you are saying that assessor will be happy if we
> > analyze it with ASSERT enabled but in production we use it wout them
> > enabled? The assumption here is that they should have *never* been triggered
> > so they surely should not happen in production.
> > 
> > Cheers,
> 
> First of all, Andrew is experimenting with an alternate solution, so we should
> wait making
> any decision here until he can share the outcome of his findings.
> However, from a certification perspective, the fact that the codebase is
> tested with
> asserts enabled is a strong enough claim for a justification to be based on an
> assertion;
> the code path just needs to be exercised by the tests.
> Getting into the business of how to define asserts for static analysis is
> likely to
> just cause more trouble.

That's great. Also given Andrew's reply, then can we just go ahead with
adding the ASSERT as done in this patch (with the added in-code comment
as requested by Jan)?