Refactor some typestate-related data structures

Author: catamorphism

src/comp/middle/tstate/auxiliary.rs

@@ -76,12 +76,12 @@ fn comma_str(vec[@constr_arg_use] args) -> str {
     ret res;
 }
 
-fn constraint_to_str(ty::ctxt tcx, constr c) -> str {
-    alt (c.node) {
-        case (ninit(?i, _)) {
+fn constraint_to_str(&ty::ctxt tcx, &constr c) -> str {
+    alt (c.node.c) {
+        case (ninit(?i)) {
             ret "init(" + i + " [" + tcx.sess.span_str(c.span) + "])";
         }
-        case (npred(?p, _, ?args)) {
+        case (npred(?p, ?args)) {
             ret path_to_str(p) + "(" + comma_str(args) + ")"
                 + "[" + tcx.sess.span_str(c.span) + "]";
         }
@@ -101,7 +101,7 @@ fn bitv_to_str(fn_ctxt fcx, bitv::t v) -> str {
   ret s;
 }
 
-fn log_bitv(fn_ctxt fcx, bitv::t v) {
+fn log_bitv(&fn_ctxt fcx, &bitv::t v) {
     log(bitv_to_str(fcx, v));
 }
 
@@ -208,43 +208,50 @@ fn print_idents(vec[ident] idents) -> () {
 /* data structures */
 
 /**********************************************************************/
-/* mapping from def_id to bit number and other data
-   (ident/path/span are there for error-logging purposes) */
+/* Two different data structures represent constraints in different
+ contexts: constraint and norm_constraint.
 
-/* FIXME very confused about why we have all these different types. */
+constraint gets used to record constraints in a table keyed by def_ids.
+cinit constraints represent a single constraint, for the initialization
+state of a variable; a cpred constraint, with a single operator and a
+list of possible argument lists, could represent several constraints at
+once.
+
+norm_constraint, in contrast, gets used when handling an instance
+of a constraint rather than a definition of a constraint. It can
+also be init or pred (ninit or npred), but the npred case just has
+a single argument list. 
+
+The representation of constraints, where multiple instances of the
+same predicate are collapsed into one entry in the table, makes it
+easier to look up a specific instance.
+
+Both types are in constrast with the constraint type defined in
+front::ast, which is for predicate constraints only, and is what
+gets generated by the parser. aux and ast share the same type
+to represent predicate *arguments* however. This type
+(constr_arg_general) is parameterized (see comments in front::ast).
+
+Both types store an ident and span, for error-logging purposes.
+*/
 
 type pred_desc_ = rec(vec[@constr_arg_use] args,
                       uint bit_num);
 type pred_desc = spanned[pred_desc_];
 tag constraint {
-    cinit(uint, span, def_id, ident);
-    cpred(path, def_id, @mutable vec[pred_desc]);
+    cinit(uint, span, ident);
+    cpred(path, @mutable vec[pred_desc]);
 }
-tag constr_ {
-    ninit(ident, def_id);
-    npred(path, def_id, vec[@constr_arg_use]);
+tag constr__ {
+    ninit(ident);
+    npred(path, vec[@constr_arg_use]);
 }
+type constr_ = rec(def_id id, constr__ c);
 type constr = spanned[constr_];
 type norm_constraint = rec(uint bit_num,
                            constr c);
-/* "constraint occurrence" to disambiguate
-   between constraints. either "this is an
-   init constraint", or the list of args for
-   a pred. */
-tag constr_occ {
-    occ_init;
-    occ_args(vec[@constr_arg_use]);
-}
-   
 type constr_map = @std::map::hashmap[def_id, constraint];
 
-fn constr_id(&constr c) -> def_id {
-    ret (alt (c.node) {
-            case (ninit(_, ?i))    { i }
-            case (npred(_, ?i, _)) { i }
-        })
-}
-
 type fn_info  = rec(constr_map constrs, uint num_constraints, controlflow cf);
 
 /* mapping from node ID to typestate annotation */
@@ -529,16 +536,16 @@ fn ann_to_def(&crate_ctxt ccx, &ann a) -> option::t[def] {
     ret ccx.tcx.def_map.find(a.id);
 }
 
-fn norm_a_constraint(&constraint c) -> vec[norm_constraint] {
+fn norm_a_constraint(&def_id id, &constraint c) -> vec[norm_constraint] {
     alt (c) {
-        case (cinit(?n, ?sp, ?id, ?i)) {
-            ret [rec(bit_num=n, c=respan(sp, ninit(i, id)))];
+        case (cinit(?n, ?sp, ?i)) {
+            ret [rec(bit_num=n, c=respan(sp, rec(id=id, c=ninit(i))))];
         }
-        case (cpred(?p, ?id, ?descs)) {
+        case (cpred(?p, ?descs)) {
             let vec[norm_constraint] res = [];
             for (pred_desc pd in *descs) {
                 vec::push(res, rec(bit_num=pd.node.bit_num,
-                  c=respan(pd.span, npred(p, id, pd.node.args))));
+                  c=respan(pd.span, rec(id=id, c=npred(p, pd.node.args)))));
             }
             ret res;
         }
@@ -551,7 +558,7 @@ fn constraints(&fn_ctxt fcx) -> vec[norm_constraint] {
     let vec[norm_constraint] res = [];
     for each (@tup(def_id, constraint) p in
               fcx.enclosing.constrs.items()) {
-        res += norm_a_constraint(p._1);
+        res += norm_a_constraint(p._0, p._1);
     }
     ret res;
 }
@@ -572,13 +579,6 @@ fn match_args(&fn_ctxt fcx, vec[pred_desc] occs,
     fcx.ccx.tcx.sess.bug("match_args: no match for occurring args");  
 }
 
-fn constr_to_constr_occ(&ty::ctxt tcx, &constr_ c) -> constr_occ {
-    alt (c) {
-        case (ninit(_, _)) { ret occ_init; }
-        case (npred(_, _, ?args)) { ret occ_args(args); }
-    }
-}
-
 fn def_id_for_constr(ty::ctxt tcx, uint t) -> def_id {
     alt (tcx.def_map.find(t)) {
         case (none) {
@@ -627,8 +627,9 @@ fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constr {
             alt (operator.node) {
                 case (expr_path(?p, ?a)) {
                     ret respan(e.span,
-                               npred(p, def_id_for_constr(tcx, a.id),
-                                     exprs_to_constr_args(tcx, args))); 
+                          rec(id=def_id_for_constr(tcx, a.id),
+                              c=npred(p, 
+                                      exprs_to_constr_args(tcx, args)))); 
                 }
                 case (_) {
                     tcx.sess.span_err(operator.span, "Internal error: " +
@@ -648,20 +649,14 @@ fn pred_desc_to_str(&pred_desc p) -> str {
          pretty::ppaux::constr_args_to_str_1(p.node.args) + ">");
 }
 
-fn substitute_constr_args_(&ty::ctxt cx,
+fn substitute_constr_args(&ty::ctxt cx,
                           &vec[@expr] actuals, &@ast::constr c)
-    -> vec[@constr_arg_use] {
+    -> constr__ {
     let vec[@constr_arg_use] res = [];
     for (@constr_arg a in c.node.args) {
         res += [substitute_arg(cx, actuals, a)];
     }
-    ret res;
-
-}
-
-fn substitute_constr_args(&ty::ctxt cx,
-      &vec[@expr] actuals, &@ast::constr c) -> constr_occ {
-    ret occ_args(substitute_constr_args_(cx, actuals, c));
+    ret npred(c.node.path, res);
 }
 
 type subst = vec[tup(arg, @expr)];
@@ -683,6 +678,16 @@ fn substitute_arg(&ty::ctxt cx, &vec[@expr] actuals, @ast::constr_arg a)
     }
 }
 
+fn path_to_ident(&ty::ctxt cx, &path p) -> ident {
+    alt (vec::last(p.node.idents)) {
+        case (none) {
+            cx.sess.span_err(p.span, "Malformed path");
+        }
+        case (some(?i)) {
+            ret i;
+        }
+    }
+}
 //
 // Local Variables:
 // mode: rust

src/comp/middle/tstate/bitvectors.rs

@@ -9,13 +9,13 @@ import aux::fn_ctxt;
 import aux::fn_info;
 import aux::log_bitv;
 import aux::num_constraints;
-import aux::constr_occ;
-import aux::occ_init;
-import aux::occ_args;
 import aux::cinit;
 import aux::cpred;
+import aux::ninit;
+import aux::npred;
 import aux::pred_desc;
 import aux::match_args;
+import aux::constr_;
 
 import tstate::aux::ann_to_ts_ann;
 import tstate::ann::pre_and_post;
@@ -35,13 +35,13 @@ import tstate::ann::set_in_postcond;
 import tstate::ann::set_in_poststate;
 import tstate::ann::clear_in_poststate;
 
-fn bit_num(&fn_ctxt fcx, &def_id v, &constr_occ o) -> uint {
-    assert (fcx.enclosing.constrs.contains_key(v));
-    auto res = fcx.enclosing.constrs.get(v);
-    alt (o) {
-        case (occ_init) {
+fn bit_num(&fn_ctxt fcx, &constr_ c) -> uint {
+    assert (fcx.enclosing.constrs.contains_key(c.id));
+    auto res = fcx.enclosing.constrs.get(c.id);
+    alt (c.c) {
+        case (ninit(_)) {
             alt (res) {
-                case (cinit(?n,_,_,_)) {
+                case (cinit(?n,_,_)) {
                     ret n;
                 }
                 case (_) {
@@ -50,9 +50,9 @@ fn bit_num(&fn_ctxt fcx, &def_id v, &constr_occ o) -> uint {
                 }
             }
         }
-        case (occ_args(?args)) {
+        case (npred(_, ?args)) {
             alt (res) {
-                case (cpred(_, _, ?descs)) {
+                case (cpred(_, ?descs)) {
                     ret match_args(fcx, *descs, args);
                 }
                 case (_) {
@@ -64,8 +64,8 @@ fn bit_num(&fn_ctxt fcx, &def_id v, &constr_occ o) -> uint {
     }
 }
 
-fn promises(&fn_ctxt fcx, &poststate p, &def_id v, &constr_occ o) -> bool {
-    ret bitv::get(p, bit_num(fcx, v, o));
+fn promises(&fn_ctxt fcx, &poststate p, &constr_ c) -> bool {
+    ret bitv::get(p, bit_num(fcx, c));
 }
 
 // Given a list of pres and posts for exprs e0 ... en,
@@ -143,27 +143,26 @@ fn intersect_postconds(&vec[postcond] pcs) -> postcond {
   ret intersect_postconds_go(bitv::clone(pcs.(0)), pcs);
 }
 
-fn gen(&fn_ctxt fcx, &ann a, &def_id id, &constr_occ o) -> bool {
-  ret set_in_postcond(bit_num(fcx, id, o),
+fn gen(&fn_ctxt fcx, &ann a, &constr_ c) -> bool {
+  ret set_in_postcond(bit_num(fcx, c),
                       (ann_to_ts_ann(fcx.ccx, a)).conditions);
 }
 
-fn declare_var(&fn_ctxt fcx, def_id id, prestate pre)
-   -> prestate {
+fn declare_var(&fn_ctxt fcx, &constr_ c, prestate pre) -> prestate {
     auto res = clone(pre);
-    relax_prestate(bit_num(fcx, id, occ_init), res);
+    relax_prestate(bit_num(fcx, c), res);
     ret res;
 }
 
-fn gen_poststate(&fn_ctxt fcx, &ann a, &def_id id, &constr_occ o) -> bool {
+fn gen_poststate(&fn_ctxt fcx, &ann a, &constr_ c) -> bool {
   log "gen_poststate";
-  ret set_in_poststate(bit_num(fcx, id, o),
+  ret set_in_poststate(bit_num(fcx, c),
                        (ann_to_ts_ann(fcx.ccx, a)).states);
 }
 
-fn kill_poststate(&fn_ctxt fcx, &ann a, def_id id, &constr_occ o) -> bool {
+fn kill_poststate(&fn_ctxt fcx, &ann a, &constr_ c) -> bool {
   log "kill_poststate";
-  ret clear_in_poststate(bit_num(fcx, id, o),
+  ret clear_in_poststate(bit_num(fcx, c),
                          (ann_to_ts_ann(fcx.ccx, a)).states);
 }
 

src/comp/middle/tstate/ck.rs

@@ -133,8 +133,9 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
 
     auto cf = fcx.enclosing.cf;
     /* Finally, check that the return value is initialized */
+    let aux::constr_ ret_c = rec(id=fcx.id, c=aux::ninit(fcx.name));
     if (f.proto == ast::proto_fn
-        && ! promises(fcx, *post, fcx.id, aux::occ_init)
+        && ! promises(fcx, *post, ret_c)
         && ! type_is_nil(fcx.ccx.tcx,
                          ret_ty_of_fn(fcx.ccx.tcx, a))
         && cf == return) {
@@ -148,7 +149,7 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
         // check that this really always fails
         // the fcx.id bit means "returns" for a returning fn,
         // "diverges" for a non-returning fn
-        if (! promises(fcx, *post, fcx.id, aux::occ_init)) {
+        if (! promises(fcx, *post, ret_c)) {
             fcx.ccx.tcx.sess.span_err(f.body.span,
               "In non-returning function " + fcx.name +
               ", some control paths may return to the caller");