ThreeCounterAbstractInterpretation.scala

package abstr.interpretation

import scala.annotation.tailrec
import scala.util.parsing.combinator.RegexParsers

sealed trait ParityDomain {
  def join(p: ParityDomain): ParityDomain = ParityDomain.join(this, p)
}
case object Bottom extends ParityDomain
case object Top extends ParityDomain
case object Odd extends ParityDomain
case object Even extends ParityDomain

object ParityDomain {
  val bot = Bottom
  val leq: (ParityDomain, ParityDomain) => Boolean = {
    case (Bottom, _) => true
    case (_, Top) => true
    case _ => false
  }
  val join: (ParityDomain, ParityDomain) => ParityDomain = {
    case (Bottom, a) => a
    case (a, Bottom) => a
    case (a, b) if a == b => a
    case _ => Top
  }
  val iszero: ParityDomain => ParityDomain = {
    case Bottom | Odd => Bottom
    case _ => Even
  }
  val notzero: ParityDomain => ParityDomain = identity
  val incr: ParityDomain => ParityDomain = {
    case Even => Odd
    case Odd => Even
    case a => a
  }
  val decr: ParityDomain => ParityDomain = incr
}

sealed trait Operation
case class Inc(v: Var) extends Operation
case class Dec(v: Var) extends Operation
case class Zero(test: Var, th: Int, el: Int) extends Operation
case object Stop extends Operation

sealed trait Var
case object X extends Var
case object Y extends Var
case object Z extends Var

object LineParser extends RegexParsers {
  val VAR: Parser[Var] = "x" ^^ {_ => X} | "y" ^^ {_ => Y} | "z" ^^ {_ => Z}
  val inc: Parser[Operation] = "inc" ~> VAR ^^ Inc
  val dec: Parser[Operation] = "dec" ~> VAR ^^ Dec
  val line: Parser[Int] = """\d+""".r ^^ {_.toInt}
  val zero: Parser[Operation] = "zero" ~> VAR ~ line ~ ("else" ~> line) ^^ {
    case v ~ th ~ e => Zero(v, th, e)
  }
  val stop: Parser[Operation] = "stop" ^^ {_ => Stop}

  val expression: Parser[Operation] = inc | dec | zero | stop

  def parse(s: String): Operation = {
    try {
      LineParser.parse(LineParser.expression, s).get
    }
    catch {
      case _: Throwable =>
        println(s"error for $s")
        Stop
    }
  }
}

object ThreeCounterAnalyzer {
  def main(args: Array[String]) {
    val program =
      """
        |inc z
        |zero z 3 else 4
        |inc y
        |dec z
        |stop
      """.stripMargin.trim
    val programLines = program.lines.filter(_.nonEmpty).toSeq
    val operationList = programLines.map(LineParser.parse)

    type ParityTriple = (ParityDomain, ParityDomain, ParityDomain)
    def join(p1: ParityTriple, p2: ParityTriple): ParityTriple = {
      (p1._1 join p2._1, p1._2 join p2._2, p1._3 join p2._3)
    }

    val bottom: Map[Int, ParityTriple] = (1 to operationList.length).map((_, (Bottom, Bottom, Bottom))).toMap

    def iterate(map: Map[Int, ParityTriple]): Map[Int, ParityTriple] = {
      var res = bottom
      def update(index: Int, joinValue: ParityTriple): Unit = {
        res = res.updated(index, join(joinValue, res(index)))
      }
      update(1, (Top, Even, Even))
      for (i <- 1 to operationList.length) {
        operationList(i - 1) match {
          case Inc(X) => update(i + 1, map(i).copy(_1 = ParityDomain.incr(map(i)._1)))
          case Inc(Y) => update(i + 1, map(i).copy(_2 = ParityDomain.incr(map(i)._2)))
          case Inc(Z) => update(i + 1, map(i).copy(_3 = ParityDomain.incr(map(i)._3)))
          case Dec(X) => update(i + 1, map(i).copy(_1 = ParityDomain.decr(map(i)._1)))
          case Dec(Y) => update(i + 1, map(i).copy(_2 = ParityDomain.decr(map(i)._2)))
          case Dec(Z) => update(i + 1, map(i).copy(_3 = ParityDomain.decr(map(i)._3)))
          case Zero(X, th, el) =>
            update(th, map(i).copy(_1 = ParityDomain.iszero(map(i)._1)))
            update(el, map(i).copy(_1 = ParityDomain.notzero(map(i)._1)))
          case Zero(Y, th, el) =>
            update(th, map(i).copy(_2 = ParityDomain.iszero(map(i)._2)))
            update(el, map(i).copy(_2 = ParityDomain.notzero(map(i)._2)))
          case Zero(Z, th, el) =>
            update(th, map(i).copy(_3 = ParityDomain.iszero(map(i)._3)))
            update(el, map(i).copy(_3 = ParityDomain.notzero(map(i)._3)))
          case Stop => //do nothing
        }
      }
      res
    }

    var map: Map[Int, ParityTriple] = (1 to operationList.length).map((_, (Bottom, Bottom, Bottom))).toMap
    var nextMap = iterate(map)

    def printMap(): Unit = {
      for (i <- 1 to operationList.length) {
        val p = map(i)
        println(f"$i: ${programLines(i - 1)}%-20s {x: ${p._1.toString}, y: ${p._2.toString}, z: ${p._3.toString}}")
      }
    }
    while (map != nextMap) {
      map = nextMap
      nextMap = iterate(nextMap)
    }
    printMap()
  }
}