package linksem

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

Source file elf_note.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
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
(*Generated by Lem from elf_note.lem.*)
(** [elf_note] contains data types and functions for interpreting the .note
  * section/segment of an ELF file, and extracting information from that
  * section/segment.
  *)

open Lem_assert_extra
open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_maybe
open Lem_num
open Lem_string

open Auxv
open Byte_sequence
open Endianness
open Error
open Missing_pervasives
open Show

open Elf_program_header_table
open Elf_section_header_table
open Elf_types_native_uint

(** [elf32_note] represents the contents of a .note section or segment.
  *)
type elf32_note =
  { elf32_note_namesz : Uint32_wrapper.uint32 (** The size of the name field. *)
   ; elf32_note_descsz : Uint32_wrapper.uint32 (** The size of the description field. *)
   ; elf32_note_type   : Uint32_wrapper.uint32 (** The type of the note. *)
   ; elf32_note_name   : byte_sequence0 (** The byte sequence corresponding to the name string. *)
   ; elf32_note_desc   : byte_sequence0 (** The byte sequence corresponding to the desc string. *)
   }

(** [elf64_note] represents the contents of a .note section or segment.
  *)
type elf64_note =
  { elf64_note_namesz : Uint32_wrapper.uint32 (** The size of the name field. *)
   ; elf64_note_descsz : Uint32_wrapper.uint32 (** The size of the description field. *)
   ; elf64_note_type   : Uint32_wrapper.uint32 (** The type of the note. *)
   ; elf64_note_name   : byte_sequence0 (** The byte sequence corresponding to the name string. *)
   ; elf64_note_desc   : byte_sequence0 (** The byte sequence corresponding to the desc string. *)
   }

(* Legal values for note segment descriptor types for core files. *)

