Source file memory_image.ml

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

open Byte_pattern
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 Endianness

open Missing_pervasives

(* Now we can define memory images *)

(* An element might have an address/offset, and it has some contents. *)
type element = { startpos :  Nat_big_num.num option
                ; length1   :  Nat_big_num.num option
                ; contents : byte_pattern
                }

(* HMM -- ideally I want to fold these into the memory image notion
 * and the startpos thingy. *)
type allocated_symbols_map = (string, (Nat_big_num.num * Nat_big_num.num)) Pmap.map (* start, length *)

(* Instead of modelling address calculations (in linker scripts) like so:

type address_expr = natural -> allocated_symbols_map -> natural
                  ( pos     -> environment           -> result address )

   ... we model it as expressions in terms of CursorPosition. HMM.
*)

type expr_operand = Var of string
                   | CursorPosition          (* only valid in certain expressions... HMM *)
                   | Constant of Nat_big_num.num
                   | UnOp of (expr_unary_operation * expr_operand)
                   | BinOp of (expr_binary_operation * expr_operand * expr_operand)
and
expr_unary_operation = Neg of expr_operand
                           | BitwiseInverse of expr_operand
and
expr_binary_operation = Add of (expr_operand * expr_operand)
                           | Sub of (expr_operand * expr_operand)
                           | BitwiseAnd of (expr_operand * expr_operand)
                           | BitwiseOr of (expr_operand * expr_operand)

type expr_binary_relation =
    Lt
    | Lte
    | Gt
    | Gte
    | Eq
    | Neq

