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

[Nicola Vetrini <nicola.vetrini@bugseng.com>]

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)