Source file `abi_cheri_mips64_dynamic.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
(*Generated by Lem from abis/cheri_mips64/abi_cheri_mips64_dynamic.lem.*)
open Lem_basic_classes
open Lem_maybe
open Lem_num
open Lem_string

open Error
open Missing_pervasives
open Show
open String_table

open Elf_dynamic
open Elf_types_native_uint

open Abi_mips64_dynamic

let abi_cheri_dt___caprelocs : Nat_big_num.num=  (natural_of_hex "0x7000c000") (** start of __cap_relocs section *)
let abi_cheri_dt___caprelocssz : Nat_big_num.num=  (natural_of_hex "0x7000c001") (** size of __cap_relocs section *)

(*val string_of_abi_cheri_dynamic_tag : natural -> maybe string*)
let string_of_abi_cheri_dynamic_tag m:(string)option=
   (if Nat_big_num.equal m abi_cheri_dt___caprelocs then
    Some "CHERI___CAPRELOCS"
  else if Nat_big_num.equal m abi_cheri_dt___caprelocssz then
    Some "CHERI___CAPRELOCSSZ"
  else
    None)

(*val string_of_abi_cheri_mips64_dynamic_tag : natural -> string*)
let string_of_abi_cheri_mips64_dynamic_tag m:string=
   ((match string_of_abi_cheri_dynamic_tag m with
    | Some s -> s
    | None -> string_of_abi_mips64_dynamic_tag m
  ))

(*val abi_cheri_tag_correspondence_of_tag : natural -> error tag_correspondence*)
let abi_cheri_tag_correspondence_of_tag m:(tag_correspondence)error=
   (if Nat_big_num.equal m abi_cheri_dt___caprelocs then
    return C_Ptr
  else if Nat_big_num.equal m abi_cheri_dt___caprelocssz then
    return C_Val
  else
    fail ("abi_cheri_tag_correspondence_of_tag: invalid CHERI dynamic tag 0x" ^ (hex_string_of_natural m)))

(*val abi_cheri_mips64_tag_correspondence_of_tag : natural -> error tag_correspondence*)
let abi_cheri_mips64_tag_correspondence_of_tag m:(tag_correspondence)error=
   ((match abi_cheri_tag_correspondence_of_tag m with
    | Success v -> return v
    | Fail _ -> abi_mips64_tag_correspondence_of_tag m
  ))

(*val abi_cheri_elf64_value_of_elf64_dyn : elf64_dyn -> string_table -> error elf64_dyn_value*)
let abi_cheri_elf64_value_of_elf64_dyn dyn stbl:(((Uint64_wrapper.uint64),(Uint64_wrapper.uint64))dyn_value)error=
   (let tag = (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag)) in
  if Nat_big_num.equal tag abi_cheri_dt___caprelocs then bind (match dyn.elf64_dyn_d_un with
      | D_Ptr v -> return v
      | _ -> fail "abi_cheri_elf64_value_of_elf64_dyn: __CAPRELOCS must be a PTR"
    ) (fun v ->
    return (Address v))
  else if Nat_big_num.equal tag abi_cheri_dt___caprelocssz then bind (match dyn.elf64_dyn_d_un with
      | D_Val v -> return v
      | _ -> fail "abi_cheri_elf64_value_of_elf64_dyn: __CAPSRELOCSSZ must be a Val"
    ) (fun v ->
    return (Numeric (Ml_bindings.nat_big_num_of_uint64 v)))
  else
    fail ("abi_cheri_elf64_value_of_elf64_dyn: invalid CHERI dynamic tag 0x" ^ (hex_string_of_natural tag)))

(*val abi_cheri_mips64_elf64_value_of_elf64_dyn : elf64_dyn -> string_table -> error elf64_dyn_value*)
let abi_cheri_mips64_elf64_value_of_elf64_dyn dyn stbl:(elf64_dyn_value)error=
   ((match abi_cheri_elf64_value_of_elf64_dyn dyn stbl with
    | Success v -> return v
    | Fail _ -> abi_mips64_elf64_value_of_elf64_dyn dyn stbl
  ))