Merge branch 'main' into grammar-update2

scripts/format_adt.py

@@ -40,7 +40,7 @@
 notspace_re = re.compile(rb'\S')
 head_re = re.compile(rb'[^\s(]+')
 num_re = re.compile(rb'[_0-9xa-fA-F]+')
-string_re = re.compile(rb'"(?:[^"\\]|\\.)*"')
+string_re = re.compile(rb'''"(?:[^"\\]|\\.)*"|'(?:[^'\\]|\\.)*\'''')
 
 @dataclasses.dataclass
 class Context:
@@ -79,8 +79,8 @@ def pretty(outfile, data: bytes, spaces: int):
       assert m
       outfile.write(m[0])
       i = m.end(0)
-    elif c == b',':
-      outfile.write(b',')
+    elif c in b',;':
+      outfile.write(c)
       i += 1
       if stack[-1].multiline:
         outfile.write(b'\n')
@@ -97,11 +97,14 @@ def pretty(outfile, data: bytes, spaces: int):
       outfile.write(c)
       i += 1
       islist = c == b'[' and ']' != chr(data[i])
-      multiline = islist or head in (b'Project', b'Def', b'Goto', b'Call', b'Sub', b'Blk', b'Arg')
+      multiline = islist or head in (b'Project', b'Def', b'Goto', b'Call', b'Sub', b'Blk', b'Arg') or head.startswith(b'Stmt_') or head in (b'Expr_TApply', b'Expr_Slices')
       if multiline:
         depth += 1
-        outfile.write(b'\n')
-        outfile.write(indent * depth)
+        if islist and stack and stack[-1].multiline:
+          outfile.write(indent[1:])
+        else:
+          outfile.write(b'\n')
+          outfile.write(indent * depth)
 
       stack.append(Context(i, flip[c], multiline))
     elif c in b')]':
@@ -115,7 +118,7 @@ def pretty(outfile, data: bytes, spaces: int):
         depth -= 1
       if not stack:
         outfile.write(b'\n')
-    elif c == b'"':
+    elif c in b'"\'':
       string = string_re.match(data, i)
       if not string:
         raise ValueError(f"unclosed string beginning at byte {i+1}.")

src/main/scala/ir/IRCursor.scala

@@ -46,8 +46,8 @@ object IRWalk:
 
   def commandBegin(pos: CFGPosition) : Option[Command] = {
     pos match {
-      case p: Procedure => p.entryBlock.map(b => b.statements.headOption().getOrElse(b.jump))
-      case b: Block => Some(b.statements.headOption().getOrElse(b.jump))
+      case p: Procedure => p.entryBlock.map(b => b.statements.headOption.getOrElse(b.jump))
+      case b: Block => Some(b.statements.headOption.getOrElse(b.jump))
       case c: Command => Some(c)
     }
   }
