---

yaml
---
r: 3836
b: refs/heads/master
c: e1f9bfb
h: refs/heads/master
v: v3

Author: catamorphism

[refs]

@@ -1,2 +1,2 @@
 ---
-refs/heads/master: 21b94d57d5319e42f5a30818c88b95c95449864e
+refs/heads/master: e1f9bfbac93765f833cd20a599165025f18faebe

trunk/src/comp/middle/tstate/auxiliary.rs

@@ -8,6 +8,7 @@ import std::int;
 import std::uint;
 import syntax::ast::*;
 import syntax::codemap::span;
+import syntax::visit;
 import util::common;
 import util::common::log_block;
 import std::map::new_int_hash;
@@ -527,13 +528,7 @@ fn match_args(&fn_ctxt fcx, &pred_desc[] occs, &(@constr_arg_use)[] occ) ->
         fn eq(&tup(ident, def_id) p, &tup(ident, def_id) q) -> bool {
             ret p._1 == q._1;
         }
-
-        // FIXME: Remove this vec->ivec conversion.
-        let (@constr_arg_use)[] cau_ivec = ~[];
-        for (@constr_arg_use cau in pd.node.args) {
-            cau_ivec += ~[cau];
-        }
-        if (ty::args_eq(eq, cau_ivec, occ)) { ret pd.node.bit_num; }
+        if (ty::args_eq(eq, pd.node.args, occ)) { ret pd.node.bit_num; }
     }
     fcx.ccx.tcx.sess.bug("match_args: no match for occurring args");
 }
@@ -1038,6 +1033,11 @@ fn op_to_oper_ty(init_op io) -> oper_type {
         case (_)         { oper_assign }
     }
 }
+
+// default function visitor
+fn do_nothing[T](&_fn f, &ty_param[] tp, &span sp, &fn_ident i,
+              node_id iid, &T cx, &visit::vt[T] v) {
+}
 //
 // Local Variables:
 // mode: rust

trunk/src/comp/middle/tstate/ck.rs

@@ -17,7 +17,7 @@ import ast::crate;
 import ast::return;
 import ast::noreturn;
 import ast::expr;
-import syntax::walk;
+import syntax::visit;
 import syntax::codemap::span;
 import middle::ty::type_is_nil;
 import middle::ty::ret_ty_of_fn;
@@ -62,7 +62,9 @@ fn check_unused_vars(&fn_ctxt fcx) {
     }
 }
 
-fn check_states_expr(&fn_ctxt fcx, &@expr e) {
+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);
 
@@ -90,7 +92,9 @@ fn check_states_expr(&fn_ctxt fcx, &@expr e) {
     }
 }
 
-fn check_states_stmt(&fn_ctxt fcx, &@stmt 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);
@@ -126,24 +130,13 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f,
        because we want the smallest possible erroneous statement
        or expression. */
 
-    let @mutable bool keepgoing = @mutable true;
-    
-    /* TODO probably should use visit instead */
-
-    fn quit(@mutable bool keepgoing, &@ast::item i) {
-        *keepgoing = false;
-    }
-    fn kg(@mutable bool keepgoing) -> bool { 
-        ret *keepgoing;
-    }
+    auto visitor = visit::default_visitor[fn_ctxt]();
 
-    auto v = rec (visit_stmt_post=bind check_states_stmt(fcx, _),
-                  visit_expr_post=bind check_states_expr(fcx, _),
-                  visit_item_pre=bind quit(keepgoing, _),
-                  keep_going=bind kg(keepgoing)
-                  with walk::default_visitor());
-
-    walk::walk_fn(v, f, tps, sp, i, id);
+    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);
@@ -189,10 +182,12 @@ fn check_fn_states(&fn_ctxt fcx, &_fn f, &ast::ty_param[] tps,
     check_states_against_conditions(fcx, f, tps, id, sp, i);
 }
 
-fn fn_states(&crate_ctxt ccx, &_fn f, &ast::ty_param[] tps,
-             &span sp, &fn_ident i, node_id id) {
+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);
@@ -210,19 +205,14 @@ fn check_crate(ty::ctxt cx, @crate crate) {
     annotate_crate(ccx, *crate);
     /* Compute the pre and postcondition for every subexpression */
 
-    auto do_pre_post = walk::default_visitor();
-    do_pre_post =
-        rec(visit_fn_post=bind fn_pre_post(ccx, _, _, _, _, _)
-            with do_pre_post);
-    walk::walk_crate(do_pre_post, *crate);
+    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 */
-
-    auto do_states = walk::default_visitor();
-    do_states =
-        rec(visit_fn_post=bind fn_states(ccx, _, _, _, _, _)
-            with do_states);
-    walk::walk_crate(do_states, *crate);
+    vtor = @rec(visit_fn=fn_states with *vtor);
+    visit::visit_crate(*crate, ccx, visit::mk_vt(vtor));
 }
 //
 // Local Variables:

trunk/src/comp/middle/tstate/collect_locals.rs

@@ -9,18 +9,7 @@ import syntax::visit;
 import walk::walk_crate;
 import walk::walk_fn;
 import walk::ast_visitor;
-import aux::cinit;
-import aux::ninit;
-import aux::npred;
-import aux::cpred;
-import aux::constraint;
-import aux::fn_info;
-import aux::crate_ctxt;
-import aux::num_constraints;
-import aux::constr_map;
-import aux::expr_to_constr;
-import aux::constraints_expr;
-import aux::node_id_to_def_strict;
+import aux::*;
 import std::map::new_int_hash;
 import util::common::new_def_hash;
 import syntax::codemap::span;
@@ -63,10 +52,6 @@ fn collect_pred(&@expr e, &ctxt cx, &visit::vt[ctxt] v) {
     // visit subexpressions
     visit::visit_expr(e, cx, v);
 }
-
-fn do_nothing(&_fn f, &ty_param[] tp, &span sp, &fn_ident i,
-              node_id iid, &ctxt cx, &visit::vt[ctxt] v) {
-}
 
 fn find_locals(&ty::ctxt tcx, &_fn f, &ty_param[] tps, &span sp, &fn_ident i,
                node_id id) -> ctxt {

trunk/src/comp/middle/tstate/pre_post_conditions.rs

@@ -32,6 +32,7 @@ import bitvectors::relax_precond_block;
 import bitvectors::gen;
 import tritv::tritv_clone;
 import syntax::ast::*;
+import syntax::visit;
 import std::map::new_int_hash;
 import util::common::new_def_hash;
 import util::common::log_expr;
@@ -719,8 +720,10 @@ fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) {
     }
 }
 
-fn fn_pre_post(crate_ctxt ccx, &_fn f, &ty_param[] tps,
-               &span sp, &fn_ident i, node_id id) {
+fn fn_pre_post(&_fn f, &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);
     assert (ccx.fm.contains_key(id));
     auto fcx = rec(enclosing=ccx.fm.get(id), id=id,
                    name=fn_ident_to_string(id, i), ccx=ccx);

trunk/src/comp/middle/tstate/states.rs

@@ -24,52 +24,6 @@ import tstate::ann::ts_ann;
 import tstate::ann::set_prestate;
 import tstate::ann::set_poststate;
 import aux::*;
-/*
-import aux::crate_ctxt;
-import aux::fn_ctxt;
-import aux::num_constraints;
-import aux::expr_pp;
-import aux::stmt_pp;
-import aux::block_pp;
-import aux::set_pre_and_post;
-import aux::expr_prestate;
-import aux::expr_precond;
-import aux::expr_postcond;
-import aux::stmt_poststate;
-import aux::expr_poststate;
-import aux::block_prestate;
-import aux::block_poststate;
-import aux::block_precond;
-import aux::block_postcond;
-import aux::fn_info;
-import aux::log_pp;
-import aux::log_pp_err;
-import aux::extend_prestate_ann;
-import aux::extend_poststate_ann;
-import aux::set_prestate_ann;
-import aux::set_poststate_ann;
-import aux::pure_exp;
-import aux::log_tritv;
-import aux::log_tritv_err;
-import aux::stmt_to_ann;
-import aux::log_states;
-import aux::log_states_err;
-import aux::block_states;
-import aux::controlflow_expr;
-import aux::node_id_to_def;
-import aux::expr_to_constr;
-import aux::ninit;
-import aux::npred;
-import aux::path_to_ident;
-import aux::if_ty;
-import aux::if_check;
-import aux::plain_if;
-import aux::forget_in_poststate;
-import aux::forget_in_poststate_still_init;
-import aux::copy_in_poststate;
-import aux::copy_in_poststate_two;
-import aux::local_node_id_to_def;
-*/
 import tritv::tritv_clone;
 import tritv::tritv_set;
 import tritv::ttrue;
@@ -229,7 +183,13 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l,
 
     auto changed = set_prestate_ann(fcx.ccx, id, loop_pres) |
         find_pre_post_state_expr(fcx, pres, index);
-        find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, index), body);
+
+    // Make sure the index var is considered initialized
+    // in the body
+    auto index_post = tritv_clone(expr_poststate(fcx.ccx, index));
+    set_in_poststate_ident(fcx, l.node.id, l.node.ident, index_post);
+
+    changed |= find_pre_post_state_block(fcx, index_post, body);
 
     if (has_nonlocal_exits(body)) { 
         // See [Break-unsound]
@@ -238,11 +198,6 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l,
     else {
         auto res_p = intersect_states(expr_poststate(fcx.ccx, index),
                                       block_poststate(fcx.ccx, body));
-    /*
-    auto res_p =
-        intersect_postconds([expr_poststate(fcx.ccx, index),
-        block_poststate(fcx.ccx, body)]); */
-
         ret changed | set_poststate_ann(fcx.ccx, id, res_p);
     }
 }