[Termtools] About memory examples in C category
Juergen Giesl
giesl at informatik.rwth-aachen.de
Tue Jul 21 15:46:48 CEST 2015
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>:
> 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>>:
>>
>> 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>
>>
>>
>> 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>>> 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>
>>
>>
>> _______________________________________________
>> 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>
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>>
>>
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lists.lri.fr <mailto:Termtools at lists.lri.fr>
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150721/e53f5e83/attachment-0001.html>
More information about the Termtools
mailing list