diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/elf_relocation.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/elf_relocation.ml | 312 |
1 files changed, 0 insertions, 312 deletions
diff --git a/lib/ocaml_rts/linksem/elf_relocation.ml b/lib/ocaml_rts/linksem/elf_relocation.ml deleted file mode 100644 index 65a77ef8..00000000 --- a/lib/ocaml_rts/linksem/elf_relocation.ml +++ /dev/null @@ -1,312 +0,0 @@ -(*Generated by Lem from elf_relocation.lem.*) -(** [elf_relocation] formalises types, functions and other definitions for working - * with ELF relocation and relocation with addend entries. - *) - -open Lem_basic_classes -open Lem_num -open Lem_list -(*import Set*) - -open Endianness -open Byte_sequence -open Error - -open Lem_string -open Show -open Missing_pervasives - -open Elf_types_native_uint - -(** ELF relocation records *) - -(** [elf32_relocation] is a simple relocation record (without addend). - *) -type elf32_relocation = - { elf32_r_offset : Uint32.uint32 (** Address at which to relocate *) - ; elf32_r_info : Uint32.uint32 (** Symbol table index/type of relocation to apply *) - } - -(** [elf32_relocation_a] is a relocation record with addend. - *) -type elf32_relocation_a = - { elf32_ra_offset : Uint32.uint32 (** Address at which to relocate *) - ; elf32_ra_info : Uint32.uint32 (** Symbol table index/type of relocation to apply *) - ; elf32_ra_addend : Int32.t (** Addend used to compute value to be stored *) - } - -(** [elf64_relocation] is a simple relocation record (without addend). - *) -type elf64_relocation = - { elf64_r_offset : Uint64.uint64 (** Address at which to relocate *) - ; elf64_r_info : Uint64.uint64 (** Symbol table index/type of relocation to apply *) - } - -(** [elf64_relocation_a] is a relocation record with addend. - *) -type elf64_relocation_a = - { elf64_ra_offset : Uint64.uint64 (** Address at which to relocate *) - ; elf64_ra_info : Uint64.uint64 (** Symbol table index/type of relocation to apply *) - ; elf64_ra_addend : Int64.t (** Addend used to compute value to be stored *) - } - -(** [elf64_relocation_a_compare r1 r2] is an ordering comparison function for - * relocation with addend records suitable for constructing sets, finite map - * and other ordered data structures. - * NB: we exclusively use elf64_relocation_a in range tags, regardless of what - * file/reloc the info came from, so only this one needs an Ord instance. - *) -(*val elf64_relocation_a_compare : elf64_relocation_a -> elf64_relocation_a -> - ordering*) -let elf64_relocation_a_compare ent1 ent2:int= - (tripleCompare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare (Ml_bindings.nat_big_num_of_uint64 ent1.elf64_ra_offset, Ml_bindings.nat_big_num_of_uint64 ent1.elf64_ra_info, - Nat_big_num.of_int64 ent1.elf64_ra_addend) - (Ml_bindings.nat_big_num_of_uint64 ent2.elf64_ra_offset, Ml_bindings.nat_big_num_of_uint64 ent2.elf64_ra_info, - Nat_big_num.of_int64 ent2.elf64_ra_addend)) - -let instance_Basic_classes_Ord_Elf_relocation_elf64_relocation_a_dict:(elf64_relocation_a)ord_class= ({ - - compare_method = elf64_relocation_a_compare; - - isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf64_relocation_a_compare f1 f2) (-1)))); - - isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf64_relocation_a_compare f1 f2)(Pset.from_list compare [(-1); 0]))); - - isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf64_relocation_a_compare f1 f2) 1))); - - isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf64_relocation_a_compare f1 f2)(Pset.from_list compare [1; 0])))}) - -(** Extracting useful information *) - -(** [extract_elf32_relocation_r_sym w] computes the symbol table index associated with - * an ELF32 relocation(a) entry. - * [w] here is the [r_info] member of the [elf32_relocation(a)] type. - *) -(*val extract_elf32_relocation_r_sym : elf32_word -> natural*) -let extract_elf32_relocation_r_sym w:Nat_big_num.num= - (Nat_big_num.of_string (Uint32.to_string (Uint32.shift_right w( 8)))) - -(** [extract_elf64_relocation_r_sym w] computes the symbol table index associated with - * an ELF64 relocation(a) entry. - * [w] here is the [r_info] member of the [elf64_relocation(a)] type. - *) -(*val extract_elf64_relocation_r_sym : elf64_xword -> natural*) -let extract_elf64_relocation_r_sym w:Nat_big_num.num= - (Ml_bindings.nat_big_num_of_uint64 (Uint64.shift_right w( 32))) - -(** [extract_elf32_relocation_r_type w] computes the symbol type associated with an ELF32 - * relocation(a) entry. - * [w] here is the [r_info] member of the [elf32_relocation(a)] type. - *) -(*val extract_elf32_relocation_r_type : elf32_word -> natural*) -let extract_elf32_relocation_r_type w:Nat_big_num.num= (Nat_big_num.modulus - (Nat_big_num.of_string (Uint32.to_string w))(Nat_big_num.of_int 256)) - -(** [extract_elf64_relocation_r_type w] computes the symbol type associated with an ELF64 - * relocation(a) entry. - * [w] here is the [r_info] member of the [elf64_relocation(a)] type. - *) -(*val extract_elf64_relocation_r_type : elf64_xword -> natural*) -let extract_elf64_relocation_r_type w:Nat_big_num.num= - (let magic = (Nat_big_num.sub_nat ( Nat_big_num.mul(Nat_big_num.of_int 65536)(Nat_big_num.of_int 65536))(Nat_big_num.of_int 1)) in (* 0xffffffffL *) - Ml_bindings.nat_big_num_of_uint64 (Uint64.logand w (Uint64.of_string (Nat_big_num.to_string magic)))) - -(* Accessors *) - -(*val get_elf32_relocation_r_sym : elf32_relocation -> natural*) -let get_elf32_relocation_r_sym r:Nat_big_num.num= - (extract_elf32_relocation_r_sym r.elf32_r_info) - -(*val get_elf32_relocation_a_sym : elf32_relocation_a -> natural*) -let get_elf32_relocation_a_sym r:Nat_big_num.num= - (extract_elf32_relocation_r_sym r.elf32_ra_info) - -(*val get_elf64_relocation_sym : elf64_relocation -> natural*) -let get_elf64_relocation_sym r:Nat_big_num.num= - (extract_elf64_relocation_r_sym r.elf64_r_info) - -(*val get_elf64_relocation_a_sym : elf64_relocation_a -> natural*) -let get_elf64_relocation_a_sym r:Nat_big_num.num= - (extract_elf64_relocation_r_sym r.elf64_ra_info) - -(*val get_elf32_relocation_type : elf32_relocation -> natural*) -let get_elf32_relocation_type r:Nat_big_num.num= - (extract_elf32_relocation_r_type r.elf32_r_info) - -(*val get_elf32_relocation_a_type : elf32_relocation_a -> natural*) -let get_elf32_relocation_a_type r:Nat_big_num.num= - (extract_elf32_relocation_r_type r.elf32_ra_info) - -(*val get_elf64_relocation_type : elf64_relocation -> natural*) -let get_elf64_relocation_type r:Nat_big_num.num= - (extract_elf64_relocation_r_type r.elf64_r_info) - -(*val get_elf64_relocation_a_type : elf64_relocation_a -> natural*) -let get_elf64_relocation_a_type r:Nat_big_num.num= - (extract_elf64_relocation_r_type r.elf64_ra_info) - - -(** Reading relocation entries *) - -(** [read_elf32_relocation ed bs0] parses an [elf32_relocation] record from - * byte sequence [bs0] assuming endianness [ed]. The suffix of [bs0] remaining - * after parsing is also returned. - * Fails if the relocation record cannot be parsed. - *) -(*val read_elf32_relocation : endianness -> byte_sequence -> - error (elf32_relocation * byte_sequence)*) -let read_elf32_relocation endian bs:(elf32_relocation*byte_sequence)error= - (read_elf32_addr endian bs >>= (fun (r_offset, bs) -> - read_elf32_word endian bs >>= (fun (r_info, bs) -> - return ({ elf32_r_offset = r_offset; elf32_r_info = r_info }, bs)))) - -(** [read_elf64_relocation ed bs0] parses an [elf64_relocation] record from - * byte sequence [bs0] assuming endianness [ed]. The suffix of [bs0] remaining - * after parsing is also returned. - * Fails if the relocation record cannot be parsed. - *) -(*val read_elf64_relocation : endianness -> byte_sequence -> - error (elf64_relocation * byte_sequence)*) -let read_elf64_relocation endian bs:(elf64_relocation*byte_sequence)error= - (read_elf64_addr endian bs >>= (fun (r_offset, bs) -> - read_elf64_xword endian bs >>= (fun (r_info, bs) -> - return ({ elf64_r_offset = r_offset; elf64_r_info = r_info }, bs)))) - -(** [read_elf32_relocation_a ed bs0] parses an [elf32_relocation_a] record from - * byte sequence [bs0] assuming endianness [ed]. The suffix of [bs0] remaining - * after parsing is also returned. - * Fails if the relocation record cannot be parsed. - *) -(*val read_elf32_relocation_a : endianness -> byte_sequence -> - error (elf32_relocation_a * byte_sequence)*) -let read_elf32_relocation_a endian bs:(elf32_relocation_a*byte_sequence)error= - (read_elf32_addr endian bs >>= (fun (r_offset, bs) -> - read_elf32_word endian bs >>= (fun (r_info, bs) -> - read_elf32_sword endian bs >>= (fun (r_addend, bs) -> - return ({ elf32_ra_offset = r_offset; elf32_ra_info = r_info; - elf32_ra_addend = r_addend }, bs))))) - -(** [read_elf64_relocation_a ed bs0] parses an [elf64_relocation_a] record from - * byte sequence [bs0] assuming endianness [ed]. The suffix of [bs0] remaining - * after parsing is also returned. - * Fails if the relocation record cannot be parsed. - *) -(*val read_elf64_relocation_a : endianness -> byte_sequence -> error (elf64_relocation_a * byte_sequence)*) -let read_elf64_relocation_a endian bs:(elf64_relocation_a*byte_sequence)error= - (read_elf64_addr endian bs >>= (fun (r_offset, bs) -> - read_elf64_xword endian bs >>= (fun (r_info, bs) -> - read_elf64_sxword endian bs >>= (fun (r_addend, bs) -> - return ({ elf64_ra_offset = r_offset; elf64_ra_info = r_info; - elf64_ra_addend = r_addend }, bs))))) - -(** [read_elf32_relocation_section' ed bs0] parses a list of [elf32_relocation] - * records from byte sequence [bs0], which is assumed to have the exact size - * required, assuming endianness [ed]. - * Fails if any of the records cannot be parsed. - *) -(*val read_elf32_relocation_section' : endianness -> byte_sequence -> - error (list elf32_relocation)*) -let rec read_elf32_relocation_section' endian bs0:((elf32_relocation)list)error= - (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 0) then - return [] - else - read_elf32_relocation endian bs0 >>= (fun (entry, bs1) -> - read_elf32_relocation_section' endian bs1 >>= (fun tail -> - return (entry::tail)))) - -(** [read_elf64_relocation_section' ed bs0] parses a list of [elf64_relocation] - * records from byte sequence [bs0], which is assumed to have the exact size - * required, assuming endianness [ed]. - * Fails if any of the records cannot be parsed. - *) -(*val read_elf64_relocation_section' : endianness -> byte_sequence -> - error (list elf64_relocation)*) -let rec read_elf64_relocation_section' endian bs0:((elf64_relocation)list)error= - (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 0) then - return [] - else - read_elf64_relocation endian bs0 >>= (fun (entry, bs1) -> - read_elf64_relocation_section' endian bs1 >>= (fun tail -> - return (entry::tail)))) - -(** [read_elf32_relocation_a_section' ed bs0] parses a list of [elf32_relocation_a] - * records from byte sequence [bs0], which is assumed to have the exact size - * required, assuming endianness [ed]. - * Fails if any of the records cannot be parsed. - *) -(*val read_elf32_relocation_a_section' : endianness -> byte_sequence -> - error (list elf32_relocation_a)*) -let rec read_elf32_relocation_a_section' endian bs0:((elf32_relocation_a)list)error= - (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 0) then - return [] - else - read_elf32_relocation_a endian bs0 >>= (fun (entry, bs1) -> - read_elf32_relocation_a_section' endian bs1 >>= (fun tail -> - return (entry::tail)))) - -(** [read_elf64_relocation_a_section' ed bs0] parses a list of [elf64_relocation_a] - * records from byte sequence [bs0], which is assumed to have the exact size - * required, assuming endianness [ed]. - * Fails if any of the records cannot be parsed. - *) -(*val read_elf64_relocation_a_section' : endianness -> byte_sequence -> - error (list elf64_relocation_a)*) -let rec read_elf64_relocation_a_section' endian bs0:((elf64_relocation_a)list)error= - (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 0) then - return [] - else - read_elf64_relocation_a endian bs0 >>= (fun (entry, bs1) -> - read_elf64_relocation_a_section' endian bs1 >>= (fun tail -> - return (entry::tail)))) - -(** [read_elf32_relocation_section sz ed bs0] reads in a list of [elf32_relocation] - * records from a prefix of [bs0] of size [sz] assuming endianness [ed]. The - * suffix of [bs0] remaining after parsing is also returned. - * Fails if any of the records cannot be parsed or if the length of [bs0] is - * less than [sz]. - *) -(*val read_elf32_relocation_section : natural -> endianness -> byte_sequence - -> error (list elf32_relocation * byte_sequence)*) -let read_elf32_relocation_section table_size endian bs0:((elf32_relocation)list*byte_sequence)error= - (partition0 table_size bs0 >>= (fun (eat, rest) -> - read_elf32_relocation_section' endian eat >>= (fun entries -> - return (entries, rest)))) - -(** [read_elf64_relocation_section sz ed bs0] reads in a list of [elf64_relocation] - * records from a prefix of [bs0] of size [sz] assuming endianness [ed]. The - * suffix of [bs0] remaining after parsing is also returned. - * Fails if any of the records cannot be parsed or if the length of [bs0] is - * less than [sz]. - *) -(*val read_elf64_relocation_section : natural -> endianness -> byte_sequence - -> error (list elf64_relocation * byte_sequence)*) -let read_elf64_relocation_section table_size endian bs0:((elf64_relocation)list*byte_sequence)error= - (partition0 table_size bs0 >>= (fun (eat, rest) -> - read_elf64_relocation_section' endian eat >>= (fun entries -> - return (entries, rest)))) - -(** [read_elf32_relocation_a_section sz ed bs0] reads in a list of [elf32_relocation_a] - * records from a prefix of [bs0] of size [sz] assuming endianness [ed]. The - * suffix of [bs0] remaining after parsing is also returned. - * Fails if any of the records cannot be parsed or if the length of [bs0] is - * less than [sz]. - *) -(*val read_elf32_relocation_a_section : natural -> endianness -> byte_sequence -> - error (list elf32_relocation_a * byte_sequence)*) -let read_elf32_relocation_a_section table_size endian bs0:((elf32_relocation_a)list*byte_sequence)error= - (partition0 table_size bs0 >>= (fun (eat, rest) -> - read_elf32_relocation_a_section' endian eat >>= (fun entries -> - return (entries, rest)))) - -(** [read_elf64_relocation_a_section sz ed bs0] reads in a list of [elf64_relocation_a] - * records from a prefix of [bs0] of size [sz] assuming endianness [ed]. The - * suffix of [bs0] remaining after parsing is also returned. - * Fails if any of the records cannot be parsed or if the length of [bs0] is - * less than [sz]. - *) -(*val read_elf64_relocation_a_section : natural -> endianness -> byte_sequence -> - error (list elf64_relocation_a * byte_sequence)*) -let read_elf64_relocation_a_section table_size endian bs0:((elf64_relocation_a)list*byte_sequence)error= - (partition0 table_size bs0 >>= (fun (eat, rest) -> - read_elf64_relocation_a_section' endian eat >>= (fun entries -> - return (entries, rest)))) |