[Termtools] About memory examples in C category
Akihisa Yamada
akihisa.yamada at uibk.ac.at
Sun Jul 19 23:16:10 CEST 2015
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
>
More information about the Termtools
mailing list