Source file abi_mips64_dynamic.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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
(*Generated by Lem from abis/mips64/abi_mips64_dynamic.lem.*)
open Lem_basic_classes
open Lem_num
open Lem_string

open Error
open Missing_pervasives
open Show
open String_table

open Elf_dynamic
open Elf_types_native_uint

(* Legal values for d_tag field of Elf32_Dyn. *)

let abi_mips64_dt_rld_version : Nat_big_num.num=  (natural_of_hex "0x70000001") (** Runtime linker interface version *)
let abi_mips64_dt_time_stamp : Nat_big_num.num=  (natural_of_hex "0x70000002") (** Timestamp *)
let abi_mips64_dt_ichecksum : Nat_big_num.num=  (natural_of_hex "0x70000003") (** Checksum *)
let abi_mips64_dt_iversion : Nat_big_num.num=  (natural_of_hex "0x70000004") (** Version string (string tbl index) *)
let abi_mips64_dt_flags : Nat_big_num.num=  (natural_of_hex "0x70000005") (** Flags *)
let abi_mips64_dt_base_address : Nat_big_num.num=  (natural_of_hex "0x70000006") (** Base address *)
let abi_mips64_dt_msym : Nat_big_num.num=  (natural_of_hex "0x70000007")
let abi_mips64_dt_conflict : Nat_big_num.num=  (natural_of_hex "0x70000008") (** Address of CONFLICT section *)
let abi_mips64_dt_liblist : Nat_big_num.num=  (natural_of_hex "0x70000009") (** Address of LIBLIST section *)
let abi_mips64_dt_local_gotno : Nat_big_num.num=  (natural_of_hex "0x7000000a") (** Number of local GOT entries *)
let abi_mips64_dt_conflictno : Nat_big_num.num=  (natural_of_hex "0x7000000b") (** Number of CONFLICT entries *)
let abi_mips64_dt_liblistno : Nat_big_num.num=  (natural_of_hex "0x70000010") (** Number of LIBLIST entries *)
let abi_mips64_dt_symtabno : Nat_big_num.num=  (natural_of_hex "0x70000011") (** Number of DYNSYM entries *)
let abi_mips64_dt_unrefextno : Nat_big_num.num=  (natural_of_hex "0x70000012") (** First external DYNSYM *)
let abi_mips64_dt_gotsym : Nat_big_num.num=  (natural_of_hex "0x70000013") (** First GOT entry in DYNSYM *)
let abi_mips64_dt_hipageno : Nat_big_num.num=  (natural_of_hex "0x70000014") (** Number of GOT page table entries *)
let abi_mips64_dt_rld_map : Nat_big_num.num=  (natural_of_hex "0x70000016") (** Address of run time loader map.  *)
let abi_mips64_dt_delta_class : Nat_big_num.num=  (natural_of_hex "0x70000017") (** Delta C++ class definition.  *)
let abi_mips64_dt_delta_class_no : Nat_big_num.num=  (natural_of_hex "0x70000018") (** Number of entries in DT_MIPS_DELTA_CLASS.  *)
let abi_mips64_dt_delta_instance : Nat_big_num.num=  (natural_of_hex "0x70000019") (** Delta C++ class instances.  *)
let abi_mips64_dt_delta_instance_no : Nat_big_num.num=  (natural_of_hex "0x7000001a") (** Number of entries in DT_MIPS_DELTA_INSTANCE.  *)
let abi_mips64_dt_delta_reloc : Nat_big_num.num=  (natural_of_hex "0x7000001b") (** Delta relocations.  *)
let abi_mips64_dt_delta_reloc_no : Nat_big_num.num=  (natural_of_hex "0x7000001c") (** Number of entries in DT_MIPS_DELTA_RELOC.  *)
let abi_mips64_dt_delta_sym : Nat_big_num.num=  (natural_of_hex "0x7000001d") (** Delta symbols that Delta relocations refer to.  *)
let abi_mips64_dt_delta_sym_no : Nat_big_num.num=  (natural_of_hex "0x7000001e") (** Number of entries in DT_MIPS_DELTA_SYM.  *)
let abi_mips64_dt_delta_classsym : Nat_big_num.num=  (natural_of_hex "0x70000020") (** Delta symbols that hold the class declaration.  *)
let abi_mips64_dt_delta_classsym_no : Nat_big_num.num=  (natural_of_hex "0x70000021") (** Number of entries in DT_MIPS_DELTA_CLASSSYM.  *)
let abi_mips64_dt_cxx_flags : Nat_big_num.num=  (natural_of_hex "0x70000022") (** Flags indicating for C++ flavor.  *)
let abi_mips64_dt_pixie_init : Nat_big_num.num=  (natural_of_hex "0x70000023")
let abi_mips64_dt_symbol_lib : Nat_big_num.num=  (natural_of_hex "0x70000024")
let abi_mips64_dt_localpage_gotidx : Nat_big_num.num=  (natural_of_hex "0x70000025")
let abi_mips64_dt_local_gotidx : Nat_big_num.num=  (natural_of_hex "0x70000026")
let abi_mips64_dt_hidden_gotidx : Nat_big_num.num=  (natural_of_hex "0x70000027")
let abi_mips64_dt_protected_gotidx : Nat_big_num.num=  (natural_of_hex "0x70000028")
let abi_mips64_dt_options : Nat_big_num.num=  (natural_of_hex "0x70000029") (** Address of .options.  *)
let abi_mips64_dt_interface : Nat_big_num.num=  (natural_of_hex "0x7000002a") (** Address of .interface.  *)
let abi_mips64_dt_dynstr_align : Nat_big_num.num=  (natural_of_hex "0x7000002b")
let abi_mips64_dt_interface_size : Nat_big_num.num=  (natural_of_hex "0x7000002c") (** Size of the .interface section. *)
(** Address of rld_text_rsolve function stored in GOT.  *)
let abi_mips64_dt_rld_text_resolve_addr : Nat_big_num.num=  (natural_of_hex "0x7000002d")
(** Default suffix of dso to be added by rld on dlopen() calls.  *)
let abi_mips64_dt_perf_suffix : Nat_big_num.num=  (natural_of_hex "0x7000002e")
let abi_mips64_dt_compact_size : Nat_big_num.num=  (natural_of_hex "0x7000002f") (** (O32)Size of compact rel section. *)
let abi_mips64_dt_gp_value : Nat_big_num.num=  (natural_of_hex "0x70000030") (** GP value for aux GOTs.  *)
let abi_mips64_dt_aux_dynamic : Nat_big_num.num=  (natural_of_hex "0x70000031") (** Address of aux .dynamic.  *)
(** The address of .got.plt in an executable using the new non-PIC ABI.  *)
let abi_mips64_dt_pltgot : Nat_big_num.num=  (natural_of_hex "0x70000032")
(** The base of the PLT in an executable using the new non-PIC ABI if that
    PLT is writable.  For a non-writable PLT, this is omitted or has a zero
    value.  *)
