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

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

On 2023-11-11 02:13, Stefano Stabellini wrote:
> 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)?
Yes, and sorry for the late reply.

--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)