[C-safe-secure-studygroup] On MISRA C:2012 Rule 14.1

[Robert Seacord]

A lively discussion!  I'm sort of glad I was preoccupied for most of it.

I'll just agree with one of Martin's points that the deviation process is
tangential to this working group as we are only concerned with what rules
an analyzer must enforce and to conform with the requirements of this IS
you must support the full safety/security set. Processes such as MISRA may
be implemented on top of this.  If the safety community likes noisey rules
they will have them, but we should endeavor to be as precise as possible.



On Fri, Apr 20, 2018, 12:40 AM Martin Sebor <msebor at gmail.com> wrote:

> On 04/19/2018 11:14 AM, Fulvio Baccaglini wrote:
> >
> > On 19/04/18 16:35, Martin Sebor wrote:
> >> I think we have digressed.  Let me try again.
> >>
> >> The rationale for Rule 14.1 is that a loop with a floating
> >> point counter can end up iterating fewer or more times than
> >> expected because of one or both of these conditions:
> >>
> >> 1) rounding errors accumulated in the loop counter when
> >>    the loop step is not a multiple of FLT_RADIX
> >> 2) differences in precision between different floating point
> >>    formats/representations
> >>
> >> To prevent the problem, 14.1 banishes floating point loop
> >> counters.
> >>
> >> It should be obvious that it's not only more restrictive than
> >> necessary, but given the definition of /loop counter/ (has to
> >> vary monotonically), it also isn't sufficient to detect such
> >> problems even in cases when it would otherwise be possible.
> >>
> >> For example, neither (1) nor (2) applies to the loop below
> >> yet 14.1 makes it non-compliant:
> >>
> >>   for (float f = 1; f <= 32; f *= 2)
> >>     printf ("%f ", f);
> >
> > I think that an exception for this case would lead to Rule 14.1 becoming
> > undecidable, for instance:
> >
> > void f (float x)
> > {
> >     for (float f = 1; f <= 32; f *= x)
> >         printf ("%f ", f);
> > }
>
> Rule 14.1 already _is_ undecidable (it's clearly marked as such)
> and Roberto explained it's because of the loop counter definition
> (must change monotonically).
>
> I'm also not suggesting to carve out exceptions to rule 14.1.
> I think the rule is poorly specified (as is the definition of
> loop counter) and should be replaced with one that's specified
> without so many problems.
>
> >
> > Also, a tool would then need to shadow the specific floating point
> > format/representation intended for the code under analysis, to track the
> > values of x, and decide whether there is a rounding error or not.
>
> Sure.  That's implied and not unique to floating point.  TS
> 17961 already requires it for pointers (rule 5.22 -- forming
> out-of-bounds pointers and array subscripts) and integers
> (rule 5.30 -- signed integer overflow).
>
> >> Conversely, the following loop is subject to (1) yet, according
> >> to what has been explained in this discussion, it is compliant
> >> because its loop counter is not of floating point type (f does
> >> not vary monotonically so it's not a loop counter; i does
> >> increase monotonically so it is the one and only loop counter):
> >>
> >>   float f = 0;
> >>   for (int i = 1; f < 1 && i <= 32; i *= 2)
> >>     f += sin (i);
> >
> > This would violate Rule 14.2 "A loop should be well formed would be
> > violated", e.g. second clause uses another object that is modified in
> > the loop body.
>
> We are not discussing rule 14.2 so it's not relevant whether
> it's violated by the example but presumably the equivalent
> variant would be compliant with it and still show the same
> problem:
>
>    float f = 0;
>    for (int i = 1; i <= 32; i *= 2)
>    {
>      if (f >= 1)
>        break;
>      f += sin (i);
>    }
>
> (The point of the examples I gave is to illustrate what I view
> as problems with 14.1.  They are not meant to be representative
> of best practices or conform to all MISRA (or any other) rules.)
>
> >> Likewise, the loop below is subject to (2) but it is also
> >> compliant, for the same reason as above.
> >>
> >>   for (int i = 1; exp (i) <= 8.0; i *= 2)
> >>     foo (i);
> >
> > It seems to me that (1) unintended consequences of the accumulation of
> > rounding errors is much more relevant to loops, while (2) the dependency
> > on floating point format/representation is an issue that would apply
> > anywhere "exp (i) <= 8.0" is used. My initial feeling is that this could
> > be acceptable.
>
> I'm not sure I understand what you mean by "this could be
> acceptable."  Are you suggesting that even though the loop
> above suffers from the problems discussed in 14.1's rationale
> it's not a problem that the rule doesn't apply to it?
>
> >> In fact, so is this one, even though the number of times it
> >> iterates depends on the size of unsigned long:
> >>
> >>   for (unsigned long i = 1; i; i << 1)
> >>     foo (i);
> >
> > Here Dir 4.6 "typedefs that indicate size and signedness should be used
> > in place of the basic numerical types" would make the intent clear, e.g.:
> >
> > for (uint32_t i = 1; i; i <<= 1)
> >   foo (i);
> >
>
> Yes, that might be a solution.  But my point is that the same
> problem that rule 14.1 tries to solve by disallowing floating
> point loop counters affects integers as well.  That suggests
> that the solution in 14.1 isn't general enough and this is
> an opportunity for us to try to come up with one that is.
>
> Martin
>
>
> _______________________________________________
> C-safe-secure-studygroup mailing list
> C-safe-secure-studygroup at lists.trustable.io
>
> https://lists.trustable.io/cgi-bin/mailman/listinfo/c-safe-secure-studygroup
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.trustable.io/pipermail/c-safe-secure-studygroup/attachments/20180422/4e662c07/attachment.html>