let nt_prstatus : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** Contains copy of prstatus struct *)
let nt_fpregset : Nat_big_num.num= ( (Nat_big_num.of_int 2)) (** Contains copy of fpregset struct *)
let nt_prpsinfo : Nat_big_num.num= ( (Nat_big_num.of_int 3)) (** Contains copy of prpsinfo struct *)
let nt_prxreg : Nat_big_num.num= ( (Nat_big_num.of_int 4)) (** Contains copy of prxregset struct *)
let nt_taskstruct : Nat_big_num.num= ( (Nat_big_num.of_int 4)) (** Contains copy of task structure *)
let nt_platform : Nat_big_num.num= ( (Nat_big_num.of_int 5)) (** String from sysinfo(SI_PLATFORM) *)
let nt_auxv : Nat_big_num.num= ( (Nat_big_num.of_int 6)) (** Contains copy of auxv array *)
let nt_gwindows : Nat_big_num.num= ( (Nat_big_num.of_int 7)) (** Contains copy of gwindows struct *)
let nt_asrs : Nat_big_num.num= ( (Nat_big_num.of_int 8)) (** Contains copy of asrset struct *)
let nt_pstatus : Nat_big_num.num= ( (Nat_big_num.of_int 10)) (** Contains copy of pstatus struct *)
let nt_psinfo : Nat_big_num.num= ( (Nat_big_num.of_int 13)) (** Contains copy of psinfo struct *)
let nt_prcred : Nat_big_num.num= ( (Nat_big_num.of_int 14)) (** Contains copy of prcred struct *)
let nt_utsname : Nat_big_num.num= ( (Nat_big_num.of_int 15)) (** Contains copy of utsname struct *)
let nt_lwpstatus : Nat_big_num.num= ( (Nat_big_num.of_int 16)) (** Contains copy of lwpstatus struct *)
let nt_lwpsinfo : Nat_big_num.num= ( (Nat_big_num.of_int 17)) (** Contains copy of lwpinfo struct *)
let nt_prfpxreg : Nat_big_num.num= ( (Nat_big_num.of_int 20)) (** Contains copy of fprxregset struct *)
let nt_siginfo : Nat_big_num.num=  (natural_of_hex "0x53494749") (** Contains copy of siginfo_t, size might increase *)
let nt_file : Nat_big_num.num=  (natural_of_hex "0x46494c45") (** Contains information about mapped files *)
let nt_prxfpreg : Nat_big_num.num=  (natural_of_hex "0x46e62b7f") (** Contains copy of user_fxsr_struct *)
let nt_ppc_vmx : Nat_big_num.num=  (natural_of_hex "0x100") (** PowerPC Altivec/VMX registers *)
let nt_ppc_spe : Nat_big_num.num=  (natural_of_hex "0x101") (** PowerPC SPE/EVR registers *)
let nt_ppc_vsx : Nat_big_num.num=  (natural_of_hex "0x102") (** PowerPC VSX registers *)
let nt_ppc_tar : Nat_big_num.num=  (natural_of_hex "0x103") (** Target Address Register *)
let nt_ppc_ppr : Nat_big_num.num=  (natural_of_hex "0x104") (** Program Priority Register *)
let nt_ppc_dscr : Nat_big_num.num=  (natural_of_hex "0x105") (** Data Stream Control Register *)
let nt_ppc_ebb : Nat_big_num.num=  (natural_of_hex "0x106") (** Event Based Branch Registers *)
let nt_ppc_pmu : Nat_big_num.num=  (natural_of_hex "0x107") (** Performance Monitor Registers *)
let nt_ppc_tm_cgpr : Nat_big_num.num=  (natural_of_hex "0x108") (** TM checkpointed GPR Registers *)
let nt_ppc_tm_cfpr : Nat_big_num.num=  (natural_of_hex "0x109") (** TM checkpointed FPR Registers *)
let nt_ppc_tm_cvmx : Nat_big_num.num=  (natural_of_hex "0x10a") (** TM checkpointed VMX Registers *)
let nt_ppc_tm_cvsx : Nat_big_num.num=  (natural_of_hex "0x10b") (** TM checkpointed VSX Registers *)
let nt_ppc_tm_spr : Nat_big_num.num=  (natural_of_hex "0x10c") (** TM Special Purpose Registers *)
let nt_ppc_tm_ctar : Nat_big_num.num=  (natural_of_hex "0x10d") (** TM checkpointed Target Address Register *)
let nt_ppc_tm_cppr : Nat_big_num.num=  (natural_of_hex "0x10e") (** TM checkpointed Program Priority Register *)
let nt_ppc_tm_cdscr : Nat_big_num.num=  (natural_of_hex "0x10f") (** TM checkpointed Data Stream Control Register *)
let nt_386_tls : Nat_big_num.num=  (natural_of_hex "0x200") (** i386 TLS slots (struct user_desc) *)
let nt_386_ioperm : Nat_big_num.num=  (natural_of_hex "0x201") (** x86 io permission bitmap (1=deny) *)
let nt_x86_xstate : Nat_big_num.num=  (natural_of_hex "0x202") (** x86 extended state using xsave *)
let nt_s390_high_gprs : Nat_big_num.num=  (natural_of_hex "0x300") (** s390 upper register halves *)
let nt_s390_timer : Nat_big_num.num=  (natural_of_hex "0x301") (** s390 timer register *)
let nt_s390_todcmp : Nat_big_num.num=  (natural_of_hex "0x302") (** s390 TOD clock comparator register *)
let nt_s390_todpreg : Nat_big_num.num=  (natural_of_hex "0x303") (** s390 TOD programmable register *)
let nt_s390_ctrs : Nat_big_num.num=  (natural_of_hex "0x304") (** s390 control registers *)
let nt_s390_prefix : Nat_big_num.num=  (natural_of_hex "0x305") (** s390 prefix register *)
let nt_s390_last_break : Nat_big_num.num=  (natural_of_hex "0x306") (** s390 breaking event address *)
let nt_s390_system_call : Nat_big_num.num=  (natural_of_hex "0x307") (** s390 system call restart data *)
let nt_s390_tdb : Nat_big_num.num=  (natural_of_hex "0x308") (** s390 transaction diagnostic block *)
let nt_arm_vfp : Nat_big_num.num=  (natural_of_hex "0x400") (** ARM VFP/NEON registers *)
let nt_arm_tls : Nat_big_num.num=  (natural_of_hex "0x401") (** ARM TLS register *)
let nt_arm_hw_break : Nat_big_num.num=  (natural_of_hex "0x402") (** ARM hardware breakpoint registers *)
let nt_arm_hw_watch : Nat_big_num.num=  (natural_of_hex "0x403") (** ARM hardware watchpoint registers *)
let nt_arm_system_call : Nat_big_num.num=  (natural_of_hex "0x404") (** ARM system call number *)
let nt_arm_sve : Nat_big_num.num=  (natural_of_hex "0x405") (** ARM Scalable Vector Extension registers *)

(* Legal values for the note segment descriptor types for object files. *)

let nt_version : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** Contains a version string. *)

(* FreeBSD-specific *)

let nt_procstat_proc : Nat_big_num.num= ( (Nat_big_num.of_int 8)) (** Procstat proc data. *)
let nt_procstat_files : Nat_big_num.num= ( (Nat_big_num.of_int 9)) (** Procstat files data. *)
let nt_procstat_vmmap : Nat_big_num.num= ( (Nat_big_num.of_int 10)) (** Procstat vmmap data. *)
let nt_procstat_groups : Nat_big_num.num= ( (Nat_big_num.of_int 11)) (** Procstat groups data. *)
let nt_procstat_umask : Nat_big_num.num= ( (Nat_big_num.of_int 12)) (** Procstat umask data. *)
let nt_procstat_rlimit : Nat_big_num.num= ( (Nat_big_num.of_int 13)) (** Procstat rlimit data. *)
let nt_procstat_osrel : Nat_big_num.num= ( (Nat_big_num.of_int 14)) (** Procstat osreldate data. *)
let nt_procstat_psstrings : Nat_big_num.num= ( (Nat_big_num.of_int 15)) (** Procstat ps_strings data. *)
let nt_procstat_auxv : Nat_big_num.num= ( (Nat_big_num.of_int 16)) (** Procstat auxv data. *)


