(*Generated by Lem from adaptors/sail_interface.lem.*)
open Lem_basic_classes
open Lem_function
open Lem_list
open Lem_maybe
open Lem_num
open Lem_string
open Lem_tuple

open Lem_assert_extra

open Byte_sequence
open Error
open Missing_pervasives
open Show

open Elf_header
open Elf_file
open Elf_interpreted_section
open Elf_interpreted_segment
open String_table
open Elf_symbol_table
open Elf_program_header_table
open Elf_types_native_uint

open Hex_printing

type executable_process_image =
  | ELF_Class_32 of elf32_executable_process_image
  | ELF_Class_64 of elf64_executable_process_image

(*val string_of_segment_provenance : segment_provenance -> string*)
let string_of_segment_provenance p:string=  
 ((match p with
    | FromELF -> "Segment from ELF file"
    | AutoGenerated -> "Segment auto generated"
  ))

(*val string_of_executable_process_image : executable_process_image -> string*)
let string_of_executable_process_image img2:string=  
 ((match img2 with
    | ELF_Class_32 (segs, entry_point, machine_type) ->
        let machine_type = (string_of_elf_machine_architecture machine_type) in
        let entry_point  = (unsafe_hex_string_of_natural( 16) entry_point) in
        let segs         = (Lem_list.map (fun (seg, prov) ->
                             let prov = (string_of_segment_provenance prov) in
                             let seg  = (string_of_elf32_interpreted_segment seg) in
                                 "Segment provenance: " ^ (prov ^ ("\n" ^ seg))
                           ) segs)
        in
          unlines ( List.rev_append (List.rev [
            "32-bit ELF executable image"
          ; ("Machine type: " ^ machine_type)
          ; ("Entry point: " ^ entry_point)
          ; ""
          ]) segs)
    | ELF_Class_64 (segs, entry_point, machine_type) ->
        let machine_type = (string_of_elf_machine_architecture machine_type) in
        let entry_point  = (unsafe_hex_string_of_natural( 16) entry_point) in
        let segs         = (intercalate "\n" (Lem_list.map (fun (seg, prov) ->
                             let prov = (string_of_segment_provenance prov) in
                             let seg  = (string_of_elf64_interpreted_segment seg) in
                                 "Segment provenance: " ^ (prov ^ ("\n" ^ seg))
                           ) segs))
        in
          unlines ( List.rev_append (List.rev [
            "64-bit ELF executable image"
          ; ("Machine type: " ^ machine_type)
          ; ("Entry point: " ^ entry_point)
          ; ""
          ]) segs)
  ))

(*val populate : string -> error executable_process_image*)
let populate fname1:(executable_process_image)error=  
( 
  (* Acquire the data from the file... *)Byte_sequence.acquire fname1 >>= (fun bs0 ->
  (* Read the magic number and the flags in the header... *)
  repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) ->
    (match Lem_list.list_index ident( 4) with
      | None -> fail "populate: ELF ident transcription error"
      | Some c  ->
        (* Calculate whether we are dealing with a 32- or 64-bit file based on
         * what we have read...
         *)
        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then
          Elf_file.read_elf32_file bs0 >>= (fun ef5 ->
          if Elf_program_header_table.get_elf32_static_linked ef5.elf32_file_program_header_table then
            Elf_file.get_elf32_executable_image ef5 >>= (fun img2 ->
            return (ELF_Class_32 img2))
          else
            fail "populate: not a statically linked executable")
        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then
          Elf_file.read_elf64_file bs0 >>= (fun ef5 ->
          if Elf_program_header_table.get_elf64_static_linked ef5.elf64_file_program_header_table then
            Elf_file.get_elf64_executable_image ef5 >>= (fun img2 ->
            return (ELF_Class_64 img2))
          else
            fail "populate: not a statically linked executable")
        else
          fail "populate: ELF class unrecognised"
    ))))

(*val populate' : byte_sequence -> error executable_process_image*)
let populate' bs0:(executable_process_image)error=  
( 
  (* Read the magic number and the flags in the header... *)repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) ->
    (match Lem_list.list_index ident( 4) with
      | None -> fail "populate': ELF ident transcription error"
      | Some c  ->
        (* Calculate whether we are dealing with a 32- or 64-bit file based on
         * what we have read...
         *)
        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then
          Elf_file.read_elf32_file bs0 >>= (fun ef5 ->
          if Elf_program_header_table.get_elf32_static_linked ef5.elf32_file_program_header_table then
            Elf_file.get_elf32_executable_image ef5 >>= (fun img2 ->
            return (ELF_Class_32 img2))
          else
            fail "populate': not a statically linked executable")
        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then
          Elf_file.read_elf64_file bs0 >>= (fun ef5 ->
          if Elf_program_header_table.get_elf64_static_linked ef5.elf64_file_program_header_table then
            Elf_file.get_elf64_executable_image ef5 >>= (fun img2 ->
            return (ELF_Class_64 img2))
          else
            fail "populate': not a statically linked executable")
        else
          fail "populate': ELF class unrecognised"
    )))

