Source file `abi_power64_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
(*Generated by Lem from abis/power64/abi_power64_elf_header.lem.*)
(** [abi_power64_elf_header], Power64 ABI specific definitions related to the 
  * ELF file header.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_maybe
open Missing_pervasives

open Elf_header
open Elf_types_native_uint

open Endianness

(** [is_valid_abi_power64_machine_architecture m] checks whether the ELF header's
  * machine architecture is valid according to the ABI-specific specification.
  * Machine architecture must be Power64 (Section 4.1).
  *)
(*val is_valid_abi_power64_machine_architecture : nat -> bool*)
let is_valid_abi_power64_machine_architecture m:bool=
   (m = Nat_big_num.to_int elf_ma_ppc64)

(** [is_valid_abi_power64_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 (Section 4.1)
  * Data encoding must be little or big endian and must match the data encoding
  * of the file. (Section 4.1)
  *)
(*val is_valid_abi_power64_magic_number : list unsigned_char -> endianness -> bool*)
let is_valid_abi_power64_magic_number magic endian: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 ed ->
          (match endian with
            | Little ->
                ( Nat_big_num.equal(Uint32_wrapper.to_bigint cls) elf_class_64) &&
                  ( Nat_big_num.equal(Uint32_wrapper.to_bigint ed) elf_data_2lsb)
            | Big    ->
                ( Nat_big_num.equal(Uint32_wrapper.to_bigint cls) elf_class_64) &&
                  ( Nat_big_num.equal(Uint32_wrapper.to_bigint ed) elf_data_2msb)
          )
      )
  ))