Skip to content
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

Check soundness of clone erasure #136

Open
1 task
yannbolliger opened this issue Apr 15, 2021 · 0 comments
Open
1 task

Check soundness of clone erasure #136

yannbolliger opened this issue Apr 15, 2021 · 0 comments
Labels
enhancement Improvement to an existing feature imperative Feature or bug related to imperative features

Comments

@yannbolliger
Copy link
Collaborator

yannbolliger commented Apr 15, 2021

From #124 on, calls to st::clone::Clone::clone as well as implementations of the trait are erased/replaced by identity. This is to facilitate some benchmarks and is correct on the small and immutable examples of the test suite. However, in general this is unsound:

  • in presence of mutation (let mut), a cloned ADT can be modified, but the original should remain unchanged,
  • the same is true for types that have internal mutability, and
  • if the implementation of Clone is not derived, then there are no guarantees as to what it does.

The frontend needs to check these cases and forbid them. A more complicated problem arises with generic functions that have type parameters.

fn f<T: Clone>(t: T) { t.clone() }

Here, it cannot be decided at definition site of the function, whether the Clone is safe and can be erased or not.
Two solutions come to mind:

  • Use a flag/annotation on T to state whether the Clone should be treated as sound/safe or not. This is the same as the @mutable annotations in Scala Stainless. Then detect/check the soundness at call-site of the function.

  • Use a marker trait like SafeClone that states that the particular implementation is safe. The user then needs to opt-in that trait for all needed types.

  • Could the user opt-in to SafeClone by deriving it? (with a proc-macro)

@yannbolliger yannbolliger added enhancement Improvement to an existing feature imperative Feature or bug related to imperative features labels Apr 15, 2021
@yannbolliger yannbolliger self-assigned this May 2, 2021
@yannbolliger yannbolliger removed their assignment Mar 12, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement Improvement to an existing feature imperative Feature or bug related to imperative features
Projects
None yet
Development

No branches or pull requests

1 participant