(*Generated by Lem from test_image.lem.*) open Lem_basic_classes open Lem_list open Lem_map open Lem_maybe open Lem_set open Missing_pervasives open Lem_num open Lem_assert_extra open Error open Elf64_file_of_elf_memory_image open Elf_relocation open Elf_header open Elf_file open Elf_interpreted_segment open Elf_program_header_table open Elf_symbol_table open Elf_types_native_uint open Abi_amd64_relocation open Abis open Elf_memory_image open Memory_image open Command_line open Input_list open Linkable_list open Byte_sequence open Link open Show let ref_rec:symbol_reference= ({ ref_symname = "test" (* symbol name *) ; ref_syment = ({ elf64_st_name = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) ; elf64_st_info = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) ; elf64_st_other = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) ; elf64_st_shndx = (Uint32.of_string (Nat_big_num.to_string shn_undef)) ; elf64_st_value = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) ; elf64_st_size = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) }) ; ref_sym_scn =(Nat_big_num.of_int 0) ; ref_sym_idx =(Nat_big_num.of_int 0) }) (* the record representing the symbol reference and relocation site *) let ref_and_reloc_rec:symbol_reference_and_reloc_site= ({ ref = ref_rec ; maybe_def_bound_to = None ; maybe_reloc = (Some( { ref_relent = ({ 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 r_x86_64_32)) ; elf64_ra_addend = (Nat_big_num.to_int64(Nat_big_num.of_int 0)) }) ; 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) } )) }) let def_rec:symbol_definition= ({ def_symname = "test" ; def_syment = ({ elf64_st_name = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) ; elf64_st_info = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) ; elf64_st_other = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) ; elf64_st_shndx = (Uint32.of_string (Nat_big_num.to_string shn_undef)) ; elf64_st_value = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) ; elf64_st_size = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) }) ; def_sym_scn =(Nat_big_num.of_int 0) ; def_sym_idx =(Nat_big_num.of_int 1) ; def_linkable_idx =(Nat_big_num.of_int 0) }) (*val meta : nat -> list ((maybe element_range) * elf_range_tag)*) let meta offset:((string*(Nat_big_num.num*Nat_big_num.num))option*(any_abi_feature)range_tag)list= ([ (Some (".text", (Nat_big_num.of_int 1,Nat_big_num.of_int 4)), SymbolRef(ref_and_reloc_rec)) ; (Some (".data", (Nat_big_num.of_int offset,Nat_big_num.of_int 8)), SymbolDef(def_rec)) ]) let img0 (addr : int) (data_size : int) instr_bytes:(any_abi_feature)annotated_memory_image= (let initial_img = ({ elements = (Lem_map.fromList (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) [(".text", { startpos = (Some(Nat_big_num.of_int 4194304)) ; length1 = (Some(Nat_big_num.of_int 16)) ; contents = (Lem_list.map (fun x -> Some x) instr_bytes) }); (".data", { startpos = (Some(Nat_big_num.of_int 4194320)) ; length1 = (Some (Nat_big_num.of_int data_size)) ; contents = (Lem_list.map (fun x -> Some x) (Lem_list.replicate data_size (Char.chr (Nat_big_num.to_int (Nat_big_num.of_int 42))))) }) ]) ; by_range = (Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) (meta ( Nat_num.nat_monus addr( 4194316)))) ; by_tag = (by_tag_from_by_range (instance_Basic_classes_SetType_Maybe_maybe_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_Num_natural_dict instance_Basic_classes_SetType_Num_natural_dict))) instance_Basic_classes_SetType_var_dict ((Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) (meta ( Nat_num.nat_monus addr( 4194316)))))) }) in let ref_input_item = ("test.o", Reloc(Sequence([])), ((File(Filename("blah"), Command_line.null_input_file_options)), [InCommandLine(Nat_big_num.of_int 0)])) in let ref_linkable_item = (RelocELF(initial_img), ref_input_item, Input_list.null_input_options) in let bindings_by_name = (Lem_map.fromList (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) [ ("test", [(Nat_big_num.of_int 0, ((Nat_big_num.of_int 0, ref_rec, ref_linkable_item), Some(Nat_big_num.of_int 0, def_rec, ref_linkable_item)))]) ]) in relocate_output_image Abis.sysv_amd64_std_abi bindings_by_name initial_img) (* XXX: DPM, no longer needed? let compute_relocated_bytes () = let res = let relocatable_program = List.map byte_of_natural [72; 199; 4; 37; 0; 0; 0; 0; 5; 0; 0; 0; 72; 139; 4; 37; 0; 0; 0; 0] in let ef = elf64_file_of_elf_memory_image sysv_amd64_std_abi id "at_least_some_relocations_relocate.out" (img relocatable_program) in get_elf64_executable_image ef >>= fun (segs_and_provenance, entry, mach) -> if mach = elf_ma_x86_64 then let filtered = List.filter (fun x -> x.elf64_segment_type = elf_pt_load) (List.map (fun (x, y) -> x) segs_and_provenance) in let filtered = List.map Byte_sequence.byte_list_of_byte_sequence (List.map (fun x -> x.elf64_segment_body) filtered) in let _ = List.map (fun x -> outln (show x)) filtered in return () else failwith "wrong machine type returned" in match res with | Success s -> outln "success" | Fail e -> errln e end *)