Add an alternative way to represent trait contracts
The current way how traits are dealt with (adding a default implementation which enforces contracts and calls into a virtual renamed method for the implementation) is rather smart and efficient regards implementation effort as well as code size. However, it has a few disadvantages:
-
The DevX is not nice. If a dev forgets to add
#[contract_trait]
to animpl
, he gets incoherent compiler errors. As devs are general skeptical about contracts, this might be a (minor) adoption blocker. In general, we can expects Devs to be not very receptive to tools rewriting their programs s.t. they do not compile any longer. -
For a static analyzer, the current representation is challenging. As we are attaching the pre/post to the trait method, they are hard to analyze in that context, because when the trait is analyzed, nothing is known about the implementation (it is basically an uninterpreted function). So we would need to analyze the trait method on a rather abstract level, then inject the result of that analysis into caller sides. As a matter of fact, having a
impl T for S
, many caller sides work onS
, and the abstract representation of the contract onT
is only rarely needed (namely where traits are actually used for representing polymorphism).
This issue is about adding an alternative way how traits are compiled which may improve on the above.
Given a contract trait declaration as below:
#[contract_trait]
trait T {
#[pre(x > 0)]
#[post(ret > old(*x) && ret == *x)]
fn f(&self, x: &mut i64) -> i64;
}
struct S{}
#[contract_trait]
impl T for S {
fn f(&self, x: &mut i64) -> i64 {
*x = *x + 1;
*x
}
}
We would generate the following code:
trait T {
fn f(&self, x: &mut i64) -> i64;
fn __pre_f(&self, x: &&mut i64) -> bool {
**x > 0
}
fn __capture_old_f(&self, x: &&mut i64) -> __Old_f {
__Old_f{x: (**x).clone()} // notice we need to make a copy
}
fn __post_f(&self, x: &&mut i64, ret: &i64, __old: __Old_f) -> bool {
*ret > __old.x && *ret == **x
}
}
#[allow(non_camel_case_types)]
struct __Old_f {
x: i64
}
struct S {}
impl T for S {
fn f(&self, x: &mut i64) -> i64 {
assert!(self.__pre_f(&x));
let __old = self.__capture_old_f(&x);
let mut __run = ||{
*x = *x + 1;
*x
};
let ret = __run();
assert!(self.__post_f(&x, &ret, __old));
ret
}
}
Generating this code, however, is challenging compared to the current approach.
- In order to generate
struct __Old_f
we need to somehow get hand on the types ofold(E)
expressions. It is not clear whether this is even possible with procedural macros. - We need to more fundamentally rewrite code. For instance whenever we refer to a parameter
x
in pre/post code, we need to rewrite it as*x
. - Possibly more problems ...