Source file test_image.ml

(*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_wrapper.of_bigint( (Nat_big_num.of_int 0)))
                   ; elf64_st_info  = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
                   ; elf64_st_other = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
                   ; elf64_st_shndx = (Uint32_wrapper.of_bigint shn_undef)
                   ; elf64_st_value = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
                   ; elf64_st_size  = (Uint64_wrapper.of_bigint( (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_wrapper.of_bigint( (Nat_big_num.of_int 0)))
                 ; elf64_ra_info   = (Uint64_wrapper.of_bigint 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_wrapper.of_bigint( (Nat_big_num.of_int 0)))
                       ; elf64_st_info  = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
                       ; elf64_st_other = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
                       ; elf64_st_shndx = (Uint32_wrapper.of_bigint shn_undef)
                       ; elf64_st_value = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
                       ; elf64_st_size  = (Uint64_wrapper.of_bigint( (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(Byte_sequence.empty), ((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
*)