let abi_mips64_dt_rwplt : Nat_big_num.num=  (natural_of_hex "0x70000034")
(** An alternative description of the classic MIPS RLD_MAP that is usable
    in a PIE as it stores a relative offset from the address of the tag
    rather than an absolute address.  *)
let abi_mips64_dt_rld_map_rel : Nat_big_num.num=  (natural_of_hex "0x70000035")
let abi_mips64_dt_num : Nat_big_num.num=  (natural_of_hex "0x36")

(*val string_of_abi_mips64_dynamic_tag : natural -> string*)
let string_of_abi_mips64_dynamic_tag m:string=
   (if Nat_big_num.equal m abi_mips64_dt_rld_version then
    "MIPS64_RLD_VERSION"
  else if Nat_big_num.equal m abi_mips64_dt_flags then
    "MIPS64_FLAGS"
  else if Nat_big_num.equal m abi_mips64_dt_base_address then
    "MIPS64_BASE_ADDRESS"
  else if Nat_big_num.equal m abi_mips64_dt_local_gotno then
    "MIPS64_LOCAL_GOTNO"
  else if Nat_big_num.equal m abi_mips64_dt_symtabno then
    "MIPS64_SYMTABNO"
  else if Nat_big_num.equal m abi_mips64_dt_unrefextno then
    "MIPS64_RLD_UNREFEXTNO"
  else if Nat_big_num.equal m abi_mips64_dt_gotsym then
    "MIPS64_RLD_GOTSYM"
  else if Nat_big_num.equal m abi_mips64_dt_rld_map then
    "MIPS64_RLD_MAP"
  else if Nat_big_num.equal m abi_mips64_dt_rld_map_rel then
    "MIPS64_RLD_MAP_REL"
  else
    "Invalid MIPS64 dynamic tag 0x" ^ (hex_string_of_natural m))

