186 lines
6 KiB
Rust
186 lines
6 KiB
Rust
import syntax::ast::*;
|
|
import syntax::visit;
|
|
import option::*;
|
|
import aux::*;
|
|
import tstate::ann::{pre_and_post, precond, postcond, prestate, poststate,
|
|
relax_prestate, relax_precond, relax_poststate,
|
|
pps_len, true_precond,
|
|
difference, union, clone,
|
|
set_in_postcond, set_in_poststate, set_in_poststate_,
|
|
clear_in_poststate, clear_in_prestate,
|
|
clear_in_poststate_};
|
|
import tritv::*;
|
|
import driver::session::session;
|
|
import std::map::hashmap;
|
|
|
|
fn bit_num(fcx: fn_ctxt, c: tsconstr) -> uint {
|
|
let d = c.def_id;
|
|
assert (fcx.enclosing.constrs.contains_key(d));
|
|
let rslt = fcx.enclosing.constrs.get(d);
|
|
match_args(fcx, rslt.descs, c.args)
|
|
}
|
|
|
|
fn promises(fcx: fn_ctxt, p: poststate, c: tsconstr) -> bool {
|
|
ret promises_(bit_num(fcx, c), p);
|
|
}
|
|
|
|
fn promises_(n: uint, p: poststate) -> bool {
|
|
ret tritv_get(p, n) == ttrue;
|
|
}
|
|
|
|
// v "happens after" u
|
|
fn seq_trit(u: trit, v: trit) -> trit {
|
|
alt v { ttrue { ttrue } tfalse { tfalse } dont_care { u } }
|
|
}
|
|
|
|
// idea: q "happens after" p -- so if something is
|
|
// 1 in q and 0 in p, it's 1 in the result; however,
|
|
// if it's 0 in q and 1 in p, it's 0 in the result
|
|
fn seq_tritv(p: postcond, q: postcond) {
|
|
let mut i = 0u;
|
|
assert (p.nbits == q.nbits);
|
|
while i < p.nbits {
|
|
tritv_set(i, p, seq_trit(tritv_get(p, i), tritv_get(q, i)));
|
|
i += 1u;
|
|
}
|
|
}
|
|
|
|
fn seq_postconds(fcx: fn_ctxt, ps: ~[postcond]) -> postcond {
|
|
let sz = vec::len(ps);
|
|
if sz >= 1u {
|
|
let prev = tritv_clone(ps[0]);
|
|
vec::iter_between(ps, 1u, sz, |p| seq_tritv(prev, p) );
|
|
ret prev;
|
|
} else { ret ann::empty_poststate(num_constraints(fcx.enclosing)); }
|
|
}
|
|
|
|
// Given a list of pres and posts for exprs e0 ... en,
|
|
// return the precondition for evaluating each expr in order.
|
|
// So, if e0's post is {x} and e1's pre is {x, y, z}, the entire
|
|
// precondition shouldn't include x.
|
|
fn seq_preconds(fcx: fn_ctxt, pps: ~[pre_and_post]) -> precond {
|
|
let sz: uint = vec::len(pps);
|
|
let num_vars: uint = num_constraints(fcx.enclosing);
|
|
|
|
fn seq_preconds_go(fcx: fn_ctxt, pps: ~[pre_and_post],
|
|
idx: uint, first: pre_and_post)
|
|
-> precond {
|
|
let mut idx = idx;
|
|
let mut first = first;
|
|
loop {
|
|
let sz: uint = vec::len(pps) - idx;
|
|
if sz >= 1u {
|
|
let second = pps[0];
|
|
assert (pps_len(second) == num_constraints(fcx.enclosing));
|
|
let second_pre = clone(second.precondition);
|
|
difference(second_pre, first.postcondition);
|
|
let next_first = clone(first.precondition);
|
|
union(next_first, second_pre);
|
|
let next_first_post = clone(first.postcondition);
|
|
seq_tritv(next_first_post, second.postcondition);
|
|
idx += 1u;
|
|
first = {precondition: next_first,
|
|
postcondition: next_first_post};
|
|
} else { ret first.precondition; }
|
|
}
|
|
}
|
|
|
|
if sz >= 1u {
|
|
let first = pps[0];
|
|
assert (pps_len(first) == num_vars);
|
|
ret seq_preconds_go(fcx, pps, 1u, first);
|
|
} else { ret true_precond(num_vars); }
|
|
}
|
|
|
|
fn intersect_states(p: prestate, q: prestate) -> prestate {
|
|
let rslt = tritv_clone(p);
|
|
tritv_intersect(rslt, q);
|
|
ret rslt;
|
|
}
|
|
|
|
fn gen(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
|
|
ret set_in_postcond(bit_num(fcx, c),
|
|
node_id_to_ts_ann(fcx.ccx, id).conditions);
|
|
}
|
|
|
|
fn declare_var(fcx: fn_ctxt, c: tsconstr, pre: prestate) -> prestate {
|
|
let rslt = clone(pre);
|
|
relax_prestate(bit_num(fcx, c), rslt);
|
|
// idea is this is scoped
|
|
relax_poststate(bit_num(fcx, c), rslt);
|
|
ret rslt;
|
|
}
|
|
|
|
fn relax_precond_expr(e: @expr, cx: relax_ctxt, vt: visit::vt<relax_ctxt>) {
|
|
relax_precond(cx.i as uint, expr_precond(cx.fcx.ccx, e));
|
|
visit::visit_expr(e, cx, vt);
|
|
}
|
|
|
|
fn relax_precond_stmt(s: @stmt, cx: relax_ctxt, vt: visit::vt<relax_ctxt>) {
|
|
relax_precond(cx.i as uint, stmt_precond(cx.fcx.ccx, *s));
|
|
visit::visit_stmt(s, cx, vt);
|
|
}
|
|
|
|
type relax_ctxt = {fcx: fn_ctxt, i: node_id};
|
|
|
|
fn relax_precond_block_inner(b: blk, cx: relax_ctxt,
|
|
vt: visit::vt<relax_ctxt>) {
|
|
relax_precond(cx.i as uint, block_precond(cx.fcx.ccx, b));
|
|
visit::visit_block(b, cx, vt);
|
|
}
|
|
|
|
fn relax_precond_block(fcx: fn_ctxt, i: node_id, b: blk) {
|
|
let cx = {fcx: fcx, i: i};
|
|
let visitor = visit::default_visitor::<relax_ctxt>();
|
|
let visitor =
|
|
@{visit_block: relax_precond_block_inner,
|
|
visit_expr: relax_precond_expr,
|
|
visit_stmt: relax_precond_stmt,
|
|
visit_item:
|
|
fn@(_i: @item, _cx: relax_ctxt, _vt: visit::vt<relax_ctxt>) { },
|
|
visit_fn: do_nothing
|
|
with *visitor};
|
|
let v1 = visit::mk_vt(visitor);
|
|
v1.visit_block(b, cx, v1);
|
|
}
|
|
|
|
fn gen_poststate(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
|
|
#debug("gen_poststate");
|
|
ret set_in_poststate(bit_num(fcx, c),
|
|
node_id_to_ts_ann(fcx.ccx, id).states);
|
|
}
|
|
|
|
fn kill_prestate(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
|
|
ret clear_in_prestate(bit_num(fcx, c),
|
|
node_id_to_ts_ann(fcx.ccx, id).states);
|
|
}
|
|
|
|
fn kill_all_prestate(fcx: fn_ctxt, id: node_id) {
|
|
tritv::tritv_kill(node_id_to_ts_ann(fcx.ccx, id).states.prestate);
|
|
}
|
|
|
|
|
|
fn kill_poststate(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
|
|
#debug("kill_poststate");
|
|
ret clear_in_poststate(bit_num(fcx, c),
|
|
node_id_to_ts_ann(fcx.ccx, id).states);
|
|
}
|
|
|
|
fn kill_poststate_(fcx: fn_ctxt, c: tsconstr, post: poststate) -> bool {
|
|
#debug("kill_poststate_");
|
|
ret clear_in_poststate_(bit_num(fcx, c), post);
|
|
}
|
|
|
|
fn set_in_prestate_constr(fcx: fn_ctxt, c: tsconstr, t: prestate) -> bool {
|
|
ret set_in_poststate_(bit_num(fcx, c), t);
|
|
}
|
|
|
|
//
|
|
// Local Variables:
|
|
// mode: rust
|
|
// fill-column: 78;
|
|
// indent-tabs-mode: nil
|
|
// c-basic-offset: 4
|
|
// buffer-file-coding-system: utf-8-unix
|
|
// End:
|
|
//
|