type expr =
    False
    | True
    | Not of expr
    | And of (expr * expr)
    | Or of (expr * expr)
    | BinRel of (expr_binary_relation * expr_operand)  (* LH operand is the expr's value *)

(*
val cond_expr : expr -> expr -> expr -> expr
let cond_expr expr1 expr2 expr3 = (Or((And(expr1, expr2)), (And((Not(expr1)), expr3))))
*)

(* Memory image elements all have identities. For convenience
 * we make the identities strings. The string contents are arbitrary,
 * and only their equality is relevant, but choosing friendly names
 * like "ELF header" is good practice.*)
type memory_image = (string, element) Pmap.map

type range = Nat_big_num.num * Nat_big_num.num (* start, length *)

type element_range = string * range

(* An "element" of an ELF image, in the linking phase, is either a section,
 * the ELF header, the section header table or the program header table.
 *
 * PROBLEM: We'd like to use section names as the identifiers
 * for those elements that are sections.
 * but we can't, because they are not guaranteed to be unique.
 *
 * SOLUTION: Names that are unique in the file are used as keys.
 * If not unique, the sections are treated as anonymous and given
 * gensym'd string ids (FIXME: implement this).
 *)

(* Currently, our elements have unique names, which are strings.
 * We *don't* want to encode any meaning onto these strings.
 * All meaning should be encoded into labelled ranges.
 * We want to be able to look up
 *
 * - elements
 * - ranges within elements
 *
 * ... by their *labels* -- or sometimes just *part* of their labels.
 *)

(* ELF file features with which we can label ranges of the memory image. *)
type elf_file_feature =
    ElfHeader of elf64_header
    | ElfSectionHeaderTable of elf64_section_header_table (* do we want to expand these? *)
    | ElfProgramHeaderTable of elf64_program_header_table
    | ElfSection of (Nat_big_num.num * elf64_interpreted_section) (* SHT idx *)
    | ElfSegment of (Nat_big_num.num * elf64_interpreted_segment) (* PHT idx *)

type symbol_definition
 = { def_symname : string
    ; def_syment : elf64_symbol_table_entry (* definition's symtab entry *)
    ; def_sym_scn : Nat_big_num.num                 (* symtab section index, to disamiguate dynsym *)
    ; def_sym_idx : Nat_big_num.num                 (* index of symbol into the symtab *)
    ; def_linkable_idx : Nat_big_num.num            (* used to propagate origin linkable information to linked image *)
    }

let symDefCompare x1 x2:int=
         (quintupleCompare compare elf64_symbol_table_entry_compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare (x1.def_symname, x1.def_syment, x1.def_sym_scn, x1.def_sym_idx, x1.def_linkable_idx)
                (x2.def_symname, x2.def_syment, x2.def_sym_scn, x2.def_sym_idx, x2.def_linkable_idx))

let instance_Basic_classes_Ord_Memory_image_symbol_definition_dict:(symbol_definition)ord_class= ({

  compare_method = symDefCompare;

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

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

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

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

type symbol_reference
 = { ref_symname : string                  (* symbol name *)
    ; ref_syment : elf64_symbol_table_entry (* likely-undefined (referencing) symbol *)
    ; ref_sym_scn : Nat_big_num.num                 (* symtab section idx *)
    ; ref_sym_idx : Nat_big_num.num                 (* index into symbol table *)
    }

let symRefCompare x1 x2:int=
         (quadrupleCompare compare elf64_symbol_table_entry_compare Nat_big_num.compare Nat_big_num.compare (x1.ref_symname, x1.ref_syment, x1.ref_sym_scn, x1.ref_sym_idx)
                (x2.ref_symname, x2.ref_syment, x2.ref_sym_scn, x2.ref_sym_idx))

let instance_Basic_classes_Ord_Memory_image_symbol_reference_dict:(symbol_reference)ord_class= ({

  compare_method = symRefCompare;

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

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

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

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

type reloc_site = {
      ref_relent  : elf64_relocation_a
    ; ref_rel_scn : Nat_big_num.num  (* the relocation section idx *)
    ; ref_rel_idx : Nat_big_num.num  (* the index of the relocation rec *)
    ; ref_src_scn : Nat_big_num.num  (* the section *from which* the reference logically comes *)
}

let relocSiteCompare x1 x2:int=
         (quadrupleCompare elf64_relocation_a_compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare (x1.ref_relent, x1.ref_rel_scn, x1.ref_rel_idx, x1.ref_src_scn)
                (x2.ref_relent, x2.ref_rel_scn, x2.ref_rel_idx, x2.ref_src_scn))

let instance_Basic_classes_Ord_Memory_image_reloc_site_dict:(reloc_site)ord_class= ({

  compare_method = relocSiteCompare;

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

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

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

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

type reloc_decision = LeaveReloc
                    | ApplyReloc
                    | ChangeRelocTo of (Nat_big_num.num * symbol_reference * reloc_site)
                    (* | MakePIC    -- is now a kind of ChangeRelocTo *)

let relocDecisionCompare x1 x2:int=
   ((match (x1, x2) with
    | (LeaveReloc, LeaveReloc) -> 0
    | (LeaveReloc, _)          -> (-1)
    | (ApplyReloc, ApplyReloc) -> 0
    | (ApplyReloc, ChangeRelocTo _) -> (-1)
    | (ApplyReloc, LeaveReloc)      -> 1
    | (ChangeRelocTo t1, ChangeRelocTo t2) -> (tripleCompare Nat_big_num.compare symRefCompare relocSiteCompare t1 t2)
    | (ChangeRelocTo _, _) -> 1
  ))

let instance_Basic_classes_Ord_Memory_image_reloc_decision_dict:(reloc_decision)ord_class= ({

  compare_method = relocDecisionCompare;

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

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

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

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

type symbol_reference_and_reloc_site = {
      ref         : symbol_reference
    ; maybe_reloc :  reloc_site option
    ; maybe_def_bound_to :  (reloc_decision *  symbol_definition option)option
    }

let symRefAndRelocSiteCompare x1 x2:int=
         (tripleCompare symRefCompare (maybeCompare relocSiteCompare) (maybeCompare (pairCompare relocDecisionCompare (maybeCompare symDefCompare))) (x1.ref, x1.maybe_reloc, x1.maybe_def_bound_to)
                (x2.ref, x2.maybe_reloc, x2.maybe_def_bound_to))

let instance_Basic_classes_Ord_Memory_image_symbol_reference_and_reloc_site_dict:(symbol_reference_and_reloc_site)ord_class= ({

  compare_method = symRefAndRelocSiteCompare;

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

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

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

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

(* We can also annotate arbitrary ranges of bytes within an element
 * with arbitrary metadata.
 *
 * Ideally we want to data-abstract this a bit. But it's hard to do
 * so without baking in ELF-specific and/or (moreover) per-ABI concepts,
 * like PLTs and GOTs. Ideally we would use something like polymorphic
 * variants here. For now, this has to be the union of all the concepts
 * that we find in the various ABIs we care about. To avoid ELFy things
 * creeping in, we parameterise by 'a, and instantiate the 'a with the
 * relevant ELFy thing when we use it. OH, but then 'a is different for
 * every distinct ELF thing, which is no good. Can we define a mapping
 * from an umbrella "ELF" type to the relevant types in each case? *)
type 'abifeature range_tag = (*  forall 'abifeature . *)
                 ImageBase
               | EntryPoint
               | SymbolDef of symbol_definition
               | SymbolRef of symbol_reference_and_reloc_site
               | FileFeature of elf_file_feature (* file feature other than symdef and reloc *)
               | AbiFeature of 'abifeature

type 'abifeature annotated_memory_image = {
      elements         : memory_image
    ; by_range         : (( element_range option) * ( 'abifeature range_tag)) Pset.set
    ; by_tag           : (( 'abifeature range_tag), ( element_range option)) multimap
}

(*val get_empty_memory_image : forall 'abifeature. unit -> annotated_memory_image 'abifeature*)
let get_empty_memory_image:unit ->'abifeature annotated_memory_image=  (fun _ -> {
      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)))))
})

(* Basic ELFy and ABI-y things. *)
(* "Special" sections are those that necessarily require special treatment by the
 * linker. Examples include symbol tables and relocation tables. There are some
 * grey areas, such as .eh_frame, debug info, and string tables. For us, the rule
 * is that if we have special code to create them, i.e. that we don't rely on
 * ordinary section concatenation during the linker script interpretation, they
 * should be special -- it means strip_metadata_sections will remove them from
 * the image, they won't be seen by the linker script, and that it's *our* job
 * to reinstate them afterwards (as we do with symtab and strtab, for example). *)
(* FIXME: this shouldn't really be here, but needs to be in some low-lying module;
 * keeping it out of elf_* for now to avoid duplication into elf64_, elf32_. *)
let elf_section_is_special 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)
                     && (not (Nat_big_num.equal s.elf64_section_type sht_fini_array)
                     && not (Nat_big_num.equal s.elf64_section_type sht_init_array))))

(* This record collects things that ABIs may or must define.
 *
 * Since we want to put all ABIs in a list and select one at run time,
 * we can't maintain a type-level distinction between ABIs; we have to
 * use elf_memory_image any_abi_feature. To avoid a reference cycle,
 * stay polymorphic in the ABI feature type until we define specific ABIs.
 * In practice we'll use only any_abi_feature, because we need to pull
 * the ABI out of a list at run time.
 *)
type null_abi_feature = unit

(* The reloc calculation is complicated, so we split up the big function
 * type into smaller ones. *)

(* Q. Do we want "existing", or is it a kind of addend?
 * A. We do want it -- modelling both separately is necessary,
 * because we model relocations bytewise, but some arches
 * do bitfield relocations (think ARM). *)
type reloc_calculate_fn    = Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num (* symaddr -> addend -> existing -> relocated *)

type 'abifeature reloc_apply_fn = 'abifeature
                                (* elf memory image: the context in which the relocation is being applied *)
                                annotated_memory_image ->
                               (* the site address *)
                                Nat_big_num.num ->
                                (* Typically there are two symbol table entries involved in a relocation.
                                 * One is the reference, and is usually undefined.
                                 * The other is the definition, and is defined (else absent, when we use 0).
                                 * However, sometimes the reference is itself a defined symbol.
                                 * Almost always, if so, *that* symbol *is* "the definition".
                                 * However, copy relocs are an exception.
                                 *
                                 * In the case of copy relocations being fixed up by the dynamic
                                 * linker, the dynamic linker must figure out which definition to
                                 * copy from. This can't be as simple as "the first definition in
                                 * link order", because *our* copy of that symbol is a definition
                                 * (typically in bss). It could be as simple as "the first *after us*
                                 * in link order". FIXME: find the glibc code that does this.
                                 *
                                 * Can we dig this stuff out of the memory image? If we pass the address
                                 * being relocated, we can find the tags. But I don't want to pass
                                 * the symbol address until the very end. It seems better to pass the symbol
                                 * name, since that's the key that the dynamic linker uses to look for
                                 * other definitions.
                                 *
                                 * Do we want to pass a whole symbol_reference? This has not only the
                                 * symbol name but also syment, scn and idx. The syment is usually UND,
                                 * but *could* be defined (and is for copy relocs). The scn and idx are
                                 * not relevant, but it seems cleaner to pass the whole thing anyway.
                                 *)
                                symbol_reference_and_reloc_site ->
                                (* Should we pass a symbol_definition too? Implicitly, we pass part of it
                                 * by passing the symaddr argument (below). I'd prefer not to depend on
                                 * others -- relocation calculations should look like "mostly address
                                 * arithmetic", i.e. only the weird ones do something else. *)
                                 (* How wide, in bytes, is the relocated field? this may depend on img
                                 * and on the wider image (copy relocs), so it's returned *by* the reloc function. *)
                                (Nat_big_num.num (* width *) * reloc_calculate_fn)

(* Some kinds of relocation necessarily give us back a R_*_RELATIVE reloc.
 * We don't record this explicitly. Instead, the "bool" is a flag recording whether
 * the field represents an absolute address.
 * Similarly, some relocations can "fail" according to their ABI manuals.
 * This just means that the result can't be represented in the field width.
 * We detect this when actually applying the reloc in the memory image content
 * (done elsewhere). *)
type 'abifeature reloc_fn = Nat_big_num.num -> (bool * 'abifeature reloc_apply_fn)

(*val noop_reloc_calculate : natural -> integer -> natural -> natural*)
let noop_reloc_calculate symaddr addend existing:Nat_big_num.num=  existing

(*val noop_reloc_apply : forall 'abifeature. reloc_apply_fn 'abifeature*)
let noop_reloc_apply img2 site_addr ref1:Nat_big_num.num*(Nat_big_num.num ->Nat_big_num.num ->Nat_big_num.num ->Nat_big_num.num)=  ( (Nat_big_num.of_int 0), noop_reloc_calculate)

(*val noop_reloc : forall 'abifeature. natural -> (bool (* result is absolute addr *) * reloc_apply_fn 'abifeature)*)
let noop_reloc k:bool*('abifeature annotated_memory_image ->Nat_big_num.num ->symbol_reference_and_reloc_site ->Nat_big_num.num*reloc_calculate_fn)=  (false, noop_reloc_apply)

type 'abifeature abi = (* forall 'abifeature. *)
   { is_valid_elf_header : elf64_header -> bool (* doesn't this generalise outrageously? is_valid_elf_file? *)
    ; make_elf_header    : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> elf64_header
                           (* t entry shoff phoff phnum shnum shstrndx *)
    ; reloc              : 'abifeature reloc_fn
    ; section_is_special : elf64_interpreted_section -> 'abifeature annotated_memory_image -> bool
    ; section_is_large   : elf64_interpreted_section -> 'abifeature annotated_memory_image -> bool
    ; maxpagesize        : Nat_big_num.num
    ; minpagesize        : Nat_big_num.num
    ; commonpagesize     : Nat_big_num.num
    ; symbol_is_generated_by_linker : string -> bool
    (*; link_inputs_tap    :
    ; link_output_sections_tap   :
    ; link_output_image_tap      : *)
    ; make_phdrs         : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num (* file type *) -> 'abifeature annotated_memory_image -> elf64_interpreted_section list -> elf64_program_header_table_entry list
    ; max_phnum          : Nat_big_num.num
    ; guess_entry_point  : 'abifeature annotated_memory_image ->  Nat_big_num.num option
    ; pad_data           : Nat_big_num.num -> char list
    ; pad_code           : Nat_big_num.num -> char list
    ; generate_support   : (string * 'abifeature annotated_memory_image) (* list (list reloc_site_resolution) ->  *)list -> 'abifeature annotated_memory_image
    ; concretise_support : 'abifeature annotated_memory_image -> 'abifeature annotated_memory_image
    ; get_reloc_symaddr  : symbol_definition -> 'abifeature annotated_memory_image -> ( element_range option * symbol_definition) list ->  reloc_site option -> Nat_big_num.num
    ; parse_reloc_info   : Uint64_wrapper.uint64 -> (Nat_big_num.num (* type *) * Nat_big_num.num (* symbol *))
    }

(*val align_up_to : natural -> natural -> natural*)
let align_up_to align addr:Nat_big_num.num=
     (let quot = (Nat_big_num.div addr align)
    in
    if Nat_big_num.equal (Nat_big_num.mul quot align) addr then addr else Nat_big_num.mul ( Nat_big_num.add quot( (Nat_big_num.of_int 1))) align)

(*val round_down_to : natural -> natural -> natural*)
let round_down_to align addr:Nat_big_num.num=
     (let quot = (Nat_big_num.div addr align)
    in Nat_big_num.mul
    quot align)

(*val uint32_max : natural*)
let uint32_max:Nat_big_num.num=  (Nat_big_num.sub_nat ( Nat_big_num.pow_int( (Nat_big_num.of_int 2)) 32)( (Nat_big_num.of_int 1)))

(*val uint64_max : natural*)
let uint64_max:Nat_big_num.num=  (Nat_big_num.add (Nat_big_num.sub_nat (Nat_big_num.mul
    (* HACK around Lem's inability to parse 18446744073709551615:
     * the square of uint32_max is
     *       (2**32 - 1) (2**32 - 1)
     * i.e.   2**64 - 2**32 - 2**32 + 1
     * So
     * 2**64 - 1 =  uint32_max * uint32_max  + 2**32 + 2**32 - 2
     *)
    uint32_max uint32_max)( (Nat_big_num.of_int 2))) (Nat_big_num.pow_int( (Nat_big_num.of_int 2))33))
    (* 18446744073709551615 *) (* i.e. 0x ffff ffff ffff ffff *)
    (* HMM. This still overflows int64 *)

(* The 2's complement of a value, at 64-bit width *)
(*val compl64 : natural -> natural*)
let compl64 v:Nat_big_num.num=  (Nat_big_num.add( (Nat_big_num.of_int 1)) (Nat_big_num.bitwise_xor v uint64_max))

(*val gcd : natural -> natural -> natural*)
let rec gcd a b:Nat_big_num.num=
     (if Nat_big_num.equal b( (Nat_big_num.of_int 0)) then a else gcd b ( Nat_big_num.modulus a b))

(*val lcm : natural -> natural -> natural*)
let lcm a b:Nat_big_num.num=  (Nat_big_num.div
    (* let _ = errln ("lcm of " ^ (show a) ^ " and " ^ (show b) ^ "?")
    in *)
    ( Nat_big_num.mul a b) (gcd a b))

(*val address_of_range : forall 'abifeature. element_range -> annotated_memory_image 'abifeature -> natural*)
let address_of_range el_range img2:Nat_big_num.num=
     (let (el_name, (start, len)) = el_range
    in
    (match Pmap.lookup el_name img2.elements with
        Some el ->
            (match el.startpos with
                Some addr -> Nat_big_num.add addr start
                | None -> failwith "address_of_range called for element with no address"
            )
        | None -> failwith "address_of_range called on nonexistent element"
    ))

(*val range_contains : (natural * natural) -> (natural * natural) -> bool*)
let range_contains (r1begin, r1len) (r2begin, r2len):bool=  (Nat_big_num.greater_equal
    (* r1 is at least as big as r2 *)
    r2begin r1begin && Nat_big_num.less_equal ( Nat_big_num.add r2begin r2len) ( Nat_big_num.add r1begin r1len))

(*val range_overlaps : (natural * natural) -> (natural * natural) -> bool*)
let range_overlaps (r1begin, r1len) (r2begin, r2len):bool=
     (( Nat_big_num.less r1begin ( Nat_big_num.add r2begin r2len) && Nat_big_num.greater ( Nat_big_num.add r1begin r1len) r2begin)
     || ( Nat_big_num.less r2begin ( Nat_big_num.add r1begin r1len) && Nat_big_num.greater ( Nat_big_num.add r2begin r2len) r1begin))

(*val is_partition : list (natural * natural) -> list (natural * natural) -> bool*)
let is_partition rs ranges:bool=
     (
    (* 1. each element of the first list falls entirely within some element
     * from the second list. *)let r_is_contained_by_some_range
     = (fun r -> List.fold_left (||) false (Lem_list.map (fun range1 -> range_contains range1 r) ranges))
    in
    List.for_all (fun r -> r_is_contained_by_some_range r) rs
    &&
    (* 2. elements of the first list do not overlap *)
    List.for_all (fun r -> List.for_all (fun r2 -> ( (Lem.pair_equal Nat_big_num.equal Nat_big_num.equal r (* should be "=="? *) r2)) || (not (range_overlaps r r2))) rs) rs)

(*val     nat_range : natural -> natural -> list natural*)
let rec nat_range base len:(Nat_big_num.num)list= 
  (
  if(Nat_big_num.equal len ( (Nat_big_num.of_int 0))) then ([]) else
    (base ::
       (nat_range ( Nat_big_num.add base ( (Nat_big_num.of_int 1)))
          ( Nat_big_num.sub_nat len ( (Nat_big_num.of_int 1))))))

(* Expand a sorted list of ranges into a list of bool, where the list contains
 * true if its index is included in one or more ranges, else false. *)
(*val expand_sorted_ranges : list (natural * natural) -> natural -> list bool -> list bool*)
let rec expand_sorted_ranges sorted_ranges min_length accum:(bool)list=
     ((match sorted_ranges with
        [] ->  List.rev_append (List.rev accum) (
            let pad_length = (Nat_big_num.max( (Nat_big_num.of_int 0)) ( Nat_big_num.sub_nat min_length (Missing_pervasives.length accum)))
            in
            (* let _ = Missing_pervasives.errln (
                "padding ranges cares list with " ^ (show pad_length) ^
                " cares (accumulated " ^ (show (Missing_pervasives.length accum)) ^
                ", min length " ^ (show min_length) ^ ")")
            in *)
            Missing_pervasives.replicate0 pad_length true)
     |  (base, len) :: more ->
            (* pad the accum so that it reaches up to base *)
            let up_to_base = (Missing_pervasives.replicate0 ( Nat_big_num.sub_nat base (Missing_pervasives.length accum)) true)
            in
            let up_to_end_of_range =  (List.rev_append (List.rev up_to_base) (Missing_pervasives.replicate0 len false))
            in
            expand_sorted_ranges more min_length ( List.rev_append (List.rev accum) up_to_end_of_range)
    ))

(*val expand_unsorted_ranges : list (natural * natural) -> natural -> list bool -> list bool*)
let rec expand_unsorted_ranges unsorted_ranges min_length accum:(bool)list=
     (expand_sorted_ranges (insertSortBy (fun (base1, len1) -> (fun (base2, len2) -> Nat_big_num.less base1 base2)) unsorted_ranges) min_length accum)

let swap_pairs dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b s:('a*'b)Pset.set=  (let x2 =(Pset.from_list (pairCompare  
  dict_Basic_classes_SetType_a.setElemCompare_method  dict_Basic_classes_SetType_b.setElemCompare_method) []) in  Pset.fold (fun(k, v) x2 -> if true then Pset.add (v, k) x2 else x2) s x2)

let by_range_from_by_tag dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b:('a*'b)Pset.set ->('b*'a)Pset.set= 
  (swap_pairs dict_Basic_classes_SetType_b dict_Basic_classes_SetType_a)

let by_tag_from_by_range dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b:('a*'b)Pset.set ->('b*'a)Pset.set= 
  (swap_pairs dict_Basic_classes_SetType_b dict_Basic_classes_SetType_a)

(*val filter_elements : forall 'abifeature. ((string * element) -> bool) ->
    annotated_memory_image 'abifeature -> annotated_memory_image 'abifeature*)
let filter_elements pred img2:'abifeature annotated_memory_image=
     (let new_elements = (Lem_map.fromList 
  (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) (let x2 = ([]) in  List.fold_right
   (fun(n, r) x2 ->
    if
    let result = (pred (n, r)) in
    if not result then
      (*let _ = Missing_pervasives.outln ("Discarding element named " ^ n) in*) result
    else result then (n, r) :: x2 else x2)
   (Pset.elements
      ((Pmap.bindings (pairCompare compare compare) img2.elements))) 
 x2))
    in
    let new_by_range =  (Pset.filter (fun (maybe_range, tag) -> (match maybe_range with
            None -> true
            | Some (el_name, el_range) ->  Pset.mem el_name (Pmap.domain new_elements)
        )) img2.by_range)
    in
    let new_by_tag = (let x2 =(Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) 
  []) in  Pset.fold (fun(k, v) x2 -> if true then Pset.add (v, k) x2 else x2)
   new_by_range x2)
    in
    { elements = new_elements
     ; by_range = new_by_range
     ; by_tag   = new_by_tag
     })

(*val tag_image : forall 'abifeature. range_tag 'abifeature -> string -> natural -> natural -> annotated_memory_image 'abifeature
    ->  annotated_memory_image 'abifeature*)
let tag_image t el_name el_offset tag_len img2:'abifeature annotated_memory_image=
     (let (k, v) = (Some (el_name, (el_offset, tag_len)), t)
    in
    let new_by_range = (Pset.add (k, v) img2.by_range)
    in
    let new_by_tag = (Pset.add (v, k) img2.by_tag)
    in
    { elements = (img2.elements)
     ; by_range = new_by_range
     ; by_tag   = new_by_tag
     })

(*val address_to_element_and_offset : forall 'abifeature. natural -> annotated_memory_image 'abifeature -> maybe (string * natural)*)
let address_to_element_and_offset query_addr img2:(string*Nat_big_num.num)option=
     (
    (* Find the element with the highest address <= addr.
     * What about zero-length elements?
     * Break ties on the bigger size. *)let (maybe_highest_le :  (Nat_big_num.num * string * element)option)
     = (List.fold_left (fun maybe_current_max_le -> (fun (el_name, el_rec) ->
        (*let _ = errln ("Saw element named `" ^ el_name ^ " with startpos " ^ (
            (match el_rec.startpos with Just addr -> ("0x" ^ (hex_string_of_natural addr)) | Nothing -> "(none)" end)
            ^ " and length " ^
            (match el_rec.length with Just len -> ("0x" ^ (hex_string_of_natural len)) | Nothing -> "(none)" end)
            ))
        in*)
        (match (maybe_current_max_le, el_rec.startpos) with
              (None,                                    None) -> None
            | (None,                                    Some this_element_pos) -> if Nat_big_num.less_equal this_element_pos query_addr
                                                                                     then Some (this_element_pos, el_name, el_rec)
                                                                                     else None
            | (Some (cur_max_le, cur_el_name, cur_el_rec), None) ->               maybe_current_max_le
            | (Some (cur_max_le, cur_el_name, cur_el_rec), Some this_element_pos) -> if Nat_big_num.less_equal this_element_pos query_addr
                                                                                        && ( Nat_big_num.greater this_element_pos cur_max_le
                                                                                         || ( Nat_big_num.equal this_element_pos cur_max_le
                                                                                             && ( (Lem.option_equal Nat_big_num.equal cur_el_rec.length1 (Some( (Nat_big_num.of_int 0)))))))
                                                                                        then Some (this_element_pos, el_name, el_rec)
                                                                                        else maybe_current_max_le
        )
    )) None (Pmap.bindings_list img2.elements))
    in
    (match maybe_highest_le with
        Some (el_def_startpos, el_name, el_rec) ->
            (* final sanity check: is the length definite, and if so, does the
             * element span far enough? *)
            (match el_rec.length1 with
                Some l -> if Nat_big_num.greater_equal (Nat_big_num.add el_def_startpos l) query_addr
                    then Some (el_name, Nat_big_num.sub_nat query_addr el_def_startpos)
                    else
                        (*let _ = errln ("Discounting " ^ el_name ^ " because length is too short") in*) None
                | None -> (*let _ = errln ("Gave up because element has unknown length") in*) None
            )
        | None ->
            (* no elements with a low enough assigned address, so nothing *)
            (*let _ = errln ("Found no elements with low enough address") in*) None
    ))

(*val element_and_offset_to_address : forall 'abifeature. (string * natural) -> annotated_memory_image 'abifeature -> maybe natural*)
let element_and_offset_to_address (el_name, el_off) img2:(Nat_big_num.num)option=
     ((match Pmap.lookup el_name img2.elements with
        Some el -> (match el.startpos with
                        Some addr -> Some ( Nat_big_num.add addr el_off)
                        | None -> None
                   )
        | None -> failwith ("error: nonexistent element: " ^ el_name)
    ))

let null_symbol_reference:symbol_reference=  ({
    ref_symname = ""
    ; ref_syment = elf64_null_symbol_table_entry
    ; ref_sym_scn =( (Nat_big_num.of_int 0))
    ; ref_sym_idx =( (Nat_big_num.of_int 0))
})

let null_elf_relocation_a:elf64_relocation_a=
   ({ elf64_ra_offset = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_ra_info   = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_ra_addend = (Nat_big_num.to_int64( (Nat_big_num.of_int 0)))
   })


let null_symbol_reference_and_reloc_site:symbol_reference_and_reloc_site=  ({
      ref = null_symbol_reference
    ; maybe_reloc =
        (Some   { ref_relent = null_elf_relocation_a
                ; ref_rel_scn =( (Nat_big_num.of_int 0))
                ; ref_rel_idx =( (Nat_big_num.of_int 0))
                ; ref_src_scn =( (Nat_big_num.of_int 0))
                })
    ; maybe_def_bound_to = None
    })

let null_symbol_definition:symbol_definition=  ({
    def_symname = ""
    ; def_syment = elf64_null_symbol_table_entry
    ; def_sym_scn =( (Nat_big_num.of_int 0))
    ; def_sym_idx =( (Nat_big_num.of_int 0))
    ; def_linkable_idx =( (Nat_big_num.of_int 0))
})

(*val pattern_possible_starts_in_one_byte_sequence : byte_pattern -> list byte -> natural -> list natural*)
let pattern_possible_starts_in_one_byte_sequence pattern seq offset:(Nat_big_num.num)list=
     (
    (* let _ = Missing_pervasives.errs ("Looking for matches of " ^
        (show (List.length pattern)) ^ "-byte pattern in " ^ (show (List.length seq)) ^ "-byte region\n")
    in *)accum_pattern_possible_starts_in_one_byte_sequence pattern (Nat_big_num.to_int (byte_pattern_length pattern)) seq (List.length seq) offset [])

(*val compute_virtual_address_adjustment : natural -> natural -> natural -> natural*)
let compute_virtual_address_adjustment max_page_size offset vaddr:Nat_big_num.num=  (Nat_big_num.modulus
  ( Nat_big_num.sub_nat vaddr offset) max_page_size)

(*val natural_of_be_byte_list : list byte -> natural*)
let natural_of_be_byte_list bytes:Nat_big_num.num=
   (List.fold_left (fun acc b -> Nat_big_num.add (Nat_big_num.mul
      acc( (Nat_big_num.of_int 256))) (Nat_big_num.of_int (Char.code b))
  )( (Nat_big_num.of_int 0)) bytes)

(*val natural_of_le_byte_list : list byte -> natural*)
let natural_of_le_byte_list bytes:Nat_big_num.num=
   (natural_of_be_byte_list (List.rev bytes))

(*val natural_of_byte_list : endianness -> list byte -> natural*)
let natural_of_byte_list endian bytes:Nat_big_num.num=
   ((match endian with
    | Big -> natural_of_be_byte_list bytes
    | Little -> natural_of_le_byte_list bytes
  ))

(*val extract_natural_field : natural -> element -> natural -> natural*)
let extract_natural_field width element1 offset:Nat_big_num.num=
     (
    (* Read n bytes from the contents *)let maybe_bytes = (take0 width (drop0 offset element1.contents))
    in
    let bytes = (Lem_list.map (fun mb -> (match mb with None -> Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 0))) | Some mb -> mb )) maybe_bytes)
    in
    (* FIXME: do we want little- or big-endian? *)
    natural_of_le_byte_list bytes)

(*val natural_to_le_byte_list : natural -> list byte*)
let rec natural_to_le_byte_list n:(char)list=
     ((Char.chr (Nat_big_num.to_int ( Nat_big_num.modulus n( (Nat_big_num.of_int 256))))) :: (let d =(Nat_big_num.div n( (Nat_big_num.of_int 256))) in if Nat_big_num.equal d( (Nat_big_num.of_int 0)) then [] else natural_to_le_byte_list ( Nat_big_num.div n( (Nat_big_num.of_int 256)))))

(*val natural_to_be_byte_list : natural -> list byte*)
let natural_to_be_byte_list n:(char)list=
     (List.rev (natural_to_le_byte_list n))

(*val natural_to_byte_list : endianness -> natural -> list byte*)
let natural_to_byte_list endian n:(char)list=
     ((match endian with
      | Big -> natural_to_be_byte_list n
      | Little -> natural_to_le_byte_list n
    ))

(*val natural_to_le_byte_list_padded_to : natural -> natural -> list byte*)
let rec natural_to_le_byte_list_padded_to width n:(char)list=
     (let bytes = (natural_to_le_byte_list n)
    in 
    List.rev_append (List.rev bytes) (replicate0 ( Nat_big_num.sub_nat width (length bytes)) (Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 0))))))

(*val natural_to_be_byte_list_padded_to : natural -> natural -> list byte*)
let natural_to_be_byte_list_padded_to width n:(char)list=
     (List.rev (natural_to_le_byte_list_padded_to width n))

(*val natural_to_byte_list_padded_to : endianness -> natural -> natural -> list byte*)
let natural_to_byte_list_padded_to endian width n:(char)list=
     ((match endian with
      | Big -> natural_to_be_byte_list_padded_to width n
      | Little -> natural_to_le_byte_list_padded_to width n
    ))

(*val n2i : natural -> integer*)
let n2i:Nat_big_num.num ->Nat_big_num.num=  (fun n-> n)

(*val i2n: integer -> natural*)
let i2n:Nat_big_num.num ->Nat_big_num.num=  Nat_big_num.abs

(*val i2n_signed : nat -> integer -> natural*)
let i2n_signed width i:Nat_big_num.num=
     (if Nat_big_num.greater_equal i( (Nat_big_num.of_int 0)) then
        if Nat_big_num.greater_equal i (Nat_big_num.pow_int( (Nat_big_num.of_int 2)) (Nat_num.nat_monus width 1)) then failwith "overflow"
        else Nat_big_num.abs i
    else
        (* We manually encode the 2's complement of the negated value *)
        let negated = (Nat_big_num.abs ( Nat_big_num.sub( (Nat_big_num.of_int 0)) i)) in
        let (xormask : Nat_big_num.num) = ( Nat_big_num.sub_nat (Nat_big_num.pow_int( (Nat_big_num.of_int 2)) width)( (Nat_big_num.of_int 1))) in
        let compl = (Nat_big_num.add( (Nat_big_num.of_int 1)) (Nat_big_num.bitwise_xor negated xormask))
        in
        (*let _ = errln ("Signed value " ^ (show i) ^ " is 2's-compl'd to 0x" ^ (hex_string_of_natural compl))
        in*) compl)

(*val to_le_signed_bytes : natural -> integer -> list byte*)
let to_le_signed_bytes bytewidth i:(char)list=
     (natural_to_le_byte_list_padded_to bytewidth (i2n_signed (Nat_big_num.to_int (Nat_big_num.mul( (Nat_big_num.of_int 8))bytewidth)) i))

(*val to_le_unsigned_bytes : natural -> integer -> list byte*)
let to_le_unsigned_bytes bytewidth i:(char)list=
     (natural_to_le_byte_list_padded_to bytewidth (Nat_big_num.abs i))

(*val write_natural_field : natural -> natural -> element -> natural -> element*)
let write_natural_field new_field_value width element1 offset:element=
     (let pre_bytes = (take0 offset element1.contents)
    in
    let post_bytes = (drop0 ( Nat_big_num.add offset width) element1.contents)
    in
    (* FIXME: avoid hard-coding little-endian *)
    let field_bytes = (natural_to_le_byte_list new_field_value)
    in
    if Nat_big_num.greater (length field_bytes) width then failwith "internal error: relocation output unrepresentable"
    else
    {
        contents =  (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev pre_bytes) (let x2 = 
  ([]) in  List.fold_right (fun b x2 -> if true then Some b :: x2 else x2) field_bytes
   x2))) (replicate0 ( Nat_big_num.sub_nat width (length field_bytes)) (Some (Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 0)))))))) post_bytes)
        ; startpos = (element1.startpos)
        ; length1 = (element1.length1)
     })