(** [elf64_nt_file_entry] represents the contents of a NT_FILE note entry. *)
type elf64_nt_file_entry =
  { elf64_nt_file_entry_start : Uint64_wrapper.uint64
   ; elf64_nt_file_entry_end : Uint64_wrapper.uint64
   ; elf64_nt_file_entry_offset : Uint64_wrapper.uint64
   ; elf64_nt_file_entry_filename : string
   }

(** [elf64_nt_file] represents the contents of a NT_FILE note. *)
type elf64_nt_file =
  { elf64_nt_file_count : Uint64_wrapper.uint64
   ; elf64_nt_file_page_size : Uint64_wrapper.uint64
   ; elf64_nt_file_entries : elf64_nt_file_entry list
   }

(** [elf64_nt_procstat_vmentry] represents the contents of a FreeBSD
    NT_PROCSTAT_VMMAP note entry (see `struct kinfo_vmentry`). *)
type elf64_nt_procstat_vmentry =
  { elf64_nt_procstat_vmentry_type : Uint32_wrapper.uint32 (** Type of map entry. *)
   ; elf64_nt_procstat_vmentry_start : Uint64_wrapper.uint64 (** Starting address. *)
   ; elf64_nt_procstat_vmentry_end : Uint64_wrapper.uint64 (** Finishing address. *)
   ; elf64_nt_procstat_vmentry_offset : Uint64_wrapper.uint64 (** Mapping offset in object *)
   ; elf64_nt_procstat_vmentry_vn_fileid : Uint64_wrapper.uint64 (** inode number if vnode *)
   ; elf64_nt_procstat_vmentry_vn_fsid : Uint32_wrapper.uint32 (** dev_t of vnode location *)
   ; elf64_nt_procstat_vmentry_flags : Uint32_wrapper.uint32 (** Flags on map entry. *)
   ; elf64_nt_procstat_vmentry_resident : Uint32_wrapper.uint32 (** Number of resident pages. *)
   ; elf64_nt_procstat_vmentry_protection : Uint32_wrapper.uint32 (** Protection bitmask. *)
   ; elf64_nt_procstat_vmentry_ref_count : Uint32_wrapper.uint32 (** VM obj ref count. *)
   ; elf64_nt_procstat_vmentry_shadow_count : Uint32_wrapper.uint32 (** VM obj shadow count. *)
   ; elf64_nt_procstat_vmentry_vn_type : Uint32_wrapper.uint32 (** Vnode type. *)
   ; elf64_nt_procstat_vmentry_vn_size : Uint64_wrapper.uint64 (** File size. *)
   ; elf64_nt_procstat_vmentry_vn_rdev : Uint32_wrapper.uint32 (** Device id if device. *)
   ; elf64_nt_procstat_vmentry_vn_mode : Uint32_wrapper.uint32 (** File mode. *)
   ; elf64_nt_procstat_vmentry_status : Uint32_wrapper.uint32 (** Status flags. *)
   ; elf64_nt_procstat_vmentry_path : string (** Path to VM obj, if any. *)
   }

(* Note names and descriptions are 4-byte aligned (even ELF64 notes) *)
(*val note_align : natural -> natural*)
let note_align n:Nat_big_num.num=  (Nat_big_num.mul
  ( Nat_big_num.div( Nat_big_num.add n( (Nat_big_num.of_int 3)))( (Nat_big_num.of_int 4)))( (Nat_big_num.of_int 4)))

(** [read_elf32_note endian bs0] transcribes an ELF note section from byte
  * sequence [bs0] assuming endianness [endian].  May fail if transcription fails
  * (i.e. if the byte sequence is not sufficiently long).
  *)
(*val read_elf32_note : endianness -> byte_sequence -> error (elf32_note * byte_sequence)*)
let read_elf32_note endian bs0:(elf32_note*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf32_word endian bs0) (fun (namesz, bs0) -> bind (read_elf32_word endian bs0) (fun (descsz, bs0) -> bind (read_elf32_word endian bs0) (fun (typ, bs0) -> bind (Byte_sequence.partition0 (note_align (Uint32_wrapper.to_bigint namesz)) bs0) (fun (name1, bs0) -> bind (Byte_sequence.partition0 (note_align (Uint32_wrapper.to_bigint descsz)) bs0) (fun (desc, bs0) -> bind (
  (* Strip padding *)Byte_sequence.takebytes (Uint32_wrapper.to_bigint namesz) name1) (fun (name1) -> bind (Byte_sequence.takebytes (Uint32_wrapper.to_bigint descsz) desc) (fun (desc) ->
  let note = ({
    elf32_note_namesz = namesz;
    elf32_note_descsz = descsz;
    elf32_note_type = typ;
    elf32_note_name = name1;
    elf32_note_desc = desc
  }) in
  return (note, bs0)))))))))

