Source file `auxv.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
(*Generated by Lem from auxv.lem.*)
open Lem_basic_classes
open Lem_list
open Lem_maybe
open Lem_num
open Show
open Lem_string

open Byte_sequence
open Endianness
open Error
open Missing_pervasives

open Elf_types_native_uint

(* Legal values for auxiliary vector entry types. *)

let at_null : Nat_big_num.num= ( (Nat_big_num.of_int 0)) (** End of vector *)
let at_ignore : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** Entry should be ignored *)
let at_execfd : Nat_big_num.num= ( (Nat_big_num.of_int 2)) (** File descriptor of program *)
let at_phdr : Nat_big_num.num= ( (Nat_big_num.of_int 3)) (** Program headers for program *)
let at_phent : Nat_big_num.num= ( (Nat_big_num.of_int 4)) (** Size of program header entry *)
let at_phnum : Nat_big_num.num= ( (Nat_big_num.of_int 5)) (** Number of program headers *)
let at_pagesz : Nat_big_num.num= ( (Nat_big_num.of_int 6)) (** System page size *)
let at_base : Nat_big_num.num= ( (Nat_big_num.of_int 7)) (** Base address of interpreter *)
let at_flags : Nat_big_num.num= ( (Nat_big_num.of_int 8)) (** Flags *)
let at_entry : Nat_big_num.num= ( (Nat_big_num.of_int 9)) (** Entry point of program *)
let at_notelf : Nat_big_num.num= ( (Nat_big_num.of_int 10)) (** Program is not ELF *)
let at_uid : Nat_big_num.num= ( (Nat_big_num.of_int 11)) (** Real uid *)
let at_euid : Nat_big_num.num= ( (Nat_big_num.of_int 12)) (** Effective uid *)
let at_gid : Nat_big_num.num= ( (Nat_big_num.of_int 13)) (** Real gid *)
let at_egid : Nat_big_num.num= ( (Nat_big_num.of_int 14)) (** Effective gid *)
let at_clktck : Nat_big_num.num= ( (Nat_big_num.of_int 17)) (** Frequency of times() *)
(* Some more special a_type values describing the hardware. *)
let at_platform : Nat_big_num.num= ( (Nat_big_num.of_int 15)) (** String identifying platform. *)
let at_hwcap : Nat_big_num.num= ( (Nat_big_num.of_int 16)) (** Machine-dependent hints about processor capabilities. *)
(* This entry gives some information about the FPU initialization performed by the kernel. *)
let at_fpucw : Nat_big_num.num= ( (Nat_big_num.of_int 18)) (** Used FPU control word. *)
(* Cache block sizes. *)
let at_dcachebsize : Nat_big_num.num= ( (Nat_big_num.of_int 19)) (** Data cache block size. *)
let at_icachebsize : Nat_big_num.num= ( (Nat_big_num.of_int 20)) (** Instruction cache block size. *)
let at_ucachebsize : Nat_big_num.num= ( (Nat_big_num.of_int 21)) (** Unified cache block size. *)
(* A special ignored value for PPC, used by the kernel to control the interpretation of the AUXV. Must be > 16. *)
let at_ignoreppc : Nat_big_num.num= ( (Nat_big_num.of_int 22)) (** Entry should be ignored. *)
let at_secure : Nat_big_num.num= ( (Nat_big_num.of_int 23)) (** Boolean, was exec setuid-like? *)
let at_base_platform : Nat_big_num.num= ( (Nat_big_num.of_int 24)) (** String identifying real platforms.*)
let at_random : Nat_big_num.num= ( (Nat_big_num.of_int 25)) (** Address of 16 random bytes. *)
let at_hwcap2 : Nat_big_num.num= ( (Nat_big_num.of_int 26)) (** More machine-dependent hints about processor capabilities. *)
let at_execfn : Nat_big_num.num= ( (Nat_big_num.of_int 31)) (** Filename of executable. *)
(* Pointer to the global system page used for system calls and other nice things. *)
let at_sysinfo : Nat_big_num.num= ( (Nat_big_num.of_int 32))
let at_sysinfo_ehdr : Nat_big_num.num= ( (Nat_big_num.of_int 33))

(** Auxiliary vector *)
type elf64_auxv = {
  elf64_auxv_type : Uint64_wrapper.uint64;
  elf64_auxv_value : Uint64_wrapper.uint64
}

(* Defined in include/uapi/linux/elfcore.h *)
type elf64_siginfo = {
  elf64_si_signo : Uint64_wrapper.uint64;
  elf64_si_code : Uint64_wrapper.uint64;
  elf64_si_errno : Uint64_wrapper.uint64
}

(* Defined in include/uapi/linux/elfcore.h *)
type elf64_prstatus = {
  elf64_pr_info : elf64_siginfo;
}

(*val read_elf64_auxv : endianness -> byte_sequence -> error (elf64_auxv * byte_sequence)*)
let read_elf64_auxv endian bs:(elf64_auxv*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf64_xword endian bs) (fun (typ, bs) -> bind (read_elf64_xword endian bs) (fun (value, bs) ->
  let av = ({
    elf64_auxv_type = typ;
    elf64_auxv_value = value
  }) in
  return (av, bs))))

(*val read_all_elf64_auxv : endianness -> byte_sequence -> error (list elf64_auxv)*)
let rec read_all_elf64_auxv endian bs:((elf64_auxv)list)error=
   (if Nat_big_num.equal (Byte_sequence.length0 bs)( (Nat_big_num.of_int 0)) then
    fail "read_all_elf64_auxv: EOF before reading a NULL auxv"
  else bind (read_elf64_auxv endian bs) (fun (av, bs) ->
    if Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 av.elf64_auxv_type) at_null then
      return []
    else bind (read_all_elf64_auxv endian bs) (fun (next) ->
      return (av :: next))))

(*val find_elf64_auxv_value : list elf64_auxv -> natural -> error (maybe natural)*)
let find_elf64_auxv_value auxv_list auxv_type:((Nat_big_num.num)option)error=
   (Error.foldM (fun value auxv ->
    if Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 auxv.elf64_auxv_type) auxv_type then
      (match value with
        | None -> return (Some (Ml_bindings.nat_big_num_of_uint64 auxv.elf64_auxv_value))
        | Some _ -> Error.fail ("find_elf64_auxv_value: duplicate value for type " ^ (Nat_big_num.to_string auxv_type))
      )
    else
      return value
  ) None auxv_list)