Source file `test_image.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
(*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
*)