2011-06-15 13:19:50 -05:00
|
|
|
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
import tritv::*;
|
2011-03-24 14:12:04 -05:00
|
|
|
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
type precond = t;
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-07-13 17:44:09 -05:00
|
|
|
/* 2 means "this constraint may or may not be true after execution"
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
1 means "this constraint is definitely true after execution"
|
|
|
|
0 means "this constraint is definitely false after execution" */
|
|
|
|
type postcond = t;
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-06-16 18:55:46 -05:00
|
|
|
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
/* 2 means "don't know about this constraint"
|
|
|
|
1 means "this constraint is definitely true before entry"
|
|
|
|
0 means "this constraint is definitely false on entry" */
|
|
|
|
type prestate = t;
|
2011-06-16 18:55:46 -05:00
|
|
|
|
|
|
|
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
/* similar to postcond */
|
|
|
|
type poststate = t;
|
2011-06-16 18:55:46 -05:00
|
|
|
|
|
|
|
|
|
|
|
/* 1 means "this variable is definitely initialized"
|
|
|
|
0 means "don't know whether this variable is
|
|
|
|
initialized" */
|
|
|
|
|
2011-07-13 17:44:09 -05:00
|
|
|
/*
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
This says: this expression requires the constraints whose value is 1 in
|
|
|
|
<pre> to be true, and given the precondition, it guarantees that the
|
|
|
|
constraints in <post> whose values are 1 are true, and that the constraints
|
|
|
|
in <post> whose values are 0 are false.
|
|
|
|
*/
|
2011-06-16 18:55:46 -05:00
|
|
|
|
|
|
|
/* named thus so as not to confuse with prestate and poststate */
|
2011-07-27 07:19:39 -05:00
|
|
|
type pre_and_post = @{precondition: precond, postcondition: postcond};
|
2011-06-15 13:19:50 -05:00
|
|
|
|
|
|
|
|
2011-03-24 14:12:04 -05:00
|
|
|
/* FIXME: once it's implemented: */
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
// : ((*.precondition).nbits == (*.postcondition).nbits);
|
2011-07-27 07:19:39 -05:00
|
|
|
type pre_and_post_state = {prestate: prestate, poststate: poststate};
|
2011-04-04 16:31:49 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
type ts_ann = @{conditions: pre_and_post, states: pre_and_post_state};
|
2011-03-24 14:12:04 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
fn true_precond(num_vars: uint) -> precond { be create_tritv(num_vars); }
|
2011-03-24 14:12:04 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
fn true_postcond(num_vars: uint) -> postcond { be true_precond(num_vars); }
|
2011-03-24 14:12:04 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
fn empty_prestate(num_vars: uint) -> prestate { be true_precond(num_vars); }
|
2011-04-06 19:56:44 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
fn empty_poststate(num_vars: uint) -> poststate { be true_precond(num_vars); }
|
2011-04-06 19:56:44 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
fn false_postcond(num_vars: uint) -> postcond {
|
|
|
|
let rslt = create_tritv(num_vars);
|
2011-06-24 12:04:08 -05:00
|
|
|
tritv_set_all(rslt);
|
|
|
|
ret rslt;
|
Further work on typestate_check
Lots of work on typestate_check, seems to get a lot of the way
through checking the standard library.
* Added for, for_each, assign_op, bind, cast, put, check, break,
and cont. (I'm not sure break and cont are actually handled correctly.)
* Fixed side-effect bug in seq_preconds so that unioning the
preconditions of a sequence of statements or expressions
is handled correctly.
* Pass poststate correctly through a stmt_decl.
* Handle expr_ret and expr_fail properly (after execution of a ret
or fail, everything is true -- this is needed to handle ifs and alts
where one branch is a ret or fail)
* Fixed bug in set_prestate_ann where a thing that needed to be
mutated wasn't getting passed as an alias
* Fixed bug in how expr_alt was treated (zero is not the identity
for intersect, who knew, right?)
* Update logging to reflect log_err vs. log
* Fixed find_locals so as to return all local decls and exclude
function arguments.
* Make union_postconds work on an empty vector (needed to handle
empty blocks correctly)
* Added _vec.cat_options, which takes a list of option[T] to a list
of T, ignoring any Nones
* Added two test cases.
2011-04-20 14:11:01 -05:00
|
|
|
}
|
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
fn empty_pre_post(num_vars: uint) -> pre_and_post {
|
|
|
|
ret @{precondition: empty_prestate(num_vars),
|
|
|
|
postcondition: empty_poststate(num_vars)};
|
2011-03-24 14:12:04 -05:00
|
|
|
}
|
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
fn empty_states(num_vars: uint) -> pre_and_post_state {
|
|
|
|
ret {prestate: true_precond(num_vars),
|
|
|
|
poststate: true_postcond(num_vars)};
|
2011-04-04 16:31:49 -05:00
|
|
|
}
|
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
fn empty_ann(num_vars: uint) -> ts_ann {
|
|
|
|
ret @{conditions: empty_pre_post(num_vars),
|
|
|
|
states: empty_states(num_vars)};
|
2011-04-06 19:56:44 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn get_pre(p: pre_and_post) -> precond { ret p.precondition; }
|
2011-03-24 14:12:04 -05:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn get_post(p: pre_and_post) -> postcond { ret p.postcondition; }
|
2011-03-24 14:12:04 -05:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn difference(p1: precond, p2: precond) -> bool {
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
ret tritv_difference(p1, p2);
|
2011-03-24 14:12:04 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn union(p1: precond, p2: precond) -> bool { ret tritv_union(p1, p2); }
|
2011-03-24 14:12:04 -05:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn intersect(p1: precond, p2: precond) -> bool {
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
ret tritv_intersect(p1, p2);
|
|
|
|
}
|
2011-04-12 21:03:52 -05:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn pps_len(p: pre_and_post) -> uint {
|
2011-06-15 13:19:50 -05:00
|
|
|
// gratuitous check
|
|
|
|
|
|
|
|
assert (p.precondition.nbits == p.postcondition.nbits);
|
|
|
|
ret p.precondition.nbits;
|
2011-03-24 14:12:04 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn require(i: uint, p: pre_and_post) {
|
2011-06-15 13:19:50 -05:00
|
|
|
// sets the ith bit in p's pre
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
tritv_set(i, p.precondition, ttrue);
|
2011-06-09 11:56:35 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn require_and_preserve(i: uint, p: pre_and_post) {
|
2011-06-15 13:19:50 -05:00
|
|
|
// sets the ith bit in p's pre and post
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
tritv_set(i, p.precondition, ttrue);
|
|
|
|
tritv_set(i, p.postcondition, ttrue);
|
2011-04-04 16:31:49 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn set_in_postcond(i: uint, p: pre_and_post) -> bool {
|
2011-06-15 13:19:50 -05:00
|
|
|
// sets the ith bit in p's post
|
2011-07-08 23:50:09 -05:00
|
|
|
ret set_in_postcond_(i, p.postcondition);
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn set_in_postcond_(i: uint, p: postcond) -> bool {
|
2011-07-27 07:19:39 -05:00
|
|
|
let was_set = tritv_get(p, i);
|
2011-07-08 23:50:09 -05:00
|
|
|
tritv_set(i, p, ttrue);
|
2011-06-27 20:12:37 -05:00
|
|
|
ret was_set != ttrue;
|
2011-04-12 14:16:21 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn set_in_poststate(i: uint, s: pre_and_post_state) -> bool {
|
2011-06-15 13:19:50 -05:00
|
|
|
// sets the ith bit in p's post
|
2011-06-25 00:17:17 -05:00
|
|
|
ret set_in_poststate_(i, s.poststate);
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn set_in_poststate_(i: uint, p: poststate) -> bool {
|
2011-07-27 07:19:39 -05:00
|
|
|
let was_set = tritv_get(p, i);
|
2011-06-25 00:17:17 -05:00
|
|
|
tritv_set(i, p, ttrue);
|
2011-06-27 20:12:37 -05:00
|
|
|
ret was_set != ttrue;
|
2011-06-25 00:17:17 -05:00
|
|
|
|
2011-04-06 19:56:44 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn clear_in_poststate(i: uint, s: pre_and_post_state) -> bool {
|
2011-06-15 13:19:50 -05:00
|
|
|
// sets the ith bit in p's post
|
2011-06-25 00:17:17 -05:00
|
|
|
ret clear_in_poststate_(i, s.poststate);
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn clear_in_poststate_(i: uint, s: poststate) -> bool {
|
2011-07-27 07:19:39 -05:00
|
|
|
let was_set = tritv_get(s, i);
|
2011-06-25 00:17:17 -05:00
|
|
|
tritv_set(i, s, tfalse);
|
2011-06-27 20:12:37 -05:00
|
|
|
ret was_set != tfalse;
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn clear_in_prestate(i: uint, s: pre_and_post_state) -> bool {
|
2011-06-27 20:12:37 -05:00
|
|
|
// sets the ith bit in p's pre
|
|
|
|
ret clear_in_prestate_(i, s.prestate);
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn clear_in_prestate_(i: uint, s: prestate) -> bool {
|
2011-07-27 07:19:39 -05:00
|
|
|
let was_set = tritv_get(s, i);
|
2011-06-27 20:12:37 -05:00
|
|
|
tritv_set(i, s, tfalse);
|
|
|
|
ret was_set != tfalse;
|
2011-05-20 21:50:29 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn clear_in_postcond(i: uint, s: pre_and_post) -> bool {
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
// sets the ith bit in p's post
|
2011-07-27 07:19:39 -05:00
|
|
|
let was_set = tritv_get(s.postcondition, i);
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
tritv_set(i, s.postcondition, tfalse);
|
2011-06-27 20:12:37 -05:00
|
|
|
ret was_set != tfalse;
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-04-06 19:56:44 -05:00
|
|
|
// Sets all the bits in a's precondition to equal the
|
|
|
|
// corresponding bit in p's precondition.
|
2011-09-12 04:27:30 -05:00
|
|
|
fn set_precondition(a: ts_ann, p: precond) {
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
tritv_copy(a.conditions.precondition, p);
|
2011-04-06 19:56:44 -05:00
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-04-06 19:56:44 -05:00
|
|
|
// Sets all the bits in a's postcondition to equal the
|
|
|
|
// corresponding bit in p's postcondition.
|
2011-09-12 04:27:30 -05:00
|
|
|
fn set_postcondition(a: ts_ann, p: postcond) {
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
tritv_copy(a.conditions.postcondition, p);
|
2011-04-06 19:56:44 -05:00
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-04-07 20:15:56 -05:00
|
|
|
// Sets all the bits in a's prestate to equal the
|
|
|
|
// corresponding bit in p's prestate.
|
2011-09-12 04:27:30 -05:00
|
|
|
fn set_prestate(a: ts_ann, p: prestate) -> bool {
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
ret tritv_copy(a.states.prestate, p);
|
2011-04-07 20:15:56 -05:00
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-04-07 20:15:56 -05:00
|
|
|
// Sets all the bits in a's postcondition to equal the
|
|
|
|
// corresponding bit in p's postcondition.
|
2011-09-12 04:27:30 -05:00
|
|
|
fn set_poststate(a: ts_ann, p: poststate) -> bool {
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
ret tritv_copy(a.states.poststate, p);
|
2011-04-12 14:16:21 -05:00
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-04-12 14:16:21 -05:00
|
|
|
// Set all the bits in p that are set in new
|
2011-09-12 04:27:30 -05:00
|
|
|
fn extend_prestate(p: prestate, new: poststate) -> bool {
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
ret tritv_union(p, new);
|
2011-04-07 20:15:56 -05:00
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-04-06 19:56:44 -05:00
|
|
|
// Set all the bits in p that are set in new
|
2011-09-12 04:27:30 -05:00
|
|
|
fn extend_poststate(p: poststate, new: poststate) -> bool {
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
ret tritv_union(p, new);
|
2011-04-06 19:56:44 -05:00
|
|
|
}
|
|
|
|
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
// Sets the given bit in p to "don't care"
|
|
|
|
// FIXME: is this correct?
|
2011-09-12 04:27:30 -05:00
|
|
|
fn relax_prestate(i: uint, p: prestate) -> bool {
|
2011-07-27 07:19:39 -05:00
|
|
|
let was_set = tritv_get(p, i);
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
tritv_set(i, p, dont_care);
|
|
|
|
ret was_set != dont_care;
|
Further work on typestate_check
Lots of work on typestate_check, seems to get a lot of the way
through checking the standard library.
* Added for, for_each, assign_op, bind, cast, put, check, break,
and cont. (I'm not sure break and cont are actually handled correctly.)
* Fixed side-effect bug in seq_preconds so that unioning the
preconditions of a sequence of statements or expressions
is handled correctly.
* Pass poststate correctly through a stmt_decl.
* Handle expr_ret and expr_fail properly (after execution of a ret
or fail, everything is true -- this is needed to handle ifs and alts
where one branch is a ret or fail)
* Fixed bug in set_prestate_ann where a thing that needed to be
mutated wasn't getting passed as an alias
* Fixed bug in how expr_alt was treated (zero is not the identity
for intersect, who knew, right?)
* Update logging to reflect log_err vs. log
* Fixed find_locals so as to return all local decls and exclude
function arguments.
* Make union_postconds work on an empty vector (needed to handle
empty blocks correctly)
* Added _vec.cat_options, which takes a list of option[T] to a list
of T, ignoring any Nones
* Added two test cases.
2011-04-20 14:11:01 -05:00
|
|
|
}
|
|
|
|
|
2011-06-17 21:07:23 -05:00
|
|
|
// Clears the given bit in p
|
2011-09-12 04:27:30 -05:00
|
|
|
fn relax_poststate(i: uint, p: poststate) -> bool {
|
2011-06-17 21:07:23 -05:00
|
|
|
ret relax_prestate(i, p);
|
|
|
|
}
|
|
|
|
|
|
|
|
// Clears the given bit in p
|
2011-09-12 04:27:30 -05:00
|
|
|
fn relax_precond(i: uint, p: precond) { relax_prestate(i, p); }
|
2011-06-15 13:19:50 -05:00
|
|
|
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
// Sets all the bits in p to "don't care"
|
2011-09-12 04:27:30 -05:00
|
|
|
fn clear(p: precond) { tritv_clear(p); }
|
2011-05-18 17:43:05 -05:00
|
|
|
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
// Sets all the bits in p to true
|
2011-09-12 04:27:30 -05:00
|
|
|
fn set(p: precond) { tritv_set_all(p); }
|
2011-05-18 17:43:05 -05:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn ann_precond(a: ts_ann) -> precond { ret a.conditions.precondition; }
|
2011-04-06 19:56:44 -05:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn ann_prestate(a: ts_ann) -> prestate { ret a.states.prestate; }
|
2011-04-06 19:56:44 -05:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn ann_poststate(a: ts_ann) -> poststate { ret a.states.poststate; }
|
2011-05-14 21:02:30 -05:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn pp_clone(p: pre_and_post) -> pre_and_post {
|
2011-07-27 07:19:39 -05:00
|
|
|
ret @{precondition: clone(p.precondition),
|
|
|
|
postcondition: clone(p.postcondition)};
|
Further work on typestate_check
Lots of work on typestate_check, seems to get a lot of the way
through checking the standard library.
* Added for, for_each, assign_op, bind, cast, put, check, break,
and cont. (I'm not sure break and cont are actually handled correctly.)
* Fixed side-effect bug in seq_preconds so that unioning the
preconditions of a sequence of statements or expressions
is handled correctly.
* Pass poststate correctly through a stmt_decl.
* Handle expr_ret and expr_fail properly (after execution of a ret
or fail, everything is true -- this is needed to handle ifs and alts
where one branch is a ret or fail)
* Fixed bug in set_prestate_ann where a thing that needed to be
mutated wasn't getting passed as an alias
* Fixed bug in how expr_alt was treated (zero is not the identity
for intersect, who knew, right?)
* Update logging to reflect log_err vs. log
* Fixed find_locals so as to return all local decls and exclude
function arguments.
* Make union_postconds work on an empty vector (needed to handle
empty blocks correctly)
* Added _vec.cat_options, which takes a list of option[T] to a list
of T, ignoring any Nones
* Added two test cases.
2011-04-20 14:11:01 -05:00
|
|
|
}
|
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
fn clone(p: prestate) -> prestate { ret tritv_clone(p); }
|
2011-06-15 13:19:50 -05:00
|
|
|
|
Handle nested items correctly in typestate_check
Summary says it all. Actually, only nested objects and functions
are handled, but that's better than before. The fold that I was using
before to traverse a crate wasn't working correctly, because annotations
have to reflect the number of local variables of the nearest enclosing
function (in turn, because annotations are represented as bit vectors).
The fold was traversing the AST in the wrong order, first filling in
the annotations correctly, but then re-traversing them with the bit
vector length for any outer nested functions, and so on.
Remedying this required writing a lot of tedious boilerplate code
because I scrapped the idea of using a fold altogether.
I also made typestate_check handle unary, field, alt, and fail.
Also, some miscellaneous changes:
* added annotations to blocks in typeck
* fix pprust so it can handle spawn
* added more logging functions in util.common
* fixed _vec.or
* added maybe and from_maybe in option
* removed fold_block field from ast_fold, since it was never used
2011-04-18 17:33:10 -05:00
|
|
|
|
2011-04-12 14:16:21 -05:00
|
|
|
// returns true if a implies b
|
|
|
|
// that is, returns true except if for some bits c and d,
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
// c = 1 and d = either 0 or "don't know"
|
|
|
|
// FIXME: is this correct?
|
2011-07-27 07:19:39 -05:00
|
|
|
fn implies(a: t, b: t) -> bool {
|
|
|
|
let tmp = tritv_clone(b);
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
tritv_difference(tmp, a);
|
|
|
|
ret tritv_doesntcare(tmp);
|
2011-04-04 16:31:49 -05:00
|
|
|
}
|
2011-06-25 00:17:17 -05:00
|
|
|
|
2011-09-02 17:34:58 -05:00
|
|
|
fn trit_str(t: trit) -> str {
|
|
|
|
alt t { dont_care. { "?" } ttrue. { "1" } tfalse. { "0" } }
|
2011-06-25 00:17:17 -05:00
|
|
|
}
|
Handle nested items correctly in typestate_check
Summary says it all. Actually, only nested objects and functions
are handled, but that's better than before. The fold that I was using
before to traverse a crate wasn't working correctly, because annotations
have to reflect the number of local variables of the nearest enclosing
function (in turn, because annotations are represented as bit vectors).
The fold was traversing the AST in the wrong order, first filling in
the annotations correctly, but then re-traversing them with the bit
vector length for any outer nested functions, and so on.
Remedying this required writing a lot of tedious boilerplate code
because I scrapped the idea of using a fold altogether.
I also made typestate_check handle unary, field, alt, and fail.
Also, some miscellaneous changes:
* added annotations to blocks in typeck
* fix pprust so it can handle spawn
* added more logging functions in util.common
* fixed _vec.or
* added maybe and from_maybe in option
* removed fold_block field from ast_fold, since it was never used
2011-04-18 17:33:10 -05:00
|
|
|
//
|
|
|
|
// Local Variables:
|
|
|
|
// mode: rust
|
|
|
|
// fill-column: 78;
|
|
|
|
// indent-tabs-mode: nil
|
|
|
|
// c-basic-offset: 4
|
|
|
|
// buffer-file-coding-system: utf-8-unix
|
|
|
|
// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
|
|
|
|
// End:
|
|
|
|
//
|