(** [read_elf64_note endian bs0] transcribes an ELF note section from byte
  * sequence [bs0] assuming endianness [endian].  May fail if transcription fails
  * (i.e. if the byte sequence is not sufficiently long).
  *)
(*val read_elf64_note : endianness -> byte_sequence -> error (elf64_note * byte_sequence)*)
let read_elf64_note endian bs0:(elf64_note*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf64_word endian bs0) (fun (namesz, bs0) -> bind (read_elf64_word endian bs0) (fun (descsz, bs0) -> bind (read_elf64_word endian bs0) (fun (typ, bs0) -> bind (Byte_sequence.partition0 (note_align (Uint32_wrapper.to_bigint namesz)) bs0) (fun (name1, bs0) -> bind (Byte_sequence.partition0 (note_align (Uint32_wrapper.to_bigint descsz)) bs0) (fun (desc, bs0) -> bind (
  (* Strip padding *)Byte_sequence.takebytes (Uint32_wrapper.to_bigint namesz) name1) (fun (name1) -> bind (Byte_sequence.takebytes (Uint32_wrapper.to_bigint descsz) desc) (fun (desc) ->
  let note = ({
    elf64_note_namesz = namesz;
    elf64_note_descsz = descsz;
    elf64_note_type = typ;
    elf64_note_name = name1;
    elf64_note_desc = desc
  }) in
  return (note, bs0)))))))))

(*val read_all_elf32_notes : endianness -> byte_sequence -> error (list elf32_note)*)
let rec read_all_elf32_notes endian bs:((elf32_note)list)error=
   (if Nat_big_num.equal (Byte_sequence.length0 bs)( (Nat_big_num.of_int 0)) then
    return []
  else bind (read_elf32_note endian bs) (fun (note, next_bs) -> bind (read_all_elf32_notes endian next_bs) (fun next_notes ->
    return (note :: next_notes))))

(*val read_all_elf64_notes : endianness -> byte_sequence -> error (list elf64_note)*)
let rec read_all_elf64_notes endian bs:((elf64_note)list)error=
   (if Nat_big_num.equal (Byte_sequence.length0 bs)( (Nat_big_num.of_int 0)) then
    return []
  else bind (read_elf64_note endian bs) (fun (note, next_bs) -> bind (read_all_elf64_notes endian next_bs) (fun next_notes ->
    return (note :: next_notes))))

(** [obtain_elf32_note_sections endian sht bs0] returns all note sections present
  * in an ELF file, as indicated by the file's section header table [sht], reading
  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
  * transcription of a note section fails.
  *)
(*val obtain_elf32_note_sections : endianness -> elf32_section_header_table ->
  byte_sequence -> error (list elf32_note)*)
let obtain_elf32_note_sections endian sht bs0:((elf32_note)list)error=
   (let note_sects =
    (List.filter (fun x ->
      x.elf32_sh_type = Uint32_wrapper.of_bigint sht_note
    ) sht)
  in
    foldM (fun notes x ->
      let offset = (Uint32_wrapper.to_bigint x.elf32_sh_offset) in
      let size2 = (Uint32_wrapper.to_bigint x.elf32_sh_size) in bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun rel -> bind (read_all_elf32_notes endian rel) (fun sec_notes ->
      return ( List.rev_append (List.rev sec_notes) notes)))
    ) [] note_sects)

(** [obtain_elf64_note_sections endian sht bs0] returns all note sections present
  * in an ELF file, as indicated by the file's section header table [sht], reading
  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
  * transcription of a note section fails.
  *)
(*val obtain_elf64_note_sections : endianness -> elf64_section_header_table ->
  byte_sequence -> error (list elf64_note)*)
let obtain_elf64_note_sections endian sht bs0:((elf64_note)list)error=
   (let note_sects =
    (List.filter (fun x ->
      x.elf64_sh_type = Uint32_wrapper.of_bigint sht_note
    ) sht)
  in
    foldM (fun notes x ->
      let offset = (Uint64_wrapper.to_bigint x.elf64_sh_offset) in
      let size2   = (Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_size) in bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun rel -> bind (read_all_elf64_notes endian rel) (fun sec_notes ->
      return ( List.rev_append (List.rev sec_notes) notes)))
    ) [] note_sects)

(** [obtain_elf32_note_segments endian pht bs0] returns all note segments present
  * in an ELF file, as indicated by the file's program header table [pht], reading
  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
  * transcription of a note section fails.
  *)
(*val obtain_elf32_note_segments : endianness -> elf32_program_header_table ->
  byte_sequence -> error (list elf32_note)*)
let obtain_elf32_note_segments endian pht bs0:((elf32_note)list)error=
   (let note_segs =
    (List.filter (fun x ->
      x.elf32_p_type = Uint32_wrapper.of_bigint elf_pt_note
    ) pht)
  in
    foldM (fun notes x ->
      let offset = (Uint32_wrapper.to_bigint x.elf32_p_offset) in
      let size2 = (Uint32_wrapper.to_bigint x.elf32_p_filesz) in bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun rel -> bind (read_all_elf32_notes endian rel) (fun seg_notes ->
      return ( List.rev_append (List.rev seg_notes) notes)))
    ) [] note_segs)

