diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/elf_interpreted_segment.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/elf_interpreted_segment.ml | 167 |
1 files changed, 167 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/elf_interpreted_segment.ml b/lib/ocaml_rts/linksem/elf_interpreted_segment.ml new file mode 100644 index 00000000..1971f350 --- /dev/null +++ b/lib/ocaml_rts/linksem/elf_interpreted_segment.ml @@ -0,0 +1,167 @@ +(*Generated by Lem from elf_interpreted_segment.lem.*) +(** [elf_interpreted_segment] defines interpreted segments, i.e. the contents of + * a program header table entry converted to more amenable types, and operations + * built on top of them. + *) + +open Lem_basic_classes +open Lem_bool +open Lem_num +open Lem_string + +open Elf_types_native_uint +open Elf_program_header_table + +open Byte_sequence +open Missing_pervasives +open Show + +open Hex_printing + +(** [elf32_interpreted_segment] represents an ELF32 interpreted segment, i.e. the + * contents of an ELF program header table entry converted into more amenable + * (infinite precision) types, for manipulation. + * Invariant: the nth entry of the program header table corresponds to the nth + * entry of the list of interpreted segments in an [elf32_file] record. The + * lengths of the two lists are exactly the same. + *) +type elf32_interpreted_segment = + { elf32_segment_body : byte_sequence (** Body of the segment *) + ; elf32_segment_type : Nat_big_num.num (** Type of the segment *) + ; elf32_segment_size : Nat_big_num.num (** Size of the segment in bytes *) + ; elf32_segment_memsz : Nat_big_num.num (** Size of the segment in memory in bytes *) + ; elf32_segment_base : Nat_big_num.num (** Base address of the segment *) + ; elf32_segment_paddr : Nat_big_num.num (** Physical address of segment *) + ; elf32_segment_align : Nat_big_num.num (** Alignment of the segment *) + ; elf32_segment_offset : Nat_big_num.num (** Offset of the segment *) + ; elf32_segment_flags : (bool * bool * bool) (** READ, WRITE, EXECUTE flags. *) + } + +(** [elf64_interpreted_segment] represents an ELF64 interpreted segment, i.e. the + * contents of an ELF program header table entry converted into more amenable + * (infinite precision) types, for manipulation. + * Invariant: the nth entry of the program header table corresponds to the nth + * entry of the list of interpreted segments in an [elf64_file] record. The + * lengths of the two lists are exactly the same. + *) +type elf64_interpreted_segment = + { elf64_segment_body : byte_sequence (** Body of the segment *) + ; elf64_segment_type : Nat_big_num.num (** Type of the segment *) + ; elf64_segment_size : Nat_big_num.num (** Size of the segment in bytes *) + ; elf64_segment_memsz : Nat_big_num.num (** Size of the segment in memory in bytes *) + ; elf64_segment_base : Nat_big_num.num (** Base address of the segment *) + ; elf64_segment_paddr : Nat_big_num.num (** Physical address of segment *) + ; elf64_segment_align : Nat_big_num.num (** Alignment of the segment *) + ; elf64_segment_offset : Nat_big_num.num (** Offset of the segment *) + ; elf64_segment_flags : (bool * bool * bool) (** READ, WRITE, EXECUTE flags. *) + } + +(** [compare_elf64_interpreted_segment seg1 seg2] is an ordering comparison function + * on interpreted segments suitable for constructing sets, finite maps and other + * ordered data types out of. + *) +(*val compare_elf64_interpreted_segment : elf64_interpreted_segment -> + elf64_interpreted_segment -> ordering*) +let compare_elf64_interpreted_segment s1 s2:int= + (tripleCompare compare_byte_sequence (Lem_list.lexicographic_compare Nat_big_num.compare) (Lem_list.lexicographic_compare Nat_big_num.compare) + (s1.elf64_segment_body, + [s1.elf64_segment_type ; + s1.elf64_segment_size ; + s1.elf64_segment_memsz ; + s1.elf64_segment_base ; + s1.elf64_segment_paddr ; + s1.elf64_segment_align ; + s1.elf64_segment_offset], + (let (f1, f2, f3) = (s1.elf64_segment_flags) in + Lem_list.map natural_of_bool [f1; f2; f3])) + (s2.elf64_segment_body, + [s2.elf64_segment_type ; + s2.elf64_segment_size ; + s2.elf64_segment_memsz ; + s2.elf64_segment_base ; + s2.elf64_segment_paddr ; + s2.elf64_segment_align ; + s2.elf64_segment_offset], +(let (f1, f2, f3) = (s2.elf64_segment_flags) in + Lem_list.map natural_of_bool [f1; f2; f3]))) + +let instance_Basic_classes_Ord_Elf_interpreted_segment_elf64_interpreted_segment_dict:(elf64_interpreted_segment)ord_class= ({ + + compare_method = compare_elf64_interpreted_segment; + + isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_interpreted_segment f1 f2) (-1)))); + + isLessEqual_method = (fun f1 -> (fun f2 -> let result = (compare_elf64_interpreted_segment f1 f2) in Lem.orderingEqual result (-1) || Lem.orderingEqual result 0)); + + isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_interpreted_segment f1 f2) 1))); + + isGreaterEqual_method = (fun f1 -> (fun f2 -> let result = (compare_elf64_interpreted_segment f1 f2) in Lem.orderingEqual result 1 || Lem.orderingEqual result 0))}) + +type elf32_interpreted_segments = elf32_interpreted_segment list +type elf64_interpreted_segments = elf64_interpreted_segment list + +(** [elf32_interpreted_program_header_flags w] extracts a boolean triple of flags + * from the flags field of an interpreted segment. + *) +(*val elf32_interpret_program_header_flags : elf32_word -> (bool * bool * bool)*) +let elf32_interpret_program_header_flags flags:bool*bool*bool= + (let zero = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) in + let one = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 1))) in + let two = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 2))) in + let four = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 4))) in + (not (Uint32.logand flags one = zero), + not (Uint32.logand flags two = zero), + not (Uint32.logand flags four = zero))) + +(** [elf64_interpreted_program_header_flags w] extracts a boolean triple of flags + * from the flags field of an interpreted segment. + *) +(*val elf64_interpret_program_header_flags : elf64_word -> (bool * bool * bool)*) +let elf64_interpret_program_header_flags flags:bool*bool*bool= + (let zero = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) in + let one = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 1))) in + let two = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 2))) in + let four = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 4))) in + (not (Uint32.logand flags one = zero), + not (Uint32.logand flags two = zero), + not (Uint32.logand flags four = zero))) + +(** [string_of_flags bs] produces a string-based representation of an interpreted + * segments flags (represented as a boolean triple). + *) +(*val string_of_flags : (bool * bool * bool) -> string*) +let string_of_flags flags:string= + ((match flags with + | (read, write, execute) -> + bracket [string_of_bool read; string_of_bool write; string_of_bool execute] + )) + +(** [string_of_elf32_interpreted_segment seg] produces a string-based representation + * of interpreted segment [seg]. + *) +(*val string_of_elf32_interpreted_segment : elf32_interpreted_segment -> string*) +let string_of_elf32_interpreted_segment seg:string= + (unlines [ +("Body of length: " ^ unsafe_hex_string_of_natural( 16) (Byte_sequence.length0 seg.elf32_segment_body)) + ; ("Segment type: " ^ string_of_segment_type (fun _ -> "ABI specific") (fun _ -> "ABI specific") seg.elf32_segment_type) + ; ("Segment size: " ^ unsafe_hex_string_of_natural( 16) seg.elf32_segment_size) + ; ("Segment memory size: " ^ unsafe_hex_string_of_natural( 16) seg.elf32_segment_memsz) + ; ("Segment base address: " ^ unsafe_hex_string_of_natural( 16) seg.elf32_segment_base) + ; ("Segment physical address: " ^ unsafe_hex_string_of_natural( 16) seg.elf32_segment_paddr) + ; ("Segment flags: " ^ string_of_flags seg.elf32_segment_flags) + ]) + +(** [string_of_elf64_interpreted_segment seg] produces a string-based representation + * of interpreted segment [seg]. + *) +(*val string_of_elf64_interpreted_segment : elf64_interpreted_segment -> string*) +let string_of_elf64_interpreted_segment seg:string= + (unlines [ +("Body of length: " ^ unsafe_hex_string_of_natural( 16) (Byte_sequence.length0 seg.elf64_segment_body)) + ; ("Segment type: " ^ string_of_segment_type (fun _ -> "ABI specific") (fun _ -> "ABI specific") seg.elf64_segment_type) + ; ("Segment size: " ^ unsafe_hex_string_of_natural( 16) seg.elf64_segment_size) + ; ("Segment memory size: " ^ unsafe_hex_string_of_natural( 16) seg.elf64_segment_memsz) + ; ("Segment base address: " ^ unsafe_hex_string_of_natural( 16) seg.elf64_segment_base) + ; ("Segment physical address: " ^ unsafe_hex_string_of_natural( 16) seg.elf64_segment_paddr) + ; ("Segment flags: " ^ string_of_flags seg.elf64_segment_flags) + ]) |