diff options
Diffstat (limited to 'src/elf_model/elf_interpreted_segment.lem')
| -rw-r--r-- | src/elf_model/elf_interpreted_segment.lem | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/src/elf_model/elf_interpreted_segment.lem b/src/elf_model/elf_interpreted_segment.lem new file mode 100644 index 00000000..81ee74e2 --- /dev/null +++ b/src/elf_model/elf_interpreted_segment.lem @@ -0,0 +1,77 @@ +open import Basic_classes +open import Bool +open import Num +open import String + +open import Elf_types + +open import Bitstring +open import Missing_pervasives +open import Show + +type elf32_interpreted_segment = + <| elf32_segment_body : bitstring (** Body of the segment *) + ; elf32_segment_type : nat (** Type of the segment *) + ; elf32_segment_size : nat (** Size of the segment in bytes *) + ; elf32_segment_memsz : nat (** Size of the segment in memory in bytes *) + ; elf32_segment_base : nat (** Base address of the segment *) + ; elf32_segment_flags : (bool * bool * bool) (** READ, WRITE, EXECUTE flags. *) + |> + +type elf64_interpreted_segment = + <| elf64_segment_body : bitstring (** Body of the segment *) + ; elf64_segment_type : nat (** Type of the segment *) + ; elf64_segment_size : nat (** Size of the segment in bytes *) + ; elf64_segment_memsz : nat (** Size of the segment in memory in bytes *) + ; elf64_segment_base : nat (** Base address of the segment *) + ; elf64_segment_flags : (bool * bool * bool) (** READ, WRITE, EXECUTE flags. *) + |> + +val elf32_interpret_program_header_flags : elf32_word -> (bool * bool * bool) +let elf32_interpret_program_header_flags flags = + let zero = elf32_word_of_int32 0 in + let one = elf32_word_of_int32 1 in + let two = elf32_word_of_int32 2 in + let four = elf32_word_of_int32 4 in + (not (elf32_word_land flags one = zero), + not (elf32_word_land flags two = zero), + not (elf32_word_land flags four = zero)) + +val elf64_interpret_program_header_flags : elf64_word -> (bool * bool * bool) +let elf64_interpret_program_header_flags flags = + let zero = elf64_word_of_int32 0 in + let one = elf64_word_of_int32 1 in + let two = elf64_word_of_int32 2 in + let four = elf64_word_of_int32 4 in + (not (elf64_word_land flags one = zero), + not (elf64_word_land flags two = zero), + not (elf64_word_land flags four = zero)) + +val string_of_flags : (bool * bool * bool) -> string +let string_of_flags flags = + match flags with + | (read, write, execute) -> + bracket [show read; show write; show execute] + end + +val string_of_elf32_interpreted_segment : elf32_interpreted_segment -> string +let string_of_elf32_interpreted_segment seg = + unlines [ + "Body of length: " ^ show (Bitstring.length seg.elf32_segment_body) + ; "Segment type: " ^ show seg.elf32_segment_type + ; "Segment size: " ^ show seg.elf32_segment_size + ; "Segment memory size: " ^ show seg.elf32_segment_memsz + ; "Segment base address: " ^ show seg.elf32_segment_base + ; "Segment flags: " ^ string_of_flags seg.elf32_segment_flags + ] + +val string_of_elf64_interpreted_segment : elf64_interpreted_segment -> string +let string_of_elf64_interpreted_segment seg = + unlines [ + "Body of length: " ^ show (Bitstring.length seg.elf64_segment_body) + ; "Segment type: " ^ show seg.elf64_segment_type + ; "Segment size: " ^ show seg.elf64_segment_size + ; "Segment memory size: " ^ show seg.elf64_segment_memsz + ; "Segment base address: " ^ show seg.elf64_segment_base + ; "Segment flags: " ^ string_of_flags seg.elf64_segment_flags + ] |