SE547: Lecture 5 (BDDs)

Contents [0/22]

BDDs: Overview [1/22]

BDDs: Software Security [2/22]

BDDs: Software Security [3/22]

BDDs: Software Model Checking [4/22]

BDDs: Software Model Checking [5/22]

BDDs: Logical Satisfaction [6/22]

BDDs: Logical Satisfaction [7/22]

BDDs: Binary Decision Diagrams [8/22]

BDDs: Binary Decision Diagrams [9/22]

BDDs: Binary Decision Diagrams [10/22]

BDDs: Binary Decision Diagrams [11/22]

BDDs: Binary Decision Diagrams [12/22]

BDDs: Implementing BDDs [13/22]

BDDs: Implementing BDDs [14/22]

BDDs: Implementing BDDs [15/22]

BDDs: Implementing BDDs [16/22]

BDDs: Next week [17/22]

BDDs: Acknowledgement [18/22]

BDDs: Bool Code [19/22]

BDDs: Integer Code [20/22]

BDDs: Integer Test Code [21/22]

BDDs: Util Code [22/22]

BDDs: Overview [1/22]

Overview

Software Security

Software Model Checking

Logical Satisfaction

Binary Decision Diagrams

Implementing BDDs

BDDs: Software Security [2/22]

Secure software is intended to grant rights to users acting in certain roles.

What are examples of rights and roles?

Incorrect software can result in rights escalation. What is this? What are examples?

What are common strategies for attackers achieving rights escalation?

What can we do about these attacks?

BDDs: Software Security [3/22]

What is a buffer overflow attack?

Can buffer overflow attacks occur in C? In Java?

What language feature of C or Java allows buffer overflows?

What can we do about it? Statically? Dynamically?

What are the tradeoffs between static and dynamic checks?

Check out this cool applet: http://nsfsecurity.pr.erau.edu/bom/

BDDs: Software Model Checking [4/22]

What is a software model checker?

How does a software model checker compare to conventional testing?

Can a software model checker find all bugs?

BDDs: Software Model Checking [5/22]

Software model checkers translate source code into (possibly big!) logical formulas. For example:

  void foo (int x, int y) {
    char[] z = new char[x+1];
    if (y < x) { z[y] = 'a'; }
  }

Is this program safe? What logical formula do we generate from it?

We have turned the problem of software model checking into the problem of logical satisfaction.

More on software model checkers later...

BDDs: Logical Satisfaction [6/22]

What is first order predicate logic? What is logical satisfaction?

Logical satisfaction is NP-complete. What does this mean? What is the best-known running time for an NP-complete problem?

For example, how long will it take to determine satisfaction for:

x : uint16 . y : uint16 . z : uint16 . (x + y) + z = x + (y + z)

Try it... file:simplebdd.zip contains a file:simplebdd/test/TestArithBrute.java [source] [doc-public] [doc-private] class.

BDDs: Logical Satisfaction [7/22]

Logical satisfaction is solved by SAT-solvers.

High-quality production SAT-solvers exist Chaff, zChaff, ... See http://www.satlive.org.

We have success stories of using zChaff to solve problems with more than one million variables and 10 million clauses.
-- zChaff web site

A common simple solution is binary decision diagrams.

Try it... file:simplebdd.zip contains a BDD-based file:simplebdd/test/TestArith.java [source] [doc-public] [doc-private] class.

BDDs: Binary Decision Diagrams [8/22]

A first shot at solving satisfaction: convert to Disjunctive Normal Form (DNF).

What is DNF?

How do we check satisfiability of a formula in DNF?

Why is this not an acceptable solution?

BDDs: Binary Decision Diagrams [9/22]

A better shot; use:

s t, u read as `if s then t else u'

Convert to If-then-else Normal Form (INF).

What is INF?

What is the INF for the following:

x y z

We can draw INFs as binary decision trees. What is a decision tree? What is the decision tree for this formula?

Decision trees are still not acceptable: why not?

BDDs: Binary Decision Diagrams [10/22]

A decision diagram is a decision tree where we share nodes.

What is the decision diagram for the following:

x y z

What is the decision diagram for the follwing:

x₁ ... x_n

Hooray, much better!

BDDs: Binary Decision Diagrams [11/22]

Binary Decision Diagrams are a graphical representation of the grammar:

s, t, u ::=
    0
    1
    x t, u

A couple of improvements to Binary Decision Diagrams:

a) What should we do about x t, t? [Reduced BDDs.]

b) There are two representations of x y: what are they? What should we do about this? [Ordered BDDs.]

BDDs: Binary Decision Diagrams [12/22]

Reduced, Ordered BDDs have the following very nice property:

t u is a tautology just when t = u

that is syntactic equality is the same as semantic equality.

In particular, for ROBDDs:

The only tautology is 1.
The only unsatisfiable formula is 0.

This makes checking for satisfiability pretty easy! (But remember that satisfiability is NP-complete; where did the hard work go?)

BDDs: Implementing BDDs [13/22]

How can we convert this grammar into a class hierarchy?

s, t, u ::=
    0
    1
    x t, u

Hint: start with:

  interface BoolPred {
    BoolPred ite (BoolPred p, BoolPred q); // this -> p, q
    ...
    static final BoolPred T = ...;
    static final BoolPred F = ...;
  }

BDDs: Implementing BDDs [14/22]

How can we implement the ite method?

  interface BoolPred {
    BoolPred ite (BoolPred p, BoolPred q); // this -> p, q
    ...
    static final BoolPred T = ...;
    static final BoolPred F = ...;
  }

BDDs: Implementing BDDs [15/22]

Implementation trick: use the flyweight pattern. What is this? Why does it help?

(Other names for this kind of flyweighting: dynamic programming, memoization...)

A very simple implementation of BDDs is in simplebdd.bool.BoolPred in file:simplebdd.zip (approx. 150loc!).

BDDs: Implementing BDDs [16/22]

BDDs are just about binary data, but we can code up fixed-width arithmetic...

How do we code an n-bit integer variable?

How do we code an n-bit integer expression?

How do we code n-bit integer arithmetic?

A partial implementation is in simplebdd.integer.IntPred in file:simplebdd.zip (approx. 200loc).

BDDs: Next week [17/22]

Model checking.

BDDs: Acknowledgement [18/22]

These notes and the associated code are from Alan Jeffrey

BDDs: Bool Code [19/22]

file:simplebdd/bool/BoolPred.java [source] [doc-public] [doc-private]

00001: package simplebdd.bool;
00002: 
00003: /**
00004:  * An implementation of Boolean Predicates using BDDs.
00005:  * The functions which take arguments of type BoolPred may throw a
00006:  * ClassCastException if given an object that was not created by
00007:  * BoolPred.factory().
00008:  */
00009: public interface BoolPred {
00010:   public static BoolPred T = new True ();
00011:   public static BoolPred F = new False ();
00012:   public static BoolPredFactory factory = new BPFactory ();
00013:   public static BoolPredFunctions functions = new BPFunctions ();
00014:   
00015:   public BoolPred not  ();
00016:   public BoolPred and  (BoolPred p);
00017:   public BoolPred or   (BoolPred p);
00018:   public BoolPred xor  (BoolPred p);
00019:   public BoolPred impl (BoolPred p);
00020:   public BoolPred iff  (BoolPred p);
00021:   public BoolPred ite  (BoolPred p, BoolPred q);
00022:   
00023:   public String name();
00024: }
00025: 
00026: interface pBoolPred extends BoolPred, Comparable {
00027:   public String id();
00028:   public void initToGraphString();
00029:   public void toGraphString(StringBuffer b);
00030:   public int compareTo (Object that);
00031: }
00032: 
00033: // in the comparison order, T and F are biggest (and they are both bigger than each other!)
00034: class True implements pBoolPred {
00035:   public BoolPred not  ()           { return F; }
00036:   public BoolPred and  (BoolPred p) { return p; }
00037:   public BoolPred or   (BoolPred p) { return this; }
00038:   public BoolPred xor  (BoolPred p) { return p.not (); }
00039:   public BoolPred impl (BoolPred p) { return p; }
00040:   public BoolPred iff  (BoolPred p) { return p; }
00041:   public BoolPred ite  (BoolPred p, BoolPred q) { return p; }
00042:   
00043:   public String name()      { return "0"; }
00044:   public String id()        { return "0"; }
00045:   public String toString () { return "true"; }
00046:   
00047:   public int compareTo (Object that) { return 1; }
00048:   public void initToGraphString() {}
00049:   public void toGraphString(StringBuffer b) {}
00050: }
00051: 
00052: class False implements pBoolPred {
00053:   public BoolPred not  ()           { return T; }
00054:   public BoolPred and  (BoolPred p) { return this; }
00055:   public BoolPred or   (BoolPred p) { return p; }
00056:   public BoolPred xor  (BoolPred p) { return p; }
00057:   public BoolPred impl (BoolPred p) { return T; }
00058:   public BoolPred iff  (BoolPred p) { return p.not (); }
00059:   public BoolPred ite  (BoolPred p, BoolPred q) { return q; }
00060:   
00061:   public String name()      { return "1"; }
00062:   public String id()        { return "1"; }
00063:   public String toString () { return "false"; }
00064:   
00065:   public int compareTo (Object that) { return 1; }
00066:   public void initToGraphString() {}
00067:   public void toGraphString(StringBuffer b) {}
00068: }
00069: 
00070: class Cond implements pBoolPred {
00071:   private final String _id;
00072:   private final String _name;
00073:   final pBoolPred _t;
00074:   final pBoolPred _f; 
00075:   Cond (String id, String name, BoolPred t, BoolPred f) {
00076:     _id = id; _name = name; _t = (pBoolPred)t; _f = (pBoolPred)f;
00077:   }
00078:   
00079:   public final BoolPred not  ()           { return ite (F, T); }
00080:   public final BoolPred and  (BoolPred p) { return ite (p, F); }
00081:   public final BoolPred or   (BoolPred p) { return ite (T, p); }
00082:   public final BoolPred xor  (BoolPred p) { return ite (p.not (), p); }
00083:   public final BoolPred impl (BoolPred p) { return ite (p, T); }
00084:   public final BoolPred iff  (BoolPred p) { return ite (p, p.not ()); }
00085:   public final BoolPred ite  (BoolPred p, BoolPred q) {
00086:     return BPFactory.buildCond (this, (pBoolPred)p, (pBoolPred)q);
00087:   }
00088:   
00089:   public String name() { return _name; }
00090:   public String id() { return _id; }
00091:   public String toString () { 
00092:     if ( _t == T && _f == F) {
00093:       return _name;
00094:     } else if (_t == F && _f == T) {
00095:       return "!" + _name;
00096:     } else {
00097:       return "(" + _name + " ? " + _t + " : " + _f + ")";
00098:     }
00099:   }
00100:   
00101:   public int compareTo (Object that) { return _name.compareTo (((BoolPred)that).name()); }
00102:   
00103:   private boolean _printed = false;
00104:   public void initToGraphString() {
00105:     _printed=false;
00106:     _t.initToGraphString();
00107:     _f.initToGraphString();
00108:   }
00109:   public void toGraphString(StringBuffer b) {
00110:     if (!_printed) { b.append (id() + " ? " + _t.id() + " : " + _f.id() + "\n"); }
00111:     _printed = true; 
00112:     _t.toGraphString(b);
00113:     _f.toGraphString(b);
00114:   }
00115: }
00116: 
00117:

file:simplebdd/bool/BoolPredFactory.java [source] [doc-public] [doc-private]

00001: package simplebdd.bool;
00002: 
00003: import simplebdd.util.HashMap3;
00004: 
00005: public interface BoolPredFactory {
00006:   public BoolPred buildVar (String name);
00007: }
00008: 
00009: class BPFactory implements BoolPredFactory {
00010:   private static final HashMap3 flyweight = new HashMap3 ();
00011:   private static int _COUNT = 0;
00012:   private static pBoolPred min(pBoolPred p1, pBoolPred p2, pBoolPred p3) {
00013:     pBoolPred result = p1;
00014:     if (p2.compareTo(result) < 0) { result =  p2; }
00015:     if (p3.compareTo(result) < 0) { result =  p3; }
00016:     return result;
00017:   }
00018:   static BoolPred buildCond (Cond b, pBoolPred p, pBoolPred q) {
00019:     BoolPred result = (pBoolPred)(flyweight.get (b, p, q));
00020:     if (result == null) {
00021:       // Since b is a Cond, n cannot be 0 or 1
00022:       // But b have the same name as p or q
00023:       String n = min(b, p, q).name();
00024:       // The following two lines assign t and f properly but are hard to read
00025:       // BoolPred t = (b.name()!=n ? b : b._t).ite((p.name()!=n ? p : ((Cond)p)._t), (q.name()!=n ? q : ((Cond)q)._t));
00026:       // BoolPred f = (b.name()!=n ? b : b._f).ite((p.name()!=n ? p : ((Cond)p)._f), (q.name()!=n ? q : ((Cond)q)._f));
00027:       BoolPred bt = (b.name() != n) ? b : b._t;
00028:       BoolPred bf = (b.name() != n) ? b : b._f;
00029:       BoolPred pt = (p.name() != n) ? p : ((Cond)p)._t;
00030:       BoolPred pf = (p.name() != n) ? p : ((Cond)p)._f;
00031:       BoolPred qt = (q.name() != n) ? q : ((Cond)q)._t;
00032:       BoolPred qf = (q.name() != n) ? q : ((Cond)q)._f;
00033:       BoolPred t = bt.ite(pt, qt);
00034:       BoolPred f = bf.ite(pf, qf);
00035:       if (t == f) {
00036:         result = t;
00037:       } else {
00038:         result = (BoolPred)(flyweight.get (n, t, f));
00039:         if (result == null) { 
00040:           result = new Cond (n + (++_COUNT), n, t, f);
00041:           flyweight.put (n, t, f, result);
00042:         }
00043:       }
00044:       flyweight.put (b, p, q, result);
00045:     }
00046:     return result;
00047:   }
00048:   public BoolPred buildVar (String name) {
00049:     BoolPred result = (BoolPred)(flyweight.get (name, BoolPred.T, BoolPred.F));
00050:     if (result == null) { 
00051:       result = new Cond (name + (++_COUNT), name, BoolPred.T, BoolPred.F);
00052:       flyweight.put (name, BoolPred.T, BoolPred.F, result);
00053:     }
00054:     return result;
00055:   }
00056: }
00057:

file:simplebdd/bool/BoolPredFunctions.java [source] [doc-public] [doc-private]

00001: package simplebdd.bool;
00002: 
00003: public interface BoolPredFunctions {
00004:   public String toGraphString (BoolPred p);
00005: }
00006: 
00007: class BPFunctions implements BoolPredFunctions {
00008:   /** @throws ClassCastException if p is not created by BoolPred.factory() */
00009:   public String toGraphString (BoolPred p) {
00010:     ((pBoolPred)p).initToGraphString();
00011:     StringBuffer b = new StringBuffer();
00012:     ((pBoolPred)p).toGraphString(b);
00013:     return b.toString();
00014:   }
00015: }
00016:

file:simplebdd/test/TestBool.java [source] [doc-public] [doc-private]

00001: package simplebdd.test;
00002: 
00003: import simplebdd.bool.BoolPred;
00004: 
00005: public class TestBool {
00006:   public static void main (String[] args) {
00007:     new TestBool().run ();
00008:   }
00009:   
00010:   final BoolPred x;
00011:   final BoolPred y;
00012:   final BoolPred z;
00013:   TestBool () {
00014:     this.x = BoolPred.factory.buildVar ("x");
00015:     this.y = BoolPred.factory.buildVar ("y");
00016:     this.z = BoolPred.factory.buildVar ("z");
00017:   }
00018:   
00019:   void runtest (String s, BoolPred p, boolean expectedValue) {
00020:     String trueString  = (expectedValue? "Good. " : "BAD!! ");
00021:     String falseString = (expectedValue? "BAD!! " : "Good. ");
00022:     if (p == BoolPred.T) {
00023:       System.out.println 
00024:         (trueString + s + " is always true");
00025:     } else {
00026:       System.out.println 
00027:         (falseString + s + " is sometimes false");
00028:     }
00029:   }
00030:   
00031:   public void run () {
00032:     System.out.println (BoolPred.T);
00033:     System.out.println (BoolPred.functions.toGraphString(BoolPred.T));
00034:     System.out.println (x);
00035:     System.out.println (BoolPred.functions.toGraphString(x));
00036:     System.out.println (x.not());
00037:     System.out.println (BoolPred.functions.toGraphString(x.not()));
00038:     System.out.println (x.ite(y,z));
00039:     System.out.println (BoolPred.functions.toGraphString(x.ite(y,z)));
00040:     System.out.println ("(y ? z : x)");
00041:     System.out.println (BoolPred.functions.toGraphString(y.ite(z,x)));
00042:     
00043:     System.out.println ("x xor y xor z");
00044:     System.out.println (BoolPred.functions.toGraphString(x.xor (y).xor (z)));
00045:     System.out.println ("x and x");
00046:     System.out.println (BoolPred.functions.toGraphString(x.and (x)));
00047:     System.out.println ("x or y");
00048:     System.out.println (BoolPred.functions.toGraphString(x.or (y)));
00049:     System.out.println ("y or x");
00050:     System.out.println (BoolPred.functions.toGraphString(y.or (x)));
00051:     
00052:     runtest (x.and (y) + "iff" + y.and (x),
00053:              x.and (y).iff (y.and (x)), true);
00054:     runtest ("", x.and (BoolPred.T).iff (x), true);
00055:     runtest ("", x.xor (y.xor (z)).iff (x.xor (y).xor (z)), true);
00056:   }
00057:   
00058: }
00059:

BDDs: Integer Code [20/22]

file:simplebdd/integer/IntConst.java [source] [doc-public] [doc-private]

00001: package simplebdd.integer;
00002: 
00003: public interface IntConst extends IntExp {
00004:   
00005:   public int val ();
00006:   
00007:   public static final IntConstFactory factory = new IntConstFactoryImpl ();
00008:   
00009: }
00010:

file:simplebdd/integer/IntConstFactory.java [source] [doc-public] [doc-private]

00001: package simplebdd.integer;
00002: 
00003: public interface IntConstFactory {
00004:   
00005:   public IntConst build (int bits, int value);
00006:   
00007: }
00008:

file:simplebdd/integer/IntExp.java [source] [doc-public] [doc-private]

00001: package simplebdd.integer;
00002: 
00003: import simplebdd.bool.BoolPred;
00004: 
00005: public interface IntExp {
00006:   
00007:   public IntPred eq (IntExp e);
00008:   public IntPred gtr (IntExp e);
00009:   public IntPred geq (IntExp e);
00010:   public IntExp plus (IntExp e);
00011:   public IntExp minus (IntExp e);
00012:   
00013:   public int bits ();
00014:   public BoolPred bit (int i);
00015:   
00016: }
00017:

file:simplebdd/integer/IntExpFactory.java [source] [doc-public] [doc-private]

00001: package simplebdd.integer;
00002: 
00003: public interface IntExpFactory {
00004:   
00005:   public IntExp buildConst (int bits, int val);
00006:   public IntVar buildVar (int bits, String name);
00007:   
00008: }
00009:

file:simplebdd/integer/IntPred.java [source] [doc-public] [doc-private]

00001: package simplebdd.integer;
00002: 
00003: import simplebdd.bool.BoolPred;
00004: 
00005: public interface IntPred {
00006:   public static IntPred T = new TrueImpl ();
00007:   public static IntPred F = new FalseImpl ();
00008:   
00009:   public IntPred not ();
00010:   public IntPred and (IntPred p);
00011:   public IntPred or (IntPred p);
00012:   public IntPred impl (IntPred p);
00013:   public IntPred iff (IntPred p);
00014:   
00015:   public boolean isTautology ();
00016:   public IntConst solution (IntVar x);
00017:   
00018:   public BoolPred contents ();
00019: }
00020: 
00021: abstract class IntPredAbst implements IntPred {
00022:   final BoolPred contents;
00023:   IntPredAbst (BoolPred contents) { this.contents = contents; }
00024:   
00025:   public final BoolPred contents () { return this.contents; }
00026:   
00027:   public final IntPred not ()           { return new NotImpl (this); }
00028:   public final IntPred and (IntPred p)  { return new AndImpl (this, p); }
00029:   public final IntPred or (IntPred p)   { return new OrImpl (this, p); }
00030:   public final IntPred impl (IntPred p) { return new ImplImpl (this, p); }
00031:   public final IntPred iff (IntPred p)  { return new IffImpl (this, p); }
00032:   
00033:   public final boolean isTautology () { return this.contents == BoolPred.T; }
00034:   
00035:   public final IntConst solution (IntVar var) {
00036:     int result = 0;
00037:     int mask = 1;
00038:     BoolPred prop = this.contents ();
00039:     if (prop == BoolPred.F) { 
00040:       throw new RuntimeException 
00041:         ("Can't solve " + this + " for " + var + " since it is unsatisfiable");
00042:     }
00043:     for (int i=0; i<var.bits(); i++) {
00044:       if (prop.and (var.bit (i).not ()) == BoolPred.F) {
00045:         result = result + mask;
00046:         prop = prop.and (var.bit (i));
00047:       } else {
00048:         prop = prop.and (var.bit (i).not ());
00049:       }
00050:       mask = mask * 2;
00051:     }
00052:     return IntConst.factory.build (var.bits (), result);
00053:   }
00054:   
00055:   protected static void sameBits (IntExp e, IntExp f) {
00056:     if (e.bits () != f.bits ()) {
00057:       throw new RuntimeException ("Expressions " + e + " and " + f + " have different bit lengths");
00058:     }
00059:   }
00060:   
00061: }
00062: 
00063: class TrueImpl extends IntPredAbst {
00064:   TrueImpl ()               { super (BoolPred.T); }
00065:   public String toString () { return "true"; }
00066: }
00067: 
00068: class FalseImpl extends IntPredAbst {
00069:   FalseImpl ()              { super (BoolPred.F); }
00070:   public String toString () { return "false"; }
00071: }
00072: 
00073: class NotImpl extends IntPredAbst {
00074:   final IntPred p;
00075:   NotImpl (IntPred p)       { super (p.contents ().not ()); this.p = p; }
00076:   public String toString () { return "!" + p; }
00077: }
00078: 
00079: class AndImpl extends IntPredAbst {
00080:   final IntPred p; final IntPred q;
00081:   AndImpl (IntPred p, IntPred q) { super (p.contents ().and (q.contents ())); this.p = p; this.q = q; }
00082:   public String toString ()      { return "(" + p + " && " + q + ")"; }
00083: }
00084: 
00085: class OrImpl extends IntPredAbst {
00086:   final IntPred p; final IntPred q;
00087:   OrImpl (IntPred p, IntPred q) { super (p.contents ().or (q.contents ())); this.p = p; this.q = q; }
00088:   public String toString ()     { return "(" + p + " || " + q + ")"; }
00089: }
00090: 
00091: class ImplImpl extends IntPredAbst {
00092:   final IntPred p; final IntPred q;
00093:   ImplImpl (IntPred p, IntPred q) { super (p.contents ().impl (q.contents ())); this.p = p; this.q = q; }
00094:   public String toString ()       { return "(" + p + " ==> " + q + ")"; }
00095: }
00096: 
00097: class IffImpl extends IntPredAbst {
00098:   final IntPred p; final IntPred q;
00099:   IffImpl (IntPred p, IntPred q) { super (p.contents ().iff (q.contents ())); this.p = p; this.q = q; }
00100:   public String toString ()      { return "(" + p + " <=> " + q + ")"; }
00101: }
00102: 
00103: class EqImpl extends IntPredAbst {
00104:   final IntExp e; final IntExp f;
00105:   EqImpl (IntExp e, IntExp f) { super (mkContents (e, f)); this.e = e; this.f = f; }
00106:   public String toString ()   { return "(" + e + " == " + f + ")"; }
00107:   
00108:   private static BoolPred mkContents (IntExp e, IntExp f) {
00109:     BoolPred result = BoolPred.T;
00110:     sameBits (e, f);
00111:     for (int i=0; i<e.bits (); i++) {
00112:       result = result.and (e.bit (i).iff (f.bit (i)));
00113:     }
00114:     return result;
00115:   }
00116: }
00117: 
00118: class GeqImpl extends IntPredAbst {
00119:   final IntExp e; final IntExp f;
00120:   GeqImpl (IntExp e, IntExp f) { super (mkContents (e, f)); this.e = e; this.f = f; }
00121:   public String toString ()    { return "(" + e + " >= " + f + ")"; }
00122:   
00123:   private static BoolPred mkContents (IntExp e, IntExp f) {
00124:     BoolPred result = BoolPred.T;
00125:     sameBits (e, f);
00126:     for (int i=0; i<e.bits (); i++) {
00127:       result = e.bit (i).ite (f.bit (i).not ().or (result), f.bit(i).not ().and (result));
00128:     }
00129:     return result;
00130:   }
00131: }
00132: 
00133: class GtrImpl extends IntPredAbst {
00134:   final IntExp e; final IntExp f;
00135:   GtrImpl (IntExp e, IntExp f) { super (mkContents (e, f)); this.e = e; this.f = f; }
00136:   public String toString ()    { return "(" + e + " > " + f + ")"; }
00137:   
00138:   private static BoolPred mkContents (IntExp e, IntExp f) {
00139:     BoolPred result = BoolPred.F;
00140:     sameBits (e, f);
00141:     for (int i=0; i<e.bits (); i++) {
00142:       result = e.bit (i).ite (f.bit (i).not ().or (result), f.bit(i).not ().and (result));
00143:     }
00144:     return result;
00145:   }
00146: }
00147: 
00148: abstract class IntExpAbst implements IntExp {
00149:   final BoolPred[] bits;
00150:   
00151:   IntExpAbst (BoolPred[] bits) { this.bits = bits; }
00152:   
00153:   public final IntExp plus (IntExp e)  { return new PlusImpl (this, e); }
00154:   public final IntExp minus (IntExp e) { return new MinusImpl (this, e); }
00155:   
00156:   public final IntPred eq (IntExp e)   { return new EqImpl (this, e); }
00157:   public final IntPred geq (IntExp e)  { return new GeqImpl (this, e); }
00158:   public final IntPred gtr (IntExp e)  { return new GtrImpl (this, e); }
00159:   
00160:   public final int bits () { return bits.length; }
00161:   public final BoolPred bit (int i) { return bits[i]; }
00162: }
00163: 
00164: class ConstImpl extends IntExpAbst implements IntConst {
00165:   final int val;
00166:   ConstImpl (int bits, int val) { super (mkBits (bits, val)); this.val = val; }
00167:   public String toString ()     { return "" + val; }
00168:   public int val ()             { return this.val; }
00169:   
00170:   private static BoolPred[] mkBits (int bits, int val) {
00171:     BoolPred[] result = new BoolPred[bits];
00172:     for (int i=0; i<bits; i++) {
00173:       result[i] = (val%2 == 1 ? BoolPred.T : BoolPred.F);
00174:       val = val/2;
00175:     }
00176:     return result;
00177:   }
00178: }
00179: 
00180: class VarImpl extends IntExpAbst implements IntVar {
00181:   final String name;
00182:   VarImpl (int bits, String name) { super (mkBits (bits, name)); this.name = name; }
00183:   public String toString ()       { return name; }
00184:   
00185:   private static BoolPred[] mkBits (int bits, String name) {
00186:     BoolPred[] result = new BoolPred[bits];
00187:     for (int i=0; i<bits; i++) {
00188:       result[i] = BoolPred.factory.buildVar ("[" + i + "]" + name);
00189:     }
00190:     return result;
00191:   }
00192: }
00193: 
00194: class PlusImpl extends IntExpAbst {
00195:   final IntExp e; final IntExp f;
00196:   PlusImpl (IntExp e, IntExp f) { super (mkBits (e, f)); this.e = e; this.f = f; }
00197:   public String toString ()     { return "(" + e + " + " + f + ")"; }
00198:   
00199:   private static BoolPred[] mkBits (IntExp e, IntExp f) {
00200:     IntPredAbst.sameBits (e, f);
00201:     BoolPred[] result = new BoolPred[e.bits ()];
00202:     BoolPred carry = BoolPred.F;
00203:     for (int i=0; i<result.length; i++) {
00204:       result[i] = e.bit (i).xor (f.bit (i)).xor (carry);
00205:       carry = carry.ite (e.bit (i).or (f.bit (i)), e.bit (i).and (f.bit (i)));
00206:     }
00207:     return result;
00208:   }
00209: }
00210: 
00211: class MinusImpl extends IntExpAbst {
00212:   final IntExp e; final IntExp f;
00213:   MinusImpl (IntExp e, IntExp f) { super (mkBits (e, f)); this.e = e; this.f = f; }
00214:   public String toString () { return "(" + e + " - " + f + ")"; }
00215:   
00216:   static BoolPred[] mkBits (IntExp e, IntExp f) {
00217:     // TODO
00218:   }
00219: }
00220: 
00221: class IntConstFactoryImpl implements IntConstFactory {
00222:   public IntConst build (int bits, int val) {
00223:     return new ConstImpl (bits, val);
00224:   }
00225: }
00226: 
00227: class IntVarFactoryImpl implements IntVarFactory {
00228:   public IntVar build (int bits, String name) {
00229:     return new VarImpl (bits, name);
00230:   }
00231: }
00232: 
00233:

file:simplebdd/integer/IntVar.java [source] [doc-public] [doc-private]

00001: package simplebdd.integer;
00002: 
00003: public interface IntVar extends IntExp {
00004:   
00005:   public final static IntVarFactory factory = new IntVarFactoryImpl ();
00006:   
00007: }
00008:

file:simplebdd/integer/IntVarFactory.java [source] [doc-public] [doc-private]

00001: package simplebdd.integer;
00002: 
00003: public interface IntVarFactory {
00004:   
00005:   public IntVar build (int bits, String name);
00006:   
00007: }
00008:

BDDs: Integer Test Code [21/22]

file:simplebdd/test/TestArith.java [source] [doc-public] [doc-private]

00001: package simplebdd.test;
00002: 
00003: import simplebdd.integer.IntVar;
00004: import simplebdd.integer.IntConst;
00005: import simplebdd.integer.IntPred;
00006: 
00007: public class TestArith {
00008:   public static void main (String[] args) {
00009:     int max;
00010:     try {
00011:       max = Integer.parseInt (args[0]);
00012:     } catch (Exception e) {
00013:       System.out.println("Usage: TestArith max");
00014:       return;
00015:     }
00016:     new TestArith(max).run ();
00017:   }
00018:   
00019:   final IntVar x;
00020:   final IntVar y;
00021:   final IntVar z;
00022:   final IntConst zero;
00023:   final IntConst one;
00024:   final int bits;
00025:   TestArith (int bits) {
00026:     this.x = IntVar.factory.build (bits, "x");
00027:     this.y = IntVar.factory.build (bits, "y");
00028:     this.z = IntVar.factory.build (bits, "z");
00029:     this.zero = IntConst.factory.build (bits, 0);
00030:     this.one = IntConst.factory.build (bits, 1);
00031:     this.bits = bits;
00032:   }
00033:   
00034:   void runtest (IntPred p, boolean expectedValue) {
00035:     String trueString  = (expectedValue? "Good. " : "BAD!! ");
00036:     String falseString = (expectedValue? "BAD!! " : "Good. ");
00037:     if (p.isTautology ()) {
00038:       System.out.println 
00039:         (trueString + p + " is always true");
00040:     } else {
00041:       IntConst xSoln = p.not ().solution (x);
00042:       IntConst ySoln = p.not ().and (x.eq (xSoln)).solution (y);
00043:       IntConst zSoln = p.not ().and (x.eq (xSoln)).and (y.eq (ySoln)).solution (z);
00044:       System.out.println 
00045:         (falseString + p + " is sometimes false: " +
00046:          "x = " + xSoln + ", " +
00047:          "y = " + ySoln + ", " +
00048:          "z = " + zSoln +
00049:          ".");
00050:     }
00051:   }
00052:   
00053:   public void run () {
00054:     runtest (x.plus (y).eq (y.plus (x)), true);
00055:     runtest (x.plus (zero).eq (x), true);
00056:     runtest (x.plus (y.plus (z)).eq (x.plus (y).plus (z)), true);
00057:     runtest (x.geq (zero), true);
00058:     runtest (x.eq (zero), false);
00059:     runtest (x.gtr (zero), false);
00060:     runtest (x.plus (one).gtr (x), false);
00061:     runtest (x.plus (y).geq (x), false);
00062:     runtest (x.plus (x).eq (x), false);
00063:     runtest (x.plus (x).gtr (x), false);
00064:     runtest (x.plus (one).eq (x), false);
00065:   }
00066:   
00067: }
00068:

file:simplebdd/test/TestArithBrute.java [source] [doc-public] [doc-private]

00001: package simplebdd.test;
00002: 
00003: interface Test {
00004:   public boolean isTautology (int max); 
00005:   public boolean expectedValue (); 
00006: }
00007: 
00008: abstract class Test1 implements Test {
00009:   public abstract boolean test (int x);
00010:   public boolean isTautology (int max) {
00011:     for (int i=0; i < max; i++) {
00012:       if (!test (i)) { return false; }
00013:     }
00014:     return true;
00015:   }
00016: }
00017: 
00018: abstract class Test2 implements Test {
00019:   public abstract boolean test (int x, int y);
00020:   public boolean isTautology (int max) {
00021:     for (int i=0; i < max; i++) {
00022:       for (int j=0; j < max; j++) {
00023:         if (!test (i,j)) { return false; }
00024:       }
00025:     }
00026:     return true;
00027:   }
00028: }
00029: 
00030: abstract class Test3 implements Test {
00031:   public abstract  boolean test (int x, int y, int z);
00032:   public boolean isTautology (int max) {
00033:     for (int i=0; i < max; i++) {
00034:       for (int j=0; j < max; j++) {
00035:         for (int k=0; k < max; k++) {
00036:           if (!test (i,j, k)) { return false; }
00037:         }
00038:       }
00039:     }
00040:     return true;
00041:   }
00042: }
00043: 
00044: public class TestArithBrute {
00045:   public static void main (String[] args) {
00046:     int max;
00047:     try {
00048:       max = Integer.parseInt (args[0]);
00049:     } catch (Exception e) {
00050:       System.out.println("Usage: TestArithBrute max");
00051:       return;
00052:     }
00053:     new TestArithBrute(max).run ();
00054:   }
00055:   
00056:   final int bits;
00057:   final int max;
00058:   final Test[] test;
00059:   TestArithBrute (int bits) {
00060:     int[] x = new int[] {1,2,3};
00061:     x[0]=1;
00062:     x[1]=2;
00063:     x[2]=3;
00064:     this.bits = bits;
00065:     this.max = 1 << (bits-1);
00066:     this.test  = new Test[] {
00067:       new Test2 () {
00068:         public String toString () { return "x+y=y+x"; }
00069:         public boolean expectedValue () { return true; }
00070:         public boolean test (int x, int y) {
00071:           return (x+y)%max == (y+x)%max;
00072:         } },
00073:       new Test1 () {
00074:         public String toString () { return "x+0=x"; }
00075:         public boolean expectedValue () { return true; }
00076:         public boolean test (int x) {
00077:           return (x+0)%max == x;
00078:         } },
00079:       new Test3 () {
00080:         public String toString () { return "x+(y+z)=(x+y)+z"; }
00081:         public boolean expectedValue () { return true; }
00082:         public boolean test (int x, int y, int z) {
00083:           return (x+((y+z)%max))%max == (((x+y)%max)+z)%max;
00084:         } },
00085:       new Test1 () {
00086:         public String toString () { return "x>=0"; }
00087:         public boolean expectedValue () { return true; }
00088:         public boolean test (int x) {
00089:           return x>=0;
00090:         } },
00091:       new Test1 () {
00092:         public String toString () { return "X+1>x"; }
00093:         public boolean expectedValue () { return false; }
00094:         public boolean test (int x) {
00095:           return (x+1)%max > x;
00096:         } },
00097:       new Test1 () {
00098:         public String toString () { return "x+x=x"; }
00099:         public boolean expectedValue () { return false; }
00100:         public boolean test (int x) {
00101:           return (x+x)%max == x;
00102:         } },
00103:       new Test1 () {
00104:         public String toString () { return "x+x>x"; }
00105:         public boolean expectedValue () { return false; }
00106:         public boolean test (int x) {
00107:           return (x+x)%max > x;
00108:         } },
00109:       new Test1 () {
00110:         public String toString () { return "x+1=x"; }
00111:         public boolean expectedValue () { return false; }
00112:         public boolean test (int x) {
00113:           return (x+1)%max == x;
00114:         } },
00115:       new Test1 () {
00116:         public String toString () { return "x>0"; }
00117:         public boolean expectedValue () { return false; }
00118:         public boolean test (int x) {
00119:           return x>0;
00120:         } }
00121:     };
00122:   }
00123:   
00124:   public void run () {
00125:     for (int i = 0; i<test.length; i++) {
00126:       String trueString  = (test[i].expectedValue() ? "Good. " : "BAD!! ");
00127:       String falseString = (test[i].expectedValue() ? "BAD!! " : "Good. ");
00128:       if (test[i].isTautology (max)) {
00129:         System.out.println (trueString + test[i] + " is always true");
00130:       } else {
00131:         System.out.println (falseString + test[i] + " is sometimes false");
00132:       }
00133:     }
00134:   }
00135: }
00136:

file:simplebdd/test/TestSubtraction.java [source] [doc-public] [doc-private]

00001: package simplebdd.test;
00002: 
00003: public class TestSubtraction extends TestArith {
00004:   public static void main (String[] args) {
00005:     int max;
00006:     try {
00007:       max = Integer.parseInt (args[0]);
00008:     } catch (Exception e) {
00009:       System.out.println("Usage: TestSubtraction max");
00010:       return;
00011:     }
00012:     new TestSubtraction(max).run ();
00013:   }
00014:   
00015:   TestSubtraction (int bits) { super (bits); }
00016:   
00017:   public void run () {
00018:     runtest (x.minus (zero).eq (x), true);
00019:     runtest (x.minus (x).eq (zero), true);
00020:     runtest (x.plus (y).minus (y).eq (x), true);
00021:     runtest (x.plus (y).minus (x).eq (y), true);
00022:     runtest (x.minus (y).plus (y).eq (x), true);
00023:     runtest (x.minus (y.plus (z)).eq (x.minus (y).minus (z)), true);
00024:     runtest (x.gtr (x.minus (one)), false);
00025:     runtest (x.geq (x.minus (y)), false);
00026:     runtest (x.gtr (x.minus (y)), false);
00027:     runtest (x.eq (x.minus (y)), false);
00028:   }
00029:   
00030: }
00031:

BDDs: Util Code [22/22]

file:simplebdd/util/HashMap3.java [source] [doc-public] [doc-private]

00001: package simplebdd.util;
00002: 
00003: // An implementation of a hash table where each value has a composite key
00004: // generated from 3 objects.  Acts like the Java HashMap except that:
00005: //
00006: // a) None of the keys or values are allowed to be null
00007: // b) None of the values are allowed to be arrays.
00008: // c) It usees == rather than .equals to compare objects for equality.
00009: //
00010: // Hack hack hack for space efficiency...
00011: 
00012: import java.util.HashMap;
00013: 
00014: public class HashMap3 {
00015:   
00016:   Object[] values = new Object[128];
00017:   Object[] keys1 = new Object[128];
00018:   Object[] keys2 = new Object[128];
00019:   Object[] keys3 = new Object[128];
00020:   int size=0;
00021:   
00022:   public void put (Object key1, Object key2, Object key3, Object value) {
00023:     if (size > values.length) {
00024:       grow ();
00025:     }
00026:     putNoGrow (key1, key2, key3, value);
00027:   }
00028:   
00029:   public void grow () {
00030:     Object[] oldValues = this.values;
00031:     Object[] oldKeys1 = this.keys1;
00032:     Object[] oldKeys2 = this.keys2;
00033:     Object[] oldKeys3 = this.keys3;
00034:     this.values = new Object[oldValues.length * 2];
00035:     this.keys1 = new Object[oldValues.length * 2];
00036:     this.keys2 = new Object[oldValues.length * 2];
00037:     this.keys3 = new Object[oldValues.length * 2];
00038:     for (int i=0; i<oldValues.length; i++) {
00039:       if (oldValues[i] == null) { 
00040:         continue;
00041:       } else if (oldValues[i] instanceof Object[]) {
00042:         Object[] valuesBucket = (Object[])(oldValues[i]);
00043:         Object[] keys1Bucket = (Object[])(oldKeys1[i]);
00044:         Object[] keys2Bucket = (Object[])(oldKeys2[i]);
00045:         Object[] keys3Bucket = (Object[])(oldKeys3[i]);
00046:         for (int j=0; j<valuesBucket.length; j++) {
00047:           if (valuesBucket[j] == null) {
00048:             break;
00049:           }
00050:           putNoGrow (keys1Bucket[j], keys2Bucket[j], keys3Bucket[j], valuesBucket[j]);
00051:         }
00052:       } else {
00053:         putNoGrow (oldKeys1[i], oldKeys2[i], oldKeys3[i], oldValues[i]);
00054:       }
00055:     }
00056:   }
00057:   
00058:   public void putNoGrow (Object key1, Object key2, Object key3, Object value) {
00059:     size++;
00060:     int hash = hash3 (key1, key2, key3) % values.length;
00061:     if (values[hash] == null) { 
00062:       keys1[hash] = key1;
00063:       keys2[hash] = key2;
00064:       keys3[hash] = key3;
00065:       values[hash] = value;
00066:       return;
00067:     } else if (values[hash] instanceof Object[]) {
00068:       Object[] valuesBucket = (Object[])(values[hash]);
00069:       Object[] keys1Bucket = (Object[])(keys1[hash]);
00070:       Object[] keys2Bucket = (Object[])(keys2[hash]);
00071:       Object[] keys3Bucket = (Object[])(keys3[hash]);
00072:       for (int i=0; i<valuesBucket.length; i++) {
00073:         if (valuesBucket[i] == null) {
00074:           keys1Bucket[i] = key1;
00075:           keys2Bucket[i] = key2;
00076:           keys3Bucket[i] = key3;
00077:           valuesBucket[i] = value;
00078:           return;
00079:         }
00080:       }
00081:       Object[] newValuesBucket = new Object[valuesBucket.length * 2];
00082:       Object[] newKeys1Bucket = new Object[valuesBucket.length * 2];
00083:       Object[] newKeys2Bucket = new Object[valuesBucket.length * 2];
00084:       Object[] newKeys3Bucket = new Object[valuesBucket.length * 2];
00085:       for (int i=0; i<valuesBucket.length; i++) {
00086:         newValuesBucket[i] = valuesBucket[i];
00087:         newKeys1Bucket[i] = keys1Bucket[i];
00088:         newKeys2Bucket[i] = keys2Bucket[i];
00089:         newKeys3Bucket[i] = keys3Bucket[i];
00090:       }
00091:       newValuesBucket[valuesBucket.length] = value;
00092:       newKeys1Bucket[valuesBucket.length] = key1;
00093:       newKeys2Bucket[valuesBucket.length] = key2;
00094:       newKeys3Bucket[valuesBucket.length] = key3;
00095:       values[hash] = newValuesBucket;
00096:       keys1[hash] = newKeys1Bucket;
00097:       keys2[hash] = newKeys2Bucket;
00098:       keys3[hash] = newKeys3Bucket;
00099:       return;
00100:     } else {
00101:       values[hash] = new Object[]{ values[hash], value };
00102:       keys1[hash] = new Object[]{ keys1[hash], key1 };
00103:       keys2[hash] = new Object[]{ keys2[hash], key2 };
00104:       keys3[hash] = new Object[]{ keys3[hash], key3 };
00105:       return;
00106:     }
00107:   }
00108:   
00109:   public Object get (Object key1, Object key2, Object key3) {
00110:     int hash = hash3 (key1, key2, key3) % values.length;
00111:     if (values[hash] == null) { 
00112:       return null;
00113:     } else if (values[hash] instanceof Object[]) {
00114:       Object[] valuesBucket = (Object[])(values[hash]);
00115:       Object[] keys1Bucket = (Object[])(keys1[hash]);
00116:       Object[] keys2Bucket = (Object[])(keys2[hash]);
00117:       Object[] keys3Bucket = (Object[])(keys3[hash]);
00118:       for (int i=0; i<valuesBucket.length; i++) {
00119:         if (keys1Bucket[i] == key1
00120:             && keys2Bucket[i] == key2
00121:             && keys3Bucket[i] == key3) {
00122:           return valuesBucket[i];
00123:         }
00124:       }
00125:       return null;
00126:     } else if (keys1[hash] == key1
00127:                && keys2[hash] == key2
00128:                && keys3[hash] == key3) {
00129:       return values[hash];
00130:     } else {
00131:       return null;
00132:     }
00133:   }
00134:   
00135:   public int hash3 (Object key1, Object key2, Object key3) {
00136:     return key1.hashCode () + 5 * key2.hashCode () + 13 * key3.hashCode ();
00137:   }
00138:   
00139: }
00140:

Revised: 2006/04/20 17:16