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)
From #124 on, calls to
st::clone::Clone::cloneas 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:let mut), a cloned ADT can be modified, but the original should remain unchanged,Cloneis 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.
Here, it cannot be decided at definition site of the function, whether the
Cloneis safe and can be erased or not. Two solutions come to mind:Tto state whether theCloneshould be treated as sound/safe or not. This is the same as the@mutableannotations in Scala Stainless. Then detect/check the soundness at call-site of the function.SafeClonethat states that the particular implementation is safe. The user then needs to opt-in that trait for all needed types.SafeCloneby deriving it? (with a proc-macro)