package linksem

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file elf_memory_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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
(*Generated by Lem from elf_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 Set*)
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_symbol_table
open Elf_types_native_uint
open Elf_relocation
open String_table

open Memory_image
open Abis

type elf_memory_image = any_abi_feature annotated_memory_image

let elf_section_is_special0 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))

(*val noop_reloc : forall 'abifeature. natural -> ((maybe elf64_symbol_table_entry -> natural) * (annotated_memory_image 'abifeature -> maybe natural))*)
let noop_reloc0 r:((elf64_symbol_table_entry)option ->Nat_big_num.num)*('abifeature annotated_memory_image ->(Nat_big_num.num)option)=  ((fun r_type -> (Nat_big_num.of_int 8)), (fun sym_val -> None))

let empty_elf_memory_image:(any_abi_feature)annotated_memory_image=  ({
      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)))))
})

(* HMM. For the elf_ident, I don't really want to express it this way.
 * I want something more bidirectional: something that can tell me
 * not only that a given ident is valid for a given ABI, but also,
 * to *construct* an ident for a given abstract ELF file satisfying x.
 * This is very much like a lens.
 *
 * Similarly for relocs, I might want a way to map back to an allowable
 * *concrete* representation, from some *abstract* description of the
 * reloc's intent (i.e. a symbol binding: "point this reference at symbol
 * Foo"), given the constraints imposed by the ABI (such as "use only
 * RELA, not rel". FIXME: figure out how to lensify what we're doing. *)

type elf_range_tag = any_abi_feature range_tag

let null_section_header_table:elf_file_feature=  (ElfSectionHeaderTable([]))
let null_program_header_table:elf_file_feature=  (ElfProgramHeaderTable([]))
let null_elf_header:elf64_header=  ({
     elf64_ident    = ([])
   ; elf64_type     = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_machine  = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_version  = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_entry    = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_phoff    = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_shoff    = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_flags    = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_ehsize   = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_phentsize= (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_phnum    = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_shentsize= (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_shnum    = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_shstrndx = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   })

(* Here we build the image of a file in file offset space.
 * To transform to memory space, we
 *
 * - switch positions to be addresses
 * - switch lengths of nobits etc. to be memory lengths
 * - PROBLEM: an offset might map to >1 virtual address.
 *   So we have to clone it as multiple elements.
 *   Each gets a label identifying the "file feature" it came from
 *   -- i.e. sections, ELF header, SHT and PHT are all file features.
 * - PROBLEM: the memory image might only contain part of an element.
 *   We need to reflect this truncatedness somehow in the label.
 *
 * Is the offset-space view really useful?
 * SORT OF: want to be able to make an image out of relocatable ELF files
 * that have no address assignments or phdrs yet.
 * AHA. NO. This is not an offset-space view; it's a sectionwise memory view.
 * All allocatable sections become elements with Nothing as their address.
 * The remainder of the ELF file *should* be represented as labels.
 * But, hmm, some stuff like the ELF header and SHT will likely get discarded.
 *
 * In short, we should work entirely with memory space.
 * Then
 *
 * - do we want to encode the aliasing of multiple virtual addresses
 *   down to single "features" in offset-space, like multiple mappings
 *   of the ELF header, say?
 *)

(*val offset_to_vaddr_mappings : elf64_file -> natural -> list (natural * elf64_interpreted_segment)*)
let offset_to_vaddr_mappings f off:(Nat_big_num.num*elf64_interpreted_segment)list=
     (Lem_list.mapMaybe (fun ph ->
        if Nat_big_num.greater_equal off ph.elf64_segment_offset
            && Nat_big_num.less off (Nat_big_num.add ph.elf64_segment_base ph.elf64_segment_size)
        then Some ( Nat_big_num.add ph.elf64_segment_base ( Nat_big_num.sub_nat off ph.elf64_segment_offset), ph)
        else None
    ) f.elf64_file_interpreted_segments)

(*val gensym : string -> string*)
let gensym hint:string=  hint (* FIXME: remember duplicates *)

(*val extract_symbol : (elf64_symbol_table * string_table * natural) -> natural -> maybe (string * elf64_symbol_table_entry)*)
let extract_symbol symtab_triple symidx:(string*elf64_symbol_table_entry)option=
     (let (symtab, strtab, scnidx) = symtab_triple
    in
    (match Ml_bindings.list_index_big_int symidx symtab with
        Some ent ->
            (match (get_string_at (Uint32_wrapper.to_bigint ent.elf64_st_name) strtab) with
                Success str -> Some (str, ent)
                | Fail _ -> Some ("", ent)    (* ELF doesn't distinguish "no string" from "empty string" *)
            )
      | None -> None
    ))

(*val extract_satisfying_symbols : (elf64_symbol_table * string_table * natural) ->
    (elf64_symbol_table_entry -> bool) -> list (string * elf64_symbol_table_entry * natural (* scnidx *) * natural (* symidx *))*)
let extract_satisfying_symbols symtab_triple pred:(string*elf64_symbol_table_entry*Nat_big_num.num*Nat_big_num.num)list=
     (let (symtab, strtab, scnidx) = symtab_triple
    in
    (*let _ = Missing_pervasives.errln ("extracting satisfying symbols from symtab index " ^ (show scnidx) ^ ", size "
        ^ (show (length symtab)) )
    in*)
    mapMaybei (fun symidx -> (fun ent ->
        ((match (get_string_at (Uint32_wrapper.to_bigint ent.elf64_st_name) strtab) with
            Success str ->
                (* exclude those that don't match *)
                if (pred ent)
                then Some(str, ent, scnidx, symidx)
                else None
            | Fail s -> (*let _ = Missing_pervasives.errln ("couldn't get string from strtab of symtab with index " ^ (show scnidx)
                ^ ": " ^ s) in *)
                None
        ))
        )) symtab)

(*val extract_all_symbols : (elf64_symbol_table * string_table * natural) -> list (string * elf64_symbol_table_entry * natural (* scnidx *) * natural (* symidx *))*)
let extract_all_symbols symtab_triple:(string*elf64_symbol_table_entry*Nat_big_num.num*Nat_big_num.num)list=  (extract_satisfying_symbols symtab_triple (fun _ -> true))

let definitions_pred:elf64_symbol_table_entry ->bool=  (fun ent -> not (Nat_big_num.equal (Uint32_wrapper.to_bigint ent.elf64_st_shndx) stn_undef))
let references_pred:elf64_symbol_table_entry ->bool=  (fun ent -> Nat_big_num.equal (Uint32_wrapper.to_bigint ent.elf64_st_shndx) stn_undef && (not (is_elf64_null_entry ent)))

(*val extract_definitions_from_symtab_of_type : natural -> elf64_file -> list symbol_definition*)
let extract_definitions_from_symtab_of_type t e:(symbol_definition)list=
     ((match ( bind (find_elf64_symtab_by_type t e) (fun symtab -> (
        let (allsyms : (string * elf64_symbol_table_entry * Nat_big_num.num (* scnidx *) * Nat_big_num.num (* symidx *)) list)
         = (extract_satisfying_symbols symtab definitions_pred)
        in
        let (extracted : symbol_definition list)
         = (mapMaybei (fun i -> (fun (str, ent, scnidx, symidx) -> Some {
                   def_symname = str
                 ; def_syment = ent
                 ; def_sym_scn = scnidx
                 ; def_sym_idx = symidx
                 ; def_linkable_idx =( (Nat_big_num.of_int 0))
                 })) allsyms)
        in return extracted
    ))) with Fail _ -> [] | Success x -> x ))

(*val extract_references_from_symtab_of_type : natural -> elf64_file -> list symbol_reference*)
let extract_references_from_symtab_of_type t e:(symbol_reference)list=
     ((match ( bind (find_elf64_symtab_by_type t e) (fun symtab -> (
    let (allsyms : (string * elf64_symbol_table_entry * Nat_big_num.num (* scnidx *) * Nat_big_num.num (* symidx *)) list)
     = (extract_satisfying_symbols symtab references_pred)
    in
    let (extracted : symbol_reference list) =
        (mapMaybei (fun symidx -> (fun (str, ent, scnidx, symidx) -> Some {
                   ref_symname = str
                 ; ref_syment = ent
                 ; ref_sym_scn = scnidx
                 ; ref_sym_idx = symidx
                 })) allsyms)
    in
    (*let _ = Missing_pervasives.errs ("Extracted " ^ (show (length allsyms)) ^ " undefined references: "
        ^ (show (List.map (fun (str, _, scnidx, symidx) -> (str, scnidx, symidx)) allsyms)) ^ "\n")
(*       ^ " (syminds "
        ^ (show (List.map (fun extracted -> extracted.ref_sym_idx) x)) ^ ", symnames "
        ^ (show (List.map (fun extracted -> extracted.ref_symname) x)) ^ ")") *)

    in*) return extracted
    ))) with Fail _ -> [] | Success x -> x ))

(*val extract_all_relocs : string -> elf64_file -> list (natural (* scn *) * natural (* rel idx *) * natural (* rel src scn *) * elf64_relocation_a)*)
let extract_all_relocs fname1 e:(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*elf64_relocation_a)list=
     (let (all_rel_sections : (Nat_big_num.num * elf64_interpreted_section) list) = (mapMaybei (fun i -> (fun isec1 ->
        if Nat_big_num.equal isec1.elf64_section_type sht_rel then Some (i, isec1) else None
    )) e.elf64_file_interpreted_sections)
    in
    (*let _ = Missing_pervasives.errln ("File " ^ fname ^ " has " ^ (show (length all_rel_sections)) ^
        " rel sections (indices " ^ (show (List.map (fun (scn, _) -> scn) all_rel_sections)) ^ ")")
    in*)
    let (all_rela_sections : (Nat_big_num.num * elf64_interpreted_section) list) = (mapMaybei (fun i -> (fun isec1 ->
        if Nat_big_num.equal isec1.elf64_section_type sht_rela then Some (i, isec1) else None
    )) e.elf64_file_interpreted_sections)
    in
    (*let _ = Missing_pervasives.errln ("File " ^ fname ^ " has " ^ (show (length all_rela_sections)) ^
        " rela sections (indices " ^ (show (List.map (fun (scn, _) -> scn) all_rela_sections)) ^ ")")
    in*)
    let rel_to_rela = (fun rel -> {
         elf64_ra_offset = (rel.elf64_r_offset)
       ; elf64_ra_info   = (rel.elf64_r_info)
       ; elf64_ra_addend = (Nat_big_num.to_int64( (Nat_big_num.of_int 0)))
    })
    in
    let endian = (get_elf64_header_endianness e.elf64_file_header)
    in
    (* Build per-section lists of rels paired with their originating section id.
     * We also pair each element with its index *in that section*, and then flatten
     * the whole lot using mapConcat. *)
    let (all_rels_list : (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * elf64_relocation_a) list) = (list_reverse_concat_map (fun (scn, isec1) ->
        (match read_elf64_relocation_section   isec1.elf64_section_size endian isec1.elf64_section_body
        with
            Success (relocs, _) ->
                (*let _ = Missing_pervasives.errln ("Rel section with index " ^ (show scn) ^ " has " ^ (show (length relocs)) ^
                    " entries")
                in*)
                mapMaybei (fun idx1 -> (fun rel -> Some (scn, idx1, isec1.elf64_section_info, rel_to_rela rel))) relocs
            | Fail _ -> []
        )) all_rel_sections)
    in
    let (all_relas_list : (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * elf64_relocation_a) list) = (list_reverse_concat_map (fun (scn, isec1) ->
        (match read_elf64_relocation_a_section isec1.elf64_section_size endian isec1.elf64_section_body
        with
            Success (relocs, _) ->
            (*let _ = Missing_pervasives.errln ("Rela section with index " ^ (show scn) ^ " has " ^ (show (length relocs)) ^
                " entries")
            in*)
            mapMaybei (fun idx1 -> (fun rela -> Some (scn, idx1, isec1.elf64_section_info, rela))) relocs
            | Fail _ -> []
        )) all_rela_sections)
    in 
    List.rev_append (List.rev all_rels_list) all_relas_list)

(*val extract_all_relocs_as_symbol_references : string -> elf64_file -> list symbol_reference_and_reloc_site*)
let extract_all_relocs_as_symbol_references fname1 e:(symbol_reference_and_reloc_site)list=   
(let maybe_guessed_abi = (Lem_list.list_find_opt (fun abi1 ->
        abi1.is_valid_elf_header e.elf64_file_header
    ) Abis.all_abis) in
    let a = ((match maybe_guessed_abi with
        | Some a -> a
        | None -> failwith "extract_all_relocs_as_symbol_references: unknown ABI"
    )) in
    let all_relocs = (extract_all_relocs fname1 e)
    in
    let all_symtab_triples_by_scnidx = (mapMaybei (fun scnidx -> (fun isec1 ->
        if Nat_big_num.equal isec1.elf64_section_type sht_symtab
        then
            let found = (find_elf64_symbols_by_symtab_idx scnidx e)
            in
            (match found with
                Fail _ -> None
                | Success triple -> Some (scnidx, triple)
            )
        else None
    )) e.elf64_file_interpreted_sections)
    in
    let (all_extracted_symtabs_by_scnidx : ( (Nat_big_num.num, ( (string * elf64_symbol_table_entry * Nat_big_num.num (* scnidx *) * Nat_big_num.num (* symidx *))list))Pmap.map))
     = (List.fold_left (fun acc -> (fun (scnidx, triple) -> Pmap.add scnidx (extract_all_symbols triple) acc)) (Pmap.empty Nat_big_num.compare) all_symtab_triples_by_scnidx)
    in
    (*let _ = Missing_pervasives.errln ("All extracted symtabs by scnidx: " ^ (show (Set_extra.toList (Map.toSet all_extracted_symtabs_by_scnidx))))
    in*)
    let ref_for_relocation_a_in_section_index = (fun rel_scn_idx -> (fun rel_idx -> (fun rela ->
        let rela_isec = ((match Ml_bindings.list_index_big_int rel_scn_idx e.elf64_file_interpreted_sections with
            Some x -> x
            | None -> failwith "relocation references nonexistent section"
        ))
        in
        let symtab_idx = (rela_isec.elf64_section_link)
        in
        (match Pmap.lookup symtab_idx all_extracted_symtabs_by_scnidx with
            None -> failwith "referenced symtab does not exist"
            | Some quads ->
                let (_, sym_idx) = (a.parse_reloc_info rela.elf64_ra_info)
                in
                let maybe_quad = (Ml_bindings.list_index_big_int sym_idx quads)
                in
                (match maybe_quad with
                    Some(symname, syment, scnidx, symidx) -> {
                           ref_symname = symname
                         ; ref_syment = syment
                         ; ref_sym_scn = symtab_idx
                         ; ref_sym_idx = sym_idx
                         }
                    | None -> failwith "reloc references symbol that does not exist" (*("reloc at index " ^ (show rel_idx) ^ " references symbol (index " ^ (show sym_idx) ^
                        ") that does not exist: symtab (index " ^ (show symtab_idx) ^ ") has " ^ (show (length quads)) ^ " entries")*)
                )
        )
    )))
    in
    (*let _ = Missing_pervasives.errs ("Extracted " ^ (show (length all_relocs)) ^ " reloc references (rel_scn, rel_idx, src_scn): "
        ^ (show (List.map (fun (rel_scn, rel_idx, srcscn, rela) -> (rel_scn, rel_idx, srcscn)) all_relocs)) ^ "\n")
    in*)
    Lem_list.map (fun (scn, idx1, srcscn, rela) -> {
          ref = ( (* NOTE that a reference is not necessarily to an undefined symbol! *)ref_for_relocation_a_in_section_index scn idx1 rela)
        ; maybe_reloc = (Some
           { ref_relent = rela
            ; ref_rel_scn = scn
            ; ref_rel_idx = idx1
            ; ref_src_scn = srcscn (* what section does the reference come from? it's the 'info' link of the rel section header *)
            })
        ; maybe_def_bound_to = None
        }) all_relocs)
OCaml

Innovation. Community. Security.