(** [obtain_elf64_note_segments endian pht bs0] returns all note segments present
  * in an ELF file, as indicated by the file's program header table [pht], reading
  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
  * transcription of a note section fails.
  *)
(*val obtain_elf64_note_segments : endianness -> elf64_program_header_table ->
  byte_sequence -> error (list elf64_note)*)
let obtain_elf64_note_segments endian pht bs0:((elf64_note)list)error=
   (let note_segs =
    (List.filter (fun x ->
      x.elf64_p_type = Uint32_wrapper.of_bigint elf_pt_note
    ) pht)
  in
    foldM (fun notes x ->
      let offset = (Uint64_wrapper.to_bigint x.elf64_p_offset) in
      let size2 = (Ml_bindings.nat_big_num_of_uint64 x.elf64_p_filesz) in bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun rel -> bind (read_all_elf64_notes endian rel) (fun seg_notes ->
      return ( List.rev_append (List.rev seg_notes) notes)))
    ) [] note_segs)

(** [obtain_elf32_note_section_and_segments endian pht sht bs0] returns all note
  * sections and segments present in an ELF file, as indicated by the file's
  * program header table [pht] and section header table [sht], reading
  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
  * transcription of a note section or segment fails.
  *)
(*val obtain_elf32_note_section_and_segments : endianness -> elf32_program_header_table ->
  elf32_section_header_table -> byte_sequence -> error (list elf32_note)*)
let obtain_elf32_note_section_and_segments endian pht sht bs0:((elf32_note)list)error=  (bind (obtain_elf32_note_segments endian pht bs0) (fun pht_notes -> bind (obtain_elf32_note_sections endian sht bs0) (fun sht_notes ->
  return ( List.rev_append (List.rev pht_notes) sht_notes))))

(** [obtain_elf64_note_section_and_segments endian pht sht bs0] returns all note
  * sections and segments present in an ELF file, as indicated by the file's
  * program header table [pht] and section header table [sht], reading
  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
  * transcription of a note section or segment fails.
  *)
(*val obtain_elf64_note_section_and_segments : endianness -> elf64_program_header_table ->
  elf64_section_header_table -> byte_sequence -> error (list elf64_note)*)
let obtain_elf64_note_section_and_segments endian pht sht bs0:((elf64_note)list)error=  (bind (obtain_elf64_note_segments endian pht bs0) (fun pht_notes -> bind (obtain_elf64_note_sections endian sht bs0) (fun sht_notes ->
  return ( List.rev_append (List.rev pht_notes) sht_notes))))

(** [name_string_of_elf32_note note] extracts the name string of an ELF note
  * section, interpreting the section's uninterpreted name field as a string.
  *)
(*val name_string_of_elf32_note : elf32_note -> string*)
let name_string_of_elf32_note note:string=
   (
  (* Strip NULL terminator *)(match Byte_sequence.takebytes ( Nat_big_num.sub_nat(Uint32_wrapper.to_bigint note.elf32_note_namesz)( (Nat_big_num.of_int 1))) note.elf32_note_name with
    | Success bs -> Byte_sequence.string_of_byte_sequence bs
    | Fail err -> failwith err
  ))

(** [name_string_of_elf64_note note] extracts the name string of an ELF note
  * section, interpreting the section's uninterpreted name field as a string.
  *)
(*val name_string_of_elf64_note : elf64_note -> string*)
let name_string_of_elf64_note note:string=
   (
  (* Strip NULL terminator *)(match Byte_sequence.takebytes ( Nat_big_num.sub_nat(Uint32_wrapper.to_bigint note.elf64_note_namesz)( (Nat_big_num.of_int 1))) note.elf64_note_name with
    | Success bs -> Byte_sequence.string_of_byte_sequence bs
    | Fail err -> failwith err
  ))

(** [read_freebsd_note_desc] unwraps a FreeBSD note description, checking that
    the size of  *)
(*val read_elf64_freebsd_note_desc : endianness -> elf64_note -> natural -> error byte_sequence*)
let read_elf64_freebsd_note_desc endian note struct_size:(Byte_sequence_wrapper.byte_sequence)error=
   (let note_name = (name_string_of_elf64_note note) in
  if not (note_name = "FreeBSD") then Error.fail ("read_elf64_freebsd_note_desc: `" ^ (note_name ^ "` isn't a FreeBSD note")) else bind (read_elf64_word endian note.elf64_note_desc) (fun (size2, bs) ->
  if not (Nat_big_num.equal (Uint32_wrapper.to_bigint size2) struct_size) then
    Error.fail ("read_elf64_freebsd_note_desc: unsupported struct size for FreeBSD note type " ^ ((Uint32_wrapper.to_string note.elf64_note_type) ^ (" (has " ^ ((Uint32_wrapper.to_string size2) ^ (", want " ^ ((Nat_big_num.to_string struct_size) ^ ")"))))))
  else
    return bs))

