74 lines
2.2 KiB
Rust
74 lines
2.2 KiB
Rust
|
/// Correctness for protocols
|
||
|
|
|
||
|
|
/*
|
||
|
|
|
||
|
|
This section of code makes sure the protocol is likely to generate
|
||
|
|
correct code. The correctness criteria include:
|
||
|
|
|
||
|
|
* No protocols transition to states that don't exist.
|
||
|
|
* Messages step to states with the right number of type parameters.
|
||
|
|
|
||
|
|
In addition, this serves as a lint pass. Lint warns for the following
|
||
|
|
things.
|
||
|
|
|
||
|
|
* States with no messages, it's better to step to !.
|
||
|
|
|
||
|
|
It would also be nice to warn about unreachable states, but the
|
||
|
|
visitor infrastructure for protocols doesn't currently work well for
|
||
|
|
that.
|
||
|
|
|
||
|
|
*/
|
||
|
|
|
||
|
|
import dvec::extensions;
|
||
|
|
|
||
|
|
import ext::base::ext_ctxt;
|
||
|
|
|
||
|
|
import ast::{ident};
|
||
|
|
|
||
|
|
import proto::{state, protocol, next_state, methods};
|
||
|
|
import ast_builder::empty_span;
|
||
|
|
|
||
|
|
impl proto_check of proto::visitor<(), (), ()> for ext_ctxt {
|
||
|
|
fn visit_proto(_proto: protocol,
|
||
|
|
_states: &[()]) { }
|
||
|
|
|
||
|
|
fn visit_state(state: state, _m: &[()]) {
|
||
|
|
if state.messages.len() == 0 {
|
||
|
|
self.span_warn(
|
||
|
|
empty_span(), // use a real span!
|
||
|
|
#fmt("state %s contains no messages, \
|
||
|
|
consider stepping to a terminal state instead",
|
||
|
|
*state.name))
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
fn visit_message(name: ident, _tys: &[@ast::ty],
|
||
|
|
this: state, next: next_state) {
|
||
|
|
alt next {
|
||
|
|
some({state: next, tys: next_tys}) {
|
||
|
|
let proto = this.proto;
|
||
|
|
if !proto.has_state(next) {
|
||
|
|
// This should be a span fatal, but then we need to
|
||
|
|
// track span information.
|
||
|
|
self.span_err(
|
||
|
|
empty_span(),
|
||
|
|
#fmt("message %s steps to undefined state, %s",
|
||
|
|
*name, *next));
|
||
|
|
}
|
||
|
|
|
||
|
|
let next = proto.get_state(next);
|
||
|
|
|
||
|
|
if next.ty_params.len() != next_tys.len() {
|
||
|
|
self.span_err(
|
||
|
|
empty_span(), // use a real span
|
||
|
|
#fmt("message %s target (%s) \
|
||
|
|
needs %u type parameters, but got %u",
|
||
|
|
*name, *next.name,
|
||
|
|
next.ty_params.len(),
|
||
|
|
next_tys.len()));
|
||
|
|
}
|
||
|
|
}
|
||
|
|
none { }
|
||
|
|
}
|
||
|
|
}
|
||
|
|
}
|