Redo typestate-related data structures to support predicate constraints. No actual support yet, just infrastructure.
This commit is contained in:
Tim Chevalier
parent
af4554aadf
commit
1402cd101b
8 changed files with 473 additions and 147 deletions
|
|
@ -51,7 +51,7 @@ import util::common::log_stmt;
|
|||
|
||||
import aux::fn_info;
|
||||
import aux::fn_info_map;
|
||||
import aux::num_locals;
|
||||
import aux::num_constraints;
|
||||
import aux::get_fn_info;
|
||||
import aux::crate_ctxt;
|
||||
import aux::add_node;
|
||||
|
|
@ -109,19 +109,19 @@ fn init_vecs(&crate_ctxt ccx, @vec[uint] node_ids, uint len) -> () {
|
|||
}
|
||||
}
|
||||
|
||||
fn visit_fn(&crate_ctxt ccx, uint num_locals, &_fn f,
|
||||
fn visit_fn(&crate_ctxt ccx, uint num_constraints, &_fn f,
|
||||
&span sp, &ident i, &def_id d, &ann a) -> () {
|
||||
let vec[uint] node_ids_ = [];
|
||||
let @vec[uint] node_ids = @node_ids_;
|
||||
node_ids_in_fn(f, sp, i, d, a, node_ids);
|
||||
init_vecs(ccx, node_ids, num_locals);
|
||||
init_vecs(ccx, node_ids, num_constraints);
|
||||
}
|
||||
|
||||
fn annotate_in_fn(&crate_ctxt ccx, &_fn f, &span sp, &ident i,
|
||||
&def_id f_id, &ann a)
|
||||
-> () {
|
||||
auto f_info = get_fn_info(ccx, f_id);
|
||||
visit_fn(ccx, num_locals(f_info), f, sp, i, f_id, a);
|
||||
visit_fn(ccx, num_constraints(f_info), f, sp, i, f_id, a);
|
||||
}
|
||||
|
||||
fn annotate_crate(&crate_ctxt ccx, &crate crate) -> () {
|
||||
|
|
|
|||
|
|
@ -8,35 +8,21 @@ import std::option::none;
|
|||
import std::option::some;
|
||||
import std::option::maybe;
|
||||
|
||||
import front::ast;
|
||||
import front::ast::def;
|
||||
import front::ast::def_fn;
|
||||
import front::ast::_fn;
|
||||
import front::ast::def_obj_field;
|
||||
import front::ast::def_id;
|
||||
import front::ast::expr_path;
|
||||
import front::ast::ident;
|
||||
import front::ast::controlflow;
|
||||
import front::ast::ann;
|
||||
import front::ast::stmt;
|
||||
import front::ast::expr;
|
||||
import front::ast::block;
|
||||
import front::ast::block_;
|
||||
import front::ast::stmt_decl;
|
||||
import front::ast::stmt_expr;
|
||||
import front::ast::stmt_crate_directive;
|
||||
import front::ast::return;
|
||||
import front::ast::expr_field;
|
||||
import front::ast::*;
|
||||
|
||||
import middle::ty::expr_ann;
|
||||
|
||||
import util::common;
|
||||
import util::common::span;
|
||||
import util::common::respan;
|
||||
import util::common::log_block;
|
||||
import util::common::new_def_hash;
|
||||
import util::common::new_uint_hash;
|
||||
import util::common::log_expr_err;
|
||||
import util::common::uistr;
|
||||
import util::common::lit_eq;
|
||||
import pretty::pprust::path_to_str;
|
||||
import pretty::pprust::lit_to_str;
|
||||
|
||||
import tstate::ann::pre_and_post;
|
||||
import tstate::ann::pre_and_post_state;
|
||||
|
|
@ -63,14 +49,51 @@ fn def_id_to_str(def_id d) -> str {
|
|||
ret (istr(d._0) + "," + istr(d._1));
|
||||
}
|
||||
|
||||
fn comma_str(vec[@constr_arg] args) -> str {
|
||||
auto res = "";
|
||||
auto comma = false;
|
||||
for (@constr_arg a in args) {
|
||||
if (comma) {
|
||||
res += ", ";
|
||||
}
|
||||
else {
|
||||
comma = true;
|
||||
}
|
||||
alt (a.node) {
|
||||
case (carg_base) {
|
||||
res += "*";
|
||||
}
|
||||
case (carg_ident(?i)) {
|
||||
res += i;
|
||||
}
|
||||
case (carg_lit(?l)) {
|
||||
res += lit_to_str(l);
|
||||
}
|
||||
}
|
||||
}
|
||||
ret res;
|
||||
}
|
||||
|
||||
fn constraint_to_str(ty::ctxt tcx, constr c) -> str {
|
||||
alt (c.node) {
|
||||
case (ninit(?i)) {
|
||||
ret "init(" + i + " [" + tcx.sess.span_str(c.span) + "])";
|
||||
}
|
||||
case (npred(?p, ?args)) {
|
||||
ret path_to_str(p) + "(" + comma_str(args) + ")"
|
||||
+ "[" + tcx.sess.span_str(c.span) + "]";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn bitv_to_str(fn_ctxt fcx, bitv::t v) -> str {
|
||||
auto s = "";
|
||||
auto comma = false;
|
||||
|
||||
for each (@tup(def_id, var_info) p in fcx.enclosing.vars.items()) {
|
||||
if (bitv::get(v, p._1.bit_num)) {
|
||||
for (norm_constraint p in constraints(fcx)) {
|
||||
if (bitv::get(v, p.bit_num)) {
|
||||
s += (if (comma) { ", " } else { comma = true; "" })
|
||||
+ p._1.name + " [" + fcx.ccx.tcx.sess.span_str(p._1.sp) + "]";
|
||||
+ aux::constraint_to_str(fcx.ccx.tcx, p.c);
|
||||
}
|
||||
}
|
||||
ret s;
|
||||
|
|
@ -84,19 +107,19 @@ fn first_difference_string(&fn_ctxt fcx, &bitv::t expected,
|
|||
&bitv::t actual) -> str {
|
||||
let str s = "";
|
||||
auto done = false;
|
||||
for each (@tup(def_id, var_info) p in fcx.enclosing.vars.items()) {
|
||||
for (norm_constraint c in constraints(fcx)) {
|
||||
if (!done) {
|
||||
if (bitv::get(expected, p._1.bit_num) &&
|
||||
!bitv::get(actual, p._1.bit_num)) {
|
||||
if (bitv::get(expected, c.bit_num) &&
|
||||
!bitv::get(actual, c.bit_num)) {
|
||||
|
||||
/*
|
||||
FIXME
|
||||
for fun, try either:
|
||||
* "ret s" after the assignment to s
|
||||
or
|
||||
* using break here
|
||||
*/
|
||||
s = (p._1.name + " ["
|
||||
+ fcx.ccx.tcx.sess.span_str(p._1.sp) + "]");
|
||||
s = constraint_to_str(fcx.ccx.tcx, c.c);
|
||||
|
||||
done = true;
|
||||
}
|
||||
|
|
@ -183,14 +206,35 @@ fn print_idents(vec[ident] idents) -> () {
|
|||
/* data structures */
|
||||
|
||||
/**********************************************************************/
|
||||
/* mapping from variable name (def_id is assumed to be for a local
|
||||
variable in a given function) to bit number
|
||||
(also remembers the ident and span for error-logging purposes) */
|
||||
type var_info = rec(uint bit_num,
|
||||
ident name,
|
||||
span sp);
|
||||
type fn_info = rec(@std::map::hashmap[def_id, var_info] vars,
|
||||
controlflow cf);
|
||||
/* mapping from def_id to bit number and other data
|
||||
(ident/path/span are there for error-logging purposes) */
|
||||
|
||||
type pred_desc_ = rec(vec[@constr_arg] args,
|
||||
uint bit_num);
|
||||
type pred_desc = spanned[pred_desc_];
|
||||
tag constraint {
|
||||
cinit(uint, span, ident);
|
||||
cpred(path, vec[pred_desc]);
|
||||
}
|
||||
tag constr_ {
|
||||
ninit(ident);
|
||||
npred(path, vec[@constr_arg]);
|
||||
}
|
||||
type constr = spanned[constr_];
|
||||
type norm_constraint = rec(uint bit_num,
|
||||
constr c);
|
||||
/* "constraint occurrence" to disambiguate
|
||||
between constraints. either "this is an
|
||||
init constraint", or the list of args for
|
||||
a pred. */
|
||||
tag constr_occ {
|
||||
occ_init;
|
||||
occ_args(vec[@constr_arg]);
|
||||
}
|
||||
|
||||
type constr_map = @std::map::hashmap[def_id, constraint];
|
||||
|
||||
type fn_info = rec(constr_map constrs, uint num_constraints, controlflow cf);
|
||||
|
||||
/* mapping from node ID to typestate annotation */
|
||||
type node_ann_table = @vec[ts_ann];
|
||||
|
|
@ -418,8 +462,8 @@ fn fixed_point_states(&fn_ctxt fcx,
|
|||
}
|
||||
}
|
||||
|
||||
fn num_locals(fn_info m) -> uint {
|
||||
ret m.vars.size();
|
||||
fn num_constraints(fn_info m) -> uint {
|
||||
ret m.num_constraints;
|
||||
}
|
||||
|
||||
fn new_crate_ctxt(ty::ctxt cx) -> crate_ctxt {
|
||||
|
|
@ -463,6 +507,89 @@ fn ann_to_def(&crate_ctxt ccx, &ann a) -> option::t[def] {
|
|||
ret ccx.tcx.def_map.find(a.id);
|
||||
}
|
||||
|
||||
fn norm_a_constraint(&constraint c) -> vec[norm_constraint] {
|
||||
alt (c) {
|
||||
case (cinit(?n, ?sp, ?i)) {
|
||||
ret [rec(bit_num=n, c=respan(sp, ninit(i)))];
|
||||
}
|
||||
case (cpred(?p, ?descs)) {
|
||||
let vec[norm_constraint] res = [];
|
||||
for (pred_desc pd in descs) {
|
||||
vec::push(res, rec(bit_num=pd.node.bit_num,
|
||||
c=respan(pd.span, npred(p, pd.node.args))));
|
||||
}
|
||||
ret res;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Tried to write this as an iterator, but I got a
|
||||
// non-exhaustive match in trans.
|
||||
fn constraints(&fn_ctxt fcx) -> vec[norm_constraint] {
|
||||
let vec[norm_constraint] res = [];
|
||||
for each (@tup(def_id, constraint) p in
|
||||
fcx.enclosing.constrs.items()) {
|
||||
res += norm_a_constraint(p._1);
|
||||
}
|
||||
ret res;
|
||||
}
|
||||
|
||||
fn arg_eq(@constr_arg a, @constr_arg b) -> bool {
|
||||
alt (a.node) {
|
||||
case (carg_base) {
|
||||
alt (b.node) {
|
||||
case (carg_base) {
|
||||
ret true;
|
||||
}
|
||||
case (_) {
|
||||
ret false;
|
||||
}
|
||||
}
|
||||
}
|
||||
case (carg_ident(?s)) {
|
||||
alt (b.node) {
|
||||
case (carg_ident(?t)) {
|
||||
ret (s == t);
|
||||
}
|
||||
case (_) {
|
||||
ret false;
|
||||
}
|
||||
}
|
||||
}
|
||||
case (carg_lit(?l)) {
|
||||
alt (b.node) {
|
||||
case (carg_lit(?m)) {
|
||||
ret lit_eq(l, m);
|
||||
}
|
||||
case (_) {
|
||||
ret false;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn args_eq(vec[@constr_arg] a, vec[@constr_arg] b) -> bool {
|
||||
let uint i = 0u;
|
||||
for (@constr_arg arg in a) {
|
||||
if (!arg_eq(arg, b.(i))) {
|
||||
ret false;
|
||||
}
|
||||
i += 1u;
|
||||
}
|
||||
ret true;
|
||||
}
|
||||
|
||||
fn match_args(&fn_ctxt fcx, vec[pred_desc] occs,
|
||||
vec[@constr_arg] occ) -> uint {
|
||||
for (pred_desc pd in occs) {
|
||||
if (args_eq(pd.node.args, occ)) {
|
||||
ret pd.node.bit_num;
|
||||
}
|
||||
}
|
||||
fcx.ccx.tcx.sess.bug("match_args: no match for occurring args");
|
||||
}
|
||||
|
||||
//
|
||||
// Local Variables:
|
||||
// mode: rust
|
||||
|
|
|
|||
|
|
@ -3,15 +3,19 @@ import std::vec;
|
|||
import std::vec::len;
|
||||
import std::vec::slice;
|
||||
|
||||
import front::ast;
|
||||
import front::ast::def_id;
|
||||
import front::ast::expr;
|
||||
import front::ast::ann;
|
||||
import front::ast::*;
|
||||
|
||||
import aux::fn_ctxt;
|
||||
import aux::fn_info;
|
||||
import aux::log_bitv;
|
||||
import aux::num_locals;
|
||||
import aux::num_constraints;
|
||||
import aux::constr_occ;
|
||||
import aux::occ_init;
|
||||
import aux::occ_args;
|
||||
import aux::cinit;
|
||||
import aux::cpred;
|
||||
import aux::pred_desc;
|
||||
import aux::match_args;
|
||||
|
||||
import tstate::aux::ann_to_ts_ann;
|
||||
import tstate::ann::pre_and_post;
|
||||
|
|
@ -31,13 +35,37 @@ import tstate::ann::set_in_postcond;
|
|||
import tstate::ann::set_in_poststate;
|
||||
import tstate::ann::clear_in_poststate;
|
||||
|
||||
fn bit_num(def_id v, fn_info m) -> uint {
|
||||
assert (m.vars.contains_key(v));
|
||||
ret m.vars.get(v).bit_num;
|
||||
fn bit_num(&fn_ctxt fcx, &def_id v, &constr_occ o) -> uint {
|
||||
assert (fcx.enclosing.constrs.contains_key(v));
|
||||
auto res = fcx.enclosing.constrs.get(v);
|
||||
alt (o) {
|
||||
case (occ_init) {
|
||||
alt (res) {
|
||||
case (cinit(?n,_,_)) {
|
||||
ret n;
|
||||
}
|
||||
case (_) {
|
||||
fcx.ccx.tcx.sess.bug("bit_num: asked for init constraint,"
|
||||
+ " found a pred constraint");
|
||||
}
|
||||
}
|
||||
}
|
||||
case (occ_args(?args)) {
|
||||
alt (res) {
|
||||
case (cpred(_, ?descs)) {
|
||||
ret match_args(fcx, descs, args);
|
||||
}
|
||||
case (_) {
|
||||
fcx.ccx.tcx.sess.bug("bit_num: asked for pred constraint,"
|
||||
+ " found an init constraint");
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn promises(&poststate p, def_id v, fn_info m) -> bool {
|
||||
ret bitv::get(p, bit_num(v, m));
|
||||
fn promises(&fn_ctxt fcx, &poststate p, &def_id v, &constr_occ o) -> bool {
|
||||
ret bitv::get(p, bit_num(fcx, v, o));
|
||||
}
|
||||
|
||||
// Given a list of pres and posts for exprs e0 ... en,
|
||||
|
|
@ -46,7 +74,7 @@ fn promises(&poststate p, def_id v, fn_info m) -> bool {
|
|||
// precondition shouldn't include x.
|
||||
fn seq_preconds(fn_ctxt fcx, vec[pre_and_post] pps) -> precond {
|
||||
let uint sz = len[pre_and_post](pps);
|
||||
let uint num_vars = num_locals(fcx.enclosing);
|
||||
let uint num_vars = num_constraints(fcx.enclosing);
|
||||
|
||||
if (sz >= 1u) {
|
||||
auto first = pps.(0);
|
||||
|
|
@ -115,33 +143,38 @@ fn intersect_postconds(&vec[postcond] pcs) -> postcond {
|
|||
ret intersect_postconds_go(bitv::clone(pcs.(0)), pcs);
|
||||
}
|
||||
|
||||
fn gen(&fn_ctxt fcx, &ann a, def_id id) -> bool {
|
||||
fn gen(&fn_ctxt fcx, &ann a, &def_id id, &constr_occ o) -> bool {
|
||||
log "gen";
|
||||
assert (fcx.enclosing.vars.contains_key(id));
|
||||
let uint i = (fcx.enclosing.vars.get(id)).bit_num;
|
||||
ret set_in_postcond(i, (ann_to_ts_ann(fcx.ccx, a)).conditions);
|
||||
ret set_in_postcond(bit_num(fcx, id, o),
|
||||
(ann_to_ts_ann(fcx.ccx, a)).conditions);
|
||||
}
|
||||
|
||||
fn declare_var(&fn_info enclosing, def_id id, prestate pre)
|
||||
fn declare_var(&fn_ctxt fcx, def_id id, prestate pre)
|
||||
-> prestate {
|
||||
assert (enclosing.vars.contains_key(id));
|
||||
let uint i = (enclosing.vars.get(id)).bit_num;
|
||||
auto res = clone(pre);
|
||||
relax_prestate(i, res);
|
||||
relax_prestate(bit_num(fcx, id, occ_init), res);
|
||||
ret res;
|
||||
}
|
||||
|
||||
fn gen_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
|
||||
fn gen_poststate(&fn_ctxt fcx, &ann a, &def_id id, &constr_occ o) -> bool {
|
||||
log "gen_poststate";
|
||||
assert (fcx.enclosing.vars.contains_key(id));
|
||||
let uint i = (fcx.enclosing.vars.get(id)).bit_num;
|
||||
ret set_in_poststate(i, (ann_to_ts_ann(fcx.ccx, a)).states);
|
||||
ret set_in_poststate(bit_num(fcx, id, o),
|
||||
(ann_to_ts_ann(fcx.ccx, a)).states);
|
||||
}
|
||||
|
||||
fn kill_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
|
||||
fn kill_poststate(&fn_ctxt fcx, &ann a, def_id id, &constr_occ o) -> bool {
|
||||
log "kill_poststate";
|
||||
assert (fcx.enclosing.vars.contains_key(id));
|
||||
let uint i = (fcx.enclosing.vars.get(id)).bit_num;
|
||||
ret clear_in_poststate(i, (ann_to_ts_ann(fcx.ccx, a)).states);
|
||||
ret clear_in_poststate(bit_num(fcx, id, o),
|
||||
(ann_to_ts_ann(fcx.ccx, a)).states);
|
||||
}
|
||||
|
||||
//
|
||||
// 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:
|
||||
//
|
||||
|
|
|
|||
|
|
@ -50,7 +50,7 @@ import aux::expr_prestate;
|
|||
import aux::expr_poststate;
|
||||
import aux::stmt_poststate;
|
||||
import aux::stmt_to_ann;
|
||||
import aux::num_locals;
|
||||
import aux::num_constraints;
|
||||
import aux::fixed_point_states;
|
||||
import aux::bitv_to_str;
|
||||
import aux::first_difference_string;
|
||||
|
|
@ -113,7 +113,7 @@ fn check_states_stmt(&fn_ctxt fcx, &stmt s) -> () {
|
|||
|
||||
fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
|
||||
auto enclosing = fcx.enclosing;
|
||||
auto nv = num_locals(enclosing);
|
||||
auto nv = num_constraints(enclosing);
|
||||
auto post = @empty_poststate(nv);
|
||||
|
||||
fn do_one_(fn_ctxt fcx, &@stmt s, @poststate post) -> () {
|
||||
|
|
@ -134,7 +134,7 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
|
|||
auto cf = fcx.enclosing.cf;
|
||||
/* Finally, check that the return value is initialized */
|
||||
if (f.proto == ast::proto_fn
|
||||
&& ! promises(*post, fcx.id, enclosing)
|
||||
&& ! promises(fcx, *post, fcx.id, aux::occ_init)
|
||||
&& ! type_is_nil(fcx.ccx.tcx,
|
||||
ret_ty_of_fn(fcx.ccx.tcx, a))
|
||||
&& cf == return) {
|
||||
|
|
@ -147,8 +147,8 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
|
|||
else if (cf == noreturn) {
|
||||
// check that this really always fails
|
||||
// the fcx.id bit means "returns" for a returning fn,
|
||||
// "diverges" for a non-returning fn (I need to use the word
|
||||
if (! promises(*post, fcx.id, enclosing)) {
|
||||
// "diverges" for a non-returning fn
|
||||
if (! promises(fcx, *post, fcx.id, aux::occ_init)) {
|
||||
fcx.ccx.tcx.sess.span_err(f.body.span,
|
||||
"In non-returning function " + fcx.name +
|
||||
", some control paths may return to the caller");
|
||||
|
|
|
|||
|
|
@ -1,68 +1,157 @@
|
|||
import std::vec;
|
||||
import std::vec::plus_option;
|
||||
|
||||
import front::ast;
|
||||
import front::ast::crate;
|
||||
import front::ast::ann;
|
||||
import front::ast::arg;
|
||||
import front::ast::method;
|
||||
import front::ast::local;
|
||||
import front::ast::item;
|
||||
import front::ast::item_fn;
|
||||
import front::ast::item_obj;
|
||||
import front::ast::_obj;
|
||||
import front::ast::obj_def_ids;
|
||||
import front::ast::_fn;
|
||||
import front::ast::ty_param;
|
||||
import front::ast::_mod;
|
||||
import front::ast::decl;
|
||||
import front::ast::decl_local;
|
||||
import front::ast::def_id;
|
||||
import front::ast::ident;
|
||||
import front::ast::*;
|
||||
import option::*;
|
||||
|
||||
import middle::walk::walk_crate;
|
||||
import middle::walk::walk_fn;
|
||||
import middle::walk::ast_visitor;
|
||||
|
||||
import aux::cinit;
|
||||
import aux::ninit;
|
||||
import aux::npred;
|
||||
import aux::cpred;
|
||||
import aux::constraint;
|
||||
import aux::fn_info;
|
||||
import aux::var_info;
|
||||
import aux::crate_ctxt;
|
||||
import aux::num_constraints;
|
||||
import aux::constr_map;
|
||||
|
||||
import util::common::new_def_hash;
|
||||
import util::common::uistr;
|
||||
import util::common::span;
|
||||
import util::common::respan;
|
||||
|
||||
type identifier = rec(ident name, def_id id, span sp);
|
||||
type ctxt = rec(@vec[constraint_info] cs,
|
||||
ty::ctxt tcx);
|
||||
|
||||
fn var_is_local(def_id v, fn_info m) -> bool {
|
||||
ret (m.vars.contains_key(v));
|
||||
}
|
||||
type constraint_info = rec(def_id id, aux::constr c);
|
||||
|
||||
fn collect_local(&@vec[identifier] vars, &@decl d) -> () {
|
||||
fn collect_local(&ctxt cx, &@decl d) -> () {
|
||||
alt (d.node) {
|
||||
case (decl_local(?loc)) {
|
||||
log("collect_local: pushing " + loc.ident);
|
||||
vec::push[identifier](*vars, rec(name=loc.ident,
|
||||
id=loc.id,
|
||||
sp=d.span));
|
||||
vec::push[constraint_info](*cx.cs,
|
||||
rec(id=loc.id,
|
||||
c=respan(d.span,
|
||||
ninit(loc.ident))));
|
||||
}
|
||||
case (_) { ret; }
|
||||
}
|
||||
}
|
||||
|
||||
fn find_locals(&_fn f, &span sp, &ident i, &def_id d, &ann a)
|
||||
-> @vec[identifier] {
|
||||
auto res = @vec::alloc[identifier](0u);
|
||||
auto visitor = walk::default_visitor();
|
||||
visitor = rec(visit_decl_pre=bind collect_local(res,_) with visitor);
|
||||
walk_fn(visitor, f, sp, i, d, a);
|
||||
ret res;
|
||||
fn exprs_to_constr_args(ty::ctxt tcx, vec[@expr] args) -> vec[@constr_arg] {
|
||||
fn one(ty::ctxt tcx, &@expr e) -> @constr_arg {
|
||||
alt (e.node) {
|
||||
case (expr_path(?p, _)) {
|
||||
if (vec::len(p.node.idents) == 1u) {
|
||||
ret @respan(p.span, carg_ident(p.node.idents.(0)));
|
||||
}
|
||||
else {
|
||||
tcx.sess.bug("exprs_to_constr_args: non-local variable "
|
||||
+ "as pred arg");
|
||||
}
|
||||
}
|
||||
case (expr_lit(?l, _)) {
|
||||
ret @respan(e.span, carg_lit(l));
|
||||
}
|
||||
case (_) {
|
||||
tcx.sess.bug("exprs_to_constr_args: ill-formed pred arg");
|
||||
}
|
||||
}
|
||||
}
|
||||
auto f = bind one(tcx, _);
|
||||
ret vec::map(f, args);
|
||||
}
|
||||
|
||||
fn def_id_for_constr(ty::ctxt tcx, uint t) -> def_id {
|
||||
alt (tcx.def_map.find(t)) {
|
||||
case (none) {
|
||||
tcx.sess.bug("def_id_for_constr: bad node_id " + uistr(t));
|
||||
}
|
||||
case (some(def_fn(?i))) {
|
||||
ret i;
|
||||
}
|
||||
case (_) {
|
||||
tcx.sess.bug("def_id_for_constr: pred is not a function");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn add_var(def_id v, span sp, ident nm, uint next, fn_info tbl) -> uint {
|
||||
log(nm + " |-> " + util::common::uistr(next));
|
||||
tbl.vars.insert(v, rec(bit_num=next, name=nm, sp=sp));
|
||||
fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constraint_info {
|
||||
alt (e.node) {
|
||||
// change the first pattern to expr_path to test a typechecker bug
|
||||
case (expr_call(?operator, ?args, _)) {
|
||||
alt (operator.node) {
|
||||
case (expr_path(?p, ?a)) {
|
||||
ret rec(id=def_id_for_constr(tcx, a.id),
|
||||
c=respan(e.span,
|
||||
npred(p, exprs_to_constr_args(tcx, args))));
|
||||
}
|
||||
case (_) {
|
||||
tcx.sess.span_err(operator.span, "Internal error: " +
|
||||
" ill-formed operator in predicate");
|
||||
}
|
||||
}
|
||||
}
|
||||
case (_) {
|
||||
tcx.sess.span_err(e.span, "Internal error: " +
|
||||
" ill-formed predicate");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn collect_pred(&ctxt cx, &@expr e) -> () {
|
||||
alt (e.node) {
|
||||
case (expr_check(?e, _)) {
|
||||
vec::push[constraint_info](*cx.cs, expr_to_constr(cx.tcx, e));
|
||||
}
|
||||
case (_) { }
|
||||
}
|
||||
}
|
||||
|
||||
fn find_locals(&ty::ctxt tcx, &_fn f, &span sp, &ident i, &def_id d, &ann a)
|
||||
-> ctxt {
|
||||
let ctxt cx = rec(cs=@vec::alloc[constraint_info](0u), tcx=tcx);
|
||||
auto visitor = walk::default_visitor();
|
||||
visitor = rec(visit_decl_pre=bind collect_local(cx,_),
|
||||
visit_expr_pre=bind collect_pred(cx,_)
|
||||
with visitor);
|
||||
walk_fn(visitor, f, sp, i, d, a);
|
||||
ret cx;
|
||||
}
|
||||
|
||||
fn add_constraint(&ty::ctxt tcx, constraint_info c, uint next, constr_map tbl)
|
||||
-> uint {
|
||||
log(aux::constraint_to_str(tcx, c.c) + " |-> "
|
||||
+ util::common::uistr(next));
|
||||
let aux::constr cn = c.c;
|
||||
alt (cn.node) {
|
||||
case (ninit(?i)) {
|
||||
tbl.insert(c.id, cinit(next, cn.span, i));
|
||||
}
|
||||
case (npred(?p, ?args)) {
|
||||
alt (tbl.find(c.id)) {
|
||||
case (some[constraint](?ct)) {
|
||||
alt (ct) {
|
||||
case (cinit(_,_,_)) {
|
||||
tcx.sess.bug("add_constraint: same def_id used"
|
||||
+ " as a variable and a pred");
|
||||
}
|
||||
case (cpred(_, ?pds)) {
|
||||
vec::push(pds, respan(cn.span,
|
||||
rec(args=args, bit_num=next)));
|
||||
}
|
||||
}
|
||||
}
|
||||
case (none[constraint]) {
|
||||
tbl.insert(c.id, cpred(p,
|
||||
[respan(cn.span, rec(args=args, bit_num=next))]));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
ret (next + 1u);
|
||||
}
|
||||
|
||||
|
|
@ -71,26 +160,33 @@ fn add_var(def_id v, span sp, ident nm, uint next, fn_info tbl) -> uint {
|
|||
fn mk_fn_info(&crate_ctxt ccx, &_fn f, &span f_sp,
|
||||
&ident f_name, &def_id f_id, &ann a)
|
||||
-> () {
|
||||
auto res = rec(vars=@new_def_hash[var_info](),
|
||||
cf=f.decl.cf);
|
||||
auto res_map = @new_def_hash[constraint]();
|
||||
let uint next = 0u;
|
||||
let vec[arg] f_args = f.decl.inputs;
|
||||
|
||||
/* ignore args, which we know are initialized;
|
||||
just collect locally declared vars */
|
||||
|
||||
let @vec[identifier] locals = find_locals(f, f_sp, f_name, f_id, a);
|
||||
for (identifier p in *locals) {
|
||||
next = add_var(p.id, p.sp, p.name, next, res);
|
||||
let ctxt cx = find_locals(ccx.tcx, f, f_sp, f_name, f_id, a);
|
||||
/* now we have to add bit nums for both the constraints
|
||||
and the variables... */
|
||||
|
||||
for (constraint_info c in *cx.cs) {
|
||||
next = add_constraint(cx.tcx, c, next, res_map);
|
||||
}
|
||||
/* add a pseudo-entry for the function's return value
|
||||
we can safely use the function's name itself for this purpose */
|
||||
add_var(f_id, f_sp, f_name, next, res);
|
||||
add_constraint(cx.tcx, rec(id=f_id,
|
||||
c=respan(f_sp, ninit(f_name))), next, res_map);
|
||||
|
||||
log(f_name + " has " + uistr(vec::len[identifier](*locals))
|
||||
+ " locals");
|
||||
auto res = rec(constrs=res_map,
|
||||
num_constraints=vec::len(*cx.cs) + 1u,
|
||||
cf=f.decl.cf);
|
||||
|
||||
ccx.fm.insert(f_id, res);
|
||||
|
||||
log(f_name + " has " + uistr(num_constraints(res)) + " constraints");
|
||||
|
||||
}
|
||||
|
||||
/* initializes the global fn_info_map (mapping each function ID, including
|
||||
|
|
|
|||
|
|
@ -17,10 +17,11 @@ import tstate::ann::pp_clone;
|
|||
import tstate::ann::empty_prestate;
|
||||
import tstate::ann::set_precondition;
|
||||
import tstate::ann::set_postcondition;
|
||||
import aux::var_info;
|
||||
import aux::crate_ctxt;
|
||||
import aux::fn_ctxt;
|
||||
import aux::num_locals;
|
||||
import aux::occ_init;
|
||||
import aux::num_constraints;
|
||||
import aux::constraint;
|
||||
import aux::expr_pp;
|
||||
import aux::stmt_pp;
|
||||
import aux::block_pp;
|
||||
|
|
@ -93,7 +94,9 @@ fn find_pre_post_item(&crate_ctxt ccx, &item i) -> () {
|
|||
alt (i.node) {
|
||||
case (item_const(?id, ?t, ?e, ?di, ?a)) {
|
||||
// make a fake fcx
|
||||
auto fake_fcx = rec(enclosing=rec(vars=@new_def_hash[var_info](),
|
||||
auto fake_fcx = rec(enclosing=
|
||||
rec(constrs=@new_def_hash[constraint](),
|
||||
num_constraints=0u,
|
||||
cf=return),
|
||||
id=tup(0,0),
|
||||
name="",
|
||||
|
|
@ -136,7 +139,7 @@ fn find_pre_post_exprs(&fn_ctxt fcx, &vec[@expr] args, ann a) {
|
|||
|
||||
auto enclosing = fcx.enclosing;
|
||||
auto fm = fcx.ccx.fm;
|
||||
auto nv = num_locals(enclosing);
|
||||
auto nv = num_constraints(enclosing);
|
||||
|
||||
fn do_one(fn_ctxt fcx, &@expr e) -> () {
|
||||
find_pre_post_expr(fcx, e);
|
||||
|
|
@ -163,7 +166,7 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@decl d, &@expr index,
|
|||
find_pre_post_expr(fcx, index);
|
||||
find_pre_post_block(fcx, body);
|
||||
log("222");
|
||||
auto loop_precond = declare_var(fcx.enclosing, decl_lhs(d),
|
||||
auto loop_precond = declare_var(fcx, decl_lhs(d),
|
||||
seq_preconds(fcx, [expr_pp(fcx.ccx, index), block_pp(fcx.ccx, body)]));
|
||||
auto loop_postcond = intersect_postconds
|
||||
([expr_postcond(fcx.ccx, index), block_postcond(fcx.ccx, body)]);
|
||||
|
|
@ -180,7 +183,7 @@ fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs,
|
|||
auto p = expr_pp(fcx.ccx, rhs);
|
||||
set_pre_and_post(fcx.ccx, larger_ann,
|
||||
p.precondition, p.postcondition);
|
||||
gen(fcx, larger_ann, d_id);
|
||||
gen(fcx, larger_ann, d_id, aux::occ_init);
|
||||
}
|
||||
case (_) { find_pre_post_exprs(fcx, [lhs, rhs], larger_ann); }
|
||||
}
|
||||
|
|
@ -192,13 +195,13 @@ fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs,
|
|||
/* Fills in annotations as a side effect. Does not rebuild the expr */
|
||||
fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
|
||||
auto enclosing = fcx.enclosing;
|
||||
auto num_local_vars = num_locals(enclosing);
|
||||
auto num_local_vars = num_constraints(enclosing);
|
||||
|
||||
fn do_rand_(fn_ctxt fcx, &@expr e) -> () {
|
||||
find_pre_post_expr(fcx, e);
|
||||
}
|
||||
|
||||
log("find_pre_post_expr (num_locals =" +
|
||||
log("find_pre_post_expr (num_constraints =" +
|
||||
uistr(num_local_vars) + "):");
|
||||
log_expr(*e);
|
||||
|
||||
|
|
@ -233,7 +236,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
|
|||
auto df = ann_to_def_strict(fcx.ccx, a);
|
||||
alt (df) {
|
||||
case (def_local(?d_id)) {
|
||||
auto i = bit_num(d_id, enclosing);
|
||||
auto i = bit_num(fcx, d_id, occ_init);
|
||||
require_and_preserve(i, res);
|
||||
}
|
||||
case (_) { /* nothing to check */ }
|
||||
|
|
@ -511,7 +514,7 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s)
|
|||
log_stmt(s);
|
||||
|
||||
auto enclosing = fcx.enclosing;
|
||||
auto num_local_vars = num_locals(enclosing);
|
||||
auto num_local_vars = num_constraints(enclosing);
|
||||
alt(s.node) {
|
||||
case(stmt_decl(?adecl, ?a)) {
|
||||
alt(adecl.node) {
|
||||
|
|
@ -526,7 +529,7 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s)
|
|||
copy_pre_post(fcx.ccx, a, an_init.expr);
|
||||
/* log("gen (decl):");
|
||||
log_stmt(s); */
|
||||
gen(fcx, a, alocal.id);
|
||||
gen(fcx, a, alocal.id, occ_init);
|
||||
/* log_err("for stmt");
|
||||
log_stmt(s);
|
||||
log_err("pp = ");
|
||||
|
|
@ -569,7 +572,7 @@ fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
|
|||
|
||||
won't have a postcondition that says x is initialized, but that's ok.
|
||||
*/
|
||||
auto nv = num_locals(fcx.enclosing);
|
||||
auto nv = num_constraints(fcx.enclosing);
|
||||
|
||||
fn do_one_(fn_ctxt fcx, &@stmt s) -> () {
|
||||
find_pre_post_stmt(fcx, *s);
|
||||
|
|
|
|||
|
|
@ -24,10 +24,9 @@ import tstate::ann::false_postcond;
|
|||
import tstate::ann::ts_ann;
|
||||
import tstate::ann::extend_prestate;
|
||||
import tstate::ann::extend_poststate;
|
||||
import aux::var_info;
|
||||
import aux::crate_ctxt;
|
||||
import aux::fn_ctxt;
|
||||
import aux::num_locals;
|
||||
import aux::num_constraints;
|
||||
import aux::expr_pp;
|
||||
import aux::stmt_pp;
|
||||
import aux::block_pp;
|
||||
|
|
@ -49,6 +48,7 @@ import aux::log_states;
|
|||
import aux::block_states;
|
||||
import aux::controlflow_expr;
|
||||
import aux::ann_to_def;
|
||||
import aux::occ_init;
|
||||
|
||||
import bitvectors::seq_preconds;
|
||||
import bitvectors::union_postconds;
|
||||
|
|
@ -121,7 +121,7 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@decl d,
|
|||
fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a) -> bool {
|
||||
alt (ann_to_def(fcx.ccx, a_new_var)) {
|
||||
case (some(def_local(?loc))) {
|
||||
ret gen_poststate(fcx, a, loc);
|
||||
ret gen_poststate(fcx, a, loc, occ_init);
|
||||
}
|
||||
case (_) { ret false; }
|
||||
}
|
||||
|
|
@ -129,7 +129,7 @@ fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a) -> bool {
|
|||
|
||||
fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
|
||||
auto changed = false;
|
||||
auto num_local_vars = num_locals(fcx.enclosing);
|
||||
auto num_local_vars = num_constraints(fcx.enclosing);
|
||||
|
||||
/*
|
||||
log_err("states:");
|
||||
|
|
@ -319,11 +319,14 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
|
|||
|
||||
case (expr_ret(?maybe_ret_val, ?a)) {
|
||||
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
||||
/* normally, everything is true if execution continues after
|
||||
a ret expression (since execution never continues locally
|
||||
after a ret expression */
|
||||
set_poststate_ann(fcx.ccx, a, false_postcond(num_local_vars));
|
||||
/* return from an always-failing function clears the return bit */
|
||||
alt (fcx.enclosing.cf) {
|
||||
case (noreturn) {
|
||||
kill_poststate(fcx, a, fcx.id);
|
||||
kill_poststate(fcx, a, fcx.id, occ_init);
|
||||
}
|
||||
case (_) {}
|
||||
}
|
||||
|
|
@ -578,7 +581,8 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
|
|||
(stmt_ann.states.poststate,
|
||||
expr_poststate(fcx.ccx, an_init.expr))
|
||||
|| changed;
|
||||
changed = gen_poststate(fcx, a, alocal.id)
|
||||
changed = gen_poststate(fcx, a,
|
||||
alocal.id, occ_init)
|
||||
|| changed;
|
||||
log("Summary: stmt = ");
|
||||
log_stmt(*s);
|
||||
|
|
@ -642,7 +646,7 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
|
|||
-> bool {
|
||||
|
||||
auto changed = false;
|
||||
auto num_local_vars = num_locals(fcx.enclosing);
|
||||
auto num_local_vars = num_constraints(fcx.enclosing);
|
||||
|
||||
/* First, set the pre-states and post-states for every expression */
|
||||
auto pres = pres0;
|
||||
|
|
@ -694,7 +698,7 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
|
|||
}
|
||||
|
||||
fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
|
||||
auto num_local_vars = num_locals(fcx.enclosing);
|
||||
auto num_local_vars = num_constraints(fcx.enclosing);
|
||||
auto changed = find_pre_post_state_block(fcx,
|
||||
empty_prestate(num_local_vars), f.body);
|
||||
|
||||
|
|
@ -715,7 +719,7 @@ fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
|
|||
false_postcond(num_local_vars));
|
||||
alt (fcx.enclosing.cf) {
|
||||
case (noreturn) {
|
||||
kill_poststate(fcx, tailann, fcx.id);
|
||||
kill_poststate(fcx, tailann, fcx.id, occ_init);
|
||||
}
|
||||
case (_) { }
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,6 +9,8 @@ import front::ast;
|
|||
import front::ast::ty;
|
||||
import front::ast::pat;
|
||||
import front::codemap::codemap;
|
||||
import front::ast::lit;
|
||||
import front::ast::path;
|
||||
import middle::walk;
|
||||
|
||||
import std::io::stdout;
|
||||
|
|
@ -17,9 +19,11 @@ import std::io::string_writer;
|
|||
import pretty::pprust::print_block;
|
||||
import pretty::pprust::print_item;
|
||||
import pretty::pprust::print_expr;
|
||||
import pretty::pprust::print_path;
|
||||
import pretty::pprust::print_decl;
|
||||
import pretty::pprust::print_fn;
|
||||
import pretty::pprust::print_type;
|
||||
import pretty::pprust::print_literal;
|
||||
import pretty::pprust::mo_untyped;
|
||||
import pretty::pp::mk_printer;
|
||||
|
||||
|
|
@ -227,6 +231,65 @@ fn local_rhs_span(&@ast::local l, &span def) -> span {
|
|||
}
|
||||
}
|
||||
|
||||
fn lit_eq(&@ast::lit l, &@ast::lit m) -> bool {
|
||||
alt (l.node) {
|
||||
case (ast::lit_str(?s)) {
|
||||
alt (m.node) {
|
||||
case (ast::lit_str(?t)) { ret s == t; }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
case (ast::lit_char(?c)) {
|
||||
alt (m.node) {
|
||||
case (ast::lit_char(?d)) { ret c == d; }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
case (ast::lit_int(?i)) {
|
||||
alt (m.node) {
|
||||
case (ast::lit_int(?j)) { ret i == j; }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
case (ast::lit_uint(?i)) {
|
||||
alt (m.node) {
|
||||
case (ast::lit_uint(?j)) { ret i == j; }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
case (ast::lit_mach_int(_, ?i)) {
|
||||
alt (m.node) {
|
||||
case (ast::lit_mach_int(_, ?j)) { ret i == j; }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
case (ast::lit_float(?s)) {
|
||||
alt (m.node) {
|
||||
case (ast::lit_float(?t)) { ret s == t; }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
case (ast::lit_mach_float(_,?s)) {
|
||||
alt (m.node) {
|
||||
case (ast::lit_mach_float(_,?t)) { ret s == t; }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
case (ast::lit_nil) {
|
||||
alt (m.node) {
|
||||
case (ast::lit_nil) { ret true; }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
case (ast::lit_bool(?b)) {
|
||||
alt (m.node) {
|
||||
case (ast::lit_bool(?c)) { ret b == c; }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn respan[T](&span sp, &T t) -> spanned[T] {
|
||||
ret rec(node=t, span=sp);
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue