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

open Byte_sequence
open Elf_file
open Elf_header
open Elf_relocation
open Elf_symbol_table
open Elf_types_native_uint
open Endianness
open Error
open Memory_image
open Missing_pervasives

open Abi_mips64_relocation

(* Relocation types *)

let r_mips_cheri_absptr : Nat_big_num.num= ( (Nat_big_num.of_int 70))
let r_mips_cheri_size : Nat_big_num.num= ( (Nat_big_num.of_int 71))
let r_mips_cheri_capability : Nat_big_num.num= ( (Nat_big_num.of_int 90))

(*val string_of_cheri_mips_relocation_subtype : natural -> string*)
let string_of_cheri_mips_relocation_subtype rel_type1:string=
   (if Nat_big_num.equal rel_type1 r_mips_cheri_absptr then
    "R_MIPS_CHERI_ABSPTR"
  else if Nat_big_num.equal rel_type1 r_mips_cheri_absptr then
    "R_MIPS_CHERI_SIZE"
  else if Nat_big_num.equal rel_type1 r_mips_cheri_capability then
    "R_MIPS_CHERI_CAPABILITY"
  else
    string_of_mips64_relocation_subtype rel_type1)

(*val string_of_cheri_mips64_relocation_type : natural -> string*)
let string_of_cheri_mips64_relocation_type rel_type1:string=
   (let (type1, type2, type3) = (get_mips64_relocation_subtypes rel_type1) in
  (string_of_cheri_mips_relocation_subtype type1)
    ^ ("/" ^ ((string_of_cheri_mips_relocation_subtype type2)
    ^ ("/" ^ (string_of_cheri_mips_relocation_subtype type3)))))

(*val cheri_mips64_reloc : forall 'abifeature. reloc_fn 'abifeature*)
let cheri_mips64_reloc r:bool*'abifeature reloc_apply_fn=
   ((match (string_of_cheri_mips64_relocation_type r) with
    (* TODO: it seems rather strange to return a natural with a capability in it.
       Should we do that? *)
    | "R_MIPS_CHERI_CAPABILITY/R_MIPS_NONE/R_MIPS_NONE" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 32) (* TODO: this is only for CHERI256 *), (fun s -> fun a -> fun ea -> failwith "cheri_mips64_reloc: unimplemented R_MIPS_CHERI_CAPABILITY"))))))
    | _ -> mips64_reloc r
  ))


(* CHERI __cap_relocs section *)

let abi_cheri_mips64_function_reloc_flag:Nat_big_num.num=  (natural_of_hex "0x8000000000000000")

type cheri_mips64_cap_reloc = {
  cheri_mips64_cap_reloc_location : Uint64_wrapper.uint64;
  cheri_mips64_cap_reloc_object : Uint64_wrapper.uint64;
  cheri_mips64_cap_reloc_offset : Uint64_wrapper.uint64;
  cheri_mips64_cap_reloc_size : Uint64_wrapper.uint64;
  cheri_mips64_cap_reloc_permissions : Uint64_wrapper.uint64
}

(*val read_cheri_mips64_cap_relocs : endianness -> byte_sequence -> error (list cheri_mips64_cap_reloc)*)
let rec read_cheri_mips64_cap_relocs endian bs:((cheri_mips64_cap_reloc)list)error=
   (if Nat_big_num.equal (Byte_sequence.length0 bs)( (Nat_big_num.of_int 0)) then return [] else bind (read_elf64_xword endian bs) (fun (location, bs) -> bind (read_elf64_xword endian bs) (fun (obj, bs) -> bind (read_elf64_xword endian bs) (fun (offset, bs) -> bind (read_elf64_xword endian bs) (fun (size2, bs) -> bind (read_elf64_xword endian bs) (fun (permissions, bs) ->
  let cap_reloc = ({
    cheri_mips64_cap_reloc_location = location;
    cheri_mips64_cap_reloc_object = obj;
    cheri_mips64_cap_reloc_offset = offset;
    cheri_mips64_cap_reloc_size = size2;
    cheri_mips64_cap_reloc_permissions = permissions
  }) in bind (read_cheri_mips64_cap_relocs endian bs) (fun next ->
  return (cap_reloc :: next))))))))

(*val cheri_mips64_cap_reloc_is_function : cheri_mips64_cap_reloc -> bool*)
let cheri_mips64_cap_reloc_is_function reloc1:bool=
   (let perms = (Ml_bindings.nat_big_num_of_uint64 reloc1.cheri_mips64_cap_reloc_permissions) in not (Nat_big_num.equal (Nat_big_num.bitwise_and perms abi_cheri_mips64_function_reloc_flag)( (Nat_big_num.of_int 0))))