Skip to content

Commit 582e1f1

Browse files
catamorphismcatamorphism
committed
Invalidate constraints correctly after an assignment expression
Modified typestate to throw away any constraints mentioning a variable on the LHS of an assignment, recv, assign_op, or on either side of a swap. Some code cleanup as well.
1 parent 818d7c9 commit 582e1f1

File tree

10 files changed

+441
-375
lines changed

10 files changed

+441
-375
lines changed

‎src/comp/front/ast.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,9 @@ type ident = str;
1111
// Functions may or may not have names.
1212
type fn_ident = option::t[ident];
1313

14+
// FIXME: with typestate constraint, could say
15+
// idents and types are the same length, and are
16+
// non-empty
1417
type path_ = rec(vec[ident] idents, vec[@ty] types);
1518

1619
type path = spanned[path_];

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

Lines changed: 25 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -112,28 +112,37 @@ fn set_in_postcond(uint i, &pre_and_post p) -> bool {
112112
// sets the ith bit in p's post
113113
auto was_set = tritv_get(p.postcondition, i);
114114
tritv_set(i, p.postcondition, ttrue);
115-
ret was_set != ttrue;
115+
ret was_set == dont_care;
116116
}
117117

118118
fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
119119
// sets the ith bit in p's post
120-
auto was_set = tritv_get(s.poststate, i);
121-
tritv_set(i, s.poststate, ttrue);
122-
ret was_set != ttrue;
120+
ret set_in_poststate_(i, s.poststate);
121+
}
122+
123+
fn set_in_poststate_(uint i, &poststate p) -> bool {
124+
auto was_set = tritv_get(p, i);
125+
tritv_set(i, p, ttrue);
126+
ret was_set == dont_care;
127+
123128
}
124129

125130
fn clear_in_poststate(uint i, &pre_and_post_state s) -> bool {
126131
// sets the ith bit in p's post
127-
auto was_set = tritv_get(s.poststate, i);
128-
tritv_set(i, s.poststate, tfalse);
129-
ret was_set != tfalse;
132+
ret clear_in_poststate_(i, s.poststate);
133+
}
134+
135+
fn clear_in_poststate_(uint i, &poststate s) -> bool {
136+
auto was_set = tritv_get(s, i);
137+
tritv_set(i, s, tfalse);
138+
ret was_set == dont_care;
130139
}
131140

132141
fn clear_in_postcond(uint i, &pre_and_post s) -> bool {
133142
// sets the ith bit in p's post
134143
auto was_set = tritv_get(s.postcondition, i);
135144
tritv_set(i, s.postcondition, tfalse);
136-
ret was_set != tfalse;
145+
ret was_set == dont_care;
137146
}
138147

139148
// Sets all the bits in a's precondition to equal the
@@ -222,6 +231,14 @@ fn implies(t a, t b) -> bool {
222231
tritv_difference(tmp, a);
223232
ret tritv_doesntcare(tmp);
224233
}
234+
235+
fn trit_str(trit t) -> str {
236+
alt (t) {
237+
case (dont_care) { "?" }
238+
case (ttrue) { "1" }
239+
case (tfalse) { "0" }
240+
}
241+
}
225242
//
226243
// Local Variables:
227244
// mode: rust

‎src/comp/middle/tstate/auxiliary.rs

Lines changed: 86 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ import tstate::ann::set_postcondition;
3939
import tstate::ann::ts_ann;
4040
import tstate::ann::clear_in_postcond;
4141
import tstate::ann::clear_in_poststate;
42+
import tstate::ann::clear_in_poststate_;
4243
import tritv::*;
4344

4445
import pretty::ppaux::constr_args_to_str;
@@ -655,8 +656,9 @@ tag if_ty {
655656
plain_if;
656657
}
657658

