Скачать или смотреть Towards Clear Memory Object Semantics for ISO and De Facto C - GNU Tools Cauldron 2018

Presented by Peter Sewell at GNU Tools Cauldron 2018

The semantics of pointers and memory objects in C has been a vexed question for many years. C values cannot be treated as simple abstract or concrete entities: the language exposes their representations, but compiler optimisations rely on analyses that reason about provenance and initialisation status, not just runtime representations. The ISO standard leaves much of this unclear, and in some aspects differs with de facto standard usage - which itself is difficult to investigate.

This talk will describe the issues involved in defining a clear source-language semantics for pointers and memory objects, focussing especially on pointer provenance. We aim ultimately to reconcile the ISO C standard, mainstream compiler behaviour, and the semantics relied on by the corpus of existing C code.

It will also describe how a proposed semantics has been made executable as a test oracle (to calculate all the semantics-allowed executions of small tests), by integrating it with the Cerberus semantics for much of the rest of C, and preliminary experimental work to assess what code out there depends on.

The talk will be a revised version of a keynote given at EuroLLVM 2018, informed by discussion with the recently created ISO WG14 C Memory Object Model Study Group. We would be very interested to get feedback from the broader GCC community about these issues.

This is joint work with Kayvan Memarian, Victor B. F. Gomes, Stephen Kell, Brooks Davis, Robert Watson, Alex Richardson, and members of the ISO WG14 C Memory Object Model Study Group.