diff --git a/ELFSage/Commands/Read.lean b/ELFSage/Commands/Read.lean index c65915c..eb95196 100644 --- a/ELFSage/Commands/Read.lean +++ b/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 diff --git a/ELFSage/Types/File.lean b/ELFSage/Types/File.lean index 64191a1..917ff6b 100644 --- a/ELFSage/Types/File.lean +++ b/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 diff --git a/ELFSage/Types/StringTable.lean b/ELFSage/Types/StringTable.lean index 9b40f55..eff873a 100644 --- a/ELFSage/Types/StringTable.lean +++ b/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 diff --git a/Main.lean b/Main.lean index 0081818..5cc9793 100644 --- a/Main.lean +++ b/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=. " ++ + x, "hex-dump" : String; "hex-dump=. " ++ "Dump the contents of section as bytes" p, "string-dump" : Nat; "--string-dump=. " ++ "Dump the contents of section as strings"