# 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)
}
}```