From 6e9cb706fd83fdfe656134c1f4baf9048d23ec00 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 25 Jul 2018 12:47:56 +0200 Subject: [PATCH] clarify that what miri does not not a reasonable choice for language semantics --- personal/_posts/2018-07-24-pointers-and-bytes.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/personal/_posts/2018-07-24-pointers-and-bytes.md b/personal/_posts/2018-07-24-pointers-and-bytes.md index 5d6b60d..64ea94b 100644 --- a/personal/_posts/2018-07-24-pointers-and-bytes.md +++ b/personal/_posts/2018-07-24-pointers-and-bytes.md @@ -137,8 +137,10 @@ However, this simple model starts to fall apart once you consider pointer-intege In miri, casting a pointer to an integer does not actually do anything, we now just have an integer variable (i.e., its *type* says it is an integer) whose *value* is a pointer (i.e., an allocation-offset pair). However, multiplying that "integer" by 2 leads to an error, because it is entirely unclear what it means to multiply such an abstract pointer by 2. -This is the most lazy thing to do, and we do it because it is not clear what else to do (other than not supporting these casts at all -- but this way, miri can run more programs). -In our abstract machine, there is no single coherent "address space" that all allocations live in, that we could use to map every pointer to a distinct integer. +I should clarify that this is *not* a good solution when defining language semantics. +It works fine for an interpreter though. +It is the most lazy thing to do, and we do it because it is not clear what else to do (other than not supporting these casts at all -- but this way, miri can run more programs): +In our abstract machine, there just is no single coherent "address space" that all allocations live in, that we could use to map every pointer to a distinct integer. Every allocation is just identified by an (unobservable) ID. We could now start to enrich this model with extra data like a base address for each allocation, and somehow use that when casting an integer back to a pointer... but that's where it gets really complicated, and anyway discussing such a model is not the point of this post. The point it to discuss the *need* for such a model. -- 2.30.2