Load ELF symbol information from GTIRB and compare to readelf

basilmill/basildocs.mill

@@ -48,9 +48,9 @@ trait BasilDocs extends ScalaModule {
 
   def scalaDocExternalMappingOptions = Task {
     val defaultExternals = Seq(
-      ".*scala/.*::scaladoc3::https://scala-lang.org/api/3.3_LTS/",
-      "java/.*::javadoc::https://docs.oracle.com/en/java/javase/17/docs/api/java.base/",
-      ".*com/google/protobuf.*::javadoc::https://protobuf.dev/reference/java/api-docs/",
+      ".*/scala/.*::scaladoc3::https://scala-lang.org/api/3.3_LTS/",
+      ".*/java/.*::javadoc::https://docs.oracle.com/en/java/javase/17/docs/api/java.base/",
+      ".*/com/google/protobuf.*::javadoc::https://protobuf.dev/reference/java/api-docs/",
     )
     val externals = defaultExternals ++ docsRegexes().map {
       case (path, regex) => s"$regex::$baseUrl/$path"

src/main/scala/Main.scala

@@ -10,14 +10,17 @@ import util.{
   BoogieMemoryAccessMode,
   DSAConfig,
   DebugDumpIRLogger,
+  FrontendMode,
   ILLoadingConfig,
+  IRLoading,
   LogLevel,
   Logger,
   MemoryRegionsMode,
   PCTrackingOption,
   ProcRelyVersion,
   RunUtils,
-  StaticAnalysisConfig
+  StaticAnalysisConfig,
+  writeToFile
 }
 
 import scala.language.postfixOps
@@ -144,6 +147,12 @@ object Main {
       doc = "Switch version of procedure rely/guarantee checks to emit. (function|ifblock)"
     )
     procedureRG: Option[String],
+    @arg(
+      name = "gts-relf",
+      doc =
+        "Use .gts file for obtaining ELF symbol information (overrides --relf) (defaults to true if using GTIRB input and no --relf)"
+    )
+    useGTIRBReadELF: Flag,
     @arg(name = "verbose", short = 'v', doc = "Show extra debugging logs (the same as -vl log)")
     verbose: Flag,
     @arg(
@@ -157,6 +166,8 @@ object Main {
     interpret: Flag,
     @arg(name = "dump-il", doc = "Dump the Intermediate Language to text.")
     dumpIL: Option[String],
+    @arg(name = "dump-relf", doc = "Dump Basil's representation of the readelf information to the given file and exit.")
+    dumpRelf: Option[String],
     @arg(name = "main-procedure-name", short = 'm', doc = "Name of the main procedure to begin analysis at.")
     mainProcedureName: String = "main",
     @arg(
@@ -335,7 +346,7 @@ object Main {
     val boogieGeneratorConfig =
       BoogieGeneratorConfig(boogieMemoryAccessMode, true, rely, conf.threadSplit.value, conf.noif.value)
 
-    val loadingInputs = if (conf.bapInputDirName.isDefined) then {
+    var loadingInputs = if (conf.bapInputDirName.isDefined) then {
       loadDirectory(ChooseInput.Bap, conf.bapInputDirName.get)
 
     } else if (conf.gtirbInputDirName.isDefined) then {
@@ -350,6 +361,56 @@ object Main {
       )
     }
 
+    val isGTIRB = loadingInputs.frontendMode == FrontendMode.Gtirb
+
+    // NOTE: --dump-relf ignores --gts-relf, to ensure that the output ELF files are correctly named
+    conf.dumpRelf match {
+      case None => ()
+      case Some(relfOut) =>
+
+        val gtirbRelfFile = Some(loadingInputs.inputFile).filter(_ => isGTIRB)
+        val realRelfFile = loadingInputs.relfFile
+
+        Logger.setLevel(LogLevel.DEBUG)
+        val (relf, gtirb) = (realRelfFile, gtirbRelfFile) match {
+          case (Some(relfFile), _) =>
+            val (a, b) = IRLoading.loadReadELFWithGTIRB(relfFile, loadingInputs)
+            (Some(a), b)
+          case (None, Some(_)) => (None, Some(IRLoading.loadGTIRBReadELF(loadingInputs)))
+          case _ => throw IllegalArgumentException("--dump-relf requires either --relf or a GTIRB input")
+        }
+
+        // skip writing files if the given path is an empty string. this checks compatibility and exits.
+        if (relfOut.trim.isEmpty)
+          return
+
+        relf match {
+          case Some(relf) =>
+            writeToFile(
+              relf.sorted.toScala
+                .replace("@GLIBC_2.17", "")
+                .replace("@GLIBC_2.38", "")
+                .replace("@GLIBC_2.34", ""),
+              relfOut + "-readelf.scala"
+            )
+          case None => Logger.warn(s"Failed to load .relf information, $relfOut-readelf.scala not written")
+        }
+        gtirb match {
+          case Some(relf) => writeToFile(relf.sorted.toScala, relfOut + "-gtsrelf.scala")
+          case None => Logger.warn(s"Failed to load GTIRB information, $relfOut-gtsrelf.scala not written")
+        }
+        return
+    }
+
+    // patch in gtirb-as-relf if directed or if relf is omitted but we are using gtirb.
+    // NOTE: this must be done early, because lots of later places make checks about loadingInputs.relfFile.
+    if (conf.useGTIRBReadELF.value || (isGTIRB && loadingInputs.relfFile.isEmpty)) {
+      if (!isGTIRB) {
+        throw IllegalArgumentException("--gts-relf requires a GTIRB input")
+      }
+      loadingInputs = loadingInputs.copy(relfFile = Some(loadingInputs.inputFile))
+    }
+
     if (loadingInputs.specFile.isDefined && loadingInputs.relfFile.isEmpty) {
       throw IllegalArgumentException("--spec requires --relf")
     }

src/main/scala/boogie/BExpr.scala

@@ -1,5 +1,6 @@
 package boogie
 import ir.*
+import ir.dsl.given
 import specification.*
 import util.assertion.*
 
@@ -788,7 +789,7 @@ case class SpecGlobal(
   arraySize: Option[Int],
   override val address: BigInt
 ) extends SymbolTableEntry,
-      SpecGlobalOrAccess {
+      SpecGlobalOrAccess derives ir.dsl.ToScala {
   override def specGlobals: Set[SpecGlobalOrAccess] = Set(this)
 
   def sanitisedName = util.StringEscape.escape(name)

src/main/scala/gtirb/AuxDecoder.scala

@@ -29,8 +29,9 @@ object AuxDecoder {
 
   /**
    * [[AuxKind]] provides pre-defined decoders for some official AuxData fields. An [[AuxKind]] can be
-   * passed to [[decodeAux]] to automatically extract and decode the given AuxData from a GTIRB
-   * [[com.grammatech.gtirb.proto.Module.Module]].
+   * passed to [[decodeAux]] to automatically extract and decode the given AuxData from a GTIRB [[com.grammatech.gtirb.proto.Module.Module]].
+   * See the [Standard AuxData Schemata](https://grammatech.github.io/gtirb/md__aux_data.html) for a list of official AuxData fields
+   * and their types.
    */
   enum AuxKind[T](val name: String, val decoder: Decoder[T]) {
     case ElfSymbolTabIdxInfo
@@ -40,13 +41,16 @@ object AuxDecoder {
           "elfSymbolInfo",
           readMap(readUuid, readTuple(readUint(64), readString, readString, readString, readUint(64)))
         )
+    case SectionProperties
+        extends AuxKind("sectionProperties", readMap(readUuid, readTuple(readUint(64), readUint(64))))
     case FunctionEntries extends AuxKind("functionEntries", readMap(readUuid, readSet(readUuid)))
     case FunctionBlocks extends AuxKind("functionBlocks", readMap(readUuid, readSet(readUuid)))
     case FunctionNames extends AuxKind("functionNames", readMap(readUuid, readUuid))
+    case SymbolForwarding extends AuxKind("symbolForwarding", readMap(readUuid, readUuid))
   }
 
   type Input = ByteArrayInputStream
-  type Decoder[T] = Input => T
+  type Decoder[T] = ByteArrayInputStream => T
 
   def decodeAux[T](known: AuxKind[T])(mod: Module) =
     decode(known.decoder)(mod.auxData(known.name))
@@ -145,6 +149,17 @@ object AuxDecoder {
     val x6 = r6(bs)
     (x1, x2, x3, x4, x5, x6)
 
+  // type ReadTuple[T <: Tuple] <: Tuple = T match
+  //   case Reader[out] *: rest => out *: ReadTuple[rest]
+  //   case EmptyTuple => EmptyTuple
+  //
+  // inline def readTuple[T <: Tuple](xs: T)(bs: Input): ReadTuple[T] =
+  //   inline xs match
+  //     case xs: (Reader[o] *: rest) =>
+  //       xs match
+  //         case h *: t => h(bs) *: readTuple[rest](t)(bs)
+  //     case _: EmptyTuple => EmptyTuple
+
   def readUuid(bs: Input) =
     // ByteString.copyFrom(readBytes(16)(bs))
     Base64.getEncoder().encodeToString(readBytes(16)(bs))