summaryrefslogtreecommitdiff
path: root/src/elf_model/elf_section_header.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/elf_model/elf_section_header.ml')
-rw-r--r--src/elf_model/elf_section_header.ml298
1 files changed, 0 insertions, 298 deletions
diff --git a/src/elf_model/elf_section_header.ml b/src/elf_model/elf_section_header.ml
deleted file mode 100644
index 1a73d35f..00000000
--- a/src/elf_model/elf_section_header.ml
+++ /dev/null
@@ -1,298 +0,0 @@
-(*Generated by Lem from elf_section_header.lem.*)
-open Lem_basic_classes
-open Lem_bool
-open Lem_list
-open Lem_num
-open Lem_string
-
-open Bitstring
-open Error
-open Elf_types
-open Show
-
-(** Special section indices. *)
-
-(** [shn_undef]: marks an undefined, missing or irrelevant section reference.
- *)
-let shn_undef : int =( 0)
-(** [shn_loreserve]: this specifies the lower bound of the range of reserved
- * indices.
- *)
-let shn_loreserve : int =( 65280) (* 0xff00 *)
-(** [shn_loproc]: start of the range reserved for processor-specific semantics.
- *)
-let shn_loproc : int =( 65280) (* 0xff00 *)
-(** [shn_hiproc]: end of the range reserved for processor-specific semantics.
- *)
-let shn_hiproc : int =( 65311) (* 0xff1f *)
-(** [shn_loos]: start of the range reserved for operating system-specific
- * semantics.
- *)
-let shn_loos : int =( 65312) (* 0xff20 *)
-(** [shn_hios]: end of the range reserved for operating system-specific
- * semantics.
- *)
-let shn_hios : int =( 65343) (* 0xff3f *)
-(** [shn_abs]: specifies the absolute values for the corresponding reference.
- * Symbols defined relative to section number [shn_abs] have absolute values
- * and are not affected by relocation.
- *)
-let shn_abs : int =( 65521) (* 0xfff1 *)
-(** [shn_common]: symbols defined relative to this index are common symbols,
- * such as unallocated C external variables.
- *)
-let shn_common : int =( 65522) (* 0xfff2 *)
-(** [shn_xindex]: an escape value. It indicates the actual section header index
- * is too large to fit in the containing field and is located in another
- * location (specific to the structure where it appears).
- *)
-let shn_xindex : int =( 65535) (* 0xffff *)
-(** [shn_hireserve]: specifies the upper-bound of reserved values.
- *)
-let shn_hireserve : int =( 65535) (* 0xffff *)
-
-(*val string_of_special_section_index : nat -> string*)
-let string_of_special_section_index i =
-(if i = shn_undef then
- "SHN_UNDEF"
- else if i = shn_loreserve then
- "SHN_LORESERVE"
- else if (i >= shn_loproc) && (i <= shn_hiproc) then
- "SHN_PROCESSOR_SPECIFIC"
- else if (i >= shn_loos) && (i <= shn_hios) then
- "SHN_OS_SPECIFIC"
- else if i = shn_abs then
- "SHN_ABS"
- else if i = shn_common then
- "SHN_COMMON"
- else if i = shn_xindex then
- "SHN_XINDEX"
- else if i = shn_hireserve then
- "SHN_HIRESERVE"
- else
- "SHN UNDEFINED")
-
-(** Section types. *)
-
-(** Marks the section header as being inactive. *)
-let sht_null : int =( 0)
-(** Section holds information defined by the program. *)
-let sht_progbits : int =( 1)
-(** The following two section types hold a symbol table. An object file may only
- * have one symbol table of each of the respective types. The symtab provides
- * a place for link editing, whereas the dynsym section holds a minimal set of
- * dynamic linking symbols
- *)
-let sht_symtab : int =( 2)
-let sht_dynsym : int =( 11)
-(** Section holds a string table *)
-let sht_strtab : int =( 3)
-(** Section holds relocation entries with explicit addends. An object file may
- * have multiple section of this type.
- *)
-let sht_rela : int =( 4)
-(** Section holds a symbol hash table. An object file may only have a single
- * hash table.
- *)
-let sht_hash : int =( 5)
-(** Section holds information for dynamic linking. An object file may only have
- * a single dynamic section.
- *)
-let sht_dynamic : int =( 6)
-(** Section holds information that marks the file in some way. *)
-let sht_note : int =( 7)
-(** Section occupies no space in the file but otherwise resembles a progbits
- * section.
- *)
-let sht_nobits : int =( 8)
-(** Section holds relocation entries without explicit addends. An object file
- * may have multiple section of this type.
- *)
-let sht_rel : int =( 9)
-(** Section type is reserved but has an unspecified meaning. *)
-let sht_shlib : int =( 10)
-(** Section contains an array of pointers to initialisation functions. Each
- * pointer is taken as a parameterless function with a void return type.
- *)
-let sht_init_array : int =( 14)
-(** Section contains an array of pointers to termination functions. Each
- * pointer is taken as a parameterless function with a void return type.
- *)
-let sht_fini_array : int =( 15)
-(** Section contains an array of pointers to initialisation functions that are
- * invoked before all other initialisation functions. Each
- * pointer is taken as a parameterless function with a void return type.
- *)
-let sht_preinit_array : int =( 16)
-(** Section defines a section group, i.e. a set of sections that are related and
- * must be treated especially by the linker. May only appear in relocatable
- * objects.
- *)
-let sht_group : int =( 17)
-(** Section is associated with sections of type SHT_SYMTAB and is required if
- * any of the section header indices referenced by that symbol table contains
- * the escape value SHN_XINDEX.
- *)
-let sht_symtab_shndx : int =( 18)
-(** XXX: broken for the time being due to Lem bug. *)
-let sht_loos : int =( 0)
-let sht_hios : int =( 0)
-let sht_loproc : int =( 0)
-let sht_hiproc : int =( 0)
-let sht_louser : int =( 0)
-let sht_hiuser : int =( 0)
-(* XXX: constants too big for Lem to parse, apparently!
-let sht_loos : nat = 1610612736 (* 0x60000000 *)
-let sht_hios : nat = 1879048191 (* 0x6fffffff *)
-let sht_loproc : nat = 1879048192 (* 0x70000000 *)
-let sht_hiproc : nat = 2147483647 (* 0x7fffffff *)
-let sht_louser : nat = 2147483648 (* 0x80000000 *)
-let sht_hiuser : nat = 2415919103 (* 0x8fffffff *)
-*)
-
-let string_of_section_type i =
-(if i = sht_null then
- "SHT_NULL"
- else if i = sht_progbits then
- "SHT_PROGBITS"
- else if i = sht_symtab then
- "SHT_SYMTAB"
- else if i = sht_strtab then
- "SHT_STRTAB"
- else if i = sht_rela then
- "SHT_RELA"
- else if i = sht_hash then
- "SHT_HASH"
- else if i = sht_dynamic then
- "SHT_DYNAMIC"
- else if i = sht_note then
- "SHT_NOTE"
- else if i = sht_nobits then
- "SHT_NOBITS"
- else if i = sht_rel then
- "SHT_REL"
- else if i = sht_shlib then
- "SHT_SHLIB"
- else if i = sht_dynsym then
- "SHT_DYNSYM"
- else if i = sht_init_array then
- "SHT_INIT_ARRAY"
- else if i = sht_fini_array then
- "SHT_FINI_ARRAY"
- else if i = sht_preinit_array then
- "SHT_PREINIT_ARRAY"
- else if i = sht_group then
- "SHT_GROUP"
- else if i = sht_symtab_shndx then
- "SHT_SYMTAB_SHNDX"
- else if (i >= sht_loos) && (i <= sht_hios) then
- "SHT_OS_SPECIFIC"
- else if (i >= sht_loproc) && (i <= sht_hiproc) then
- "SHT_PROCESSOR_SPECIFIC"
- else if (i >= sht_louser) && (i <= sht_hiuser) then
- "SHT_USER_SPECIFIC"
- else
- "SHT UNDEFINED")
-
-(** Section header table entry type. *)
-
-type elf32_section_header_table_entry =
- { elf32_sh_name : Int64.t
- ; elf32_sh_type : Int64.t
- ; elf32_sh_flags : Int64.t
- ; elf32_sh_addr : Int64.t
- ; elf32_sh_offset : Int64.t
- ; elf32_sh_size : Int64.t
- ; elf32_sh_link : Int64.t
- ; elf32_sh_info : Int64.t
- ; elf32_sh_addralign : Int64.t
- ; elf32_sh_entsize : Int64.t
- }
-
-let read_elf32_section_header_table_entry (bs : Bitstring.bitstring) =
-(Ml_bindings.read_elf32_word bs >>= (fun (sh_name, bs) ->
- Ml_bindings.read_elf32_word bs >>= (fun (sh_type, bs) ->
- Ml_bindings.read_elf32_word bs >>= (fun (sh_flags, bs) ->
- Ml_bindings.read_elf32_addr bs >>= (fun (sh_addr, bs) ->
- Ml_bindings.read_elf32_off bs >>= (fun (sh_offset, bs) ->
- Ml_bindings.read_elf32_word bs >>= (fun (sh_size, bs) ->
- Ml_bindings.read_elf32_word bs >>= (fun (sh_link, bs) ->
- Ml_bindings.read_elf32_word bs >>= (fun (sh_info, bs) ->
- Ml_bindings.read_elf32_word bs >>= (fun (sh_addralign, bs) ->
- Ml_bindings.read_elf32_word bs >>= (fun (sh_entsize, bs) ->
- return
- { elf32_sh_name = sh_name
- ; elf32_sh_type = sh_type
- ; elf32_sh_flags = sh_flags
- ; elf32_sh_addr = sh_addr
- ; elf32_sh_offset = sh_offset
- ; elf32_sh_size = sh_size
- ; elf32_sh_link = sh_link
- ; elf32_sh_info = sh_info
- ; elf32_sh_addralign = sh_addralign
- ; elf32_sh_entsize = sh_entsize
- })))))))))))
-
-let string_of_elf32_section_header_table_entry entry =
-(List.fold_right (^) [
- "\t"; "Name: "; Int64.to_string entry.elf32_sh_name
- ; "\t"; "Type: "; string_of_section_type (Int64.to_int entry.elf32_sh_type)
- ; "\n\t"; "Flags: "; Int64.to_string entry.elf32_sh_flags
- ; "\t"; "Address: "; Int64.to_string entry.elf32_sh_addr
- ; "\t"; "Size: "; Int64.to_string entry.elf32_sh_size; "\n\n"
- ] "")
-
-let instance_Show_Show_Elf_section_header_elf32_section_header_table_entry_dict =({
-
- show_method = string_of_elf32_section_header_table_entry})
-
-(** Section header table type. *)
-
-type elf32_section_header_table = elf32_section_header_table_entry list
-;;
-
-let rec read_elf32_section_header_table' entry_size bitstring0 =
-(if Bitstring.bitstring_length bitstring0 = 0 then
- return []
- else
- let (eat, rest) = (Utility.partition_bitstring entry_size bitstring0) in
- read_elf32_section_header_table_entry eat >>= (fun sect ->
- read_elf32_section_header_table' entry_size rest >>= (fun tail ->
- return (sect::tail))))
-
-(*val read_elf32_section_header_table : nat -> nat -> nat -> bitstring -> error (elf32_section_header_table * bitstring)*)
-let read_elf32_section_header_table size entry_size offset bitstring0 =
-(let (prefix, relevant) = (Utility.partition_bitstring offset bitstring0) in
- let (eat, rest) = (Utility.partition_bitstring (size * entry_size) relevant) in
- read_elf32_section_header_table' entry_size eat >>= (fun entries ->
- return (entries, rest)))
-;;
-
-(*val elf32_size_correct : elf32_section_header_table_entry -> elf32_section_header_table -> bool*)
-let elf32_size_correct hdr tbl =
-((match Int64.to_int hdr.elf32_sh_size with
- | 0 -> true
- | m -> m = List.length tbl
- ))
-;;
-
-(*val is_valid_elf32_section_header_table : elf32_section_header_table -> bool*)
-let is_valid_elf32_section_header_table tbl =
-((match tbl with
- | [] -> false
- | x::xs ->
-(Int64.to_int x.elf32_sh_name = 0) &&
- ((Int64.to_int x.elf32_sh_type = sht_null) &&
- ((Int64.to_int x.elf32_sh_flags = 0) &&
- ((Int64.to_int x.elf32_sh_addr = 0) &&
- ((Int64.to_int x.elf32_sh_offset = 0) &&
- ((Int64.to_int x.elf32_sh_info = 0) &&
- ((Int64.to_int x.elf32_sh_addralign = 0) &&
- ((Int64.to_int x.elf32_sh_entsize = 0) &&
- elf32_size_correct x tbl)))))))
- (* XXX: more correctness criteria in time *)
- ))
-
-let string_of_elf32_section_header_table (tbl : elf32_section_header_table) : string =
-("Section header table:" ^ ("\n" ^
- List.fold_right (^) (List.map string_of_elf32_section_header_table_entry tbl) ""))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:12:56 +0000