Source file abi_mips64_relocation.ml

(*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))