Source file `abi_aarch64_le.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
82
(*Generated by Lem from abis/aarch64/abi_aarch64_le.lem.*)
(** [abi_aarch64_le] contains top-level definition for the AArch64 ABI (little-endian case).
  *)

open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_num
open Lem_maybe
open Lem_assert_extra
open Error
open Missing_pervasives

open Elf_header
open Elf_types_native_uint
open Elf_file
open Elf_interpreted_segment
open Elf_interpreted_section

open Endianness
(* open import Elf_memory_image *)
open Abi_classes
open Memory_image
open Abi_aarch64_relocation
open Abi_aarch64_le_elf_header

(** [abi_aarch64_le_compute_program_entry_point segs entry] computes the program
  * entry point using ABI-specific conventions.  On AArch64 the entry point in
  * the ELF header ([entry] here) is the real entry point.  On other ABIs, e.g.
  * PowerPC64, the entry point [entry] is a pointer into one of the segments
  * constituting the process image (passed in as [segs] here for a uniform
  * interface).
  *)
(*val abi_aarch64_le_compute_program_entry_point : list elf64_interpreted_segments -> elf64_addr -> error natural*)
let abi_aarch64_le_compute_program_entry_point segs entry:(Nat_big_num.num)error=
	 (return (Ml_bindings.nat_big_num_of_uint64 entry))

(*val header_is_aarch64_le : elf64_header -> bool*)
let header_is_aarch64_le h:bool= 
     (is_valid_elf64_header h
    && ((Lem.option_equal (=) (Lem_list.list_index h.elf64_ident (Nat_big_num.to_int elf_ii_data)) (Some (Uint32_wrapper.of_bigint elf_data_2lsb)))
    && (is_valid_abi_aarch64_le_machine_architecture (Uint32_wrapper.to_bigint h.elf64_machine)
    && is_valid_abi_aarch64_le_magic_number h.elf64_ident)))
    
type aarch64_le_abi_feature = GOT | PLT (* placeholder / FIXME *)

(*val abiFeatureCompare : aarch64_le_abi_feature -> aarch64_le_abi_feature -> Basic_classes.ordering*)
let abiFeatureCompare f1 f2:int= 
     ((match (f1, f2) with
        (GOT, GOT) -> 0
        | (GOT, PLT) -> (-1)
        | (PLT, PLT) -> 0
        | (PLT, GOT) -> 1
    ))

(*val abiFeatureTagEq : aarch64_le_abi_feature -> aarch64_le_abi_feature -> bool*)
let abiFeatureTagEq f1 f2:bool= 
     ((match (f1, f2) with
        (GOT, GOT) -> true
        | (PLT, PLT) -> true
        | (_, _) -> false
    ))

let instance_Basic_classes_Ord_Abi_aarch64_le_aarch64_le_abi_feature_dict:(aarch64_le_abi_feature)ord_class= ({

  compare_method = abiFeatureCompare;

  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(abiFeatureCompare f1 f2) (-1))));

  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (abiFeatureCompare f1 f2)(Pset.from_list compare [(-1); 0])));

  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(abiFeatureCompare f1 f2) 1)));

  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (abiFeatureCompare f1 f2)(Pset.from_list compare [1; 0])))})

let instance_Abi_classes_AbiFeatureTagEquiv_Abi_aarch64_le_aarch64_le_abi_feature_dict:(aarch64_le_abi_feature)abiFeatureTagEquiv_class= ({

  abiFeatureTagEquiv_method = abiFeatureTagEq})

(*val section_is_special : forall 'abifeature. elf64_interpreted_section -> annotated_memory_image 'abifeature -> bool*)
let section_is_special0 s f:bool= 
     (elf_section_is_special s f || (* FIXME *) false)