Add support for hexdumping sections by name

ELFSage/Commands/Read.lean

@@ -72,6 +72,8 @@ def getSymbolNameInSection
     | .ok ste => RawELFFile.symbolNameByLinkAndOffset
       elffile (SectionHeaderTableEntry.sh_link shte) (SymbolTableEntry.st_name ste)
 
+--TODO find? might be more appropriate than filter here.
+
 def printSymbolsForSectionType (elffile: RawELFFile) (ent_type : Nat) :=
   let ofType := elffile.getRawSectionHeaderTableEntries.filter $ λ⟨shte, _⟩↦
     SectionHeaderTableEntry.sh_type shte == ent_type
@@ -88,6 +90,18 @@ def printHexForSectionIdx (elffile : RawELFFile) (idx : Nat) :=
   | .none => IO.println s!"There doesn't appear to be a section header {idx}"
   | .some ⟨_, sec⟩ => dumpBytesAsHex sec.section_body
 
+def printHexForSectionName (elffile : RawELFFile) (name : String) :=
+  match elffile.getSectionHeaderStringTable? with
+  | .error err => IO.println err
+  | .ok (_,shstrtab_sec) =>
+  let shstrtab : ELFStringTable := ⟨shstrtab_sec.section_body⟩
+  let offset := shstrtab.stringToOffset name
+  let findPred : RawSectionHeaderTableEntry × InterpretedSection → Bool := (λent => SectionHeaderTableEntry.sh_name ent.fst == offset)
+  let msec := elffile.getRawSectionHeaderTableEntries.find? findPred
+  match msec with
+  | .none => IO.println s!"There doesn't appear to be a section header named {name}"
+  | .some ⟨_, sec⟩ => dumpBytesAsHex sec.section_body
+
 def printHexForSymbolIdx (elffile : RawELFFile) (idx : Nat) :=
   match do
     let ⟨symshte, symsec⟩ ← elffile.getSymbolTable?
@@ -239,8 +253,10 @@ def runReadCmd (p : Cli.Parsed): IO UInt32 := do
       | none => IO.println "couldn't parse section number provided for string dump"
       | some idx => printStringsForSectionIdx elffile idx
     | "hex-dump" => match flag.as? Nat with
-      | none => IO.println "couldn't parse section number provided for hex dump"
       | some idx => printHexForSectionIdx elffile idx
+      | none => match flag.as? String with
+        | some name => printHexForSectionName elffile name
+        | none => IO.println "couldn't parse section provided for hex dump"
     | "sym-dump" => match flag.as? Nat with
       | none => IO.println "couldn't parse symbol number provided for hex dump"
       | some idx => printHexForSymbolIdx elffile idx

ELFSage/Types/File.lean

@@ -142,6 +142,8 @@ def RawELFFile.getRawELFHeader : RawELFFile → RawELFHeader
   | .elf32 elffile => .elf32 elffile.file_header
   | .elf64 elffile => .elf64 elffile.file_header
 
+-- TODO Perhaps just make ELFFile an ELFHeader instance
+
 def RawELFFile.isBigendian (elffile : RawELFFile) := ELFHeader.isBigendian elffile.getRawELFHeader
 
 def RawELFFile.is64Bit (elffile : RawELFFile) := ELFHeader.is64Bit elffile.getRawELFHeader
@@ -156,6 +158,17 @@ def RawELFFile.getSymbolTable? (elffile : RawELFFile)
   where noSymTable := .error "No symbol table present, no st_size given, can't guess byte range"
         symbolSections := elffile.getRawSectionHeaderTableEntries.filter $ λ⟨shte, _⟩↦
           SectionHeaderTableEntry.sh_type shte == ELFSectionHeaderTableEntry.Type.SHT_SYMTAB
+
+/--
+Get the section .shstrtab. Defined by e_shstrndx in the ELF header and therefore unique
+-/
+def RawELFFile.getSectionHeaderStringTable? (elffile : RawELFFile)
+    : Except String (RawSectionHeaderTableEntry × InterpretedSection) :=
+    let sections := elffile.getRawSectionHeaderTableEntries
+    match sections[ELFHeader.e_shstrndx elffile.getRawELFHeader]? with
+    | none => .error "e_shstrndx in ELF header refers to a nonexistent section"
+    | some entry => .ok entry
+
 /--
 Get the section of type SHT_DYNSYM
 There's at most one: https://refspecs.linuxbase.org/elf/gabi4+/ch4.sheader.html

ELFSage/Types/StringTable.lean

@@ -22,3 +22,30 @@ def ELFStringTable.stringAt (st : ELFStringTable) (idx : Nat) : String :=
     let range := st.strings.extract idx idx₂
     let chars := range.toList.map (λbyte => Char.ofNat byte.toNat)
     String.mk chars
+
+structure StringTableEntry where
+  /-- String associated with a string table entry --/
+  string : String
+  /-- Offset within the associated string table --/
+  offset : Nat
+  deriving Repr
+
+-- Get all the string entries in an ELFStringTable as a list
+def ELFStringTable.allStrings (st : ELFStringTable) : List StringTableEntry := Id.run do
+  let mut idx := 0
+  let mut idx₂ := 0
+  let mut rslt := []
+  for ptr in st.strings do
+    if ptr = 0 then do
+      let range := st.strings.extract idx idx₂
+      let chars := range.toList.map (λbyte => Char.ofNat byte.toNat)
+      rslt := ⟨String.mk chars, idx⟩::rslt
+      idx := idx₂ + 1 -- point to the head of the next string, if there is one
+    idx₂ := idx₂ + 1 -- sync with ptr
+  return rslt
+
+-- Get the offset associated with a given string inside of a string table
+def ELFStringTable.stringToOffset (st : ELFStringTable) (str : String) : Option Nat := do
+  let strings := st.allStrings
+  let entry ← strings.find? (·.string = str)
+  return entry.offset

Main.lean

@@ -61,7 +61,7 @@ def readCmd : Cmd := `[Cli|
     c,  "archive-index";        "Display the symbol/file index in an archive"
     D,  "use-dynamic";          "Use the dynamic section info when displaying symbols"
     L,  "lint";                 "Display warning messages for possible problems"
-    x,  "hex-dump" : Nat;       "hex-dump=<number|name>. " ++
+    x,  "hex-dump" : String;       "hex-dump=<number|name>. " ++
                                 "Dump the contents of section <number|name> as bytes"
     p,  "string-dump" : Nat;    "--string-dump=<number|name>. " ++
                                 "Dump the contents of section <number|name> as strings"