Merge branch 'main' into intrusive-list-parent-assertion-fix

UQ-PAC · Jun 5, 2024 · df44840 · df44840
2 parents 6f3231c + 104f4aa
commit df44840
Show file tree

Hide file tree

Showing 2 changed files with 38 additions and 26 deletions.
diff --git 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}.")

diff --git 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 {