[C-safe-secure-studygroup] On MISRA C:2012 Rule 14.1
Clive Pygott
clivepygott at gmail.com
Thu Apr 19 18:11:37 BST 2018
Thanks for the plug info
Clive
On Thu, Apr 19, 2018 at 4:35 PM, Martin Sebor <msebor at gmail.com> wrote:
> I think we have digressed. Let me try again.
>
> The rationale for Rule 14.1 is that a loop with a floating
> point counter can end up iterating fewer or more times than
> expected because of one or both of these conditions:
>
> 1) rounding errors accumulated in the loop counter when
> the loop step is not a multiple of FLT_RADIX
> 2) differences in precision between different floating point
> formats/representations
>
> To prevent the problem, 14.1 banishes floating point loop
> counters.
>
> It should be obvious that it's not only more restrictive than
> necessary, but given the definition of /loop counter/ (has to
> vary monotonically), it also isn't sufficient to detect such
> problems even in cases when it would otherwise be possible.
>
> For example, neither (1) nor (2) applies to the loop below
> yet 14.1 makes it non-compliant:
>
> for (float f = 1; f <= 32; f *= 2)
> printf ("%f ", f);
>
> Conversely, the following loop is subject to (1) yet, according
> to what has been explained in this discussion, it is compliant
> because its loop counter is not of floating point type (f does
> not vary monotonically so it's not a loop counter; i does
> increase monotonically so it is the one and only loop counter):
>
> float f = 0;
> for (int i = 1; f < 1 && i <= 32; i *= 2)
> f += sin (i);
>
> Likewise, the loop below is subject to (2) but it is also
> compliant, for the same reason as above.
>
> for (int i = 1; exp (i) <= 8.0; i *= 2)
> foo (i);
>
> In fact, so is this one, even though the number of times it
> iterates depends on the size of unsigned long:
>
> for (unsigned long i = 1; i; i << 1)
> foo (i);
>
> So my point is that although the goal of the rule makes sense
> the way it's specified leads to needlessly many false positives
> as well as negatives.
>
> I suggest we focus on the goal and specify a better rule that
> achieves it with fewer problems.
>
> Martin
>
> PS I think Czech sockets are the same as (or close enough to)
> the German kind. When traveling to Europe I always look this
> up to be sure. Here's a site that lets you select where you're
> traveling from to see if you need an adapter:
>
> https://www.power-plugs-sockets.com/czech-republic/
>
> On 04/19/2018 03:32 AM, Clive Pygott wrote:
>
>> First of all an apology - I've just been to a MISRA C++ meeting and
>> dropped into C++ mode. We wrote our loop counter rules before MISRA
>> C:2012 and we're more restrictive on what constituted an acceptable for
>> loop - we're in the middle of an rewrite that amongst other things aims
>> to remove unnecessary differences between the C and C++ rules.
>>
>> Going back to your original example, however you argue it, its
>> non-compliant.
>>
>> * if you argue that x is a loop counter, then it violates 14.1 - but
>> this seems unreasonable as there is no sign of monotonic modification
>> * if you argue its not a loop counter, then it violates 14.2. The
>> condition expression of a well formed for loop must use the loop
>> counter, and z certainly isn't one. My while loop example doesn't
>> need to satisfy 14.2 (its not a for loop), and error isn't a loop
>> counter - so doesn't violate 14.1 (there is no evidence that it
>> changes monotonically)
>>
>> Clive
>>
>> PS: on a more practical level, I'm I right in assuming that for the
>> meeting next week in Brno, electrical sockets are going to be the usual
>> European standard?
>>
>>
>>
>> On Wed, Apr 18, 2018 at 9:27 PM, Martin Sebor <msebor at gmail.com
>> <mailto:msebor at gmail.com>> wrote:
>>
>> On 04/18/2018 01:03 PM, Clive Pygott wrote:
>>
>>
>> - 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.
>>
>>
>> I'm interested in learning how to decide which of the two it
>> is
>> for the simple examples we've seen in this thread. That seems
>> like a fairly elementary expectation for a discussion of
>> the merits of the rule.
>>
>>
>> Why are you arguing that this is undecidable?
>>
>>
>> I am not arguing that the rule is undecidable: it is marked as
>> such.
>>
>> Roberto explained that the reason why the rule is undecidable
>> is because the question of what exactly is a loop counter is
>> undecidable.
>>
>> The practical
>> interpretation of "/Its value varies monotonically on each
>> iteration
>> of a given instance of a loop//" is that if x is potentially the
>> loop
>> counter, then the code will use one of ++x x++ --x x--
>> x += n
>> x -= n x = x + n x = n + x or x = x - n where n
>> is a
>> constant. This is illustrated in the examples in the MISRA
>> document. /
>>
>>
>> Other expressions satisfy the monotonicity requirement (e.g.,
>> x *= 2). Many others might satisfy it under some conditions
>> (x /= y even if y is non-constant but in some positive range).
>>
>> But because whether or not a function is monotonic is, in general
>> undecidable (e.g., x *= y for an arbitrary y), as Roberto explained,
>> there is no reliable way to identify what's a loop counter. That
>> implies that the answer to whether my original example compliant
>> or even subject to the rule is unknown:
>>
>> void converge_on (double z)
>> {
>> for (double x = 0; x < z; )
>> x = foo (x);
>> }
>>
>> Same for your rewrite:
>>
>> void converge_on (double requiredPrecision)
>> {
>> double error = requiredPrecision +1.0;
>>
>> while (error > requiredPrecision)
>> error = iterate();
>> }
>>
>> /
>> /
>> /The only ambiguity about error is that we don't know what is in
>> iterate(). If it does something equivalent to one of the above
>> - it's a
>> loop counter, if it doesn't - it isn't. If the body of iterate
>> isn't
>> available (say its a library function), I'd expect it to be
>> reported as
>> a violation/
>>
>>
>> I find this sort of ambiguity unsatisfactory, for at least two
>> reasons:
>>
>> 1) It has taken a non-trivial amount of discussion to arrive
>> at the answers above. What chance do non-expert programmers
>> have of getting their code to comply?
>>
>> 2) The fundamental undecidability of what is a loop counter
>> means that some analyzers will complain about this simple
>> code while others will not. Not because some may be able
>> to see the body of iterate() and others may not be, but
>> because it's not clear which loops are meant to be subject
>> to the rule and which ones shouldn't.
>>
>> As a result, there would be way to write such simple loops and
>> comply with the standard, and so portable programs (portable
>> across analyzers) would need to find a different way to write
>> them. I don't think that would be helpful because it would
>> force unintuitive and so likely buggy) workarounds. (I have
>> seen that happen on a large scale with the adoption of Annex
>> K -- see N1969).
>>
>> That said, interpreting 14.1 to to apply in the constant cases
>> (i.e., only to loops whose counters are known to change
>> monotonically) would seemingly arbitrarily exclude loops that
>> change non-monotonically. If that's intended what is the
>> rationale?
>>
>> Martin
>>
>> /
>> /
>> / Clive/
>>
>>
>>
>>
>>
>>
>> On Wed, Apr 18, 2018 at 7:41 PM, Roberto Bagnara
>> <bagnara at cs.unipr.it <mailto:bagnara at cs.unipr.it>
>> <mailto:bagnara at cs.unipr.it <mailto:bagnara at cs.unipr.it>>> wrote:
>>
>> On 04/18/2018 08:18 PM, Martin Sebor wrote:
>> > On 04/18/2018 11:16 AM, Roberto Bagnara wrote:
>> >> 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.
>> >
>> > It was a typo -- I meant to say "has a floating type."
>>
>> OK.
>>
>> >>> 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:
>> >
>> > Yes, but MISRA's deviation process is only of peripheral
>> > interest to this group. The document we are working on
>> doesn't
>> > define such a process.
>>
>> Well, there are other MISRA documents (which can be freely
>> downloaded BTW) that define it more formally, but if you look
>> for the string "deviation" in MISRA C:2012 you will find.
>> What is more important is that the deviation process is
>> an integral, crucial part of applying the MISRA C coding
>> standard.
>> If this group still considers this of peripheral interest,
>> then I am afraid the group is wasting time.
>>
>> >> - 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.
>> >
>> > I'm interested in learning how to decide which of the two
>> it is
>> > for the simple examples we've seen in this thread. That
>> seems
>> > like a fairly elementary expectation for a discussion of
>> > the merits of the rule.
>>
>> The examples I have seen in this thread are not detailed
>> enough
>> to decide which entities occurring in them are loop counters.
>>
>> >> 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.
>> >
>> > It was my assumption that 14.1 was undecidable because of
>> the second
>> > sentence in the Rationale, i.e., because it's impossible
>> to determine
>> > whether a loop does or does not iterate the expected
>> number of times.
>> > (It's hard to tell from just a rationale and examples but
>> no single
>> > word of normative requirements.)
>>
>> The normative requirements for loop counters are spelled out
>> in
>> Section 8.14.
>>
>> > If 14.1 is undecidable because it's actually impossible to
>> reliably
>> > identify what is and what isn't a loop counter then the
>> rules that
>> > depend on the term are not just undecidable, they're
>> unimplementable
>> > in a way that will give consistent results across
>> analyzers even for
>> > basic test cases. (Different implementations will analyze
>> different
>> > pieces of code.)
>>
>> This is true for all undecidable rules.
>>
>> >> 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).
>> >
>> > Sorry, but saying that "this means something in between
>> these
>> > other two rules from different standards" is just a little
>> too
>> > vague for me.
>>
>> The two extremes were only provided to explain what I meant
>> by saying
>> that the set of MISRA C rules dealing with determinate
>> iteration is
>> (like most other sets of rules) a compromise. I thought that
>> illustrating two extremes of the range could help.
>>
>> --
>> Prof. Roberto Bagnara
>>
>> Applied Formal Methods Laboratory - University of Parma, Italy
>> mailto:bagnara at cs.unipr.it <mailto:bagnara at cs.unipr.it>
>> <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>
>> <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>
>> <mailto: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>
>>
>> <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
>> <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
>> <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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.trustable.io/pipermail/c-safe-secure-studygroup/attachments/20180419/86b370c5/attachment-0001.html>
More information about the C-safe-secure-studygroup
mailing list