@@ -81,7 +81,7 @@ trait IntraProcIRCursor extends IRWalk[CFGPosition, CFGPosition] {
   def succ(pos: CFGPosition): Set[CFGPosition] = {
     pos match {
       case proc: Procedure => proc.entryBlock.toSet
-      case b: Block        => Set(b.statements.headOption().getOrElse(b.jump))
+      case b: Block        => Set(b.statements.headOption.getOrElse(b.jump))
       case s: Statement    =>  Set(s.succ().getOrElse(s.parent.jump))
       case n: GoTo         => n.targets.asInstanceOf[Set[CFGPosition]]
       case c: Call         => c.parent.fallthrough.toSet

src/main/scala/ir/Program.scala

@@ -358,9 +358,8 @@ class Block private (
   statements.onInsert = x => x.setParent(this)
   statements.onRemove = x => x.deParent()
 
-
   def this(label: String, address: Option[Int] = None, statements: IterableOnce[Statement] = Set.empty, jump: Jump = GoTo(Set.empty)) = {
-    this(label, address, IntrusiveList.from(statements), jump,  mutable.HashSet.empty, None)
+    this(label, address, IntrusiveList().addAll(statements), jump, mutable.HashSet.empty, None)
   }
 
   def jump: Jump = _jump
@@ -377,7 +376,8 @@ class Block private (
     _fallthrough = g
   }
 
-  def jump_=(j: Jump): Unit = {
+  private def jump_=(j: Jump): Unit = {
+    require(!j.hasParent)
     if (j ne _jump) {
       _jump.deParent()
       _jump = j
@@ -386,6 +386,11 @@ class Block private (
   }
 
   def replaceJump(j: Jump): Block = {
+    if (j.hasParent) {
+      val parent = j.parent
+      j.deParent()
+      parent.jump = GoTo(Set.empty)
+    }
     jump = j
     this
   }

src/main/scala/ir/Statement.scala

@@ -127,21 +127,7 @@ object GoTo:
 
 
 sealed trait Call extends Jump {
-  private var _returnTarget: Option[Block] = None
-
-  // replacing the return target of a call
-  def returnTarget_=(b: Block): Unit = {
-    require(b.hasParent)
-
-    if (hasParent) {
-      // if we don't have a parent now, delay adding the fallthrough block until linking
-      parent.fallthrough = Some(GoTo(Set(b)))
-    }
-
-    _returnTarget = Some(b)
-  }
-
-  def returnTarget: Option[Block] = _returnTarget
+  val returnTarget: Option[Block]
 
   // moving a call between blocks
   override def linkParent(p: Block): Unit = {
@@ -154,10 +140,9 @@ sealed trait Call extends Jump {
 }
 
 class DirectCall(val target: Procedure,
-                 private val _returnTarget: Option[Block] = None,
+                 override val returnTarget: Option[Block] = None,
                  override val label: Option[String] = None
                 ) extends Call {
-  _returnTarget.foreach(x => returnTarget = x)
   /* override def locals: Set[Variable] = condition match {
     case Some(c) => c.locals
     case None => Set()
@@ -182,10 +167,9 @@ object DirectCall:
   def unapply(i: DirectCall): Option[(Procedure, Option[Block], Option[String])] = Some(i.target, i.returnTarget, i.label)
 
 class IndirectCall(var target: Variable,
-                   private val _returnTarget: Option[Block] = None,
+                   override val returnTarget: Option[Block] = None,
                    override val label: Option[String] = None
                   ) extends Call {
-  _returnTarget.foreach(x => returnTarget = x)
   /* override def locals: Set[Variable] = condition match {
     case Some(c) => c.locals + target
     case None => Set(target)

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

@@ -47,7 +47,10 @@ case class EventuallyIndirectCall(target: Variable, fallthrough: Option[DelayNam
 
 case class EventuallyCall(target: DelayNameResolve, fallthrough: Option[DelayNameResolve]) extends EventuallyJump {
   override def resolve(p: Program): DirectCall = {
-    val t = target.resolveProc(p).get
+    val t = target.resolveProc(p) match {
+      case Some(x) => x
+      case None => throw Exception("can't resolve proc " + p)
+    }
     val ft = fallthrough.flatMap(_.resolveBlock(p))
     DirectCall(t, ft)
   }
@@ -70,11 +73,9 @@ def goto(targets: List[String]): EventuallyGoto = {
   EventuallyGoto(targets.map(p => DelayNameResolve(p)))
 }
 
-def indirectCall(tgt: String, fallthrough: Option[String]): EventuallyCall = EventuallyCall(DelayNameResolve(tgt), fallthrough.map(x => DelayNameResolve(x)))
+def directCall(tgt: String, fallthrough: Option[String]): EventuallyCall = EventuallyCall(DelayNameResolve(tgt), fallthrough.map(x => DelayNameResolve(x)))
 
-def call(tgt: String, fallthrough: Option[String]): EventuallyCall = EventuallyCall(DelayNameResolve(tgt), fallthrough.map(x => DelayNameResolve(x)))
-
-def call(tgt: Variable, fallthrough: Option[String]): EventuallyIndirectCall = EventuallyIndirectCall(tgt, fallthrough.map(x => DelayNameResolve(x)))
+def indirectCall(tgt: Variable, fallthrough: Option[String]): EventuallyIndirectCall = EventuallyIndirectCall(tgt, fallthrough.map(x => DelayNameResolve(x)))
 // def directcall(tgt: String) = EventuallyCall(DelayNameResolve(tgt), None)
 
 

src/main/scala/translating/GTIRBToIR.scala

@@ -299,7 +299,7 @@ class GTIRBToIR(mods: Seq[Module], parserMap: immutable.Map[String, Array[Array[
   private def cleanUpIfPCAssign(block: Block, procedure: Procedure): Unit = {
     var newBlockCount = 0
     var currentBlock = block
-    var currentStatement = currentBlock.statements.head()
+    var currentStatement = currentBlock.statements.head
     var breakLoop = false
     val queue = mutable.Queue[Block]()
     while (!breakLoop) {
@@ -313,7 +313,7 @@ class GTIRBToIR(mods: Seq[Module], parserMap: immutable.Map[String, Array[Array[
 
           if (queue.nonEmpty) {
             currentBlock = queue.dequeue()
-            currentStatement = currentBlock.statements.head()
+            currentStatement = currentBlock.statements.head
           } else {
             breakLoop = true
           }
@@ -322,7 +322,7 @@ class GTIRBToIR(mods: Seq[Module], parserMap: immutable.Map[String, Array[Array[
             currentStatement = currentBlock.statements.getNext(currentStatement)
           } else if (queue.nonEmpty) {
             currentBlock = queue.dequeue()
-            currentStatement = currentBlock.statements.head()
+            currentStatement = currentBlock.statements.head
           } else {
             breakLoop = true
           }

src/main/scala/translating/IRToBoogie.scala

@@ -637,7 +637,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     case g: GoTo =>
       // collects all targets of the goto with a branch condition that we need to check the security level for
       // and collects the variables for that
-      val conditions = g.targets.flatMap(_.statements.headOption()).collect { case a: Assume if a.checkSecurity => a }
+      val conditions = g.targets.flatMap(_.statements.headOption.collect { case a: Assume if a.checkSecurity => a })
       val conditionVariables = conditions.flatMap(_.body.variables)
       val gammas = conditionVariables.map(_.toGamma).toList.sorted
       val conditionAssert: List[BCmd] = if (gammas.size > 1) {

src/main/scala/translating/SpecificationLoader.scala

@@ -318,7 +318,11 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) {
 
   def visitId(ctx: IdContext, nameToGlobals: Map[String, SpecGlobal], params: Map[String, Parameter] = Map()): BExpr = {
     val id = ctx.getText
-    if (id.startsWith("Gamma_")) {
+    id match {
+      case id if id.startsWith("Gamma_R") => {
+        BVariable(id, BoolBType, Scope.Global)
+      }
+      case id if (id.startsWith("Gamma_")) => {
       val gamma_id = id.stripPrefix("Gamma_")
       params.get(gamma_id) match {
         case Some(p: Parameter) => p.value.toGamma
@@ -327,26 +331,31 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) {
             case Some(g: SpecGlobal) => SpecGamma(g)
             case None                => throw new Exception(s"unresolvable reference to '$id' in specification")
           }
+        }
+      }
+      case id if id.startsWith("R") => {
+        BVariable(id, BitVecBType(64), Scope.Global)
+      }
+      case id =>  {
+        params.get(id) match {
+          case Some(p: Parameter) =>
+            val registerSize = p.value.size
+            val paramSize = p.size
+            if (paramSize == registerSize) {
+              p.value.toBoogie
+            } else if (registerSize > paramSize) {
+              BVExtract(registerSize - p.size, 0, p.value.toBoogie)
+            } else {
+              throw Exception(s"parameter $p doesn't fit in register ${p.value} for ID $id")
+            }
+          case None =>
+            nameToGlobals.get(ctx.getText) match {
+              case Some(g: SpecGlobal) => g
+              case None                => throw new Exception(s"unresolvable reference to '$id' in specification")
+            }
+        }
       }
-    } else {
-      params.get(id) match {
-        case Some(p: Parameter) =>
-          val registerSize = p.value.size
-          val paramSize = p.size
-          if (paramSize == registerSize) {
-            p.value.toBoogie
-          } else if (registerSize > paramSize) {
-            BVExtract(registerSize - p.size, 0, p.value.toBoogie)
-          } else {
-            throw Exception(s"parameter $p doesn't fit in register ${p.value} for ID $id")
-          }
-        case None =>
-          nameToGlobals.get(ctx.getText) match {
-            case Some(g: SpecGlobal) => g
-            case None                => throw new Exception(s"unresolvable reference to '$id' in specification")
-          }
       }
-    }
   }
 
   def visitMulDivModOp(ctx: MulDivModOpContext): BVBinOp = ctx.getText match {

src/main/scala/util/intrusive_list/IntrusiveList.scala

@@ -1,5 +1,6 @@
 package util.intrusive_list
 import scala.collection.mutable
+import scala.collection.mutable.ArrayBuffer
 
 // TODO: implement IterableOps
 //   So need iterablefactory https://docs.scala-lang.org/overviews/core/custom-collections.html
@@ -90,7 +91,7 @@ final class IntrusiveList[T <: IntrusiveListElement[T]] private (
     elem
   }
 
-  class IntrusiveListIterator(var elem: Option[T], forward: Boolean) extends Iterator[T] {
+  private class IntrusiveListIterator(var elem: Option[T], forward: Boolean) extends Iterator[T] {
     override def hasNext: Boolean = elem.isDefined
     override def next: T = {
       val t = elem.get
@@ -133,14 +134,14 @@ final class IntrusiveList[T <: IntrusiveListElement[T]] private (
   /**
    * Unsafely return the first element of the list.
    */
-  override def head(): T = firstElem.get
+  override def head: T = firstElem.get
 
-  override def headOption(): Option[T] = firstElem
+  override def headOption: Option[T] = firstElem
 
   /**
    * Unsafely return the first element of the list.
    */
-  def begin(): T = firstElem.get
+  def begin: T = firstElem.get
 
   /**
    * Check whether the list contains the given element (by reference) by linear scan.
@@ -169,7 +170,7 @@ final class IntrusiveList[T <: IntrusiveListElement[T]] private (
   /**
    * Unsafely return the last element of the list.
    */
-  def back(): T = lastElem.get
+  def back: T = lastElem.get
 
   /**
    * Add an element to the beginning of the list.
@@ -232,19 +233,19 @@ final class IntrusiveList[T <: IntrusiveListElement[T]] private (
   }
 
   /**
-   * Split the list into two lists, the first retains all elements up to to and including the provided element,
-   * and and returns the second list from the element until the end.
+   * Removes all elements after the provided element n and returns an ArrayBuffer containing the removed elements,
+   * maintaining the ordering.
    *
    * @param n The element to split on, remains in the first list.
-   * @return A list containing all elements after n.
+   * @return An ArrayBuffer containing all elements after n.
    */
-  def splitOn(n: T): IntrusiveList[T] = {
+  def splitOn(n: T): ArrayBuffer[T] = {
     require(!lastElem.contains(n))
     require(containsRef(n))
 
     val ne = n.next
 
-    val newlist = new IntrusiveList[T]()
+    val newlist = ArrayBuffer[T]()
     var next = n.next
     while (next.isDefined) {
       remove(next.get)
@@ -355,12 +356,7 @@ final class IntrusiveList[T <: IntrusiveListElement[T]] private (
   }
 
 object IntrusiveList {
-
-  def from[T <: IntrusiveListElement[T]](it: IntrusiveList[T]): IntrusiveList[T] = it
-
-  def from[T <: IntrusiveListElement[T]](it: IterableOnce[T]): IntrusiveList[T] = IntrusiveList[T]().addAll(it)
-
-  def empty[T <: IntrusiveListElement[T]]: IntrusiveList[T] = new IntrusiveList[T]()
+  def empty[T <: IntrusiveListElement[T]]: IntrusiveList[T] = IntrusiveList[T]()
 }
 
 /**
@@ -382,8 +378,6 @@ trait IntrusiveListElement[T <: IntrusiveListElement[T]]:
     elem
   }
 
-
-
   private[intrusive_list] final def unitary: Boolean = next.isEmpty && prev.isEmpty
 
   private[intrusive_list] final def insertAfter(elem: T): T = {