The freeze operation has some unexpected ad-hoc rules in the v1 borrow semantics: when a reference is frozen, there must not exist any other mutable reference pointing to the same location. It is, however, ok if the currently frozen reference is used later again. This seems to be over-restrictive since it shouldn't matter whether copies of the mutable reference exist as long as they aren't passed at the same time as an argument to a function, i.e. as long as they do not create aliasing.

This PR simulates the v1 borrow rules for freeze, so we avoid bytcode verification errors. At later point we may relax the rules in the bytecode verifier, at which point we could remove those rules or guard them behind a flag.

Closes #12554.  Als repairs some of the bugs in #12701, but not all, so keeping this bug open.

The freeze operation has some unexpected ad-hoc rules in the v1 borrow semantics: when a reference is frozen, there must not exist any other mutable reference pointing to the same location. It is, however, ok if the currently frozen reference is used later again. This seems to be over-restrictive since it shouldn't matter whether copies of the mutable reference exist as long as they aren't passed at the same time as an argument to a function, i.e. as long as they do not create aliasing.

This PR simulates the v1 borrow rules for freeze, so we avoid bytcode verification errors. At later point we may relax the rules in the bytecode verifier, at which point we could remove those rules or guard them behind a flag.

Closes #12554.  Als repairs some of the bugs in #12701, but not all, so keeping this bug open.

The freeze operation has some unexpected ad-hoc rules in the v1 borrow semantics: when a reference is frozen, there must not exist any other mutable reference pointing to the same location. It is, however, ok if the currently frozen reference is used later again. This seems to be over-restrictive since it shouldn't matter whether copies of the mutable reference exist as long as they aren't passed at the same time as an argument to a function, i.e. as long as they do not create aliasing.

This PR simulates the v1 borrow rules for freeze, so we avoid bytcode verification errors. At later point we may relax the rules in the bytecode verifier, at which point we could remove those rules or guard them behind a flag.

Closes #12554.  Als repairs some of the bugs in #12701, but not all, so keeping this bug open.

The freeze operation has some unexpected ad-hoc rules in the v1 borrow semantics: when a reference is frozen, there must not exist any other mutable reference pointing to the same location. It is, however, ok if the currently frozen reference is used later again. This seems to be over-restrictive since it shouldn't matter whether copies of the mutable reference exist as long as they aren't passed at the same time as an argument to a function, i.e. as long as they do not create aliasing.

This PR simulates the v1 borrow rules for freeze, so we avoid bytcode verification errors. At later point we may relax the rules in the bytecode verifier, at which point we could remove those rules or guard them behind a flag.

Closes #12554.  Als repairs some of the bugs in #12701, but not all, so keeping this bug open.

