Merge pull request #205 from UQ-PAC/spec-registers

Lets you refer to registers in existing spec language by naive pattern match on the name of idents.
UQ-PAC · Jun 4, 2024 · 9292109 · 9292109
2 parents b6a2409 + 9cab102
commit 9292109
Showing 1 changed file with 28 additions and 19 deletions.
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 {