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

Roberto Bagnara bagnara at cs.unipr.it
Wed Apr 18 06:31:12 BST 2018


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
                              BUGSENG srl - http://bugseng.com
                              mailto:roberto.bagnara at bugseng.com

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2093 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://lists.trustable.io/pipermail/c-safe-secure-studygroup/attachments/20180418/1758e967/attachment.bin>


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