(*val read_memory_image : forall 'abifeature. annotated_memory_image 'abifeature -> natural -> natural -> maybe (list byte)*)
let read_memory_image img2 start len:((char)list)option=
   (let stop = (Nat_big_num.add start len) in
  let elements1 = (Pmap.bindings_list img2.elements) in
  List.fold_left (fun maybe_field (_, el) ->
    let el_start = (assert_unwrap_maybe el.startpos) in
    (* let el_len = assert_unwrap_maybe el.length in *)
    let el_len = (Nat_big_num.of_int (List.length el.contents)) in (* TODO? *)
    let el_stop = (Nat_big_num.add el_start el_len) in
    (* Do not allow reading fields across elements *)
    if Nat_big_num.greater_equal start el_start && Nat_big_num.less_equal stop el_stop then
      (* TODO: check consistency if maybe_field is not Nothing *)
      let offset = (Nat_big_num.sub_nat start el_start) in
      let bp = (read_byte_pattern el.contents offset len) in
      let l = (byte_pattern_to_byte_list bp) in
      Some l
    else
      maybe_field
  ) None elements1)

(*val read_memory_image_byte_sequence : forall 'abifeature. annotated_memory_image 'abifeature -> natural -> natural -> maybe byte_sequence*)
let read_memory_image_byte_sequence img2 start len:(Byte_sequence_wrapper.byte_sequence)option=
   (let maybe_bl = (read_memory_image img2 start len) in
  Lem.option_map byte_sequence_of_byte_list maybe_bl)

