Instantiate function preconditions inside the function body

so that if we have a function like:
f(...) : p(x) {
  ...
}

p(x) is true inside the body of f.

Closes #694.

diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs
index d6303b15fe63de22d6fef054a803631cdebaee8c..c2a69c4426c0995263393f328973508e6df101d1 100644 (file)
--- a/src/comp/middle/tstate/auxiliary.rs
+++ b/src/comp/middle/tstate/auxiliary.rs
@@ -1053,6 +1053,29 @@ fn op_to_oper_ty(init_op io) -> oper_type {
 fn do_nothing[T](&_fn f, &ty_param[] tp, &span sp, &fn_ident i,
               node_id iid, &T cx, &visit::vt[T] v) {
 }
+
+
+fn args_to_constr_args(&span sp, &arg[] args) -> (@constr_arg_use)[] {
+    let (@constr_arg_use)[] actuals = ~[];
+    for (arg a in args) {
+        actuals += ~[@respan(sp, carg_ident(tup(a.ident, a.id)))];
+    }
+    ret actuals;
+}
+
+fn ast_constr_to_ts_constr(&ty::ctxt tcx, &arg[] args, &@constr c)
+    -> tsconstr {
+    auto tconstr = ty::ast_constr_to_constr(tcx, c);
+    ret npred(tconstr.node.path, tconstr.node.id,
+               args_to_constr_args(tconstr.span, args));
+}
+
+fn ast_constr_to_sp_constr(&ty::ctxt tcx, &arg[] args, &@constr c)
+    -> sp_constr {
+    auto tconstr = ast_constr_to_ts_constr(tcx, args, c);
+    ret respan(c.span, tconstr);
+}
+
 //
 // Local Variables:
 // mode: rust

diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs
index e7afe85f34f777b40752d73ab2565de30202dda8..e3538d1527c6c10ccd85fd4b9ab3fb60304a9b83 100644 (file)
--- a/src/comp/middle/tstate/bitvectors.rs
+++ b/src/comp/middle/tstate/bitvectors.rs
@@ -233,6 +233,10 @@ fn set_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
     ret set_in_poststate_(bit_num(fcx, ninit(id, ident)), t);
 }
 
+fn set_in_prestate_constr(&fn_ctxt fcx, &tsconstr c, &prestate t) -> bool {
+    ret set_in_poststate_(bit_num(fcx, c), t);
+}
+
 fn clear_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
                             &node_id parent) -> bool {
     ret kill_poststate(fcx, parent, ninit(id, ident));

diff --git a/src/comp/middle/tstate/collect_locals.rs b/src/comp/middle/tstate/collect_locals.rs
index 5005ad5132b2c0ab176af5a12785746ad055d3fb..8d4fc6cc1199d82ce14ae2a8e048a86faa40e10d 100644 (file)
--- a/src/comp/middle/tstate/collect_locals.rs
+++ b/src/comp/middle/tstate/collect_locals.rs
@@ -1,4 +1,5 @@
-
+import std::uint;
+import std::int;
 import std::ivec;
 import syntax::ast::*;
 import util::ppaux::fn_ident_to_string;
@@ -96,6 +97,7 @@ fn add_constraint(&ty::ctxt tcx, sp_constr c, uint next, constr_map tbl) ->
    to a bit number in the precondition/postcondition vectors */
 fn mk_fn_info(&crate_ctxt ccx, &_fn f, &ty_param[] tp,
               &span f_sp, &fn_ident f_name, node_id id) {
+    auto name = fn_ident_to_string(id, f_name);
     auto res_map = @new_def_hash[constraint]();
     let uint next = 0u;
 
@@ -106,15 +108,23 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &ty_param[] tp,
     for (sp_constr c in { *cx.cs }) {
         next = add_constraint(cx.tcx, c, next, res_map);
     }
+    /* if this function has any constraints, instantiate them to the
+       argument names and add them */
+    auto sc;
+    for (@constr c in f.decl.constraints) {
+        sc = ast_constr_to_sp_constr(cx.tcx, f.decl.inputs, c);
+        next = add_constraint(cx.tcx, sc, 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 */
 
-    auto name = fn_ident_to_string(id, f_name);
     add_constraint(cx.tcx, respan(f_sp, ninit(id, name)), next, res_map);
     let @mutable node_id[] v = @mutable ~[];
     auto rslt =
         rec(constrs=res_map,
-            num_constraints=ivec::len(*cx.cs) + 1u,
+            num_constraints=ivec::len(*cx.cs) + ivec::len(f.decl.constraints)
+                            + 1u,
             cf=f.decl.cf,
             used_vars=v);
     ccx.fm.insert(id, rslt);

diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index 88b21748a3f1d1571f94a8af287c74ccf80c793b..c91687be0f8b991b34394086e0ccceb4e91baffe 100644 (file)
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -1,3 +1,4 @@
+import syntax::print::pprust::path_to_str;
 import std::ivec;
 import std::option;
 import std::option::get;
@@ -25,6 +26,8 @@
 import tritv::tritv_set;
 import tritv::ttrue;
 
+import bitvectors::*;
+/*
 import bitvectors::set_in_poststate_ident;
 import bitvectors::clear_in_poststate_expr;
 import bitvectors::clear_in_prestate_ident;
@@ -33,6 +36,7 @@
 import bitvectors::kill_poststate;
 import bitvectors::clear_in_poststate_ident;
 import bitvectors::intersect_states;
+*/
 import syntax::ast::*;
 import middle::ty::expr_ty;
 import middle::ty::type_is_nil;
@@ -731,9 +735,15 @@ fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
     auto num_local_vars = num_constraints(fcx.enclosing);
     // make sure the return bit starts out False
     clear_in_prestate_ident(fcx, fcx.id, fcx.name, f.body.node.id);
-    auto changed =
-        find_pre_post_state_block(fcx, block_prestate(fcx.ccx, f.body),
-                                  f.body);
+    // Instantiate any constraints on the arguments so we can use them
+    auto block_pre = block_prestate(fcx.ccx, f.body);
+    auto tsc;
+    for (@constr c in f.decl.constraints) {
+        tsc = ast_constr_to_ts_constr(fcx.ccx.tcx, f.decl.inputs, c);
+        set_in_prestate_constr(fcx, tsc, block_pre);
+    }
+
+    auto changed = find_pre_post_state_block(fcx, block_pre, f.body);
     // Treat the tail expression as a return statement
 
     alt (f.body.node.expr) {

diff --git a/src/test/run-pass/typestate-transitive.rs b/src/test/run-pass/typestate-transitive.rs
new file mode 100644 (file)
index 0000000..86dacb2
--- /dev/null
+++ b/src/test/run-pass/typestate-transitive.rs
@@ -0,0 +1,8 @@
+pred p(int i) -> bool { true }
+
+fn f(int i) : p(i) -> int { i }
+
+fn g(int i) : p(i) -> int { f(i) }
+
+fn main() {
+}