package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/src/linksem_zarith/abi_mips64_relocation.ml.html
Source file abi_mips64_relocation.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 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241(*Generated by Lem from abis/mips64/abi_mips64_relocation.lem.*) (** [abi_mips64_relocation] contains types and definitions relating to ABI * specific relocation functionality for the MIPS64 ABI. *) open Lem_basic_classes open Lem_map open Lem_maybe open Lem_num open Show open Lem_string open Lem_assert_extra open Error open Missing_pervasives open Elf_file open Elf_header open Elf_relocation open Elf_symbol_table open Elf_types_native_uint open Memory_image open Abi_classes open Abi_utilities (* Relocation types *) let r_mips_none : Nat_big_num.num= ( (Nat_big_num.of_int 0)) (** No reloc *) let r_mips_16 : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** Direct 16 bit *) let r_mips_32 : Nat_big_num.num= ( (Nat_big_num.of_int 2)) (** Direct 32 bit *) let r_mips_rel32 : Nat_big_num.num= ( (Nat_big_num.of_int 3)) (** PC relative 32 bit *) let r_mips_26 : Nat_big_num.num= ( (Nat_big_num.of_int 4)) (** Direct 26 bit shifted *) let r_mips_hi16 : Nat_big_num.num= ( (Nat_big_num.of_int 5)) (** High 16 bit *) let r_mips_lo16 : Nat_big_num.num= ( (Nat_big_num.of_int 6)) (** Low 16 bit *) let r_mips_gprel16 : Nat_big_num.num= ( (Nat_big_num.of_int 7)) (** GP relative 16 bit *) let r_mips_literal : Nat_big_num.num= ( (Nat_big_num.of_int 8)) (** 16 bit literal entry *) let r_mips_got16 : Nat_big_num.num= ( (Nat_big_num.of_int 9)) (** 16 bit GOT entry *) let r_mips_pc16 : Nat_big_num.num= ( (Nat_big_num.of_int 10)) (** PC relative 16 bit *) let r_mips_call16 : Nat_big_num.num= ( (Nat_big_num.of_int 11)) (** 16 bit GOT entry for function *) let r_mips_gprel32 : Nat_big_num.num= ( (Nat_big_num.of_int 12)) (** GP relative 32 bit *) let r_mips_shift5 : Nat_big_num.num= ( (Nat_big_num.of_int 16)) let r_mips_shift6 : Nat_big_num.num= ( (Nat_big_num.of_int 17)) let r_mips_64 : Nat_big_num.num= ( (Nat_big_num.of_int 18)) let r_mips_got_disp : Nat_big_num.num= ( (Nat_big_num.of_int 19)) let r_mips_got_page : Nat_big_num.num= ( (Nat_big_num.of_int 20)) let r_mips_got_ofst : Nat_big_num.num= ( (Nat_big_num.of_int 21)) let r_mips_got_hi16 : Nat_big_num.num= ( (Nat_big_num.of_int 22)) let r_mips_got_lo16 : Nat_big_num.num= ( (Nat_big_num.of_int 23)) let r_mips_sub : Nat_big_num.num= ( (Nat_big_num.of_int 24)) let r_mips_insert_a : Nat_big_num.num= ( (Nat_big_num.of_int 25)) let r_mips_insert_b : Nat_big_num.num= ( (Nat_big_num.of_int 26)) let r_mips_delete : Nat_big_num.num= ( (Nat_big_num.of_int 27)) let r_mips_higher : Nat_big_num.num= ( (Nat_big_num.of_int 28)) let r_mips_highest : Nat_big_num.num= ( (Nat_big_num.of_int 29)) let r_mips_call_hi16 : Nat_big_num.num= ( (Nat_big_num.of_int 30)) let r_mips_call_lo16 : Nat_big_num.num= ( (Nat_big_num.of_int 31)) let r_mips_scn_disp : Nat_big_num.num= ( (Nat_big_num.of_int 32)) let r_mips_rel16 : Nat_big_num.num= ( (Nat_big_num.of_int 33)) let r_mips_add_immediate : Nat_big_num.num= ( (Nat_big_num.of_int 34)) let r_mips_pjump : Nat_big_num.num= ( (Nat_big_num.of_int 35)) let r_mips_relgot : Nat_big_num.num= ( (Nat_big_num.of_int 36)) let r_mips_jalr : Nat_big_num.num= ( (Nat_big_num.of_int 37)) let r_mips_tls_dtpmod32 : Nat_big_num.num= ( (Nat_big_num.of_int 38)) (** Module number 32 bit *) let r_mips_tls_dtprel32 : Nat_big_num.num= ( (Nat_big_num.of_int 39)) (** Module-relative offset 32 bit *) let r_mips_tls_dtpmod64 : Nat_big_num.num= ( (Nat_big_num.of_int 40)) (** Module number 64 bit *) let r_mips_tls_dtprel64 : Nat_big_num.num= ( (Nat_big_num.of_int 41)) (** Module-relative offset 64 bit *) let r_mips_tls_gd : Nat_big_num.num= ( (Nat_big_num.of_int 42)) (** 16 bit GOT offset for GD *) let r_mips_tls_ldm : Nat_big_num.num= ( (Nat_big_num.of_int 43)) (** 16 bit GOT offset for LDM *) let r_mips_tls_dtprel_hi16 : Nat_big_num.num= ( (Nat_big_num.of_int 44)) (** Module-relative offset, high 16 bits *) let r_mips_tls_dtprel_lo16 : Nat_big_num.num= ( (Nat_big_num.of_int 45)) (** Module-relative offset, low 16 bits *) let r_mips_tls_gottprel : Nat_big_num.num= ( (Nat_big_num.of_int 46)) (** 16 bit GOT offset for IE *) let r_mips_tls_tprel32 : Nat_big_num.num= ( (Nat_big_num.of_int 47)) (** TP-relative offset, 32 bit *) let r_mips_tls_tprel64 : Nat_big_num.num= ( (Nat_big_num.of_int 48)) (** TP-relative offset, 64 bit *) let r_mips_tls_tprel_hi16 : Nat_big_num.num= ( (Nat_big_num.of_int 49)) (** TP-relative offset, high 16 bits *) let r_mips_tls_tprel_lo16 : Nat_big_num.num= ( (Nat_big_num.of_int 50)) (** TP-relative offset, low 16 bits *) let r_mips_glob_dat : Nat_big_num.num= ( (Nat_big_num.of_int 51)) let r_mips_copy : Nat_big_num.num= ( (Nat_big_num.of_int 126)) let r_mips_jump_slot : Nat_big_num.num= ( (Nat_big_num.of_int 127)) (* TODO: borrowed from Dwarf, this should probbaly go somewhere else *) (*val natural_nat_shift_right : natural -> nat -> natural*) let byte_mask : Nat_big_num.num= (natural_of_hex "0xFF") (*val get_mips64_relocation_subtypes : natural -> (natural * natural * natural)*) let get_mips64_relocation_subtypes rel_type1:Nat_big_num.num*Nat_big_num.num*Nat_big_num.num= (let type1 = (Nat_big_num.bitwise_and rel_type1 byte_mask) in let type2 = (Nat_big_num.bitwise_and (Nat_big_num.shift_right rel_type1 8) byte_mask) in let type3 = (Nat_big_num.bitwise_and (Nat_big_num.shift_right rel_type1 16) byte_mask) in (type1, type2, type3)) (*val string_of_mips64_relocation_subtype : natural -> string*) let string_of_mips64_relocation_subtype rel_type1:string= (if Nat_big_num.equal rel_type1 r_mips_none then "R_MIPS_NONE" else if Nat_big_num.equal rel_type1 r_mips_16 then "R_MIPS_16" else if Nat_big_num.equal rel_type1 r_mips_32 then "R_MIPS_32" else if Nat_big_num.equal rel_type1 r_mips_rel32 then "R_MIPS_REL32" else if Nat_big_num.equal rel_type1 r_mips_26 then "R_MIPS_26" else if Nat_big_num.equal rel_type1 r_mips_hi16 then "R_MIPS_HI16" else if Nat_big_num.equal rel_type1 r_mips_lo16 then "R_MIPS_LO16" else if Nat_big_num.equal rel_type1 r_mips_gprel16 then "R_MIPS_GPREL16" else if Nat_big_num.equal rel_type1 r_mips_literal then "R_MIPS_LITERAL" else if Nat_big_num.equal rel_type1 r_mips_got16 then "R_MIPS_GOT16" else if Nat_big_num.equal rel_type1 r_mips_pc16 then "R_MIPS_PC16" else if Nat_big_num.equal rel_type1 r_mips_call16 then "R_MIPS_CALL16" else if Nat_big_num.equal rel_type1 r_mips_gprel32 then "R_MIPS_GPREL32" else if Nat_big_num.equal rel_type1 r_mips_shift5 then "R_MIPS_SHIFT5" else if Nat_big_num.equal rel_type1 r_mips_shift6 then "R_MIPS_SHIFT6" else if Nat_big_num.equal rel_type1 r_mips_64 then "R_MIPS_64" else if Nat_big_num.equal rel_type1 r_mips_got_disp then "R_MIPS_GOT_DISP" else if Nat_big_num.equal rel_type1 r_mips_got_page then "R_MIPS_GOT_PAGE" else if Nat_big_num.equal rel_type1 r_mips_got_ofst then "R_MIPS_GOT_OFST" else if Nat_big_num.equal rel_type1 r_mips_got_hi16 then "R_MIPS_GOT_HI16" else if Nat_big_num.equal rel_type1 r_mips_got_lo16 then "R_MIPS_GOT_LO16" else if Nat_big_num.equal rel_type1 r_mips_sub then "R_MIPS_SUB" else if Nat_big_num.equal rel_type1 r_mips_insert_a then "R_MIPS_INSERT_A" else if Nat_big_num.equal rel_type1 r_mips_insert_b then "R_MIPS_INSERT_B" else if Nat_big_num.equal rel_type1 r_mips_delete then "R_MIPS_DELETE" else if Nat_big_num.equal rel_type1 r_mips_higher then "R_MIPS_HIGHER" else if Nat_big_num.equal rel_type1 r_mips_highest then "R_MIPS_HIGHEST" else if Nat_big_num.equal rel_type1 r_mips_call_hi16 then "R_MIPS_CALL_HI16" else if Nat_big_num.equal rel_type1 r_mips_call_lo16 then "R_MIPS_CALL_LO16" else if Nat_big_num.equal rel_type1 r_mips_scn_disp then "R_MIPS_SCN_DISP" else if Nat_big_num.equal rel_type1 r_mips_rel16 then "R_MIPS_REL16" else if Nat_big_num.equal rel_type1 r_mips_add_immediate then "R_MIPS_ADD_IMMEDIATE" else if Nat_big_num.equal rel_type1 r_mips_pjump then "R_MIPS_PJUMP" else if Nat_big_num.equal rel_type1 r_mips_relgot then "R_MIPS_RELGOT" else if Nat_big_num.equal rel_type1 r_mips_jalr then "R_MIPS_JALR" else if Nat_big_num.equal rel_type1 r_mips_tls_dtpmod32 then "R_MIPS_TLS_DTPMOD32" else if Nat_big_num.equal rel_type1 r_mips_tls_dtprel32 then "R_MIPS_TLS_DTPREL32" else if Nat_big_num.equal rel_type1 r_mips_tls_dtpmod64 then "R_MIPS_TLS_DTPMOD64" else if Nat_big_num.equal rel_type1 r_mips_tls_dtprel64 then "R_MIPS_TLS_DTPREL64" else if Nat_big_num.equal rel_type1 r_mips_tls_gd then "R_MIPS_TLS_GD" else if Nat_big_num.equal rel_type1 r_mips_tls_ldm then "R_MIPS_TLS_LDM" else if Nat_big_num.equal rel_type1 r_mips_tls_dtprel_hi16 then "R_MIPS_TLS_DTPREL_HI16" else if Nat_big_num.equal rel_type1 r_mips_tls_dtprel_lo16 then "R_MIPS_TLS_DTPREL_LO16" else if Nat_big_num.equal rel_type1 r_mips_tls_gottprel then "R_MIPS_TLS_GOTTPREL" else if Nat_big_num.equal rel_type1 r_mips_tls_tprel32 then "R_MIPS_TLS_TPREL32" else if Nat_big_num.equal rel_type1 r_mips_tls_tprel64 then "R_MIPS_TLS_TPREL64" else if Nat_big_num.equal rel_type1 r_mips_tls_tprel_hi16 then "R_MIPS_TLS_TPREL_HI16" else if Nat_big_num.equal rel_type1 r_mips_tls_tprel_lo16 then "R_MIPS_TLS_TPREL_LO16" else if Nat_big_num.equal rel_type1 r_mips_glob_dat then "R_MIPS_GLOB_DAT" else if Nat_big_num.equal rel_type1 r_mips_copy then "R_MIPS_COPY" else if Nat_big_num.equal rel_type1 r_mips_jump_slot then "R_MIPS_JUMP_SLOT" else "[Invalid MIPS relocation 0x" ^ ((hex_string_of_natural rel_type1) ^ "]")) (*val string_of_mips64_relocation_type : natural -> string*) let string_of_mips64_relocation_type rel_type1:string= (let (type1, type2, type3) = (get_mips64_relocation_subtypes rel_type1) in (string_of_mips64_relocation_subtype type1) ^ ("/" ^ ((string_of_mips64_relocation_subtype type2) ^ ("/" ^ (string_of_mips64_relocation_subtype type3))))) (*val mips64_base_addr : symbol_reference_and_reloc_site -> natural -> natural*) let mips64_base_addr rr site_addr:Nat_big_num.num= (let reloc_site1 = ((match rr.maybe_reloc with | None -> failwith "amd64_base_addr: no reloc site during relocation" | Some rs -> rs )) in let offset = (Ml_bindings.nat_big_num_of_uint64 reloc_site1.ref_relent.elf64_ra_offset) in Nat_big_num.sub_nat site_addr offset) (*val mips64_reloc : forall 'abifeature. reloc_fn 'abifeature*) let mips64_reloc r:bool*('abifeature annotated_memory_image ->Nat_big_num.num ->symbol_reference_and_reloc_site ->Nat_big_num.num*(Nat_big_num.num ->Nat_big_num.num ->Nat_big_num.num ->Nat_big_num.num))= ((match (string_of_mips64_relocation_type r) with | "R_MIPS_NONE/R_MIPS_NONE/R_MIPS_NONE" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 0), (fun s -> fun a -> fun ea -> failwith "mips64_reloc: tried to apply a R_MIPS_NONE/R_MIPS_NONE/R_MIPS_NONE relocation")))))) (* TODO: not sure if always adding the base address is a good idea. Might be better to make the caller do so only if the symbol is undefined. *) | "R_MIPS_REL32/R_MIPS_64/R_MIPS_NONE" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun ea -> Nat_big_num.add (i2n ( Nat_big_num.add (Nat_big_num.sub a (n2i ea)) (n2i s))) (mips64_base_addr rr site_addr))))))) | (* TODO *) "R_MIPS_TLS_TPREL64/R_MIPS_NONE/R_MIPS_NONE" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun ea -> (Nat_big_num.of_int 0))))))) | (* TODO *) "R_MIPS_TLS_DTPMOD64/R_MIPS_NONE/R_MIPS_NONE" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun ea -> (Nat_big_num.of_int 0))))))) | "R_MIPS_JUMP_SLOT/R_MIPS_NONE/R_MIPS_NONE" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun ea -> s)))))) | _ -> failwith ("unrecognised relocation " ^ (string_of_mips64_relocation_type r)) )) (* MIPS has a non-standard encoding for reloc info. See https://sourceware.org/ml/libc-alpha/2003-03/msg00224.html *) (*val abi_mips_parse_elf64_relocation_info : elf64_xword -> (natural (* type *) * natural (* symbol *))*) let abi_mips_parse_elf64_relocation_info w:Nat_big_num.num*Nat_big_num.num= (let mask = (Uint64_wrapper.of_bigint (natural_of_hex "0xffffffff")) in let sym1 = (Ml_bindings.nat_big_num_of_uint64 (Uint64_wrapper.logand w mask)) in let typ = (Ml_bindings.nat_big_num_of_uint64 (Uint64_wrapper.shift_right w 32)) in let (s1, s2, s3, s4) = (Uint32_wrapper.to_bytes (Uint32_wrapper.of_bigint typ)) in let typ = (Uint32_wrapper.to_bigint (Uint32_wrapper.of_quad s4 s3 s2 s1)) in (typ, sym1))