(* Functions to parse specific note types *)

(*val read_string' : byte_sequence -> error (list byte * byte_sequence)*)
let rec read_string' bs:((char)list*Byte_sequence_wrapper.byte_sequence)error=  (bind (Byte_sequence.read_char bs) (fun (b, bs) ->
  if b = '\000' then
    return ([], bs)
  else bind (read_string' bs) (fun (next, bs) ->
    return ((b :: next), bs))))

(* Parses a single NULL-terminated string *)
(* TODO: move this somewhere else *)
(*val read_string : byte_sequence -> error (string * byte_sequence)*)
let read_string bs:(string*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_string' bs) (fun (l, bs) ->
  return (Byte_sequence.string_of_byte_sequence (Byte_sequence.byte_sequence_of_byte_list l), bs)))

(*val read_elf64_nt_file_entry : endianness -> byte_sequence -> string -> error (elf64_nt_file_entry * byte_sequence)*)
let read_elf64_nt_file_entry endian bs filename1:(elf64_nt_file_entry*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf64_xword endian bs) (fun (map_start, bs) -> bind (read_elf64_xword endian bs) (fun (map_end, bs) -> bind (read_elf64_xword endian bs) (fun (file_offset, bs) ->
  let e = ({
    elf64_nt_file_entry_start = map_start;
    elf64_nt_file_entry_end = map_end;
    elf64_nt_file_entry_offset = file_offset;
    elf64_nt_file_entry_filename = filename1
  }) in
  return (e, bs)))))

(*val read_elf64_nt_file_entries : endianness -> byte_sequence -> byte_sequence -> error (list elf64_nt_file_entry)*)
let rec read_elf64_nt_file_entries endian entries_bs filenames_bs:((elf64_nt_file_entry)list)error=
   (if Nat_big_num.equal (Byte_sequence.length0 entries_bs)( (Nat_big_num.of_int 0)) then
    if not (Nat_big_num.equal (Byte_sequence.length0 filenames_bs)( (Nat_big_num.of_int 0))) then
      fail "read_nt_file_entries: malformed filenames (trailing data)"
    else
      return []
  else bind (read_string filenames_bs) (fun (filename1, filenames_bs) -> bind (read_elf64_nt_file_entry endian entries_bs filename1) (fun (e, entries_bs) -> bind (read_elf64_nt_file_entries endian entries_bs filenames_bs) (fun (next) ->
    return (e :: next)))))

