trait PartialOrder { type Elem def leq(x : Elem, y : Elem) : Boolean // less than or equal } trait Lattice extends PartialOrder { val top : Elem // universal set val bottom : Elem // empty set def join(x : Elem, y : Elem) : Elem // union def meet(x : Elem, y : Elem) : Elem // intersection } // there should be more elegant definition--but make sure domain of results are correct class PointwiseLattice[I,E,L <: Lattice{type Elem=E}](base : L, domain : Set[I]) extends Lattice { type Elem=Map[I,E] def leq(x : Elem, y : Elem) : Boolean = domain.forall(i => base.leq(x(i),y(i))) val (top : Elem) = { var res = Map[I,E]() for (i <- domain) res = res.update(i, base.top) res } val (bottom : Elem) = { var res = Map[I,E]() for (i <- domain) res = res.update(i, base.bottom) res } def join(x : Elem, y : Elem) = { var res = Map[I,E]() for (i <- domain) res = res.update(i, base.join(x(i),y(i))) res } def meet(x : Elem, y : Elem) = { var res = Map[I,E]() for (i <- domain) res = res.update(i, base.meet(x(i),y(i))) res } } object InitalizationLattice extends Lattice { sealed abstract class InitStatus case object BottomStatus extends InitStatus case object Initialized extends InitStatus case object TopStatus extends InitStatus type Elem = InitStatus def leq(x : InitStatus, y : InitStatus) = (x,y) match { case (BottomStatus,_) => true case (_,TopStatus) => true case _ if x==y => true case _ => false } val top = TopStatus val bottom = BottomStatus def join(x : InitStatus, y : InitStatus) = (x,y) match { case (BottomStatus,_) => y case (_,BottomStatus) => x case _ if x==y => x case _ => TopStatus } def meet(x : InitStatus, y : InitStatus) = (x,y) match { case (TopStatus,_) => y case (_,TopStatus) => x case _ if x==y => x case _ => BottomStatus } } object ConstantPropagationLattice extends Lattice { sealed abstract class PointedConstant case object TopPoint extends PointedConstant case object BottomPoint extends PointedConstant case class Constant(c : Int) extends PointedConstant type Elem = PointedConstant def leq(x : PointedConstant, y : PointedConstant) = (x,y) match { case (BottomPoint,_) => true case (_,TopPoint) => true case (Constant(c1),Constant(c2)) => (c1==c2) case _ => false } val top = TopPoint val bottom = BottomPoint def join(x : PointedConstant, y : PointedConstant) = (x,y) match { case (BottomPoint,_) => y case (_,BottomPoint) => x case _ if x==y => x case _ => TopPoint } def meet(x : PointedConstant, y : PointedConstant) = (x,y) match { case (TopPoint,_) => y case (_,TopPoint) => x case _ if x==y => x case _ => BottomPoint } } object RangeLattice extends Lattice { sealed abstract class Range case object Empty extends Range // {} case class Bounded(a : Int, b : Int) extends Range // [a,b] { assert (a <= b) } case class LeftUnbounded(b : Int) extends Range // (-inf,b] case class RightUnbounded(a : Int) extends Range // [a,+inf) case object Full extends Range // (-inf,+inf) type Elem = Range def leq(x : Range, y : Range) = (x,y) match { case (Empty,_) => true case (_,Full) => true case (Bounded(a1,b1),Bounded(a2,b2)) => (a2 <= a1 && b1 <= b2) // a2...a1...b1...b2 case (Bounded(a1,b1),LeftUnbounded(b2)) => (b1 <= b2) case (Bounded(a1,b1),RightUnbounded(a2)) => (a2 <= a1) case (LeftUnbounded(b1),LeftUnbounded(b2)) => (b1 <= b2) case (RightUnbounded(a1),RightUnbounded(a2)) => (a2 <= a1) case _ => false } val top = Full val bottom = Empty def join(x : Range, y : Range) = { import Math.{min,max} (x,y) match { case (Empty,_) => y case (_,Empty) => x case (Full,_) => Full case (_,Full) => Full case (Bounded(a1,b1),Bounded(a2,b2)) => Bounded(min(a1,a2), max(b1,b2)) case (LeftUnbounded(b1),LeftUnbounded(b2)) => LeftUnbounded(max(b1,b2)) case (RightUnbounded(a1),RightUnbounded(a2)) => RightUnbounded(min(a1,a2)) case (LeftUnbounded(_),RightUnbounded(_)) => Full case (RightUnbounded(_),LeftUnbounded(_)) => Full case (Bounded(a1,b1),LeftUnbounded(b2)) => LeftUnbounded(max(b1,b2)) case (LeftUnbounded(b2),Bounded(a1,b1)) => LeftUnbounded(max(b1,b2)) case (Bounded(a1,b1),RightUnbounded(a2)) => RightUnbounded(min(a1,a2)) case (RightUnbounded(a2),Bounded(a1,b1)) => RightUnbounded(min(a1,a2)) } } def meet(x : Range, y : Range) = { import Math.{min,max} (x,y) match { case (Empty,_) => Empty case (_,Empty) => Empty case (Full,_) => y case (_,Full) => x case (Bounded(a1,b1),Bounded(a2,b2)) => { val a = max(a1,a2) val b = min(b1,b2) if (a <= b) Bounded(a,b) else Empty } case (LeftUnbounded(b1),LeftUnbounded(b2)) => LeftUnbounded(min(b1,b2)) case _ => error("PLEASE COMPLETE") } } } object LatticeCombination { def product(first : Lattice, second : Lattice) : Lattice = new Lattice { type Elem = (first.Elem, second.Elem) def leq(x : Elem, y : Elem) : Boolean = first.leq(x._1,y._1) && second.leq(x._2,y._2) val top = (first.top, second.top) val bottom = (first.bottom, second.bottom) def join(x : Elem, y : Elem) : Elem = (first.join(x._1,y._1), second.join(x._2,y._2)) def meet(x : Elem, y : Elem) : Elem = (first.meet(x._1,y._1), second.meet(x._2,y._2)) } def mapPower[T](m : Map[T,Lattice]) : Lattice = new Lattice { type Elem = Map[T,Any] def leq(x : Elem, y : Elem) : Boolean = { def leqAt(t:T, lat : Lattice) : Boolean = { type e = lat.Elem lat.leq(x(t).asInstanceOf[e], y(t).asInstanceOf[e]) } m.transform(leqAt).forall(_._2) } val (top : Elem) = { def topAt(t : T, lat : Lattice) : Any = { lat.top } m.transform(topAt) } val (bottom : Elem) = { def bottomAt(t : T, lat : Lattice) : Any = { lat.bottom } m.transform(bottomAt) } def join(x : Elem, y : Elem) = { def joinAt(t : T, lat : Lattice) : Any = { type e = lat.Elem lat.join(x(t).asInstanceOf[e], y(t).asInstanceOf[e]) } m.transform(joinAt) } def meet(x : Elem, y : Elem) = { def meetAt(t : T, lat : Lattice) : Any = { type e = lat.Elem lat.meet(x(t).asInstanceOf[e], y(t).asInstanceOf[e]) } m.transform(meetAt) } } }