Source file abi_power64.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
(** [abi_power64] contains top-level definition for the PowerPC64 ABI.
*)
open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_num
open Lem_maybe
open Byte_sequence
open Error
open Missing_pervasives
open Elf_header
open Elf_types_native_uint
open Elf_file
open Elf_interpreted_segment
(** [abi_power64_compute_program_entry_point segs entry] computes the program
* entry point using ABI-specific conventions. On Power64 the entry point in
* the ELF header ([entry] here) is a pointer into a program segment that
* contains the "real" entry point. On other ABIs, e.g.
* AArch64 and AMD64, the entry point in the ELF header [entry] is the actual
* program entry point.
*)
let abi_power64_compute_program_entry_point segs entry:(Nat_big_num.num)error=
(let entry = (Ml_bindings.nat_big_num_of_uint64 entry) in
let filtered = (List.filter (
fun seg ->
let base = (seg.elf64_segment_base) in
let size2 = (seg.elf64_segment_memsz) in Nat_big_num.less_equal
base entry && Nat_big_num.less_equal entry ( Nat_big_num.add base size2)
) segs)
in
(match filtered with
| [] -> fail "abi_power64_compute_program_entry_point: no program segment contains the program entry point"
| [x] ->
let rebase = (Nat_big_num.sub_nat entry x.elf64_segment_base) in bind (Byte_sequence.offset_and_cut rebase( (Nat_big_num.of_int 8)) x.elf64_segment_body) (fun bytes -> bind (Byte_sequence.read_8_bytes_le bytes) (fun (bytes, _) ->
let (b1,b2,b3,b4,b5,b6,b7,b8) = bytes in
return (Ml_bindings.nat_big_num_of_uint64 (Uint64_wrapper.of_oct b1 b2 b3 b4 b5 b6 b7 b8))))
| _ -> fail "abi_power64_compute_program_entry_point: multiple program segments contain the program entry point"
))