Source file `abi_aarch64_le_elf_header.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
(*Generated by Lem from abis/aarch64/abi_aarch64_le_elf_header.lem.*)
(** [abi_aarch64_le_elf_header] contains types and definitions relating to ABI
  * specific ELF header functionality for the AArch64 ABI (little-endian).
  *)

open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_num
open Lem_maybe
open Missing_pervasives

open Elf_header
open Elf_types_native_uint

open Endianness

(*val abi_aarch64_le_data_encoding : natural*)
let abi_aarch64_le_data_encoding:Nat_big_num.num=  elf_data_2lsb

(*val abi_aarch64_le_endianness : endianness*)
let abi_aarch64_le_endianness:endianness=  Little (* Must match above *)

(*val abi_aarch64_le_file_class : natural*)
let abi_aarch64_le_file_class:Nat_big_num.num=  elf_class_64

(*val abi_aarch64_le_file_version : natural*)
let abi_aarch64_le_file_version:Nat_big_num.num=  elf_ev_current

(*val abi_aarch64_le_page_size_min : natural*)
let abi_aarch64_le_page_size_min:Nat_big_num.num= ( (Nat_big_num.of_int 4096))

(*val abi_aarch64_le_page_size_max : natural*)
let abi_aarch64_le_page_size_max:Nat_big_num.num= ( (Nat_big_num.of_int 65536))

(** [is_valid_abi_aarch64_le_machine_architecture m] checks whether the ELF header's
  * machine architecture is valid according to the ABI-specific specification.
  * Machine architecture must be AArch64 (pg 60)
  *)
(*val is_valid_abi_aarch64_le_machine_architecture : natural -> bool*)
let is_valid_abi_aarch64_le_machine_architecture m:bool=  (Nat_big_num.equal
  m elf_ma_aarch64)

(** [is_valid_abi_aarch64_le_magic_number magic] checks whether the ELF header's
  * magic number is valid according to the ABI-specific specification.
  * File class must be 64-bit (pg 60)
  * Data encoding must be little endian (pg 60)
  *)
(*val is_valid_abi_aarch64_le_magic_number : list unsigned_char -> bool*)
let is_valid_abi_aarch64_le_magic_number magic:bool=
   ((match Lem_list.list_index magic (Nat_big_num.to_int elf_ii_class) with
    | None  -> false
    | Some cls ->
      (match Lem_list.list_index magic (Nat_big_num.to_int elf_ii_data) with
        | None   -> false
        | Some data ->
            ( Nat_big_num.equal(Uint32_wrapper.to_bigint cls) abi_aarch64_le_file_class) &&
              ( Nat_big_num.equal(Uint32_wrapper.to_bigint data) abi_aarch64_le_data_encoding)
      )
  ))