(*val obtain_global_symbol_init_info : string -> error global_symbol_init_info*)
let obtain_global_symbol_init_info fname1:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence)option*Nat_big_num.num))list)error=  
( 
  (* Acquire the data from the file... *)Byte_sequence.acquire fname1 >>= (fun bs0 ->
  (* Read the magic number and the flags in the header... *)
  repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) ->
    (match Lem_list.list_index ident( 4) with
      | None -> fail "obtain_global_symbol_init_info: ELF ident transcription error"
      | Some c  ->
        (* Calculate whether we are dealing with a 32- or 64-bit file based on
         * what we have read...
         *)
        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then
          Elf_file.read_elf32_file bs0 >>= (fun f1 ->
          if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then
            Elf_file.get_elf32_file_global_symbol_init f1 >>= (fun init1 ->
            return init1)
          else
            fail "obtain_global_symbol_init_info: not a statically linked executable")
        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then
          Elf_file.read_elf64_file bs0 >>= (fun f1 ->
          if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then
            Elf_file.get_elf64_file_global_symbol_init f1 >>= (fun init1 ->
            return init1)
          else
            fail "obtain_global_symbol_init_info: not a statically linked executable")
        else
          fail "obtain_global_symbol_init_info: ELF class unrecognised"
    ))))

(*val obtain_global_symbol_init_info' : byte_sequence -> error global_symbol_init_info*)
let obtain_global_symbol_init_info' bs0:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence)option*Nat_big_num.num))list)error=  
( 
  (* Read the magic number and the flags in the header... *)repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) ->
    (match Lem_list.list_index ident( 4) with
      | None -> fail "obtain_global_symbol_init_info': ELF ident transcription error"
      | Some c  ->
        (* Calculate whether we are dealing with a 32- or 64-bit file based on
         * what we have read...
         *)
        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then
          Elf_file.read_elf32_file bs0 >>= (fun f1 ->
          if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then
            Elf_file.get_elf32_file_global_symbol_init f1 >>= (fun init1 ->
            return init1)
          else
            fail "obtain_global_symbol_init_info': not a statically linked executable")
        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then
          Elf_file.read_elf64_file bs0 >>= (fun f1 ->
          if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then
            Elf_file.get_elf64_file_global_symbol_init f1 >>= (fun init1 ->
            return init1)
          else
            fail "obtain_global_symbol_init_info': not a statically linked executable")
        else
          fail "obtain_global_symbol_init_info': ELF class unrecognised"
    )))

(*val populate_and_obtain_global_symbol_init_info : string -> error (elf_file * executable_process_image * global_symbol_init_info)*)
let populate_and_obtain_global_symbol_init_info fname1:(elf_file*executable_process_image*(string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence)option*Nat_big_num.num))list)error=  
( 
  (* Acquire the data from the file... *)Byte_sequence.acquire fname1 >>= (fun bs0 ->
  (* Read the magic number and the flags in the header... *)
  repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) ->
    (match Lem_list.list_index ident( 4) with
      | None -> fail "populate_and_obtain_global_symbol_init_info: ELF ident transcription error"
      | Some c  ->
        (* Calculate whether we are dealing with a 32- or 64-bit file based on
         * what we have read...
         *)
        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then
          Elf_file.read_elf32_file bs0 >>= (fun f1 ->
          if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then
            Elf_file.get_elf32_file_global_symbol_init f1 >>= (fun init1 ->
            Elf_file.get_elf32_executable_image f1 >>= (fun img2 ->           
            return ((ELF_File_32 f1), (ELF_Class_32 img2), init1)))
          else
            fail "populate_and_obtain_global_symbol_init_info: not a statically linked executable")
        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then
          Elf_file.read_elf64_file bs0 >>= (fun f1 ->
          if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then
            Elf_file.get_elf64_file_global_symbol_init f1 >>= (fun init1 ->
            Elf_file.get_elf64_executable_image f1 >>= (fun img2 ->
            return ((ELF_File_64 f1), (ELF_Class_64 img2), init1)))
          else
            fail "populate_and_obtain_global_symbol_init_info: not a statically linked executable")
        else
          fail "populate_and_obtain_global_symbol_init_info: ELF class unrecognised"
    ))))

(*val populate_and_obtain_global_symbol_init_info' : byte_sequence -> error (elf_file * executable_process_image * global_symbol_init_info)*)
let populate_and_obtain_global_symbol_init_info' bs0:(elf_file*executable_process_image*(string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence)option*Nat_big_num.num))list)error=  
( 
  (* Read the magic number and the flags in the header... *)repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) ->
    (match Lem_list.list_index ident( 4) with
      | None -> fail "populate_and_obtain_global_symbol_init_info': ELF ident transcription error"
      | Some c  ->
        (* Calculate whether we are dealing with a 32- or 64-bit file based on
         * what we have read...
         *)
        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then
          Elf_file.read_elf32_file bs0 >>= (fun f1 ->
          if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then
            Elf_file.get_elf32_file_global_symbol_init f1 >>= (fun init1 ->
            Elf_file.get_elf32_executable_image f1 >>= (fun img2 ->           
            return ((ELF_File_32 f1), (ELF_Class_32 img2), init1)))
          else
            fail "populate_and_obtain_global_symbol_init_info': not a statically linked executable")
        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then
          Elf_file.read_elf64_file bs0 >>= (fun f1 ->
          if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then
            Elf_file.get_elf64_file_global_symbol_init f1 >>= (fun init1 ->
            Elf_file.get_elf64_executable_image f1 >>= (fun img2 ->
            return ((ELF_File_64 f1), (ELF_Class_64 img2), init1)))
          else
            fail "populate_and_obtain_global_symbol_init_info': not a statically linked executable")
        else
          fail "populate_and_obtain_global_symbol_init_info': ELF class unrecognised"
    )))