bd4aeef78b
Programs with constrained types now parse and typecheck, but typestate doesn't check them specially, so the one relevant test case so far is XFAILed. Also rewrote all of the constraint-related data structures in the process (again), for some reason. I got rid of a superfluous data structure in the context that was mapping front-end constraints to resolved constraints, instead handling constraints in the same way in which everything else gets resolved.
226 lines
7.3 KiB
Rust
226 lines
7.3 KiB
Rust
|
|
import syntax::ast;
|
|
import ast::method;
|
|
import ast::item;
|
|
import ast::item_fn;
|
|
import ast::_fn;
|
|
import ast::obj_field;
|
|
import ast::_obj;
|
|
import ast::stmt;
|
|
import ast::ident;
|
|
import ast::fn_ident;
|
|
import ast::node_id;
|
|
import ast::def_id;
|
|
import ast::local_def;
|
|
import ast::ty_param;
|
|
import ast::crate;
|
|
import ast::return;
|
|
import ast::noreturn;
|
|
import ast::expr;
|
|
import syntax::visit;
|
|
import syntax::codemap::span;
|
|
import middle::ty::type_is_nil;
|
|
import middle::ty::ret_ty_of_fn;
|
|
import tstate::ann::ts_ann;
|
|
import tstate::ann::empty_poststate;
|
|
import tstate::ann::true_precond;
|
|
import tstate::ann::true_postcond;
|
|
import tstate::ann::false_postcond;
|
|
import tstate::ann::precond;
|
|
import tstate::ann::postcond;
|
|
import tstate::ann::poststate;
|
|
import tstate::ann::prestate;
|
|
import tstate::ann::implies;
|
|
import tstate::ann::ann_precond;
|
|
import tstate::ann::ann_prestate;
|
|
import std::option;
|
|
import std::option::t;
|
|
import std::option::some;
|
|
import std::option::none;
|
|
import aux::*;
|
|
import syntax::print::pprust::ty_to_str;
|
|
import util::common::log_stmt_err;
|
|
import bitvectors::promises;
|
|
import annotate::annotate_crate;
|
|
import collect_locals::mk_f_to_fn_info;
|
|
import pre_post_conditions::fn_pre_post;
|
|
import states::find_pre_post_state_fn;
|
|
|
|
fn check_unused_vars(&fn_ctxt fcx) {
|
|
// FIXME: could be more efficient
|
|
for (norm_constraint c in constraints(fcx)) {
|
|
alt (c.c.node) {
|
|
case (ninit(?id, ?v)) {
|
|
if (!vec_contains(fcx.enclosing.used_vars, id)) {
|
|
fcx.ccx.tcx.sess.span_warn(c.c.span,
|
|
"Unused variable " + v);
|
|
}
|
|
}
|
|
case (_) { /* ignore pred constraints */ }
|
|
}
|
|
}
|
|
}
|
|
|
|
fn check_states_expr(&@expr e, &fn_ctxt fcx, &visit::vt[fn_ctxt] v) {
|
|
visit::visit_expr(e, fcx, v);
|
|
|
|
let precond prec = expr_precond(fcx.ccx, e);
|
|
let prestate pres = expr_prestate(fcx.ccx, e);
|
|
|
|
/*
|
|
log_err("check_states_expr:");
|
|
util::common::log_expr_err(*e);
|
|
log_err("prec = ");
|
|
log_tritv_err(fcx, prec);
|
|
log_err("pres = ");
|
|
log_tritv_err(fcx, pres);
|
|
*/
|
|
|
|
if (!implies(pres, prec)) {
|
|
auto s = "";
|
|
auto diff = first_difference_string(fcx, prec, pres);
|
|
s +=
|
|
"Unsatisfied precondition constraint (for example, " + diff +
|
|
") for expression:\n";
|
|
s += syntax::print::pprust::expr_to_str(e);
|
|
s += "\nPrecondition:\n";
|
|
s += tritv_to_str(fcx, prec);
|
|
s += "\nPrestate:\n";
|
|
s += tritv_to_str(fcx, pres);
|
|
fcx.ccx.tcx.sess.span_fatal(e.span, s);
|
|
}
|
|
}
|
|
|
|
fn check_states_stmt(&@stmt s, &fn_ctxt fcx, &visit::vt[fn_ctxt] v) {
|
|
visit::visit_stmt(s, fcx, v);
|
|
|
|
auto a = stmt_to_ann(fcx.ccx, *s);
|
|
let precond prec = ann_precond(a);
|
|
let prestate pres = ann_prestate(a);
|
|
|
|
/*
|
|
log_err("check_states_stmt:");
|
|
log_stmt_err(*s);
|
|
log_err("prec = ");
|
|
log_tritv_err(fcx, prec);
|
|
log_err("pres = ");
|
|
log_tritv_err(fcx, pres);
|
|
*/
|
|
|
|
if (!implies(pres, prec)) {
|
|
auto ss = "";
|
|
auto diff = first_difference_string(fcx, prec, pres);
|
|
ss +=
|
|
"Unsatisfied precondition constraint (for example, " + diff +
|
|
") for statement:\n";
|
|
ss += syntax::print::pprust::stmt_to_str(*s);
|
|
ss += "\nPrecondition:\n";
|
|
ss += tritv_to_str(fcx, prec);
|
|
ss += "\nPrestate: \n";
|
|
ss += tritv_to_str(fcx, pres);
|
|
fcx.ccx.tcx.sess.span_fatal(s.span, ss);
|
|
}
|
|
}
|
|
|
|
fn check_states_against_conditions(&fn_ctxt fcx, &_fn f,
|
|
&ast::ty_param[] tps,
|
|
node_id id, &span sp, &fn_ident i) {
|
|
/* Postorder traversal instead of pre is important
|
|
because we want the smallest possible erroneous statement
|
|
or expression. */
|
|
|
|
auto visitor = visit::default_visitor[fn_ctxt]();
|
|
|
|
visitor = @rec(visit_stmt=check_states_stmt,
|
|
visit_expr=check_states_expr,
|
|
visit_fn=do_nothing
|
|
with *visitor);
|
|
visit::visit_fn(f, tps, sp, i, id, fcx, visit::mk_vt(visitor));
|
|
|
|
/* Check that the return value is initialized */
|
|
auto post = aux::block_poststate(fcx.ccx, f.body);
|
|
let tsconstr ret_c = ninit(fcx.id, fcx.name);
|
|
if (f.proto == ast::proto_fn && !promises(fcx, post, ret_c) &&
|
|
!type_is_nil(fcx.ccx.tcx, ret_ty_of_fn(fcx.ccx.tcx, id)) &&
|
|
f.decl.cf == return) {
|
|
fcx.ccx.tcx.sess.span_note(f.body.span,
|
|
"In function " + fcx.name +
|
|
", not all control paths \
|
|
return a value");
|
|
fcx.ccx.tcx.sess.span_fatal(f.decl.output.span,
|
|
"see declared return type of '" +
|
|
ty_to_str(*f.decl.output) + "'");
|
|
} else if (f.decl.cf == noreturn) {
|
|
|
|
// check that this really always fails
|
|
// the fcx.id bit means "returns" for a returning fn,
|
|
// "diverges" for a non-returning fn
|
|
if (!promises(fcx, post, ret_c)) {
|
|
fcx.ccx.tcx.sess.span_fatal(f.body.span,
|
|
"In non-returning function " + fcx.name
|
|
+
|
|
", some control paths may \
|
|
return to the caller");
|
|
}
|
|
}
|
|
|
|
/* Finally, check for unused variables */
|
|
check_unused_vars(fcx);
|
|
}
|
|
|
|
fn check_fn_states(&fn_ctxt fcx, &_fn f, &ast::ty_param[] tps,
|
|
node_id id, &span sp, &fn_ident i) {
|
|
/* Compute the pre- and post-states for this function */
|
|
|
|
// Fixpoint iteration
|
|
while (find_pre_post_state_fn(fcx, f)) {}
|
|
|
|
/* Now compare each expr's pre-state to its precondition
|
|
and post-state to its postcondition */
|
|
|
|
check_states_against_conditions(fcx, f, tps, id, sp, i);
|
|
}
|
|
|
|
fn fn_states(&_fn f, &ast::ty_param[] tps,
|
|
&span sp, &fn_ident i, node_id id, &crate_ctxt ccx,
|
|
&visit::vt[crate_ctxt] v) {
|
|
visit::visit_fn(f, tps, sp, i, id, ccx, v);
|
|
/* Look up the var-to-bit-num map for this function */
|
|
|
|
assert (ccx.fm.contains_key(id));
|
|
auto f_info = ccx.fm.get(id);
|
|
auto name = option::from_maybe("anon", i);
|
|
auto fcx = rec(enclosing=f_info, id=id, name=name, ccx=ccx);
|
|
check_fn_states(fcx, f, tps, id, sp, i);
|
|
}
|
|
|
|
fn check_crate(ty::ctxt cx, @crate crate) {
|
|
let crate_ctxt ccx = new_crate_ctxt(cx);
|
|
/* Build the global map from function id to var-to-bit-num-map */
|
|
|
|
mk_f_to_fn_info(ccx, crate);
|
|
/* Add a blank ts_ann for every statement (and expression) */
|
|
|
|
annotate_crate(ccx, *crate);
|
|
/* Compute the pre and postcondition for every subexpression */
|
|
|
|
auto vtor = visit::default_visitor[crate_ctxt]();
|
|
vtor = @rec(visit_fn=fn_pre_post with *vtor);
|
|
visit::visit_crate(*crate, ccx, visit::mk_vt(vtor));
|
|
|
|
/* Check the pre- and postcondition against the pre- and poststate
|
|
for every expression */
|
|
vtor = @rec(visit_fn=fn_states with *vtor);
|
|
visit::visit_crate(*crate, ccx, visit::mk_vt(vtor));
|
|
}
|
|
//
|
|
// Local Variables:
|
|
// mode: rust
|
|
// fill-column: 78;
|
|
// indent-tabs-mode: nil
|
|
// c-basic-offset: 4
|
|
// buffer-file-coding-system: utf-8-unix
|
|
// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
|
|
// End:
|
|
//
|