[Termtools] About memory examples in C category
Akihisa Yamada
akihisa.yamada at uibk.ac.at
Tue Jul 21 16:17:49 CEST 2015
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
>
>
--
Akihisa Yamada, Ph.D.
Computational Logic Group, Institute of Computer Science,
University of Innsbruck
http://cl-informatik.uibk.ac.at/~ayamada/
More information about the Termtools
mailing list