diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/memory_image.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/memory_image.ml | 839 |
1 files changed, 0 insertions, 839 deletions
diff --git a/lib/ocaml_rts/linksem/memory_image.ml b/lib/ocaml_rts/linksem/memory_image.ml deleted file mode 100644 index fa9d1535..00000000 --- a/lib/ocaml_rts/linksem/memory_image.ml +++ /dev/null @@ -1,839 +0,0 @@ -(*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) - }) |