Source file memory_image_orderings.ml

(*Generated by Lem from memory_image_orderings.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
open Lem_set
open Multimap
open Lem_num
open Lem_maybe
open Lem_assert_extra
open Show

open Byte_sequence
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 Memory_image
open Abi_classes
(* open import Abis *)

open Missing_pervasives

(*val elfFileFeatureCompare : elf_file_feature -> elf_file_feature -> Basic_classes.ordering*)
let elfFileFeatureCompare f1 f2:int=
     (
    (* order is: *)(match (f1, f2) with
        (ElfHeader(x1), ElfHeader(x2)) -> (* equal tags, so ... *) elf64_header_compare x1 x2
      | (ElfHeader(x1), _) -> (-1)
      | (ElfSectionHeaderTable(x1), ElfHeader(x2)) -> 1
      | (ElfSectionHeaderTable(x1), ElfSectionHeaderTable(x2)) -> ( (* equal tags, so ... *)lexicographic_compare compare_elf64_section_header_table_entry x1 x2)
      | (ElfSectionHeaderTable(x1), _) -> (-1)
      | (ElfProgramHeaderTable(x1), ElfHeader(x2)) -> 1
      | (ElfProgramHeaderTable(x1), ElfSectionHeaderTable(x2)) -> 1
      | (ElfProgramHeaderTable(x1), ElfProgramHeaderTable(x2)) -> (lexicographic_compare compare_elf64_program_header_table_entry x1 x2)
      | (ElfProgramHeaderTable(x1), _) -> (-1)
      | (ElfSection(x1), ElfHeader(x2)) -> 1
      | (ElfSection(x1), ElfSectionHeaderTable(x2)) -> 1
      | (ElfSection(x1), ElfProgramHeaderTable(x2)) -> 1
      | (ElfSection(x1), ElfSection(x2)) -> (pairCompare Nat_big_num.compare compare_elf64_interpreted_section x1 x2)
      | (ElfSection(x1), _) -> (-1)
      | (ElfSegment(x1), ElfHeader(x2)) -> 1
      | (ElfSegment(x1), ElfSectionHeaderTable(x2)) -> 1
      | (ElfSegment(x1), ElfProgramHeaderTable(x2)) -> 1
      | (ElfSegment(x1), ElfSection(x2)) -> 1
      | (ElfSegment(x1), ElfSegment(x2)) -> (pairCompare Nat_big_num.compare compare_elf64_interpreted_segment x1 x2)
      | (ElfSegment(x1), _) -> (-1)
    ))

(*val elfFileFeatureTagEquiv : elf_file_feature -> elf_file_feature -> bool*)
let elfFileFeatureTagEquiv f1 f2:bool=
     (
    (* order is: *)(match (f1, f2) with
        (ElfHeader(x1), ElfHeader(x2)) -> (* equal tags, so ... *) true
      | (ElfSectionHeaderTable(x1), ElfSectionHeaderTable(x2)) -> true
      | (ElfProgramHeaderTable(x1), ElfProgramHeaderTable(x2)) -> true
      | (ElfSection(x1), ElfSection(x2)) -> true
      | (ElfSegment(x1), ElfSegment(x2)) -> true
      | (_, _) -> false
    ))

let instance_Basic_classes_Ord_Memory_image_elf_file_feature_dict:(elf_file_feature)ord_class= ({

  compare_method = elfFileFeatureCompare;

  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elfFileFeatureCompare f1 f2) (-1))));

  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elfFileFeatureCompare f1 f2)(Pset.from_list compare [(-1); 0])));

  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elfFileFeatureCompare f1 f2) 1)));

  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elfFileFeatureCompare f1 f2)(Pset.from_list compare [1; 0])))})

(*val tagCompare : forall 'abifeature. Ord 'abifeature =>
    range_tag 'abifeature -> range_tag 'abifeature -> Basic_classes.ordering*)
