Source file `abi_amd64.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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
(*Generated by Lem from abis/amd64/abi_amd64.lem.*)
(** [abi_amd64] contains top-level definition for the AMD64 ABI.
  *)

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

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 Memory_image
(* open import Elf_memory_image *)

open Abi_classes
open Abi_amd64_relocation
open Abi_amd64_elf_header

(** [abi_amd64_compute_program_entry_point segs entry] computes the program
  * entry point using ABI-specific conventions.  On AMD64 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_amd64_compute_program_entry_point : list elf64_interpreted_segments -> elf64_addr -> error natural*)
let abi_amd64_compute_program_entry_point segs entry:(Nat_big_num.num)error=
	 (return (Ml_bindings.nat_big_num_of_uint64 entry))

(*val header_is_amd64 : elf64_header -> bool*)
let header_is_amd64 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_amd64_machine_architecture (Uint32_wrapper.to_bigint h.elf64_machine)
    && is_valid_abi_amd64_magic_number h.elf64_ident)))

let shf_x86_64_large : Nat_big_num.num=  ( Nat_big_num.mul( (Nat_big_num.of_int 256))( (Nat_big_num.of_int 1048576))) (* 0x10000000 a.k.a. 2^28 *)

(* We model the PLT as a list of symbol name, maybe def, and a function
 * - from the PLT slot offset and the whole with-addresses image (overkill)
 * - to... what? currently it's the address of the named symbol *)
type 'abifeature plt_entry_content_fn = Nat_big_num.num -> Nat_big_num.num -> (Nat_big_num.num * char list)
                                     (* PLT base addr, GOT base addr (the rest is closure-captured) -> slot_addr, slot contents *)

type 'abifeature amd64_abi_feature = 
    GOT0 of  ( (string * ( symbol_definition option))list)
    | PLT0 of ( (string * ( symbol_definition option) * 'abifeature plt_entry_content_fn)list)
    
(*val abiFeatureCompare : forall 'abifeature. amd64_abi_feature 'abifeature -> amd64_abi_feature 'abifeature -> Basic_classes.ordering*)
let abiFeatureCompare0 f1 f2:int= 
     ((match (f1, f2) with
        (GOT0(_), GOT0(_)) -> 0
        | (GOT0(_), PLT0(_)) -> (-1)
        | (PLT0(_), PLT0(_)) -> 0
        | (PLT0(_), GOT0(_)) -> 1
    ))

(*val abiFeatureTagEq : forall 'abifeature. amd64_abi_feature 'abifeature -> amd64_abi_feature 'abifeature -> bool*)
let abiFeatureTagEq0 f1 f2:bool=
     ((match (f1, f2) with
        (GOT0(_), GOT0(_)) -> true
        | (PLT0(_), PLT0(_)) -> true
        | (_, _) -> false
    ))

let instance_Abi_classes_AbiFeatureTagEquiv_Abi_amd64_amd64_abi_feature_dict:('abifeature amd64_abi_feature)abiFeatureTagEquiv_class= ({

  abiFeatureTagEquiv_method = abiFeatureTagEq0})

let instance_Basic_classes_Ord_Abi_amd64_amd64_abi_feature_dict:('abifeature amd64_abi_feature)ord_class= ({

  compare_method = abiFeatureCompare0;

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

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

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

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

(*val section_is_special : forall 'abifeature. elf64_interpreted_section -> annotated_memory_image 'abifeature -> bool*)
let section_is_special1 s img2:bool= 
     (elf_section_is_special s img2 ||
    (match s.elf64_section_name_as_string with 
        ".eh_frame" -> true (* HACK needed because SHT_X86_64_UNWIND is often not used *)
       | _ -> false
    ))