(* See https://sourceware.org/ml/binutils/2012-10/msg00309.html *)
(*val read_elf64_nt_file : endianness -> byte_sequence -> error elf64_nt_file*)
let read_elf64_nt_file endian bs:(elf64_nt_file)error=  (bind (read_elf64_xword endian bs) (fun (count, bs) -> bind (read_elf64_xword endian bs) (fun (page_size, bs) ->
  let addr_size =( (Nat_big_num.of_int 8)) in bind (
  (* read_nt_file_entry reads 3 elf64_xword values *)Byte_sequence.partition0 ( Nat_big_num.mul (Nat_big_num.mul( (Nat_big_num.of_int 3)) addr_size) (Ml_bindings.nat_big_num_of_uint64 count)) bs) (fun (entries_bs, filenames_bs) -> bind (read_elf64_nt_file_entries endian entries_bs filenames_bs) (fun (entries) ->
  return {
    elf64_nt_file_count = count;
    elf64_nt_file_page_size = page_size;
    elf64_nt_file_entries = entries
  })))))

(*val read_elf64_nt_procstat_vmentry : endianness -> byte_sequence -> error (elf64_nt_procstat_vmentry * byte_sequence)*)
let read_elf64_nt_procstat_vmentry endian bs:(elf64_nt_procstat_vmentry*Byte_sequence_wrapper.byte_sequence)error=
   (let bs_len_before = (Byte_sequence.length0 bs) in bind (read_elf64_word endian bs) (fun (structsize, bs) -> bind (read_elf64_word endian bs) (fun (type_, bs) -> bind (read_elf64_xword endian bs) (fun (start, bs) -> bind (read_elf64_xword endian bs) (fun (end_, bs) -> bind (read_elf64_xword endian bs) (fun (offset, bs) -> bind (read_elf64_xword endian bs) (fun (vn_fileid, bs) -> bind (read_elf64_word endian bs) (fun (vn_fsid, bs) -> bind (read_elf64_word endian bs) (fun (flags, bs) -> bind (read_elf64_word endian bs) (fun (resident, bs) -> bind (read_elf64_word endian bs) (fun (protection, bs) -> bind (read_elf64_word endian bs) (fun (ref_count, bs) -> bind (read_elf64_word endian bs) (fun (shadow_count, bs) -> bind (read_elf64_word endian bs) (fun (vn_type, bs) -> bind (read_elf64_xword endian bs) (fun (vn_size, bs) -> bind (read_elf64_word endian bs) (fun (vn_rdev, bs) -> bind (read_elf64_half endian bs) (fun (vn_mode, bs) -> bind (read_elf64_half endian bs) (fun (status, bs) -> bind (read_elf64_word endian bs) (fun (vn_rdev, bs) -> bind (Byte_sequence.dropbytes ( Nat_big_num.mul( (Nat_big_num.of_int 12))( (Nat_big_num.of_int 4))) bs) (fun bs -> (* int _kve_ispare[12] *)
  let bs_len_after = (Byte_sequence.length0 bs) in
  let remaining = (Nat_big_num.sub_nat (Uint32_wrapper.to_bigint structsize) ( Nat_big_num.sub_nat bs_len_before bs_len_after)) in bind (
  (* path_bs is NULL-terminated *)Byte_sequence.partition0 remaining bs) (fun (path_bs, bs) -> bind (read_string path_bs) (fun (path, _) ->
  let e = ({
    elf64_nt_procstat_vmentry_type = type_;
    elf64_nt_procstat_vmentry_start = start;
    elf64_nt_procstat_vmentry_end = end_;
    elf64_nt_procstat_vmentry_offset = offset;
    elf64_nt_procstat_vmentry_vn_fileid = vn_fileid;
    elf64_nt_procstat_vmentry_vn_fsid = vn_fsid;
    elf64_nt_procstat_vmentry_flags = flags;
    elf64_nt_procstat_vmentry_resident = resident;
    elf64_nt_procstat_vmentry_protection = protection;
    elf64_nt_procstat_vmentry_ref_count = ref_count;
    elf64_nt_procstat_vmentry_shadow_count = shadow_count;
    elf64_nt_procstat_vmentry_vn_type = vn_type;
    elf64_nt_procstat_vmentry_vn_size = vn_size;
    elf64_nt_procstat_vmentry_vn_rdev = vn_rdev;
    elf64_nt_procstat_vmentry_vn_mode = vn_mode;
    elf64_nt_procstat_vmentry_status = status;
    elf64_nt_procstat_vmentry_path = path;
  }) in
  return (e, bs)))))))))))))))))))))))

(*val read_elf64_nt_procstat_vmmap : endianness -> byte_sequence -> error (list elf64_nt_procstat_vmentry)*)
let rec read_elf64_nt_procstat_vmmap endian bs:((elf64_nt_procstat_vmentry)list)error=
   (if Nat_big_num.equal (Byte_sequence.length0 bs)( (Nat_big_num.of_int 0)) then
    return []
  else bind (read_elf64_nt_procstat_vmentry endian bs) (fun (e, bs) -> bind (read_elf64_nt_procstat_vmmap endian bs) (fun (next) ->
    return (e :: next))))

(*val read_elf64_nt_procstat_psstrings : endianness -> byte_sequence -> error elf64_addr*)
let read_elf64_nt_procstat_psstrings endian bs:(Uint64_wrapper.uint64)error=  (bind (read_elf64_addr endian bs) (fun (addr, _) ->
  return addr))

(* Some various structs one can find in notes *)

(** [elf64_psstrings] is FreeBSD's `struct ps_strings` *)
type elf64_psstrings = {
  elf64_psstrings_argvstr : Uint64_wrapper.uint64;
  elf64_psstrings_nargvstr : Uint32_wrapper.uint32; (** the number of argument strings *)
  elf64_psstrings_envstr : Uint64_wrapper.uint64;
  elf64_psstrings_nenvstr : Uint32_wrapper.uint32; (** the number of environment strings *)
}

(*val read_elf64_psstrings : endianness -> byte_sequence -> error elf64_psstrings*)
let read_elf64_psstrings endian bs:(elf64_psstrings)error=  (bind (read_elf64_addr endian bs) (fun (argvstr, bs) -> bind (read_elf64_word endian bs) (fun (nargvstr, bs) -> bind (read_elf64_addr endian bs) (fun (envstr, bs) -> bind (read_elf64_word endian bs) (fun (nenvstr, _) ->
  return {
    elf64_psstrings_argvstr = argvstr;
    elf64_psstrings_nargvstr = nargvstr;
    elf64_psstrings_envstr = envstr;
    elf64_psstrings_nenvstr = nenvstr;
  })))))

(* Interpreted, abstracted, common versions of those structs *)

(** A mmap table entry suitable for both Linux and FreeBSD. *)
type mmap_entry = {
  mmap_entry_start : Nat_big_num.num;
  mmap_entry_end : Nat_big_num.num;
  mmap_entry_offset : Nat_big_num.num;
  mmap_entry_path : string
}

let read_nt_file_entries endian note_segs:((mmap_entry)list)error=
   (Error.foldM (fun acc note_seg ->
    let note_name = (name_string_of_elf64_note note_seg) in
    let note_type = (Uint32_wrapper.to_bigint note_seg.elf64_note_type) in
    if (note_name = "CORE") && Nat_big_num.equal note_type nt_file then bind (read_elf64_nt_file endian note_seg.elf64_note_desc) (fun nt_file1 ->
      let entries = (Lem_list.map (fun e ->
        let _ = (prerr_endline (
          "NT_FILE"
          ^ (" start=0x" ^ ((hex_string_of_natural (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_file_entry_start))
          ^ (" end=0x" ^ ((hex_string_of_natural (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_file_entry_end))
          ^ (" offset=0x" ^ ((hex_string_of_natural (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_file_entry_offset))
          ^ (" filename=`" ^ (e.elf64_nt_file_entry_filename ^ "`"))))))))
        )) in
        {
          mmap_entry_start = (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_file_entry_start);
          mmap_entry_end = (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_file_entry_end);
          mmap_entry_offset = (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_file_entry_offset);
          mmap_entry_path = (e.elf64_nt_file_entry_filename)
        }
      ) nt_file1.elf64_nt_file_entries) in
      return ( List.rev_append (List.rev acc) entries))
    else
      return acc
  ) [] note_segs)

let read_nt_procstat_vmmap endian note_segs:((mmap_entry)list)error=
   (Error.foldM (fun acc note_seg ->
    let note_name = (name_string_of_elf64_note note_seg) in
    let note_type = (Uint32_wrapper.to_bigint note_seg.elf64_note_type) in
    if (note_name = "FreeBSD") && Nat_big_num.equal note_type nt_procstat_vmmap then
      let struct_size = (natural_of_hex "0x488") in bind ( (* sizeof(struct kinfo_vmentry) *)read_elf64_freebsd_note_desc endian note_seg struct_size) (fun bs -> bind (read_elf64_nt_procstat_vmmap endian bs) (fun entries ->

      let entries = (Lem_list.map (fun e ->
        let _ = (prerr_endline (
          "NT_PROCSTAT_VMMAP"
          ^ (" start=0x" ^ ((hex_string_of_natural (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_procstat_vmentry_start))
          ^ (" end=0x" ^ ((hex_string_of_natural (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_procstat_vmentry_end))
          ^ (" offset=0x" ^ ((hex_string_of_natural (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_procstat_vmentry_offset))
          ^ (" path=`" ^ (e.elf64_nt_procstat_vmentry_path ^ "`"))))))))
        )) in
        {
          mmap_entry_start = (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_procstat_vmentry_start);
          mmap_entry_end = (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_procstat_vmentry_end);
          mmap_entry_offset = (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_procstat_vmentry_offset);
          mmap_entry_path = (e.elf64_nt_procstat_vmentry_path)
        }
      ) entries) in

      return ( List.rev_append (List.rev acc) entries)))
    else
      return acc
  ) [] note_segs)

(*val read_mmap_table : endianness -> list elf64_note -> error (list mmap_entry)*)
let read_mmap_table endian note_segs:((mmap_entry)list)error=  (bind (read_nt_file_entries endian note_segs) (fun nt_file_entries -> bind (read_nt_procstat_vmmap endian note_segs) (fun nt_procstat_vmmap1 ->
  (* TODO: don't allow both mmap table types to be present at the same time *)
  return ( List.rev_append (List.rev nt_file_entries) nt_procstat_vmmap1))))

(*val get_mmap_entry_at : list mmap_entry -> natural -> maybe mmap_entry*)
let get_mmap_entry_at mmap_table addr:(mmap_entry)option=
   (let l = (List.filter (fun e -> Nat_big_num.greater_equal
    addr e.mmap_entry_start && Nat_big_num.less addr e.mmap_entry_end
  ) mmap_table) in
  (match l with
    | [e] -> Some e
    | [] -> None
    | _ -> failwith ("get_mmap_entry_at: multiple mmap entries found at 0x" ^ (hex_string_of_natural addr))
  ))

let read_all_elf64_nt_auxv endian note_segs:((elf64_auxv)list)error=
   (Error.foldM (fun auxv_list note_seg ->
    let note_name = (name_string_of_elf64_note note_seg) in
    let note_type = (Uint32_wrapper.to_bigint note_seg.elf64_note_type) in
    if ((note_name = "CORE") && Nat_big_num.equal note_type nt_auxv)
        || ((note_name = "FreeBSD") && Nat_big_num.equal note_type nt_procstat_auxv) then
      let bs = (note_seg.elf64_note_desc) in
      let bs_res = (if note_name = "FreeBSD" then
        read_elf64_freebsd_note_desc endian note_seg( (Nat_big_num.of_int 16)) (* sizeof(Elf_Auxvinfo) *)
      else
        return bs)
      in bind bs_res (fun bs -> bind (Auxv.read_all_elf64_auxv endian bs) (fun l ->
      return ( List.rev_append (List.rev auxv_list) l)))
    else
      return auxv_list
  ) [] note_segs)
OCaml

Innovation. Community. Security.