From 18883fea3a5c3c1a9af5c8a29464b83c0c81757b Mon Sep 17 00:00:00 2001
From: Tim Chevalier <chevalier@alum.wellesley.edu>
Date: Fri, 27 May 2011 20:41:48 -0700
Subject: [PATCH] In pre/postcondition computation, failing calls should set
 the postcondition

A non-returning call should have a postcondition in which all predicates
are true -- not just a poststate. Otherwise, alt expressions where
one or more branches terminate in a non-returning call and others
initialize a variable get rejected.

Includes a test case.
---
 src/comp/middle/tstate/pre_post_conditions.rs | 15 ++++++++--
 src/test/run-pass/nested-alts.rs              | 30 +++++++++++++++++++
 2 files changed, 42 insertions(+), 3 deletions(-)
 create mode 100644 src/test/run-pass/nested-alts.rs

diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index 8d9e08e51a32..892b9d6aadbc 100644
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -39,6 +39,7 @@ import aux::ann_to_def;
 import aux::ann_to_def_strict;
 import aux::ann_to_ts_ann;
 import aux::set_postcond_false;
+import aux::controlflow_expr;
 
 import bitvectors::seq_preconds;
 import bitvectors::union_postconds;
@@ -78,6 +79,7 @@ import front::ast::def;
 import front::ast::lit;
 import front::ast::init_op;
 import front::ast::controlflow;
+import front::ast::noreturn;
 import front::ast::return;
 import front::ast::_fn;
 import front::ast::_obj;
@@ -294,6 +296,13 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             auto args = vec::clone[@expr](operands);
             vec::push[@expr](args, operator);
             find_pre_post_exprs(fcx, args, a);
+            /* if this is a failing call, its postcondition sets everything */
+            alt (controlflow_expr(fcx.ccx, operator)) {
+                case (noreturn) {
+                    set_postcond_false(fcx.ccx, a);
+                }
+                case (_) { }
+            }
         }
         case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
             auto args = vec::clone[@expr](operands);
@@ -495,8 +504,8 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
         case (expr_index(?e, ?sub, ?a)) {
             find_pre_post_exprs(fcx, [e, sub], a);
         }
-        case (expr_alt(?e, ?alts, ?a)) {
-            find_pre_post_expr(fcx, e);
+        case (expr_alt(?ex, ?alts, ?a)) {
+            find_pre_post_expr(fcx, ex);
             fn do_an_alt(&fn_ctxt fcx, &arm an_alt) -> pre_and_post {
                 find_pre_post_block(fcx, an_alt.block);
                 ret block_pp(fcx.ccx, an_alt.block);
@@ -510,7 +519,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
                 intersect(pp.postcondition, next.postcondition);
                 ret pp;
             }
-            auto antec_pp = pp_clone(expr_pp(fcx.ccx, e)); 
+            auto antec_pp = pp_clone(expr_pp(fcx.ccx, ex)); 
             auto e_pp  = @rec(precondition=empty_prestate(num_local_vars),
                              postcondition=false_postcond(num_local_vars));
             auto g = bind combine_pp(antec_pp, fcx, _, _);
diff --git a/src/test/run-pass/nested-alts.rs b/src/test/run-pass/nested-alts.rs
new file mode 100644
index 000000000000..31eb0e4beae3
--- /dev/null
+++ b/src/test/run-pass/nested-alts.rs
@@ -0,0 +1,30 @@
+use std;
+import std::option::*;
+
+fn baz() -> ! {
+  fail;
+}
+
+fn foo() {
+   alt (some[int](5)) {
+     case (some[int](?x)) {
+       auto bar;
+       alt (none[int]) {
+         case (none[int]) {
+           bar = 5;
+         }
+         case (_) {
+           baz();
+         }
+       }
+       log bar;
+     }
+     case (none[int]) {
+       log "hello";
+     }
+   }
+}
+
+fn main() {
+  foo();
+}