-
Notifications
You must be signed in to change notification settings - Fork 59
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Must let
variables (without mut
or UnsafeCell
) be read-only?
#400
Comments
I would certain like for it to be undefined behaviour for a few reasons:
The definiton could rule out using let x = true;
if false{
unsafe{call_opaque_function(addr_of!(x))} // does this affect the closure layout?
}
(|| println!("{}",{x}))(); (loops do even more wacky things) |
Right, that is the key optimization difference here (for the case where the opaque fn call takes that ptr-to-x as argument). I just don't think this optimization is important enough to justify introducing a whole new kind of read-only allocation. Specifying these "read-only" locals will be tricky since of course they are written to, even more than once, to receive their initial value: let x: (i32, i32);
x.0 = 0;
x.1 = 1; I think we do want
This issue here is only relevant for cases where the address is taken so this seems to be orthogonal. Also I am fairly sure we don't want any rules that look anything like this in our op.sem. "Local has its address taken" is not a property that is stable under optimizations. Capture elision, like other optimizations, should fall out of the general properties of the model -- it should not itself be part of the spec. |
On Sun, May 14, 2023 at 10:38 Ralf Jung ***@***.***> wrote:
the value of the local to be optimized past an opaque function call given
addr_of!(x) rather than &x
Right, that is the key optimization difference here (for the case where
the opaque fn call takes that ptr-to-x as argument).
I just don't think this optimization is important enough to justify
introducing a whole new kind of read-only allocation. Specifying these
"read-only" locals will be tricky since of course they are written to, even
more than once, to receive their initial value:
let x: (i32, i32);
x.0 = 0;
x.1 = 1;
I think we *do* want addr_of!/addr_of_mut! to *not* generate a fresh tag
and just return an exact alias of the pointer they start with. This is
pretty much required to fix #134
<#134>. If we
take that as a given then making addr_of!(local) *not* mutable cannot be
done by the aliasing model, it has to be a property of the allocation
itself. Moreover the allocation cannot be read-only, it would have to be
something like write-once... or we need an explicit MIR statement saying
"now mark this memory read-only" (because it has been initialized).
Hmm... Yeah. Partial Init is a problem. For full init, the allocation
itself could come into existence when it's initialized possibly. My main
reasons I would like it is if it's initialized with a constant expression
(or, at least, something I can evaluate as one), but separating that
circumstance is definitely challenging.
If the nth capture does not have it's address taken by the closure body,
and is a non-mutable binding initialized by a constant expression
This issue here is only relevant for cases where the address is taken so
this seems to be orthogonal.
Right, but the difference here is whether the address is taken outside of
the closure or inside. I'd really like to be able to make the capture rules
for layout purposes only care about the initial declaration of the binding
and the body of the closure itself.
Also I am fairly sure we don't want any rules that look anything like this
in our op.sem. "Local has its address taken" is *not* a property that is
stable under optimizations. Capture elision, like other optimizations,
should fall out of the general properties of the model -- it should not
itself be part of the spec.
Yeah, I should have clarified, this is a potential rule in a future version
of lccc's abi spec, not rust. It does apply it's decision making
pre-optimization, since the point is that optimizations shouldn't affect
something that can move across cgu's in an unstable way. I'd like to be
able to justify having that rule in the first instance, since imo
const-propagation capture ellision is a useful layout optimization, and
that rule is a non-complex way of defining it.
… —
Reply to this email directly, view it on GitHub
<#400 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ABGLD2ZOCFSHBIVIU7SNWE3XGDU53ANCNFSM6AAAAAAYBC4KBA>
.
You are receiving this because you commented.Message ID:
***@***.***>
|
Another related but I think distinct potential reason to prohibit mutation of a Basically, being able to constant-propagate a static promotion as an optimization, rather than requiring the developer to notice it can be and ask for it to be const evaluated to get access to the potential promotion benefit. Footnotes
|
We can just not do that promotion if we see an |
As the maintainer, co-author, and also user of an unsettling and increasing amount of let x = 5;
let stuff = construct!(x);
stuff.do_something();
assert_ne!(x, 5);
println!("if this code is reached, modular reasoning got axed."); I would prefer the assert-not-equals line to always trigger its associated panic. And I do pass (via pointer) a considerable number of values to FFI that are then left unmodified, and I would prefer that I not have to reason carefully about optimization rules when picking between |
No unsafe code programming problem is made better by adding more UB. So I am not sure what you are arguing for here. |
Making it defined means promising to compile it which means people will start introducing things which rely on it working. |
Making it undefined is worse, it turns this into non-debuggable bugs. UB exists for optimizations and nothing else. (And sometimes as a way to paper over platform differences that we haven't found a better way to explain away yet.) Using it for anything else is just the worst kind of bug amplification.
We're talking at the level of validity invariants here, not safety invariants. If you write a library abstraction, the client's rules (safety invariant) are yours to define and default to "what can be done in safe code". Safe code cannot mutate these variables, so your libraries are not affected.
|
In practice people do in fact notice and report "the compiler discarded a write" when they pass
And in practice, people do write macros that expand to And programmers are not unwilling to brute-force-search for code that works. |
basically, in order for someone to reason "xyz var is never mutated", even if they know the monomorphic type, they must now prove a negative: no one ever used comparatively, the search for "is this |
...I suppose they could also declare every single "no, really, it's immutable" variable as a constant but perhaps Rust programmers would rather not |
We're discussing the reasoning principles permitted to the compiler here, not the reasoning principles permitted to programmers.
That's a doomed approach in a language with UB, it makes zero sense to try to account for it. Furthermore, even if we did add the extra UB you are asking for, things would still seem to "work" in many cases when you don't want them to. So this argument doesn't even support (my understanding of) your position.
These are true statements and I fail to see the relation to this discussion. People also write safe functions that contain unsafe blocks that cause UB -- people have bugs in their code. The notion of soundness for macros is a bit unclear, but certainly does not involve having to study the code the macro expands to, any more than the notion of soundness of a safe function involves having to study the code inside that function. I honestly don't understand what kind of API you're even concerned about here. The code you sketched above doesn't help me. But as a general principle there are large priors against a soundness concern motivating more UB. That's like fixing someone's trouble with their door handle by just blowing up the entire car. |
I copied this into the playground and it doesn't compile (E0381 'partially assigned binding As far as I can tell, it is also impossible to take a pointer to an uninitialized let binding. If you cannot write to a let binding more than once as it's initialization and you cannot take a pointer to an uninitialized let binding, then any pointer to a let binding must have already be initialized and therefore allowing writing to it would be as surprising as allowing writes to an initialized let binding directly (eg allowing |
There was a proposal to allow this, though I can't find it right now. It's a fairly natural language extension that we shouldn't prevent: basically, just treat initialization entirely per-field, and once all fields are initialized, consider the entire value initialized. Also, even just the single write that we already permit to let x: i32;
if b { x = 13; } Also, for MIR semantics we definitely want to permit deaggregation, where this let x: (i32, i32);
x = (0, 1); gets transformed into let x: (i32, i32);
x.0 = 0;
x.1 = 1; |
Partial initialization is still kinda besides the point if you can only take a pointer to a let binding statically known to be fully initialized. |
No, taking a pointer is besides the point. ;) The allocation exists already before the pointer gets created. We're not going to have completely different operational semantics for |
this issue has allowing
as its central question and i'm saying that allowing it would be as surprising as allowing
and unitialized let bindings are already 'special'. |
I'm saying that if a pointer can be taken then the weirdness with uninitialized let bindings is already over. |
FTR, in lccc currently I do distinguish between locals that have and have not had their address taken (though currently not for aggregates, I need to add an A similar model could theoretically be used in Minirust to achieve the required/desired semantics. |
You're thinking in terms of surface Rust, but that's not how it works in the operational semantics. In MIR, there isn't even a difference between
No idea which point you're trying to make here. We need one rule for what happens at a write to a place, treating all places uniformly. We don't even know we're writing to a local variable when we do the I suggest making yourself familiar with MiniRust or a similar operational model. Just jumping into a deeply technical discussion can be confusing and cause confusion when you're not familiar with the technical background.
Miri uses such a model to be a bit faster. |
So far there has been one proposal for an op.sem that actually makes these writes to Absent that, the best model I can think of is to introduce a new statement in MIR that says "this variable is now initialized" and marks the corresponding memory allocation as read-only. But I don't see sufficient motivation to add such a statement, and I don't know how hard it would be to make MIR building emit such a statement. |
Fair enough that including the opt by-spec is potentially a pain.
IE. Edit: Though this has one hole: Primitive slice/array indexes. |
|
If you canonize this: let x = 0i32;
let ptr = addr_of!(x) as *mut i32;
*ptr = 42; then programmers will be allowed to reason based on it. Indeed, they will be forced to. |
There's a lot of things that are awkward to reason about as programmers that is well-defined. Enum variants and |
Yes, knowing the type is required, and? |
Part of my complaint is that if this optimizes differently: let x = 5;
ffi_call(&x);
let y = x + 5; than this: let x = 5;
ffi_call(ptr::addr_of!(x));
let y = x + 5; then now I can't tell people they should just prefer to use |
Rude. I'm already familiar with MiniRust. But I suppose I must have been unclear.
Assuming:
Then the choice of operational semantic can only possibly impact a programmer writing surface rust by deciding whether an initialized let binding is read-only or read-write. I see a couple options for lowering let bindings:
The chosen semantics would be useful for verifying the lowering of surface rust or for allowing a easier path to new language features like partial initialization. but right now, as uninitialized let bindings are fully encapsulated by surface rust, the only impact the chosen operational semantics can have on programmers writing surface rust is the behavior of code like this: let x = 0;
let ptr = addr_of!(x);
unsafe { *ptr = 42 }; tldr: i don't care what specific operational semantic we choose, but we can and should make writing to an initialized let binding UB detectable by our existing tooling. |
To echo Calvin and Jubille, I do not think it is worth the confusion to allow mutating initialized let bindings (via pointer or any other way aside from interior mutability).
But you think it is worth the confusion of Heisenbugs and miscompilations to achieve this?
To be abundantly clear, there is no program that becomes easier to reason about with more UB! You are just adding more proof obligstions to the pile of things people have to worry about before basic things like debugging work reliably.
If you are passing a raw const ptr to someone else's code, and that code has a bug and does a write when it should not, this is still easier to debug (outside Miri) when there is less UB, not more!
in safe code Rust guarantees that let bindings are written to at most once
You're asking to add nontrivial complications to the spec that underpins Rust (write-once memory would have to be added in the memory model, already a quite complicated part of Rust) which will cost many people a cumulative amount of countless hours to read and understand. And what you get out of that is largely more head scratching when people have their code miscompiled. I call that a lose-lose situation.
I can sometimes see the appeal of more UB for more "structure", but certainly not when it requires adding entirely new ghost state to the language, like per byte tracking of mutability (to support initializing one field and then another)!
I really don't understand why people want to go out of their way and make the spec quite a bit more complicated just to inflict the pain of more UB on our fellow Rustaceans. This should have an extremely high bar to pass.
|
If the goal is to make Miri flag more things, then we should be talking about "erroneous behavior" (that's what C++ calls it), not Undefined or Defined behavior. Erroneous behavior means: when this happens it's a bug, and then either execution stops or it continues just fine, but no extra assumptions or optimizations can be made by the compiler. If the program doesn't abort, it continues in an entirely well-defined way. You are making some valid arguments for why writing to non-interior-mutable |
I am treating the author of the macro as potentially adversarial to the author of the code. This can remain true even if they are the same person. I find that it is often the case that I must adopt this quasi-adversarial stance in order to understand how to rectify questionably-written I can, without a doubt, guarantee you that there is more than one way to introduce a Heisenbug. |
@workingjubilee I can just repeat asking you for a fully concrete example. I asked before, but you're still just talking in generalities that are impossible to confirm or refute. I can't look into your head to see what you think would be harder to easier to audit. Until I am given a counterexample, I maintain my claim that all else being equal, adding more UB can never make anything easier to audit. (I think that's a theorem: if |
I provided one, did I not? let x = 5;
let stuff = construct!(x);
stuff.do_something();
assert_ne!(x, 5);
println!("if this code is reached, modular reasoning got axed."); The internal implementation of Oh, and yes, they're libraries that produce libraries that do IPC. |
This comment was marked as off-topic.
This comment was marked as off-topic.
This comment was marked as off-topic.
This comment was marked as off-topic.
This comment was marked as off-topic.
This comment was marked as off-topic.
This comment was marked as off-topic.
This comment was marked as off-topic.
This comment was marked as off-topic.
This comment was marked as off-topic.
This comment was marked as off-topic.
This comment was marked as off-topic.
@RalfJung "proc macros with mazy implementations that then expand into mazy code that are used as part of a library that is used to implement libraries that that get dlopened and do IPC over shmem" is an actual, no-shit, stone-faced description of what I work on. |
I guess I can't help myself so I'll write a reply before likely unsubscribing to protect my sanity. Someone please ping me when things cooled down. It's not entirely clear to me who's reasoning about what in your example. That's what I was asking you to explain. Making it an actual self-contained example that people not in your brain can understand. I was not asking you to explain how to conjure Cthulu, even if conjuring Cthulu is your dayjob. I guess it's about Let's see how this fares Without
|
Attempting to get this conversation off of the above discussion, I'm going to remake my points actually in favour of having UB here, though more concise and specific:
There should logically be a way to make "immutable after initialization" work in a reasonable way - I'd expect it would be simpler to modify |
This is a bit of an essay, sorry. I marked the most important takeaway, with the TL;DR being that I'm in support of the OP example being defined behavior. There is a weird semantic space where mutating a non- To @workingjubilee's point, as I understand it: let place: i32 = 0;
macro_from_upstream_library!(place);
assert_eq!(place, 0); Answering the issue title's question as no and declaring the OP's example as defined behavior would mean that this assertion could panic in valid executions. However, if it did, the macro would be unsound. Macros are absolutely allowed to expand to internally encapsulated When reasoning about what other code (outside the safety boundary, whatever you've locally defined that to be) can do, the question isn't about language validity and what is or isn't UB, it's about safety invariants, which are much stricter than simple validity. (Aside: I think I want to write (another) blog post on the idea of and separation between the concepts of validity and safety. It comes up and I've re-explained it frequently enough that I'd like to have a stable reference that I can point to that covers just that difference specifically.)
There is some level of cooperation which you have to assume, and that cooperation is that upstream is sound. If you can't assume that, upstream could just The correct model that Rust helps with is explicitly not an adversarial upstream. An ignorant and/or negligent upstream, sure, but upstream is always presumed to be competent, cognizant, and cooperative enough to maintain the soundness of the interface. In fact, allowing mutation helps with the case of negligent upstream, because now if they use That is the primary issue with UB — you can't reliably debug it when it happens. The main problem with how we're understanding your position is that you're apparently claiming that UB is preferable to a defined but semantically wrong result. This is a very confusing position to hold, because while you can debug a wrong result, you fundamentally can't debug a UB. Perhaps the convenience of Miri as a sanitizer works against us here. UB is not equivalent to diagnosed by Miri. UB should always be thought of as perhaps the exact opposite — daemonic nondeterminism that chooses between time traveling and changing previous control flow choices, the most sensitive data accessible by the machine, the "correct" result, or a crash, whichever is worst for you at the moment, non-exhaustively. "Forbid it, diagnose it as forbidden whenever possible, but as a mitigation permit it when it can't be prevented" is a defensible position. "Eat my laundry if I dare make a mistake" less so. To the second form of the point mentioned both by Jubilee and Calvin, between lib_call(&place); // or
lib_call(addr_of!(place)); // where
// extern fn lib_call(_: *const Type); I would still recommend using If a developer chooses to use In fairness, I absolutely could see Miri in a conservative mode (e.g. under cargo-careful) choosing to warn when If we had a formal classification for "forbidden but still with predictably defined behavior of the 'obvious' semantics or a crash," it could make sense to place this there. Exposed provenance is mostly in that bucket, I believe. But it isn't necessary to formally have that bucket in order to diagnose it. Miri isn't UBSAN which (in theory) accepts all valid programs and rejects most invalid; Miri (in theory) rejects all invalid programs and accepts a majority of valid ones. This might be "erroneous behavior." It might be "safe misbehavior." Maybe we should try to build such a catorization as we stabilize the strict provenance APIs and start moving towards supporting CHERI as an experimental target. But making it UB will never make Jubilee's million-line maze easier to manage, and can only make it more difficult to debug. I will even agree that any code written that deliberately relies on this being DB should be immediately fixed with priority equal to that of latent UB. Code which relies on the "wide" (or "infectious") model for shared mutability instead of wrapping things in None of these things are DB because we endorse doing them. They're DB because all else being equal, we prefer more things being DB. Just because you can doesn't mean you should, and we consistently make the nicer and more straightforward way to accomplish these things available at the same time as or before we canonicalize that the circuitous way is actually guaranteed to work instead of just working by happenstance. To @Calvin304's primary point about initialization tracking: I don't know at what point uninitialized bindings are currently diagnosed. However, with the shifts to use THIR unsafeck and MIR borrowck, the trend is to push these analyses later in the compilation pipeline. MIR does actually know a difference between I intuitively expect that if/when the language is extended to support piecewise initialization of Thus, once that analysis is done, it basically just becomes an implementation choice whether that information is validated in THIR then discarded or if it's passed along into MIR. We already have The benefits of immutable-after-init For such to exist in the TB model, the "root" tag for So, with that in mind, reducing the question of the OP to absurdity, it really does boil down to: If, given some My personal position and answer to the question is the following three-phase conditional:
The points/arguments I make elsewhere throughout this comment are why I agree with Ralf here that the example in the OP should be defined behavior. The most relevant point is that Separately, I also think an initial intuition can reasonably expect a binding's place mention to behave like While I absolutely agree with the sentiment of #2573, I do wonder whether the perception of Drawing from a Rust background, I5 don't expect to be able to modify through an So in (not particularly useful) C++ terms, the question is whether Perhaps more usefully (despite being less strictly correspondent), it depends on whether the C++ developer learning Rust sees As one last wrinkle, though, I've only really considered IMPORTANT TAKEAWAY BEGIN So the question finally becomes, after defining If you want errors to be detectable, you want them to not be UB. Being DB does not mean you as a developer have to tolerate it; it means the compiler has to tolerate it. Being UB doesn't mean a rushed developer is any less prone to making mistakes; it means that determining that and how they did is miles more difficult. IMPORTANT TAKEAWAY END Post-script response to @chorman0773's point: (it took >6h to write this 🙃) It's already fundamentally the case throughout Rust's semantics that simple inorder translation isn't sufficient. I don't think making one small part of the translation easier should inform any surface language visible decisions. E.g. type inference is a full-function process, so I don't see how capture elision could happen without having done full-function analysis already. Also, it seems like your eager SSA form lowering Modifying
The "proper" solution is for lccc to have an xlang optimization pass that replaces alloca with SSA form where possible and desirable. Given that needs to exist anyway if you do any optimization on the xlang form, it seems like the benefit of deferring alloca when lowering MIR to xlang is quite minimal. Especially with how eagerly surface Rust creates references. The only real potential benefit I see is in capture elision, turning by-reference capture of Final afterthought: the above prompted me to think about how closure capture is dependent on I don't think there's a fair alternative which still captures a borrow lifetime. That we do precise field capture for closures limits the impact (i.e. capturing for Footnotes
|
Note that the deference happens in the MIR level (lccc's rust frontend has its own MIR). It actually makes some reasoning (like init-tracking) easier as well, since the lowering just inherently will error on an uninit memory location. This is then lowered to using the xlang stack (note, not the call stack at the hardware level) through use of
I'd personally choose the former, though I'd rather have neither constraint. As to the capture rules, the main issue is I can't have local optimization-dependent type layout - and I need to define type layout very exactly, in terms of (post-mono, fully-inferred) surface rust (I cannot refer to dynamic-only semantics). Closures are no exception, and in fact, their layout rules for a backbone for most of the anonymous types, given that generators and async blocks/async functions use the same capture-for-layout-purposes rules. |
Although I'm certain lccc isn't particularly enthused about it, since you're trying so hard to have a more stable ABI than Rustc provides, the semantics of Rust should not be beholden to implementations that want to provide stronger guarantees than provided by the language. If you'll forgive the hyperbole, this is how a lang gets into the pit that C and C++ find themselves in — the language provides no guarantees for ABI (has no concept of compiled objects, only linking based on surface language semantics), but can't make otherwise desirable changes because it might require a deliberately fragile compiler implementation to break ABI. Because Rust layout and ABI is unspecified, it's entirely okay if the language relies on that to be able to get reasonable performance characteristics. And anyway, if you want to specify the captures of a witness table in terms of surface language semantics, the obviously correct answer is to just include each reference that gets captured. Attempting to do stably observable guaranteed promotion is a poor idea. Rustc does some of a similar promotion where In fact, I don't think rustc ever optimizes closure captures beyond the naive capture semantics, even for capturing every field of a binding independently. And while the size of TL;DR: While alternative implementations can and should inform decisions, those alternative implementations choosing to tie their own feet more than necessary shouldn't restrict the main language from benefitting from the flexibility it deliberately reserves. (A plea to "lccc Rust" — at least for anonymous closure/ |
@CAD97 I too drafted a much longer explanation, but the part of the problem is that I understand everything you're saying, and the actual communication gap is that scale is not an isolated quantity of the discussion, to be torn away so someone can refute it in isolation. The problem is that in my experience, the code doesn't necessarily become more sound if the mutation is permitted, because later code may be relying on that immutability. For, yes, soundness reasons. "Everything is a big mesh of horrible, hard-to-understand, entangled state, with unclear invariants" is exactly why I have trouble explaining it. That is my point about scale, and about this behavior being so counterintuitive it can undermine the code around it. Allowing mutation lets the error become more nonlocal, thus harder to find, as the mutation means it can flow downstream until it hits something that has become unsound because values changed. For every source line in a toy example I provide, there may be hundreds separating them... if they're even in the same crate or repo... in the real thing. People by and large won't set a breakpoint on the variable changing if they never imagine it can be changed. I would genuinely rather the composited binaries try to do something that makes valgrind scream at the impossibility, immediately. Because Miri isn't the only game in town. As annoying as they may be, it's very easy to pop gdb and examine a core dump of a segfault, too (...the immediate backtrace and register dump, anyway, the rest can be somewhat "???"). |
The only real "optimization" available that I am aware of in the separate compilation case... ...we did all agree that this is most likely to occur in the case of FFI, right?... ...where an address must be revealed to the world, and that must have a legible value at that location, or the program simply cannot work, neither as the abstract machine understands it nor as the programmer understands it... is to move the data into read-only memory. Attempts to write to that location will generally violate virtual memory protection and immediately trigger SIGSEGV or the equivalent... Windows still calls it Unconditionally permitting the mutation does not allow this transformation, allowing errors to be latent in the actual binary. |
As a note, I can think of at least one place where two different translation units may need to come up with the layout of an anonymous type de novo, that being inlining/generics. This is because now two (or more) different compilation units can contain the definition, and need to agree in order to be interconvertible. Especially in the generics case, because the captures' list can be built partially, but not entirely (by-ref to by-copy lifting requires knowing the monomorphic type, this optimization is present in v0, for types at most the size of a pointer) so the compiler on both sides of this must agree on the same final steps at least (ie. on the small-copy capture optimization) - this is true even if the compiler is the exact same build of lccc. The case in question is something like fn mk_sized_array<T>(_: &T) -> [u8; core::mem::size_of::<T>()]{
[0xFF; core::mem::size_of::<T>()]
}
pub fn foo<T: Copy + Display>(x: T) -> impl Any{
let f = || println!("{}", {x});
mk_sized_array(&f)
} Two different calls to |
I think that "erroneous behavior" classification is worth exploring more. It seems nice to have a way to forbid things in a way that the compiler can insert checks for, instead of the "I assume it never happens and generate code that way" nasal demons of UB. Like, "this is forbidden and I'm going to check it when I can" sounds way better for things where the reason it's forbidden is to make code more intelligible, instead of more optimizable. What would the performance impact be of placing fully initialized |
Note that it would specifically have to be put into a |
Since I don't see it mentioned yet, the Rust Reference currently documents that "Mutating immutable bytes" is UB, and that
Note however that the Reference is explicitly non-normative and subject to change. |
Bart Jacobs makes a good point on Zulip: an immutable local can be mutated more than once using destructors. struct S(i32);
impl Drop for S {
fn drop(&mut self) {
self.0 = 42;
}
}
let s: S;
s = S(0); // first mutation
// there may be a "variable now fully initialized" marker here, it doesn't help
// the implicit drop-in-place is the second mutation I think that breaks the schemes suggested above for how an operational semantics could treat non- |
It doesn't really break my proposal that &raw const be special-cased in lowering to minirust on an immutable binding. Also doesn't really interfere with the opts I'd like to do (they mostly only apply to types that aren't Drop). Drop is funny in general. |
It's not clear to me which proposal you are referring to. Where have you sketched the op.sem for that? |
I'm not sure there would be op-sem for that proposal. No different Minirust semantics are required, only a different lowering Rust->Minirust. |
Ah, I see. I don't remember seeing this proposal before, but I think I understand. My personal opinion is that I am not a fan of non-compositional lowerings so I'd rather not have such a special case. |
I'm going to withdraw my concern re. closure captures. |
This came up in rust-lang/rust#111502 and overlaps with #257: should it be allowed to mutate
let
-bound variables, via code like this?Tree Borrows currently accepts this code since
addr_of
never generates a new tag, it just creates an alias to the original pointer. Stacked Borrows rejects it due to #257. There are other ways to reject this code while making*const
and*mut
equivalent, hence I opened this as a separate issue.Personally I favor the Tree Borrows behavior here and don't think it is worth the extra effort to make these variables read-only.
The text was updated successfully, but these errors were encountered: