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

[Martin Sebor]

On 04/18/2018 01:38 AM, Clive Pygott wrote:
> My thought on this is that the example Martin suggests shouldn't be
> implemented as a for loop. I'd expect it to be implemented as a while loop
>
>              void converge_on (double  requiredPrecision)
>                     { double error =  requiredPrecision +1.0;  //
> anything >  requiredPrecision
>                       while (error > requiredPrecision)
>                                 error = iterate();;
>                     }

By my understanding of 8.14 this loop would also violate the rule
because the /loop counter/ (i.e., the variable that's involved
in a decision to exit the loop) doesn't have a scalar type.

I can't think of a way to write a loop like the one above under
these constraints.

Martin

>
>     Clive
>
> On Wed, Apr 18, 2018 at 6:31 AM, Roberto Bagnara <bagnara at cs.unipr.it
> <mailto:bagnara at cs.unipr.it>> wrote:
>
>     On 18/04/2018 04:15, Martin Sebor wrote:
>     > On 04/17/2018 05:54 AM, Roberto Bagnara wrote:
>     >> MISRA C:2012 Rule 14.1:
>     >> A loop counter shall not have essentially floating type
>     >>
>     >> This is a required rule.  The aim is to avoid that the
>     complication and non-determinism of floating-point computations is
>     reflected into the number of times loops are executed.
>     >>
>     >> By "complication" I mean that the limitations of floating-point
>     types are not well understood by many programmers;  for instance
>     many do not know that 0.1 is not exactly representable as a binary
>     floating-point number and many of those who do know would not be
>     able to say how it will be rounded and upon what conditions.
>     >>
>     >> By "non-determinism" I mean that, even if the C implementation at
>     hand is based on, say, IEEE~754, obtaining deterministic behavior
>     (that is, behavior that is reproducible on different systems, even
>     using the very same compiler) is a challenging task.
>     >>
>     >> Being able to reliably predict the number of iterations of a
>     numerically-controlled loop is important both for safety and
>     security: for such loops, integer numbers should be used.
>     >
>     > Not to dispute the validity of the rule in the (I suspect rare)
>     > instances when a floating type is misused for the counter but
>     > what about the cases where the number of iterations isn't known
>     > ahead of time and the loop terminates only when the computation
>     > converges on some predetermined floating result?  How does one
>     > write a loop like that so it doesn't violate the rule?
>     >
>     > For instance:
>     >
>     >   void converge_on (double z)
>     >   {
>     >     for (double x = 0; x < z; )
>     >       x = foo (x);
>     >   }
>     >
>     > Based on the definitions in 8.14 Control statement expressions,
>     > it seems impossible to write a loop like that.  The concern that
>     > the loop may not terminate is no different than with a scalar
>     > counter:
>     >
>     >   void converge_on (int z)
>     >   {
>     >     for (int x = 0; x < z; )
>     >       x = foo (x);
>     >   }
>     >
>     > I wonder if it might be worthwhile to distill the underlying
>     > problem that rule 14.1 is trying to prevent and formulate
>     > a rule aimed at avoiding it instead.
>
>     Sorry, I should have clarified that "loop counter" is a technical
>     term in MISRA C: it is defined in Section 8.14.  The overall idea
>     is to be able to express determinate iteration in MISRA C, that is,
>     iteration whereby the maximum number of iterations can be known
>     before the first iteration begins.  In Pascal, the FOR construct
>     plays this role;  in MISRA C we have well-formed for loops.
>     For indeterminate iteration you can use while or do-while loops,
>     or you can deviate the relevant 14.* rules if you want to use
>     for loops for that purpose as well.
>
>     If you prefer semantic restrictions, you may consider
>     Rule 3 of NASA JPL Institutional Coding Standard
>     for the C Programming Language:
>
>     Rule 3 (loop bounds)
>     All loops shall have a statically determinable upper-bound on the
>     maximum number of loop iterations. It shall be possible for a static
>     compliance checking tool to affirm the existence of the bound. An
>     exception is allowed for the use of a single non-terminating loop
>     per task
>     or thread where requests are received and processed. Such a server loop
>     shall be annotated with the C comment: /* @non-terminating@ */.
>     [Power of Ten Rule 2]
>
>
>     --
>          Prof. Roberto Bagnara
>
>     Applied Formal Methods Laboratory - University of Parma, Italy
>     mailto:bagnara at cs.unipr.it <mailto:bagnara at cs.unipr.it>
>                                   BUGSENG srl - http://bugseng.com
>                                   mailto:roberto.bagnara at bugseng.com
>     <mailto:roberto.bagnara at bugseng.com>
>
>
>     _______________________________________________
>     C-safe-secure-studygroup mailing list
>     C-safe-secure-studygroup at lists.trustable.io
>     <mailto:C-safe-secure-studygroup at lists.trustable.io>
>     https://lists.trustable.io/cgi-bin/mailman/listinfo/c-safe-secure-studygroup
>     <https://lists.trustable.io/cgi-bin/mailman/listinfo/c-safe-secure-studygroup>
>
>
>
>
> _______________________________________________
> 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
>