(*val abi_mips64_tag_correspondence_of_tag : natural -> error tag_correspondence*)
let abi_mips64_tag_correspondence_of_tag m:(tag_correspondence)error=
   (if Nat_big_num.equal m abi_mips64_dt_rld_version then
    return C_Val
  else if Nat_big_num.equal m abi_mips64_dt_flags then
    return C_Val
  else if Nat_big_num.equal m abi_mips64_dt_base_address then
    return C_Ptr
  else if Nat_big_num.equal m abi_mips64_dt_local_gotno then
    return C_Val
  else if Nat_big_num.equal m abi_mips64_dt_symtabno then
    return C_Val
  else if Nat_big_num.equal m abi_mips64_dt_unrefextno then
    return C_Val
  else if Nat_big_num.equal m abi_mips64_dt_gotsym then
    return C_Val
  else if Nat_big_num.equal m abi_mips64_dt_rld_map then
    return C_Ptr
  else if Nat_big_num.equal m abi_mips64_dt_rld_map_rel then
    return C_Ptr
  else
    fail ("abi_mips64_tag_correspondence_of_tag: invalid MIPS64 dynamic tag 0x" ^ (hex_string_of_natural m)))

(*val abi_mips64_elf64_value_of_elf64_dyn : elf64_dyn -> string_table -> error elf64_dyn_value*)
let abi_mips64_elf64_value_of_elf64_dyn dyn stbl:(((Uint64_wrapper.uint64),(Uint64_wrapper.uint64))dyn_value)error=
   (let tag = (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag)) in
  if Nat_big_num.equal tag abi_mips64_dt_rld_version then bind (match dyn.elf64_dyn_d_un with
      | D_Val v -> return v
      | _ -> fail "abi_mips64_elf64_value_of_elf64_dyn: RLD_VERSION must be a Val"
    ) (fun v ->
    return (Numeric (Ml_bindings.nat_big_num_of_uint64 v)))
  else if Nat_big_num.equal tag abi_mips64_dt_flags then bind (match dyn.elf64_dyn_d_un with
      | D_Val v -> return v
      | _ -> fail "abi_mips64_elf64_value_of_elf64_dyn: FLAGS must be a Val"
    ) (fun flags ->
    return (Flags (Ml_bindings.nat_big_num_of_uint64 flags)))
  else if Nat_big_num.equal tag abi_mips64_dt_base_address then bind (match dyn.elf64_dyn_d_un with
      | D_Ptr v -> return v
      | _ -> fail "abi_mips64_elf64_value_of_elf64_dyn: BASE_ADDRESS must be a PTR"
    ) (fun v ->
    return (Address v))
  else if Nat_big_num.equal tag abi_mips64_dt_local_gotno then bind (match dyn.elf64_dyn_d_un with
      | D_Val v -> return v
      | _ -> fail "abi_mips64_elf64_value_of_elf64_dyn: LOCAL_GOTNO must be a Val"
    ) (fun v ->
    return (Numeric (Ml_bindings.nat_big_num_of_uint64 v)))
  else if Nat_big_num.equal tag abi_mips64_dt_symtabno then bind (match dyn.elf64_dyn_d_un with
      | D_Val v -> return v
      | _ -> fail "abi_mips64_elf64_value_of_elf64_dyn: SYMTABNO must be a Val"
    ) (fun v ->
    return (Numeric (Ml_bindings.nat_big_num_of_uint64 v)))
  else if Nat_big_num.equal tag abi_mips64_dt_unrefextno then bind (match dyn.elf64_dyn_d_un with
      | D_Val v -> return v
      | _ -> fail "abi_mips64_elf64_value_of_elf64_dyn: UNREFEXTNO must be a Val"
    ) (fun v ->
    return (Numeric (Ml_bindings.nat_big_num_of_uint64 v)))
  else if Nat_big_num.equal tag abi_mips64_dt_gotsym then bind (match dyn.elf64_dyn_d_un with
      | D_Val v -> return v
      | _ -> fail "abi_mips64_elf64_value_of_elf64_dyn: GOTSYM must be a Val"
    ) (fun v ->
    return (Numeric (Ml_bindings.nat_big_num_of_uint64 v)))
  else if Nat_big_num.equal tag abi_mips64_dt_rld_map then bind (match dyn.elf64_dyn_d_un with
      | D_Ptr v -> return v
      | _ -> fail "abi_mips64_elf64_value_of_elf64_dyn: RLD_MAP must be a PTR"
    ) (fun v ->
    return (Address v))
  else if Nat_big_num.equal tag abi_mips64_dt_rld_map_rel then bind (match dyn.elf64_dyn_d_un with
      | D_Ptr v -> return v
      | _ -> fail "abi_mips64_elf64_value_of_elf64_dyn: RLD_MAP_REL must be a PTR"
    ) (fun v ->
    return (Address v))
  else
    fail ("abi_mips64_elf64_value_of_elf64_dyn: invalid MIPS64 dynamic tag 0x" ^ (hex_string_of_natural tag)))