package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/src/linksem_zarith/elf_section_header_table.ml.html
Source file elf_section_header_table.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 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135
(*Generated by Lem from elf_section_header_table.lem.*) (** [elf_section_header_table] provides types, functions and other definitions * for working with section header tables and their entries. *) open Lem_basic_classes open Lem_bool open Lem_function open Lem_list open Lem_map open Lem_maybe open Lem_num open Lem_string open Byte_sequence open Error open Missing_pervasives open Show open Endianness open String_table open Elf_header open Elf_types_native_uint open Elf_program_header_table (** Special section indices. *) (** See elf_header.lem for shn_undef *) (** [shn_loreserve]: this specifies the lower bound of the range of reserved * indices. *) let shn_loreserve : Nat_big_num.num= ( (Nat_big_num.of_int 65280)) (* 0xff00 *) (** [shn_loproc]: start of the range reserved for processor-specific semantics. *) let shn_loproc : Nat_big_num.num= ( (Nat_big_num.of_int 65280)) (* 0xff00 *) (** [shn_hiproc]: end of the range reserved for processor-specific semantics. *) let shn_hiproc : Nat_big_num.num= ( (Nat_big_num.of_int 65311)) (* 0xff1f *) (** [shn_loos]: start of the range reserved for operating system-specific * semantics. *) let shn_loos : Nat_big_num.num= ( (Nat_big_num.of_int 65312)) (* 0xff20 *) (** [shn_hios]: end of the range reserved for operating system-specific * semantics. *) let shn_hios : Nat_big_num.num= ( (Nat_big_num.of_int 65343)) (* 0xff3f *) (** [shn_abs]: specifies the absolute values for the corresponding reference. * Symbols defined relative to section number [shn_abs] have absolute values * and are not affected by relocation. *) let shn_abs : Nat_big_num.num= ( (Nat_big_num.of_int 65521)) (* 0xfff1 *) (** [shn_common]: symbols defined relative to this index are common symbols, * such as unallocated C external variables. *) let shn_common : Nat_big_num.num= ( (Nat_big_num.of_int 65522)) (* 0xfff2 *) (** See elf_header.lem for shn_xindex. *) (** [shn_hireserve]: specifies the upper-bound of reserved values. *) let shn_hireserve : Nat_big_num.num= ( (Nat_big_num.of_int 65535)) (* 0xffff *) (** [string_of_special_section_index m] produces a string-based representation * of a section header entry's special section index, [m]. *) (*val string_of_special_section_index : natural -> string*) let string_of_special_section_index i:string= (if Nat_big_num.equal i shn_undef then "SHN_UNDEF" else if Nat_big_num.equal i shn_loreserve then "SHN_LORESERVE" else if Nat_big_num.greater_equal i shn_loproc && Nat_big_num.less_equal i shn_hiproc then "SHN_PROCESSOR_SPECIFIC" else if Nat_big_num.greater_equal i shn_loos && Nat_big_num.less_equal i shn_hios then "SHN_OS_SPECIFIC" else if Nat_big_num.equal i shn_abs then "SHN_ABS" else if Nat_big_num.equal i shn_common then "SHN_COMMON" else if Nat_big_num.equal i shn_xindex then "SHN_XINDEX" else if Nat_big_num.equal i shn_hireserve then "SHN_HIRESERVE" else "SHN UNDEFINED") (** Section types. *) (** Marks the section header as being inactive. *) let sht_null : Nat_big_num.num= ( (Nat_big_num.of_int 0)) (** Section holds information defined by the program. *) let sht_progbits : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** The following two section types hold a symbol table. An object file may only * have one symbol table of each of the respective types. The symtab provides * a place for link editing, whereas the dynsym section holds a minimal set of * dynamic linking symbols *) let sht_symtab : Nat_big_num.num= ( (Nat_big_num.of_int 2)) let sht_dynsym : Nat_big_num.num= ( (Nat_big_num.of_int 11)) (** Section holds a string table *) let sht_strtab : Nat_big_num.num= ( (Nat_big_num.of_int 3)) (** Section holds relocation entries with explicit addends. An object file may * have multiple section of this type. *) let sht_rela : Nat_big_num.num= ( (Nat_big_num.of_int 4)) (** Section holds a symbol hash table. An object file may only have a single * hash table. *) let sht_hash : Nat_big_num.num= ( (Nat_big_num.of_int 5)) (** Section holds information for dynamic linking. An object file may only have * a single dynamic section. *) let sht_dynamic : Nat_big_num.num= ( (Nat_big_num.of_int 6)) (** Section holds information that marks the file in some way. *) let sht_note : Nat_big_num.num= ( (Nat_big_num.of_int 7)) (** Section occupies no space in the file but otherwise resembles a progbits * section. *) let sht_nobits : Nat_big_num.num= ( (Nat_big_num.of_int 8)) (** Section holds relocation entries without explicit addends. An object file * may have multiple section of this type. *) let sht_rel : Nat_big_num.num= ( (Nat_big_num.of_int 9)) (** Section type is reserved but has an unspecified meaning. *) let sht_shlib : Nat_big_num.num= ( (Nat_big_num.of_int 10)) (** Section contains an array of pointers to initialisation functions. Each * pointer is taken as a parameterless function with a void return type. *) let sht_init_array : Nat_big_num.num= ( (Nat_big_num.of_int 14)) (** Section contains an array of pointers to termination functions. Each * pointer is taken as a parameterless function with a void return type. *) let sht_fini_array : Nat_big_num.num= ( (Nat_big_num.of_int 15)) (** Section contains an array of pointers to initialisation functions that are * invoked before all other initialisation functions. Each * pointer is taken as a parameterless function with a void return type. *) let sht_preinit_array : Nat_big_num.num= ( (Nat_big_num.of_int 16)) (** Section defines a section group, i.e. a set of sections that are related and * must be treated especially by the linker. May only appear in relocatable * objects. *) let sht_group : Nat_big_num.num= ( (Nat_big_num.of_int 17)) (** Section is associated with sections of type SHT_SYMTAB and is required if * any of the section header indices referenced by that symbol table contains * the escape value SHN_XINDEX. * * FIXME: Lem bug as [int] type used throughout Lem codebase, rather than * [BigInt.t], so Lem chokes on these large constants below, hence the weird * way in which they are written. *) let sht_symtab_shndx : Nat_big_num.num= ( (Nat_big_num.of_int 18)) (** The following ranges are reserved solely for OS-, processor- and user- * specific semantics, respectively. *) let sht_loos : Nat_big_num.num= (Nat_big_num.mul (Nat_big_num.mul (Nat_big_num.mul( (Nat_big_num.of_int 3))( (Nat_big_num.of_int 1024)))( (Nat_big_num.of_int 1024)))( (Nat_big_num.of_int 512))) (* 1610612736 (* 0x60000000 *) *) let sht_hios : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 469762047))( (Nat_big_num.of_int 4)))( (Nat_big_num.of_int 3))) (* 1879048191 (* 0x6fffffff *) *) let sht_loproc : Nat_big_num.num= ( Nat_big_num.mul( (Nat_big_num.of_int 469762048))( (Nat_big_num.of_int 4))) (* 1879048192 (* 0x70000000 *) *) let sht_hiproc : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 536870911))( (Nat_big_num.of_int 4)))( (Nat_big_num.of_int 3))) (* 2147483647 (* 0x7fffffff *) *) let sht_louser : Nat_big_num.num= ( Nat_big_num.mul( (Nat_big_num.of_int 536870912))( (Nat_big_num.of_int 4))) (* 2147483648 (* 0x80000000 *) *) let sht_hiuser : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 603979775))( (Nat_big_num.of_int 4)))( (Nat_big_num.of_int 3))) (* 2415919103 (* 0x8fffffff *) *) (** [string_of_section_type os proc user i] produces a string-based representation * of section type [i]. Some section types are defined by ABI-specific supplements * in reserved ranges, in which case the functions [os], [proc] and [user] are * used to produce the string. *) (*val string_of_section_type : (natural -> string) -> (natural -> string) -> (natural -> string) -> natural -> string*) let string_of_section_type os proc user i:string= (if Nat_big_num.equal i sht_null then "NULL" else if Nat_big_num.equal i sht_progbits then "PROGBITS" else if Nat_big_num.equal i sht_symtab then "SYMTAB" else if Nat_big_num.equal i sht_strtab then "STRTAB" else if Nat_big_num.equal i sht_rela then "RELA" else if Nat_big_num.equal i sht_hash then "HASH" else if Nat_big_num.equal i sht_dynamic then "DYNAMIC" else if Nat_big_num.equal i sht_note then "NOTE" else if Nat_big_num.equal i sht_nobits then "NOBITS" else if Nat_big_num.equal i sht_rel then "REL" else if Nat_big_num.equal i sht_shlib then "SHLIB" else if Nat_big_num.equal i sht_dynsym then "DYNSYM" else if Nat_big_num.equal i sht_init_array then "INIT_ARRAY" else if Nat_big_num.equal i sht_fini_array then "FINI_ARRAY" else if Nat_big_num.equal i sht_preinit_array then "PREINIT_ARRAY" else if Nat_big_num.equal i sht_group then "GROUP" else if Nat_big_num.equal i sht_symtab_shndx then "SYMTAB_SHNDX" else if Nat_big_num.greater_equal i sht_loos && Nat_big_num.less_equal i sht_hios then os i else if Nat_big_num.greater_equal i sht_loproc && Nat_big_num.less_equal i sht_hiproc then proc i else if Nat_big_num.greater_equal i sht_louser && Nat_big_num.less_equal i sht_hiuser then user i else "Undefined or invalid section type") (** Section flag numeric values. *) (** The section contains data that should be writable during program execution. *) let shf_write : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** The section occupies memory during program execution. *) let shf_alloc : Nat_big_num.num= ( (Nat_big_num.of_int 2)) (** The section contains executable instructions. *) let shf_execinstr : Nat_big_num.num= ( (Nat_big_num.of_int 4)) (** The data in the section may be merged to reduce duplication. Each section * is compared based on name, type and flags set with sections with identical * values at run time being mergeable. *) let shf_merge : Nat_big_num.num= ( (Nat_big_num.of_int 16)) (** The section contains null-terminated character strings. *) let shf_strings : Nat_big_num.num= ( (Nat_big_num.of_int 32)) (** The [info] field of this section header contains a section header table * index. *) let shf_info_link : Nat_big_num.num= ( (Nat_big_num.of_int 64)) (** Adds special link ordering for link editors. *) let shf_link_order : Nat_big_num.num= ( (Nat_big_num.of_int 128)) (** This section requires special OS-specific processing beyond the standard * link rules. *) let shf_os_nonconforming : Nat_big_num.num= ( (Nat_big_num.of_int 256)) (** This section is a member (potentially the only member) of a link group. *) let shf_group : Nat_big_num.num= ( (Nat_big_num.of_int 512)) (** This section contains Thread Local Storage (TLS) meaning that each thread of * execution has its own instance of this data. *) let shf_tls : Nat_big_num.num= ( (Nat_big_num.of_int 1024)) (** This section contains compressed data. Compressed data may not be marked as * allocatable. *) let shf_compressed : Nat_big_num.num= ( (Nat_big_num.of_int 2048)) (** All bits included in these masks are reserved for OS and processor specific * semantics respectively. *) let shf_mask_os : Nat_big_num.num= ( (Nat_big_num.of_int 267386880)) (* 0x0ff00000 *) let shf_mask_proc : Nat_big_num.num= (Nat_big_num.mul( (Nat_big_num.of_int 4))( (Nat_big_num.of_int 1006632960))) (* 0xf0000000 *) (** [string_of_section_flags os proc f] produces a string based representation * of section flag [f]. Some section flags are defined by the ABI and are in * reserved ranges, in which case the flag string is produced by functions * [os] and [proc]. * TODO: add more as validation tests require them. *) (*val string_of_section_flags : (natural -> string) -> (natural -> string) -> natural -> string*) let string_of_section_flags os proc f:string= (if Nat_big_num.equal f shf_write then "W" else if Nat_big_num.equal f shf_alloc then " A" else if Nat_big_num.equal f shf_execinstr then " X" else if Nat_big_num.equal f (Nat_big_num.add shf_alloc shf_execinstr) then " AX" else if Nat_big_num.equal f (Nat_big_num.add shf_write shf_alloc) then " WA" else if Nat_big_num.equal f shf_merge then " M " else if Nat_big_num.equal f (Nat_big_num.add shf_merge shf_alloc) then " AM" else if Nat_big_num.equal f (Nat_big_num.add (Nat_big_num.add shf_merge shf_alloc) shf_strings) then "AMS" else if Nat_big_num.equal f (Nat_big_num.add (Nat_big_num.add shf_alloc shf_execinstr) shf_group) then "AXG" else if Nat_big_num.equal f shf_strings then " S" else if Nat_big_num.equal f (Nat_big_num.add shf_merge shf_strings) then " MS" else if Nat_big_num.equal f shf_tls then " T" else if Nat_big_num.equal f (Nat_big_num.add shf_tls shf_alloc) then " AT" else if Nat_big_num.equal f (Nat_big_num.add (Nat_big_num.add shf_write shf_alloc) shf_tls) then "WAT" else if Nat_big_num.equal f shf_info_link then " I" else if Nat_big_num.equal f (Nat_big_num.add shf_alloc shf_info_link) then " AI" else " ") (** Section compression. *) (** Type [elf32_compression_header] provides information about the compression and * decompression of compressed sections. All compressed sections on ELF32 begin * with an [elf32_compression_header] entry. *) type elf32_compression_header = { elf32_chdr_type : Uint32_wrapper.uint32 (** Specifies the compression algorithm *) ; elf32_chdr_size : Uint32_wrapper.uint32 (** Size in bytes of the uncompressed data *) ; elf32_chdr_addralign : Uint32_wrapper.uint32 (** Specifies the required alignment of the uncompressed data *) } (** Type [elf64_compression_header] provides information about the compression and * decompression of compressed sections. All compressed sections on ELF64 begin * with an [elf64_compression_header] entry. *) type elf64_compression_header = { elf64_chdr_type : Uint32_wrapper.uint32 (** Specified the compression algorithm *) ; elf64_chdr_reserved : Uint32_wrapper.uint32 (** Reserved. *) ; elf64_chdr_size : Uint64_wrapper.uint64 (** Size in bytes of the uncompressed data *) ; elf64_chdr_addralign : Uint64_wrapper.uint64 (** Specifies the required alignment of the uncompressed data *) } (** This section is compressed with the ZLIB algorithm. The compressed data begins * at the first byte immediately following the end of the compression header. *) let elfcompress_zlib : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** Values in these ranges are reserved for OS-specific semantics. *) let elfcompress_loos : Nat_big_num.num= (Nat_big_num.mul( (Nat_big_num.of_int 4))( (Nat_big_num.of_int 402653184))) (* 0x60000000 *) let elfcompress_hios : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939524095)))( (Nat_big_num.of_int 1))) (* 0x6fffffff *) (** Values in these ranges are reserved for processor-specific semantics. *) let elfcompress_loproc : Nat_big_num.num= (Nat_big_num.mul( (Nat_big_num.of_int 4))( (Nat_big_num.of_int 469762048))) (* 0x70000000 *) let elfcompress_hiproc : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 1073741823)))( (Nat_big_num.of_int 1))) (* 0x7fffffff *) (** [read_elf32_compression_header ed bs0] reads an [elf32_compression_header] * entry from byte sequence [bs0], interpreting [bs0] with endianness [ed]. * Also returns the suffix of [bs0] after reading in the compression header. * Fails if the header cannot be read. *) (*val read_elf32_compression_header : endianness -> byte_sequence -> error (elf32_compression_header * byte_sequence)*) let read_elf32_compression_header ed bs0:(elf32_compression_header*Byte_sequence_wrapper.byte_sequence)error= (bind (read_elf32_word ed bs0) (fun (typ, bs1) -> bind (read_elf32_word ed bs1) (fun (siz, bs2) -> bind (read_elf32_word ed bs2) (fun (ali, bs3) -> return ({ elf32_chdr_type = typ; elf32_chdr_size = siz; elf32_chdr_addralign = ali }, bs3))))) (** [read_elf64_compression_header ed bs0] reads an [elf64_compression_header] * entry from byte sequence [bs0], interpreting [bs0] with endianness [ed]. * Also returns the suffix of [bs0] after reading in the compression header. * Fails if the header cannot be read. *) (*val read_elf64_compression_header : endianness -> byte_sequence -> error (elf64_compression_header * byte_sequence)*) let read_elf64_compression_header ed bs0:(elf64_compression_header*Byte_sequence_wrapper.byte_sequence)error= (bind (read_elf64_word ed bs0) (fun (typ, bs1) -> bind (read_elf64_word ed bs1) (fun (res, bs2) -> bind (read_elf64_xword ed bs2) (fun (siz, bs3) -> bind (read_elf64_xword ed bs3) (fun (ali, bs4) -> return ({ elf64_chdr_type = typ; elf64_chdr_reserved = res; elf64_chdr_size = siz; elf64_chdr_addralign = ali }, bs4)))))) (** Section header table entry type. *) (** [elf32_section_header_table_entry] is the type of entries in the section * header table in 32-bit ELF files. Each entry in the table details a section * in the body of the ELF file. *) type elf32_section_header_table_entry = { elf32_sh_name : Uint32_wrapper.uint32 (** Name of the section *) ; elf32_sh_type : Uint32_wrapper.uint32 (** Type of the section and its semantics *) ; elf32_sh_flags : Uint32_wrapper.uint32 (** Flags associated with the section *) ; elf32_sh_addr : Uint32_wrapper.uint32 (** Address of first byte of section in memory image *) ; elf32_sh_offset : Uint32_wrapper.uint32 (** Offset from beginning of file of first byte of section *) ; elf32_sh_size : Uint32_wrapper.uint32 (** Section size in bytes *) ; elf32_sh_link : Uint32_wrapper.uint32 (** Section header table index link *) ; elf32_sh_info : Uint32_wrapper.uint32 (** Extra information, contents depends on type of section *) ; elf32_sh_addralign : Uint32_wrapper.uint32 (** Alignment constraints for section *) ; elf32_sh_entsize : Uint32_wrapper.uint32 (** Size of each entry in table, if section is one *) } let elf32_null_section_header:elf32_section_header_table_entry= ({ elf32_sh_name = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf32_sh_type = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf32_sh_flags = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf32_sh_addr = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf32_sh_offset = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf32_sh_size = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf32_sh_link = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf32_sh_info = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf32_sh_addralign = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf32_sh_entsize = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) }) (** [compare_elf32_section_header_table_entry ent1 ent2] is an ordering comparison * function on section header table entries suitable for use in constructing * sets, finite maps and other ordered data types. *) (*val compare_elf32_section_header_table_entry : elf32_section_header_table_entry -> elf32_section_header_table_entry -> ordering*) let compare_elf32_section_header_table_entry h1 h2:int= (lexicographic_compare Nat_big_num.compare [Uint32_wrapper.to_bigint h1.elf32_sh_name; Uint32_wrapper.to_bigint h1.elf32_sh_type; Uint32_wrapper.to_bigint h1.elf32_sh_flags; Uint32_wrapper.to_bigint h1.elf32_sh_addr; Uint32_wrapper.to_bigint h1.elf32_sh_offset; Uint32_wrapper.to_bigint h1.elf32_sh_size; Uint32_wrapper.to_bigint h1.elf32_sh_link; Uint32_wrapper.to_bigint h1.elf32_sh_info; Uint32_wrapper.to_bigint h1.elf32_sh_addralign; Uint32_wrapper.to_bigint h1.elf32_sh_entsize] [Uint32_wrapper.to_bigint h2.elf32_sh_name; Uint32_wrapper.to_bigint h2.elf32_sh_type; Uint32_wrapper.to_bigint h2.elf32_sh_flags; Uint32_wrapper.to_bigint h2.elf32_sh_addr; Uint32_wrapper.to_bigint h2.elf32_sh_offset; Uint32_wrapper.to_bigint h2.elf32_sh_size; Uint32_wrapper.to_bigint h2.elf32_sh_link; Uint32_wrapper.to_bigint h2.elf32_sh_info; Uint32_wrapper.to_bigint h2.elf32_sh_addralign; Uint32_wrapper.to_bigint h2.elf32_sh_entsize]) let instance_Basic_classes_Ord_Elf_section_header_table_elf32_section_header_table_entry_dict:(elf32_section_header_table_entry)ord_class= ({ compare_method = compare_elf32_section_header_table_entry; isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf32_section_header_table_entry f1 f2) (-1)))); isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf32_section_header_table_entry f1 f2)(Pset.from_list compare [(-1); 0]))); isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf32_section_header_table_entry f1 f2) 1))); isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf32_section_header_table_entry f1 f2)(Pset.from_list compare [1; 0])))}) (** [elf64_section_header_table_entry] is the type of entries in the section * header table in 64-bit ELF files. Each entry in the table details a section * in the body of the ELF file. *) type elf64_section_header_table_entry = { elf64_sh_name : Uint32_wrapper.uint32 (** Name of the section *) ; elf64_sh_type : Uint32_wrapper.uint32 (** Type of the section and its semantics *) ; elf64_sh_flags : Uint64_wrapper.uint64 (** Flags associated with the section *) ; elf64_sh_addr : Uint64_wrapper.uint64 (** Address of first byte of section in memory image *) ; elf64_sh_offset : Uint64_wrapper.uint64 (** Offset from beginning of file of first byte of section *) ; elf64_sh_size : Uint64_wrapper.uint64 (** Section size in bytes *) ; elf64_sh_link : Uint32_wrapper.uint32 (** Section header table index link *) ; elf64_sh_info : Uint32_wrapper.uint32 (** Extra information, contents depends on type of section *) ; elf64_sh_addralign : Uint64_wrapper.uint64 (** Alignment constraints for section *) ; elf64_sh_entsize : Uint64_wrapper.uint64 (** Size of each entry in table, if section is one *) } let elf64_null_section_header:elf64_section_header_table_entry= ({ elf64_sh_name = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf64_sh_type = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf64_sh_flags = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf64_sh_addr = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf64_sh_offset = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf64_sh_size = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf64_sh_link = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf64_sh_info = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf64_sh_addralign = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf64_sh_entsize = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))) }) (** [compare_elf64_section_header_table_entry ent1 ent2] is an ordering comparison * function on section header table entries suitable for use in constructing * sets, finite maps and other ordered data types. *) (*val compare_elf64_section_header_table_entry : elf64_section_header_table_entry -> elf64_section_header_table_entry -> ordering*) let compare_elf64_section_header_table_entry h1 h2:int= (lexicographic_compare Nat_big_num.compare [Uint32_wrapper.to_bigint h1.elf64_sh_name; Uint32_wrapper.to_bigint h1.elf64_sh_type; Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_flags; Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_addr; Uint64_wrapper.to_bigint h1.elf64_sh_offset; Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_size; Uint32_wrapper.to_bigint h1.elf64_sh_link; Uint32_wrapper.to_bigint h1.elf64_sh_info; Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_addralign; Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_entsize] [Uint32_wrapper.to_bigint h2.elf64_sh_name; Uint32_wrapper.to_bigint h2.elf64_sh_type; Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_flags; Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_addr; Uint64_wrapper.to_bigint h2.elf64_sh_offset; Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_size; Uint32_wrapper.to_bigint h2.elf64_sh_link; Uint32_wrapper.to_bigint h2.elf64_sh_info; Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_addralign; Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_entsize]) let instance_Basic_classes_Ord_Elf_section_header_table_elf64_section_header_table_entry_dict:(elf64_section_header_table_entry)ord_class= ({ compare_method = compare_elf64_section_header_table_entry; isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_section_header_table_entry f1 f2) (-1)))); isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_section_header_table_entry f1 f2)(Pset.from_list compare [(-1); 0]))); isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_section_header_table_entry f1 f2) 1))); isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_section_header_table_entry f1 f2)(Pset.from_list compare [1; 0])))}) (** Section header table type *) (** Type [elf32_section_header_table] represents a section header table for 32-bit * ELF files. A section header table is an array (implemented as a list, here) * of section header table entries. *) type elf32_section_header_table = elf32_section_header_table_entry list (** Type [elf64_section_header_table] represents a section header table for 64-bit * ELF files. A section header table is an array (implemented as a list, here) * of section header table entries. *) type elf64_section_header_table = elf64_section_header_table_entry list (** Parsing and blitting *) (** [bytes_of_elf32_section_header_table_entry ed ent] blits [ent] to a byte sequence * assuming endianness [ed]. *) (*val bytes_of_elf32_section_header_table_entry : endianness -> elf32_section_header_table_entry -> byte_sequence*) let bytes_of_elf32_section_header_table_entry endian entry:Byte_sequence_wrapper.byte_sequence= (Byte_sequence.from_byte_lists [ bytes_of_elf32_word endian entry.elf32_sh_name ; bytes_of_elf32_word endian entry.elf32_sh_type ; bytes_of_elf32_word endian entry.elf32_sh_flags ; bytes_of_elf32_addr endian entry.elf32_sh_addr ; bytes_of_elf32_off endian entry.elf32_sh_offset ; bytes_of_elf32_word endian entry.elf32_sh_size ; bytes_of_elf32_word endian entry.elf32_sh_link ; bytes_of_elf32_word endian entry.elf32_sh_info ; bytes_of_elf32_word endian entry.elf32_sh_addralign ; bytes_of_elf32_word endian entry.elf32_sh_entsize ]) (** [read_elf32_section_header_table_entry ed bs0] reads a section header table * entry from [bs0] assuming endianness [ed]. Also returns the suffix of [bs0] * after parsing. Fails if the entry cannot be read. *) (*val read_elf32_section_header_table_entry : endianness -> byte_sequence -> error (elf32_section_header_table_entry * byte_sequence)*) let read_elf32_section_header_table_entry endian bs:(elf32_section_header_table_entry*Byte_sequence_wrapper.byte_sequence)error= (bind (read_elf32_word endian bs) (fun (sh_name, bs) -> bind (read_elf32_word endian bs) (fun (sh_type, bs) -> bind (read_elf32_word endian bs) (fun (sh_flags, bs) -> bind (read_elf32_addr endian bs) (fun (sh_addr, bs) -> bind (read_elf32_off endian bs) (fun (sh_offset, bs) -> bind (read_elf32_word endian bs) (fun (sh_size, bs) -> bind (read_elf32_word endian bs) (fun (sh_link, bs) -> bind (read_elf32_word endian bs) (fun (sh_info, bs) -> bind (read_elf32_word endian bs) (fun (sh_addralign, bs) -> bind (read_elf32_word endian bs) (fun (sh_entsize, bs) -> return ({ elf32_sh_name = sh_name; elf32_sh_type = sh_type; elf32_sh_flags = sh_flags; elf32_sh_addr = sh_addr; elf32_sh_offset = sh_offset; elf32_sh_size = sh_size; elf32_sh_link = sh_link; elf32_sh_info = sh_info; elf32_sh_addralign = sh_addralign; elf32_sh_entsize = sh_entsize }, bs)))))))))))) (** [bytes_of_elf64_section_header_table_entry ed ent] blits [ent] to a byte sequence * assuming endianness [ed]. *) (*val bytes_of_elf64_section_header_table_entry : endianness -> elf64_section_header_table_entry -> byte_sequence*) let bytes_of_elf64_section_header_table_entry endian entry:Byte_sequence_wrapper.byte_sequence= (Byte_sequence.from_byte_lists [ bytes_of_elf64_word endian entry.elf64_sh_name ; bytes_of_elf64_word endian entry.elf64_sh_type ; bytes_of_elf64_xword endian entry.elf64_sh_flags ; bytes_of_elf64_addr endian entry.elf64_sh_addr ; bytes_of_elf64_off endian entry.elf64_sh_offset ; bytes_of_elf64_xword endian entry.elf64_sh_size ; bytes_of_elf64_word endian entry.elf64_sh_link ; bytes_of_elf64_word endian entry.elf64_sh_info ; bytes_of_elf64_xword endian entry.elf64_sh_addralign ; bytes_of_elf64_xword endian entry.elf64_sh_entsize ]) (** [read_elf64_section_header_table_entry ed bs0] reads a section header table * entry from [bs0] assuming endianness [ed]. Also returns the suffix of [bs0] * after parsing. Fails if the entry cannot be read. *) (*val read_elf64_section_header_table_entry : endianness -> byte_sequence -> error (elf64_section_header_table_entry * byte_sequence)*) let read_elf64_section_header_table_entry endian bs:(elf64_section_header_table_entry*Byte_sequence_wrapper.byte_sequence)error= (bind (read_elf64_word endian bs) (fun (sh_name, bs) -> bind (read_elf64_word endian bs) (fun (sh_type, bs) -> bind (read_elf64_xword endian bs) (fun (sh_flags, bs) -> bind (read_elf64_addr endian bs) (fun (sh_addr, bs) -> bind (read_elf64_off endian bs) (fun (sh_offset, bs) -> bind (read_elf64_xword endian bs) (fun (sh_size, bs) -> bind (read_elf64_word endian bs) (fun (sh_link, bs) -> bind (read_elf64_word endian bs) (fun (sh_info, bs) -> bind (read_elf64_xword endian bs) (fun (sh_addralign, bs) -> bind (read_elf64_xword endian bs) (fun (sh_entsize, bs) -> return ({ elf64_sh_name = sh_name; elf64_sh_type = sh_type; elf64_sh_flags = sh_flags; elf64_sh_addr = sh_addr; elf64_sh_offset = sh_offset; elf64_sh_size = sh_size; elf64_sh_link = sh_link; elf64_sh_info = sh_info; elf64_sh_addralign = sh_addralign; elf64_sh_entsize = sh_entsize }, bs)))))))))))) (** [bytes_of_elf32_section_header_table ed tbl] blits section header table [tbl] * to a byte sequence assuming endianness [ed]. *) (*val bytes_of_elf32_section_header_table : endianness -> elf32_section_header_table -> byte_sequence*) let bytes_of_elf32_section_header_table endian tbl:Byte_sequence_wrapper.byte_sequence= (Byte_sequence.concat (Lem_list.map (bytes_of_elf32_section_header_table_entry endian) tbl)) (** [bytes_of_elf64_section_header_table ed tbl] blits section header table [tbl] * to a byte sequence assuming endianness [ed]. *) (*val bytes_of_elf64_section_header_table : endianness -> elf64_section_header_table -> byte_sequence*) let bytes_of_elf64_section_header_table endian tbl:Byte_sequence_wrapper.byte_sequence= (Byte_sequence.concat (Lem_list.map (bytes_of_elf64_section_header_table_entry endian) tbl)) (** [read_elf32_section_header_table' ed bs0] parses an ELF32 section header table * from byte sequence [bs0] assuming endianness [ed]. Assumes [bs0] is of the * exact length required to parse the entire table. * Fails if any of the section header table entries cannot be parsed. *) (*val read_elf32_section_header_table' : endianness -> byte_sequence -> error elf32_section_header_table*) let rec read_elf32_section_header_table' endian bs0:((elf32_section_header_table_entry)list)error= (if Nat_big_num.equal (Byte_sequence.length0 bs0)( (Nat_big_num.of_int 0)) then return [] else bind (read_elf32_section_header_table_entry endian bs0) (fun (entry, bs1) -> bind (read_elf32_section_header_table' endian bs1) (fun sht -> return (entry :: sht)))) (** [read_elf64_section_header_table' ed bs0] parses an ELF64 section header table * from byte sequence [bs0] assuming endianness [ed]. Assumes [bs0] is of the * exact length required to parse the entire table. * Fails if any of the section header table entries cannot be parsed. *) (*val read_elf64_section_header_table' : endianness -> byte_sequence -> error elf64_section_header_table*) let rec read_elf64_section_header_table' endian bs0:((elf64_section_header_table_entry)list)error= (if Nat_big_num.equal (Byte_sequence.length0 bs0)( (Nat_big_num.of_int 0)) then return [] else bind (read_elf64_section_header_table_entry endian bs0) (fun (entry, bs1) -> bind (read_elf64_section_header_table' endian bs1) (fun sht -> return (entry :: sht)))) (** [read_elf32_section_header_table sz ed bs0] parses an ELF32 section header * table from a [sz] sized prefix of byte sequence [bs0] assuming endianness * [ed]. The suffix of [bs0] remaining after parsing is also returned. * Fails if any of the section header entries cannot be parsed or if [sz] is * greater than the length of [bs0]. *) (*val read_elf32_section_header_table : natural -> endianness -> byte_sequence -> error (elf32_section_header_table * byte_sequence)*) let read_elf32_section_header_table table_size endian bs0:((elf32_section_header_table_entry)list*Byte_sequence_wrapper.byte_sequence)error= (bind (partition0 table_size bs0) (fun (eat, rest) -> bind (read_elf32_section_header_table' endian eat) (fun entries -> return (entries, rest)))) (** [read_elf64_section_header_table sz ed bs0] parses an ELF64 section header * table from a [sz] sized prefix of byte sequence [bs0] assuming endianness * [ed]. The suffix of [bs0] remaining after parsing is also returned. * Fails if any of the section header entries cannot be parsed or if [sz] is * greater than the length of [bs0]. *) (*val read_elf64_section_header_table : natural -> endianness -> byte_sequence -> error (elf64_section_header_table * byte_sequence)*) let read_elf64_section_header_table table_size endian bs0:((elf64_section_header_table_entry)list*Byte_sequence_wrapper.byte_sequence)error= (bind (partition0 table_size bs0) (fun (eat, rest) -> bind (read_elf64_section_header_table' endian eat) (fun entries -> return (entries, rest)))) (** Correctness criteria *) (** TODO: what is going on here? *) (*val elf32_size_correct : elf32_section_header_table_entry -> elf32_section_header_table -> bool*) let elf32_size_correct hdr tbl:bool= (let m = (Uint32_wrapper.to_bigint hdr.elf32_sh_size) in if Nat_big_num.equal m( (Nat_big_num.of_int 0)) then true else Nat_big_num.equal m (Nat_big_num.of_int (List.length tbl))) (** TODO: what is going on here? *) (*val elf64_size_correct : elf64_section_header_table_entry -> elf64_section_header_table -> bool*) let elf64_size_correct hdr tbl:bool= (let m = (Ml_bindings.nat_big_num_of_uint64 hdr.elf64_sh_size) in if Nat_big_num.equal m( (Nat_big_num.of_int 0)) then true else Nat_big_num.equal m (Nat_big_num.of_int (List.length tbl))) (** [is_elf32_addr_addralign_correct ent] checks whether an internal address * alignment constraint is met on section header table [ent]. * TODO: needs tweaking to add in power-of-two constraint, too. *) (*val is_elf32_addr_addralign_correct : elf32_section_header_table_entry -> bool*) let is_elf32_addr_addralign_correct ent:bool= (let align = (Uint32_wrapper.to_bigint ent.elf32_sh_addralign) in let addr = (Uint32_wrapper.to_bigint ent.elf32_sh_addr) in if Nat_big_num.equal (Nat_big_num.modulus addr align)( (Nat_big_num.of_int 0)) then Nat_big_num.equal align( (Nat_big_num.of_int 0)) || Nat_big_num.equal align( (Nat_big_num.of_int 1)) (* TODO: or a power of two *) else false) (** [is_elf64_addr_addralign_correct ent] checks whether an internal address * alignment constraint is met on section header table [ent]. * TODO: needs tweaking to add in power-of-two constraint, too. *) (*val is_elf64_addr_addralign_correct : elf64_section_header_table_entry -> bool*) let is_elf64_addr_addralign_correct ent:bool= (let align = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_addralign) in let addr = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_addr) in if Nat_big_num.equal (Nat_big_num.modulus addr align)( (Nat_big_num.of_int 0)) then Nat_big_num.equal align( (Nat_big_num.of_int 0)) || Nat_big_num.equal align( (Nat_big_num.of_int 1)) (* TODO: or a power of two *) else false) (** [is_valid_elf32_section_header_table sht] checks whether all entries of * section header table [sht] are valid. *) (*val is_valid_elf32_section_header_table : elf32_section_header_table -> bool*) let is_valid_elf32_section_header_table tbl:bool= ((match tbl with | [] -> true | x::xs -> Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_sh_name)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_sh_type) sht_null && (Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_sh_flags)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_sh_addr)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_sh_offset)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_sh_info)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_sh_addralign)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_sh_entsize)( (Nat_big_num.of_int 0)) && elf32_size_correct x tbl))))))) (* XXX: more correctness criteria in time *) )) (** [is_valid_elf64_section_header_table sht] checks whether all entries of * section header table [sht] are valid. *) (*val is_valid_elf64_section_header_table : elf64_section_header_table -> bool*) let is_valid_elf64_section_header_table tbl:bool= ((match tbl with | [] -> true | x::xs -> Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf64_sh_name)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf64_sh_type) sht_null && (Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_flags)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_addr)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal (Uint64_wrapper.to_bigint x.elf64_sh_offset)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf64_sh_info)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_addralign)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_entsize)( (Nat_big_num.of_int 0)) && elf64_size_correct x tbl))))))) (* XXX: more correctness criteria in time *) )) (** Pretty printing *) (** The [sht_print_bundle] type is used to tidy up other type signatures. Some of the * top-level string_of_ functions require six or more functions passed to them, * which quickly gets out of hand. This type is used to reduce that complexity. * The first component of the type is an OS specific print function, the second is * a processor specific print function. *) type sht_print_bundle = (Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string) (** [string_of_elf32_section_header_table_entry sht ent] produces a string * representation of section header table entry [ent] using [sht], a * [sht_print_bundle]. * OCaml specific definition. *) (*val string_of_elf32_section_header_table_entry : sht_print_bundle -> elf32_section_header_table_entry -> string*) let string_of_elf32_section_header_table_entry (os, proc, user) entry:string= (unlines [ ("\t" ^ ("Name: " ^ Uint32_wrapper.to_string entry.elf32_sh_name)) ; ("\t" ^ ("Type: " ^ string_of_section_type os proc user (Uint32_wrapper.to_bigint entry.elf32_sh_type))) ; ("\t" ^ ("Flags: " ^ Uint32_wrapper.to_string entry.elf32_sh_flags)) ; ("\t" ^ ("Address: " ^ Uint32_wrapper.to_string entry.elf32_sh_addr)) ; ("\t" ^ ("Size: " ^ Uint32_wrapper.to_string entry.elf32_sh_size)) ]) (** [string_of_elf64_section_header_table_entry sht ent] produces a string * representation of section header table entry [ent] using [sht], a * [sht_print_bundle]. * OCaml specific definition. *) (*val string_of_elf64_section_header_table_entry : sht_print_bundle -> elf64_section_header_table_entry -> string*) let string_of_elf64_section_header_table_entry (os, proc, user) entry:string= (unlines [ ("\t" ^ ("Name: " ^ Uint32_wrapper.to_string entry.elf64_sh_name)) ; ("\t" ^ ("Type: " ^ string_of_section_type os proc user (Uint32_wrapper.to_bigint entry.elf64_sh_type))) ; ("\t" ^ ("Flags: " ^ Uint64_wrapper.to_string entry.elf64_sh_flags)) ; ("\t" ^ ("Address: " ^ Uint64_wrapper.to_string entry.elf64_sh_addr)) ; ("\t" ^ ("Size: " ^ Uint64_wrapper.to_string entry.elf64_sh_size)) ]) (** [string_of_elf32_section_header_table_entry' sht stab ent] produces a string * representation of section header table entry [ent] using [sht] and section * header string table [stab] to print the name of the section header entry * correctly. * OCaml specific definition. *) (*val string_of_elf32_section_header_table_entry' : sht_print_bundle -> string_table -> elf32_section_header_table_entry -> string*) let string_of_elf32_section_header_table_entry' (os, proc, user) stbl entry:string= (let name1 = ((match get_string_at (Uint32_wrapper.to_bigint entry.elf32_sh_name) stbl with | Fail _ -> "Invalid index into string table" | Success i -> i )) in unlines [ ("\t" ^ ("Name: " ^ name1)) ; ("\t" ^ ("Type: " ^ string_of_section_type os proc user (Uint32_wrapper.to_bigint entry.elf32_sh_type))) ; ("\t" ^ ("Flags: " ^ Uint32_wrapper.to_string entry.elf32_sh_flags)) ; ("\t" ^ ("Address: " ^ Uint32_wrapper.to_string entry.elf32_sh_addr)) ; ("\t" ^ ("Size: " ^ Uint32_wrapper.to_string entry.elf32_sh_size)) ]) (** [string_of_elf64_section_header_table_entry' sht stab ent] produces a string * representation of section header table entry [ent] using [sht] and section * header string table [stab] to print the name of the section header entry * correctly. * OCaml specific definition. *) (*val string_of_elf64_section_header_table_entry' : sht_print_bundle -> string_table -> elf64_section_header_table_entry -> string*) let string_of_elf64_section_header_table_entry' (os, proc, user) stbl entry:string= (let name1 = ((match get_string_at (Uint32_wrapper.to_bigint entry.elf64_sh_name) stbl with | Fail _ -> "Invalid index into string table" | Success i -> i )) in unlines [ ("\t" ^ ("Name: " ^ name1)) ; ("\t" ^ ("Type: " ^ string_of_section_type os proc user (Uint32_wrapper.to_bigint entry.elf64_sh_type))) ; ("\t" ^ ("Flags: " ^ Uint64_wrapper.to_string entry.elf64_sh_flags)) ; ("\t" ^ ("Address: " ^ Uint64_wrapper.to_string entry.elf64_sh_addr)) ; ("\t" ^ ("Size: " ^ Uint64_wrapper.to_string entry.elf64_sh_size)) ]) (** The following defintions are default printing functions, with no ABI-specific * functionality, in order to produce a [Show] instance for section header * table entries. *) (*val string_of_elf32_section_header_table_entry_default : elf32_section_header_table_entry -> string*) let string_of_elf32_section_header_table_entry_default:elf32_section_header_table_entry ->string= (string_of_elf32_section_header_table_entry (((fun y->"*Default OS specific print*")), ((fun y->"*Default processor specific print*")), ((fun y->"*Default user specific print*")))) let instance_Show_Show_Elf_section_header_table_elf32_section_header_table_entry_dict:(elf32_section_header_table_entry)show_class= ({ show_method = string_of_elf32_section_header_table_entry_default}) (*val string_of_elf64_section_header_table_entry_default : elf64_section_header_table_entry -> string*) let string_of_elf64_section_header_table_entry_default:elf64_section_header_table_entry ->string= (string_of_elf64_section_header_table_entry (((fun y->"*Default OS specific print*")), ((fun y->"*Default processor specific print*")), ((fun y->"*Default user specific print*")))) let instance_Show_Show_Elf_section_header_table_elf64_section_header_table_entry_dict:(elf64_section_header_table_entry)show_class= ({ show_method = string_of_elf64_section_header_table_entry_default}) (*val string_of_elf32_section_header_table : sht_print_bundle -> elf32_section_header_table -> string*) let string_of_elf32_section_header_table sht_bdl tbl:string= (unlines (Lem_list.map (string_of_elf32_section_header_table_entry sht_bdl) tbl)) (*val string_of_elf32_section_header_table_default : elf32_section_header_table -> string*) let string_of_elf32_section_header_table_default:elf32_section_header_table ->string= (string_of_elf32_section_header_table (((fun y->"*Default OS specific print*")), ((fun y->"*Default processor specific print*")), ((fun y->"*Default user specific print*")))) (*val string_of_elf64_section_header_table : sht_print_bundle -> elf64_section_header_table -> string*) let string_of_elf64_section_header_table sht_bdl tbl:string= (unlines (Lem_list.map (string_of_elf64_section_header_table_entry sht_bdl) tbl)) (*val string_of_elf64_section_header_table_default : elf64_section_header_table -> string*) let string_of_elf64_section_header_table_default:elf64_section_header_table ->string= (string_of_elf64_section_header_table (((fun y->"*Default OS specific print*")), ((fun y->"*Default processor specific print*")), ((fun y->"*Default user specific print*")))) (*val string_of_elf32_section_header_table' : sht_print_bundle -> string_table -> elf32_section_header_table -> string*) let string_of_elf32_section_header_table' sht_bdl stbl tbl:string= (unlines (Lem_list.map (string_of_elf32_section_header_table_entry' sht_bdl stbl) tbl)) (*val string_of_elf64_section_header_table' : sht_print_bundle -> string_table -> elf64_section_header_table -> string*) let string_of_elf64_section_header_table' sht_bdl stbl tbl:string= (unlines (Lem_list.map (string_of_elf64_section_header_table_entry' sht_bdl stbl) tbl)) (** Section to segment mappings *) (** [elf32_tbss_special shdr seg] implements the ELF_TBSS_SPECIAL macro from readelf: * * #define ELF_TBSS_SPECIAL(sec_hdr, segment) \ * (((sec_hdr)->sh_flags & SHF_TLS) != 0 \ * && (sec_hdr)->sh_type == SHT_NOBITS \ * && (segment)->p_type != PT_TLS) * * From readelf source code, file [internal.h]. * *) (*val is_elf32_tbss_special : elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) let is_elf32_tbss_special sec_hdr segment:bool= (not ((Uint32_wrapper.logand sec_hdr.elf32_sh_flags (Uint32_wrapper.of_bigint shf_tls)) = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))) && (( Nat_big_num.equal(Uint32_wrapper.to_bigint sec_hdr.elf32_sh_type) sht_nobits) && ( not (Nat_big_num.equal (Uint32_wrapper.to_bigint segment.elf32_p_type) elf_pt_tls)))) (** [elf64_tbss_special shdr seg] implements the ELF_TBSS_SPECIAL macro from readelf: * * #define ELF_TBSS_SPECIAL(sec_hdr, segment) \ * (((sec_hdr)->sh_flags & SHF_TLS) != 0 \ * && (sec_hdr)->sh_type == SHT_NOBITS \ * && (segment)->p_type != PT_TLS) * * From readelf source code, file [internal.h]. * *) (*val is_elf64_tbss_special : elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) let is_elf64_tbss_special sec_hdr segment:bool= (not ((Uint64_wrapper.logand sec_hdr.elf64_sh_flags (Uint64_wrapper.of_bigint shf_tls)) = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))) && (( Nat_big_num.equal(Uint32_wrapper.to_bigint sec_hdr.elf64_sh_type) sht_nobits) && ( not (Nat_big_num.equal (Uint32_wrapper.to_bigint segment.elf64_p_type) elf_pt_tls)))) (** [get_elf32_section_to_segment_mapping hdr sht pht isin stbl] computes the * section to segment mapping for an ELF file using information in the section * header table [sht], program header table [pht] and file header [hdr]. A * string table [stbl] is taken to produce the string output. The test whether * a section lies withing a segment is ABI specific, so [isin] is used to perform * the test. *) (*val get_elf32_section_to_segment_mapping : elf32_header -> elf32_section_header_table -> elf32_program_header_table_entry -> (elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool) -> string_table -> error (list string)*) let rec get_elf32_section_to_segment_mapping hdr sects pent isin stbl:((string)list)error= ((match sects with | [] -> return [] | x::xs -> if is_elf32_tbss_special x pent then get_elf32_section_to_segment_mapping hdr xs pent isin stbl else if not (isin hdr x pent) then get_elf32_section_to_segment_mapping hdr xs pent isin stbl else let nm = (Uint32_wrapper.to_bigint x.elf32_sh_name) in bind (get_string_at nm stbl) (fun str -> bind (get_elf32_section_to_segment_mapping hdr xs pent isin stbl) (fun tl -> return (str :: tl))) )) (** [get_elf64_section_to_segment_mapping hdr sht pht isin stbl] computes the * section to segment mapping for an ELF file using information in the section * header table [sht], program header table [pht] and file header [hdr]. A * string table [stbl] is taken to produce the string output. The test whether * a section lies withing a segment is ABI specific, so [isin] is used to perform * the test. *) (*val get_elf64_section_to_segment_mapping : elf64_header -> elf64_section_header_table -> elf64_program_header_table_entry -> (elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool) -> string_table -> error (list string)*) let rec get_elf64_section_to_segment_mapping hdr sects pent isin stbl:((string)list)error= ((match sects with | [] -> return [] | x::xs -> if not (isin hdr x pent) then get_elf64_section_to_segment_mapping hdr xs pent isin stbl else if is_elf64_tbss_special x pent then get_elf64_section_to_segment_mapping hdr xs pent isin stbl else let nm = (Uint32_wrapper.to_bigint x.elf64_sh_name) in bind (get_string_at nm stbl) (fun str -> bind (get_elf64_section_to_segment_mapping hdr xs pent isin stbl) (fun tl -> return (str :: tl))) )) (** Section groups *) (** This is a COMDAT group and may duplicate other COMDAT groups in other object * files. *) let grp_comdat : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** Any bits in the following mask ranges are reserved exclusively for OS and * processor specific semantics, respectively. *) let grp_maskos : Nat_big_num.num= ( (Nat_big_num.of_int 267386880)) (* 0x0ff00000 *) let grp_maskproc : Nat_big_num.num= (Nat_big_num.mul( (Nat_big_num.of_int 4))( (Nat_big_num.of_int 1006632960))) (* 0xf0000000 *) (** [obtain_elf32_section_group_indices endian sht bs0] extracts all section header * table indices of sections that are marked as being part of a section group. *) (*val obtain_elf32_section_group_indices : endianness -> elf32_section_header_table -> byte_sequence -> error (list (natural * list elf32_word))*) let obtain_elf32_section_group_indices endian sht bs0:((Nat_big_num.num*(Uint32_wrapper.uint32)list)list)error= (let filtered = (List.filter (fun ent -> Nat_big_num.equal (Uint32_wrapper.to_bigint ent.elf32_sh_type) sht_group) sht) in mapM (fun grp -> let off = (Uint32_wrapper.to_bigint grp.elf32_sh_offset) in let siz = (Uint32_wrapper.to_bigint grp.elf32_sh_size) in let cnt = (Nat_big_num.div siz( (Nat_big_num.of_int 4))) (* size of elf32_word in bytes *) in bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (Error.repeatM' cnt rel (read_elf32_word endian)) (fun (mems, _) -> (match mems with | [] -> fail "obtain_elf32_section_group_indices: section group sections must consist of at least one elf32_word" | x::xs -> let flag = (Uint32_wrapper.to_bigint x) in return (flag, xs) ))) ) filtered) (** [obtain_elf64_section_group_indices endian sht bs0] extracts all section header * table indices of sections that are marked as being part of a section group. *) (*val obtain_elf64_section_group_indices : endianness -> elf64_section_header_table -> byte_sequence -> error (list (natural * list elf64_word))*) let obtain_elf64_section_group_indices endian sht bs0:((Nat_big_num.num*(Uint32_wrapper.uint32)list)list)error= (let filtered = (List.filter (fun ent -> Nat_big_num.equal (Uint32_wrapper.to_bigint ent.elf64_sh_type) sht_group) sht) in mapM (fun grp -> let off = (Uint64_wrapper.to_bigint grp.elf64_sh_offset) in let siz = (Ml_bindings.nat_big_num_of_uint64 grp.elf64_sh_size) in let cnt = (Nat_big_num.div siz( (Nat_big_num.of_int 4))) (* size of elf64_word in bytes *) in bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (Error.repeatM' cnt rel (read_elf64_word endian)) (fun (mems, _) -> (match mems with | [] -> fail "obtain_elf64_section_group_indices: section group sections must consist of at least one elf64_word" | x::xs -> let flag = (Uint32_wrapper.to_bigint x) in return (flag, xs) ))) ) filtered) (** [obtain_elf32_tls_template sht] extracts the TLS template (i.e. all sections * in section header table [sht] that have their TLS flag bit set). *) (*val obtain_elf32_tls_template : elf32_section_header_table -> elf32_section_header_table*) let obtain_elf32_tls_template sht:(elf32_section_header_table_entry)list= (List.filter (fun ent -> let flags = (Uint32_wrapper.to_bigint ent.elf32_sh_flags) in not (Nat_big_num.equal (Nat_big_num.bitwise_and flags shf_tls)( (Nat_big_num.of_int 0)))) sht) (** [obtain_elf64_tls_template sht] extracts the TLS template (i.e. all sections * in section header table [sht] that have their TLS flag bit set). *) (*val obtain_elf64_tls_template : elf64_section_header_table -> elf64_section_header_table*) let obtain_elf64_tls_template sht:(elf64_section_header_table_entry)list= (List.filter (fun ent -> let flags = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_flags) in not (Nat_big_num.equal (Nat_big_num.bitwise_and flags shf_tls)( (Nat_big_num.of_int 0)))) sht) (** [obtain_elf32_hash_table endian sht bs0] extracts a hash table from an ELF file * providing a section of type SHT_HASH exists in section header table [sht]. * Extraction is from byte sequence [bs0] assuming endianness [endian]. The * return type represents the number of buckets, the number of chains, the buckets * and finally the chains. *) (*val obtain_elf32_hash_table : endianness -> elf32_section_header_table -> byte_sequence -> error (elf32_word * elf32_word * list elf32_word * list elf32_word)*) let obtain_elf32_hash_table endian sht bs0:(Uint32_wrapper.uint32*Uint32_wrapper.uint32*(Uint32_wrapper.uint32)list*(Uint32_wrapper.uint32)list)error= (let filtered = (List.filter (fun ent -> Nat_big_num.equal (Uint32_wrapper.to_bigint ent.elf32_sh_type) sht_hash) sht) in (match filtered with | [] -> fail "obtain_elf32_hash_table: no section header table entry of type sht_hash" | [x] -> let siz = (Uint32_wrapper.to_bigint x.elf32_sh_size) in let off = (Uint32_wrapper.to_bigint x.elf32_sh_offset) in bind (Byte_sequence.offset_and_cut siz off bs0) (fun rel -> bind (read_elf32_word endian rel) (fun (nbucket, rel) -> bind (read_elf32_word endian rel) (fun (nchain, rel) -> bind (Error.repeatM' (Uint32_wrapper.to_bigint nbucket) rel (read_elf32_word endian)) (fun (buckets, rel) -> bind (Error.repeatM' (Uint32_wrapper.to_bigint nchain) rel (read_elf32_word endian)) (fun (chain, _) -> return (nbucket, nchain, buckets, chain)))))) | _ -> fail "obtain_elf32_hash_table: multiple section header table entries of type sht_hash" )) (** [obtain_elf64_hash_table endian sht bs0] extracts a hash table from an ELF file * providing a section of type SHT_HASH exists in section header table [sht]. * Extraction is from byte sequence [bs0] assuming endianness [endian]. The * return type represents the number of buckets, the number of chains, the buckets * and finally the chains. *) (*val obtain_elf64_hash_table : endianness -> elf64_section_header_table -> byte_sequence -> error (elf64_word * elf64_word * list elf64_word * list elf64_word)*) let obtain_elf64_hash_table endian sht bs0:(Uint32_wrapper.uint32*Uint32_wrapper.uint32*(Uint32_wrapper.uint32)list*(Uint32_wrapper.uint32)list)error= (let filtered = (List.filter (fun ent -> Nat_big_num.equal (Uint32_wrapper.to_bigint ent.elf64_sh_type) sht_hash) sht) in (match filtered with | [] -> fail "obtain_elf64_hash_table: no section header table entry of type sht_hash" | [x] -> let siz = (Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_size) in let off = (Uint64_wrapper.to_bigint x.elf64_sh_offset) in bind (Byte_sequence.offset_and_cut siz off bs0) (fun rel -> bind (read_elf64_word endian rel) (fun (nbucket, rel) -> bind (read_elf64_word endian rel) (fun (nchain, rel) -> bind (Error.repeatM' (Uint32_wrapper.to_bigint nbucket) rel (read_elf64_word endian)) (fun (buckets, rel) -> bind (Error.repeatM' (Uint32_wrapper.to_bigint nchain) rel (read_elf64_word endian)) (fun (chain, _) -> return (nbucket, nchain, buckets, chain)))))) | _ -> fail "obtain_elf64_hash_table: multiple section header table entries of type sht_hash" )) (** Special sections *) (** [construct_special_sections] contains a finite map from section name (as * a string) to the expected attributes and flags expected of that section, * as specified in the ELF specification. * NOTE: some of these are overriden by the ABI. *) (*val elf_special_sections : Map.map string (natural * natural)*) let elf_special_sections:((string),(Nat_big_num.num*Nat_big_num.num))Pmap.map= (Lem_map.fromList (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) [ (".bss", (sht_nobits, Nat_big_num.add shf_alloc shf_write)) ; (".comment", (sht_progbits, (Nat_big_num.of_int 0))) ; (".data", (sht_progbits, Nat_big_num.add shf_alloc shf_write)) ; (".data1", (sht_progbits, Nat_big_num.add shf_alloc shf_write)) ; (".debug", (sht_progbits, (Nat_big_num.of_int 0))) (* ; (".dynamic", (sht_dynamic, ?)) *) ; (".dynstr", (sht_strtab, shf_alloc)) ; (".dynsym", (sht_dynsym, shf_alloc)) ; (".fini", (sht_progbits, Nat_big_num.add shf_alloc shf_execinstr)) ; (".fini_array", (sht_fini_array, Nat_big_num.add shf_alloc shf_write)) (* ; (".got", (sht_progbits, ?)) *) ; (".hash", (sht_hash, shf_alloc)) ; (".init", (sht_progbits, Nat_big_num.add shf_alloc shf_execinstr)) ; (".init_array", (sht_init_array, Nat_big_num.add shf_alloc shf_write)) (* ; (".interp", (sht_progbits, ?)) *) ; (".line", (sht_progbits, (Nat_big_num.of_int 0))) ; (".note", (sht_note, (Nat_big_num.of_int 0))) (* ; (".plt", (sht_progbits, ?)) *) ; (".preinit_array", (sht_preinit_array, Nat_big_num.add shf_alloc shf_write)) (* ; (".relname", (sht_rel, ?)) *) (* ; (".relaname", (sht_rela, ?)) *) ; (".rodata", (sht_progbits, shf_alloc)) ; (".rodata1", (sht_progbits, shf_alloc)) ; (".shstrtab", (sht_strtab, (Nat_big_num.of_int 0))) (* ; (".strtab", (sht_strtab, ?)) *) (* ; (".symtab", (sht_symtab, ?)) *) (* ; (".symtab_shndx", (sht_symtab_shndx, ?)) *) ; (".tbss", (sht_nobits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_tls)) ; (".tdata", (sht_progbits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_tls)) ; (".tdata1", (sht_progbits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_tls)) ; (".text", (sht_progbits, Nat_big_num.add shf_alloc shf_execinstr)) ])
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>