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

Clive Pygott clivepygott at gmail.com
Wed Apr 18 17:36:53 BST 2018


Just seen your recent post - I believe that loop (that limits the maximum
number of iterations) is legal - because error isn't a loop counter -
because of the need to monotonically vary on each iteration.  i is the loop
counter, and the loop satisfies the requirements of 14.2

   Clive

On Wed, Apr 18, 2018 at 5:29 PM, Clive Pygott <clivepygott at gmail.com> wrote:

> An aside on terminology - a double value is scalar -
>
>    - C11: 6.2.5#18   "*Integer and floating types are collectively called
>    arithmetic types*"
>    - C11: 6.2.5#21  "*Arithmetic types and pointer types are collectively
>    called scalar types.*"  So a double is an arithmetic type
>
>
> I'd argue that my while loop doesn't violate 14.1 because error is (almost
> certainly) not a loop counter - because the definition of loop counter
> includes "*Its value varies monotonically on each iteration of a given
> instance of a loop*".  Its a strange form of convergence calculation that
> guarantees that the error changes by the same amount on each iteration.
>
> Even if you ignore/deviate 14.1 both your floating and integer examples
> violate 14.2 "A for loop shall be well formed"
>
> The definition of 'well formed' includes requirements for the third
> expression of the for loop (which are empty in your examples):
>          * Third clause which:*
>
>    - *Shall be an expression whose only persistent side effect is to
>       modify the value of the loop counter, and*
>       - *Shall not use objects that are modified in the for loop body*
>
>
>
>
>   void converge_on (double z)
>        {
>          for (double x = 0;  x < z;   x = foo (x) )
>               ;
>        }
>
> You might just argue that this is a well formed for loop, if foo returns a
> value that monotonically decreases, and  converge_on is always called
> with z < 0
>
>     Clive
>
>
>
>
>
>
>
>
>
>
>
> On Wed, Apr 18, 2018 at 4:45 PM, Martin Sebor <msebor at gmail.com> wrote:
>
>> 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-s
>>> ecure-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-s
>>> ecure-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-s
>> ecure-studygroup
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.trustable.io/pipermail/c-safe-secure-studygroup/attachments/20180418/e963d59c/attachment-0001.html>


More information about the C-safe-secure-studygroup mailing list