[Termtools] About memory examples in C category
Thomas Ströder
stroeder at informatik.rwth-aachen.de
Mon Jul 27 13:29:34 CEST 2015
Dear Akihisa,
I agree with you. What about the following additional rule:
"Programs where the evaluation order of operations is not defined
according to the C standard are not allowed. As an example, the program
int main(){
int x = 0;
while( x++ == x );
}
is not allowed since the evaluation order between ++ and == is not
defined according to the C standard."
Would all participants of the C category be fine with that rule or do
you see problems with it? If all participants agree, I would add it to
the rules on termination-portal.
Best regards,
Thomas
Am 21.07.2015 um 16:17 schrieb Akihisa Yamada:
> Dear Jürgen,
>
> great, then I'll do this update.
>
> For the future rule, I'd like to propose also forbidding programs that
> depends on unspecified behavior, such as
>
> int main(){
> int x = 0;
> while( x++ == x );
> }
>
> Evaluation order of function arguments are specified only for
> "||" "&&" "," and "_:_?", so the above program can be both
> terminating (if left-hand side comes first) and
> nonterminating (if right-hand side comes first).
>
> Cf. http://en.cppreference.com/w/c/language/eval_order
>
> Best regards,
> Akihisa
>
> On 2015/07/21 15:46, Juergen Giesl wrote:
>> Dear Akihisa,
>>
>> you're right. I also think that it would be good to make
>> initializiations explicit. Then all statements of the form
>>
>>
>> int* x = alloca(sizeof(int));
>> int i = *x;
>>
>>
>> in the examples would have to be replaced by
>>
>>
>> int* x = alloca(sizeof(int));
>> *x = __VERIFIER_nondet_int();
>> int i = *x;
>>
>>
>> Moreover, one should then add a corresponding rule for the C category
>> which forbids examples where one accesses such non-initialized values.
>>
>> Best Regards
>> Juergen
>>
>>
>>
>>
>> 2015-07-19 23:16 GMT+02:00 Akihisa Yamada <akihisa.yamada at uibk.ac.at
>> <mailto:akihisa.yamada at uibk.ac.at>>:
>>
>> Dear Juergen and all,
>>
>> oh sorry, I was concerning not memory safety here, but the undefined
>> behavior of accessing uninitialized values. (And indeed, this is also
>> undecidable in general.)
>>
>> My concern is that, if I understand the C standard correctly,
>>
>> int* x = alloca(sizeof(int));
>> int i = *x;
>>
>> leads to an undefined behavior, not just unspecified value is
>> substituted to i. So it is not equivalent to the well-defined:
>>
>> int* x = alloca(sizeof(int));
>> *x = __VERIFIER_nondet_int();
>> int i = *x;
>>
>> As the later seems to be intended, I would agree with Ton-Chanh's
>> suggestion for making the initialization explicit.
>>
>> Best regards,
>> Akihisa
>>
>> On 2015/07/19 21:50, Juergen Giesl wrote:
>>
>> Dear all,
>>
>> I'm not really convinced by the argument that memory unsafety
>> can be
>> eliminated by coding rules. This is an undecidable property,
>> just like
>> termination. Thus, it makes sense to check this property
>> automatically,
>> I think. But of course there could also be an additional
>> category where
>> memory safety can be assumed.
>>
>> Best Regards
>> Juergen
>>
>> Am 19.07.2015 20:43 schrieb "Akihisa Yamada"
>> <akihisa.yamada at uibk.ac.at <mailto:akihisa.yamada at uibk.ac.at>
>> <mailto:akihisa.yamada at uibk.ac.at
>> <mailto:akihisa.yamada at uibk.ac.at>>>:
>>
>> Dear all,
>>
>> - Although "allocation of memory always succeeds", how
>> about the
>> value of the allocated memory cell? Is it a
>> non-deterministic value?
>>
>>
>> it seems natural that neither YES or NO is correct in such
>> cases, since
>> the C standard identifies the case "The value of the object
>> allocated
>> by the malloc function is used" in Annex J.2 "Undefined
>> Behavior",
>> not just "Unspecified".
>> Cf.
>> http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf
>>
>> Of course I have no request on how these will be treated
>> in the
>> coming competition, since I'm not involved in the
>> category. :)
>>
>> But as a former C developer, I personally feel having
>> "defined" C
>> category is nice in the future, since undefined behavior
>> can be
>> eliminated by coding rules etc.
>>
>> Best regards,
>> Akihisa
>>
>> On 2015/07/19 19:51, Thomas Ströder wrote:
>>
>> Dear all,
>>
>> Am 19.07.2015 um 16:33 schrieb Ton-Chanh Le:
>>
>> Dear Yamada,
>>
>> Thank you very much for pointing out the rule.
>>
>> We asked the question as the rule also mentioned
>> that "we could also offer an additional category
>> where
>> memory safety can be assumed" and we did not know
>> whether that category is implemented in this
>> competition
>> or not.
>>
>>
>> Currently, there is no additional category where memory
>> safety
>> can be
>> assumed. If there is enough interest in it, we could
>> build up such a
>> category for the next competition (we would need to
>> gather suitable
>> examples and/or check existing ones).
>>
>> Regarding to the rule for C programs, we would
>> like to
>> clarify some points:
>>
>> - The rule says that "neither YES nor NO is a
>> correct result
>> for programs violating memory safety", does this
>> mean
>> the expected result in this case is MAYBE?
>>
>>
>> Yes. Such examples won't yield any points, but can lead
>> to a
>> penalty if
>> claimed to be proven to (non-)terminate. Together
>> with some
>> people from
>> SV-COMP, I had a little discussion about this rule. The
>> question is
>> whether the property "non-termination" means that you
>> can definitely
>> reach a non-terminating run or whether it is the
>> negation of the
>> property "termination". Another related question is
>> whether
>> undefined
>> behavior means that everything counts as definitely
>> reachable
>> behavior.
>> Both answers to these questions have their pros and
>> cons.
>> Currently, the
>> interpretation at termCOMP is that "non-termination"
>> means that a
>> non-terminating run can definitely be reached and
>> undefined behavior
>> does not give you any guarantee of what can be reached.
>> Hence, only
>> MAYBE is a correct answer for memory-unsafe examples
>> (but since
>> MAYBE
>> does not require any proof, this answer gives no
>> points).
>>
>> I would neither vote for nor against changing this
>> rule, but if the
>> majority of participants would be in favor of changing
>> the rule such
>> that violation of memory-safety implies
>> non-termination, I think we
>> could do this (not sure whether this would already work
>> for the
>> current
>> competition, but it would definitely be possible for
>> future
>> editions).
>> However, violation of memory-safety would not include
>> memory
>> leaks as
>> these do not lead to undefined behavior and, thus, do
>> not influence
>> termination behavior.
>>
>> - Although "allocation of memory always succeeds",
>> how about the
>> value of the allocated memory cell? Is it a
>> non-deterministic value?
>>
>>
>> Yes.
>>
>> Thank you very much.
>>
>> Best Regards,
>>
>> Le Ton Chanh
>> Email: chanhle at comp.nus.edu.sg
>> <http://comp.nus.edu.sg> <http://comp.nus.edu.sg>
>> <http://comp.nus.edu.sg>
>>
>>
>> Best regards,
>>
>> Thomas
>>
>>
>> On Sun, Jul 19, 2015 at 8:19 PM, Akihisa Yamada
>> <akihisa.yamada at uibk.ac.at
>> <mailto:akihisa.yamada at uibk.ac.at>
>> <mailto:akihisa.yamada at uibk.ac.at
>> <mailto:akihisa.yamada at uibk.ac.at>>
>> <mailto:akihisa.yamada at uibk.ac.at
>> <mailto:akihisa.yamada at uibk.ac.at>
>> <mailto:akihisa.yamada at uibk.ac.at
>> <mailto:akihisa.yamada at uibk.ac.at>>>> wrote:
>>
>> Dear Le Ton Chanh,
>>
>> your question seems to be discussed in the
>> competition
>> rule:
>> http://termination-portal.org/wiki/C_Programs
>>
>> Best regards,
>> Akihisa
>>
>>
>> On 2015/07/16 4:36, Ton-Chanh Le wrote:
>>
>> Dear PC members,
>>
>> I would like to ask whether we have the
>> assumption
>> that the pointer examples in the C
>> category is
>> memory safe or we need to prove memory
>> safety
>> prior to termination proofs.
>>
>> Thank you.
>>
>> Best Regards,
>>
>> Le Ton Chanh
>> Email: chanhle at comp.nus.edu.sg
>> <http://comp.nus.edu.sg>
>> <http://comp.nus.edu.sg> <http://comp.nus.edu.sg>
>> <http://comp.nus.edu.sg>
>>
>>
>>
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lists.lri.fr <mailto:Termtools at lists.lri.fr>
>> <mailto:Termtools at lists.lri.fr <mailto:Termtools at lists.lri.fr>>
>> <mailto:Termtools at lists.lri.fr
>> <mailto:Termtools at lists.lri.fr> <mailto:Termtools at lists.lri.fr
>> <mailto:Termtools at lists.lri.fr>>>
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>>
>>
>>
>>
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lists.lri.fr <mailto:Termtools at lists.lri.fr>
>> <mailto:Termtools at lists.lri.fr <mailto:Termtools at lists.lri.fr>>
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>>
>>
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lists.lri.fr <mailto:Termtools at lists.lri.fr>
>> <mailto:Termtools at lists.lri.fr <mailto:Termtools at lists.lri.fr>>
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>>
>>
>
--
Thomas Ströder mailto:stroeder at informatik.rwth-aachen.de
LuFG Informatik 2 http://verify.rwth-aachen.de/stroeder
RWTH Aachen phone: +49 241 80-21241
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150727/4d1ad3b9/attachment.sig>
More information about the Termtools
mailing list