LARA

// Lattice of concrete executions of integer programs
object ConcreteLattice extends Lattice {
  type State = Map[String,Int] // specific to this particular example
  type Elem = Set[State]
  def leq(x : Elem, y : Elem) : Boolean = x.subsetOf(y)
  val bottom = Set[State]()
  lazy val top = error("lattice element too big to compute")
  def join(x : Elem, y : Elem) = (x ++ y) // union
  def meet(x : Elem, y : Elem) = (x ** y) // intersection
}
 
import SimpleCFG._
object ConcreteTransFun extends 
       TransferFunction[ConcreteLattice.Elem, CfgStmt] {
  def apply(node : CfgStmt, states : ConcreteLattice.Elem) : ConcreteLattice.Elem = {
     states.flatMap(execute(node,_))
  }
  def evalOp(op : SimpleCFG.Operation, x : Int, y : Int) : Int = op match {
    case PlusOp => x+y
    case ArithOp() => error("this was to make type checker happy")
    case EqOp => {if (x==y) 1 else 0}
    case NeqOp => {if (x!=y) 1 else 0}
    case LeqOp => {if (x<=y) 1 else 0}
    case LTOp => {if (x<y) 1 else 0}
  }
 
  def execute(node : CfgStmt, s : ConcreteLattice.State) : Set[ConcreteLattice.State] = {  
    def value(x : SimpleValue) : Int = x match {
      case Const(c) => c
      case VarValue(v) => s(v)
    }
    node match {
      case AssignBin(res,x,op,y) => 
	Set(s.update(res, evalOp(op,value(x),value(y))))
      case Copy(res,x) => Set(s.update(res, value(x)))
      case Assume(x,rop,y) => { 
	if (evalOp(rop, value(x), value(y)) != 0)   Set(s)
	else Set()
      }
      case Print(x) => { println(value(x)); Set(s) }
      case Skip => Set(s)
    }
  }
}
 
import SimpleAST._
object ExecutionTest {
  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(0)),
	WhileStat(Leq(Var("i"), IntConst(9)),
		  body),
	AssignStat("res", Var("j"))))
    val cfg = new Cfg
    new ASTtoCFG(cfg).translate(stat2)
    cfg.dottyView
    val alg = new AnalysisAlgoritm[ConcreteLattice.Elem,CfgStmt](ConcreteTransFun, 
								 ConcreteLattice, cfg)
    alg.init
    val initialState = Map[String,Int]().withDefaultValue(0)
    alg.setNodeFact(cfg.entry, Set(initialState))
    print(alg.facts)
    alg.computeFixpoint
    println(alg.getResult)
  }
}