…on (#12725)

* [compiler-v2] Introduces custom rules for checking the freeze operation

The freeze operation has some unexpected ad-hoc rules in the v1 borrow semantics: when a reference is frozen, there must not exist any other mutable reference pointing to the same location. It is, however, ok if the currently frozen reference is used later again. This seems to be over-restrictive since it shouldn't matter whether copies of the mutable reference exist as long as they aren't passed at the same time as an argument to a function, i.e. as long as they do not create aliasing.

This PR simulates the v1 borrow rules for freeze, so we avoid bytcode verification errors. At later point we may relax the rules in the bytecode verifier, at which point we could remove those rules or guard them behind a flag.

Closes #12554.  Als repairs some of the bugs in #12701, but not all, so keeping this bug open.

* Adding new test case

…r semantics

This does a number of adaptions to reference safety to deal with some of the unexpected quirks of the v1 borrow semantics. Additional cases are now detected which are logical safe but anyway rejected by v1. Also, the treatment of freeze has been updated to relax some corner cases which led to failures in framework compilation. With this PR, all known bytecode verification failures are now detected except of a few which are sensitive to optimizations on and which pass without optimizations but not without (see #12756).

This closes #12301 and closes #12701

- Fixes `borrow_global` borrow edge to carry a code offset, to be able to distinguish multiple global borrows with different addresses. Since the address in `borrow_global<R>(addr)` is dynamic, the reference checker cannot know whether to borrows results in the same reference. We already tackle this situation for calls which derive reference by adding the code offset, and now do the same for borrow global.
- Makes assignment and let a checkpoint for borrow safety. Until now, we have considered those operations as no-ops for safety (which is safe from memory perspective), but v1 insists on borrow safety for those ops.
- Adds a new check to borrow safety for mut refs which are duplicated and live beyond a safety check point. A particular quirk in v1 is that a mut ref which was used to derive another mut ref is allowed, but one which is duplicated is not. Since the information from which temps refs have been derived is not present in the borrow graph, which is designed to abstract from mut ref copies, we needed to introduce a new field in the borrow state to track this information. Specifically, the following is _not_ allowed in v1: `let r = &mut s; let r1 = r; let x = &mut r.f; *x; *r1`. However, this is allowed: `let r = &mut s; let x = &mut r.f; *x; *r`. The v1 logic behind this seems to be that `x` is derived from `r` but not (for the first example) from `r1`.

…r semantics

This does a number of adaptions to reference safety to deal with some of the unexpected quirks of the v1 borrow semantics. Additional cases are now detected which are logical safe but anyway rejected by v1. Also, the treatment of freeze has been updated to relax some corner cases which led to failures in framework compilation. With this PR, all known bytecode verification failures are now detected except of a few which are sensitive to optimizations on and which pass without optimizations but not without (see #12756).

This closes #12301 and closes #12701

- Fixes `borrow_global` borrow edge to carry a code offset, to be able to distinguish multiple global borrows with different addresses. Since the address in `borrow_global<R>(addr)` is dynamic, the reference checker cannot know whether to borrows results in the same reference. We already tackle this situation for calls which derive reference by adding the code offset, and now do the same for borrow global.
- Makes assignment and let a checkpoint for borrow safety. Until now, we have considered those operations as no-ops for safety (which is safe from memory perspective), but v1 insists on borrow safety for those ops.
- Adds a new check to borrow safety for mut refs which are duplicated and live beyond a safety check point. A particular quirk in v1 is that a mut ref which was used to derive another mut ref is allowed, but one which is duplicated is not. Since the information from which temps refs have been derived is not present in the borrow graph, which is designed to abstract from mut ref copies, we needed to introduce a new field in the borrow state to track this information. Specifically, the following is _not_ allowed in v1: `let r = &mut s; let r1 = r; let x = &mut r.f; *x; *r1`. However, this is allowed: `let r = &mut s; let x = &mut r.f; *x; *r`. The v1 logic behind this seems to be that `x` is derived from `r` but not (for the first example) from `r1`.

…r semantics

This does a number of adaptions to reference safety to deal with some of the unexpected quirks of the v1 borrow semantics. Additional cases are now detected which are logical safe but anyway rejected by v1. Also, the treatment of freeze has been updated to relax some corner cases which led to failures in framework compilation. With this PR, all known bytecode verification failures are now detected except of a few which are sensitive to optimizations on and which pass without optimizations but not without (see #12756).

This closes #12301 and closes #12701

- Fixes `borrow_global` borrow edge to carry a code offset, to be able to distinguish multiple global borrows with different addresses. Since the address in `borrow_global<R>(addr)` is dynamic, the reference checker cannot know whether to borrows results in the same reference. We already tackle this situation for calls which derive reference by adding the code offset, and now do the same for borrow global.
- Makes assignment and let a checkpoint for borrow safety. Until now, we have considered those operations as no-ops for safety (which is safe from memory perspective), but v1 insists on borrow safety for those ops.
- Adds a new check to borrow safety for mut refs which are duplicated and live beyond a safety check point. A particular quirk in v1 is that a mut ref which was used to derive another mut ref is allowed, but one which is duplicated is not. Since the information from which temps refs have been derived is not present in the borrow graph, which is designed to abstract from mut ref copies, we needed to introduce a new field in the borrow state to track this information. Specifically, the following is _not_ allowed in v1: `let r = &mut s; let r1 = r; let x = &mut r.f; *x; *r1`. However, this is allowed: `let r = &mut s; let x = &mut r.f; *x; *r`. The v1 logic behind this seems to be that `x` is derived from `r` but not (for the first example) from `r1`.