[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