Source file `abi_cheri_mips64_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
(*Generated by Lem from abis/cheri_mips64/abi_cheri_mips64_elf_header.lem.*)
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_cheri_mips64_data_encoding : natural*)
let abi_cheri_mips64_data_encoding:Nat_big_num.num=  elf_data_2msb

(*val abi_cheri_mips64_endianness : endianness*)
let abi_cheri_mips64_endianness:endianness=  Big (* Must match above *)

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

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

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

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

let ef_mips_abi_cheriabi : Nat_big_num.num=  (natural_of_hex "0x0000C000")

let ef_mips_mach_cheri128 : Nat_big_num.num=  (natural_of_hex "0x00C10000")
let ef_mips_mach_cheri256 : Nat_big_num.num=  (natural_of_hex "0x00C20000")

(*val is_valid_abi_cheri_mips64_machine_architecture : natural -> bool*)
let is_valid_abi_cheri_mips64_machine_architecture m:bool=  (Nat_big_num.equal
  m elf_ma_mips)

(*val is_valid_abi_cheri_mips64_magic_number : list unsigned_char -> bool*)
let is_valid_abi_cheri_mips64_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_cheri_mips64_file_class) &&
              ( Nat_big_num.equal(Uint32_wrapper.to_bigint data) abi_cheri_mips64_data_encoding)
      )
  ))

(*val is_pure_abi_cheri_mips64_flag : natural -> bool*)
let is_pure_abi_cheri_mips64_flag flags:bool=  (not (Nat_big_num.equal (Nat_big_num.bitwise_and flags ef_mips_abi_cheriabi)( (Nat_big_num.of_int 0))))

(*val is_valid_abi_cheri256_mips64_flag : natural -> bool*)
let is_valid_abi_cheri256_mips64_flag flags:bool=  (not (Nat_big_num.equal (Nat_big_num.bitwise_and flags ef_mips_mach_cheri256)( (Nat_big_num.of_int 0))))