let tagCompare dict_Basic_classes_Ord_abifeature k1 k2:int=
     ((match (k1, k2) with
        (ImageBase, ImageBase) -> 0
        | (ImageBase, _) -> (-1)
        | (EntryPoint, ImageBase) -> 1
        | (EntryPoint, EntryPoint) -> 0
        | (EntryPoint, _) -> (-1)
        | (SymbolDef(_), ImageBase) -> 1
        | (SymbolDef(_), EntryPoint) -> 1
        | (SymbolDef(x1), SymbolDef(x2)) -> symDefCompare x1 x2
        | (SymbolDef(_), _) -> (-1)
        | (SymbolRef(_), ImageBase) -> 1
        | (SymbolRef(_), EntryPoint) -> 1
        | (SymbolRef(_), SymbolDef(_)) -> 1
        | (SymbolRef(x1), SymbolRef(x2)) -> symRefAndRelocSiteCompare x1 x2
        | (SymbolRef(_), _) -> (-1)
        | (FileFeature(_), ImageBase) -> 1
        | (FileFeature(_), EntryPoint) -> 1
        | (FileFeature(_), SymbolDef(_)) -> 1
        | (FileFeature(_), SymbolRef(_)) -> 1
        | (FileFeature(x1), FileFeature(x2)) -> elfFileFeatureCompare x1 x2
        | (FileFeature(_), _) -> (-1)
        | (AbiFeature(_), ImageBase) -> 1
        | (AbiFeature(_), EntryPoint) -> 1
        | (AbiFeature(_), SymbolDef(_)) -> 1
        | (AbiFeature(_), SymbolRef(_)) -> 1
        | (AbiFeature(_), FileFeature(_)) -> 1
        | (AbiFeature(x1), AbiFeature(x2)) -> 
  dict_Basic_classes_Ord_abifeature.compare_method x1 x2
        | (AbiFeature(_), _) -> (-1)
    ))

let instance_Basic_classes_Ord_Memory_image_range_tag_dict dict_Basic_classes_Ord_abifeature:('abifeature range_tag)ord_class= ({

  compare_method = 
  (tagCompare dict_Basic_classes_Ord_abifeature);

  isLess_method = (fun tag1 -> (fun tag2 -> ( Lem.orderingEqual(tagCompare 
  dict_Basic_classes_Ord_abifeature tag1 tag2) (-1))));

  isLessEqual_method = (fun tag1 -> (fun tag2 -> Pset.mem (tagCompare 
  dict_Basic_classes_Ord_abifeature tag1 tag2)(Pset.from_list compare [(-1); 0])));

  isGreater_method = (fun tag1 -> (fun tag2 -> ( Lem.orderingEqual(tagCompare 
  dict_Basic_classes_Ord_abifeature tag1 tag2) 1)));

  isGreaterEqual_method = (fun tag1 -> (fun tag2 -> Pset.mem (tagCompare 
  dict_Basic_classes_Ord_abifeature tag1 tag2)(Pset.from_list compare [1; 0])))})

(*val tagEquiv : forall 'abifeature. AbiFeatureTagEquiv 'abifeature => range_tag 'abifeature -> range_tag 'abifeature -> bool*)
let tagEquiv dict_Abi_classes_AbiFeatureTagEquiv_abifeature k1 k2:bool=
     ((match (k1, k2) with
        (ImageBase, ImageBase) -> true
        | (EntryPoint, EntryPoint) -> true
        | (SymbolDef(x1), SymbolDef(x2)) -> true
        | (SymbolRef(_), SymbolRef(_)) -> true
        | (FileFeature(x1), FileFeature(x2)) -> elfFileFeatureTagEquiv x1 x2
        | (AbiFeature(x1), AbiFeature(x2)) -> 
  dict_Abi_classes_AbiFeatureTagEquiv_abifeature.abiFeatureTagEquiv_method x1 x2
        | (_, _) -> false
    ))

(* ------- end of Ord / compare / ConstructorToNaturalList functions *)


(*val unique_tag_matching : forall 'abifeature. Ord 'abifeature, AbiFeatureTagEquiv 'abifeature => range_tag 'abifeature -> annotated_memory_image 'abifeature -> range_tag 'abifeature*)
let unique_tag_matching dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature tag img2:'abifeature range_tag=
     ((match Multimap.lookupBy0 
  (instance_Basic_classes_Ord_Memory_image_range_tag_dict
     dict_Basic_classes_Ord_abifeature) (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)))  (tagEquiv dict_Abi_classes_AbiFeatureTagEquiv_abifeature) tag img2.by_tag with
        [] -> failwith "no tag match found"
        | [(t, r)] -> t
        | x -> failwith ("more than one tag match") (* (ranges: " ^
            (show (List.map (fun (t, r) -> r) x))
            ^  ") when asserted unique")" *)
    ))

