From 4492847e0a779141c26a3c747256a693c2cf4056 Mon Sep 17 00:00:00 2001
From: rina <k@rina.fyi>
Date: Wed, 10 Apr 2024 15:15:29 +1000
Subject: [PATCH 1/2] patch format_adt.py for aslt format.

aslt is almost python. this adds support for semicolon separation,
single-quote strings, and adds rules for line breaking aslt stmt/exprs.
---
 scripts/format_adt.py | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/scripts/format_adt.py b/scripts/format_adt.py
index 3a9da6a74..9f8eacfac 100755
--- a/scripts/format_adt.py
+++ b/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}.")

From 9cab1025c46aa97fa225ca0009ce8f5302e05471 Mon Sep 17 00:00:00 2001
From: Alistair Michael <alistair.michael@uq.edu.au>
Date: Tue, 16 Apr 2024 15:23:09 +1000
Subject: [PATCH 2/2] registers in spec

---
 .../translating/SpecificationLoader.scala     | 47 +++++++++++--------
 1 file changed, 28 insertions(+), 19 deletions(-)

diff --git a/src/main/scala/translating/SpecificationLoader.scala b/src/main/scala/translating/SpecificationLoader.scala
index 29aaa5587..1d9b82336 100644
--- a/src/main/scala/translating/SpecificationLoader.scala
+++ b/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 {