Source file abi_power64.ml

(*Generated by Lem from abis/power64/abi_power64.lem.*)
(** [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.
  *)
(*val abi_power64_compute_program_entry_point : list elf64_interpreted_segment -> elf64_addr -> error natural*)
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"
    ))