提交 082d8314 编写于 作者: T Tim Chevalier

Rewrite bitv to use classes and optimize its representation

Rewrote bitv as a class that uses a 32-bit int as its representation
for bit vectors of 32 bits or less, and a vector (the old representation)
otherwise. I didn't benchmark very much, but a bit of informal benchmarking
suggested this is a win.

Closes #2341
上级 6ac86e92
此差异已折叠。
...@@ -29,7 +29,7 @@ ...@@ -29,7 +29,7 @@
import dvec::extensions; import dvec::extensions;
import std::bitv::{bitv, methods}; import std::bitv::{bitv};
import proto::methods; import proto::methods;
import ast_builder::empty_span; import ast_builder::empty_span;
...@@ -38,7 +38,7 @@ fn analyze(proto: protocol, _cx: ext_ctxt) { ...@@ -38,7 +38,7 @@ fn analyze(proto: protocol, _cx: ext_ctxt) {
#debug("initializing colive analysis"); #debug("initializing colive analysis");
let num_states = proto.num_states(); let num_states = proto.num_states();
let colive = do (copy proto.states).map_to_vec |state| { let colive = do (copy proto.states).map_to_vec |state| {
let bv = bitv(num_states, false); let bv = ~bitv(num_states, false);
for state.reachable |s| { for state.reachable |s| {
bv.set(s.id, true); bv.set(s.id, true);
} }
......
...@@ -53,8 +53,8 @@ fn empty_poststate(num_vars: uint) -> poststate { ...@@ -53,8 +53,8 @@ fn empty_poststate(num_vars: uint) -> poststate {
fn false_postcond(num_vars: uint) -> postcond { fn false_postcond(num_vars: uint) -> postcond {
let rslt = create_tritv(num_vars); let rslt = create_tritv(num_vars);
tritv_set_all(rslt); rslt.set_all();
ret rslt; rslt
} }
fn empty_pre_post(num_vars: uint) -> pre_and_post { fn empty_pre_post(num_vars: uint) -> pre_and_post {
...@@ -76,15 +76,11 @@ fn empty_ann(num_vars: uint) -> ts_ann { ...@@ -76,15 +76,11 @@ fn empty_ann(num_vars: uint) -> ts_ann {
fn get_post(&&p: pre_and_post) -> postcond { ret p.postcondition; } fn get_post(&&p: pre_and_post) -> postcond { ret p.postcondition; }
fn difference(p1: precond, p2: precond) -> bool { fn difference(p1: precond, p2: precond) -> bool { p1.difference(p2) }
ret tritv_difference(p1, p2);
}
fn union(p1: precond, p2: precond) -> bool { ret tritv_union(p1, p2); } fn union(p1: precond, p2: precond) -> bool { p1.union(p2) }
fn intersect(p1: precond, p2: precond) -> bool { fn intersect(p1: precond, p2: precond) -> bool { p1.intersect(p2) }
ret tritv_intersect(p1, p2);
}
fn pps_len(p: pre_and_post) -> uint { fn pps_len(p: pre_and_post) -> uint {
// gratuitous check // gratuitous check
...@@ -95,13 +91,13 @@ fn pps_len(p: pre_and_post) -> uint { ...@@ -95,13 +91,13 @@ fn pps_len(p: pre_and_post) -> uint {
fn require(i: uint, p: pre_and_post) { fn require(i: uint, p: pre_and_post) {
// sets the ith bit in p's pre // sets the ith bit in p's pre
tritv_set(i, p.precondition, ttrue); p.precondition.set(i, ttrue);
} }
fn require_and_preserve(i: uint, p: pre_and_post) { fn require_and_preserve(i: uint, p: pre_and_post) {
// sets the ith bit in p's pre and post // sets the ith bit in p's pre and post
tritv_set(i, p.precondition, ttrue); p.precondition.set(i, ttrue);
tritv_set(i, p.postcondition, ttrue); p.postcondition.set(i, ttrue);
} }
fn set_in_postcond(i: uint, p: pre_and_post) -> bool { fn set_in_postcond(i: uint, p: pre_and_post) -> bool {
...@@ -110,8 +106,8 @@ fn set_in_postcond(i: uint, p: pre_and_post) -> bool { ...@@ -110,8 +106,8 @@ fn set_in_postcond(i: uint, p: pre_and_post) -> bool {
} }
fn set_in_postcond_(i: uint, p: postcond) -> bool { fn set_in_postcond_(i: uint, p: postcond) -> bool {
let was_set = tritv_get(p, i); let was_set = p.get(i);
tritv_set(i, p, ttrue); p.set(i, ttrue);
ret was_set != ttrue; ret was_set != ttrue;
} }
...@@ -121,8 +117,8 @@ fn set_in_poststate(i: uint, s: pre_and_post_state) -> bool { ...@@ -121,8 +117,8 @@ fn set_in_poststate(i: uint, s: pre_and_post_state) -> bool {
} }
fn set_in_poststate_(i: uint, p: poststate) -> bool { fn set_in_poststate_(i: uint, p: poststate) -> bool {
let was_set = tritv_get(p, i); let was_set = p.get(i);
tritv_set(i, p, ttrue); p.set(i, ttrue);
ret was_set != ttrue; ret was_set != ttrue;
} }
...@@ -133,8 +129,8 @@ fn clear_in_poststate(i: uint, s: pre_and_post_state) -> bool { ...@@ -133,8 +129,8 @@ fn clear_in_poststate(i: uint, s: pre_and_post_state) -> bool {
} }
fn clear_in_poststate_(i: uint, s: poststate) -> bool { fn clear_in_poststate_(i: uint, s: poststate) -> bool {
let was_set = tritv_get(s, i); let was_set = s.get(i);
tritv_set(i, s, tfalse); s.set(i, tfalse);
ret was_set != tfalse; ret was_set != tfalse;
} }
...@@ -144,61 +140,61 @@ fn clear_in_prestate(i: uint, s: pre_and_post_state) -> bool { ...@@ -144,61 +140,61 @@ fn clear_in_prestate(i: uint, s: pre_and_post_state) -> bool {
} }
fn clear_in_prestate_(i: uint, s: prestate) -> bool { fn clear_in_prestate_(i: uint, s: prestate) -> bool {
let was_set = tritv_get(s, i); let was_set = s.get(i);
tritv_set(i, s, tfalse); s.set(i, tfalse);
ret was_set != tfalse; ret was_set != tfalse;
} }
fn clear_in_postcond(i: uint, s: pre_and_post) -> bool { fn clear_in_postcond(i: uint, s: pre_and_post) -> bool {
// sets the ith bit in p's post // sets the ith bit in p's post
let was_set = tritv_get(s.postcondition, i); let was_set = s.postcondition.get(i);
tritv_set(i, s.postcondition, tfalse); s.postcondition.set(i, tfalse);
ret was_set != tfalse; ret was_set != tfalse;
} }
// Sets all the bits in a's precondition to equal the // Sets all the bits in a's precondition to equal the
// corresponding bit in p's precondition. // corresponding bit in p's precondition.
fn set_precondition(a: ts_ann, p: precond) { fn set_precondition(a: ts_ann, p: precond) {
tritv_copy(a.conditions.precondition, p); a.conditions.precondition.become(p);
} }
// Sets all the bits in a's postcondition to equal the // Sets all the bits in a's postcondition to equal the
// corresponding bit in p's postcondition. // corresponding bit in p's postcondition.
fn set_postcondition(a: ts_ann, p: postcond) { fn set_postcondition(a: ts_ann, p: postcond) {
tritv_copy(a.conditions.postcondition, p); a.conditions.postcondition.become(p);
} }
// Sets all the bits in a's prestate to equal the // Sets all the bits in a's prestate to equal the
// corresponding bit in p's prestate. // corresponding bit in p's prestate.
fn set_prestate(a: ts_ann, p: prestate) -> bool { fn set_prestate(a: ts_ann, p: prestate) -> bool {
ret tritv_copy(a.states.prestate, p); a.states.prestate.become(p)
} }
// Sets all the bits in a's postcondition to equal the // Sets all the bits in a's postcondition to equal the
// corresponding bit in p's postcondition. // corresponding bit in p's postcondition.
fn set_poststate(a: ts_ann, p: poststate) -> bool { fn set_poststate(a: ts_ann, p: poststate) -> bool {
ret tritv_copy(a.states.poststate, p); a.states.poststate.become(p)
} }
// Set all the bits in p that are set in new // Set all the bits in p that are set in new
fn extend_prestate(p: prestate, newv: poststate) -> bool { fn extend_prestate(p: prestate, newv: poststate) -> bool {
ret tritv_union(p, newv); p.union(newv)
} }
// Set all the bits in p that are set in new // Set all the bits in p that are set in new
fn extend_poststate(p: poststate, newv: poststate) -> bool { fn extend_poststate(p: poststate, newv: poststate) -> bool {
ret tritv_union(p, newv); p.union(newv)
} }
// Sets the given bit in p to "don't care" // Sets the given bit in p to "don't care"
fn relax_prestate(i: uint, p: prestate) -> bool { fn relax_prestate(i: uint, p: prestate) -> bool {
let was_set = tritv_get(p, i); let was_set = p.get(i);
tritv_set(i, p, dont_care); p.set(i, dont_care);
ret was_set != dont_care; ret was_set != dont_care;
} }
...@@ -211,10 +207,10 @@ fn relax_poststate(i: uint, p: poststate) -> bool { ...@@ -211,10 +207,10 @@ fn relax_poststate(i: uint, p: poststate) -> bool {
fn relax_precond(i: uint, p: precond) { relax_prestate(i, p); } fn relax_precond(i: uint, p: precond) { relax_prestate(i, p); }
// Sets all the bits in p to "don't care" // Sets all the bits in p to "don't care"
fn clear(p: precond) { tritv_clear(p); } fn clear(p: precond) { p.clear(); }
// Sets all the bits in p to true // Sets all the bits in p to true
fn set(p: precond) { tritv_set_all(p); } fn set(p: precond) { p.set_all(); }
fn ann_precond(a: ts_ann) -> precond { ret a.conditions.precondition; } fn ann_precond(a: ts_ann) -> precond { ret a.conditions.precondition; }
...@@ -227,16 +223,16 @@ fn pp_clone(p: pre_and_post) -> pre_and_post { ...@@ -227,16 +223,16 @@ fn pp_clone(p: pre_and_post) -> pre_and_post {
postcondition: clone(p.postcondition)}; postcondition: clone(p.postcondition)};
} }
fn clone(p: prestate) -> prestate { ret tritv_clone(p); } fn clone(p: prestate) -> prestate { p.clone() }
// returns true if a implies b // returns true if a implies b
// that is, returns true except if for some bits c and d, // that is, returns true except if for some bits c and d,
// c = 1 and d = either 0 or "don't know" // c = 1 and d = either 0 or "don't know"
fn implies(a: t, b: t) -> bool { fn implies(a: t, b: t) -> bool {
let tmp = tritv_clone(b); let tmp = b.clone();
tritv_difference(tmp, a); tmp.difference(a);
ret tritv_doesntcare(tmp); tmp.doesntcare()
} }
fn trit_str(t: trit) -> ~str { fn trit_str(t: trit) -> ~str {
......
...@@ -15,7 +15,7 @@ ...@@ -15,7 +15,7 @@
clear_in_poststate_}; clear_in_poststate_};
import driver::session::session; import driver::session::session;
import dvec::{dvec, extensions}; import dvec::{dvec, extensions};
import tritv::{dont_care, tfalse, tritv_get, ttrue}; import tritv::{trit, tfalse, ttrue, dont_care, t};
import syntax::print::pprust::{constr_args_to_str, lit_to_str}; import syntax::print::pprust::{constr_args_to_str, lit_to_str};
...@@ -59,7 +59,7 @@ fn tritv_to_str(fcx: fn_ctxt, v: tritv::t) -> ~str { ...@@ -59,7 +59,7 @@ fn tritv_to_str(fcx: fn_ctxt, v: tritv::t) -> ~str {
let mut s = ~""; let mut s = ~"";
let mut comma = false; let mut comma = false;
for constraints(fcx).each |p| { for constraints(fcx).each |p| {
alt tritv_get(v, p.bit_num) { alt v.get(p.bit_num) {
dont_care { } dont_care { }
tt { tt {
s += s +=
...@@ -80,8 +80,8 @@ fn first_difference_string(fcx: fn_ctxt, expected: tritv::t, actual: tritv::t) ...@@ -80,8 +80,8 @@ fn first_difference_string(fcx: fn_ctxt, expected: tritv::t, actual: tritv::t)
-> ~str { -> ~str {
let mut s = ~""; let mut s = ~"";
for constraints(fcx).each |c| { for constraints(fcx).each |c| {
if tritv_get(expected, c.bit_num) == ttrue && if expected.get(c.bit_num) == ttrue &&
tritv_get(actual, c.bit_num) != ttrue { actual.get(c.bit_num) != ttrue {
s = constraint_to_str(fcx.ccx.tcx, c.c); s = constraint_to_str(fcx.ccx.tcx, c.c);
break; break;
} }
...@@ -108,8 +108,8 @@ fn tos(v: ~[uint]) -> ~str { ...@@ -108,8 +108,8 @@ fn tos(v: ~[uint]) -> ~str {
fn log_cond_err(v: ~[uint]) { log(error, tos(v)); } fn log_cond_err(v: ~[uint]) { log(error, tos(v)); }
fn log_pp(pp: pre_and_post) { fn log_pp(pp: pre_and_post) {
let p1 = tritv::to_vec(pp.precondition); let p1 = pp.precondition.to_vec();
let p2 = tritv::to_vec(pp.postcondition); let p2 = pp.postcondition.to_vec();
#debug("pre:"); #debug("pre:");
log_cond(p1); log_cond(p1);
#debug("post:"); #debug("post:");
...@@ -117,8 +117,8 @@ fn log_pp(pp: pre_and_post) { ...@@ -117,8 +117,8 @@ fn log_pp(pp: pre_and_post) {
} }
fn log_pp_err(pp: pre_and_post) { fn log_pp_err(pp: pre_and_post) {
let p1 = tritv::to_vec(pp.precondition); let p1 = pp.precondition.to_vec();
let p2 = tritv::to_vec(pp.postcondition); let p2 = pp.postcondition.to_vec();
#error("pre:"); #error("pre:");
log_cond_err(p1); log_cond_err(p1);
#error("post:"); #error("post:");
...@@ -126,8 +126,8 @@ fn log_pp_err(pp: pre_and_post) { ...@@ -126,8 +126,8 @@ fn log_pp_err(pp: pre_and_post) {
} }
fn log_states(pp: pre_and_post_state) { fn log_states(pp: pre_and_post_state) {
let p1 = tritv::to_vec(pp.prestate); let p1 = pp.prestate.to_vec();
let p2 = tritv::to_vec(pp.poststate); let p2 = pp.poststate.to_vec();
#debug("prestate:"); #debug("prestate:");
log_cond(p1); log_cond(p1);
#debug("poststate:"); #debug("poststate:");
...@@ -135,8 +135,8 @@ fn log_states(pp: pre_and_post_state) { ...@@ -135,8 +135,8 @@ fn log_states(pp: pre_and_post_state) {
} }
fn log_states_err(pp: pre_and_post_state) { fn log_states_err(pp: pre_and_post_state) {
let p1 = tritv::to_vec(pp.prestate); let p1 = pp.prestate.to_vec();
let p2 = tritv::to_vec(pp.poststate); let p2 = pp.poststate.to_vec();
#error("prestate:"); #error("prestate:");
log_cond_err(p1); log_cond_err(p1);
#error("poststate:"); #error("poststate:");
......
...@@ -184,7 +184,7 @@ fn handle_update(fcx: fn_ctxt, parent: @expr, lhs: @expr, rhs: @expr, ...@@ -184,7 +184,7 @@ fn handle_update(fcx: fn_ctxt, parent: @expr, lhs: @expr, rhs: @expr,
alt lhs.node { alt lhs.node {
expr_path(p) { expr_path(p) {
let post = expr_postcond(fcx.ccx, parent); let post = expr_postcond(fcx.ccx, parent);
let tmp = tritv_clone(post); let tmp = post.clone();
alt ty { alt ty {
oper_move { oper_move {
...@@ -497,7 +497,7 @@ fn find_pre_post_stmt(fcx: fn_ctxt, s: stmt) { ...@@ -497,7 +497,7 @@ fn find_pre_post_stmt(fcx: fn_ctxt, s: stmt) {
/* Clear out anything that the previous initializer /* Clear out anything that the previous initializer
guaranteed */ guaranteed */
let e_pp = expr_pp(fcx.ccx, an_init.expr); let e_pp = expr_pp(fcx.ccx, an_init.expr);
tritv_copy(prev_pp.precondition, prev_pp.precondition.become(
seq_preconds(fcx, ~[prev_pp, e_pp])); seq_preconds(fcx, ~[prev_pp, e_pp]));
/* Include the LHSs too, since those aren't in the /* Include the LHSs too, since those aren't in the
......
import ann::*; import ann::*;
import aux::*; import aux::*;
import tritv::{tritv_clone, tritv_set, ttrue}; import tritv::*;
import syntax::print::pprust::block_to_str; import syntax::print::pprust::block_to_str;
import bitvectors::*; import bitvectors::*;
...@@ -57,14 +57,14 @@ fn handle_move_or_copy(fcx: fn_ctxt, post: poststate, rhs_path: @path, ...@@ -57,14 +57,14 @@ fn handle_move_or_copy(fcx: fn_ctxt, post: poststate, rhs_path: @path,
fn seq_states(fcx: fn_ctxt, pres: prestate, bindings: ~[binding]) -> fn seq_states(fcx: fn_ctxt, pres: prestate, bindings: ~[binding]) ->
{changed: bool, post: poststate} { {changed: bool, post: poststate} {
let mut changed = false; let mut changed = false;
let mut post = tritv_clone(pres); let mut post = pres.clone();
for bindings.each |b| { for bindings.each |b| {
alt b.rhs { alt b.rhs {
some(an_init) { some(an_init) {
// an expression, with or without a destination // an expression, with or without a destination
changed |= changed |=
find_pre_post_state_expr(fcx, post, an_init.expr) || changed; find_pre_post_state_expr(fcx, post, an_init.expr) || changed;
post = tritv_clone(expr_poststate(fcx.ccx, an_init.expr)); post = expr_poststate(fcx.ccx, an_init.expr).clone();
for b.lhs.each |d| { for b.lhs.each |d| {
alt an_init.expr.node { alt an_init.expr.node {
expr_path(p) { expr_path(p) {
...@@ -93,7 +93,7 @@ fn find_pre_post_state_sub(fcx: fn_ctxt, pres: prestate, e: @expr, ...@@ -93,7 +93,7 @@ fn find_pre_post_state_sub(fcx: fn_ctxt, pres: prestate, e: @expr,
changed = set_prestate_ann(fcx.ccx, parent, pres) || changed; changed = set_prestate_ann(fcx.ccx, parent, pres) || changed;
let post = tritv_clone(expr_poststate(fcx.ccx, e)); let post = expr_poststate(fcx.ccx, e).clone();
alt c { alt c {
none { } none { }
some(c1) { set_in_poststate_(bit_num(fcx, c1), post); } some(c1) { set_in_poststate_(bit_num(fcx, c1), post); }
...@@ -113,7 +113,7 @@ fn find_pre_post_state_two(fcx: fn_ctxt, pres: prestate, lhs: @expr, ...@@ -113,7 +113,7 @@ fn find_pre_post_state_two(fcx: fn_ctxt, pres: prestate, lhs: @expr,
changed; changed;
forbid_upvar(fcx, rhs.id, rhs.span, ty); forbid_upvar(fcx, rhs.id, rhs.span, ty);
let post = tritv_clone(expr_poststate(fcx.ccx, rhs)); let post = expr_poststate(fcx.ccx, rhs).clone();
alt lhs.node { alt lhs.node {
expr_path(p) { expr_path(p) {
...@@ -121,7 +121,7 @@ fn find_pre_post_state_two(fcx: fn_ctxt, pres: prestate, lhs: @expr, ...@@ -121,7 +121,7 @@ fn find_pre_post_state_two(fcx: fn_ctxt, pres: prestate, lhs: @expr,
// changed flag // changed flag
// tmp remembers "old" constraints we'd otherwise forget, // tmp remembers "old" constraints we'd otherwise forget,
// for substitution purposes // for substitution purposes
let tmp = tritv_clone(post); let tmp = post.clone();
alt ty { alt ty {
oper_move { oper_move {
...@@ -210,8 +210,8 @@ fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk, ...@@ -210,8 +210,8 @@ fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk,
alt chk { alt chk {
if_check { if_check {
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec); let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
let conseq_prestate = tritv_clone(expr_poststate(fcx.ccx, antec)); let conseq_prestate = expr_poststate(fcx.ccx, antec).clone();
tritv_set(bit_num(fcx, c.node), conseq_prestate, ttrue); conseq_prestate.set(bit_num(fcx, c.node), ttrue);
changed |= changed |=
find_pre_post_state_block(fcx, conseq_prestate, conseq) | find_pre_post_state_block(fcx, conseq_prestate, conseq) |
set_poststate_ann(fcx.ccx, id, set_poststate_ann(fcx.ccx, id,
...@@ -235,8 +235,8 @@ fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk, ...@@ -235,8 +235,8 @@ fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk,
alt chk { alt chk {
if_check { if_check {
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec); let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
conseq_prestate = tritv_clone(conseq_prestate); conseq_prestate = conseq_prestate.clone();
tritv_set(bit_num(fcx, c.node), conseq_prestate, ttrue); conseq_prestate.set(bit_num(fcx, c.node), ttrue);
} }
_ { } _ { }
} }
...@@ -270,7 +270,7 @@ fn find_pre_post_state_cap_clause(fcx: fn_ctxt, e_id: node_id, ...@@ -270,7 +270,7 @@ fn find_pre_post_state_cap_clause(fcx: fn_ctxt, e_id: node_id,
{ {
let ccx = fcx.ccx; let ccx = fcx.ccx;
let pres_changed = set_prestate_ann(ccx, e_id, pres); let pres_changed = set_prestate_ann(ccx, e_id, pres);
let post = tritv_clone(pres); let post = pres.clone();
for (*cap_clause).each |cap_item| { for (*cap_clause).each |cap_item| {
if cap_item.is_move { if cap_item.is_move {
forget_in_poststate(fcx, post, cap_item.id); forget_in_poststate(fcx, post, cap_item.id);
...@@ -432,7 +432,7 @@ fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool { ...@@ -432,7 +432,7 @@ fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool {
worst case, the body could invalidate all preds and worst case, the body could invalidate all preds and
deinitialize everything before breaking */ deinitialize everything before breaking */
let post = empty_poststate(num_constrs); let post = empty_poststate(num_constrs);
tritv::tritv_kill(post); post.kill();
ret changed | set_poststate_ann(fcx.ccx, e.id, post); ret changed | set_poststate_ann(fcx.ccx, e.id, post);
} else { } else {
ret changed | set_poststate_ann(fcx.ccx, e.id, ret changed | set_poststate_ann(fcx.ccx, e.id,
...@@ -507,8 +507,8 @@ fn find_pre_post_state_stmt(fcx: fn_ctxt, pres: prestate, s: @stmt) -> bool { ...@@ -507,8 +507,8 @@ fn find_pre_post_state_stmt(fcx: fn_ctxt, pres: prestate, s: @stmt) -> bool {
#debug["[ %s ]", *fcx.name]; #debug["[ %s ]", *fcx.name];
#debug["*At beginning: stmt = %s", stmt_to_str(*s)]; #debug["*At beginning: stmt = %s", stmt_to_str(*s)];
#debug["*prestate = %s", tritv::to_str(stmt_ann.states.prestate)]; #debug["*prestate = %s", stmt_ann.states.prestate.to_str()];
#debug["*poststate = %s", tritv::to_str(stmt_ann.states.prestate)]; #debug["*poststate = %s", stmt_ann.states.prestate.to_str()];
alt s.node { alt s.node {
stmt_decl(adecl, id) { stmt_decl(adecl, id) {
...@@ -525,8 +525,8 @@ fn find_pre_post_state_stmt(fcx: fn_ctxt, pres: prestate, s: @stmt) -> bool { ...@@ -525,8 +525,8 @@ fn find_pre_post_state_stmt(fcx: fn_ctxt, pres: prestate, s: @stmt) -> bool {
set_poststate(stmt_ann, c_and_p.post) | c_and_p.changed; set_poststate(stmt_ann, c_and_p.post) | c_and_p.changed;
#debug["Summary: stmt = %s", stmt_to_str(*s)]; #debug["Summary: stmt = %s", stmt_to_str(*s)];
#debug["prestate = %s", tritv::to_str(stmt_ann.states.prestate)]; #debug["prestate = %s", stmt_ann.states.prestate.to_str()];
#debug["poststate = %s",tritv::to_str(stmt_ann.states.poststate)]; #debug["poststate = %s", stmt_ann.states.poststate.to_str()];
#debug["changed = %s", bool::to_str(changed)]; #debug["changed = %s", bool::to_str(changed)];
ret changed; ret changed;
...@@ -545,8 +545,8 @@ fn find_pre_post_state_stmt(fcx: fn_ctxt, pres: prestate, s: @stmt) -> bool { ...@@ -545,8 +545,8 @@ fn find_pre_post_state_stmt(fcx: fn_ctxt, pres: prestate, s: @stmt) -> bool {
#debug["Finally: %s", stmt_to_str(*s)]; #debug["Finally: %s", stmt_to_str(*s)];
#debug["prestate = %s", tritv::to_str(stmt_ann.states.prestate)]; #debug["prestate = %s", stmt_ann.states.prestate.to_str()];
#debug["poststate = %s", tritv::to_str(stmt_ann.states.poststate)]; #debug["poststate = %s", stmt_ann.states.poststate.to_str()];
#debug["changed = %s", bool::to_str(changed)]; #debug["changed = %s", bool::to_str(changed)];
ret changed; ret changed;
......
import std::bitv; import std::bitv::*;
export t; export t;
export create_tritv; export create_tritv;
export tritv_clone; export trit, tfalse, ttrue, dont_care;
export tritv_set;
export to_vec;
export trit;
export dont_care;
export ttrue;
export tfalse;
export tritv_get;
export tritv_set_all;
export tritv_difference;
export tritv_union;
export tritv_intersect;
export tritv_copy;
export tritv_clear;
export tritv_kill;
export tritv_doesntcare;
export to_str;
/* for a fixed index: /* for a fixed index:
10 = "this constraint may or may not be true after execution" 10 = "this constraint may or may not be true after execution"
...@@ -31,17 +15,160 @@ ...@@ -31,17 +15,160 @@
per discussion at). per discussion at).
*/ */
type t = {uncertain: bitv::bitv, val: bitv::bitv, nbits: uint};
enum trit { ttrue, tfalse, dont_care, } enum trit { ttrue, tfalse, dont_care, }
fn create_tritv(len: uint) -> t { class t {
ret {uncertain: bitv::bitv(len, true), // Shouldn't be mut; instead we should have a different
val: bitv::bitv(len, false), // constructor that takes two bitvs
nbits: len}; let mut uncertain: bitv;
let mut val: bitv;
let nbits: uint;
// next two should be private (#2297)
fn set_uncertain(-b: bitv) {
self.uncertain <- b;
}
fn set_val(-b: bitv) {
self.val <- b;
}
fn clone() -> t {
let rs = t(self.nbits);
let r = self.uncertain.clone();
rs.set_uncertain(r);
let r1 = self.val.clone();
rs.set_val(r1);
rs
}
fn difference(p: t) -> bool {
assert (self.nbits == p.nbits);
let mut changed = false;
for uint::range(0, p.nbits) |i| {
let old = p.get(i);
let newv = minus(old, p.get(i));
changed = change(changed, old, newv);
self.set(i, newv);
};
changed
}
pure fn get(i: uint) -> trit {
let b1 = self.uncertain.get(i);
let b2 = self.val.get(i);
assert (!(b1 && b2));
if b1 { dont_care } else if b2 { ttrue } else { tfalse }
}
pure fn set(i: uint, t: trit) -> bool {
let old = self.get(i);
alt t {
dont_care {
self.uncertain.set(i, true);
self.val.set(i, false);
}
ttrue {
self.uncertain.set(i, false);
self.val.set(i, true);
}
tfalse {
self.uncertain.set(i, false);
self.val.set(i, false);
}
}
change(false, old, t)
}
fn set_all() {
for uint::range(0u, self.nbits) |i| {
self.set(i, ttrue);
}
}
fn clear() {
for uint::range(0, self.nbits) |i| {
self.set(i, dont_care);
}
}
fn kill() {
for uint::range(0, self.nbits) |i| {
self.set(i, dont_care);
}
}
fn doesntcare() -> bool {
for uint::range(0, self.nbits) |i| {
if self.get(i) != dont_care { ret false; }
}
true
}
fn to_vec() -> ~[uint] {
let mut rslt: ~[uint] = ~[];
for uint::range(0, self.nbits) |i| {
vec::push(rslt,
alt self.get(i) {
dont_care { 2 }
ttrue { 1 }
tfalse { 0 }
});
};
rslt
}
fn to_str() -> str {
let mut rs: str = "";
for uint::range(0, self.nbits) |i| {
rs +=
alt self.get(i) {
dont_care { "?" }
ttrue { "1" }
tfalse { "0" }
};
};
rs
}
fn intersect(p: t) -> bool {
assert (self.nbits == p.nbits);
let mut changed = false;
for uint::range(0, self.nbits) |i| {
let old = self.get(i);
let newv = trit_and(old, p.get(i));
changed = change(changed, old, newv);
self.set(i, newv);
}
ret changed;
}
fn become(source: t) -> bool {
assert (self.nbits == source.nbits);
let changed = !self.uncertain.equal(source.uncertain) ||
!self.val.equal(source.val);
self.uncertain.assign(source.uncertain);
self.val.assign(source.val);
changed
}
fn union(p: t) -> bool {
assert (self.nbits == p.nbits);
let mut changed = false;
for uint::range(0, self.nbits) |i| {
let old = self.get(i);
let newv = trit_or(old, p.get(i));
changed = change(changed, old, newv);
self.set(i, newv);
}
ret changed;
}
new(len: uint) {
self.uncertain = mk_bitv(len, true);
self.val = mk_bitv(len, false);
self.nbits = len;
}
} }
fn create_tritv(len: uint) -> t { t(len) }
fn trit_minus(a: trit, b: trit) -> trit {
fn minus(a: trit, b: trit) -> trit {
/* 2 - anything = 2 /* 2 - anything = 2
1 - 1 = 2 1 - 1 = 2
...@@ -56,10 +183,6 @@ fn trit_minus(a: trit, b: trit) -> trit { ...@@ -56,10 +183,6 @@ fn trit_minus(a: trit, b: trit) -> trit {
alt b { alt b {
ttrue { dont_care } ttrue { dont_care }
tfalse { ttrue } tfalse { ttrue }
/* internally contradictory, but /* internally contradictory, but
I guess it'll get flagged? */ I guess it'll get flagged? */
dont_care { dont_care {
...@@ -70,18 +193,14 @@ fn trit_minus(a: trit, b: trit) -> trit { ...@@ -70,18 +193,14 @@ fn trit_minus(a: trit, b: trit) -> trit {
tfalse { tfalse {
alt b { alt b {
ttrue { tfalse } ttrue { tfalse }
/* see above comment */ /* see above comment */
_ { _ {
tfalse tfalse
} }
} }
} }
}
} }
}
fn trit_or(a: trit, b: trit) -> trit { fn trit_or(a: trit, b: trit) -> trit {
alt a { alt a {
...@@ -137,148 +256,9 @@ fn trit_and(a: trit, b: trit) -> trit { ...@@ -137,148 +256,9 @@ fn trit_and(a: trit, b: trit) -> trit {
// a and b were both dont_care // a and b were both dont_care
} }
fn change(changed: bool, old: trit, newv: trit) -> bool { pure fn change(changed: bool, old: trit, newv: trit) -> bool {
changed || newv != old changed || newv != old
} }
fn tritv_difference(p1: t, p2: t) -> bool {
let mut i: uint = 0u;
assert (p1.nbits == p2.nbits);
let sz: uint = p1.nbits;
let mut changed = false;
while i < sz {
let old = tritv_get(p1, i);
let newv = trit_minus(old, tritv_get(p2, i));
changed = change(changed, old, newv);
tritv_set(i, p1, newv);
i += 1u;
}
ret changed;
}
fn tritv_union(p1: t, p2: t) -> bool {
let mut i: uint = 0u;
assert (p1.nbits == p2.nbits);
let sz: uint = p1.nbits;
let mut changed = false;
while i < sz {
let old = tritv_get(p1, i);
let newv = trit_or(old, tritv_get(p2, i));
changed = change(changed, old, newv);
tritv_set(i, p1, newv);
i += 1u;
}
ret changed;
}
fn tritv_intersect(p1: t, p2: t) -> bool {
let mut i: uint = 0u;
assert (p1.nbits == p2.nbits);
let sz: uint = p1.nbits;
let mut changed = false;
while i < sz {
let old = tritv_get(p1, i);
let newv = trit_and(old, tritv_get(p2, i));
changed = change(changed, old, newv);
tritv_set(i, p1, newv);
i += 1u;
}
ret changed;
}
fn tritv_get(v: t, i: uint) -> trit {
let b1 = bitv::get(v.uncertain, i);
let b2 = bitv::get(v.val, i);
assert (!(b1 && b2));
if b1 { dont_care } else if b2 { ttrue } else { tfalse }
}
fn tritv_set(i: uint, v: t, t: trit) -> bool {
let old = tritv_get(v, i);
alt t {
dont_care {
bitv::set(v.uncertain, i, true);
bitv::set(v.val, i, false);
}
ttrue { bitv::set(v.uncertain, i, false); bitv::set(v.val, i, true); }
tfalse {
bitv::set(v.uncertain, i, false);
bitv::set(v.val, i, false);
}
}
ret change(false, old, t);
}
fn tritv_copy(target: t, source: t) -> bool {
assert (target.nbits == source.nbits);
let changed =
!bitv::equal(target.uncertain, source.uncertain) ||
!bitv::equal(target.val, source.val);
bitv::assign(target.uncertain, source.uncertain);
bitv::assign(target.val, source.val);
ret changed;
}
fn tritv_set_all(v: t) {
let mut i: uint = 0u;
while i < v.nbits { tritv_set(i, v, ttrue); i += 1u; }
}
fn tritv_clear(v: t) {
let mut i: uint = 0u;
while i < v.nbits { tritv_set(i, v, dont_care); i += 1u; }
}
fn tritv_kill(v: t) {
let mut i: uint = 0u;
while i < v.nbits { tritv_set(i, v, tfalse); i += 1u; }
}
fn tritv_clone(v: t) -> t {
ret {uncertain: bitv::clone(v.uncertain),
val: bitv::clone(v.val),
nbits: v.nbits};
}
fn tritv_doesntcare(v: t) -> bool {
let mut i: uint = 0u;
while i < v.nbits {
if tritv_get(v, i) != dont_care { ret false; }
i += 1u;
}
ret true;
}
fn to_vec(v: t) -> ~[uint] {
let mut i: uint = 0u;
let mut rslt: ~[uint] = ~[];
while i < v.nbits {
vec::push(rslt,
alt tritv_get(v, i) {
dont_care { 2u }
ttrue { 1u }
tfalse { 0u }
});
i += 1u;
}
ret rslt;
}
fn to_str(v: t) -> ~str {
let mut i: uint = 0u;
let mut rs: ~str = ~"";
while i < v.nbits {
rs +=
alt tritv_get(v, i) {
dont_care { ~"?" }
ttrue { ~"1" }
tfalse { ~"0" }
};
i += 1u;
}
ret rs;
}
// //
// Local Variables: // Local Variables:
// mode: rust // mode: rust
......
...@@ -52,7 +52,7 @@ fn next_color(g: grid, row: u8, col: u8, start_color: u8) -> bool { ...@@ -52,7 +52,7 @@ fn next_color(g: grid, row: u8, col: u8, start_color: u8) -> bool {
// colors not yet used // colors not yet used
let avail = bitv::bitv(10u, false); let avail = bitv::bitv(10u, false);
for u8::range(start_color, 10u8) |color| { for u8::range(start_color, 10u8) |color| {
bitv::set(avail, color as uint, true); avail.set(color as uint, true);
} }
// drop colors already in use in neighbourhood // drop colors already in use in neighbourhood
...@@ -60,7 +60,7 @@ fn next_color(g: grid, row: u8, col: u8, start_color: u8) -> bool { ...@@ -60,7 +60,7 @@ fn next_color(g: grid, row: u8, col: u8, start_color: u8) -> bool {
// find first remaining color that is available // find first remaining color that is available
for uint::range(1u, 10u) |i| { for uint::range(1u, 10u) |i| {
if bitv::get(avail, i) { if avail.get(i) {
g[row][col] = i as u8; g[row][col] = i as u8;
ret true; ret true;
} }
...@@ -74,7 +74,7 @@ fn next_color(g: grid, row: u8, col: u8, start_color: u8) -> bool { ...@@ -74,7 +74,7 @@ fn next_color(g: grid, row: u8, col: u8, start_color: u8) -> bool {
fn drop_colors(g: grid, avail: bitv::bitv, row: u8, col: u8) { fn drop_colors(g: grid, avail: bitv::bitv, row: u8, col: u8) {
fn drop_color(g: grid, colors: bitv::bitv, row: u8, col: u8) { fn drop_color(g: grid, colors: bitv::bitv, row: u8, col: u8) {
let color = g[row][col]; let color = g[row][col];
if color != 0u8 { bitv::set(colors, color as uint, false); } if color != 0u8 { colors.set(color as uint, false); }
} }
let it = |a,b| drop_color(g, avail, a, b); let it = |a,b| drop_color(g, avail, a, b);
......
...@@ -6,12 +6,12 @@ ...@@ -6,12 +6,12 @@
type fn_info = {vars: hashmap<uint, var_info>}; type fn_info = {vars: hashmap<uint, var_info>};
type var_info = {a: uint, b: uint}; type var_info = {a: uint, b: uint};
fn bitv_to_str(enclosing: fn_info, v: bitv::bitv) -> str { fn bitv_to_str(enclosing: fn_info, v: ~bitv::bitv) -> str {
let s = ""; let s = "";
// error is that the value type in the hash map is var_info, not a box // error is that the value type in the hash map is var_info, not a box
for enclosing.vars.each_value |val| { for enclosing.vars.each_value |val| {
if bitv::get(v, val) { s += "foo"; } if v.get(val) { s += "foo"; }
} }
ret s; ret s;
} }
......
use std;
import std::bitv::*;
fn bitv_test() -> bool {
let v1 = ~bitv(31, false);
let v2 = ~bitv(31, true);
v1.union(v2);
true
}
fn main() {
do iter::repeat(1000000) || {bitv_test()};
}
\ No newline at end of file
Markdown is supported
0% .
You are about to add 0 people to the discussion. Proceed with caution.
先完成此消息的编辑!
想要评论请 注册