Source file `abi_riscv.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
(*Generated by Lem from abis/riscv/abi_riscv.lem.*)
(** [abi_riscv] contains top-level definition for the RISCV 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 import Abi_riscv_relocation*)
open Abi_riscv_elf_header

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

(*val header_is_riscv : elf64_header -> bool*)
let header_is_riscv 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_2msb)))
    && (is_valid_abi_riscv_machine_architecture (Uint32_wrapper.to_bigint h.elf64_machine)
    && is_valid_abi_riscv_magic_number h.elf64_ident)))

type 'abifeature plt_entry_address_fn0 = Nat_big_num.num (* offset in PLT? *) -> 'abifeature annotated_memory_image (* img *) -> Nat_big_num.num (* addr *)

type 'abifeature riscv_abi_feature = 
    GOT2 of  ( (string * ( symbol_definition option))list)
    | PLT2 of ( (string * ( symbol_definition option) * 'abifeature plt_entry_address_fn0)list)
    
(*val abiFeatureCompare : forall 'abifeature. riscv_abi_feature 'abifeature -> riscv_abi_feature 'abifeature -> Basic_classes.ordering*)
let abiFeatureCompare2 f1 f2:int= 
     ((match (f1, f2) with
        (GOT2(_), GOT2(_)) -> 0
        | (GOT2(_), PLT2(_)) -> (-1)
        | (PLT2(_), PLT2(_)) -> 0
        | (PLT2(_), GOT2(_)) -> 1
    ))

(*val abiFeatureTagEq : forall 'abifeature. riscv_abi_feature 'abifeature -> riscv_abi_feature 'abifeature -> bool*)
let abiFeatureTagEq2 f1 f2:bool=
     ((match (f1, f2) with
        (GOT2(_), GOT2(_)) -> true
        | (PLT2(_), PLT2(_)) -> true
        | (_, _) -> false
    ))

let instance_Abi_classes_AbiFeatureTagEquiv_Abi_riscv_riscv_abi_feature_dict:('abifeature riscv_abi_feature)abiFeatureTagEquiv_class= ({

  abiFeatureTagEquiv_method = abiFeatureTagEq2})

let instance_Basic_classes_Ord_Abi_riscv_riscv_abi_feature_dict:('abifeature riscv_abi_feature)ord_class= ({

  compare_method = abiFeatureCompare2;

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

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

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

  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (abiFeatureCompare2 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_special3 s img2:bool= 
     (elf_section_is_special s img2)