(*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_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 Missing_pervasives (* Now we can define memory images *) type byte_pattern_element = char option type byte_pattern = byte_pattern_element list (* 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 -> reloc_site option -> Nat_big_num.num } (*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) (*val make_byte_pattern_revacc : list (maybe byte) -> list byte -> list bool -> list (maybe byte)*) let rec make_byte_pattern_revacc revacc bytes cares:((char)option)list= ((match bytes with [] -> List.rev revacc | b :: bs -> (match cares with care :: more -> make_byte_pattern_revacc ((if not care then None else Some b) :: revacc) bs more | _ -> failwith "make_byte_pattern: unequal length" ) )) (*val make_byte_pattern : list byte -> list bool -> list (maybe byte)*) let rec make_byte_pattern bytes cares:((char)option)list= (make_byte_pattern_revacc [] bytes cares) (*val relax_byte_pattern_revacc : list (maybe byte) -> list (maybe byte) -> list bool -> list (maybe byte)*) let rec relax_byte_pattern_revacc revacc bytes cares:((char)option)list= ((match bytes with [] -> List.rev revacc | b :: bs -> (match cares with care :: more -> relax_byte_pattern_revacc ((if not care then None else b) :: revacc) bs more | _ -> failwith ("relax_byte_pattern: unequal length") ) )) (*val relax_byte_pattern : list (maybe byte) -> list bool -> list (maybe byte)*) let rec relax_byte_pattern bytes cares:((char)option)list= (relax_byte_pattern_revacc [] bytes cares) type pad_fn = Nat_big_num.num -> char list (*val concretise_byte_pattern : list byte -> natural -> list (maybe byte) -> pad_fn -> list byte*) let rec concretise_byte_pattern rev_acc acc_pad bs pad:(char)list= ((match bs with [] -> let padding_bytes = (if Nat_big_num.greater acc_pad(Nat_big_num.of_int 0) then pad acc_pad else []) in List.rev ( List.rev_append (List.rev (List.rev padding_bytes)) rev_acc) | Some(b) :: more -> (* flush accumulated padding *) let padding_bytes = (if Nat_big_num.greater acc_pad(Nat_big_num.of_int 0) then pad acc_pad else []) in concretise_byte_pattern (b :: ( List.rev_append (List.rev (List.rev padding_bytes)) rev_acc))(Nat_big_num.of_int 0) more pad | None :: more -> concretise_byte_pattern rev_acc (Nat_big_num.add acc_pad(Nat_big_num.of_int 1)) more pad )) (*val byte_option_matches_byte : maybe byte -> byte -> bool*) let byte_option_matches_byte optb b:bool= ((match optb with None -> true | Some some -> some = b )) (*val byte_list_matches_pattern : list (maybe byte) -> list byte -> bool*) let rec byte_list_matches_pattern pattern bytes:bool= ((match pattern with [] -> true | optbyte :: more -> (match bytes with [] -> false | abyte :: morebytes -> byte_option_matches_byte optbyte abyte && byte_list_matches_pattern more morebytes ) )) (*val append_to_byte_pattern_at_offset : natural -> list (maybe byte) -> list (maybe byte) -> list (maybe byte)*) let append_to_byte_pattern_at_offset offset pat1 pat2:((char)option)list= (let pad_length = (Nat_big_num.sub_nat offset (Missing_pervasives.length pat1)) in if Nat_big_num.less pad_length(Nat_big_num.of_int 0) then failwith "can't append at offset already used" else List.rev_append (List.rev (List.rev_append (List.rev pat1) (Lem_list.replicate (Nat_big_num.to_int pad_length) None))) pat2) (*val accum_pattern_possible_starts_in_one_byte_sequence : list (maybe byte) -> nat -> list byte -> nat -> natural -> list natural -> list natural*) let rec accum_pattern_possible_starts_in_one_byte_sequence pattern pattern_len seq seq_len offset accum:(Nat_big_num.num)list= ( (* let _ = Missing_pervasives.errs ("At offset " ^ (show offset) ^ "... ") in *)(match pattern with [] -> (* let _ = Missing_pervasives.errs ("terminating with hit (empty pattern)\n") in *) offset :: accum | bpe :: more_bpes -> (* nonempty, so check for nonempty seq *) (match seq with [] -> (*let _ = Missing_pervasives.errs ("terminating with miss (empty pattern)\n") in *) accum (* ran out of bytes in the sequence, so no match *) | byte1 :: more_bytes -> let matched_this_byte = (byte_option_matches_byte bpe byte1) in (* let _ = Missing_pervasives.errs ("Byte " ^ (show byte) ^ " matched " ^ (show byte_pattern) ^ "? " ^ (show matched_this_byte) ^ "; ") in *) let sequence_long_enough = (seq_len >= pattern_len) in (* let _ = Missing_pervasives.errs ("enough bytes remaining (" ^ (show seq_len) ^ ") to match rest of pattern (" ^ (show pattern_len) ^ ")? " ^ (show sequence_long_enough) ^ "; ") in *) let matched_here = (matched_this_byte && (sequence_long_enough && byte_list_matches_pattern more_bpes more_bytes)) in (* let _ = Missing_pervasives.errs ("matched pattern anchored here? " ^ (show matched_this_byte) ^ "\n") in *) accum_pattern_possible_starts_in_one_byte_sequence pattern pattern_len more_bytes ( Nat_num.nat_monus seq_len( 1)) ( Nat_big_num.add offset(Nat_big_num.of_int 1)) (if matched_here then offset :: accum else 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.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) ; elf64_ra_info = (Uint64.of_string (Nat_big_num.to_string (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 : list (maybe byte) -> 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 (List.length pattern) seq (List.length seq) offset []) (*val byte_pattern_of_byte_sequence : byte_sequence -> list (maybe byte)*) let byte_pattern_of_byte_sequence seq:((char)option)list= ((match seq with Sequence(bs) -> Lem_list.map (fun b -> Some b) bs )) (*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 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? *) List.fold_left (fun acc -> fun next_byte -> Nat_big_num.add (Nat_big_num.mul acc(Nat_big_num.of_int 256)) (Nat_big_num.of_int (Char.code next_byte)) ) (Nat_big_num.of_int 0 : Nat_big_num.num) 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_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 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) })