71 lines
2.2 KiB
Rust
71 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 ext::base::ext_ctxt;
|
|
|
|
import proto::{state, protocol, next_state};
|
|
import ast_builder::empty_span;
|
|
|
|
impl ext_ctxt: proto::visitor<(), (), ()> {
|
|
fn visit_proto(_proto: protocol,
|
|
_states: &[()]) { }
|
|
|
|
fn visit_state(state: state, _m: &[()]) {
|
|
if state.messages.len() == 0 {
|
|
self.span_warn(
|
|
state.span, // use a real span!
|
|
fmt!{"state %s contains no messages, \
|
|
consider stepping to a terminal state instead",
|
|
state.name})
|
|
}
|
|
}
|
|
|
|
fn visit_message(name: ~str, _span: span, _tys: &[@ast::ty],
|
|
this: state, next: next_state) {
|
|
match 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(
|
|
proto.get_state(next).span,
|
|
fmt!{"message %s steps to undefined state, %s",
|
|
name, next});
|
|
}
|
|
else {
|
|
let next = proto.get_state(next);
|
|
|
|
if next.ty_params.len() != next_tys.len() {
|
|
self.span_err(
|
|
next.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 => ()
|
|
}
|
|
}
|
|
} |