Source file elf64_file_of_elf_memory_image.ml

(*Generated by Lem from elf64_file_of_elf_memory_image.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_map
(*import Set*)
open Lem_num
open Lem_maybe
open Lem_assert_extra

open Byte_pattern
open Byte_sequence
open Default_printing
open Error
open Missing_pervasives
open Show
open Endianness

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

open Memory_image
open Memory_image_orderings

open Elf_memory_image
open Elf_memory_image_of_elf64_file
open Abis

(* Things the caller should do first: *)
(* - create segment annotations *)
(* - create .dynamic-equivalent metadata (but not the section) *)
(* - concretise symbolic elements? actually they pass a function to do this. *)

type make_concrete_fn = Memory_image.element -> Memory_image.element

(* Things we do, at the caller's direction:*)
(* - create SHT *)
(* - create symtabs, strtabs, symbol hash tables (the ABI helps us) *)
(* - create shstrtab (if we're creating a SHT) *)
(* - actually create the dynamic section (and its PHDR) *)
(* - create any other PHDRs (the ABI tells us, mostly) and PT_PHDR (the user tells us) *)

(*val elf64_file_of_elf_memory_image : abi any_abi_feature -> make_concrete_fn -> string -> elf_memory_image -> elf64_file*)
let elf64_file_of_elf_memory_image a make_concrete fname1 img2:elf64_file=
     (
    (* Generate an ELF header, (optionally) SHT and (optionally) PHT,
     * based on metadata in the image.
     *
     * How do we decide what kind of ELF file to generate?     see whether we have segment annotations?
                        what architecture/osabi to give?       the ABI tells us

     *)let (section_tags, section_ranges) = (elf_memory_image_section_ranges img2)
    in
    let section_tags_bare = (Lem_list.map (fun tag ->
        (match tag with
            | FileFeature(ElfSection(idx1, isec1)) -> (idx1, isec1)
            | _ -> failwith "not section tag"
        )) section_tags)
    in
    let section_tags_bare_noidx = (Lem_list.map (fun (idx1, isec1) -> isec1) section_tags_bare)
    in
    let basic_shstrtab = (List.fold_left (fun table -> (fun str ->
        let (_, t) = (String_table.insert_string str table) in t
    )) String_table.empty0 [".shstrtab"; ".symtab"; ".strtab"])
    in
    let shstrtab = (List.fold_left (fun table -> fun (idx1, isec1) ->
        let (_, t) = (String_table.insert_string isec1.elf64_section_name_as_string table) in
        (* let _ = errln ("Adding section name `" ^ isec.elf64_section_name_as_string ^ "' to shstrtab; now has size "
            ^ (show (String_table.size t)))
        in *) t
    ) basic_shstrtab section_tags_bare)
    in
    let phoff =( (Nat_big_num.of_int 64))
    in
    let max_phnum1 = ( (* length phdrs *)a.max_phnum)
    in
        (* what do we generate?
         * .eh_frame? no, *should* come from the script
         * .got, .got.plt? HMM. These should have been created,
         * as ABI features, by the time we get here.
         * .comment -- maybe
         * .shstrtab -- YES
         * .symtab -- YES
         * .strtab -- YES.
         *
         * Do we generate them as elements in the image, or just
         * use them to write the ELF file? The latter.
         *)
    let (symbol_tags, symbol_ranges) = (elf_memory_image_symbol_def_ranges img2)
    in
    let all_sym_names = (Lem_list.map (fun tag ->
        (match tag with
            SymbolDef(sd) -> sd.def_symname
            | _ -> "not symbol tag, in symbol tags"
        )
    ) symbol_tags)
    in
    (*let _ = errln ("All symbol names: " ^ (show all_sym_names))
    in*)
    let strtab = (List.fold_left (fun table -> fun str ->
        let (_, t) = (String_table.insert_string str table) in t
    ) String_table.empty0 all_sym_names)
    in
    (* If the same address starts >1 section, all but one of those sections
     * must have size zero. These need to come *first* to avoid screwing up
     * the offset calculation. So also sort by size, so that the zero-sizers
     * come first. *)
    let element_section_tag_pairs_sorted_by_address = ( (* List.stable_sort *)List.sort
        (fun (isec1, (el1, range1)) -> (fun (isec2, (el2, range2)) -> (
            let (addr1, sz1) = ((match Pmap.lookup el1 img2.elements with
                Some(e) ->
                    (*let _ = errln ("Size of element " ^ el1 ^ " is " ^ (show e.length))
                    in*)
                    (e.startpos, e.length1)
                | None -> failwith "internal error: element does not exist"
            ))
            in
            let (addr2, sz2) = ((match Pmap.lookup el2 img2.elements with
                Some(e) -> (e.startpos, e.length1)
                | None -> failwith "internal error: element does not exist"
            ))
            in
            (pairCompare (maybeCompare Nat_big_num.compare) (maybeCompare Nat_big_num.compare) (addr1, sz1) (addr2, sz2))
        )))
    (list_combine section_tags_bare_noidx section_ranges))
    in
    let sorted_sections = (Lem_list.map (fun (isec1, (el, range1)) -> isec1)
        element_section_tag_pairs_sorted_by_address)
    in
    let filesz = (fun el -> fun isec1 ->
        (* How can we distinguish progbits from nobits?
         * A section can be nobits if its representation
         * is all zero or don't-care. But in practice we
         * don't make a section nobits unless its name is .bss. *)
        let sz = (if (* is_all_zeroes_or_dont_care *) true &&
            (isec1.elf64_section_name_as_string = ".bss") then  (Nat_big_num.of_int 0)
            else (match el.length1 with
                None -> failwith "error: concrete section element has no length"
                | Some len -> len
            ))
        in
        (*let _ = errln ("Filesz of " ^ isec.elf64_section_name_as_string ^ " is 0x" ^ (hex_string_of_natural sz))
        in*)
        sz
    )
    in
    let (last_off, section_file_offsets) = (List.fold_left (fun (current_off, offs_so_far) -> (fun (isec1, (el_name, el_range)) ->
        (* where can we place this in the file?
         * it's the next offset that's congruent to the section addr,
         * modulo the biggest page size. *)
        let el = ((match Pmap.lookup el_name img2.elements with
            Some e -> e
            | None -> failwith "nonexistent element"
        ))
        in
        let (start_off : Nat_big_num.num) =  ((match el.startpos with
            Some addr -> let this_remainder = (Nat_big_num.modulus current_off a.maxpagesize)
                in
                let target_remainder = (Nat_big_num.modulus addr a.maxpagesize)
                in
                let bump = (
                    if Nat_big_num.greater_equal target_remainder this_remainder
                    then Nat_big_num.sub_nat target_remainder this_remainder
                    else ( Nat_big_num.sub_nat (Nat_big_num.add a.maxpagesize target_remainder) this_remainder)
                )
                in Nat_big_num.add
                (*let _ = errln ("For section " ^ isec.elf64_section_name_as_string ^ ", bumping offset by " ^
                    (hex_string_of_natural bump) ^ "(remainder " ^ (hex_string_of_natural this_remainder) ^
                    ", target remainder " ^ (hex_string_of_natural target_remainder) ^ ") to 0x" ^
                    (hex_string_of_natural (current_off + bump)))
                in*)
                current_off bump
            | None ->
                (* It has no assigned address. That's okay if it's not allocatable.
                 * If it's not allocatable, it has no alignment. *)
                if flag_is_set shf_alloc isec1.elf64_section_flags then (failwith "allocatable section with no address")
                else current_off (* FIXME: is alignment important in file-offset-space? *)
        ))
        in
        let end_off = (Nat_big_num.add start_off (filesz el isec1))
        in
        (end_off,  List.rev_append (List.rev offs_so_far) [start_off])
    )) (( Nat_big_num.add phoff ( Nat_big_num.mul max_phnum1( (Nat_big_num.of_int 56)))), []) element_section_tag_pairs_sorted_by_address)
    in
    let user_sections_sorted_with_offsets = (let x2 = 
  ([]) in  List.fold_right
   (fun(off, (isec1, (el_name, el_range))) x2 ->
    if true then
      (let el = ((match Pmap.lookup el_name img2.elements with
                     Some x -> x
                   | None -> failwith "internal error: section not found"
                 )) in
       { elf64_section_name = (isec1.elf64_section_name) (* ignored *)
       ; elf64_section_type = (isec1.elf64_section_type)
       ; elf64_section_flags = (isec1.elf64_section_flags)
       ; elf64_section_addr = ((match el.startpos with
                                   Some addr -> addr
                                 | None -> (Nat_big_num.of_int 0)
                               )) ; elf64_section_offset =
       (*let _ = errln ("Assigning offset 0x" ^ (hex_string_of_natural off) ^ " to section " ^
                    isec.elf64_section_name_as_string)
                in*)
       off
       ; elf64_section_size = ((match el.length1 with
                                   Some len -> len
                                 | None -> length el.contents
                               ))
       ; elf64_section_link = (isec1.elf64_section_link)
       ; elf64_section_info = (isec1.elf64_section_info)
       ; elf64_section_align = (isec1.elf64_section_align)
       ; elf64_section_entsize = (isec1.elf64_section_entsize)
       ; elf64_section_body =
       (let pad_fn1 = (
                      if flag_is_set shf_execinstr isec1.elf64_section_flags then
                        a.pad_data else a.pad_code) in
        concretise_byte_pattern (make_concrete el).contents pad_fn1)
       ; elf64_section_name_as_string = (isec1.elf64_section_name_as_string)
       }) :: x2 else x2)
   (list_combine section_file_offsets
      element_section_tag_pairs_sorted_by_address) x2)
    in
    let symtab =
        (
        (* Get all the symbols *)elf64_null_symbol_table_entry :: (let x2 = 
  ([]) in  List.fold_right
   (fun(maybe_range, tag) x2 ->
    if true then
      (match tag with
          SymbolDef (d) ->
      let nameidx = ((match String_table.find_string d.def_symname strtab with
                         Some idx1 -> let v = (Uint32_wrapper.of_bigint idx1)
                                      in
                                      (* let _ = errln ("strtab: found `" ^ d.def_symname ^ "' at index " ^ (show v))
                                        in *)
                                      v
                       | None -> failwith
                                   "impossible: symbol name not in strtab we just created"
                     )) in
      let (shndx1, svalue, sz) = (
                                 if d.def_syment.elf64_st_shndx =
                                      Uint32_wrapper.of_bigint shn_abs then
                                   (d.def_syment.elf64_st_shndx, d.def_syment.elf64_st_value, d.def_syment.elf64_st_size)
                                 else
                                   let (el_name, (start, len)) = ((match maybe_range with
                                                                    Some(el_name, (start, len)) -> 
                                                                  (el_name, 
                                                                  (start, len))
                                                                    | None -> 
                                                                  failwith
                                                                    "impossible: non-ABS symbol with no range"
                                                                  )) in
                                   (Uint32_wrapper.of_bigint
                                      ( (* what's the section index of this element? *)
                                        let maybe_found = (mapMaybei
                                                             (fun i -> fun isec1 ->
                                                              if isec1.elf64_section_name_as_string
                                                                   = 
                                                                 el_name then
                                                                Some i else
                                                                None)
                                                             sorted_sections)
                                        in
                                        (match maybe_found with
                                            [i] -> Nat_big_num.add
                                                     ( (Nat_big_num.of_int 1))
                                                     i
                                          | [] ->
                                                   (* HMM *) (*let _ = errln ("Couldn't compute section index of symbol " ^ d.def_symname)
                                            in*) (Nat_big_num.of_int 0)
                                          | _ -> failwith
                                                   ("internal error: multiple sections named "
                                                      ^ el_name)
                                        ) ),
                                   Uint64_wrapper.of_bigint
                                     ( Nat_big_num.add start
                                         (match Pmap.lookup el_name
                                                  img2.elements with
                                             Some x -> (match x.startpos with
                                                           Some addr -> 
                                                       addr
                                                         | None -> failwith
                                                                    "internal error: symbol defined in section with no address"
                                                       )
                                           | None -> failwith
                                                       "internal error: section (of symbol) not found"
                                         )), Uint64_wrapper.of_bigint len ))
      in
      (* CHECK: can we expect these to be these usable, the way we generated them?  *)
      { elf64_st_name = nameidx
      ; elf64_st_info = (d.def_syment.elf64_st_info) (* type, binding, visibility *)
      ; elf64_st_other = (d.def_syment.elf64_st_other)
      ; elf64_st_shndx = shndx1 ; elf64_st_value = svalue
      ; elf64_st_size = sz }
      (* FIXME: do we ever get symbolrefs? *)
        | _ -> failwith "not a symbol tag, in symbol_tags"
      ) :: x2 else x2) (list_combine symbol_ranges symbol_tags) x2))
    in
    (*let _ = errln ("Building an ELF file from" ^ (show (length element_section_tag_pairs_sorted_by_address)) ^ " sections")
    in*)
    (* PROBLEM:
     * sections' offset assignments depend on phnum.
     * BUT
     * phnum depends on sections' offset assignments!
     * How do we break this cycle?
     * We can get an upper bound on the number of phdrs, then
     * fill them in later.
     *)
    (* How does the GNU BFD output a statically linked executable?
     * First the ELF header,
     * then program headers,
     * then sections in order of address:
     *      .interp,                 these are all allocatable sections! with addresses!
     * then .note.ABI-tag,
     * then .note.gnu.build-id,
     * then .gnu.hash,
     * then .dynsym,
     * then .dynstr,
     * then .gnu.version,
     * then .gnu.version_r,
     * then ...
     *
     * ... and so on ...
     *
     * then .gnu.debuglink (the only non-allocatable section)
     * then .shstrtab, then SHT.
     *
     * So how can we calculate the offset of the SHT?  We have to place
     * all the other sections first.
     *)
    let shstrndx = (Nat_big_num.add( (Nat_big_num.of_int 1)) (length section_tags))
    in
    let shstroff = last_off
    in
    let shstrsz = (String_table.size0 shstrtab)
    in
    let symoff = (align_up_to( (Nat_big_num.of_int 8)) ( Nat_big_num.add shstroff shstrsz))
    in
    let symsz = (Nat_big_num.mul( (Nat_big_num.of_int 24)) (length symtab))
    in
    let stroff = (Nat_big_num.add symoff symsz)
    in
    let strsz = (String_table.size0 strtab)
    in
    let shoff = (align_up_to( (Nat_big_num.of_int 64)) ( Nat_big_num.add stroff strsz))
    in
    let shnum = (Nat_big_num.add( (Nat_big_num.of_int 4)) (length sorted_sections)) (* null, shstrtab, symtab, strtab *)
    in
    let (entry : Nat_big_num.num) = ((match Multimap.lookupBy0 
  (instance_Basic_classes_Ord_Memory_image_range_tag_dict
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict
   (instance_Basic_classes_Ord_tup2_dict
      Lem_string_extra.instance_Basic_classes_Ord_string_dict
      (instance_Basic_classes_Ord_tup2_dict
         instance_Basic_classes_Ord_Num_natural_dict
         instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (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)))  (Memory_image_orderings.tagEquiv
    instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (EntryPoint) img2.by_tag with
        [(_, maybe_el_range)] ->
            (match maybe_el_range with
                Some (el_name, (start, len)) ->
                    address_of_range (el_name, (start, len)) img2
                | None -> failwith "entry point defined without a range"
            )
       | [] -> failwith "no entry point defined"
       | _ -> failwith "multiple entry points defined"
    ))
    in
    let hdr = (a.make_elf_header elf_ft_exec entry shoff phoff max_phnum1 shnum shstrndx)
    in
    let endian = (if (Lem.option_equal (=) (Ml_bindings.list_index_big_int elf_ii_data hdr.elf64_ident) (Some(Uint32_wrapper.of_bigint elf_data_2lsb))) then Little else Big)
    in
    let all_sections_sorted_with_offsets =  (List.rev_append (List.rev user_sections_sorted_with_offsets) [
          { elf64_section_name = ((match String_table.find_string ".shstrtab" shstrtab with
                                    Some n -> n
                                    | None -> failwith "internal error: `.shstrtab' not in shstrtab"
                                ))
           ; elf64_section_type = sht_strtab
           ; elf64_section_flags =( (Nat_big_num.of_int 0))
           ; elf64_section_addr =( (Nat_big_num.of_int 0))
           ; elf64_section_offset = shstroff
           ; elf64_section_size = shstrsz
           ; 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 0))
           ; elf64_section_entsize =( (Nat_big_num.of_int 0))
           (* TODO: don't use lists of bytes here! *)
           ; elf64_section_body = (byte_sequence_of_byte_list (Lem_list.map (fun x-> x) (Xstring.explode (String_table.get_base_string shstrtab))))
           ; elf64_section_name_as_string = ".shstrtab"
           };
          { elf64_section_name      = ((match String_table.find_string ".symtab" shstrtab with
                                    Some n -> n
                                    | None -> failwith "internal error: `.symtab' not in shstrtab"
                                ))
           ; elf64_section_type      = sht_symtab
           ; elf64_section_flags     =( (Nat_big_num.of_int 0))
           ; elf64_section_addr      =( (Nat_big_num.of_int 0))
           ; elf64_section_offset    = symoff
           ; elf64_section_size      = symsz
           ; elf64_section_link      = (Nat_big_num.add (Nat_big_num.add( (Nat_big_num.of_int 1)) (length user_sections_sorted_with_offsets))( (Nat_big_num.of_int 2)))
           ; elf64_section_info      =( (Nat_big_num.of_int 0))
           ; elf64_section_align =( (Nat_big_num.of_int 8))
           ; elf64_section_entsize   =( (Nat_big_num.of_int 24))
           ; elf64_section_body = (Byte_sequence.concat (Lem_list.map (bytes_of_elf64_symbol_table_entry endian) symtab))
           ; elf64_section_name_as_string = ".symtab"
           };
          (* strtab *)
          { elf64_section_name      = ((match String_table.find_string ".strtab" shstrtab with
                                    Some n -> n
                                    | None -> failwith "internal error: `.strtab' not in shstrtab"
                                ))
           ; elf64_section_type      = sht_strtab
           ; elf64_section_flags     =( (Nat_big_num.of_int 0))
           ; elf64_section_addr      =( (Nat_big_num.of_int 0))
           ; elf64_section_offset    = stroff
           ; elf64_section_size      = strsz
           ; 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 1))
           ; elf64_section_entsize   =( (Nat_big_num.of_int 0))
           (* TODO: don't use lists of bytes here! *)
           ; elf64_section_body = (byte_sequence_of_byte_list (Lem_list.map (fun x-> x) (Xstring.explode (String_table.get_base_string strtab))))
           ; elf64_section_name_as_string = ".strtab"
           }
        ])
    in
    let phdrs = (a.make_phdrs a.maxpagesize a.commonpagesize elf_ft_exec img2 all_sections_sorted_with_offsets)
    in
    { elf64_file_header               = ({ (* fix up hdr with the precise phnum *)
         elf64_ident = (hdr.elf64_ident)
       ; elf64_type = (hdr.elf64_type)
       ; elf64_machine = (hdr.elf64_machine)
       ; elf64_version = (hdr.elf64_version)
       ; elf64_entry = (hdr.elf64_entry)
       ; elf64_phoff = (hdr.elf64_phoff)
       ; elf64_shoff = (hdr.elf64_shoff)
       ; elf64_flags = (hdr.elf64_flags)
       ; elf64_ehsize = (hdr.elf64_ehsize)
       ; elf64_phentsize = (hdr.elf64_phentsize)
       ; elf64_phnum = (Uint32_wrapper.of_bigint (length phdrs))
       ; elf64_shentsize = (hdr.elf64_shentsize)
       ; elf64_shnum = (hdr.elf64_shnum)
       ; elf64_shstrndx = (hdr.elf64_shstrndx)
        })
     ; elf64_file_program_header_table = phdrs
     ; elf64_file_section_header_table = (elf64_null_section_header :: ((Lem_list.mapi (fun i -> fun isec1 ->
          { elf64_sh_name      = (let s = (isec1.elf64_section_name_as_string) in
                                (match String_table.find_string s shstrtab with
                                    Some n -> Uint32_wrapper.of_bigint n
                                    | None -> failwith ("internal error: section name `" ^ (s ^ "' not in shstrtab"))
                                ))
           ; elf64_sh_type      = (Uint32_wrapper.of_bigint isec1.elf64_section_type)
           ; elf64_sh_flags     = (Uint64_wrapper.of_bigint isec1.elf64_section_flags)
           ; elf64_sh_addr      = (Uint64_wrapper.of_bigint isec1.elf64_section_addr)
           ; elf64_sh_offset    = (Uint64_wrapper.of_bigint isec1.elf64_section_offset)
           ; elf64_sh_size      = (Uint64_wrapper.of_bigint isec1.elf64_section_size)
           ; elf64_sh_link      = (Uint32_wrapper.of_bigint isec1.elf64_section_link)
           ; elf64_sh_info      = (Uint32_wrapper.of_bigint isec1.elf64_section_info)
           ; elf64_sh_addralign = (Uint64_wrapper.of_bigint isec1.elf64_section_align)
           ; elf64_sh_entsize   = (Uint64_wrapper.of_bigint isec1.elf64_section_entsize)
           }
     )) (* (zip section_tags_bare section_file_offsets) *) all_sections_sorted_with_offsets))
     ; elf64_file_interpreted_segments = ([
            (* do we need to build this? I have HACKed elf_file so that we don't;
               we assume that all the relevant payload is in the section bodies,
               as it should be. *)
        ])
     ; elf64_file_interpreted_sections = (null_elf64_interpreted_section :: all_sections_sorted_with_offsets)
     ; elf64_file_bits_and_bobs        = ([])
     })