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

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

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.

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