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
147
148
149
150
151
152
153
154
155
156
157
158
|
(*Generated by Lem from main_link.lem.*)
open Lem_basic_classes
open Lem_function
open Lem_string
open Lem_tuple
open Lem_bool
open Lem_list
open Lem_sorting
(*import Map*)
(*import Set*)
(*import Set_extra*)
open Lem_num
open Lem_maybe
open Lem_assert_extra
open Byte_sequence
open Default_printing
open Error
open Missing_pervasives
open Show
open Endianness
open Elf_header
open Elf_file
open Elf_interpreted_section
open Elf_interpreted_segment
open Elf_section_header_table
open Elf_program_header_table
open Elf_types_native_uint
open Elf_relocation
open String_table
open Abi_amd64_elf_header
open Abi_amd64_serialisation
open Abis
(*import Gnu_ext_abi*)
open Command_line
open Input_list
open Linkable_list
open Memory_image
open Elf_memory_image
open Elf_memory_image_of_elf64_file
open Elf64_file_of_elf_memory_image
open Linker_script
open Link
(*val images_consistent : elf_memory_image -> elf_memory_image -> bool*)
let images_consistent img1 img2:bool=
(* img1.by_tag = img2.by_tag *) true
(*val correctly_linked : abi any_abi_feature -> linkable_list -> list string -> set link_option -> elf64_file -> maybe elf_memory_image*)
let correctly_linked a linkables names options eout:((any_abi_feature)annotated_memory_image)option=
(let output_image = (elf_memory_image_of_elf64_file a "(output file)" eout)
in
let (fresh, alloc_map, script1) = (default_linker_control_script(Nat_big_num.of_int 0) (Pmap.empty Nat_big_num.compare) a
(* user_text_segment_start *) ((match Command_line.find_option_matching_tag (TextSegmentStart(Nat_big_num.of_int 0)) options with Some(TextSegmentStart(addr)) -> Some addr | _ -> None ))
(* user_data_segment_start *) None
(* user_rodata_segment_start *) ((match Command_line.find_option_matching_tag (RodataSegmentStart(Nat_big_num.of_int 0)) options with Some(RodataSegmentStart(addr)) -> Some addr | _ -> None ))
(* elf_headers_size *)
( Nat_big_num.add(Nat_big_num.of_int
(* ELF header size *)64) (Nat_big_num.mul a.max_phnum(Nat_big_num.of_int 56)) (* size of one phdr *)
))
in
let linked_image = (link alloc_map script1 a options linkables)
in
if images_consistent output_image linked_image then Some linked_image else None)
(* We need to elaborate the command line to handle objects, archives
* and archive groups appropriately.
* We could imagine a relation between objects such that
* (o1, o2) is in the relation
* iff definitions in o1 might be used to satisfy references in o2. ("o1 supplies o2")
* If o1 is a .o, all other .o files are searched.
* If o1 comes from an archive and is not in a group, it only supplies *preceding* objects (whether from an archive or a .o).
* If o1 comes from an archive in a group, it supplies preceding objects and any objects from the same group.
*
* That doesn't capture the ordering, though:
* for each object, there's an ordered list of other objects
* in which to search for the *first* definition. *)
let ( _:unit) =
(let res =
(let (input_units1, link_options1) = (command_line ())
in
let items_and_options = (elaborate_input input_units1)
in
let (input_items, item_options) = (List.split items_and_options)
in
let _ = (prerr_endline ("Got " ^ ((Pervasives.string_of_int (List.length input_items)) ^ (" input items: {"
^ ((List.fold_left (^) "" (Lem_list.map (fun item -> (string_of_triple
instance_Show_Show_string_dict instance_Show_Show_Input_list_input_blob_dict (instance_Show_Show_tup2_dict instance_Show_Show_Command_line_input_unit_dict
(instance_Show_Show_list_dict
instance_Show_Show_Input_list_origin_coord_dict)) item) ^ ",\n") input_items)) ^ "}")))))
in
let output_filename = ((match Command_line.find_option_matching_tag (Command_line.OutputFilename("")) link_options1 with
None -> "impossible: no output file specified, despite default value of `a.out'"
| Some (Command_line.OutputFilename(s)) -> s
| _ -> "impossible: bad output filename option returned"
))
in
Byte_sequence.acquire output_filename >>= (fun out ->
let _ = (prerr_endline ("Successfully opened output file")) in
Elf_file.read_elf64_file out >>= (fun eout ->
let _ = (prerr_endline ("Output file seems to be an ELF file")) in
let guessed_abi = (list_find_opt (fun a -> a.is_valid_elf_header eout.elf64_file_header) all_abis)
in
let a = ((match guessed_abi with
Some a -> if (* get_elf64_osabi eout.elf64_file_header = elf_osabi_gnu *) true
(* The GNU linker does not set the ABI to "GNU", but happily uses GNU extensions.
* FIXME: delegate to a personality function here
*)
then let _ = (prerr_endline "Using GNU-extended ABI") in Gnu_ext_abi.gnu_extend (Abis.tls_extend a)
else (Abis.tls_extend a)
| None -> failwith "output file does not conform to any known ABI"
))
in
let make_linkable = (fun (it, opts) -> linkable_item_of_input_item_and_options a it opts)
in
let linkable_items_and_options = (Lem_list.map make_linkable items_and_options)
in
let names = (Lem_list.map
(string_of_triple instance_Show_Show_string_dict
instance_Show_Show_Input_list_input_blob_dict
(instance_Show_Show_tup2_dict
instance_Show_Show_Command_line_input_unit_dict
(instance_Show_Show_list_dict
instance_Show_Show_Input_list_origin_coord_dict))) input_items)
in
let maybe_symbolic_image = (correctly_linked a linkable_items_and_options names link_options1 eout)
in
let v = ((match maybe_symbolic_image with
None -> false
| Some img2 ->
(* generate some output, using the symbolic image we just got *)
let our_output_filename = (output_filename ^ ".test-out")
in
let f = (elf64_file_of_elf_memory_image a (fun x -> x) our_output_filename img2)
in
(match
bytes_of_elf64_file f >>= (fun bytes ->
Byte_sequence.serialise our_output_filename bytes)
with
Success _ -> true
| Fail s -> let _ = (print_endline ("error writing output: " ^ s)) in true
)
))
in
return (string_of_bool v))))
in
(match res with
| Fail err -> prerr_endline ("[!]: " ^ err)
| Success e -> prerr_endline e
))
|
