[C-safe-secure-studygroup] On MISRA C:2012 Rule 14.1
Roberto Bagnara
bagnara at cs.unipr.it
Wed Apr 18 18:16:01 BST 2018
On 04/18/2018 05:45 PM, Martin Sebor 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 don't follow: what is that does not have scalar type?
Whatever does not have scalar type cannot be a loop counter.
> I can't think of a way to write a loop like the one above under
> these constraints.
This is why MISRA has a deviation process. The point is that
for a loop like the one above there are two possibilities:
- error is not a loop counter, and rule 14.1 has nothing to say
about it;
- error is a loop counter, hence it varies monotonically, hence,
the loop body will only be execute a finite number of times
(unless the loop condition violates rule 14.3); so, in this case,
14.1 is not there to ensure a finite number of iteration (which is
guaranteed anyway), but to avoid a possible mismatch between the
number of expected iterations and the actual number of iterations on
different implementations.
Most coding rules are compromises, in any coding standard.
Rule 14.1 and the definition of loop counter is the result of:
a) the need to define numerically controlled loops for determinate
iteration, like the FOR loops in Pascal;
b) the aim not to impose a rigid form for such loops.
It is for this reason that the rule is undecidable: because recognizing
loop counters is undecidable. You can see this rule sitting between
two extremes:
- fully syntactic, e.g., prescribe Pascal FOR syntax:
for (control_variable = initial_value;
control_variable <= final_value; ++control_variable) {
body;
}
where body cannot modify or take the address of control_varible or
any variable occurring in final_value;
- fully semantic, e.g., Rule 3 of NASA/JPL C-2009: write the loops
as you like, but in the end you have to prove that there is
an upper bound to the maximum number of iterations (you need
not exhibit such upper bound, only prove that it exists).
>> 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
>>
>
>
> _______________________________________________
> 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
--
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/3ffa9a62/attachment.bin>
More information about the C-safe-secure-studygroup
mailing list