Exploring C semantics and pointer provenance
Exploring C semantics and pointer provenance
复制标题
探索 C 语义和指针起源
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Peter Sewell
中科院分区：
文献类型：
--
作者：
Kayvan Memarian;Victor B. F. Gomes;Brooks Davis;Stephen Kell;Alexander Richardson;R. Watson;Peter Sewell
C中指针和内存对象的语义多年来一直是一个争论不休的问题。C值不能被视为纯粹抽象或纯粹具体的实体：语言公开了它们的表示，但编译器优化依赖于对起源和初始化状态的分析，而不仅仅是运行时表示。ISO WG 14标准在这方面留下了许多不清楚的地方，并且在某些方面与事实上的标准用法不同-这本身就很难调查。在本文中，我们探讨了可能的源语言语义的内存对象和指针，在ISO C和C，因为它是在实践中使用和实现，特别是集中在指针出处。我们的目标是，尽可能地，调和ISO C标准，主流编译器的行为，以及现有的C代码语料库所依赖的语义。我们提出了两个连贯的建议，通过整数和不跟踪出处，都解决了许多设计问题。我们强调了一些优点和缺点以及开放性问题，并通过测试案例库来说明讨论。我们使我们的语义可执行作为一个测试的甲骨文，集成它与Cerberus语义的大部分其余的C，我们已经大大更完整和强大，并配备了一个Web界面GUI。这使我们能够在这些测试案例上通过实验评估我们的建议。为了评估它们在更大的C代码体中的可行性，我们分析了FreeBSD到CHERI的一个端口所需的更改和由此产生的行为，CHERI是一个支持硬件功能的研究架构，它（粗略地说）捕获了我们的建议认为未定义行为的内存安全违规行为。我们还开发了一个新的运行时检测工具，以检测可能的起源违反正常的C代码，并将其应用到一些SPEC基准。我们将我们的建议与Lee等人的双分配LLVM语义建议的源语言变体进行比较。最后，我们描述了与WG 14正在进行的交互，探索如何将我们的建议纳入ISO标准。
The semantics of pointers and memory objects in C has been a vexed question for many years. C values cannot be treated as either purely abstract or purely 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 WG14 standard leaves much of this unclear, and in some respects differs with de facto standard usage --- which itself is difficult to investigate. In this paper we explore the possible source-language semantics for memory objects and pointers, in ISO C and in C as it is used and implemented in practice, focussing especially on pointer provenance. We aim to, as far as possible, reconcile the ISO C standard, mainstream compiler behaviour, and the semantics relied on by the corpus of existing C code. We present two coherent proposals, tracking provenance via integers and not; both address many design questions. We highlight some pros and cons and open questions, and illustrate the discussion with a library of test cases. We make our semantics executable as a test oracle, integrating it with the Cerberus semantics for much of the rest of C, which we have made substantially more complete and robust, and equipped with a web-interface GUI. This allows us to experimentally assess our proposals on those test cases. To assess their viability with respect to larger bodies of C code, we analyse the changes required and the resulting behaviour for a port of FreeBSD to CHERI, a research architecture supporting hardware capabilities, which (roughly speaking) traps on the memory safety violations which our proposals deem undefined behaviour. We also develop a new runtime instrumentation tool to detect possible provenance violations in normal C code, and apply it to some of the SPEC benchmarks. We compare our proposal with a source-language variant of the twin-allocation LLVM semantics proposal of Lee et al. Finally, we describe ongoing interactions with WG14, exploring how our proposals could be incorporated into the ISO standard.