-
Notifications
You must be signed in to change notification settings - Fork 13.3k
Better error message for "argument 1 may alias with argument 0, which is not immutably rooted" #1822
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
Comments
I think it will be quite challenging to express the alias constraints any more clearly and succinctly than that (though maybe someone will find a way). We could include a link to a wiki page with a thorough explanation (seriously). Of course, the alias checking rules may be loosened which would obviate the need for this error message altogether. |
I guess "is not immutably rooted" could be changed to "could be potentially mutated by the callee" or something like that. That would at least help reduce the jargon factor. |
I'm just learning Rust, but how does the temp change the meaning of the code? |
With the temporary, there is no way for anyone to change the array (or its contents) as it is being iterated. This is the invariant that the alias checker is trying to enforce. This is important because when we iterate over an array using pointers into the array itself so if it were modified it might invalidate those pointers. It is somewhat difficult to explain the precise rules that is uses (I don't really understand them in detail myself), but it's always an approximation of the truth, meaning that it gives an error if it cannot determine that the code is safe, even though the code may well be safe in reality. So to some extent you just have to accept it when it asks you to insert temporaries or copies (just as you sometimes must workaround type check errors in code you know to be valid). |
I can imagine if I was to modify the vector itself (by adding or removing from it, for example), it would mess up the iteration. But I don't understand how modifying one of the elements of the array would be a problem. Regardless, the compiler should be able to tell that I'm NOT modifying v, but only reading from it. |
Sorry, I wrote that last answer in a bit of a rush and I realize it was a bit unsatisfying (particularly the second part). Let me explain in a bit more detail. So, as I said, the alias checker exists to guarantee certain aliasing properties. Like the type checker it is a conservative safety check that runs over your program: so there will always be safe programs that it still rejects, because it cannot understand how they are safe. As you point out, your program is one of those. It would certainly be nice for the alias checker to be better and of course we will work on that. Now, as to the semantic difference between your two examples: there is in fact a big difference. The temporary variable In general, the alias checker works well when working with local variables, which it can track quite well. The alias checker is not very good at tracking aliases within records. That is why your original program is rejected, because the vector being aliased lies within the record. Tracking aliases to data within records is certainly much more complex, because you have to consider the possibility that the record itself may be aliased. In this case, with the record on the stack, we could probably do better without too much difficulty, but I'm not sure: these kinds of checks are quite subtle and it's easy to make a mistake. So the alias checker aims to stay on the "clearly safe" side. As for the term "immutably rooted", it basically means that there is some path of immutable fields which begin (are "rooted in") a local or unique variable---that is, they are rooted in something that the alias tracker can easily track. Anyway, I was trying to find a better guide to the alias checker in the documentation, but I didn't find one just yet. I should add that many of the details of this particular program may change. There is talk of making vectors non-unique and also of moving to other systems to track aliases. But that is still work-in-progress and we may decide the current system is indeed the best. |
OK. Thanks for the explanation. I'm going to close, since I don't think there are any short-term improvements possible, and I don't have a long-term solution to propose. |
I don't know if I addressed your point directly: my point was that (in the original program) the alias checker did not consider itself able to prove that you are not modifying or extending Also, there does exist the possibility that this is a bug in the alias checker (i.e., something which it should be able to prove under its current set of rules but it fails to for whatever reason). @marijnh would know best. I probably should have just let him answer this question in the first place. In any case, I am going to close this bug for the time being. I opened #1823 instead---a request for better docs on the alias checker. I think this is the most important thing which is needed. |
Downgrade the rust toolchain for the nighly before the current version. This mitigates rust-lang#1822 which is caused by rust-lang#103814. Ps.: I also bumped cbmc min version since older versions don't work with Kani.
…t-lang#13922) I [recently realized that `.last()` might not call `next_back()` when it is available](https://qsantos.fr/2025/01/01/rust-gotcha-last-on-doubleendediterator/). Although the implementor could make sure to implement `last()` to do so, this is not what will happen by default. As a result, I think it is useful to add a lint to promote using `.next_back()` over `.last()` on `DoubleEndedIterator`. If this is merged, we might want to close rust-lang#1822. changelog: [`double_ended_iterator_last`]: Add lint for calling `Iterator::last()` on `DoubleEndedIterator`
Given this program:
The error produced is: "m.rs:5:19: 7:2 error: argument 1 may alias with argument 0, which is not immutably rooted", which is more than a little jargon-y. If this is really an error, then it should be easier to understand what the problem is. Note that this program compiles cleanly:
The text was updated successfully, but these errors were encountered: