improve for syntax

commenting

Author: ailrst

src/main/scala/ir/dsl/DSL.scala

@@ -185,11 +185,6 @@ def ret(params: (String, Expr)*): EventuallyReturn = EventuallyReturn(params)
 
 def unreachable: EventuallyUnreachable = EventuallyUnreachable()
 
-case class Call(target: String, actualParams: (String, Expr)*)
-
-def directCall(lhs: Iterable[(String, Variable)], rhs: Call): EventuallyCall =
-  EventuallyCall(DelayNameResolve(rhs.target), lhs.toArray, rhs.actualParams)
-
 def directCall(lhs: Iterable[(String, Variable)], tgt: String, actualParams: (String, Expr)*): EventuallyCall =
   EventuallyCall(DelayNameResolve(tgt), lhs.toArray, actualParams)
 
@@ -255,6 +250,9 @@ def block(label: String, sl: (NonCallStatement | EventuallyStatement | Eventuall
   EventuallyBlock(label, statements, rjump)
 }
 
+/**
+ * Construct a block from a list of statements with a default name.
+ */
 def stmts(sl: (EventuallyCall | NonCallStatement | EventuallyStatement | EventuallyJump)*): EventuallyBlock = {
 
   val stmts =
@@ -372,165 +370,6 @@ case class EventuallyProgram(
   def cloneable = this.copy(mainProcedure = mainProcedure.cloneable, otherProcedures = otherProcedures.map(_.cloneable))
 }
 
-object Counter {
-  var count = 1
-  def next() = {
-    count += 1
-    count
-  }
-
-  def nlabel(name: String = "id"): String = {
-    name + "_" + next()
-  }
-}
-
-extension (i: EventuallyBlock)
-  @targetName("sequenceblocklist")
-  infix def `;`(j: List[EventuallyBlock]): List[EventuallyBlock] = sequence(List(i), j)
-
-extension (i: List[EventuallyBlock])
-  @targetName("sequenceblocklist")
-  infix def `;`(j: List[EventuallyBlock]): List[EventuallyBlock] = sequence(i, j)
-
-def sequence(first: List[EventuallyBlock], rest: List[EventuallyBlock]): List[EventuallyBlock] = {
-  require(first.nonEmpty)
-  require(rest.nonEmpty)
-  require(first.last.j.isInstanceOf[EventuallyUnreachable])
-  val last = first.last
-  last.j = goto(rest.head.label)
-  first ++ rest
-}
-
-def blocks(blocks: List[EventuallyBlock]*): List[EventuallyBlock] = {
-  blocks.toList match {
-    case Nil => List()
-    case h :: Nil => h
-    case h :: tail => tail.foldLeft(h)((acc, nextb) => sequence(acc, nextb))
-  }
-
-}
-
-def setSuccIfUndef(first: List[EventuallyBlock], rest: EventuallyBlock*) = {
-  require(first.nonEmpty)
-  require(rest.nonEmpty)
-
-  if (first.last.j.isInstanceOf[EventuallyUnreachable]) {
-    val last = first.last
-    last.j = goto(rest.head.label)
-  }
-  first
-}
-
-//def While(cond: Expr, body: EventuallyBlock*): List[EventuallyBlock] = {
-//  While(cond, body.toList)
-//}
-
-def For(
-  init: List[EventuallyBlock],
-  cond: Expr,
-  after: List[EventuallyBlock],
-  body: List[EventuallyBlock]
-): List[EventuallyBlock] = {
-  require(after.nonEmpty)
-  require(init.nonEmpty)
-  val internal = sequence(body, after)
-  val loop = While(cond) Do (internal)
-  sequence(init, loop)
-}
-
-//def For(init: EventuallyBlock, cond: Expr, after: EventuallyBlock, body: EventuallyBlock*): List[EventuallyBlock] = {
-//  For(List(init), cond, List(after), body.toList)
-//}
-//
-//def For(init: NonCallStatement, cond: Expr, after: NonCallStatement, body: EventuallyBlock*): List[EventuallyBlock] = {
-//  require(body.nonEmpty)
-//  For(List(stmts(init)), cond, List(stmts(after)), body.toList)
-//}
-//def For(
-//  init: NonCallStatement,
-//  cond: Expr,
-//  after: NonCallStatement,
-//  body: List[EventuallyBlock]
-//): List[EventuallyBlock] = {
-//  For(List(stmts(init)), cond, List(stmts(after)), body.toList)
-//}
-
-case class WhileDo(cond: Expr) {
-  def Do(body: Iterable[EventuallyBlock]) = While(cond, (body.toList))
-  @targetName("doBlocks")
-  def Do(body: EventuallyBlock*) = While(cond, (body.toList))
-  @targetName("doStatements")
-  def Do(sl: (EventuallyCall | NonCallStatement | EventuallyStatement | EventuallyJump)*) =
-    While(cond, (List(stmts(sl: _*))))
-}
-
-def While(cond: Expr) = WhileDo(cond)
-
-def While(cond: Expr, body: List[EventuallyBlock]): List[EventuallyBlock] = {
-  val loopExit = Counter.nlabel("while_exit")
-  val loopBackedge = Counter.nlabel("while_backedge")
-  val loopEntry = Counter.nlabel("while_entry")
-  val loopBody = Counter.nlabel("while_body")
-  List(block(loopEntry, goto(loopBody, loopExit)))
-    ++
-      sequence(sequence(List(block(loopBody, Assume(cond))), body), List(block(loopBackedge, goto(loopEntry))))
-      ++
-      List(block(loopExit, Assume(UnaryExpr(BoolNOT, cond)), unreachable))
-}
-
-case class ThenV(cond: Expr, body: List[EventuallyBlock]) {
-  def Else(els: Iterable[EventuallyBlock]): List[EventuallyBlock] = If(cond, body, els.toList)
-  def Else(els: EventuallyBlock*): List[EventuallyBlock] = If(cond, body, els.toList)
-  @targetName("elseStatements")
-  def Else(els: (NonCallStatement | EventuallyStatement | EventuallyJump)*): List[EventuallyBlock] =
-    If(cond, body, List(stmts(els: _*)))
-}
-
-case class ElseV(cond: Expr, thenBody: List[EventuallyBlock], body: List[EventuallyBlock])
-
-given IfThenBlocks: Conversion[ThenV, List[EventuallyBlock]] with
-  def apply(x: ThenV): List[EventuallyBlock] = If(x.cond, x.body, List())
-
-given StmtList
-  : Conversion[EventuallyCall | NonCallStatement | EventuallyStatement | EventuallyJump, List[EventuallyBlock]] with
-  def apply(x: EventuallyCall | NonCallStatement | EventuallyStatement | EventuallyJump): List[EventuallyBlock] = List(
-    stmts(x)
-  )
-
-given BlockList: Conversion[EventuallyBlock, List[EventuallyBlock]] with
-  def apply(b: EventuallyBlock) = List(b)
-
-case class IfThen(cond: Expr) {
-  def Then(body: Iterable[EventuallyBlock]): ThenV = ThenV(cond, body.toList)
-  def Then(body: EventuallyBlock*): ThenV = ThenV(cond, body.toList)
-  @targetName("thenStatements")
-  def Then(body: (NonCallStatement | EventuallyStatement | EventuallyJump)*): ThenV = ThenV(cond, List(stmts(body: _*)))
-
-}
-
-def If(cond: Expr) = IfThen(cond)
-
-def If(cond: Expr, ifThen: List[EventuallyBlock], ifElse: List[EventuallyBlock]): List[EventuallyBlock] = {
-  val ifEntry = Counter.nlabel("if_entry")
-  val thenCase = Counter.nlabel("if_then")
-  val elseCase = Counter.nlabel("if_else")
-  val ifExit = Counter.nlabel("if_exit")
-
-  val thenNonempty =
-    if (ifThen.isEmpty) then List(block(Counter.nlabel("if_then_empty"), unreachable)) else ifThen
-  val elseNonempty =
-    if (ifElse.isEmpty) then List(block(Counter.nlabel("if_else_empty"), unreachable)) else ifElse.toList
-
-  val exitBlock = block(ifExit, unreachable)
-  val thenBlocks = setSuccIfUndef(thenNonempty, exitBlock)
-  val elseBlocks = setSuccIfUndef(elseNonempty, exitBlock)
-
-  List(block(ifEntry, goto(thenCase, elseCase)))
-    ++ sequence(List(block(thenCase, Assume(cond), unreachable)), thenBlocks)
-    ++ sequence(List(block(elseCase, Assume(UnaryExpr(BoolNOT, cond)), unreachable)), elseBlocks)
-    ++ List(exitBlock)
-}
-
 def prog(mainProc: EventuallyProcedure, procedures: EventuallyProcedure*): Program =
   prog(Seq(), mainProc, procedures: _*)
 
@@ -554,170 +393,3 @@ def progUnresolved(
   procedures: EventuallyProcedure*
 ): EventuallyProgram =
   EventuallyProgram(mainProc, procedures, initialMemory)
-
-  /**
-   * Expr construction
-   */
-
-extension (lvar: Variable)
-  infix def :=(j: Expr) = LocalAssign(lvar, j)
-  def :=(j: Int) = lvar.getType match {
-    case BitVecType(sz) => LocalAssign(lvar, BitVecLiteral(j, sz))
-    case IntType => LocalAssign(lvar, IntLiteral(j))
-    case _ => ???
-  }
-  def :=(j: Boolean) = lvar.getType match {
-    case BoolType => LocalAssign(lvar, if j then TrueLiteral else FalseLiteral)
-    case _ => ???
-  }
-
-extension (lvar: List[(String, Variable)]) infix def :=(j: Call) = directCall(lvar, j)
-extension (lvar: Seq[(String, Variable)]) infix def :=(j: Call) = directCall(lvar, j)
-
-extension (v: Int)
-  @targetName("ibv64")
-  def bv64 = BitVecLiteral(v, 64)
-  @targetName("ibv32")
-  def bv32 = BitVecLiteral(v, 32)
-  @targetName("ibv16")
-  def bv16 = BitVecLiteral(v, 16)
-  @targetName("ibv8")
-  def bv8 = BitVecLiteral(v, 8)
-  @targetName("ibv1")
-  def bv1 = BitVecLiteral(v, 1)
-  @targetName("itobv")
-  def bv(sz: Int) = BitVecLiteral(v, sz)
-
-def bv64 = BitVecType(64)
-def bv32 = BitVecType(32)
-def bv16 = BitVecType(16)
-def bv8 = BitVecType(8)
-def bv1 = BitVecType(1)
-
-extension (i: Expr)
-  infix def ===(j: Expr): Expr = i.getType match {
-    case IntType => BinaryExpr(IntEQ, i, j)
-    case b: BitVecType => BinaryExpr(BVEQ, i, j)
-    case BoolType => BinaryExpr(BoolEQ, i, j)
-    case m: MapType => ???
-  }
-  infix def !==(j: Expr): Expr = i.getType match {
-    case IntType => BinaryExpr(IntNEQ, i, j)
-    case b: BitVecType => BinaryExpr(BVNEQ, i, j)
-    case BoolType => BinaryExpr(BoolNEQ, i, j)
-    case m: MapType => ???
-  }
-  infix def +(j: Expr): Expr = i.getType match {
-    case IntType => BinaryExpr(IntADD, i, j)
-    case b: BitVecType => BinaryExpr(BVADD, i, j)
-    case BoolType => BinaryExpr(BoolOR, i, j)
-    case m: MapType => ???
-  }
-  infix def -(j: Expr): Expr = i.getType match {
-    case IntType => BinaryExpr(IntSUB, i, j)
-    case b: BitVecType => BinaryExpr(BVSUB, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def *(j: Expr): Expr = i.getType match {
-    case IntType => BinaryExpr(IntMUL, i, j)
-    case b: BitVecType => BinaryExpr(BVMUL, i, j)
-    case BoolType => BinaryExpr(BoolAND, i, j)
-    case m: MapType => ???
-  }
-  infix def /(j: Expr): Expr = i.getType match {
-    case IntType => BinaryExpr(IntDIV, i, j)
-    case b: BitVecType => BinaryExpr(BVSDIV, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def &&(j: Expr): Expr = i.getType match {
-    case IntType => ???
-    case b: BitVecType => BinaryExpr(BVAND, i, j)
-    case BoolType => BinaryExpr(BoolAND, i, j)
-    case m: MapType => ???
-  }
-  infix def ||(j: Expr): Expr = i.getType match {
-    case IntType => ???
-    case b: BitVecType => BinaryExpr(BVOR, i, j)
-    case BoolType => BinaryExpr(BoolOR, i, j)
-    case m: MapType => ???
-  }
-  infix def <<(j: Expr): Expr = i.getType match {
-    case IntType => ???
-    case b: BitVecType => BinaryExpr(BVSHL, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def >>(j: Expr): Expr = i.getType match {
-    case IntType => ???
-    case b: BitVecType => BinaryExpr(BVASHR, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def >>>(j: Expr): Expr = i.getType match {
-    case IntType => ???
-    case b: BitVecType => BinaryExpr(BVLSHR, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def %(j: Expr): Expr = i.getType match {
-    case IntType => BinaryExpr(IntMOD, i, j)
-    case b: BitVecType => BinaryExpr(BVSMOD, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def <(j: Expr): Expr = i.getType match {
-    case IntType => BinaryExpr(IntLT, i, j)
-    case b: BitVecType => BinaryExpr(BVSLT, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def >(j: Expr): Expr = i.getType match {
-    case IntType => BinaryExpr(IntGT, i, j)
-    case b: BitVecType => BinaryExpr(BVSGT, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def <=(j: Expr): Expr = i.getType match {
-    case IntType => BinaryExpr(IntLE, i, j)
-    case b: BitVecType => BinaryExpr(BVSLE, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def >=(j: Expr): Expr = i.getType match {
-    case IntType => BinaryExpr(IntGE, i, j)
-    case b: BitVecType => BinaryExpr(BVSGE, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def ult(j: Expr): Expr = i.getType match {
-    case IntType => ???
-    case b: BitVecType => BinaryExpr(BVULT, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def ugt(j: Expr): Expr = i.getType match {
-    case IntType => ???
-    case b: BitVecType => BinaryExpr(BVUGT, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def ule(j: Expr): Expr = i.getType match {
-    case IntType => ???
-    case b: BitVecType => BinaryExpr(BVULE, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def uge(j: Expr): Expr = i.getType match {
-    case IntType => ???
-    case b: BitVecType => BinaryExpr(BVUGE, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }
-  infix def ++(j: Expr): Expr = i.getType match {
-    case IntType => ???
-    case b: BitVecType => BinaryExpr(BVCONCAT, i, j)
-    case BoolType => ???
-    case m: MapType => ???
-  }