658-
fn local_node_id_to_def_id(&fn_ctxt fcx, &span sp, &node_id i) -> def_id {
659-
alt (fcx.ccx.tcx.def_map.find(i)) {
659+
fn local_node_id_to_def_id_strict(&fn_ctxt fcx, &span sp, &node_id i)
660+
-> def_id {
661+
alt (local_node_id_to_def(fcx, i)) {
660662
case (some(def_local(?d_id))) {
661663
ret d_id;
662664
}
@@ -675,30 +677,86 @@ fn local_node_id_to_def_id(&fn_ctxt fcx, &span sp, &node_id i) -> def_id {
675677
}
676678
}
677679

678-
fn forget_in_postcond(&fn_ctxt fcx, &span dead_sp,
679-
node_id parent_exp, node_id dead_v) {
680+
fn local_node_id_to_def(&fn_ctxt fcx, &node_id i) -> option::t[def]
681+
{ fcx.ccx.tcx.def_map.find(i) }
682+
683+
fn local_node_id_to_def_id(&fn_ctxt fcx, &node_id i) -> option::t[def_id] {
684+
alt (local_node_id_to_def(fcx, i)) {
685+
case (some(def_local(?d_id))) { some(d_id) }
686+
case (some (def_arg(?a_id))) { some(a_id) }
687+
case (_) { none }
688+
}
689+
}
690+
691+
/* FIXME should refactor this better */
692+
fn forget_in_postcond(&fn_ctxt fcx, node_id parent_exp, node_id dead_v) {
680693
// In the postcondition given by parent_exp, clear the bits
681694
// for any constraints mentioning dead_v
682-
auto d_id = local_node_id_to_def_id(fcx, dead_sp, dead_v);
683-
for (norm_constraint c in constraints(fcx)) {
684-
if (constraint_mentions(fcx, c, d_id)) {
685-
clear_in_postcond(c.bit_num,
686-
node_id_to_ts_ann(fcx.ccx, parent_exp).conditions);
695+
auto d = local_node_id_to_def_id(fcx, dead_v);
696+
alt (d) {
697+
case (some(?d_id)) {
698+
for (norm_constraint c in constraints(fcx)) {
699+
if (constraint_mentions(fcx, c, d_id)) {
700+
clear_in_postcond(c.bit_num,
701+
node_id_to_ts_ann(fcx.ccx, parent_exp).conditions);
702+
}
703+
}
687704
}
705+
case (_) {}
688706
}
689707
}
690708

691-
fn forget_in_poststate(&fn_ctxt fcx, &span dead_sp,
692-
node_id parent_exp, node_id dead_v) -> bool {
709+
fn forget_in_postcond_still_init(&fn_ctxt fcx, node_id parent_exp,
710+
node_id dead_v) {
711+
// In the postcondition given by parent_exp, clear the bits
712+
// for any constraints mentioning dead_v
713+
auto d = local_node_id_to_def_id(fcx, dead_v);
714+
alt (d) {
715+
case (some(?d_id)) {
716+
for (norm_constraint c in constraints(fcx)) {
717+
if (non_init_constraint_mentions(fcx, c, d_id)) {
718+
clear_in_postcond(c.bit_num,
719+
node_id_to_ts_ann(fcx.ccx, parent_exp).conditions);
720+
}
721+
}
722+
}
723+
case (_) { }
724+
}
725+
}
726+
727+
fn forget_in_poststate(&fn_ctxt fcx, &poststate p, node_id dead_v) -> bool {
693728
// In the poststate given by parent_exp, clear the bits
694729
// for any constraints mentioning dead_v
695-
auto d_id = local_node_id_to_def_id(fcx, dead_sp, dead_v);
730+
auto d = local_node_id_to_def_id(fcx, dead_v);
696731
auto changed = false;
697-
for (norm_constraint c in constraints(fcx)) {
698-
if (constraint_mentions(fcx, c, d_id)) {
699-
changed = clear_in_poststate(c.bit_num,
700-
node_id_to_ts_ann(fcx.ccx, parent_exp).states) || changed;
732+
alt (d) {
733+
case (some(?d_id)) {
734+
for (norm_constraint c in constraints(fcx)) {
735+
if (constraint_mentions(fcx, c, d_id)) {
736+
changed = clear_in_poststate_(c.bit_num, p) || changed;
737+
}
738+
}
739+
}
740+
case (_) {}
741+
}
742+
ret changed;
743+
}
744+
745+
fn forget_in_poststate_still_init(&fn_ctxt fcx, &poststate p, node_id dead_v)
746+
-> bool {
747+
// In the poststate given by parent_exp, clear the bits
748+
// for any constraints mentioning dead_v
749+
auto d = local_node_id_to_def_id(fcx, dead_v);
750+
auto changed = false;
751+
alt (d) {
752+
case (some(?d_id)) {
753+
for (norm_constraint c in constraints(fcx)) {
754+
if (non_init_constraint_mentions(fcx, c, d_id)) {
755+
changed = clear_in_poststate_(c.bit_num, p) || changed;
756+
}
757+
}
701758
}
759+
case (_) {}
702760
}
703761
ret changed;
704762
}
@@ -714,6 +772,18 @@ fn constraint_mentions(&fn_ctxt fcx, &norm_constraint c, &def_id v) -> bool {
714772
});
715773
}
716774

775+
fn non_init_constraint_mentions(&fn_ctxt fcx, &norm_constraint c,
776+
&def_id v) -> bool {
777+
ret (alt (c.c.node.c) {
778+
case (ninit(_)) {
779+
false
780+
}
781+
case (npred(_, ?args)) {
782+
args_mention(args, v)
783+
}
784+
});
785+
}
786+
717787

718788
fn args_mention(&vec[@constr_arg_use] args, &def_id v) -> bool {
719789
fn mentions(&def_id v, &@constr_arg_use a) -> bool {

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

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
1+
12
import front::ast::*;
3+
import std::option::*;
24
import std::vec;
35
import std::vec::len;
46
import std::vec::slice;
7+
import aux::local_node_id_to_def;
58
import aux::fn_ctxt;
69
import aux::fn_info;
710
import aux::log_tritv;
@@ -38,7 +41,9 @@ import tstate::ann::intersect;
3841
import tstate::ann::clone;
3942
import tstate::ann::set_in_postcond;
4043
import tstate::ann::set_in_poststate;
44+
import tstate::ann::set_in_poststate_;
4145
import tstate::ann::clear_in_poststate;
46+
import tstate::ann::clear_in_poststate_;
4247
import tritv::*;
4348

4449
fn bit_num(&fn_ctxt fcx, &constr_ c) -> uint {
@@ -219,6 +224,36 @@ fn kill_poststate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
219224
ret clear_in_poststate(bit_num(fcx, c),
220225
node_id_to_ts_ann(fcx.ccx, id).states);
221226
}
227+
228+
fn clear_in_poststate_expr(&fn_ctxt fcx, &@expr e, &poststate t) {
229+
alt (e.node) {
230+
case (expr_path(?p)) {
231+
alt (vec::last(p.node.idents)) {
232+
case (some(?i)) {
233+
alt (local_node_id_to_def(fcx, e.id)) {
234+
case (some(def_local(?d_id))) {
235+
clear_in_poststate_(bit_num(fcx,
236+
rec(id=d_id._1,
237+
c=ninit(i))), t);
238+
}
239+
case (some(_)) { /* ignore args (for now...) */ }
240+
case (_) {
241+
fcx.ccx.tcx.sess.bug("clear_in_poststate_expr: \
242+
unbound var"); }
243+
}
244+
}
245+
case (_) { fcx.ccx.tcx.sess.bug("clear_in_poststate_expr"); }
246+
}
247+
}
248+
case (_) { /* do nothing */ }
249+
}
250+
}
251+
252+
fn set_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
253+
&poststate t) -> bool {
254+
ret set_in_poststate_(bit_num(fcx, rec(id=id, c=ninit(ident))), t);
255+
}
256+
222257
//
223258
// Local Variables:
224259
// mode: rust

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

Lines changed: 19 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@ import aux::if_ty;
4848
import aux::if_check;
4949
import aux::plain_if;
5050
import aux::forget_in_postcond;
51+
import aux::forget_in_postcond_still_init;
5152

5253
import aux::constraints_expr;
5354
import aux::substitute_constr_args;
@@ -61,7 +62,6 @@ import bitvectors::seq_postconds;
6162
import bitvectors::intersect_postconds;
6263
import bitvectors::declare_var;
6364
import bitvectors::gen_poststate;
64-
import bitvectors::kill_poststate;
6565
import bitvectors::relax_precond_block;
6666
import bitvectors::gen;
6767
import front::ast::*;
@@ -274,27 +274,21 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
274274
auto enclosing = fcx.enclosing;
275275
auto num_local_vars = num_constraints(enclosing);
276276
fn do_rand_(fn_ctxt fcx, &@expr e) { find_pre_post_expr(fcx, e); }
277-
log "find_pre_post_expr (num_constraints =" + uistr(num_local_vars) +
278-
"):";
279-
log_expr(*e);
277+
280278
alt (e.node) {
281279
case (expr_call(?operator, ?operands)) {
282-
auto args = vec::clone[@expr](operands);
283-
vec::push[@expr](args, operator);
280+
auto args = vec::clone(operands);
281+
vec::push(args, operator);
284282
find_pre_post_exprs(fcx, args, e.id);
285283
/* see if the call has any constraints on its type */
286-
287-
log "a function: ";
288-
log_expr(*operator);
289-
auto pp = expr_pp(fcx.ccx, e);
290284
for (@ty::constr_def c in constraints_expr(fcx.ccx.tcx, operator))
291285
{
292286
auto i =
293287
bit_num(fcx,
294288
rec(id=c.node.id._1,
295289
c=substitute_constr_args(fcx.ccx.tcx,
296290
operands, c)));
297-
require(i, pp);
291+
require(i, expr_pp(fcx.ccx, e));
298292
}
299293

300294
/* if this is a failing call, its postcondition sets everything */
@@ -304,8 +298,8 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
304298
}
305299
}
306300
case (expr_spawn(_, _, ?operator, ?operands)) {
307-
auto args = vec::clone[@expr](operands);
308-
vec::push[@expr](args, operator);
301+
auto args = vec::clone(operands);
302+
vec::push(args, operator);
309303
find_pre_post_exprs(fcx, args, e.id);
310304
}
311305
case (expr_vec(?args, _, _)) {
@@ -356,7 +350,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
356350
}
357351
case (expr_rec(?fields, ?maybe_base)) {
358352
auto es = field_exprs(fields);
359-
vec::plus_option[@expr](es, maybe_base);
353+
vec::plus_option(es, maybe_base);
360354
find_pre_post_exprs(fcx, es, e.id);
361355
}
362356
case (expr_move(?lhs, ?rhs)) {
@@ -366,17 +360,22 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
366360
}
367361
case (_) { find_pre_post_exprs(fcx, [lhs, rhs], e.id); }
368362
}
369-
forget_in_postcond(fcx, rhs.span, e.id, rhs.id);
363+
forget_in_postcond(fcx, e.id, rhs.id);
370364
}
371365
case (expr_swap(?lhs, ?rhs)) {
372366
// Both sides must already be initialized
373367

374368
find_pre_post_exprs(fcx, [lhs, rhs], e.id);
369+
forget_in_postcond_still_init(fcx, e.id, lhs.id);
370+
forget_in_postcond_still_init(fcx, e.id, rhs.id);
371+
// Could be more precise and swap the roles of lhs and rhs
372+
// in any constraints
375373
}
376374
case (expr_assign(?lhs, ?rhs)) {
377375
alt (lhs.node) {
378376
case (expr_path(?p)) {
379377
gen_if_local(fcx, lhs, rhs, e.id, lhs.id, p);
378+
forget_in_postcond_still_init(fcx, e.id, lhs.id);
380379
}
381380
case (_) { find_pre_post_exprs(fcx, [lhs, rhs], e.id); }
382381
}
@@ -385,7 +384,8 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
385384
alt (rhs.node) {
386385
case (expr_path(?p)) {
387386
gen_if_local(fcx, rhs, lhs, e.id, rhs.id, p);
388-
}
387+
forget_in_postcond_still_init(fcx, e.id, lhs.id);
388+
}
389389
case (_) {
390390
// doesn't check that rhs is an lval, but
391391
// that's probably ok
@@ -399,6 +399,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
399399
already be initialized */
400400

401401
find_pre_post_exprs(fcx, [lhs, rhs], e.id);
402+
forget_in_postcond_still_init(fcx, e.id, lhs.id);
402403
}
403404
case (expr_lit(_)) { clear_pp(expr_pp(fcx.ccx, e)); }
404405
case (expr_ret(?maybe_val)) {
@@ -585,8 +586,8 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s) {
585586

586587
alt (an_init.op) {
587588
case (init_move) {
588-
forget_in_postcond(fcx, an_init.expr.span,
589-
id, an_init.expr.id);
589+
forget_in_postcond(fcx, id,
590+
an_init.expr.id);
590591
}
591592
case (_) { /* nothing gets deinitialized */ }
592593
}

0 commit comments

Comments
 (0)