(*val write_memory_image : forall 'abifeature. annotated_memory_image 'abifeature -> natural -> byte_pattern -> annotated_memory_image 'abifeature*)
let write_memory_image img2 start bp:'abifeature annotated_memory_image=
   (if (listEqualBy (Lem.option_equal (=)) bp []) then img2 else
  let len = (Nat_big_num.of_int (List.length bp)) in
  let stop = (Nat_big_num.add start len) in
  let elements1 = (Pmap.map (fun el ->
    let el_start = (assert_unwrap_maybe el.startpos) in
    (* let el_len = assert_unwrap_maybe el.length in *)
    let el_len = (Nat_big_num.of_int (List.length el.contents)) in (* TODO? *)
    let el_stop = (Nat_big_num.add el_start el_len) in
    let contents1 =
      (if Nat_big_num.greater_equal start el_start && Nat_big_num.less start el_stop then
        let write_start = (Nat_big_num.sub_nat start el_start) in
        let write_max_len = (Nat_big_num.sub_nat el_stop start) in
        let write_bp = (Lem_list.take (Nat_big_num.to_int write_max_len) bp) in
        (* let _ = Missing_pervasives.errln ("  Masking at 0x" ^ (hex_string_of_natural el_start) ^ "+0x" ^ (hex_string_of_natural write_start) ^ " max_len=0x" ^ (hex_string_of_natural write_max_len) ^ " len=0x" ^ (hex_string_of_natural (naturalFromNat (List.length write_bp)))) in *)
        write_byte_pattern el.contents write_start write_bp
      else if Nat_big_num.greater_equal stop el_start && Nat_big_num.less stop el_stop then
        (* Case el_start < start is handled above *)
        let _ = (Lem_assert_extra.ensure ( Nat_big_num.greater_equal el_start start) "write_memory_image: internal failure") in
        let write_bp = (Lem_list.drop (Nat_big_num.to_int ( Nat_big_num.sub_nat el_start start)) bp) in
        (* let _ = Missing_pervasives.errln ("  Masking at 0x" ^ (hex_string_of_natural el_start) ^ "+0 len=0x" ^ (hex_string_of_natural (naturalFromNat (List.length write_bp)))) in *)
        write_byte_pattern el.contents( (Nat_big_num.of_int 0)) write_bp
      else
        el.contents)
    in
    {
      startpos = (Some el_start);
      length1 = (Some el_len);
      contents = contents1
    }
  ) img2.elements) in
  {
    elements = elements1;
    by_range = (img2.by_range);
    by_tag = (img2.by_tag)
  })

let mask_memory_image img2 start len:'a annotated_memory_image=
   (if Nat_big_num.equal len( (Nat_big_num.of_int 0)) then img2 else
  let bp = (Lem_list.replicate (Nat_big_num.to_int len) None) in
  write_memory_image img2 start bp)

let memory_image_element_at img2 addr:(element)option=
   (let elements1 = (Pmap.bindings_list img2.elements) in
  let maybe_tuple = (Lem_list.list_find_opt (fun (_, e) ->
    let start = (assert_unwrap_maybe e.startpos) in
    let len = (assert_unwrap_maybe e.length1) in Nat_big_num.greater_equal
    addr start && Nat_big_num.less addr (Nat_big_num.add start len)
  ) elements1) in
  Lem.option_map (fun (_, e) -> e) maybe_tuple)