Handle lazy binops properly in typestate

The typestate analysis now reflects that the second operand of a
logical and or or may not be evaluated.

4 files changed, 44 insertions, 7 deletions

diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index d4495fee622..7e97a11d166 100644
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -434,10 +434,19 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
             find_pre_post_expr(fcx, ternary_to_if(e));
         }
         case (expr_binary(?bop, ?l, ?r)) {
-            /* *unless* bop is lazy (e.g. and, or)? 
-               FIXME */
-
-            find_pre_post_exprs(fcx, [l, r], e.id);
+            if (lazy_binop(bop)) {
+                find_pre_post_expr(fcx, l);
+                find_pre_post_expr(fcx, r);
+                auto overall_pre = seq_preconds(fcx,
+                   [expr_pp(fcx.ccx, l), expr_pp(fcx.ccx, r)]);
+                set_precondition(node_id_to_ts_ann(fcx.ccx, e.id),
+                                 overall_pre);
+                set_postcondition(node_id_to_ts_ann(fcx.ccx, e.id),
+                                  expr_postcond(fcx.ccx, l));
+            }
+            else {
+                find_pre_post_exprs(fcx, [l, r], e.id);
+            }
         }
         case (expr_send(?l, ?r)) {
             find_pre_post_exprs(fcx, [l, r], e.id);
diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index d5676fad7ef..91ea1a2c01f 100644
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -420,8 +420,18 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
             ret find_pre_post_state_expr(fcx, pres, ternary_to_if(e));
         }
         case (expr_binary(?bop, ?l, ?r)) {
-            /* FIXME: what if bop is lazy? */
-            ret find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure);
+            if (lazy_binop(bop)) {
+                auto changed = find_pre_post_state_expr(fcx, pres, l);
+                changed |= find_pre_post_state_expr(fcx,
+                              expr_poststate(fcx.ccx, l), r);
+                ret changed
+                    | set_prestate_ann(fcx.ccx, e.id, pres)
+                    | set_poststate_ann(fcx.ccx, e.id,
+                                        expr_poststate(fcx.ccx, l));
+            }
+            else {
+                ret find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure);
+            }
         }
         case (expr_send(?l, ?r)) {
             ret find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure);
@@ -507,7 +517,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
                 find_pre_post_state_expr(fcx, pres, val);
             auto e_post = expr_poststate(fcx.ccx, val);
             auto a_post;
-            if (vec::len[arm](alts) > 0u) {
+            if (vec::len(alts) > 0u) {
                 a_post = false_postcond(num_constrs);
                 for (arm an_alt in alts) {
                     changed |= find_pre_post_state_block
diff --git a/src/test/compile-fail/and-init.rs b/src/test/compile-fail/and-init.rs
new file mode 100644
index 00000000000..7fa9c543557
--- /dev/null
+++ b/src/test/compile-fail/and-init.rs
@@ -0,0 +1,9 @@
+// xfail-stage0
+// error-pattern: Unsatisfied precondition constraint (for example, init(i
+
+fn main() {
+  let int i;
+
+  log (false && {i = 5; true});
+  log i;
+}
\ No newline at end of file
diff --git a/src/test/compile-fail/or-init.rs b/src/test/compile-fail/or-init.rs
new file mode 100644
index 00000000000..aec1b49e6ca
--- /dev/null
+++ b/src/test/compile-fail/or-init.rs
@@ -0,0 +1,9 @@
+// xfail-stage0
+// error-pattern: Unsatisfied precondition constraint (for example, init(i
+
+fn main() {
+  let int i;
+
+  log (false || {i = 5; true});
+  log i;
+}
\ No newline at end of file