Source file elf_memory_image.ml

(*Generated by Lem from 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_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 Abis

type elf_memory_image = any_abi_feature annotated_memory_image

let elf_section_is_special0 s f:bool=  (not (Nat_big_num.equal s.elf64_section_type sht_progbits)
                     && not (Nat_big_num.equal s.elf64_section_type sht_nobits))

(*val noop_reloc : forall 'abifeature. natural -> ((maybe elf64_symbol_table_entry -> natural) * (annotated_memory_image 'abifeature -> maybe natural))*)
let noop_reloc0 r:((elf64_symbol_table_entry)option ->Nat_big_num.num)*('abifeature annotated_memory_image ->(Nat_big_num.num)option)=  ((fun r_type -> (Nat_big_num.of_int 8)), (fun sym_val -> None))

let empty_elf_memory_image:(any_abi_feature)annotated_memory_image=  ({
      elements         = (Pmap.empty compare)
    ; by_range         = (Pset.empty (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare))
    ; by_tag           = (Pset.empty (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))))
})

(* HMM. For the elf_ident, I don't really want to express it this way.
 * I want something more bidirectional: something that can tell me
 * not only that a given ident is valid for a given ABI, but also,
 * to *construct* an ident for a given abstract ELF file satisfying x.
 * This is very much like a lens.
 *
 * Similarly for relocs, I might want a way to map back to an allowable
 * *concrete* representation, from some *abstract* description of the
 * reloc's intent (i.e. a symbol binding: "point this reference at symbol
 * Foo"), given the constraints imposed by the ABI (such as "use only
 * RELA, not rel". FIXME: figure out how to lensify what we're doing. *)

type elf_range_tag = any_abi_feature range_tag

let null_section_header_table:elf_file_feature=  (ElfSectionHeaderTable([]))
let null_program_header_table:elf_file_feature=  (ElfProgramHeaderTable([]))
let null_elf_header:elf64_header=  ({
     elf64_ident    = ([])
   ; elf64_type     = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_machine  = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_version  = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_entry    = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_phoff    = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_shoff    = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_flags    = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_ehsize   = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_phentsize= (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_phnum    = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_shentsize= (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_shnum    = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_shstrndx = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   })

(* Here we build the image of a file in file offset space.
 * To transform to memory space, we
 *
 * - switch positions to be addresses
 * - switch lengths of nobits etc. to be memory lengths
 * - PROBLEM: an offset might map to >1 virtual address.
 *   So we have to clone it as multiple elements.
 *   Each gets a label identifying the "file feature" it came from
 *   -- i.e. sections, ELF header, SHT and PHT are all file features.
 * - PROBLEM: the memory image might only contain part of an element.
 *   We need to reflect this truncatedness somehow in the label.
 *
 * Is the offset-space view really useful?
 * SORT OF: want to be able to make an image out of relocatable ELF files
 * that have no address assignments or phdrs yet.
 * AHA. NO. This is not an offset-space view; it's a sectionwise memory view.
 * All allocatable sections become elements with Nothing as their address.
 * The remainder of the ELF file *should* be represented as labels.
 * But, hmm, some stuff like the ELF header and SHT will likely get discarded.
 *
 * In short, we should work entirely with memory space.
 * Then
 *
 * - do we want to encode the aliasing of multiple virtual addresses
 *   down to single "features" in offset-space, like multiple mappings
 *   of the ELF header, say?
 *)

(*val offset_to_vaddr_mappings : elf64_file -> natural -> list (natural * elf64_interpreted_segment)*)
let offset_to_vaddr_mappings f off:(Nat_big_num.num*elf64_interpreted_segment)list=
     (Lem_list.mapMaybe (fun ph ->
        if Nat_big_num.greater_equal off ph.elf64_segment_offset
            && Nat_big_num.less off (Nat_big_num.add ph.elf64_segment_base ph.elf64_segment_size)
        then Some ( Nat_big_num.add ph.elf64_segment_base ( Nat_big_num.sub_nat off ph.elf64_segment_offset), ph)
        else None
    ) f.elf64_file_interpreted_segments)

(*val gensym : string -> string*)
let gensym hint:string=  hint (* FIXME: remember duplicates *)

(*val extract_symbol : (elf64_symbol_table * string_table * natural) -> natural -> maybe (string * elf64_symbol_table_entry)*)
let extract_symbol symtab_triple symidx:(string*elf64_symbol_table_entry)option=
     (let (symtab, strtab, scnidx) = symtab_triple
    in
    (match Ml_bindings.list_index_big_int symidx symtab with
        Some ent ->
            (match (get_string_at (Uint32_wrapper.to_bigint ent.elf64_st_name) strtab) with
                Success str -> Some (str, ent)
                | Fail _ -> Some ("", ent)    (* ELF doesn't distinguish "no string" from "empty string" *)
            )
      | None -> None
    ))

(*val extract_satisfying_symbols : (elf64_symbol_table * string_table * natural) ->
    (elf64_symbol_table_entry -> bool) -> list (string * elf64_symbol_table_entry * natural (* scnidx *) * natural (* symidx *))*)
let extract_satisfying_symbols symtab_triple pred:(string*elf64_symbol_table_entry*Nat_big_num.num*Nat_big_num.num)list=
     (let (symtab, strtab, scnidx) = symtab_triple
    in
    (*let _ = Missing_pervasives.errln ("extracting satisfying symbols from symtab index " ^ (show scnidx) ^ ", size "
        ^ (show (length symtab)) )
    in*)
    mapMaybei (fun symidx -> (fun ent ->
        ((match (get_string_at (Uint32_wrapper.to_bigint ent.elf64_st_name) strtab) with
            Success str ->
                (* exclude those that don't match *)
                if (pred ent)
                then Some(str, ent, scnidx, symidx)
                else None
            | Fail s -> (*let _ = Missing_pervasives.errln ("couldn't get string from strtab of symtab with index " ^ (show scnidx)
                ^ ": " ^ s) in *)
                None
        ))
        )) symtab)

(*val extract_all_symbols : (elf64_symbol_table * string_table * natural) -> list (string * elf64_symbol_table_entry * natural (* scnidx *) * natural (* symidx *))*)
let extract_all_symbols symtab_triple:(string*elf64_symbol_table_entry*Nat_big_num.num*Nat_big_num.num)list=  (extract_satisfying_symbols symtab_triple (fun _ -> true))

let definitions_pred:elf64_symbol_table_entry ->bool=  (fun ent -> not (Nat_big_num.equal (Uint32_wrapper.to_bigint ent.elf64_st_shndx) stn_undef))
let references_pred:elf64_symbol_table_entry ->bool=  (fun ent -> Nat_big_num.equal (Uint32_wrapper.to_bigint ent.elf64_st_shndx) stn_undef && (not (is_elf64_null_entry ent)))

(*val extract_definitions_from_symtab_of_type : natural -> elf64_file -> list symbol_definition*)
let extract_definitions_from_symtab_of_type t e:(symbol_definition)list=
     ((match ( bind (find_elf64_symtab_by_type t e) (fun symtab -> (
        let (allsyms : (string * elf64_symbol_table_entry * Nat_big_num.num (* scnidx *) * Nat_big_num.num (* symidx *)) list)
         = (extract_satisfying_symbols symtab definitions_pred)
        in
        let (extracted : symbol_definition list)
         = (mapMaybei (fun i -> (fun (str, ent, scnidx, symidx) -> Some {
                   def_symname = str
                 ; def_syment = ent
                 ; def_sym_scn = scnidx
                 ; def_sym_idx = symidx
                 ; def_linkable_idx =( (Nat_big_num.of_int 0))
                 })) allsyms)
        in return extracted
    ))) with Fail _ -> [] | Success x -> x ))

(*val extract_references_from_symtab_of_type : natural -> elf64_file -> list symbol_reference*)
let extract_references_from_symtab_of_type t e:(symbol_reference)list=
     ((match ( bind (find_elf64_symtab_by_type t e) (fun symtab -> (
    let (allsyms : (string * elf64_symbol_table_entry * Nat_big_num.num (* scnidx *) * Nat_big_num.num (* symidx *)) list)
     = (extract_satisfying_symbols symtab references_pred)
    in
    let (extracted : symbol_reference list) =
        (mapMaybei (fun symidx -> (fun (str, ent, scnidx, symidx) -> Some {
                   ref_symname = str
                 ; ref_syment = ent
                 ; ref_sym_scn = scnidx
                 ; ref_sym_idx = symidx
                 })) allsyms)
    in
    (*let _ = Missing_pervasives.errs ("Extracted " ^ (show (length allsyms)) ^ " undefined references: "
        ^ (show (List.map (fun (str, _, scnidx, symidx) -> (str, scnidx, symidx)) allsyms)) ^ "\n")
(*       ^ " (syminds "
        ^ (show (List.map (fun extracted -> extracted.ref_sym_idx) x)) ^ ", symnames "
        ^ (show (List.map (fun extracted -> extracted.ref_symname) x)) ^ ")") *)

    in*) return extracted
    ))) with Fail _ -> [] | Success x -> x ))

(*val extract_all_relocs : string -> elf64_file -> list (natural (* scn *) * natural (* rel idx *) * natural (* rel src scn *) * elf64_relocation_a)*)
let extract_all_relocs fname1 e:(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*elf64_relocation_a)list=
     (let (all_rel_sections : (Nat_big_num.num * elf64_interpreted_section) list) = (mapMaybei (fun i -> (fun isec1 ->
        if Nat_big_num.equal isec1.elf64_section_type sht_rel then Some (i, isec1) else None
    )) e.elf64_file_interpreted_sections)
    in
    (*let _ = Missing_pervasives.errln ("File " ^ fname ^ " has " ^ (show (length all_rel_sections)) ^
        " rel sections (indices " ^ (show (List.map (fun (scn, _) -> scn) all_rel_sections)) ^ ")")
    in*)
    let (all_rela_sections : (Nat_big_num.num * elf64_interpreted_section) list) = (mapMaybei (fun i -> (fun isec1 ->
        if Nat_big_num.equal isec1.elf64_section_type sht_rela then Some (i, isec1) else None
    )) e.elf64_file_interpreted_sections)
    in
    (*let _ = Missing_pervasives.errln ("File " ^ fname ^ " has " ^ (show (length all_rela_sections)) ^
        " rela sections (indices " ^ (show (List.map (fun (scn, _) -> scn) all_rela_sections)) ^ ")")
    in*)
    let rel_to_rela = (fun rel -> {
         elf64_ra_offset = (rel.elf64_r_offset)
       ; elf64_ra_info   = (rel.elf64_r_info)
       ; elf64_ra_addend = (Nat_big_num.to_int64( (Nat_big_num.of_int 0)))
    })
    in
    let endian = (get_elf64_header_endianness e.elf64_file_header)
    in
    (* Build per-section lists of rels paired with their originating section id.
     * We also pair each element with its index *in that section*, and then flatten
     * the whole lot using mapConcat. *)
    let (all_rels_list : (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * elf64_relocation_a) list) = (list_reverse_concat_map (fun (scn, isec1) ->
        (match read_elf64_relocation_section   isec1.elf64_section_size endian isec1.elf64_section_body
        with
            Success (relocs, _) ->
                (*let _ = Missing_pervasives.errln ("Rel section with index " ^ (show scn) ^ " has " ^ (show (length relocs)) ^
                    " entries")
                in*)
                mapMaybei (fun idx1 -> (fun rel -> Some (scn, idx1, isec1.elf64_section_info, rel_to_rela rel))) relocs
            | Fail _ -> []
        )) all_rel_sections)
    in
    let (all_relas_list : (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * elf64_relocation_a) list) = (list_reverse_concat_map (fun (scn, isec1) ->
        (match read_elf64_relocation_a_section isec1.elf64_section_size endian isec1.elf64_section_body
        with
            Success (relocs, _) ->
            (*let _ = Missing_pervasives.errln ("Rela section with index " ^ (show scn) ^ " has " ^ (show (length relocs)) ^
                " entries")
            in*)
            mapMaybei (fun idx1 -> (fun rela -> Some (scn, idx1, isec1.elf64_section_info, rela))) relocs
            | Fail _ -> []
        )) all_rela_sections)
    in 
    List.rev_append (List.rev all_rels_list) all_relas_list)

(*val extract_all_relocs_as_symbol_references : string -> elf64_file -> list symbol_reference_and_reloc_site*)
let extract_all_relocs_as_symbol_references fname1 e:(symbol_reference_and_reloc_site)list=   
(let maybe_guessed_abi = (Lem_list.list_find_opt (fun abi1 ->
        abi1.is_valid_elf_header e.elf64_file_header
    ) Abis.all_abis) in
    let a = ((match maybe_guessed_abi with
        | Some a -> a
        | None -> failwith "extract_all_relocs_as_symbol_references: unknown ABI"
    )) in
    let all_relocs = (extract_all_relocs fname1 e)
    in
    let all_symtab_triples_by_scnidx = (mapMaybei (fun scnidx -> (fun isec1 ->
        if Nat_big_num.equal isec1.elf64_section_type sht_symtab
        then
            let found = (find_elf64_symbols_by_symtab_idx scnidx e)
            in
            (match found with
                Fail _ -> None
                | Success triple -> Some (scnidx, triple)
            )
        else None
    )) e.elf64_file_interpreted_sections)
    in
    let (all_extracted_symtabs_by_scnidx : ( (Nat_big_num.num, ( (string * elf64_symbol_table_entry * Nat_big_num.num (* scnidx *) * Nat_big_num.num (* symidx *))list))Pmap.map))
     = (List.fold_left (fun acc -> (fun (scnidx, triple) -> Pmap.add scnidx (extract_all_symbols triple) acc)) (Pmap.empty Nat_big_num.compare) all_symtab_triples_by_scnidx)
    in
    (*let _ = Missing_pervasives.errln ("All extracted symtabs by scnidx: " ^ (show (Set_extra.toList (Map.toSet all_extracted_symtabs_by_scnidx))))
    in*)
    let ref_for_relocation_a_in_section_index = (fun rel_scn_idx -> (fun rel_idx -> (fun rela ->
        let rela_isec = ((match Ml_bindings.list_index_big_int rel_scn_idx e.elf64_file_interpreted_sections with
            Some x -> x
            | None -> failwith "relocation references nonexistent section"
        ))
        in
        let symtab_idx = (rela_isec.elf64_section_link)
        in
        (match Pmap.lookup symtab_idx all_extracted_symtabs_by_scnidx with
            None -> failwith "referenced symtab does not exist"
            | Some quads ->
                let (_, sym_idx) = (a.parse_reloc_info rela.elf64_ra_info)
                in
                let maybe_quad = (Ml_bindings.list_index_big_int sym_idx quads)
                in
                (match maybe_quad with
                    Some(symname, syment, scnidx, symidx) -> {
                           ref_symname = symname
                         ; ref_syment = syment
                         ; ref_sym_scn = symtab_idx
                         ; ref_sym_idx = sym_idx
                         }
                    | None -> failwith "reloc references symbol that does not exist" (*("reloc at index " ^ (show rel_idx) ^ " references symbol (index " ^ (show sym_idx) ^
                        ") that does not exist: symtab (index " ^ (show symtab_idx) ^ ") has " ^ (show (length quads)) ^ " entries")*)
                )
        )
    )))
    in
    (*let _ = Missing_pervasives.errs ("Extracted " ^ (show (length all_relocs)) ^ " reloc references (rel_scn, rel_idx, src_scn): "
        ^ (show (List.map (fun (rel_scn, rel_idx, srcscn, rela) -> (rel_scn, rel_idx, srcscn)) all_relocs)) ^ "\n")
    in*)
    Lem_list.map (fun (scn, idx1, srcscn, rela) -> {
          ref = ( (* NOTE that a reference is not necessarily to an undefined symbol! *)ref_for_relocation_a_in_section_index scn idx1 rela)
        ; maybe_reloc = (Some
           { ref_relent = rela
            ; ref_rel_scn = scn
            ; ref_rel_idx = idx1
            ; ref_src_scn = srcscn (* what section does the reference come from? it's the 'info' link of the rel section header *)
            })
        ; maybe_def_bound_to = None
        }) all_relocs)