more academic pointers
authorRalf Jung <post@ralfj.de>
Wed, 25 Jul 2018 14:32:38 +0000 (16:32 +0200)
committerRalf Jung <post@ralfj.de>
Wed, 25 Jul 2018 14:32:38 +0000 (16:32 +0200)
ralf/_posts/2018-07-24-pointers-and-bytes.md

index 64ea94b18b909a7a900358e5bd4d57d1b9eb1ac1..53daa57ce3a5a065bd35b39f51418eb2c144a321 100644 (file)
@@ -19,7 +19,7 @@ I hope that by the end of this post, you will agree with me on both of these sta
 ## Pointers Are Complicated
 
 What is the problem with "pointers are just integers"?  Let us consider the following example:<br>
 ## Pointers Are Complicated
 
 What is the problem with "pointers are just integers"?  Let us consider the following example:<br>
-(I am using C++ code here mostly because writing unsafe code is easier in C++, and unsafe code is where these problems really show up. C has all the same issues, as does unsafe Rust.)
+(I am using C++ code here mostly because writing unsafe code is easier in C++ than in Rust, and unsafe code is where these problems really show up. C has all the same issues, as does unsafe Rust.)
 {% highlight c++ %}
 int test() {
     auto x = new int[8];
 {% highlight c++ %}
 int test() {
     auto x = new int[8];
@@ -152,6 +152,8 @@ We mostly just ignore the problem in miri and opportunistically do as much as we
 A full definition of a language like C++ or Rust of course cannot take this shortcut, it has to explain what really happens here.
 To my knowledge, no satisfying solution exists, but academic research is [getting closer](http://sf.snu.ac.kr/publications/llvmtwin.pdf).
 
 A full definition of a language like C++ or Rust of course cannot take this shortcut, it has to explain what really happens here.
 To my knowledge, no satisfying solution exists, but academic research is [getting closer](http://sf.snu.ac.kr/publications/llvmtwin.pdf).
 
+**Update:** This was by no means meant to be an exhaustive list of academic research on C in general. I do not know of other work that focuses directly on the interplay of integer-pointer casts and optimizations, but other noteworthy work on formalizing C includes [KCC](https://github.com/kframework/c-semantics), [Robbert Krebber's PhD thesis](https://robbertkrebbers.nl/thesis.html) and [Cerberus](https://www.cl.cam.ac.uk/~pes20/cerberus/). **/Update**
+
 This is why pointers are not simple, either.
 
 ## From Pointers to Bytes
 This is why pointers are not simple, either.
 
 ## From Pointers to Bytes