user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Continued sketching out code for checking states against preconditions.

Browse source 
It's still sketchy. I added a typestate annotation field to statements
tagged stmt_decl or stmt_expr, because a stmt_decl statement has a typestate
that's different from that of its child node. This necessitated trivial
changes to a bunch of other files all over to the compiler. I also added a
few small standard library functions, some of which I didn't actually end
up using but which I thought might be useful anyway.
This commit is contained in:
Tim Chevalier 2011-04-06 17:56:44 -07:00
parent 36d75d6391
commit 2e90bd94de
16 changed files with 362 additions and 151 deletions
Download patch file Download diff file Expand all files Collapse all files

53
src/comp/util/typestate_ann.rs
View file

@ -36,9 +36,17 @@ fn true_postcond(uint num_vars) -> postcond {
be true_precond(num_vars);
}
fn empty_prestate(uint num_vars) -> prestate {
be true_precond(num_vars);
}
fn empty_poststate(uint num_vars) -> poststate {
be true_precond(num_vars);
}
fn empty_pre_post(uint num_vars) -> pre_and_post {
ret(rec(precondition=true_precond(num_vars),
postcondition=true_postcond(num_vars)));
ret(rec(precondition=empty_prestate(num_vars),
postcondition=empty_poststate(num_vars)));
}
fn empty_states(uint num_vars) -> pre_and_post_state {
@ -46,6 +54,11 @@ fn empty_states(uint num_vars) -> pre_and_post_state {
poststate=true_postcond(num_vars)));
}
fn empty_ann(uint num_vars) -> ts_ann {
ret(rec(conditions=empty_pre_post(num_vars),
states=empty_states(num_vars)));
}
fn get_pre(&pre_and_post p) -> precond {
ret p.precondition;
}
@ -74,7 +87,37 @@ impure fn require_and_preserve(uint i, &pre_and_post p) -> () {
bitv.set(p.postcondition, i, true);
}
fn implies(bitv.t a, bitv.t b) -> bool {
bitv.difference(b, a);
ret (bitv.equal(b, bitv.create(b.nbits, false)));
impure fn set_in_postcond(uint i, &pre_and_post p) -> () {
// sets the ith bit in p's post
bitv.set(p.postcondition, i, true);
}
// Sets all the bits in a's precondition to equal the
// corresponding bit in p's precondition.
impure fn set_precondition(&ts_ann a, &precond p) -> () {
bitv.copy(p, a.conditions.precondition);
}
// Sets all the bits in a's postcondition to equal the
// corresponding bit in p's postcondition.
impure fn set_postcondition(&ts_ann a, &postcond p) -> () {
bitv.copy(p, a.conditions.postcondition);
}
// Set all the bits in p that are set in new
impure fn extend_prestate(&prestate p, &poststate new) -> () {
bitv.union(p, new);
}
fn ann_precond(&ts_ann a) -> precond {
ret a.conditions.precondition;
}
fn ann_prestate(&ts_ann a) -> prestate {
ret a.states.prestate;
}
impure fn implies(bitv.t a, bitv.t b) -> bool {
bitv.difference(b, a);
be bitv.is_false(b);
}