Source file gnu_ext_abi.ml

(*Generated by Lem from gnu_extensions/gnu_ext_abi.lem.*)
open Lem_basic_classes
open Lem_function
open Lem_string
open Lem_tuple
open Lem_bool
open Lem_list
open Lem_sorting
open Lem_num
open Lem_maybe
open Lem_assert_extra
open Show
open Missing_pervasives

open Byte_sequence

(* open import Abis *)

open Elf_file
open Elf_header
open Elf_interpreted_segment
open Elf_interpreted_section
open Elf_program_header_table
open Elf_section_header_table
open Elf_symbol_table
open Elf_types_native_uint
open Elf_relocation
open Elf_types_native_uint
open Memory_image

(** Optional, like [stt_func] but always points to a function or piece of
  * executable code that takes no arguments and returns a function pointer.
  *)
let stt_gnu_ifunc : Nat_big_num.num= ( (Nat_big_num.of_int 10))

(*val gnu_extend: forall 'abifeature. abi 'abifeature -> abi 'abifeature*)
let gnu_extend a:'abifeature abi=
    ({ is_valid_elf_header = (a.is_valid_elf_header)
    ; make_elf_header     =
            ( (*  t -> entry -> shoff -> phoff -> phnum -> shnum -> shstrndx -> hdr *)fun t -> fun entry -> fun shoff -> fun phoff -> fun phnum -> fun shnum -> fun shstrndx ->
            let unmod = (a.make_elf_header t entry shoff phoff phnum shnum shstrndx)
            in
              { elf64_ident    = ((match unmod.elf64_ident with
                i0 :: i1 :: i2 :: i3  :: i4  :: i5  :: i6  ::
                _  :: _  :: i9 :: i10 :: i11 :: i12 :: i13 :: i14 :: i15 :: []
                    -> [i0; i1; i2; i3; i4; i5; i6;
                        Uint32_wrapper.of_bigint elf_osabi_gnu;
                        Uint32_wrapper.of_bigint( (Nat_big_num.of_int 1));
                        i9; i10; i11; i12; i13; i14; i15]
                ))
               ; elf64_type     = (Uint32_wrapper.of_bigint t)
               ; elf64_machine  = (unmod.elf64_machine)
               ; elf64_version  = (unmod.elf64_version)
               ; elf64_entry    = (unmod.elf64_entry)
               ; elf64_phoff    = (Uint64_wrapper.of_bigint phoff)
               ; elf64_shoff    = (Uint64_wrapper.of_bigint shoff)
               ; elf64_flags    = (unmod.elf64_flags)
               ; elf64_ehsize   = (unmod.elf64_ehsize)
               ; elf64_phentsize= (unmod.elf64_phentsize)
               ; elf64_phnum    = (Uint32_wrapper.of_bigint phnum)
               ; elf64_shentsize= (unmod.elf64_shentsize)
               ; elf64_shnum    = (Uint32_wrapper.of_bigint shnum)
               ; elf64_shstrndx = (Uint32_wrapper.of_bigint shstrndx)
               })
    ; reloc               = (a.reloc)
    ; section_is_special  = (fun isec1 -> (fun img2 -> (
                                a.section_is_special isec1 img2
                                || (
                                 (Lem.option_equal (=)(Ml_bindings.string_prefix (Nat_big_num.of_int (String.length ".gnu.warning")) isec1.elf64_section_name_as_string) (Some(".gnu.warning"))))
        (* FIXME: This is a slight abuse. The GNU linker's treatment of
         * ".gnu.warning.*" section is not really a function of the output
         * ABI -- it's a function of the input ABI, or arguably perhaps just
         * of the linker itself. We have to do something to make sure these
         * sections get silently processed separately from the usual linker
         * control script, because otherwise our link map output doesn't match
         * the GNU linker's. By declaring these sections "special" we achieve
         * this by saying they don't participate in linking proper, just like
         * ".symtab" and similar sections don't. HMM. I suppose this is
         * okay, in that although a non-GNU linker might happily link these
         * sections, arguably that is a failure to understand the input files.
         * But the issue about it being a per-input-file property remains.
         * Q. What does the GNU linker do if a reloc input file whose OSABI
         * is *not* GNU contains a .gnu.warning.* section? That would be a fair
         * test about whether looking at the input ABI is worth doing. *)
                            )))
    ; section_is_large    = (a.section_is_large)
    ; maxpagesize         = (a.maxpagesize)
    ; minpagesize         = (a.minpagesize)
    ; commonpagesize      = (a.commonpagesize)
    ; symbol_is_generated_by_linker = (a.symbol_is_generated_by_linker)
    ; make_phdrs          = (a.make_phdrs) (* FIXME: also make the GNU phdrs! *)
    ; max_phnum           = (Nat_big_num.add( (Nat_big_num.of_int 1)) a.max_phnum) (* FIXME: GNU_RELRO, GNU_STACK; what else? *)
    ; guess_entry_point   = (a.guess_entry_point)
    ; pad_data            = (a.pad_data)
    ; pad_code            = (a.pad_code)
    ; generate_support    = (fun input_fnames_and_imgs ->
        let vanilla_support_img = (a.generate_support input_fnames_and_imgs) in
        (* also generate .note.gnu.build-id *)
        let new_by_range = (Pset.add (Some(".note.gnu.build-id", ( (Nat_big_num.of_int 0), (Nat_big_num.of_int 24))), FileFeature(ElfSection( (Nat_big_num.of_int 4) (* HACK: calculate this *),
          { elf64_section_name =( (Nat_big_num.of_int 0)) (* ignored *)
           ; elf64_section_type = sht_note
           ; elf64_section_flags = shf_alloc
           ; elf64_section_addr =( (Nat_big_num.of_int 0)) (* ignored -- covered by element *)
           ; elf64_section_offset =( (Nat_big_num.of_int 0)) (* ignored -- will be replaced when file offsets are assigned *)
           ; elf64_section_size =( (Nat_big_num.of_int 24)) (* ignored? NO, we use it in linker_script to avoid plumbing through the element record *)
           ; elf64_section_link =( (Nat_big_num.of_int 0))
           ; elf64_section_info =( (Nat_big_num.of_int 0))
           ; elf64_section_align =( (Nat_big_num.of_int 4))
           ; elf64_section_entsize =( (Nat_big_num.of_int 0))
           ; elf64_section_body = Byte_sequence.empty (* ignored *)
           ; elf64_section_name_as_string = ".note.gnu.build-id"
           }
        ))) vanilla_support_img.by_range)
        in
        {  elements = (Pmap.add ".note.gnu.build-id" {
                startpos = None
           ;    length1 = (Some( (Nat_big_num.of_int 24)))
           ;    contents = ([])
           } (vanilla_support_img.elements))
         ;   by_tag = (by_tag_from_by_range 
  (instance_Basic_classes_SetType_Maybe_maybe_dict
     (instance_Basic_classes_SetType_tup2_dict
        instance_Basic_classes_SetType_var_dict
        (instance_Basic_classes_SetType_tup2_dict
           instance_Basic_classes_SetType_Num_natural_dict
           instance_Basic_classes_SetType_Num_natural_dict))) instance_Basic_classes_SetType_var_dict new_by_range)
         ;   by_range = new_by_range
         })
    ; concretise_support  = (a.concretise_support)
    ; get_reloc_symaddr   = (a.get_reloc_symaddr)
    ; parse_reloc_info    = (a.parse_reloc_info)
    })