(*val tagged_ranges_matching_tag : forall 'abifeature. Ord 'abifeature, AbiFeatureTagEquiv 'abifeature => range_tag 'abifeature -> annotated_memory_image 'abifeature -> list (range_tag 'abifeature * maybe element_range)*)
let tagged_ranges_matching_tag dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature tag img2:('abifeature range_tag*(element_range)option)list=
     (Multimap.lookupBy0 
  (instance_Basic_classes_Ord_Memory_image_range_tag_dict
     dict_Basic_classes_Ord_abifeature) (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)))  (tagEquiv dict_Abi_classes_AbiFeatureTagEquiv_abifeature) tag img2.by_tag)

(*val element_range_compare : element_range -> element_range -> Basic_classes.ordering*)
let element_range_compare:string*(Nat_big_num.num*Nat_big_num.num) ->string*(Nat_big_num.num*Nat_big_num.num) ->int=  (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))

(*val unique_tag_matching_at_range_exact : forall 'abifeature. Ord 'abifeature, AbiFeatureTagEquiv 'abifeature =>
    maybe element_range
    -> range_tag 'abifeature
    -> annotated_memory_image 'abifeature
    -> range_tag 'abifeature*)
let unique_tag_matching_at_range_exact dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature r tag img2:'abifeature range_tag=
     (
    (* 1. find tags a unique range labelled as ELF section header table. *)let (_, (allRangeMatches : ( 'abifeature range_tag) list)) = (List.split (Multimap.lookupBy0 
  (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_Ord_Memory_image_range_tag_dict
   dict_Basic_classes_Ord_abifeature) (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 (Lem.option_equal (Lem.pair_equal (=) (Lem.pair_equal Nat_big_num.equal Nat_big_num.equal))) r img2.by_range))
    in
    let (tagAlsoMatches : ( 'abifeature range_tag) list) = (List.filter (fun x -> tagEquiv 
  dict_Abi_classes_AbiFeatureTagEquiv_abifeature x tag) allRangeMatches)
    in
    (match tagAlsoMatches with
        [] -> failwith "no range/tag match when asserted to exist"
        | [x] -> x
        | _ -> failwith "multiple range/tag match when asserted unique"
    ))

(*val symbol_def_ranges : forall 'abifeature. Ord 'abifeature, AbiFeatureTagEquiv 'abifeature => annotated_memory_image 'abifeature -> (list (range_tag 'abifeature) * list (maybe element_range))*)
let symbol_def_ranges dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature img2:('abifeature range_tag)list*((element_range)option)list=
     (
    (* find all element ranges labelled as ELF symbols *)let (tags, maybe_ranges) = (List.split (
        tagged_ranges_matching_tag 
  dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature (SymbolDef(null_symbol_definition)) img2
    ))
    in
    (* some symbols, specifically ABS symbols, needn't label a range. *)
    (tags, maybe_ranges))

(*val name_of_symbol_def : symbol_definition -> string*)
let name_of_symbol_def sym1:string=  (sym1.def_symname)

(*val defined_symbols_and_ranges : forall 'abifeature. Ord 'abifeature, AbiFeatureTagEquiv 'abifeature => annotated_memory_image 'abifeature -> list ((maybe element_range) * symbol_definition)*)
let defined_symbols_and_ranges dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature img2:((element_range)option*symbol_definition)list=
     (Lem_list.mapMaybe (fun (tag, maybeRange) ->
        (match tag with
            SymbolDef(ent) -> Some (maybeRange, ent)
            | _ -> failwith "impossible: non-symbol def in list of symbol defs"
        )) (tagged_ranges_matching_tag 
  dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature (SymbolDef(null_symbol_definition)) img2))

(*val make_ranges_definite : list (maybe element_range) -> list element_range*)
let make_ranges_definite rs:(string*range)list=
     (Lem_list.map (fun (maybeR :  element_range option) -> (match maybeR with
            Some r -> r
            | None -> failwith "impossible: range not definite, but asserted to be"
        )) rs)

(* val find_defs_matching : forall 'abifeature. Ord 'abifeature, AbiFeatureTagEquiv 'abifeature => symbol_definition -> annotated_memory_image 'abifeature (* list (maybe element_range * symbol_definition) *) -> list ((maybe element_range) * symbol_definition) *)
(*val find_defs_matching : symbol_definition -> list (maybe element_range * symbol_definition) -> list ((maybe element_range) * symbol_definition)*)
let find_defs_matching bound_def ranges_and_defs:((element_range)option*symbol_definition)list=
     (
    (*let _ = errln ("Searching (among " ^ (show (length ranges_and_defs)) ^ ") for the bound-to symbol `" ^ bound_def.def_symname
        ^ "', which came from linkable idx " ^
        (show bound_def.def_linkable_idx) ^ ", section " ^
        (show bound_def.def_syment.elf64_st_shndx) ^
        ", symtab shndx " ^ (show bound_def.def_sym_scn) ^
        ", symind " ^ (show bound_def.def_sym_idx))
    in*)Lem_list.mapMaybe (fun (maybe_some_range, some_def) ->
       (* let _ = errln ("Considering one: `" ^ some_def.def_symname ^ "'") in *)
       (* match maybe_some_range with
            Nothing -> failwith "symbol definition not over a definite range"
            | Just some_range -> *)
                (* if some_def.def_symname = bound_def.def_symname
                && some_def.def_linkable_idx = bound_def.def_linkable_idx then
                if some_def = bound_def
                    then Just(maybe_some_range, some_def) else Nothing*)
                    (*let _ = errln ("Found one in the same linkable: syment is " ^
                        (show some_def.def_syment))
                    in*)
                (*else*) if some_def = bound_def
                            then (
                                (*let _ = errln ("Found one: syment is " ^ (show some_def.def_syment))
                                in*)
                                Some(maybe_some_range, some_def)
                            )
                            else if some_def.def_symname = bound_def.def_symname then
                                (*let _ = errln ("Warning: passing over name-matching def with section " ^
                                    (show some_def.def_syment.elf64_st_shndx) ^
                                    ", symtab shndx " ^ (show some_def.def_sym_scn) ^
                                    ", symind " ^ (show some_def.def_sym_idx) ^
                                    ", linkable idx " ^ (show some_def.def_linkable_idx))
                                in*) None
                            else None
       (* end *)
    ) ranges_and_defs)


(*val defined_symbols : forall 'abifeature. Ord 'abifeature, AbiFeatureTagEquiv 'abifeature =>  annotated_memory_image 'abifeature -> list symbol_definition*)
let defined_symbols dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature img2:(symbol_definition)list=
     (let (all_symbol_tags, all_symbol_ranges) = (symbol_def_ranges 
  dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature img2) in
    Lem_list.mapMaybe (fun tag ->
        (match tag with
            SymbolDef(ent) -> Some ent
            | _ -> failwith "impossible: non-symbol def in list of symbol defs"
        )) all_symbol_tags)


(*val default_get_reloc_symaddr : forall 'abifeature. Ord 'abifeature, AbiFeatureTagEquiv 'abifeature => symbol_definition -> annotated_memory_image 'abifeature -> list (maybe element_range * symbol_definition) -> maybe reloc_site -> natural*)
let default_get_reloc_symaddr dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature bound_def_in_input output_img ranges_and_defs maybe_reloc1:Nat_big_num.num=
     ((match find_defs_matching bound_def_in_input ranges_and_defs with
        [] -> failwith ("internal error: bound-to symbol (name `" ^ (bound_def_in_input.def_symname ^ "') not defined"))
        | (maybe_range, d) :: more ->
            let v =
                ((match maybe_range with
                    Some(el_name, (start, len)) ->
                    (match element_and_offset_to_address (el_name, start) output_img with
                        Some a -> a
                        | None -> failwith "internal error: could not get address for symbol"
                    )
                    | None ->
                        (* okay, it'd better be an ABS symbol. *)
                        if Nat_big_num.equal (Uint32_wrapper.to_bigint d.def_syment.elf64_st_shndx) shn_abs
                            then Ml_bindings.nat_big_num_of_uint64 d.def_syment.elf64_st_value
                            else failwith "no range for non-ABS symbol"
                ))
            in
            (match more with
                [] -> v
                | _ -> (*let _ = errln ("FIXME: internal error: more than one def matching bound def `" ^
                    bound_def_in_input.def_symname ^ "'")
                    in *) v
            )
    ))