changed spec global

UQ-PAC · Jul 1, 2024 · fbcb303 · fbcb303
1 parent 5cda0e9
commit fbcb303
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 3 deletions.
diff --git a/src/main/scala/specification/Specification.scala b/src/main/scala/specification/Specification.scala
@@ -17,8 +17,17 @@ trait SpecGlobalOrAccess extends SpecVar {
   val size: Int
 }
 
-case class SpecGlobal(name: String, override val size: Int, arraySize: Option[Int], address: BigInt)
+trait SpecGlobal
     extends SpecGlobalOrAccess {
+
+  val name: String
+  override val size: Int
+  val arraySize: Option[Int]
+  val address: BigInt
+
+
+
+
   override def specGlobals: Set[SpecGlobalOrAccess] = Set(this)
   override val toAddrVar: BVar = BVariable("$" + s"${name}_addr", BitVecBType(64), Scope.Const)
   override val toOldVar: BVar = BVariable(s"${name}_old", BitVecBType(size), Scope.Local)
@@ -65,6 +74,10 @@ case class SpecGlobal(name: String, override val size: Int, arraySize: Option[In
   )
 }
 
+case class SpecObject(override val name: String, override  val size: Int, override val arraySize: Option[Int], override  val address: BigInt) extends SpecGlobal
+
+case class SpecFunc(override val name: String, override val size: Int, override val arraySize: Option[Int], override val address: BigInt) extends SpecGlobal
+
 case class SpecGamma(global: SpecGlobal) extends SpecVar {
   // TODO don't hardcode this
   override def resolveSpec: GammaLoad = GammaLoad(

diff --git a/src/main/scala/translating/ReadELFLoader.scala b/src/main/scala/translating/ReadELFLoader.scala
@@ -79,7 +79,10 @@ object ReadELFLoader {
     if ((ctx.entrytype.getText == "OBJECT" || ctx.entrytype.getText == "FUNC") && ctx.bind.getText == "GLOBAL" && ctx.vis.getText == "DEFAULT") {
       val name = ctx.name.getText
       if (name.forall(allowedChars.contains)) {
-        Some(SpecGlobal(name, ctx.size.getText.toInt * 8, None, hexToBigInt(ctx.value.getText)))
+        ctx.entrytype.getText match
+          case "OBJECT" => Some(SpecObject(name, ctx.size.getText.toInt * 8, None, hexToBigInt(ctx.value.getText)))
+          case "FUNC" => Some(SpecFunc(name, ctx.size.getText.toInt * 8, None, hexToBigInt(ctx.value.getText)))
+          case _ => None
       } else {
         None
       }

diff --git a/src/main/scala/translating/SpecificationLoader.scala b/src/main/scala/translating/SpecificationLoader.scala
@@ -130,7 +130,11 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) {
     if (bits != symbol.size) {
       throw new Exception(s"variable $id in specification does not match symbol table")
     }
-    SpecGlobal(id, size, arraySize, symbol.address)
+    symbol match
+      case SpecFunc(name, size, arraySize, address) => SpecFunc(id, size, arraySize, symbol.address)
+      case SpecObject(name, size, arraySize, address) => SpecObject(id, size, arraySize, symbol.address)
+      case _ => ???
+//    SpecGlobal(id, size, arraySize, symbol.address)
   }
 
   def visitLPred(ctx: LPredContext, nameToGlobals: Map[String, SpecGlobal]): (SpecGlobal, BExpr) = {