package linksem

You can search for identifiers within the package.
in-package search v0.2.0
linksem
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file `gnu_ext_section_header_table.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
(*Generated by Lem from gnu_extensions/gnu_ext_section_header_table.lem.*)
(** The module [gnu_ext_section_header_table] implements function, definitions
  * and types relating to the GNU extensions to the standard ELF section header
  * table.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_map
open Lem_maybe
open Lem_num
open Lem_string

open Hex_printing

open Error
open String_table
open Show

open Elf_section_header_table
open Elf_interpreted_section

(** GNU extended section types *)

(** [GNU_HASH] does not appear to be defined in the LSB but is present in
  * several ELF binaries collected in the wild...
  *
  * TODO: find out where this comes from?
  * ANSW: a mailing list apparently!  See here:
  *   https://sourceware.org/ml/binutils/2006-10/msg00377.html
  *)
let sht_gnu_hash    : Nat_big_num.num=  ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939524091)))     (* 0x6FFFFFF6 *)

(** The following are all defined in Section 10.2.2.2 of the LSB as additional
  * section types over the ones defined in the SCO ELF spec.
  *)

(** [sht_gnu_verdef] contains the symbol versions that are provided.
  *)
let sht_gnu_verdef  : Nat_big_num.num=  (Nat_big_num.sub_nat ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939524095)))( (Nat_big_num.of_int 1))) (* 0x6ffffffd *)
(** [sht_gnu_verneed] contains the symbol versions that are required.
  *)
let sht_gnu_verneed : Nat_big_num.num=  ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939524095)))     (* 0x6ffffffe *)
(** [sht_gnu_versym] contains the symbol version table.
  *)
let sht_gnu_versym  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939524095)))( (Nat_big_num.of_int 1))) (* 0x6fffffff *)
(** [sht_gnu_liblist] appears to be undocumented but appears in PowerPC 64 ELF
  * binaries in "the wild".
  *)
let sht_gnu_liblist : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939524091)))( (Nat_big_num.of_int 1))) (* 0x6FFFFFF7 *)

(** [string_of_gnu_ext_section_type m] produces a string based representation of
  * GNU extension section type [m].
  *)
(*val string_of_gnu_ext_section_type : natural -> string*)
let string_of_gnu_ext_section_type i:string=
   (if Nat_big_num.equal i sht_gnu_hash then
    "GNU_HASH"
  else if Nat_big_num.equal i sht_gnu_verdef then
    "VERDEF"
  else if Nat_big_num.equal i sht_gnu_verneed then
    "VERNEED"
  else if Nat_big_num.equal i sht_gnu_versym then
    "VERSYM"
  else if Nat_big_num.equal i sht_gnu_liblist then
    "GNU_LIBLIST"
  else if Nat_big_num.greater_equal i sht_loos && Nat_big_num.less_equal i sht_hios then
    let diff = (Nat_big_num.sub_nat i sht_loos) in
    let suff = (unsafe_hex_string_of_natural 0 diff) in
      "LOOS+" ^ suff
  else
    "Invalid GNU EXT section type: " ^ Nat_big_num.to_string i)
    
(** [gnu_ext_additionall_special_sections] records additional section names that
  * map appear in GNU ELF binaries and their required associated types and
  * attributes.  See Section 10.3.1.1 of the LSB and the related map
  * [elf_special_sections] in [Elf_section_header_table] which records section
  * names and their required types and attributes that all ELF binaries share.
  *)
(*val gnu_ext_additional_special_sections : Map.map string (natural * natural)*)
let gnu_ext_additional_special_sections:((string),(Nat_big_num.num*Nat_big_num.num))Pmap.map=
   (Lem_map.fromList (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) [
    (".ctors", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
  ; (".data.rel.ro", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
  ; (".dtors", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
  ; (".eh_frame", (sht_progbits, shf_alloc))
  ; (".eh_frame_hdr", (sht_progbits, shf_alloc))
  ; (".gcc_execpt_table", (sht_progbits, shf_alloc))
  ; (".gnu.version", (sht_gnu_versym, shf_alloc))
  ; (".gnu.version_d", (sht_gnu_verdef, shf_alloc))
  ; (".gnu.version_r", (sht_gnu_verneed, shf_alloc))
  ; (".got.plt", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
  ; (".jcr", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
  ; (".note.ABI-tag", (sht_note, shf_alloc))
  ; (".stab", (sht_progbits, (Nat_big_num.of_int 0)))
  ; (".stabstr", (sht_strtab, (Nat_big_num.of_int 0)))
  ])
  
(** [is_valid_gnu_ext_elf32_section_header_table_entry scts stbl] checks whether
  * sections [scts] conforms with the contents of the special sections table.
  * Fails otherwise.
  *)
(*val is_valid_gnu_ext_elf32_section_header_table_entry : elf32_interpreted_section ->
  string_table -> bool*)
let is_valid_gnu_ext_elf32_section_header_table_entry ent stbl:bool=
   ((match String_table.get_string_at ent.elf32_section_name stbl with
    | Fail    f    -> false
    | Success name1 ->
      (match Pmap.lookup name1 gnu_ext_additional_special_sections with
        | None           ->
            is_valid_elf32_section_header_table_entry ent stbl
        | Some (typ, flags) -> Nat_big_num.equal
            typ ent.elf32_section_type && Nat_big_num.equal flags ent.elf32_section_flags
      )
  ))
  
(** [is_valid_gnu_ext_elf32_section_header_table sht stbl] checks whether every
  * member of the section header table [sht] conforms with the special sections
  * table.
  *)
(*val is_valid_gnu_ext_elf32_section_header_table : list elf32_interpreted_section ->
  string_table -> bool*)
let is_valid_gnu_ext_elf32_section_header_table ents stbl:bool=
   (List.for_all (fun x -> is_valid_gnu_ext_elf32_section_header_table_entry x stbl) ents)
  
(** [is_valid_gnu_ext_elf64_section_header_table_entry scts stbl] checks whether
  * sections [scts] conforms with the contents of the special sections table.
  * Fails otherwise.
  *)
(*val is_valid_gnu_ext_elf64_section_header_table_entry : elf64_interpreted_section ->
  string_table -> bool*)
let is_valid_gnu_ext_elf64_section_header_table_entry ent stbl:bool=
   ((match String_table.get_string_at ent.elf64_section_name stbl with
    | Fail    f    -> false
    | Success name1 ->
      (match Pmap.lookup name1 gnu_ext_additional_special_sections with
        | None           ->
            is_valid_elf64_section_header_table_entry ent stbl
        | Some (typ, flags) -> Nat_big_num.equal
            typ ent.elf64_section_type && Nat_big_num.equal flags ent.elf64_section_flags
      )
  ))
  
(** [is_valid_gnu_ext_elf64_section_header_table sht stbl] checks whether every
  * member of the section header table [sht] conforms with the special sections
  * table.
  *)
(*val is_valid_gnu_ext_elf64_section_header_table : list elf64_interpreted_section ->
  string_table -> bool*)
let is_valid_gnu_ext_elf64_section_header_table ents stbl:bool=
   (List.for_all (fun x -> is_valid_gnu_ext_elf64_section_header_table_entry x stbl) ents)
package linksem

Source file gnu_ext_section_header_table.ml

Source file `gnu_ext_section_header_table.ml`
