path: root/src/rustc/middle/tstate/tritv.rs

import std::bitv;

export t;
export create_tritv;
export tritv_clone;
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:
   10 = "this constraint may or may not be true after execution"
   01 = "this constraint is definitely true"
   00 = "this constraint is definitely false"
   11 should never appear
 FIXME (#2178): typestate precondition (uncertain and val must
 have the same length; 11 should never appear in a given position)
 (except we're not putting typestate constraints in the compiler, as
 per discussion at).
*/

type t = {uncertain: bitv::bitv, val: bitv::bitv, nbits: uint};
enum trit { ttrue, tfalse, dont_care, }

fn create_tritv(len: uint) -> t {
    ret {uncertain: bitv::bitv(len, true),
         val: bitv::bitv(len, false),
         nbits: len};
}


fn trit_minus(a: trit, b: trit) -> trit {

    /*   2 - anything = 2
         1 - 1 = 2
         1 - 0 is an error
         1 - 2 = 1
         0 - 1 is an error
         0 - anything else - 0
     */
    alt a {
      dont_care { dont_care }
      ttrue {
        alt b {
          ttrue { dont_care }
          tfalse { ttrue }




          /* internally contradictory, but
             I guess it'll get flagged? */
          dont_care {
            ttrue
          }
        }
      }
      tfalse {
        alt b {
          ttrue { tfalse }




          /* see above comment */
          _ {
            tfalse
          }
        }
      }
    }
}

fn trit_or(a: trit, b: trit) -> trit {
    alt a {
      dont_care { b }
      ttrue { ttrue }
      tfalse {
        alt b {
          ttrue { dont_care }
          /* FIXME (#2538): ??????
             Again, unit tests would help here
           */
          _ {
            tfalse
          }
        }
      }
    }
}

// FIXME (#2538): This still seems kind of dodgy to me (that is,
// that 1 + ? = 1. But it might work out given that
// all variables start out in a 0 state. Probably I need
// to make it so that all constraints start out in a 0 state
// (we consider a constraint false until proven true), too.
fn trit_and(a: trit, b: trit) -> trit {
    alt a {
      dont_care { b }
      // also seems wrong for case b = ttrue
      ttrue {
        alt b {
          dont_care { ttrue }
          // ??? Seems wrong
          ttrue {
            ttrue
          }
          // false wins, since if something is uninit
          // on one path, we care
          // (Rationale: it's always safe to assume that
          // a var is uninitialized or that a constraint
          // needs to be re-established)
          tfalse {
            tfalse
          }
        }
      }
      // Rationale: if it's uninit on one path,
      // we can consider it as uninit on all paths
      tfalse {
        tfalse
      }
    }
    // if the result is dont_care, that means
    // a and b were both dont_care
}

fn change(changed: bool, old: trit, newv: trit) -> bool {
    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:
// mode: rust
// fill-column: 78;
// indent-tabs-mode: nil
// c-basic-offset: 4
// buffer-file-coding-system: utf-8-unix
// End:
//