LARA

object Signs {
 
  // A 5-element abstraction of sets of integers
  sealed abstract class Sign
  case object TopSign extends Sign    // all integers
  case object BottomSign extends Sign // {}
  case object Positive extends Sign   // {1,2,3,...}
  case object Zero extends Sign       // {0}
  case object Negative extends Sign   // {...,-3,-2,-1}
 
  class SignLattice extends Lattice { // Sign as a lattice
    type Elem = Sign
    val top = TopSign        // universal set is top
    val bottom = BottomSign  // empty set is bottom
    def leq(x : Sign, y : Sign) : Boolean = (x,y) match {
      case (BottomSign,_) => true  // empty set subset of all
      case (_,TopSign) => true     // full set superset of all
      case _ if x==y => true       // lattice order is reflexive
      case _ => false              // others turn out to be incomparable 
    }
    def join(x : Sign, y : Sign) : Sign = (x,y) match {
      case (BottomSign,_) => y  // bottom is neutral
      case (_,BottomSign) => x  //   and join is commutative
      case _ if x==y => x       // join is idempotent
      case _ => TopSign         // this lattice is very shallow; we get top easily
    }
    def meet(x : Sign, y : Sign) : Sign = (x,y) match {
      case (TopSign,_) => y  // dual to join
      case (_,TopSign) => x
      case _ if x==y => x
      case _ => BottomSign
    }
  }
 
  import SimpleCFG._
 
  // Compute effect of statements on lattice elements.
  //   This is the key part of abstract interpreter
  object SignTransFun extends TransferFunction[Map[Variable,Sign], CfgStmt] {
    def apply(node : CfgStmt, fact : Map[Variable,Sign]) : Map[Variable,Sign] = {
      def value(x : SimpleValue) : Sign = x match {
	case Const(c) => {
	  if (c < 0) Negative
	  else if (c > 0) Positive
	  else Zero
	}
	case VarValue(v) => fact(v)
      }
      val res =
	node match {
	  case AssignBin(res,x,op,y) => fact.update(res, evalOp(op,value(x),value(y)))
	  case Copy(res,x) => fact.update(res, value(x))
	  case Assume(x,rop,y) => {
	    if (evalOp(rop, value(x), value(y)) == Zero) 
	      Map[Variable,Sign]().withDefaultValue(BottomSign)
	    else fact
	  }
	  case Print(x) => fact
	  case Skip => fact
	}
      res
    }
    def evalOp(op : SimpleCFG.Operation, x : Sign, y : Sign) : Sign = op match {
      case PlusOp => (x,y) match {
	case (_,BottomSign) => BottomSign
	case (BottomSign,_) => BottomSign
	case (TopSign,_) => TopSign
	case (_,TopSign) => TopSign
	case (Zero,_) => y
	case (_,Zero) => x
	case (Positive,Positive) => Positive
	case (Negative,Negative) => Negative
	case (Positive,Negative) => TopSign
	case (Negative,Positive) => TopSign
      }
      case ArithOp() => error("this was to make type checker happy")
      case EqOp => (x,y) match {
	case (_,BottomSign) => BottomSign
	case (BottomSign,_) => BottomSign
	case (Zero,Zero) => Positive /* concrete semantics gives 1 */
	case (Zero,Positive) => Zero /* cannot be equal, concrete gives 0 */
	case (Positive,Zero) => Zero 
	case (Negative,Zero) => Zero
	case (Zero,Negative) => Zero
	case (Positive,Negative) => Zero
	case (Negative,Positive) => Zero
	case (_,_) => TopSign /* who knows, e.g. two positive cound be same or not */
      }
      case NeqOp => (x,y) match {
	case (_,BottomSign) => BottomSign
	case (BottomSign,_) => BottomSign
	case (Zero,Zero) => Zero
	case (Zero,Positive) => Positive
	case (Positive,Zero) => Positive
	case (Negative,Zero) => Positive
	case (Zero,Negative) => Positive
	case (Positive,Negative) => Positive
	case (Negative,Positive) => Positive
	case (_,_) => TopSign 
      }
      case LeqOp => (x,y) match {
	case (_,BottomSign) => BottomSign
	case (BottomSign,_) => BottomSign
	case (Zero,Zero) => Positive /* concrete semantics gives 1 */
	case (Zero,Positive) => Positive
	case (Negative,Zero) => Positive
	case (Negative,Positive) => Positive
	case (Positive,Zero) => Zero /* cannot hold */
	case (Zero,Negative) => Zero
	case (Positive,Negative) => Zero
	case (_,_) => TopSign /* who knows */
      }
      case LTOp => (x,y) match {
	case (_,BottomSign) => BottomSign
	case (BottomSign,_) => BottomSign
	case (Zero,Zero) => Zero
	case (Zero,Positive) => Positive
	case (Negative,Zero) => Positive
	case (Negative,Positive) => Positive
	case (Positive,Zero) => Zero
	case (Zero,Negative) => Zero
	case (Positive,Negative) => Zero
	case (_,_) => TopSign 
      }
    }
  }
 
  val signLattice = new SignLattice
  class PSignLattice(domain : Set[Variable]) extends 
    PointwiseLattice[Variable, Sign, SignLattice](signLattice, domain)
}
 
// It works!
import SimpleAST._
import SimpleCFG._
import Signs._
object SignTest {
  def main(args : Array[String]) {
    val body = BlockStat(List(AssignStat("j", Plus(Var("i"), IntConst(42))),
			      AssignStat("i", Plus(Var("j"), IntConst(+40)))))
    val stat2 =
      BlockStat(List(
	AssignStat("i", IntConst(1)),
	WhileStat(Leq(Var("i"), IntConst(9)),
		  body),
	AssignStat("res", Var("j"))))
    val cfg = new Cfg
    new ASTtoCFG(cfg).translate(stat2)
    cfg.dottyView
    val pSignLattice = new PSignLattice(Set("i","j","res"))
    val alg = new AnalysisAlgoritm[pSignLattice.Elem,CfgStmt](SignTransFun, 
							      pSignLattice, cfg)
    alg.init
    val initialState : pSignLattice.Elem =
      Map("i" -> Zero, "j" -> Zero, "res" -> Zero)
    alg.setNodeFact(cfg.entry, initialState)
    print(alg.facts)
    alg.computeFixpoint
    val res = alg.getResult
    println(res)
    println("\nEXIT: " + res(cfg.exit))
  }
}