---

yaml
---
r: 3390
b: refs/heads/master
c: 85b5b2a
h: refs/heads/master
v: v3

Author: catamorphism

[refs]

@@ -1,2 +1,2 @@
 ---
-refs/heads/master: 6d1050b1c7c8f5075aaaf6b922ff36f3aceef5e2
+refs/heads/master: 85b5b2a8e46f943a35513bb2bbe8a6d026ed2785

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

@@ -112,7 +112,7 @@ fn set_in_postcond(uint i, &pre_and_post p) -> bool {
     // sets the ith bit in p's post
     auto was_set = tritv_get(p.postcondition, i);
     tritv_set(i, p.postcondition, ttrue);
-    ret was_set == dont_care;
+    ret was_set != ttrue;
 }
 
 fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
@@ -123,7 +123,7 @@ fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
 fn set_in_poststate_(uint i, &poststate p) -> bool {
     auto was_set = tritv_get(p, i);
     tritv_set(i, p, ttrue);
-    ret was_set == dont_care;
+    ret was_set != ttrue;
 
 }
 
@@ -135,14 +135,25 @@ fn clear_in_poststate(uint i, &pre_and_post_state s) -> bool {
 fn clear_in_poststate_(uint i, &poststate s) -> bool {
     auto was_set = tritv_get(s, i);
     tritv_set(i, s, tfalse);
-    ret was_set == dont_care;
+    ret was_set != tfalse;
+}
+
+fn clear_in_prestate(uint i, &pre_and_post_state s) -> bool {
+    // sets the ith bit in p's pre
+    ret clear_in_prestate_(i, s.prestate);
+}
+
+fn clear_in_prestate_(uint i, &prestate s) -> bool {
+    auto was_set = tritv_get(s, i);
+    tritv_set(i, s, tfalse);
+    ret was_set != tfalse;
 }
 
 fn clear_in_postcond(uint i, &pre_and_post s) -> bool {
     // sets the ith bit in p's post
     auto was_set = tritv_get(s.postcondition, i);
     tritv_set(i, s.postcondition, tfalse);
-    ret was_set == dont_care;
+    ret was_set != tfalse;
 }
 
 // Sets all the bits in a's precondition to equal the

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

@@ -43,6 +43,7 @@ import tstate::ann::set_in_postcond;
 import tstate::ann::set_in_poststate;
 import tstate::ann::set_in_poststate_;
 import tstate::ann::clear_in_poststate;
+import tstate::ann::clear_in_prestate;
 import tstate::ann::clear_in_poststate_;
 import tritv::*;
 
@@ -147,22 +148,10 @@ fn seq_preconds(&fn_ctxt fcx, &vec[pre_and_post] pps) -> precond {
     } else { ret true_precond(num_vars); }
 }
 
-/* Gee, maybe we could use foldl or something */
-fn intersect_postconds_go(&postcond first, &vec[postcond] rest) -> postcond {
-    auto sz = vec::len[postcond](rest);
-    if (sz > 0u) {
-        auto other = rest.(0);
-        intersect(first, other);
-        intersect_postconds_go(first,
-                               slice[postcond](rest, 1u,
-                                               len[postcond](rest)));
-    }
-    ret first;
-}
-
-fn intersect_postconds(&vec[postcond] pcs) -> postcond {
-    assert (len[postcond](pcs) > 0u);
-    ret intersect_postconds_go(tritv_clone(pcs.(0)), pcs);
+fn intersect_states(&prestate p, &prestate q) -> prestate {
+    auto rslt = tritv_clone(p);
+    tritv_intersect(rslt, q);
+    ret rslt;
 }
 
 fn gen(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
@@ -219,6 +208,11 @@ fn gen_poststate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
                          node_id_to_ts_ann(fcx.ccx, id).states);
 }
 
+fn kill_prestate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
+    ret clear_in_prestate(bit_num(fcx, c),
+                           node_id_to_ts_ann(fcx.ccx, id).states);
+}
+
 fn kill_poststate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
     log "kill_poststate";
     ret clear_in_poststate(bit_num(fcx, c),
@@ -254,6 +248,16 @@ fn set_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
     ret set_in_poststate_(bit_num(fcx, rec(id=id, c=ninit(ident))), t);
 }
 
+fn clear_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
+                            &node_id parent) -> bool {
+    ret kill_poststate(fcx, parent, rec(id=id, c=ninit(ident)));
+}
+
+fn clear_in_prestate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
+                            &node_id parent) -> bool {
+    ret kill_prestate(fcx, parent, rec(id=id, c=ninit(ident)));
+}
+
 //
 // Local Variables:
 // mode: rust

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

@@ -70,9 +70,9 @@ fn check_states_expr(&fn_ctxt fcx, &@expr e) {
     log_err("check_states_expr:");
       util::common::log_expr_err(*e);
       log_err("prec = ");
-      log_bitv_err(fcx, prec);
+      log_tritv_err(fcx, prec);
       log_err("pres = ");
-      log_bitv_err(fcx, pres);
+      log_tritv_err(fcx, pres);
     */
 
     if (!implies(pres, prec)) {
@@ -99,9 +99,9 @@ fn check_states_stmt(&fn_ctxt fcx, &@stmt s) {
       log_err("check_states_stmt:");
       log_stmt_err(*s);
       log_err("prec = ");
-      log_bitv_err(fcx, prec);
+      log_tritv_err(fcx, prec);
       log_err("pres = ");
-      log_bitv_err(fcx, pres);
+      log_tritv_err(fcx, pres);
     */
 
     if (!implies(pres, prec)) {

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

@@ -59,7 +59,7 @@ import bitvectors::bit_num;
 import bitvectors::promises;
 import bitvectors::seq_preconds;
 import bitvectors::seq_postconds;
-import bitvectors::intersect_postconds;
+import bitvectors::intersect_states;
 import bitvectors::declare_var;
 import bitvectors::gen_poststate;
 import bitvectors::relax_precond_block;
@@ -180,9 +180,8 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block body,
         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)]);
+    auto loop_postcond = intersect_states(expr_postcond(fcx.ccx, index),
+                                          block_postcond(fcx.ccx, body));
     copy_pre_post_(fcx.ccx, id, loop_precond, loop_postcond);
 }
 
@@ -247,8 +246,7 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
                 seq_postconds(fcx, [precond_true_case,
                                     precond_false_case]);
             auto postcond_res =
-                intersect_postconds([postcond_true_case,
-                                     postcond_false_case]);
+                intersect_states(postcond_true_case, postcond_false_case);
             set_pre_and_post(fcx.ccx, id, precond_res, postcond_res);
         }
     }
@@ -459,10 +457,9 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
                              seq_preconds(fcx,
                                           [expr_pp(fcx.ccx, test),
                                            block_pp(fcx.ccx, body)]),
-                             intersect_postconds([expr_postcond(fcx.ccx,
-                                                                test),
-                                                  block_postcond(fcx.ccx,
-                                                                 body)]));
+                             intersect_states(expr_postcond(fcx.ccx, test),
+                                              block_postcond(fcx.ccx,
+                                                             body)));
         }
         case (expr_do_while(?body, ?test)) {
             find_pre_post_block(fcx, body);