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/linker_script.ml.html
Source file linker_script.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 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494 1495 1496 1497 1498 1499 1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515 1516 1517 1518 1519 1520 1521 1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 1542 1543 1544 1545 1546 1547 1548 1549 1550 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581 1582 1583 1584 1585 1586 1587 1588 1589 1590 1591 1592 1593 1594 1595 1596 1597 1598 1599 1600 1601 1602 1603 1604 1605 1606 1607 1608 1609 1610 1611 1612 1613 1614 1615 1616 1617 1618 1619 1620 1621 1622 1623 1624 1625 1626 1627 1628 1629 1630 1631 1632 1633 1634 1635 1636 1637 1638 1639 1640 1641 1642 1643 1644 1645 1646 1647 1648 1649 1650 1651 1652 1653 1654 1655 1656 1657 1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 1673 1674 1675 1676 1677 1678 1679 1680 1681 1682 1683 1684 1685 1686 1687 1688 1689 1690 1691 1692 1693 1694 1695 1696 1697 1698 1699 1700 1701 1702 1703 1704 1705 1706 1707 1708 1709 1710 1711 1712 1713 1714 1715 1716 1717 1718 1719 1720 1721 1722 1723 1724 1725 1726 1727 1728 1729 1730 1731 1732 1733 1734 1735 1736 1737 1738 1739 1740 1741 1742 1743 1744 1745 1746 1747 1748 1749 1750 1751 1752 1753 1754 1755 1756 1757 1758 1759 1760 1761 1762 1763 1764 1765 1766 1767 1768 1769 1770 1771 1772 1773 1774 1775 1776 1777 1778 1779 1780 1781 1782 1783 1784 1785 1786 1787 1788 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820 1821 1822 1823 1824 1825 1826 1827 1828 1829 1830 1831 1832 1833 1834 1835 1836 1837 1838 1839 1840 1841 1842 1843 1844 1845 1846 1847 1848 1849 1850 1851 1852 1853 1854 1855 1856 1857 1858 1859 1860 1861 1862 1863 1864 1865 1866 1867 1868 1869 1870 1871 1872 1873 1874 1875 1876 1877 1878 1879 1880 1881 1882 1883 1884 1885 1886 1887 1888 1889 1890 1891 1892 1893 1894 1895 1896 1897 1898 1899 1900 1901 1902 1903 1904 1905 1906 1907 1908 1909 1910 1911 1912 1913 1914 1915 1916 1917 1918 1919 1920 1921 1922 1923 1924 1925 1926 1927 1928 1929 1930 1931 1932 1933 1934 1935 1936 1937 1938 1939 1940 1941 1942 1943 1944 1945 1946 1947 1948 1949 1950 1951 1952 1953 1954 1955 1956 1957 1958 1959 1960 1961 1962 1963 1964 1965 1966 1967 1968 1969 1970 1971 1972 1973 1974 1975 1976 1977 1978 1979 1980 1981 1982 1983 1984 1985 1986 1987 1988 1989 1990 1991 1992 1993 1994 1995 1996 1997 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020 2021 2022 2023 2024 2025 2026 2027 2028 2029 2030 2031 2032 2033 2034 2035 2036 2037 2038 2039 2040 2041 2042 2043 2044 2045 2046 2047 2048 2049 2050 2051 2052 2053 2054 2055 2056 2057 2058 2059 2060 2061 2062 2063 2064 2065 2066 2067 2068 2069 2070 2071 2072 2073 2074 2075 2076 2077 2078 2079 2080 2081 2082 2083 2084 2085 2086 2087 2088 2089 2090 2091 2092 2093 2094 2095 2096 2097 2098 2099 2100 2101 2102 2103 2104 2105 2106 2107 2108 2109 2110 2111 2112 2113 2114 2115 2116 2117 2118 2119 2120 2121 2122 2123 2124 2125 2126 2127 2128 2129 2130 2131 2132 2133 2134 2135 2136 2137 2138 2139 2140 2141 2142 2143 2144 2145 2146 2147 2148 2149 2150 2151 2152 2153 2154 2155 2156 2157 2158 2159 2160 2161 2162 2163 2164 2165 2166 2167 2168 2169 2170 2171 2172 2173 2174 2175 2176 2177 2178 2179 2180 2181 2182 2183 2184 2185 2186 2187 2188 2189 2190 2191 2192 2193 2194 2195 2196 2197 2198 2199 2200 2201 2202 2203 2204 2205 2206 2207 2208 2209 2210 2211 2212 2213 2214 2215 2216 2217 2218 2219 2220 2221 2222 2223 2224 2225 2226 2227 2228 2229 2230 2231 2232 2233 2234 2235 2236 2237 2238 2239 2240 2241 2242 2243 2244 2245 2246 2247 2248 2249 2250 2251 2252 2253 2254 2255 2256 2257 2258 2259 2260 2261 2262 2263 2264 2265 2266 2267 2268 2269 2270 2271 2272 2273 2274 2275 2276 2277 2278 2279 2280 2281 2282 2283 2284 2285 2286 2287 2288 2289 2290 2291 2292 2293 2294 2295 2296 2297 2298 2299 2300 2301 2302 2303 2304 2305 2306 2307 2308 2309 2310 2311 2312 2313 2314 2315 2316 2317 2318 2319 2320 2321 2322 2323 2324 2325 2326 2327 2328 2329 2330 2331 2332 2333 2334 2335 2336 2337 2338 2339 2340 2341 2342 2343 2344 2345 2346 2347 2348 2349 2350 2351 2352 2353 2354 2355 2356 2357 2358 2359 2360 2361 2362 2363 2364 2365 2366 2367 2368 2369 2370 2371 2372 2373 2374 2375 2376 2377 2378 2379 2380 2381 2382 2383 2384 2385 2386 2387 2388 2389 2390 2391 2392 2393 2394 2395 2396 2397 2398 2399 2400 2401 2402 2403 2404 2405 2406 2407 2408 2409 2410 2411 2412 2413 2414 2415 2416 2417 2418 2419 2420 2421 2422 2423 2424 2425 2426 2427 2428 2429 2430 2431 2432 2433 2434 2435 2436 2437 2438 2439 2440 2441 2442 2443 2444 2445 2446 2447 2448 2449 2450 2451 2452 2453 2454 2455 2456 2457 2458 2459 2460 2461 2462 2463 2464 2465 2466 2467 2468 2469 2470 2471 2472 2473 2474 2475 2476 2477 2478 2479 2480 2481 2482 2483 2484 2485 2486 2487 2488 2489 2490 2491 2492 2493 2494 2495 2496 2497 2498 2499 2500 2501 2502 2503 2504 2505 2506 2507 2508 2509 2510 2511 2512 2513 2514 2515 2516 2517 2518 2519 2520 2521 2522 2523 2524 2525 2526 2527 2528 2529 2530 2531 2532 2533 2534 2535 2536 2537 2538 2539 2540 2541 2542 2543 2544 2545 2546 2547 2548 2549 2550 2551 2552 2553 2554 2555 2556 2557 2558 2559 2560 2561 2562 2563 2564 2565 2566 2567 2568 2569 2570 2571 2572 2573 2574 2575 2576 2577 2578 2579 2580 2581 2582 2583 2584 2585 2586 2587 2588 2589 2590 2591 2592 2593 2594 2595 2596 2597 2598 2599 2600 2601 2602 2603 2604 2605 2606 2607 2608 2609 2610 2611 2612 2613 2614 2615 2616 2617 2618 2619 2620 2621 2622 2623 2624 2625 2626 2627 2628 2629 2630 2631 2632 2633 2634 2635 2636 2637 2638 2639 2640 2641 2642 2643 2644 2645 2646 2647 2648 2649 2650 2651 2652 2653 2654 2655 2656 2657 2658 2659 2660 2661 2662 2663 2664 2665 2666 2667 2668 2669 2670 2671 2672 2673 2674 2675 2676 2677 2678 2679 2680 2681 2682 2683 2684 2685 2686 2687 2688 2689 2690 2691 2692 2693 2694 2695 2696 2697 2698 2699 2700 2701 2702 2703 2704 2705 2706 2707 2708 2709 2710 2711 2712 2713 2714 2715 2716 2717 2718 2719 2720 2721 2722 2723 2724 2725 2726 2727 2728 2729 2730 2731 2732 2733 2734 2735 2736 2737 2738 2739 2740 2741 2742 2743 2744 2745 2746 2747 2748 2749 2750 2751 2752 2753 2754 2755 2756 2757 2758 2759 2760 2761 2762 2763 2764 2765 2766 2767 2768 2769 2770 2771 2772 2773 2774 2775 2776 2777 2778 2779 2780 2781 2782 2783 2784 2785 2786 2787 2788
(*Generated by Lem from linker_script.lem.*) open Lem_basic_classes open Lem_function open Lem_string open Lem_tuple open Lem_bool open Lem_list open Lem_sorting open Lem_num open Lem_maybe open Lem_assert_extra open Lem_set (*import Map*) open Byte_pattern open Byte_sequence open Default_printing open Error open Missing_pervasives open Show open Elf_header open Elf_file open Elf_interpreted_section open Abis open Command_line open Input_list open Linkable_list open Memory_image open Elf_memory_image (* HMM -- ideally we'd be ELF-agnostic in this file. But Abstract_abi is now merged into Elf_memory_image, so never mind. *) open Elf_memory_image_of_elf64_file open Elf_relocation open Elf_symbol_table open Elf_section_header_table open Elf_types_native_uint open Memory_image_orderings (* We model two kinds of linker script: "implicit scripts", which are supplied * on the command line as input objects, and "control scripts" of which there * is exactly one per link job. The abstract syntax of each script comes from the * same grammar. * * We define the control script as a bunch of functions, to allow for * link jobs where we don't have an AST and the script behaviour is hard-coded. *) (* Input sections come from individual (relocatable) ELF files. * The name of this file is important! * * Each input "section" is always an identified section or common symbol * *within* some ELF memory image. *) type input_section_rec = { idx : Nat_big_num.num (* linkable idx *) ; fname : string ; img : elf_memory_image ; shndx : Nat_big_num.num ; secname: string ; isec : elf64_interpreted_section } type input_spec = Common of (Nat_big_num.num * string * elf_memory_image * symbol_definition) (* string is symbol name -- must be a COMMON symbol *) | InputSection of input_section_rec (* A control script defines * - output sections * - a mapping from output sections to (ordered) input sections * - extra symbols * - output format etc. (skip this for now) *) (* We will have to deal with merging etc. at some point, somewhere * (maybe here, maybe not); for now we just produce an ordered list * of sections. *) (* We can't model linker scripts as plain Lem functions without writing * them to a very different structure than that of scripts. The reason is that * certain features of the script language necessitate multiple passes * over the script structure. For example, to figure out how big an * output section is, hence where to begin the next section, you need to * know which of the input sections are marked for KEEP. For that, you need * a def-use graph over input sections. But for that, you also need to account * for *all* symbol definitions, and the script itself is allowed to add new * ones (right in among its input sections). So we have to do one pass to * enumerate the symbol additions, and another pass to eliminate sections * that we don't want to KEEP. * * Other gotchas include: * * - symbol provision and address advancement can occur in among the input * section queries, but also outside any output section. * * - semantics of DATA_SEGMENT_ALIGN depend on future script contents * * - ONLY_IF_RO and ONLY_IF_RW are tricky: need to evaluate the input section * queries * * - semantics of empty sections are subtle (". = ." will force an empty section * to be emitted, but ". = . + 0" will not do so). * * Our approach is to define an interpreter for (at present) most of the script * language. *) type symbol_def_policy = AlwaysDefine | ProvideIfUsed type input_selector = input_spec list -> input_spec list type address_expr = Memory_image.expr type output_guard = AlwaysOutput | OnlyIfRo | OnlyIfRw type symbol_spec = (Nat_big_num.num * Uint32_wrapper.uint32 * Uint32_wrapper.uint32) (* size, info, other *) type retain_policy = DefaultKeep | KeepEvenWhenGC type address_expr_fn_ref = Nat_big_num.num type 'a address_expr_fn_map = (address_expr_fn_ref, (Nat_big_num.num -> 'a -> Nat_big_num.num)) Pmap.map (* 'a = allocated_sections_map *) type output_section_composition_element = IncludeInputSection of (retain_policy * input_section_rec) | IncludeCommonSymbol of (retain_policy * string (* file *) * Nat_big_num.num (* linkable_idx *) * symbol_definition * elf_memory_image) | Hole of address_expr_fn (* compute the next addr to continue layout at *) | ProvideSymbol of (symbol_def_policy * string * symbol_spec) and sort_policy = DefaultSort (* Use command line sort option, else "seen" order *) | SeenOrder (* Always use "seen" order *) | ByName | ByNameThenAlignment | ByAlignment | ByAlignmentThenName | ByInitPriority and (* This mirrors the OutputSection constructor, except that the script elements have become * output_section_composition_elements, and we might store the size here. *) output_section_spec = OutputSectionSpec of (output_guard * Nat_big_num.num option * string * ( output_section_composition_element list)) and allocated_sections_map = AllocatedSectionsMap of (string, (output_section_spec (* OutputSection element idx *) * Nat_big_num.num)) Pmap.map and address_expr_fn = AddressExprFn of address_expr_fn_ref type script_element = DefineSymbol of (symbol_def_policy * string * symbol_spec) | AdvanceAddress of address_expr_fn | MarkAndAlignDataSegment of (Nat_big_num.num * Nat_big_num.num) (* maxpagesize, commonpagesize *) | MarkDataSegmentEnd | MarkDataSegmentRelroEnd (*of (allocated_sections_map -> (natural * (natural -> natural))) DPM: commented out because of positivity constrains in Isabelle *) | OutputSection of (output_guard * ( (* address_expr *) address_expr_fn option) * string * script_element list) | DiscardInput of input_selector (* Input queries can only occur within an output section. Output sections may not nest within other output sections. (Ideally we would use something like polymorphic variants to encode this.) *) | InputQuery of (retain_policy * sort_policy * input_selector) (* A linker control script is a function from inputs to output elements. * We can define them in syntax (using an interpreter) * or in Lem directly (as functions). *) type linker_control_script = script_element list type labelled_linker_control_script = (script_element * Nat_big_num.num) list (*val all_suffixes : list char -> list (list char)*) let rec all_suffixes chars:((char)list)list= ((match chars with [] -> [[]] | c :: morecs -> chars :: (all_suffixes morecs) )) (*val glob_match : list char -> list char -> bool*) let rec glob_match pat str:bool= ((match (pat, str) with ([], []) -> true | ('?':: morepat, _ :: morestr) -> glob_match morepat morestr | ('*':: morepat, _) -> (* if any suffix of the remaining string matches * the remaining pattern, we've matched the pattern * from '*' onwards. *) let or_suffix_match = (fun matched -> (fun newlist -> matched || glob_match morepat newlist)) in List.fold_left (or_suffix_match) false (all_suffixes str) | (patc :: morepat, c :: morestr) -> (patc = c) && glob_match morepat morestr | ([], _) -> (* ran out of pattern *) false | (_, []) -> (* ran out of str *) false )) (*val default_symbol_spec : symbol_spec*) let default_symbol_spec:Nat_big_num.num*Uint32_wrapper.uint32*Uint32_wrapper.uint32= ( (Nat_big_num.of_int 0), Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)), Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) (*val hidden_symbol_spec : symbol_spec*) let :Nat_big_num.num*Uint32_wrapper.uint32*Uint32_wrapper.uint32= ( (Nat_big_num.of_int 0), Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)), Uint32_wrapper.of_bigint stv_hidden) (* These Lem functions replicate linker script functions or builtin behaviours. *) (*val only_sections : input_selector*) let only_sections inputs:(input_spec)list= (Lem_list.mapMaybe (fun i -> (match i with | InputSection(_) -> Some(i) | _ -> None )) inputs) (*val filter_and_concat : (input_spec -> bool) -> input_selector*) (* a.k.a. list input_spec -> list input_spec *) let filter_and_concat p inputs:(input_spec)list= (List.filter p inputs) (*val name_matches : string -> input_spec -> bool*) let name_matches pat input:bool= ((match input with InputSection(inp) -> (*let _ = errln ("Does section name `" ^ inp.secname ^ "' match glob pattern `" ^ pat ^ "'? ") in let result = *)glob_match (Xstring.explode pat) (Xstring.explode inp.secname) (*in let _ = errln (if result then "yes" else "no") in result*) | _ -> false )) (*val file_matches : string -> input_spec -> bool*) let file_matches pat input:bool= ((match input with InputSection(inp) -> glob_match (Xstring.explode pat) (Xstring.explode inp.fname) | _ -> false )) let compareInputSpecByNameThenAlignment i1 i2:int= (let toPair = (fun is -> ((match is with Common(idx1, fname1, img2, def) -> ("COMMON" (* FIXME: is this right? *), Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_value) | InputSection(isrec) -> (isrec.isec.elf64_section_name_as_string, isrec.isec.elf64_section_align) ))) in (pairCompare compare Nat_big_num.compare (toPair i1) (toPair i2))) let compareInputSpecByAlignment i1 i2:int= (let toNatural = (fun is -> ((match is with Common(idx1, fname1, img2, def) -> Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_value | InputSection(isrec) -> isrec.isec.elf64_section_align ))) in Nat_big_num.compare (toNatural i1) (toNatural i2)) let compareInputSpecByName i1 i2:int= (let toString = (fun is -> ((match is with Common(idx1, fname1, img2, def) -> "COMMON" | InputSection(isrec) -> isrec.isec.elf64_section_name_as_string ))) in compare (toString i1) (toString i2)) let compareInputSpecByAlignmentThenName i1 i2:int= (let toPair = (fun is -> ((match is with Common(idx1, fname1, img2, def) -> (Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_value, "COMMON" (* FIXME: is this right? *)) | InputSection(isrec) -> (isrec.isec.elf64_section_align, isrec.isec.elf64_section_name_as_string) ))) in (pairCompare Nat_big_num.compare compare (toPair i1) (toPair i2))) let compareInputSpecByInitPriority i1 i2:int= 0 (* FIXME *) (* DATA_SEGMENT_ALIGN is defined by two formulae * (over pos and commonpagesize/maxpagesize) * "... depending on whether the latter uses fewer COMMONPAGESIZE sized pages for the data segment (area between the result of this expression and `DATA_SEGMENT_END') than the former or not. If the latter form is used, it means COMMONPAGESIZE bytes of runtime memory will be saved at the expense of up to COMMONPAGESIZE wasted bytes in the on-disk file." So the amount of padding that gets inserted here depends on the location of something that comes *later*, namely DATA_SEGMENT_END. So, we can't model it as a function of the current position. Instead, we add MarkDataSegmentEnd and friends to the script_element ADT. *) let has_writability:'a ->input_spec ->bool= (fun writable -> (fun input_sec -> ( (match input_sec with Common(_, _, _, _) -> (* all common symbols are potentially writable *) true | InputSection(inp) -> let (flags : Nat_big_num.num) = ((match elf_memory_image_section_by_index inp.shndx inp.img with Some x -> x.elf64_section_flags | None -> failwith ("impossible: no such section" (*(index " ^ (show inp.shndx) ^ ")""*)) )) in flag_is_set shf_write flags ) ))) (* LARGE_COMMON seems to have been defined in this patch set: https://sourceware.org/ml/binutils/2005-07/txt00014.txt and at the time was "only for x86-64". It seems to be analogous to ".lbss", i.e. "large bss". libbfd defines SHF_X86_64_LARGE. The best comment seems to be in llvm's Support/ELF.h: 0814 // If an object file section does not have this flag set, then it may not hold 0815 // more than 2GB and can be freely referred to in objects using smaller code 0816 // models. Otherwise, only objects using larger code models can refer to them. 0817 // For example, a medium code model object can refer to data in a section that 0818 // sets this flag besides being able to refer to data in a section that does 0819 // not set it; likewise, a small code model object can refer only to code in a 0820 // section that does not set this flag. *) (*val address_zero : natural -> address_expr_fn_map allocated_sections_map -> (natural * address_expr_fn_map allocated_sections_map * address_expr_fn)*) let address_zero fresh alloc_map:Nat_big_num.num*((Nat_big_num.num),(Nat_big_num.num ->allocated_sections_map ->Nat_big_num.num))Pmap.map*address_expr_fn= (let alloc_map' = (Pmap.add fresh (fun pos -> (fun secs -> (Nat_big_num.of_int 0))) alloc_map) in let fresh' = (Nat_big_num.add( (Nat_big_num.of_int 1)) fresh) in (fresh', alloc_map', AddressExprFn fresh)) (* val output_sec_composition_size : list output_section_composition_element -> natural let output_sec_composition_size comp = List.foldl (+) 0 (List.map size_of_output_section_composition_element comp) *) (*val do_output_section_layout_starting_at_addr : natural -> allocated_sections_map -> list output_section_composition_element -> (natural * list natural)*) let do_output_section_layout_starting_at_addr start_addr (AllocatedSectionsMap secs) comps:Nat_big_num.num*(Nat_big_num.num)list= ( (* map out where we plumb in each section, accounting for their alignment *)List.fold_left (fun (next_free_addr, addr_list) -> (fun comp_el -> (match comp_el with IncludeInputSection(retain_pol, irec (* fname, linkable_idx, shndx, isec, img *)) -> let aligned_next_free = (align_up_to irec.isec.elf64_section_align next_free_addr) in (*let _ = errln ("Aligned start address up to 0x" ^ hex_string_of_natural aligned_next_free ^ " (align 0x" ^ (hex_string_of_natural irec.isec.elf64_section_align) ^ ") for included output section `" ^ irec.isec.elf64_section_name_as_string ^ "' from file `" ^ irec.fname ^ "'") in*) ( Nat_big_num.add aligned_next_free irec.isec.elf64_section_size, List.rev_append (List.rev addr_list) [aligned_next_free]) | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> let aligned_next_free = (align_up_to (Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_value) next_free_addr) in ( Nat_big_num.add aligned_next_free (Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_size), List.rev_append (List.rev addr_list) [aligned_next_free]) (*| Hole(AddressExprFn f) -> (f next_free_addr secs, addr_list ++ [next_free_addr])*) | ProvideSymbol(pol, name1, spec) -> (next_free_addr, List.rev_append (List.rev addr_list) [next_free_addr]) ) )) (start_addr, []) comps) (*val output_sec_composition_size_given_start_addr : natural -> allocated_sections_map -> list output_section_composition_element -> natural*) let output_sec_composition_size_given_start_addr start_addr secs comp:Nat_big_num.num= (let (end_addr, comp_addrs) = (do_output_section_layout_starting_at_addr start_addr secs comp) in Nat_big_num.sub_nat end_addr start_addr) (*val sizeof : string -> allocated_sections_map -> natural*) let sizeof secname1 (AllocatedSectionsMap secs):Nat_big_num.num= ((match Pmap.lookup secname1 secs with Some(OutputSectionSpec (_, maybe_addr, _, comp), _) -> (match maybe_addr with Some addr -> output_sec_composition_size_given_start_addr addr (AllocatedSectionsMap secs) comp | None -> failwith ("error: sizeof applied to section without defined start address") ) | None -> failwith ("error: sizeof applied to non-existent section name " ^ secname1) )) (*val alignof_output_section_composition_element : output_section_composition_element -> natural*) let alignof_output_section_composition_element comp:Nat_big_num.num= ((match comp with IncludeInputSection(_, irec) -> irec.isec.elf64_section_align | IncludeCommonSymbol(_, _, _, def, _) -> Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_value | _ -> (Nat_big_num.of_int 1) (* CHECK *) )) (*val alignof_output_section : list output_section_composition_element -> natural*) let alignof_output_section comps:Nat_big_num.num= (let aligns = (Lem_list.map alignof_output_section_composition_element comps) in List.fold_left (fun acc_lcm -> fun next -> lcm acc_lcm next)( (Nat_big_num.of_int 1)) aligns) (*val default_linker_control_script : natural -> address_expr_fn_map allocated_sections_map -> abi any_abi_feature -> maybe natural -> maybe natural -> maybe natural -> natural -> (natural * address_expr_fn_map allocated_sections_map * linker_control_script)*) let default_linker_control_script fresh alloc_map a user_text_segment_start user_data_segment_start user_rodata_segment_start elf_headers_size:Nat_big_num.num*((Nat_big_num.num),(Nat_big_num.num ->allocated_sections_map ->Nat_big_num.num))Pmap.map*(script_element)list= (let segment_start name1 default= ((match name1 with "ldata-segment" -> (match user_data_segment_start with None -> default | Some addr -> (* fun _ -> *) addr ) | "text-segment" -> (match user_text_segment_start with None -> default | Some addr -> (* fun _ -> *) addr ) )) in let is_large_common = (fun inp -> (* FIXME: treat large commons separately *) false ) in let is_common = (fun isec1 -> (match isec1 with Common(idx1, fname1, img2, def) -> (*let _ = errln ("Common or large-common symbol: " ^ def.def_symname) in *) not (is_large_common isec1) | _ -> false )) in let alloc_fn1 = (fun _ -> (fun _ -> Nat_big_num.add (segment_start "text-segment" ( Nat_big_num.mul( (Nat_big_num.of_int 4))( (Nat_big_num.of_int 1048576)))) elf_headers_size)) in let alloc_fn1_ref = fresh in let alloc_map = (Pmap.add alloc_fn1_ref alloc_fn1 alloc_map) in let fresh = (Nat_big_num.add( (Nat_big_num.of_int 1)) fresh) in let alloc_fn2 = (fun addr -> (fun _ -> Nat_big_num.sub_nat (* (align_up_to a.maxpagesize addr) - (natural_land (a.maxpagesize - addr) (a.maxpagesize - 1)) *) (* FIXME: understand the intention of this assignment. Evaluating a simple example of this (from true-static-uClibc) (ALIGN (0x200000) - ((0x200000 - .) & 0x1fffff)) starting from 0x00000000004017dc means 0x600000 - ((0x200000 - 0x4017dc) & 0x1fffff) i.e. 0x600000 - (((-0x2017dc)) & 0x1fffff) i.e. 0x600000 - ( -0x2017dc & 0x1fffff ) which really does come to (according to bash) 0x4017dc i.e. we subtract 0x1fe824 from 0x600000 and end up back where we started. What does ANDing a negative number mean? It doesn't seem to work for us. Well, to take the negation we flip every bit and add one. So if we don't want to do a subtraction that might go negative, we can instead add the complement. *) (align_up_to a.maxpagesize addr) (Nat_big_num.bitwise_and ( Nat_big_num.add a.maxpagesize (compl64 addr)) ( Nat_big_num.sub_nat a.maxpagesize( (Nat_big_num.of_int 1)))))) in let (fresh, alloc_map, (address_zero_fn : address_expr_fn)) = (address_zero fresh alloc_map) in let alloc_fn2_ref = fresh in let alloc_map = (Pmap.add alloc_fn2_ref alloc_fn2 alloc_map) in let fresh = (Nat_big_num.add( (Nat_big_num.of_int 1)) fresh) in let alloc_fn3 = (fun pos -> (fun secs -> align_up_to (if Nat_big_num.equal pos( (Nat_big_num.of_int 0)) then (Nat_big_num.div( (Nat_big_num.of_int 64))( (Nat_big_num.of_int 8))) else (Nat_big_num.of_int 1)) pos)) in let alloc_fn3_ref = fresh in let alloc_map = (Pmap.add alloc_fn3_ref alloc_fn3 alloc_map) in let fresh = (Nat_big_num.add( (Nat_big_num.of_int 1)) fresh) in let alloc_fn4 = (fun pos -> (fun secs -> align_up_to (Nat_big_num.div( (Nat_big_num.of_int 64))( (Nat_big_num.of_int 8))) pos)) in let alloc_fn4_ref = fresh in let alloc_map = (Pmap.add alloc_fn4_ref alloc_fn4 alloc_map) in let fresh = (Nat_big_num.add( (Nat_big_num.of_int 1)) fresh) in let alloc_fn5 = (fun pos -> (fun secs -> segment_start "ldata-segment" pos)) in let alloc_fn5_ref = fresh in let alloc_map = (Pmap.add alloc_fn5_ref alloc_fn5 alloc_map) in let fresh = (Nat_big_num.add( (Nat_big_num.of_int 1)) fresh) in let alloc_fn6 = (fun pos -> fun secs -> align_up_to ( Nat_big_num.add a.maxpagesize ( Nat_big_num.sub_nat(Nat_big_num.bitwise_and pos a.maxpagesize)( (Nat_big_num.of_int 1)))) pos) in let alloc_fn6_ref = fresh in let alloc_map = (Pmap.add alloc_fn6_ref alloc_fn6 alloc_map) in let fresh = (Nat_big_num.add( (Nat_big_num.of_int 1)) fresh) in let alloc_fn7 = (fun pos -> (fun secs -> (if not (Nat_big_num.equal pos( (Nat_big_num.of_int 0))) then Nat_big_num.div( (Nat_big_num.of_int 64))( (Nat_big_num.of_int 8)) else (Nat_big_num.of_int 1)))) in let alloc_fn7_ref = fresh in let alloc_map = (Pmap.add alloc_fn7_ref alloc_fn7 alloc_map) in let fresh = (Nat_big_num.add( (Nat_big_num.of_int 1)) fresh) in let alloc_fn8 = (fun pos -> (fun secs -> align_up_to (Nat_big_num.div( (Nat_big_num.of_int 64))( (Nat_big_num.of_int 8))) pos)) in let alloc_fn8_ref = fresh in let alloc_map = (Pmap.add alloc_fn8_ref alloc_fn8 alloc_map) in let fresh = (Nat_big_num.add( (Nat_big_num.of_int 1)) fresh) in (fresh, alloc_map, [ (* For now, we base our script on the GNU bfd linker's scripts. Here's the static -z combreloc one. /* Script for -z combreloc: combine and sort reloc sections */ /* Copyright (C) 2014 Free Software Foundation, Inc. Copying and distribution of this script, with or without modification, are permitted in any medium without royalty provided the copyright notice and this notice are preserved. */ OUTPUT_FORMAT("elf64-x86-64", "elf64-x86-64", "elf64-x86-64") OUTPUT_ARCH(i386:x86-64) ENTRY(_start) SEARCH_DIR("=/usr/x86_64-linux-gnu/lib64"); SEARCH_DIR("=/usr/local/lib/x86_64-linux-gnu"); SEARCH_DIR("=/usr/local/lib64"); SEARCH_DIR("=/lib/x86_64-linux-gnu"); SEARCH_DIR("=/lib64"); SEARCH_DIR("=/usr/lib/x86_64-linux-gnu"); SEARCH_DIR("=/usr/lib64"); SEARCH_DIR("=/usr/x86_64-linux-gnu/lib"); SEARCH_DIR("=/usr/local/lib"); SEARCH_DIR("=/lib"); SEARCH_DIR("=/usr/lib"); SECTIONS { /* Read-only sections, merged into text segment: */ PROVIDE (__executable_start = SEGMENT_START("text-segment", 0x400000)); . = SEGMENT_START("text-segment", 0x400000) + SIZEOF_HEADERS; .interp : { *(.interp) } .note.gnu.build-id : { *(.note.gnu.build-id) } .hash : { *(.hash) } .gnu.hash : { *(.gnu.hash) } .dynsym : { *(.dynsym) } .dynstr : { *(.dynstr) } .gnu.version : { *(.gnu.version) } .gnu.version_d : { *(.gnu.version_d) } .gnu.version_r : { *(.gnu.version_r) } .rela.dyn : { *(.rela.init) *(.rela.text .rela.text.* .rela.gnu.linkonce.t.* ) *(.rela.fini) *(.rela.rodata .rela.rodata.* .rela.gnu.linkonce.r.* ) *(.rela.data .rela.data.* .rela.gnu.linkonce.d.* ) *(.rela.tdata .rela.tdata.* .rela.gnu.linkonce.td.* ) *(.rela.tbss .rela.tbss.* .rela.gnu.linkonce.tb.* ) *(.rela.ctors) *(.rela.dtors) *(.rela.got) *(.rela.bss .rela.bss.* .rela.gnu.linkonce.b.* ) *(.rela.ldata .rela.ldata.* .rela.gnu.linkonce.l.* ) *(.rela.lbss .rela.lbss.* .rela.gnu.linkonce.lb.* ) *(.rela.lrodata .rela.lrodata.* .rela.gnu.linkonce.lr.* ) *(.rela.ifunc) } .rela.plt : { *(.rela.plt) PROVIDE_HIDDEN (__rela_iplt_start = .); *(.rela.iplt) PROVIDE_HIDDEN (__rela_iplt_end = .); } .init : { KEEP ( *(SORT_NONE(.init))) } .plt : { *(.plt) *(.iplt) } .plt.bnd : { *(.plt.bnd) } .text : { *(.text.unlikely .text.*_unlikely .text.unlikely.* ) *(.text.exit .text.exit.* ) *(.text.startup .text.startup.* ) *(.text.hot .text.hot.* ) *(.text .stub .text.* .gnu.linkonce.t.* ) /* .gnu.warning sections are handled specially by elf32.em. */ *(.gnu.warning) } .fini : { KEEP ( *(SORT_NONE(.fini))) } PROVIDE (__etext = .); PROVIDE (_etext = .); PROVIDE (etext = .); .rodata : { *(.rodata .rodata.* .gnu.linkonce.r.* ) } .rodata1 : { *(.rodata1) } .eh_frame_hdr : { *(.eh_frame_hdr) } .eh_frame : ONLY_IF_RO { KEEP ( *(.eh_frame)) } .gcc_except_table : ONLY_IF_RO { *(.gcc_except_table .gcc_except_table.* ) } /* These sections are generated by the Sun/Oracle C++ compiler. */ .exception_ranges : ONLY_IF_RO { *(.exception_ranges .exception_ranges* ) } /* Adjust the address for the data segment. We want to adjust up to the same address within the page on the next page up. */ . = ALIGN (CONSTANT (MAXPAGESIZE)) - ((CONSTANT (MAXPAGESIZE) - .) & (CONSTANT (MAXPAGESIZE) - 1)); . = DATA_SEGMENT_ALIGN (CONSTANT (MAXPAGESIZE), CONSTANT (COMMONPAGESIZE)); /* Exception handling */ .eh_frame : ONLY_IF_RW { KEEP ( *(.eh_frame)) } .gcc_except_table : ONLY_IF_RW { *(.gcc_except_table .gcc_except_table.* ) } .exception_ranges : ONLY_IF_RW { *(.exception_ranges .exception_ranges* ) } /* Thread Local Storage sections */ .tdata : { *(.tdata .tdata.* .gnu.linkonce.td.* ) } .tbss : { *(.tbss .tbss.* .gnu.linkonce.tb.* ) *(.tcommon) } .preinit_array : { PROVIDE_HIDDEN (__preinit_array_start = .); KEEP ( *(.preinit_array)) PROVIDE_HIDDEN (__preinit_array_end = .); } .init_array : { PROVIDE_HIDDEN (__init_array_start = .); KEEP ( *(SORT_BY_INIT_PRIORITY(.init_array.* ) SORT_BY_INIT_PRIORITY(.ctors.* ))) KEEP ( *(.init_array EXCLUDE_FILE ( *crtbegin.o *crtbegin?.o *crtend.o *crtend?.o ) .ctors)) PROVIDE_HIDDEN (__init_array_end = .); } .fini_array : { PROVIDE_HIDDEN (__fini_array_start = .); KEEP ( *(SORT_BY_INIT_PRIORITY(.fini_array.* ) SORT_BY_INIT_PRIORITY(.dtors.* ))) KEEP ( *(.fini_array EXCLUDE_FILE ( *crtbegin.o *crtbegin?.o *crtend.o *crtend?.o ) .dtors)) PROVIDE_HIDDEN (__fini_array_end = .); } .ctors : { /* gcc uses crtbegin.o to find the start of the constructors, so we make sure it is first. Because this is a wildcard, it doesn't matter if the user does not actually link against crtbegin.o; the linker won't look for a file to match a wildcard. The wildcard also means that it doesn't matter which directory crtbegin.o is in. */ KEEP ( *crtbegin.o(.ctors)) KEEP ( *crtbegin?.o(.ctors)) /* We don't want to include the .ctor section from the crtend.o file until after the sorted ctors. The .ctor section from the crtend file contains the end of ctors marker and it must be last */ KEEP ( *(EXCLUDE_FILE ( *crtend.o *crtend?.o ) .ctors)) KEEP ( *(SORT(.ctors.* ))) KEEP ( *(.ctors)) } .dtors : { KEEP ( *crtbegin.o(.dtors)) KEEP ( *crtbegin?.o(.dtors)) KEEP ( *(EXCLUDE_FILE ( *crtend.o *crtend?.o ) .dtors)) KEEP ( *(SORT(.dtors.* ))) KEEP ( *(.dtors)) } .jcr : { KEEP ( *(.jcr)) } .data.rel.ro : { *(.data.rel.ro.local* .gnu.linkonce.d.rel.ro.local.* ) *(.data.rel.ro .data.rel.ro.* .gnu.linkonce.d.rel.ro.* ) } .dynamic : { *(.dynamic) } .got : { *(.got) *(.igot) } . = DATA_SEGMENT_RELRO_END (SIZEOF (.got.plt) >= 24 ? 24 : 0, .); .got.plt : { *(.got.plt) *(.igot.plt) } .data : { *(.data .data.* .gnu.linkonce.d.* ) SORT(CONSTRUCTORS) } .data1 : { *(.data1) } _edata = .; PROVIDE (edata = .); . = .; __bss_start = .; .bss : { *(.dynbss) *(.bss .bss.* .gnu.linkonce.b.* ) *(COMMON) /* Align here to ensure that the .bss section occupies space up to _end. Align after .bss to ensure correct alignment even if the .bss section disappears because there are no input sections. FIXME: Why do we need it? When there is no .bss section, we don't pad the .data section. */ . = ALIGN(. != 0 ? 64 / 8 : 1); } .lbss : { *(.dynlbss) *(.lbss .lbss.* .gnu.linkonce.lb.* ) *(LARGE_COMMON) } . = ALIGN(64 / 8); . = SEGMENT_START("ldata-segment", .); .lrodata ALIGN(CONSTANT (MAXPAGESIZE)) + (. & (CONSTANT (MAXPAGESIZE) - 1)) : { *(.lrodata .lrodata.* .gnu.linkonce.lr.* ) } .ldata ALIGN(CONSTANT (MAXPAGESIZE)) + (. & (CONSTANT (MAXPAGESIZE) - 1)) : { *(.ldata .ldata.* .gnu.linkonce.l.* ) . = ALIGN(. != 0 ? 64 / 8 : 1); } . = ALIGN(64 / 8); _end = .; PROVIDE (end = .); . = DATA_SEGMENT_END (.); /* Stabs debugging sections. */ .stab 0 : { *(.stab) } .stabstr 0 : { *(.stabstr) } .stab.excl 0 : { *(.stab.excl) } .stab.exclstr 0 : { *(.stab.exclstr) } .stab.index 0 : { *(.stab.index) } .stab.indexstr 0 : { *(.stab.indexstr) } .comment 0 : { *(.comment) } /* DWARF debug sections. Symbols in the DWARF debugging sections are relative to the beginning of the section so we begin them at 0. */ /* DWARF 1 */ .debug 0 : { *(.debug) } .line 0 : { *(.line) } /* GNU DWARF 1 extensions */ .debug_srcinfo 0 : { *(.debug_srcinfo) } .debug_sfnames 0 : { *(.debug_sfnames) } /* DWARF 1.1 and DWARF 2 */ .debug_aranges 0 : { *(.debug_aranges) } .debug_pubnames 0 : { *(.debug_pubnames) } /* DWARF 2 */ .debug_info 0 : { *(.debug_info .gnu.linkonce.wi.* ) } .debug_abbrev 0 : { *(.debug_abbrev) } .debug_line 0 : { *(.debug_line .debug_line.* .debug_line_end ) } .debug_frame 0 : { *(.debug_frame) } .debug_str 0 : { *(.debug_str) } .debug_loc 0 : { *(.debug_loc) } .debug_macinfo 0 : { *(.debug_macinfo) } /* SGI/MIPS DWARF 2 extensions */ .debug_weaknames 0 : { *(.debug_weaknames) } .debug_funcnames 0 : { *(.debug_funcnames) } .debug_typenames 0 : { *(.debug_typenames) } .debug_varnames 0 : { *(.debug_varnames) } /* DWARF 3 */ .debug_pubtypes 0 : { *(.debug_pubtypes) } .debug_ranges 0 : { *(.debug_ranges) } /* DWARF Extension. */ .debug_macro 0 : { *(.debug_macro) } .gnu.attributes 0 : { KEEP ( *(.gnu.attributes)) } /DISCARD/ : { *(.note.GNU-stack) *(.gnu_debuglink) *(.gnu.lto_* ) } } *) (* function from inputs and configuration to output sections-with-address-and-policy, output symbols-with-address-and-attributes, discards, orphans BUT 1. policy is not a property of output sections, but of *inputs within outputs* i.e. KEEP( *(.init)) what's helpful for writing such functions? e.g. only_if_ro (input_query) (output ): i.e. ++ only_if_ro OutputSection(AlwaysOutput, Nothing, ".eh_frame", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".eh_frame"))]) want to take a bunch of outputs and return a bunch of outputs? if so, need to return a "current address" *) (DefineSymbol(ProvideIfUsed, "__executable_start", default_symbol_spec)) ; AdvanceAddress(AddressExprFn alloc_fn1_ref) ; OutputSection(AlwaysOutput, None, ".interp", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".interp"))]) ; OutputSection(AlwaysOutput, None, ".note.gnu.build-id", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".note.gnu.build-id"))]) ; OutputSection(AlwaysOutput, None, ".hash", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".hash"))]) ; OutputSection(AlwaysOutput, None, ".gnu.hash", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".gnu.hash"))]) ; OutputSection(AlwaysOutput, None, ".dynsym", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".dynsym"))]) ; OutputSection(AlwaysOutput, None, ".dynstr", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".dynstr"))]) ; OutputSection(AlwaysOutput, None, ".gnu.version", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".gnu.version"))]) ; OutputSection(AlwaysOutput, None, ".gnu.version_d", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".gnu.version_d"))]) ; OutputSection(AlwaysOutput, None, ".gnu.version_r", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".gnu.version_r"))]) ; OutputSection(AlwaysOutput, None, ".rela.dyn", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".rela.init")) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".rela.text" s || (name_matches ".rela.text.*" s || name_matches ".rela.gnu.linkonce.t.*" s))) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".rela.rodata" s || (name_matches ".rela.rodata.*" s || name_matches ".rela.gnu.linkonce.r.*" s))) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".rela.data" s || (name_matches ".rela.data.*" s || name_matches ".rela.gnu.linkonce.d.*" s))) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".rela.tdata" s || (name_matches ".rela.tdata.*" s || name_matches ".rela.gnu.linkonce.td.*" s))) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".rela.tbss" s || (name_matches ".rela.tbss.*" s || name_matches ".rela.gnu.linkonce.tb.*" s))) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".rela.ctors")) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".rela.got")) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".rela.bss" s || (name_matches ".rela.bss.*" s || name_matches ".rela.gnu.linkonce.b.*" s))) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".rela.ldata" s || (name_matches ".rela.ldata.*" s || name_matches ".rela.gnu.linkonce.l.*" s))) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".rela.lbss" s || (name_matches ".rela.lbss.*" s || name_matches ".rela.gnu.linkonce.lb.*" s))) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".rela.ifunc")) ]) ; OutputSection(AlwaysOutput, None, ".rela.plt", [ InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".rela.plt")) ; DefineSymbol(ProvideIfUsed, "__rela_iplt_start", ( (Nat_big_num.of_int 0), make_symbol_info stb_local stt_notype (* FIXME *), make_symbol_other stv_hidden)) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".rela.iplt")) ; DefineSymbol(ProvideIfUsed, "__rela_iplt_end", ( (Nat_big_num.of_int 0), make_symbol_info stb_local stt_notype (* FIXME *), make_symbol_other stv_hidden)) ]) ; OutputSection(AlwaysOutput, None, ".init", [ InputQuery(KeepEvenWhenGC, SeenOrder, filter_and_concat (name_matches ".init")) ]) ; OutputSection(AlwaysOutput, None, ".plt", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".plt")) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".iplt")) ]) ; OutputSection(AlwaysOutput, None, ".plt.bnd", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".plt.bnd"))]) ; OutputSection(AlwaysOutput, None, ".text", [ InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".text.unlikely" s || (name_matches ".text.*_unlikely" s || name_matches ".text.unlikely.*" s) )) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".text.exit" s || name_matches ".text.exit.*" s)) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".text.startup" s || name_matches ".text.startup.*" s)) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".text.hot" s || name_matches ".text.hot.*" s)) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".text" s || (name_matches ".stub" s || (name_matches ".text.*" s || name_matches ".gnu.linkonce.t.*" s)))) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( (* ".gnu.warning sections are handled specially by elf32.em." * GAH. That means that what we specify here is not (completely) what * needs to happen with these sections. *) fun s -> name_matches ".gnu_warning" s)) ]) ; OutputSection(AlwaysOutput, None, ".fini", [ InputQuery(KeepEvenWhenGC, SeenOrder, filter_and_concat (name_matches ".fini")) ]) ; DefineSymbol(ProvideIfUsed, "__etext", default_symbol_spec) ; DefineSymbol(ProvideIfUsed, "_etext", default_symbol_spec) ; DefineSymbol(ProvideIfUsed, "etext", default_symbol_spec) ; OutputSection(AlwaysOutput, None, ".rodata", [ InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".rodata" s || (name_matches ".rodata.*" s || name_matches ".gnu.linkonce.r.*" s) ))]) ; OutputSection(AlwaysOutput, None, ".eh_frame_hdr", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".eh_frame_hdr")) ]) ; OutputSection(OnlyIfRo, None, ".eh_frame", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".eh_frame"))]) ; OutputSection(OnlyIfRo, None, ".gcc_except_table", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (fun s -> name_matches ".gcc_except_table" s || name_matches ".gcc_except_table.*" s))]) ; OutputSection(OnlyIfRo, None, ".exception_ranges", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (fun s -> name_matches ".exception_ranges" s || name_matches ".exception_ranges*" s))]) ; AdvanceAddress(AddressExprFn alloc_fn2_ref) ; MarkAndAlignDataSegment( Nat_big_num.mul (Nat_big_num.mul((* a.maxpagesize *) (Nat_big_num.of_int 2))( (Nat_big_num.of_int 1024)))( (Nat_big_num.of_int 1024)) (* <-- for some reason binutils assumes 2MB max page size, even if ABI says smaller *), a.commonpagesize) ; OutputSection(OnlyIfRw, None, ".eh_frame", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".eh_frame"))]) ; OutputSection(OnlyIfRw, None, ".gcc_except_table", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (fun s -> name_matches ".gcc_except_table" s || name_matches ".gcc_except_table.*" s))]) ; OutputSection(OnlyIfRw, None, ".exception_ranges", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (fun s -> name_matches ".exception_ranges" s || name_matches ".exception_ranges*" s))]) ; OutputSection(AlwaysOutput, None, ".tdata", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (fun s -> name_matches ".tdata" s || (name_matches ".tdata.*" s || name_matches ".gnu.linkonce.td.*" s)))]) ; OutputSection(AlwaysOutput, None, ".tbss", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (fun s -> name_matches ".tbss" s || (name_matches ".tbss.*" s || name_matches ".gnu.linkonce.tb.*" s))) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".tcommon"))]) ; OutputSection(AlwaysOutput, None, ".preinit_array", [ DefineSymbol(ProvideIfUsed, "__preinit_array_start", default_symbol_spec) ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> name_matches ".preinit_array" s)) ; DefineSymbol(ProvideIfUsed, "__preinit_array_end", default_symbol_spec) ]) ; OutputSection(AlwaysOutput, None, ".init_array", [ DefineSymbol(ProvideIfUsed, "__init_array_start", default_symbol_spec) ; InputQuery(KeepEvenWhenGC, ByInitPriority, filter_and_concat (fun s -> name_matches ".init_array.*" s)) ; InputQuery(KeepEvenWhenGC, ByInitPriority, filter_and_concat (fun s -> name_matches ".ctors.*" s)) ; InputQuery(KeepEvenWhenGC, ByInitPriority, filter_and_concat (fun s -> name_matches ".init_array" s || (name_matches ".ctors" s && not (file_matches "*crtbegin.o" s || (file_matches "*crtbegin?.o" s || (file_matches "*crtend.o" s || file_matches "*crtend?.o " s))))) ) ; DefineSymbol(ProvideIfUsed, "__init_array_end", default_symbol_spec) ]) ; OutputSection(AlwaysOutput, None, ".fini_array", [ DefineSymbol(ProvideIfUsed, "__fini_array_start", default_symbol_spec) ; InputQuery(KeepEvenWhenGC, ByInitPriority, filter_and_concat (fun s -> name_matches ".fini_array.*" s)) ; InputQuery(KeepEvenWhenGC, ByInitPriority, filter_and_concat (fun s -> name_matches ".dtors.*" s)) ; InputQuery(KeepEvenWhenGC, ByInitPriority, filter_and_concat (fun s -> name_matches ".fini_array" s || (name_matches ".dtors" s && not (file_matches "*crtbegin.o" s || (file_matches "*crtbegin?.o" s || (file_matches "*crtend.o" s || file_matches "*crtend?.o " s))))) ) ; DefineSymbol(ProvideIfUsed, "__fini_array_end", default_symbol_spec) ]) ; OutputSection(AlwaysOutput, None, ".ctors", [ InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> file_matches "*crtbegin.o" s && name_matches ".ctors" s)) ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> file_matches "*crtbegin?.o" s && name_matches ".ctors" s)) ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> not (file_matches "*crtend.o" s || file_matches "*crtend?.o" s) && name_matches ".ctors" s)) ; InputQuery(KeepEvenWhenGC, ByName, filter_and_concat (fun s -> name_matches ".ctors.*" s)) ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> (file_matches "*crtend.o" s || file_matches "*crtend?.o" s) && name_matches ".ctors" s)) (* NOTE: this exclusion is implicit in the usual linker script, * because it won't match an input section more than once. We should * just replicate this behaviour, since other parts of the script might rely on it * less obviously. *) ]) ; OutputSection(AlwaysOutput, None, ".dtors", [ InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> file_matches "*crtbegin.o" s && name_matches ".dtors" s)) ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> file_matches "*crtbegin?.o" s && name_matches ".dtors" s)) ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> not (file_matches "*crtend.o" s || file_matches "*crtend?.o" s) && name_matches ".dtors" s)) ; InputQuery(KeepEvenWhenGC, ByName, filter_and_concat (fun s -> name_matches ".dtors.*" s)) ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> (file_matches "*crtend.o" s || file_matches "*crtend?.o" s) && name_matches ".dtors" s)) ]) ; OutputSection(AlwaysOutput, None, ".jcr", [InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (name_matches ".jcr"))]) ; OutputSection(AlwaysOutput, None, ".data.rel.ro", [ InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".data.rel.ro.local*" s || name_matches ".gnu.linkonce.d.rel.ro.local.*" s )); InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".data.rel.ro" s || (name_matches ".data.rel.ro.*" s || name_matches ".gnu.linkonce.d.rel.ro.*" s) )) ]) ; OutputSection(AlwaysOutput, None, ".dynamic", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".dynamic"))]) ; OutputSection(AlwaysOutput, None, ".got", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".got")) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".igot")) ]) ; MarkDataSegmentRelroEnd (*(fun secs -> (if (sizeof ".got.plt" secs) >= 24 then 24 else 0, (fun pos -> pos)))*) ; OutputSection(AlwaysOutput, None, ".got.plt", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".got.plt")) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".igot.plt")) ]) ; OutputSection(AlwaysOutput, None, ".data", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".data" s || (name_matches ".data.*" s || name_matches ".gnu.linkonce.d.*" s))) (* the script also has SORT(CONSTRUCTORS) here, but it has no effect for ELF (I think) *) ]) ; OutputSection(AlwaysOutput, None, ".data1", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".data1"))]) ; DefineSymbol(AlwaysDefine, "_edata", default_symbol_spec) ; DefineSymbol(ProvideIfUsed, "edata", default_symbol_spec) ; (* . = .; <-- does this do anything? YES! It forces an output section to be emitted. Since it occurs *outside* any output section, it is assumed to start *) DefineSymbol(AlwaysDefine, "__bss_start", default_symbol_spec) ; OutputSection(AlwaysOutput, None, ".bss", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".dynbss")) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".bss" s || (name_matches ".bss.*" s || name_matches ".gnu.linkonce.b.*" s))) ; InputQuery(DefaultKeep, DefaultSort, (fun inputlist -> (*let _ = errln "Looking for commons" in *) let result = (filter_and_concat is_common inputlist) in (*let _ = errln ("Got " ^ (show (length (result))) ^ " commons; sanity check: input list contains " ^ (show (length inputlist)) ^ " of which " ^ (show (length (List.filter (fun inp -> match inp with Common _ -> true | _ -> false end) inputlist))) ^ " are commons." ) in*) result) ) ]) ; AdvanceAddress(AddressExprFn alloc_fn3_ref) ; OutputSection(AlwaysOutput, None, ".lbss", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".dynlbss")) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".dynlbss")) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".lbss" s || (name_matches ".lbss.*" s || name_matches ".gnu.linkonce.lb.*" s) )) ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (is_large_common)) ]) ; AdvanceAddress(AddressExprFn alloc_fn4_ref) ; AdvanceAddress(AddressExprFn alloc_fn5_ref) ; OutputSection(AlwaysOutput, Some (AddressExprFn alloc_fn6_ref), ".lrodata", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".lrodata" s || (name_matches ".lrodata.*" s || name_matches ".gnu.linkonce.lr.*" s) )) ; AdvanceAddress(AddressExprFn alloc_fn7_ref) ]) ; AdvanceAddress(AddressExprFn alloc_fn8_ref) ; DefineSymbol(AlwaysDefine, "_end", default_symbol_spec) ; DefineSymbol(ProvideIfUsed, "end", default_symbol_spec) ; MarkDataSegmentEnd ; OutputSection(AlwaysOutput, Some address_zero_fn, ".stab", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".stab"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".stabstr", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".stabstr"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".stab.excl", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".stab.excl"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".stab.exclstr", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".stab.exclstr"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".stab.index", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".stab.index"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".stab.indexstr", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".stab.indexstr"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".comment", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".comment"))]) (* DWARF debug sections. Symbols in the DWARF debugging sections are relative to the beginning of the section so we begin them at 0. *) (* DWARF 1 *) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".line", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".line"))]) (* GNU DWARF 1 extensions *) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_srcinfo", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_srcinfo"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_sfnames", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_sfname"))]) (* DWARF 1.1 and DWARF 2 *) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_aranges", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_aranges"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_pubnames", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_pubnames"))]) (* DWARF 2 *) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_info", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".debug_info" s || name_matches ".gnu.linkonce.wi.*" s))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_abbrev", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_abbrev"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_line", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( fun s -> name_matches ".debug_line" s || (name_matches ".debug_line.*" s || name_matches ".debug_line_end" s)))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_frame", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_frame"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_str", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_str"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_loc", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_loc"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_macinfo", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_macinfo"))]) (* SGI/MIPS DWARF 2 extensions *) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_weaknames", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_weaknames"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_funcnames", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_funcnames"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_typenames", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_typenames"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_varnames", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_varnames"))]) (* DWARF 3 *) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_pubtypes", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_pubtypes"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_ranges", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_ranges"))]) (* DWARF Extension. *) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_macro", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_macro"))]) ; OutputSection(AlwaysOutput, Some address_zero_fn, ".gnu.attributes", [InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (name_matches ".gnu.attributes"))]) ; DiscardInput(filter_and_concat (fun s -> name_matches ".note.GNU-stack" s || (name_matches ".gnu_debuglink" s || name_matches ".gnu.lto_*" s))) (* NOTE: orphan sections are dealt with in the core linking logic, not the script. *) ])) let interpret_guard guard comp name1:bool= ((match guard with always0 -> true | OnlyIfRo -> let v = (List.for_all (fun comp_el -> (match comp_el with IncludeInputSection(retainpol, (* fname, linkable_idx, shndx, isec, img *) irec) -> Nat_big_num.equal( (* is this section read-only? if it doesn't have shf_write, yes *) (Nat_big_num.of_int 0)) (Nat_big_num.bitwise_and irec.isec.elf64_section_flags shf_write) | _ -> (* holes, common symbols and provided symbols shouldn't prevent ONLY_IF_RO *) true )) comp) in (*let _ = errln ("only_if_ro evaluated " ^ (show v) ^ " for output section " ^ name) in*) v | OnlyIfRw -> let v = (List.for_all (fun comp_el -> (match comp_el with IncludeInputSection(retainpol, (* fname, linkable_idx, shndx, isec, img *) irec) -> not (Nat_big_num.equal( (* is this section read-only? if it doesn't have shf_write, yes *) (Nat_big_num.of_int 0)) (Nat_big_num.bitwise_and irec.isec.elf64_section_flags shf_write)) | _ -> (* holes etc. shouldn't prevent ONLY_IF_RW *) true )) comp) in (*let _ = errln ("only_if_rw evaluated " ^ (show v) ^ " for output section " ^ name) in *)v )) (* Passes over the script: * * 1. assign input sections to output sections (or discard) and define symbols. * * 2. compute def-use and optionally GC, removing unwanted sections and symbols * * 3. build image, assigning addresses as we go. * * Some passes require matching/retrieving what a previous pass on the same node did. * So we give each script element a natural "idx" label. *) (*val label_script_aux : natural -> linker_control_script -> labelled_linker_control_script*) let label_script_aux start script1:(script_element*Nat_big_num.num)list= (mapi (fun i -> fun el -> (el, ( Nat_big_num.add start (Nat_big_num.of_int i)))) script1) (*val label_script : linker_control_script -> labelled_linker_control_script*) let label_script script1:(script_element*Nat_big_num.num)list= (label_script_aux( (Nat_big_num.of_int 0)) script1) type input_output_assignment = ( input_spec list * (output_section_spec * Nat_big_num.num) list) (*val assign_inputs_to_output_sections : input_output_assignment -> (* accumulator: list of discards, list of output compositions (these include symbols) *) set (natural * natural) -> (* used sections *) set (natural * natural * natural) -> (* used commons *) list input_spec -> (* remaining inputs *) maybe (output_section_spec * natural) -> (* cur_sec -- the current output section spec and its OutputSection script item idx *) maybe input_spec -> (* last input section to be output -- might not have one *) (input_spec -> input_spec -> Basic_classes.ordering) (* "seen ordering" *) -> labelled_linker_control_script -> input_output_assignment*) (* accumulated result *) let rec assign_inputs_to_output_sections acc used_sections used_commons inputs (cur_output_sec : (output_section_spec * Nat_big_num.num)option) last_input_sec seen_ordering script1:(input_spec)list*(output_section_spec*Nat_big_num.num)list= (let (rev_discards, rev_outputs) = acc in let flush_output_sec = (fun maybe_output_sec_and_idx -> (match (maybe_output_sec_and_idx : (output_section_spec * Nat_big_num.num)option) with Some (OutputSectionSpec (guard, addr, name1, comp), script_idx) -> (*let _ = errln ("Guardedly flushing output section named " ^ name ^ " with " ^ ( match addr with Nothing -> "no address yet" | Just a -> "address 0x" ^ (hex_string_of_natural a) end ) ^ " and composed of " ^ (show (length comp)) ^ " constituents.") in*) (* evaluate the guard *) if interpret_guard guard comp name1 then (* do it *) (rev_discards, (((OutputSectionSpec (guard, addr, name1, comp)), script_idx) :: rev_outputs)) else (* ignore it *) acc | None -> (* for convenience, make this a no-op rather than error *) (* failwith "internal error: flushing output section with no current output section" *) acc )) in (match script1 with [] -> flush_output_sec cur_output_sec | (element1, idx1) :: more_elements_and_idx -> let do_nothing = (acc, used_sections, used_commons, cur_output_sec, last_input_sec) in let (new_acc, new_used_sections, new_used_commons, (new_cur_output_sec : (output_section_spec * Nat_big_num.num)option), new_last_input_sec) = ((match element1 with DefineSymbol(symdefpol, name1, (symsize, syminfo, symother)) -> (* Label the current section in the image * with a new symbol definition. If there isn't * a current section, use the ABS section (what is that labelling?). *) (acc, used_sections, used_commons, (match (cur_output_sec : (output_section_spec * Nat_big_num.num)option) with None -> (*let _ = errln ("FIXME: for defining `" ^ name ^ "': ABS symbol defs not yet supported") in*) None | Some ((OutputSectionSpec (guard, maybe_addr, secname1, comp)), output_script_idx) -> (*let _ = errln ("Including a symbol named `" ^ name ^ " in composition of output section `" ^ secname ^ "'") in*) Some ((OutputSectionSpec (guard, maybe_addr, secname1, List.rev_append (List.rev comp) [ProvideSymbol(symdefpol, name1, (symsize, syminfo, symother))])) , output_script_idx) ), last_input_sec) | AdvanceAddress(AddressExprFn advance_fn) -> (* If we're inside a section, insert a hole, * else just update the logical address *) (*let _ = errln ("Advancing location counter") in*) (match cur_output_sec with None -> do_nothing (* This assignment is setting a new LMA. *) (* (acc, *) | Some (sec, idx1) -> do_nothing ) | MarkAndAlignDataSegment(maxpagesize1, commonpagesize1) -> (* The "data segment end" is a distinguished label, * so we can encode the whole thing into a conditional. *) (*let _ = errln ("Mark/aligning data segment") in*) do_nothing | MarkDataSegmentEnd -> (*let _ = errln ("Marking data segment end") in*) do_nothing | MarkDataSegmentRelroEnd(*(fun_from_secs_to_something)*) -> (*let _ = errln ("Marking data segment relro end") in*) do_nothing | OutputSection(outputguard, maybe_expr, name1, sub_elements) -> (* If we have a current output section, finish it and add it to the image. * Q. Where do guards ("ONLY_IF_RO" etc) get evaluated? * A. Inside flush_output_sec. *) (*let _ = errln ("Recursively composing a new output section `" ^ name ^ "'...") in*) let acc_with_output_sec = (flush_output_sec cur_output_sec) in let new_cur_output_sec = (Some((OutputSectionSpec(outputguard, (* maybe_expr pos secs *) None, name1, [])), idx1)) in (* Recurse down the list of input queries, assigning them to this output sec * Note that output sections may not nest within other output sections. * At the end of the list of sub_elements, we will flush the section we built up. *) let final_acc = (assign_inputs_to_output_sections acc used_sections used_commons inputs new_cur_output_sec last_input_sec seen_ordering (label_script sub_elements)) in (* NOTE that this sub-accumulation will never add a new output section * because output sections can't nest. *) (final_acc, used_sections, used_commons, (* cur_output_sec *) None, last_input_sec) | DiscardInput(selector) -> let selected = (selector inputs) in let (rev_discards, rev_outputs) = acc in (*let _ = Missing_pervasives.errln ("Processing discard rule; selected " ^ (show (length selected)) ^ " inputs.") in*) (( List.rev_append (List.rev (List.rev (let x2 = ([]) in List.fold_right (fun i x2 -> if true then i :: x2 else x2) selected x2))) rev_discards, rev_outputs), used_sections, used_commons, cur_output_sec, last_input_sec) | InputQuery(retainpol, sortpol, selector) -> (* Input queries can only occur within an output section. *) (match cur_output_sec with None -> failwith "linker script error: input query without output section" | Some ((OutputSectionSpec (output_guard1, output_sec_addr, output_sec_name, output_composition)), output_script_idx) -> (* Add them to the current output spec. We have to be careful about ordering: * according to the GNU ld manual (and observed behaviour), by default * "the linker will place files and sections matched by wildcards in the order * in which they are seen during the link". For .o files on the command line, * this means the command line order. But for members of archives, it means * the order in which they were "pulled in" during input enumeration. We * actually don't compute this here; it is passed in from our caller in link.lem. *) let sortfun = ((match sortpol with DefaultSort -> List.sort seen_ordering (* FIXME: pay attention to command line *) | SeenOrder -> List.sort seen_ordering | ByName -> List.sort compareInputSpecByName | ByNameThenAlignment -> List.sort compareInputSpecByNameThenAlignment | ByAlignment -> List.sort compareInputSpecByAlignment | ByAlignmentThenName -> List.sort compareInputSpecByAlignmentThenName | ByInitPriority -> List.sort compareInputSpecByInitPriority )) in let selected = (selector inputs) in let selected_deduplicated = (List.filter (fun inp -> (match inp with InputSection(irec) -> not ( Pset.mem(irec.idx, irec.shndx) used_sections) | Common(idx1, fname1, img2, def) -> not ( Pset.mem(idx1, def.def_sym_scn, def.def_sym_idx) used_commons) )) selected) in (*let _ = errln ("Evaluated an input query, yielding " ^ (show (length selected)) ^ " undeduplicated and " ^ (show (length selected_deduplicated)) ^ " deduplicated results, to be added to composition currently of " ^ (show (length output_composition)) ^ " items.") in*) (* Search input memory images for matching sections. *) let sorted_selected_inputs = (sortfun selected_deduplicated) in let (sectionMatchList : input_section_rec list) = (Lem_list.mapMaybe (fun inp -> (match inp with InputSection(x) -> (*let _ = errln ("Matched an input section named " ^ x.isec.elf64_section_name_as_string ^ " in a file " ^ x.fname ^ " with first 20 bytes " ^ (show (take 20 (let maybe_elname = elf_memory_image_element_coextensive_with_section x.shndx x.img in match maybe_elname with Nothing -> failwith ("impossible: no such element (matching shndx " ^ (show x.shndx) ^ ")") | Just idstr -> match Map.lookup idstr x.img.elements with Just el -> el.contents | Nothing -> failwith "no such element" end end )))) in*) Some x | _ -> None )) sorted_selected_inputs) in let commonMatchList = (Lem_list.mapMaybe (fun inp -> (match inp with | Common(idx1, fname1, img2, def) -> Some(idx1, fname1, img2, def) | _ -> None )) sorted_selected_inputs) in (acc, Pset.(union) used_sections (let x2 =(Pset.from_list (pairCompare Nat_big_num.compare Nat_big_num.compare) []) in List.fold_right (fun irec x2 -> if true then Pset.add (irec.idx, irec.shndx) x2 else x2) sectionMatchList x2), Pset.(union) used_commons (let x2 =(Pset.from_list (tripleCompare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare) []) in List.fold_right (fun(idx1, fname1, img2, def) x2 -> if true then Pset.add (idx1, def.def_sym_scn, def.def_sym_idx) x2 else x2) commonMatchList x2), (* new_cur_output_spec *) Some ( (OutputSectionSpec(output_guard1, output_sec_addr, output_sec_name, List.rev_append (List.rev (List.rev_append (List.rev output_composition) (let x2 = ([]) in List.fold_right (fun input_sec x2 -> if true then IncludeInputSection (retainpol, (* input_sec.fname, input_sec.idx, input_sec.shndx, input_sec.isec, input_sec.img *) input_sec) :: x2 else x2) sectionMatchList x2))) (let x2 = ([]) in List.fold_right (fun(idx1, fname1, img2, def) x2 -> if true then IncludeCommonSymbol (DefaultKeep, fname1, idx1, def, img2) :: x2 else x2) commonMatchList x2) )), output_script_idx), last_input_sec ) ) )) in (*let _ = match new_cur_output_sec with Just (OutputSectionSpec (guard, addr, name, comp), script_idx) -> errln ("Now output section `" ^ name ^ "' is composed of " ^ (show (length comp)) ^ " elements.") | Nothing -> () end in*) assign_inputs_to_output_sections new_acc new_used_sections new_used_commons (inputs : input_spec list) (new_cur_output_sec) (new_last_input_sec : input_spec option) seen_ordering (more_elements_and_idx : labelled_linker_control_script) )) (* NOTE: this is also responsible for deleting any PROVIDEd symbols that * were not actually referenced. BUT HOW, if we haven't built the image and * hence haven't added the symbols yet? Symbols affect reachability, so * we're going to have to figure this out. Really we want a memory image that * does not yet have addresses assigned, but does have the symbols inserted. * BUT even that is not right, because we want to be able to remove some * sections (GC them). So the section composition is not yet fixed. So we have * a problem. * * Note that the only symbols we have to remove are ones that were PROVIDEd * in our output composition. So doing the GC on output compositions seems * sane. We can get the graph's edge list by inspecting the constituent memory * images from which each output section composition element is drawn. * Collecting sections and collecting symbols seems fair. Note that symbols * can never be placed mid-section (I don't think?? they can use arbitrary * expressions, but not that depend on whether an input section is included * or not) so removing a section should never imply the removal of a symbol. * * So that implies we need not yet build a memory image. *) (*val compute_def_use_and_gc : allocated_sections_map -> allocated_sections_map*) let compute_def_use_and_gc outputs_by_name:allocated_sections_map= outputs_by_name (* FIXME: implement GC *) let output_section_type comp:Nat_big_num.num= ( (* are we composed entirely of nobits sections and common symbols? *)let all_nobits = (List.for_all (fun comp_el -> (match comp_el with IncludeInputSection(retain_pol,(* fname, linkable_idx, shndx, isec, img *) irec) -> Nat_big_num.equal irec.isec.elf64_section_type sht_nobits | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> true | _ -> (* padding and symdefs can be nobits *) true )) comp) in if all_nobits then sht_nobits else sht_progbits) let output_section_flags comp:Nat_big_num.num= (let writable = (List.exists (fun comp_el -> (match comp_el with IncludeInputSection(retain_pol, (* fname, linkable_idx, shndx, isec, img *) irec) -> flag_is_set shf_write irec.isec.elf64_section_flags | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> (* assume common symbols are writable *) true | _ -> (* padding and symdefs do not make a section writable *) false )) comp) in let executable = (List.exists (fun comp_el -> (match comp_el with IncludeInputSection(retain_pol,(* fname, linkable_idx, shndx, isec, img *) irec) -> flag_is_set shf_execinstr irec.isec.elf64_section_flags | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> (* assume common symbols are not executable, since they're zeroed *) false | _ -> (* padding and symdefs do not make a section executable -- HMM *) false )) comp) in let alloc = (List.exists (fun comp_el -> (match comp_el with IncludeInputSection(retain_pol, (* fname, linkable_idx, shndx, isec, img *) irec) -> flag_is_set shf_alloc irec.isec.elf64_section_flags | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> (* common symbols are allocatable *) true | ProvideSymbol(pol, name1, spec) -> (* symbols make a section allocatable? HMM *) true | _ -> (* padding does not make a section allocatable *) false )) comp) in let is_thread_local_yesnomaybe = (fun comp_el -> (match comp_el with IncludeInputSection(retain_pol, (* fname, linkable_idx, shndx, isec, img *) irec) -> Some(flag_is_set shf_tls irec.isec.elf64_section_flags) | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> (* FIXME: support tcommon *) Some(false) | ProvideSymbol(pol, name1, spec) -> (* linker script symbols shouldn't be defined here, unless they can be declared thread-local (FIXME: can they?) *) Some false | _ -> (* padding does not make a section thread-local, or non-. *) None ) ) in let thread_local = ( (* Is any element positively thread-local? *) let v = (List.fold_left (fun acc_ynm -> fun comp_el -> let new_ynm = (is_thread_local_yesnomaybe comp_el) in (match (acc_ynm, new_ynm) with (None, None) -> None | (None, Some x) -> Some x | (Some x, None) -> Some x | (Some true, Some false) -> Some true | (Some true, Some true) -> Some true | (Some false, Some false) -> Some false | (Some true, Some false) -> Some true )) None comp) in if (Lem.option_equal (=) v (Some(true))) && not ( (Lem.option_equal (=)(Some(true)) (* are *all* either don't-care or positively thread-local? *) (List.fold_left (fun acc_ynm -> fun comp_el -> let new_ynm = (is_thread_local_yesnomaybe comp_el) in (match (acc_ynm, new_ynm) with (None, None) -> None | (None, Some x) -> Some x | (Some x, None) -> Some x | (Some true, Some false) -> Some false | (Some true, Some true) -> Some true | (Some false, Some false) -> Some false | (Some true, Some false) -> Some false )) None comp))) then failwith "error: section mixes thread-local and non-thread-local inputs" else (match v with None -> false | Some x -> x ) ) in Nat_big_num.bitwise_or (if thread_local then shf_tls else (Nat_big_num.of_int 0)) (Nat_big_num.bitwise_or (if executable then shf_execinstr else (Nat_big_num.of_int 0)) (Nat_big_num.bitwise_or (if writable then shf_write else (Nat_big_num.of_int 0)) (if alloc then shf_alloc else (Nat_big_num.of_int 0)) ) )) let symbol_def_for_provide_symbol name1 size2 info other control_script_linkable_idx:symbol_definition= ({ def_symname = (*let _ = errln ("Linker script is defining symbol called `" ^ name ^ "'") in*) name1 ; def_syment = ({ elf64_st_name = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) (* ignored *) ; elf64_st_info = info ; elf64_st_other = other ; elf64_st_shndx = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf64_st_value = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))) (* ignored *) ; elf64_st_size = (Uint64_wrapper.of_bigint size2) }) ; def_sym_scn =( (Nat_big_num.of_int 0)) ; def_sym_idx =( (Nat_big_num.of_int 0)) ; def_linkable_idx = control_script_linkable_idx }) (*val assign_dot_to_itself : natural -> address_expr_fn_map allocated_sections_map -> (natural * address_expr_fn_map allocated_sections_map * address_expr_fn)*) let assign_dot_to_itself fresh alloc_map:Nat_big_num.num*((Nat_big_num.num),(Nat_big_num.num ->allocated_sections_map ->Nat_big_num.num))Pmap.map*address_expr_fn= (let fn = (fun dot -> fun _ -> dot) in let alloc_map' = (Pmap.add fresh fn alloc_map) in let fresh' = (Nat_big_num.add( (Nat_big_num.of_int 1)) fresh) in (fresh', alloc_map', AddressExprFn fresh)) (*val build_image : abi any_abi_feature -> address_expr_fn_map allocated_sections_map -> (* global dictionary of address_expr_fn_ref -> address_expr_fn *) elf_memory_image -> (* accumulator *) natural -> (* location counter *) allocated_sections_map -> (* outputs constructed earlier *) (Map.map string (list (natural * binding))) -> (* bindings_by_name *) labelled_linker_control_script -> natural -> (* control_script_linkable_idx *) (Map.map string (list symbol_definition)) -> (* linker_defs_by_name *) (elf_memory_image * allocated_sections_map)*) (* accumulated result *) let rec build_image a alloc_map acc pos (AllocatedSectionsMap outputs_by_name) bindings_by_name script1 control_script_linkable_idx linker_defs_by_name:(any_abi_feature)annotated_memory_image*allocated_sections_map= (let (add_output_section : (Nat_big_num.num * elf_memory_image) -> output_section_spec -> (Nat_big_num.num * elf_memory_image * Nat_big_num.num * output_section_spec)) = (fun ((*scn_idx, *)pos, acc_img) -> (fun (OutputSectionSpec (guard, addr, secname1, comp)) -> (*let _ = errln ("Computing composition of output section `" ^ secname ^ "' from " ^ (show (length comp)) ^ " elements") in*) let unaligned_start_addr = ((match addr with Some a -> failwith ("internal error: section " ^ (secname1 ^ ": did not expect address to be assigned yet")) | None -> pos )) in let align = (alignof_output_section comp) in (*let _ = errln ("Aligning start of output section " ^ secname ^ " up to a " ^ (show align) ^ "-byte address boundary") in*) let output_section_start_addr = (align_up_to align unaligned_start_addr) in let (end_addr, comp_addrs) = (do_output_section_layout_starting_at_addr output_section_start_addr (AllocatedSectionsMap outputs_by_name) comp) in let size2 = (Nat_big_num.sub_nat end_addr output_section_start_addr) in (*let _ = Missing_pervasives.outln ( if List.null comp then secname else ( ((space_padded_and_maybe_newline 16 secname) ^ ("0x" ^ (left_zero_padded_to 16 (hex_string_of_natural output_section_start_addr))) ^ " " ^ (left_space_padded_to 10 ("0x" ^ (hex_string_of_natural size)))) ) ) in*) let (concatenated_content, final_addr, new_range_tag_pairs) = (List.fold_left (fun (accum_pat, accum_current_addr, accum_meta) -> (fun (comp_el, comp_addr) -> (*let _ = errln ("Adding an element to composition of output section `" ^ secname ^ "', current address 0x" ^ (hex_string_of_natural accum_current_addr)) in*) let make_line = (fun namestr -> (fun addrstr -> (fun szstr -> (fun rhs -> ( (space_padded_and_maybe_newline( (Nat_big_num.of_int 16)) (" " ^ namestr)) ^ (("0x" ^ (left_zero_padded_to( (Nat_big_num.of_int 16)) addrstr)) ^ (" " ^ ((left_space_padded_to( (Nat_big_num.of_int 10)) ("0x" ^ szstr)) ^ (" " ^ rhs)))) ))))) in let (sz, comp_el_pat, this_el_meta) = ((match comp_el with | IncludeInputSection(retainpolicy, (* fname, linkable_idx, shndx, isec, img *) irec) -> (* We want to get the input section as a byte pattern *) (*let _ = errln ("Processing inclusion of input section `" ^ irec.isec.elf64_section_name_as_string ^ "' from file `" ^ irec.fname ^ "' into output section `" ^ secname ^ "'") in*) let maybe_secname = (elf_memory_image_element_coextensive_with_section irec.shndx irec.img) in (match maybe_secname with None -> failwith ("impossible: no such section" (*(matching irec.shndx " ^ (show irec.shndx) ^ ")""*)) | Some idstr -> (*let _ = errln ("Found element named " ^ idstr ^ " coextensive with section named " ^ irec.isec.elf64_section_name_as_string ^ " in file " ^ irec.fname) in*) (match Pmap.lookup idstr irec.img.elements with Some el -> (*let _ = Missing_pervasives.outln (make_line irec.isec.elf64_section_name_as_string (hex_string_of_natural comp_addr) (hex_string_of_natural irec.isec.elf64_section_size) irec.fname) in*) let section_el_name = (get_unique_name_for_section_from_index irec.shndx irec.isec irec.img) in (*let _ = errln ("Copying metadata for output section `" ^ section_el_name ^ "'") in*) let range_or_sym_is_in_this_sec = (fun maybe_range -> (fun tag -> (* is it within the section we're outputting? * first we needs its element name. *) (* filter out ones that don't overlap *) (match maybe_range with Some(el_name, (start, len)) -> (* img and shndx came as a unit, so they're definitely * talking about the same file *) (* shndx = sym_shndx *) section_el_name = el_name | None -> (* ABS symbols have this property *) (match tag with SymbolDef(def) -> (* don't match section symbols, or we'll be inundated *) let sym_shndx = (Uint32_wrapper.to_bigint def.def_syment.elf64_st_shndx) in if not (Nat_big_num.equal sym_shndx shn_abs) || ( not (Nat_big_num.equal (get_elf64_symbol_type def.def_syment) stt_section)) then false else ( let abs_address = (Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_value) in (* check it against our section *) let section_end_addr = (Nat_big_num.add accum_current_addr irec.isec.elf64_section_size) in ( Nat_big_num.greater_equal abs_address accum_current_addr && Nat_big_num.less abs_address section_end_addr) (* FIXME: argument that this should be <=, i.e. can mark end addr *) (* PROBLEM: this is all very well, but there's no reason why * ABS symbols need to point at an address within some output * section. They can just be arbitrary values. This is a bit of an * abuse if we do it within the C language (to get the value, you * have to do "(int) &sym", i.e. create a meaningless pointer * intermediate) but arguably is okay in an impl-def way. * * WHAT to do? well, just always output the ABS symbols, for now. * * The example that provoked this is in glibc's * locale/lc-address.c, which compiles down to create * the following ABS symbol: * * 0000000000000001 g *ABS* 0000000000000000 _nl_current_LC_ADDRESS_used * * ... i.e. the _nl_current_LC_ADDRESS_used appears to be just a flag. * * Where can we handle this? We don't see ABS symbols since they * aren't associated with sections. We simply need to copy over * all the ABS symbols appearing in included input objects. * That means there's no point doing anything with them here * while we're fiddling with sections. Do it later in a whole- * -image pass. *) && false (* ... at least until we see a better way *) ) | _ -> false ) ) )) in let = (let x2 = ([]) in List.fold_right (fun(maybe_range, tag) x2 -> if range_or_sym_is_in_this_sec maybe_range tag then (maybe_range, tag) :: x2 else x2) (Pset.elements irec.img.by_range) x2) in let included_defs = (let x2 = ([]) in List.fold_right (fun(maybe_range, def) x2 -> if range_or_sym_is_in_this_sec maybe_range (SymbolDef (def)) then def :: x2 else x2) (elf_memory_image_defined_symbols_and_ranges irec.img) x2) in let included_global_defs = (let x2 = ([]) in List.fold_right (fun def x2 -> if not (Nat_big_num.equal ( (* filter out locals *) get_elf64_symbol_binding def.def_syment) stb_local) then def :: x2 else x2) included_defs x2) in (* What symbol defs are being included? *) (* For each global symbol defined in the section, output a line. *) (*let _ = Missing_pervasives.outs (List.foldl (^) "" ( List.map (fun def -> (make_line "" (hex_string_of_natural (comp_addr + (natural_of_elf64_addr def.def_syment.elf64_st_value))) (hex_string_of_natural (natural_of_elf64_xword def.def_syment.elf64_st_size)) (" " ^ def.def_symname)) ^ "\n" ) included_global_defs )) in*) let ( : (( element_range option) * ( any_abi_feature range_tag)) Pset.set) = (Lem_set.setMapMaybe (instance_Basic_classes_SetType_tup2_dict (instance_Basic_classes_SetType_Maybe_maybe_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_Num_natural_dict instance_Basic_classes_SetType_Num_natural_dict))) instance_Basic_classes_SetType_var_dict) (instance_Basic_classes_SetType_tup2_dict (instance_Basic_classes_SetType_Maybe_maybe_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_Num_natural_dict instance_Basic_classes_SetType_Num_natural_dict))) instance_Basic_classes_SetType_var_dict) (fun (maybe_range, tag) -> (* How do we update existing metadata? In general, * we get a new range. *) let new_range = ((match maybe_range with None -> None | Some(el_name, (start, len)) -> Some(secname1, ( (* FIXME: pass this through a section-to-element gensym. We can just (for now) define output element names to equal the section names, since we have no unnamed output sections and no output common symbols. *)let new_start_off = (Nat_big_num.add start ( Nat_big_num.sub_nat comp_addr output_section_start_addr)) in (*let _ = errln ("Calculated element offset 0x" ^ (hex_string_of_natural new_start_off) ^ " in element " ^ secname ^ " for tag at address 0x" ^ (hex_string_of_natural accum_current_addr) ^ " , start offset 0x" ^ (hex_string_of_natural start) ^ ", output section start addr 0x" ^ (hex_string_of_natural output_section_start_addr) ^ ", comp_addr 0x" ^ (hex_string_of_natural comp_addr)) in*) (new_start_off, len))) )) in (match tag with (* If it's a section, we discard it. * We will add a new section record at the end. (FIXME) *) | FileFeature(ElfSection(idx1, isec1)) -> None (* If it's a symbol def, we propagate it. * We record its linkable idx, so we can * match it later with the bindings we formed * earlier. * FIXME: this is a bit nasty. Perhaps we * should replace syment with a minimal structure * that avoids duplication. Same for isecs. *) | SymbolDef(def) -> (* if get_elf64_symbol_type def.def_syment = stt_section then Nothing FIXME: also re-create the section symbol when we create the ElfSection else *) (* This doesn't work -- some refs might be bound to this symbol. Instead, strip the symbol when we generate the output symtab (FIXME). *) (*let _ = errln ("Copying symbol named `" ^ def.def_symname ^ "'") in*) Some(new_range, SymbolDef({ def_symname = (def.def_symname) ; def_syment = (def.def_syment) ; def_sym_scn = (def.def_sym_scn) ; def_sym_idx = (def.def_sym_idx) ; def_linkable_idx = (irec.idx) })) | AbiFeature(x) -> Some(new_range, AbiFeature(x)) (* If it's a symbol ref with no reloc site, we discard it? *) | SymbolRef(r) -> (*let _ = if r.ref.ref_symname = "_start" then errln ("Saw ref to _start, " ^ "in section " ^ irec.isec.elf64_section_name_as_string ^ " of linkable " ^ (show irec.idx)) else () in*) let get_binding_for_ref = (fun symref -> (fun linkable_idx -> (fun fname1 -> let name_matches1 = ((match Pmap.lookup symref.ref_symname bindings_by_name with Some x -> x | None -> [] )) in (match List.filter (fun (bi, ((r_idx, r, r_item), m_d)) -> Nat_big_num.equal r_idx linkable_idx && (r = symref)) name_matches1 with [(b_idx, b)] -> (b_idx, b) | [] -> failwith "no binding found" | _ -> failwith ("ambiguous binding found for symbol `" ^ (symref.ref_symname ^ ("' in file " ^ fname1))) ) ))) in let (bi, b) = (get_binding_for_ref r.ref irec.idx irec.fname) in let ((ref_idx, ref1, ref_linkable), maybe_def) = b in (match r.maybe_reloc with None -> None (* If it's a reloc site, we need to somehow point it * at the *definition* that it was bound to. YES. * reloc_sites are type reloc_site = <| ref_relent : elf64_relocation_a ; ref_rel_scn : natural --the relocation section idx ; ref_rel_idx : natural --the index of the relocation rec ; ref_src_scn : natural --the section *from which* the reference logically comes |> type elfNN_relocation_a = <| elfNN_ra_offset : elf32_addr --Address at which to relocate ; elfNN_ra_info : elf32_word --Symbol table index/type of relocation to apply ; elfNN_ra_addend : elf32_sword --Addend used to compute value to be stored |> * ... of which ref_src_scn, ref_rel_idx, * ref_rel_scn and elfNN_ra_offset can be ignored. * * What *is* important is that we somehow point at * the symbol definition (or perhaps *un*definition, * if we're generating a shared library) that it * refers to. * * For that, we update ra_info use the 1 + binding_idx, * i.e. consider that there is a fresh symbol table * and that it has a distinct entry for each binding. * * FIXME: we also need to account for * reloc decisions -- MakePIC etc. *) | Some(rs) -> let (rel_type1, _) = (a.parse_reloc_info rs.ref_relent.elf64_ra_info) in Some(new_range, SymbolRef( { ref = ({ (* This is not the place to be fixing up * symbol references. We can't yet patch the element content, * because we haven't yet decided on the address of everything. * * That said, we *do* need to represent the old ref in the new * linked-image context. That's *all* we should be doing, right now. * *) ref_symname = (ref1.ref_symname) ; ref_syment = ({ elf64_st_name = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) (* unused *) ; elf64_st_info = (ref1.ref_syment.elf64_st_info) ; elf64_st_other = (ref1.ref_syment.elf64_st_other) ; elf64_st_shndx = (Uint32_wrapper.of_bigint( (* shn_abs *) (Nat_big_num.of_int 0))) ; elf64_st_value = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))) ; elf64_st_size = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))) }) ; ref_sym_scn =( (Nat_big_num.of_int 0)) ; ref_sym_idx =( (Nat_big_num.of_int 0)) (* match maybe_def with Just _ -> 1+bi | Nothing -> 0 end *) }) ; maybe_reloc = (Some { ref_relent = ({ elf64_ra_offset = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))) (* ignored *) ; elf64_ra_info = (Uint64_wrapper.logor (* HACK: use bi as the symbol index. *) (Uint64_wrapper.of_bigint rel_type1) (Uint64_wrapper.shift_left (* ... actually, don't, now we have maybe_def_bound_to *) (Uint64_wrapper.of_bigint( (* (1+bi) *) (Nat_big_num.of_int 0))) 32 ) ) ; elf64_ra_addend = (rs.ref_relent.elf64_ra_addend) }) ; ref_rel_scn =( (Nat_big_num.of_int 0)) ; ref_rel_idx =( (Nat_big_num.of_int 0)) ; ref_src_scn =( (Nat_big_num.of_int 0)) }) ; maybe_def_bound_to = ( (* Re-search the bindings list for a match, because we might have * re-bound this symbol since we created the image. FIXME: since * we do this, is there anything gained from populating this field * earlier? Probably best not to. *)let (possible_bindings : (Nat_big_num.num * binding) list) = ((match Pmap.lookup ref1.ref_symname bindings_by_name with Some l -> if ref1.ref_symname = "__fini_array_end" then (*let _ = errln ("Found " ^ (show (length l)) ^ " bindings for __fini_array_end, of which " ^ (show (length (List.filter (fun (bi, (r, maybe_d)) -> maybe_d <> Nothing) l))) ^ " are with definition") in*) l else l | None -> [] )) in (* what's the actual binding? *) (match r.maybe_def_bound_to with None -> failwith ("at this stage, all references must have a decision: `" ^ (ref1.ref_symname ^ "'")) | Some(decision, _) -> (* Search the list of bindings for a possibly-updated * binding for this reference. *) let matching_possibles = (List.filter (fun (bi, ((ref_idx, ref1, ref_item), maybe_d)) -> (match maybe_d with None -> false | Some (def_idx, def, def_item) -> Nat_big_num.equal (* match the *reference*, whose linkable we're processing now *) irec.idx ref_idx && (Nat_big_num.equal r.ref.ref_sym_scn ref1.ref_sym_scn && Nat_big_num.equal r.ref.ref_sym_idx ref1.ref_sym_idx) (* def.def_syment = sd.def_syment && def.def_sym_scn = sd.def_sym_scn && def.def_sym_idx = sd.def_sym_idx && def_idx = sd.def_linkable_idx *) ) ) possible_bindings) in (*let _ = errln ("For a ref to `" ^ ref.ref_symname ^ "', possibles list is: " ^ ( List.foldl (fun x -> fun y -> x ^ ", " ^ y) "" (List.map (fun (bi, ((_, _, _), maybe_d)) -> match maybe_d with Just(def_idx, def, def_item) -> "`" ^ def.def_symname ^ "' " ^ "in linkable " ^ (show def_idx) ^ ", section " ^ (show def.def_sym_scn) ^ ", sym idx " ^ (show def.def_sym_idx) | _ -> failwith "impossible: just filtered out no-def bindings" end ) matching_possibles) )) in*) let new_bound_to = ((match matching_possibles with [] -> Some(ApplyReloc, None) | [(bi, ((rl, r, ri), maybe_d))] -> Some(decision, (match maybe_d with Some (def_idx, def, def_item) -> Some { def_symname = (def.def_symname) ; def_syment = (def.def_syment) ; def_sym_scn = (def.def_sym_scn) ; def_sym_idx = (def.def_sym_idx) ; def_linkable_idx = def_idx } | None -> None )) | _ -> failwith ("After linker script, ambiguous bindings for `" ^ (ref1.ref_symname ^ "'")) )) in if not ((Lem.option_equal (Lem.pair_equal (=) (Lem.option_equal (=))) new_bound_to r.maybe_def_bound_to)) then (*let _ = errln ("Changed binding for reference to `" ^ ref.ref_symname ^ "' in linkable " ^ (show irec.idx)) in*) new_bound_to else if (Lem.option_equal (Lem.pair_equal (=) (Lem.option_equal (=))) new_bound_to None) then failwith "really need a decision by now" else new_bound_to )) (* if irec.fname = "libc.a(__uClibc_main.os)" && irec.isec.elf64_section_name_as_string = ".data.rel.local" then let _ = errln ("Saw the bugger: " ^ (match r.maybe_def_bound_to with Just(decision, Just(sd)) -> show sd.def_syment | _ -> "(not complete)" end)) in r.maybe_def_bound_to else r.maybe_def_bound_to *) } )) ) (* match maybe_reloc *) ) (* match tag *) ) ((Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) ranges_and_tags))) (* end mapMaybe fn *) in let isec_sz = (irec.isec.elf64_section_size) in let maybe_el_sz = (el.length1) in let contents_sz = (length el.contents) in let (actual_sz, padded_contents) = ((match maybe_el_sz with Some el_sz -> let diff = (Nat_big_num.sub_nat el_sz contents_sz) in if Nat_big_num.less diff( (Nat_big_num.of_int 0)) then (* contents greater than what the el says, so chop the end off *) (*let _ = Missing_pervasives.errln ("Warning: size mismatch for section " ^ irec.isec.elf64_section_name_as_string ^ " from " ^ irec.fname) in*) (el_sz, take0 el_sz el.contents) else (el_sz, List.rev_append (List.rev el.contents) (replicate0 diff None)) | None -> if not (Nat_big_num.equal (length el.contents) isec_sz) then failwith "input section size not equal to its content pattern length" else (isec_sz, el.contents) )) in (*let _ = errln ("Saw first 20 bytes of section " ^ irec.isec.elf64_section_name_as_string ^ " from " ^ irec.fname ^ " as " ^ (show (take 20 padded_contents))) in*) (actual_sz, padded_contents, new_ranges_and_tags) | _ -> failwith "impossible: no such element" ) (* match Map.lookup idstr img.elements *) ) (* match maybe_secname *) | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> (*let _ = errln ("Including common symbol called `" ^ def.def_symname ^ "'") in*) (* We want to get the common symbol as a byte pattern *) let sz = (Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_size) in let content = (Missing_pervasives.replicate0 sz (Some(Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 0)))))) in (*let _ = Missing_pervasives.outln (make_line "COMMON" (hex_string_of_natural comp_addr) (hex_string_of_natural sz) fname) in*) (sz, content,(Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) [(Some(secname1, ( Nat_big_num.sub_nat comp_addr output_section_start_addr, sz)), SymbolDef({ def_symname = (def.def_symname) ; def_syment = (def.def_syment) ; def_sym_scn = (def.def_sym_scn) ; def_sym_idx = (def.def_sym_idx) ; def_linkable_idx = linkable_idx }))])) (* | Hole(AddressExprFn f) -> let next_addr = f addr (AllocatedSectionsMap outputs_by_name) in let n = next_addr - addr in let content = Missing_pervasives.replicate n Nothing in let _ = Missing_pervasives.outln (make_line "*fill*" (hex_string_of_natural comp_addr) (hex_string_of_natural n) "") in (next_addr - addr, content, {}) *) | ProvideSymbol(pol, name1, (size2, info, other)) -> (*let _ = errln ("Creating symbol definition named `" ^ name ^ "' in output section `" ^ secname ^ "'") in*) let symaddr = accum_current_addr (* FIXME: support others *) in (*let _ = Missing_pervasives.outln (make_line "" (hex_string_of_natural symaddr) "" ("PROVIDE (" ^ name ^ ", .)")) in*) ((* sz *) (Nat_big_num.of_int 0), (* comp_el_pat *) [],(Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) [( Some(secname1, (( Nat_big_num.sub_nat symaddr output_section_start_addr), (Nat_big_num.of_int 0))), SymbolDef(symbol_def_for_provide_symbol name1 size2 info other control_script_linkable_idx) )]) ) )) (* match comp_el_pat *) in (*let _ = errln ("Appending byte pattern to section " ^ secname ^ ", first 20 bytes: " ^ (show (take 20 comp_el_pat))) in*) let new_content = (append_to_byte_pattern_at_offset ( Nat_big_num.sub_nat comp_addr output_section_start_addr) accum_pat comp_el_pat) in let new_addr = (Nat_big_num.add comp_addr sz) in let new_meta = (Pset.(union) accum_meta this_el_meta) in (new_content, new_addr, new_meta) )) ([], output_section_start_addr,(Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) [])) (list_combine comp comp_addrs)) in let concat_sec_el = ({ Memory_image.startpos = (Some(output_section_start_addr)) ; Memory_image.length1 = (Some(size2)) ; Memory_image.contents = concatenated_content }) in (*let _ = Missing_pervasives.outln "" in*) (* Make a new element in the image, also transferring metadata from input elements * as appropriate. *) let new_by_range_list = ((Some(secname1, ( (Nat_big_num.of_int 0), size2)), FileFeature(ElfSection((* We don't yet konw where this'll come in the output file, so ... *) (* scn_idx *) (Nat_big_num.of_int 0), { elf64_section_name =( (Nat_big_num.of_int 0)) (* ignored *) ; elf64_section_type = (output_section_type comp) ; elf64_section_flags = (output_section_flags comp) ; elf64_section_addr =( (Nat_big_num.of_int 0)) (* ignored -- covered by element *) ; elf64_section_offset =( (Nat_big_num.of_int 0)) (* ignored -- will be replaced when file offsets are assigned *) ; elf64_section_size =( (Nat_big_num.of_int 0)) (* ignored *) ; elf64_section_link =( (Nat_big_num.of_int 0)) (* HMM *) ; elf64_section_info =( (Nat_big_num.of_int 0)) (* HMM *) ; elf64_section_align = (alignof_output_section comp) ; elf64_section_entsize =( (Nat_big_num.of_int 0)) (* HMM *) ; elf64_section_body = Byte_sequence.empty (* ignored *) ; elf64_section_name_as_string = secname1 (* can't rely on this being ignored *) } ))) :: Pset.elements new_range_tag_pairs) in (*let _ = errln ("Metadata for new section " ^ secname ^ " consists of " ^ (show (length new_by_range_list)) ^ " tags.") in*) let new_by_range = (List.fold_left (fun m -> fun (maybe_range, tag) -> let new_s = (Pset.add (maybe_range, tag) m) in (* let _ = errln ("Inserting an element into by_range; before: " ^ (show (Set.size m)) ^ "; after: " ^ (show (Set.size new_s))) in *) new_s ) acc_img.by_range new_by_range_list) in let new_by_tag = (by_tag_from_by_range (instance_Basic_classes_SetType_Maybe_maybe_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict instance_Basic_classes_SetType_Num_natural_dict instance_Basic_classes_SetType_Num_natural_dict))) instance_Basic_classes_SetType_var_dict new_by_range) in let _ = (let = (List.filter (fun (maybe_range, tag) -> (match tag with | FileFeature(ElfSection(idx1, isec1)) -> true | _ -> false )) (Pset.elements new_by_range)) in (* errln ("Total metadata now includes " ^ (show (length section_tags_bare)) ^ " sections; are by_range and " ^ "by_tag consistent? " ^ (show (new_by_tag = by_tag_from_by_range new_by_range))) *) ()) in (* this expression is the return value of add_output_section *) ( Nat_big_num.add (* new_pos *) output_section_start_addr size2, (* new_acc *) { elements = (Pmap.add secname1 concat_sec_el acc_img.elements) (* tag it as a section, and transfer any tags *) ; by_range = (* let _ = errln ("Returning from add_output_section a by_range with " ^ (show (Set.size new_by_range))) in *) new_by_range ; by_tag = new_by_tag }, (* sec_sz *) size2, (* replacement_output_sec *) (OutputSectionSpec (guard, Some(output_section_start_addr), secname1, comp)) ) )) (* end add_output_section *) in (match script1 with [] -> (acc, (AllocatedSectionsMap outputs_by_name)) | (element1, el_idx) :: more_elements_and_idx -> let do_nothing = (acc, pos, (AllocatedSectionsMap outputs_by_name)) in let (new_acc, new_pos, new_outputs_by_name) = ((match element1 with DefineSymbol(symdefpol, name1, (symsize, syminfo, symother)) -> (* We've already added this to the output composition. *) do_nothing | AdvanceAddress(AddressExprFn advance_fn_ref) -> let advance_fn = ((match Pmap.lookup advance_fn_ref alloc_map with | Some m -> m | None -> failwith "alloc_map invariant failure" )) in let new_pos = (advance_fn pos (AllocatedSectionsMap outputs_by_name)) in (acc, new_pos, (AllocatedSectionsMap outputs_by_name)) (* FIXME: the allocated sections map is the subset of the outputs_by_name map * that has been allocated -- meaning *both* sized *and* placed. * Since we're a multi-pass interpreter, we've sized everything already, but * only a subset has been placed. So we need to weed out all elements from * outputs_by_name that don't correspond to a section in the accumulated image. * We should probably include the section's range_tag in the allocated_sections_map, * which would force us to do this, but at the moment neither of these is done. *) | MarkAndAlignDataSegment(maxpagesize1, commonpagesize1) -> (* GNU linker manual says: "DATA_SEGMENT_ALIGN(MAXPAGESIZE, COMMONPAGESIZE) is equivalent to either (ALIGN(MAXPAGESIZE) + (. & (MAXPAGESIZE - 1))) or (ALIGN(MAXPAGESIZE) + (. & (MAXPAGESIZE - COMMONPAGESIZE))) depending on whether the latter uses fewer COMMONPAGESIZE sized pages for the data segment (area between the result of this expression and `DATA_SEGMENT_END') than the former or not. If the latter form is used, it means COMMONPAGESIZE bytes of runtime memory will be saved at the expense of up to COMMONPAGESIZE wasted bytes in the on-disk file." In other words, we're marking the beginning of the data segment by aligning our position upwards by an amount that - guarantees we're on a new page... - ... but (option 1) at an address that's congruent, modulo the max page size (e.g. for 64kB maxpage, 4kB commonpage, we AND with 0xffff) - ... (option 2) at an offset that's at the commonpagesize boundary immediately preceding the lowest congruent address (e.g. for 64kB maxpage, 4kB commonpage, we AND with 0xf000, so if we're at pos 0x1234, we bump up to 0x11000). FIXME: The GNU linker seems to bump up to 0x12000 here, not 0x11000. Specifically, DATA_SEGMENT_ALIGN (0x200000, 0x1000) bumps 0x4017dc up to 0x602000. This is indeed better, because it allows the next section to be output without a big gap in the file. LOAD 0x0000000000000000 0x0000000000400000 0x0000000000400000 0x00000000000017dc 0x00000000000017dc R E 200000 LOAD 0x0000000000002000 0x0000000000602000 0x0000000000602000 0x0000000000000120 0x0000000000000ce8 RW 200000 ... whereas if the second LOAD began at address 0x601000, the file offset of its first section would have to be 0x11000. So what *should* the formula be? It needs to calculate the next address which - is a commonpagesize boundary; - is minimally >= the current address, modulo the commonpagesize - is minimally >= the current address, modulo the maxpagesize. The AND operation gives us something that is minimally *below* the commonpagesize boundary. I think we need to add COMMONPAGESIZE. The code does this (in ldexp.c around line 478 as of binutils 2.25): expld.result.value = align_n (expld.dot, maxpage); /* omit relro phase */ if (expld.dataseg.phase == exp_dataseg_adjust) { if (commonpage < maxpage) expld.result.value += ((expld.dot + commonpage - 1) & (maxpage - commonpage)); } else { expld.result.value += expld.dot & (maxpage - 1); Which amounts to: 1. first, align up to maxpage. So for our example, we're now 0x10000. or for our real example, we're now 0x600000 THEN since the first phase (expld_dataseg_none) hits the final "else" case, we immediately restore the modulus of the address, giving 0x60188c. or 0x6019ac the second time around (FIXME: why two?) 2. next, on the relevant phase (pass) of the script interpreter, i.e. OPTION 2 if commonpage < maxpage, bump up the *non-maxpage-aligned non-modulo-restored* address by (. + commonpage - 1) & (maxpage - commonpage) i.e. for our example earlier (0x01234 + 0x1000 - 1) & (0xf000) = 0x02233 & 0xf000 = 0x02000 i.e. for our real example (0x4019ac + 0x1000 - 1) & (0x1ff000) = 0x4019ac + 0x1000 - 1) & 0x1ff000 = 0x002000 3. OPTION 1 is implemented by the trailing "else {" -- it restores the modulus. So the problem with our original logic (below) was that it did what the manual says, not what the code does. Specifically, the code for option 2 does (. + commonpagesize - 1) & (maxpagesize - commonpagesize) and NOT simply . & (maxpagesize - commonpagesize). FIXME: report this bug. Note that intervening commands can do arbitrary things to the location counter, so we can't do any short-cut arithmetic based on section sizes; we actually have to run the layout procedure til we hit the end of the data segment, and then see how we do. We run this function *forward* with the first option on a subset of the script ending with the end of the data segment. We then see what comes back. *) (* let num_pages_used *) (*let _ = errln ("Option 1 congruence add-in from pos 0x" ^ (hex_string_of_natural pos) ^ ", maxpagesize 0x" ^ (hex_string_of_natural maxpagesize) ^ " is 0x" ^ (hex_string_of_natural (natural_land pos (maxpagesize - 1)))) in*) let option1 = (Nat_big_num.add (align_up_to maxpagesize1 pos) (Nat_big_num.bitwise_and pos ( Nat_big_num.sub_nat maxpagesize1( (Nat_big_num.of_int 1))))) in (*let _ = errln ("Mark/align data segment: option 1 is to bump pos to 0x" ^ (hex_string_of_natural option1)) in*) let option2 = (Nat_big_num.add (align_up_to maxpagesize1 pos) (Nat_big_num.bitwise_and ( Nat_big_num.sub_nat (Nat_big_num.add pos commonpagesize1)( (Nat_big_num.of_int 1))) ( Nat_big_num.sub_nat maxpagesize1 commonpagesize1))) in (*let _ = errln ("Mark/align data segment: option 2 is to bump pos to 0x" ^ (hex_string_of_natural option2)) in*) let data_segment_endpos = (fun startpos1 -> (* run forward from here until MarkDataSegmentEnd, * accumulating the actually-made outputs by name and their sizes *) let (endpos, _) = (List.fold_left (fun (curpos, seen_end) -> fun (new_script_item, new_script_item_idx) -> (*let _ = errln ("Folding at pos 0x" ^ (hex_string_of_natural curpos)) in*) if seen_end then (curpos, true) else let (newpos, new_seen) = ((match new_script_item with | MarkDataSegmentEnd -> (*let _ = errln "data segment end" in*) (* break the loop early here *) (curpos, true) | OutputSection(outputguard, maybe_expr, name1, sub_elements) -> (*let _ = errln ("output section " ^ name) in*) let maybe_found = (Pmap.lookup name1 outputs_by_name) in let (OutputSectionSpec (guard, addr, secname1, comp), seen_script_el_idx) = ((match maybe_found with Some (f, seen_script_el_idx) -> (f, seen_script_el_idx) | None -> failwith "internal error: output section not found" )) in (* Sometimes a given output section name, say .eh_frame, can come from multiple * script elements with disjoint guard conditions (only_if_ro and only_if_rw, say). * Only one of them will actually be selected when the guard is being evaluated. * So when we "replay" the sections' output here, we want to skip the ones whose * guards were false. The way we implement this is to store the originating script * element idx in the allocated_output_sections map. We can test that against our * current script element_idx here *) let replay_output = ( Nat_big_num.equal seen_script_el_idx el_idx) in if replay_output then ( let unaligned_start_addr = curpos in let start_addr = (align_up_to (alignof_output_section comp) unaligned_start_addr) in let (end_addr, comp_addrs) = (do_output_section_layout_starting_at_addr start_addr (AllocatedSectionsMap outputs_by_name) comp) in let size2 = (Nat_big_num.sub_nat end_addr start_addr) in (end_addr, (* seen_end *) false) ) else (curpos, (* seen_end *) false) | AdvanceAddress(AddressExprFn advance_fn_ref) -> (*let _ = errln "Advance address" in*) let advance_fn = ((match Pmap.lookup advance_fn_ref alloc_map with | Some m -> m | None -> failwith "alloc_map invariant failed" )) in let new_pos = (advance_fn curpos (AllocatedSectionsMap outputs_by_name)) in (new_pos, false) | _ -> (curpos, seen_end) )) in if Nat_big_num.less newpos curpos then failwith "went backwards" else (newpos, new_seen) ) (startpos1, false) more_elements_and_idx) in endpos ) in let endpos_option1 = (data_segment_endpos option1) in let endpos_option2 = (data_segment_endpos option2) in (*let _ = errln ("Mark/align data segment: option 1 gives an endpos of 0x" ^ (hex_string_of_natural endpos_option1)) in*) (*let _ = errln ("Mark/align data segment: option 2 gives an endpos of 0x" ^ (hex_string_of_natural endpos_option2)) in*) let npages = (fun startpos1 -> (fun endpos -> Nat_big_num.div ( Nat_big_num.sub_nat(align_up_to commonpagesize1 endpos) (round_down_to commonpagesize1 startpos1)) commonpagesize1 )) in let npages_option1 = (npages option1 endpos_option1) in let npages_option2 = (npages option2 endpos_option1) in (*let _ = errln ("Mark/align data segment: option 1 uses " ^ (show npages_option1) ^ " COMMONPAGESIZE-sized pages") in*) (*let _ = errln ("Mark/align data segment: option 2 uses " ^ (show npages_option2) ^ " COMMONPAGESIZE-sized pages") in*) if Nat_big_num.less npages_option1 npages_option2 then (*let _ = errln "Choosing option 1" in*) (acc, option1, (AllocatedSectionsMap outputs_by_name)) else (*let _ = errln "Choosing option 2" in*) (acc, option2, (AllocatedSectionsMap outputs_by_name)) | MarkDataSegmentEnd -> do_nothing | MarkDataSegmentRelroEnd(*(fun_from_secs_to_something)*) -> do_nothing | OutputSection(outputguard, maybe_expr, name1, sub_elements) -> (* Get the composition we computed earlier, and actually put it in * the image, assigning an address to it. *) let maybe_found = (Pmap.lookup name1 outputs_by_name) in let (found, seen_script_el_idx) = ((match maybe_found with Some (f, saved_idx) -> (f, saved_idx) | None -> failwith "internal error: output section not found" )) in let (OutputSectionSpec (guard, addr, secname1, comp)) = found in (* let next_free_section_idx = 1 + naturalFromNat (Map.size outputs_by_name) in *) let count_sections_in_image = (fun img2 -> ( let (, section_ranges) = (elf_memory_image_section_ranges img2) in let = (Lem_list.map (fun tag -> (match tag with | FileFeature(ElfSection(idx1, isec1)) -> true | _ -> false )) section_tags) in length section_tags_bare )) in (* Do we actually want to add an output section? Skip empty sections. * CARE: we actually want to heed the proper ld semantics for empty sections * (e.g. ". = ." will force output). From the GNU ld manual: The linker will not normally create output sections with no contents. This is for convenience when referring to input sections that may or may not be present in any of the input files. For example: .foo : { *(.foo) } will only create a `.foo' section in the output file if there is a `.foo' section in at least one input file, and if the input sections are not all empty. Other link script directives that allocate space in an output section will also create the output section. So too will assignments to dot even if the assignment does not create space, except for `. = 0', `. = . + 0', `. = sym', `. = . + sym' and `. = ALIGN (. != 0, expr, 1)' when `sym' is an absolute symbol of value 0 defined in the script. This allows you to force output of an empty section with `. = .'. The linker will ignore address assignments ( *note Output Section Address::) on discarded output sections, except when the linker script defines symbols in the output section. In that case the linker will obey the address assignments, possibly advancing dot even though the section is discarded. * It follows that we might discard the output section, * but *retain* the symbol definitions within it, * and keep the dot-advancements that * In other words, we care about two things: * * -- whether there are any non-empty input sections, *or* * non-excluded assignments to dot, inside the composition: * this controls whether the section is output * -- whether the script defines symbols in the section; if so * then *even if the section is discarded* * we must honour the address assignments, * which means using the ending address of do_output_section_layout_starting_at_addr, * *and* * we must retain the symbol definitions (which now could * end up going in some other section? HMM...) *) let comp_element_allocates_space = (fun comp_el -> (match comp_el with IncludeInputSection(_, irec) -> Nat_big_num.greater (*let _ = errln ("Saw an input section named `" ^ irec.isec.elf64_section_name_as_string ^ "' of size " ^ (show irec.isec.elf64_section_size)) in*) irec.isec.elf64_section_size( (Nat_big_num.of_int 0)) | IncludeCommonSymbol(retain_pol, fname1, idx1, def, img2) -> Nat_big_num.greater (Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_size)( (Nat_big_num.of_int 0)) | ProvideSymbol(pol, name1, spec) -> true (* HACK: what else makes sense here? *) | Hole(AddressExprFn(address_fn_ref)) -> let address_fn = ((match Pmap.lookup address_fn_ref alloc_map with | Some m -> m | None -> failwith "alloc_map invariant failed" )) in let assignment_is_excluded = (fun f -> (* really makes you wish you were programming in Lisp *) let always_gives_0 = ( Nat_big_num.equal(f( (Nat_big_num.of_int 0)) (AllocatedSectionsMap outputs_by_name))( (Nat_big_num.of_int 0)) && Nat_big_num.equal (f( (Nat_big_num.of_int 42)) (AllocatedSectionsMap outputs_by_name))( (Nat_big_num.of_int 0))) (* FIXME: this is wrong *) in let always_gives_dot = ( Nat_big_num.equal(f( (Nat_big_num.of_int 0)) (AllocatedSectionsMap outputs_by_name))( (Nat_big_num.of_int 0)) && Nat_big_num.equal (f( (Nat_big_num.of_int 42)) (AllocatedSectionsMap outputs_by_name))( (Nat_big_num.of_int 42))) (* FIXME: this is wrong *) in (* FIXME: what are the semantics of function equality in Lem? *) always_gives_0 || (always_gives_dot (*&& (AddressExprFn(f)) <> assign_dot_to_itself*) (* FIXME DPM: almost certainly not what is meant... *))) in not (assignment_is_excluded address_fn) )) in let section_contains_non_empty_inputs = (List.exists comp_element_allocates_space comp) in (* See note in MarkDataSegmentEnd case about script element idx. Short version: * multiple output section stanzas, for a given section name, may be in the script, * but only one was activated by the section composition pass. Ignore the others. *) let do_output = (( Nat_big_num.equal seen_script_el_idx el_idx) && section_contains_non_empty_inputs) in if not do_output then (*let _ = errln ("At pos 0x" ^ (hex_string_of_natural pos) ^ ", skipping output section " ^ name ^ " because " ^ (if not section_contains_non_empty_inputs then "it contains no non-empty inputs" else "it was excluded by its output guard")) in*) (acc, pos, (AllocatedSectionsMap outputs_by_name)) else ( (* let _ = errln ("Before adding output section, we have " ^ (show (count_sections_in_image acc)) ^ " sections.") in *) let (new_pos, new_acc, sec_sz, replacement_output_sec) = (add_output_section ((* next_free_section_idx, *) pos, acc) found) in (*let _ = errln ("At pos 0x" ^ (hex_string_of_natural pos) ^ ", adding output section " ^ name ^ " composed of " ^ (show (length comp)) ^ " items, new pos is 0x" ^ (hex_string_of_natural new_pos)) in*) (* let _ = errln ("Received from add_output_section a by_range with " ^ (show (Set.size new_acc.by_range)) ^ " metadata records of which " ^ (show (Set.size { (r, t) | forall ((r, t) IN new_acc.by_range) | match t with FileFeature(ElfSection(x)) -> true | _ -> false end } )) ^ " are ELF sections; one more time: " ^ (show (Set.size { (t, r) | forall ((t, r) IN new_acc.by_tag) | match t with FileFeature(ElfSection(x)) -> true | _ -> false end } )) ^ "; count_sections_in_image says " ^ (show ( length (Multimap.lookupBy Memory_image_orderings.tagEquiv (FileFeature(ElfSection(0, null_elf64_interpreted_section))) new_acc.by_tag) )) ) in *) (* let _ = errln ("After adding output section, we have " ^ (show (count_sections_in_image new_acc)) ^ " sections.") in *) (new_acc, new_pos, (AllocatedSectionsMap (Pmap.add name1 (replacement_output_sec, el_idx) (Pmap.remove name1 outputs_by_name)))) ) | DiscardInput(selector) -> do_nothing | InputQuery(retainpol, sortpol, selector) -> do_nothing )) in (* recurse *) build_image a alloc_map new_acc new_pos new_outputs_by_name bindings_by_name more_elements_and_idx control_script_linkable_idx linker_defs_by_name )) (* let rec consecutive_commons rev_acc l = match l with [] -> reverse rev_acc | IncludeCommonSymbol(pol, fname, def, img) :: rest -> consecutive_commons ((pol, fname, def, img) :: rev_acc) rest | _ -> reverse rev_acc end *) (*val default_place_orphans : input_output_assignment -> list input_spec -> input_output_assignment*) let default_place_orphans (discards, outputs) inputs:(input_spec)list*(output_section_spec*Nat_big_num.num)list= ( (* Try to emulate the GNU linker. * Its docs say: "It attempts to place orphan sections after non-orphan sections of the same attribute, such as code vs data, loadable vs non-loadable, etc. If there is not enough room to do this then it places at the end of the file. For ELF targets, the attribute of the section includes section type as well as section flag." * It places the .tm_clone_table orphan [ 9] .tm_clone_table PROGBITS 0000000000000000 00000160 0000000000000000 0000000000000000 WA 0 0 8 as .data 0x0000000000602120 0x0 crtend.o .data 0x0000000000602120 0x0 crtn.o .tm_clone_table 0x0000000000602120 0x0 .tm_clone_table 0x0000000000602120 0x0 crtbeginT.o .tm_clone_table 0x0000000000602120 0x0 crtend.o .data1 *(.data1) 0x0000000000602120 _edata = . i.e. between .data and .data1. In the script: .got.plt : { *(.got.plt) *(.igot.plt) } .data : { *(.data .data.* .gnu.linkonce.d.* ) SORT(CONSTRUCTORS) } .data1 : { *(.data1) } _edata = .; PROVIDE (edata = .); . = .; __bss_start = .; i.e. no clear reason for why between .data and .data1. In the code: (see elf32em.c line 1787 in binutils 2.25) ... the key bit of code is as follows. place = NULL; if ((s->flags & (SEC_ALLOC | SEC_DEBUGGING)) == 0) place = &hold[orphan_nonalloc]; else if ((s->flags & SEC_ALLOC) == 0) ; else if ((s->flags & SEC_LOAD) != 0 && ((iself && sh_type == SHT_NOTE) || (!iself && CONST_STRNEQ (secname, ".note")))) place = &hold[orphan_interp]; else if ((s->flags & (SEC_LOAD | SEC_HAS_CONTENTS | SEC_THREAD_LOCAL)) == 0) place = &hold[orphan_bss]; else if ((s->flags & SEC_SMALL_DATA) != 0) place = &hold[orphan_sdata]; else if ((s->flags & SEC_THREAD_LOCAL) != 0) place = &hold[orphan_tdata]; else if ((s->flags & SEC_READONLY) == 0) place = &hold[orphan_data]; else if (((iself && (sh_type == SHT_RELA || sh_type == SHT_REL)) || (!iself && CONST_STRNEQ (secname, ".rel"))) && (s->flags & SEC_LOAD) != 0) place = &hold[orphan_rel]; else if ((s->flags & SEC_CODE) == 0) place = &hold[orphan_rodata]; else place = &hold[orphan_text]; .. we replicate it here. *)let output_irecs = (List.fold_left (fun acc -> fun outp -> ((match outp with (OutputSectionSpec(guard, maybe_addr, name1, comp), script_el_idx) -> let all_irecs = (List.fold_left (fun inner_acc -> fun comp_el -> (match comp_el with IncludeInputSection(_, irec) -> Pset.add irec inner_acc | _ -> inner_acc ))(Pset.from_list compare []) comp) in Pset.(union) all_irecs acc | _ -> acc )))(Pset.from_list compare []) outputs) in let (orphans : input_spec list) = (List.filter (fun inp -> (match inp with InputSection(irec) -> let v = (not ( Pset.mem irec output_irecs)) in (*let _ = if v then errln ("Saw an orphan input section: " ^ irec.secname ^ " in " ^ irec.fname) else () in*) v | _ -> false )) inputs) in let place_one_orphan = (fun acc -> fun input -> ( let irec = ((match input with InputSection(irec) -> irec | _ -> failwith "impossible: orphan section is not a section" )) in let (discards, outputs) = acc in let find_output = (fun maybe_name -> fun maybe_type -> fun flags_must_have -> fun flags_must_not_have -> ( Missing_pervasives.find_index0 (fun (OutputSectionSpec (guard, maybe_addr, name1, comp), script_el_idx) -> let flags = (output_section_flags comp) in (match maybe_name with Some n -> n = name1 | None -> true ) && ((match maybe_type with Some t -> Nat_big_num.equal (output_section_type comp) t | None -> true ) && (Pset.for_all (fun x -> flag_is_set x flags) flags_must_have && Pset.for_all (fun x -> not (flag_is_set x flags)) flags_must_not_have)) ) outputs )) in let place_after_nonalloc = (find_output None None(Pset.from_list Nat_big_num.compare [])(Pset.from_list Nat_big_num.compare [ shf_alloc ])) in let place_after_interp = (find_output (Some(".interp")) (Some(sht_progbits))(Pset.from_list Nat_big_num.compare [ shf_alloc ])(Pset.from_list Nat_big_num.compare [])) in let place_after_bss = (find_output (Some(".bss")) (Some(sht_nobits))(Pset.from_list Nat_big_num.compare [ shf_alloc; shf_write])(Pset.from_list Nat_big_num.compare [])) in let place_after_rodata = (find_output (Some(".rodata")) (Some(sht_progbits))(Pset.from_list Nat_big_num.compare [ shf_alloc ])(Pset.from_list Nat_big_num.compare [ shf_write ])) in let place_after_rel = (find_output (Some(".rela.dyn")) (Some(sht_rela))(Pset.from_list Nat_big_num.compare [])(Pset.from_list Nat_big_num.compare [])) in let place_after_data = (find_output (Some(".data")) (Some(sht_progbits))(Pset.from_list Nat_big_num.compare [ shf_alloc; shf_write ])(Pset.from_list Nat_big_num.compare [])) in let place_after_text = (find_output (Some(".text")) (Some(sht_progbits))(Pset.from_list Nat_big_num.compare [ shf_alloc; shf_execinstr ])(Pset.from_list Nat_big_num.compare [])) in let (place_after : Nat_big_num.num option) = ((match input with InputSection(irec) -> (* HACK: simulates GNU linker, but this logic ought to go elsewhere *) if irec.isec.elf64_section_name_as_string = ".note.GNU-stack" then None else if not (flag_is_set shf_alloc irec.isec.elf64_section_flags) && (* not flag_is_set shf_alloc irec.isec.elf64_section_flags *) (* no debugging, for now *) true then place_after_nonalloc else (* FIXME: reinstate alloc-debugging case *) if Nat_big_num.equal irec.isec.elf64_section_type sht_note (* FIXME: replicate iself logic *) || (irec.isec.elf64_section_name_as_string = ".note") then place_after_interp else if Nat_big_num.equal irec.isec.elf64_section_type sht_nobits then place_after_bss else (* FIXME: implement thread-local case *) if not (flag_is_set shf_write irec.isec.elf64_section_flags) && not (flag_is_set shf_execinstr irec.isec.elf64_section_flags) then place_after_rodata else if flag_is_set shf_write irec.isec.elf64_section_flags && not (flag_is_set shf_execinstr irec.isec.elf64_section_flags) then place_after_data else place_after_text )) in let (discards, outputs) = acc in (match place_after with Some idx1 -> (* The section exists and has the flags we expected, and is at output idx *) (discards, mapi (fun i -> fun output -> (* FIXME: also fix up flags, alignment etc. *) let (OutputSectionSpec (guard, maybe_addr, name1, comp), script_el_idx) = output in if Nat_big_num.equal (Nat_big_num.of_int i) idx1 then (OutputSectionSpec(guard, maybe_addr, name1, List.rev_append (List.rev comp) [IncludeInputSection(DefaultKeep, irec)]), script_el_idx) else output ) outputs ) | None -> (*let _ = errln ("Warning: discarding orphan section `" ^ irec.isec.elf64_section_name_as_string ^ "' from file `" ^ irec.fname ^ "'") in*) ( List.rev_append (List.rev discards) [input], outputs) ) )) in List.fold_left place_one_orphan (discards, outputs) orphans) (*val interpret_linker_control_script : address_expr_fn_map allocated_sections_map -> linker_control_script -> linkable_list -> natural (* control_script_linkable_idx *) -> abi any_abi_feature -> list input_spec -> (input_spec -> input_spec -> ordering) (* seen ordering *) -> (input_output_assignment -> list input_spec -> input_output_assignment) (* place orphans *) -> (Map.map string (list (natural * binding))) (* initial_bindings_by_name *) -> (elf_memory_image * Map.map string (list (natural * binding)))*) let interpret_linker_control_script alloc_map script1 linkables control_script_linkable_idx a inputs seen_ordering place_orphans initial_bindings_by_name:(any_abi_feature)annotated_memory_image*((string),((Nat_big_num.num*binding)list))Pmap.map= (let labelled_script = (label_script script1) in (*let _ = List.mapi (fun i -> fun input -> errln ("Input " ^ (show i) ^ " is " ^ match input with InputSection(inp) -> "input section, name `" ^ inp.secname ^ "', from file `" ^ inp.fname ^ "' (linkable idx " ^ (show inp.idx) ^ ")" | Common(idx, symname, img, def) -> "common symbol `" ^ symname ^ "'" end ) ) inputs in*) let (discards_before_orphans, outputs_before_orphans) = (assign_inputs_to_output_sections ([], [])(Pset.from_list (pairCompare Nat_big_num.compare Nat_big_num.compare) [])(Pset.from_list (tripleCompare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare) []) inputs None None seen_ordering labelled_script) in (* place orphans *) let (discards, outputs) = (place_orphans (discards_before_orphans, outputs_before_orphans) inputs) in (* In assigning inputs to outputs, we may also have defined some symbols. These affect the * bindings that are formed. So, we rewrite the bindings here. Note that we have to do so here, * not in the caller, because these extra bindings can affect the reachability calculation * during GC. *) let (linker_defs_by_name, (bindings_by_name : ( (string, ( (Nat_big_num.num * binding)list))Pmap.map))) = ( let (script_defs_by_name : (string, ( (symbol_definition * symbol_def_policy)list)) Pmap.map) = (List.fold_left (fun acc -> (fun ((OutputSectionSpec (guard, maybe_addr, secname1, comp)), script_el_idx) -> List.fold_left (fun inner_acc -> fun comp_el -> ( (match comp_el with ProvideSymbol(pol, name1, (size2, info, other)) -> (*let _ = errln ("Linker script defining symbol `" ^ name ^ "'") in*) let def = (symbol_def_for_provide_symbol name1 size2 info other control_script_linkable_idx) in let v = ((match Pmap.lookup name1 inner_acc with None -> [(def, pol)] | Some l -> (def, pol) :: l )) in Pmap.add name1 v inner_acc | _ -> inner_acc ) )) (acc : (string, ( (symbol_definition * symbol_def_policy)list)) Pmap.map) comp )) (Pmap.empty compare) outputs) in (* Now that we've made these definitions, what bindings are affected? * We also use this opportunity to bind references to linker-generated symbols, * such as _GLOBAL_OFFSET_TABLE_, since any definitions of these should now be merged * into our inputs. *) (* bit of a HACK: reconstruct the linkable img and idx from the input items *) let idx_to_img = (List.fold_left (fun acc_m -> fun item -> (match item with Common(idx1, _, img2, symdef) -> Pmap.add idx1 img2 (Pmap.remove idx1 acc_m) | InputSection(irec) -> Pmap.add irec.idx irec.img (Pmap.remove irec.idx acc_m) ) ) (Pmap.empty Nat_big_num.compare) inputs) in let (lowest_idx : Nat_big_num.num) = ((match Pset.min_elt_opt (Pmap.domain idx_to_img) with Some x -> x | None -> failwith "internal error: no linkable items" )) in let first_linkable_item = ((match linkables with x :: more -> x | _ -> failwith "internal error: no linkables" )) in let (control_script_input_item : input_item) = ( "(built-in control script)", ControlScript, (BuiltinControlScript, [Builtin]) ) in let (control_script_linkable_item : linkable_item) = ( ControlScriptDefs, control_script_input_item, { item_fmt = "" ; item_check_sections = false ; item_copy_dt_needed = false ; item_force_output = true } ) in let updated_bindings_and_new_defs = (Pmap.map (fun b_list_initial -> Lem_list.map (fun (b_idx, b_initial) -> let ((iref_idx, iref, iref_item), maybe_idef) = b_initial in (*let _ = errln ("Looking for linker script or linker-generated defs of symbol `" ^ iref.ref_symname ^ "'") in*) let possible_script_defs = ((match Pmap.lookup iref.ref_symname script_defs_by_name with Some l -> l | None -> [] )) in let (possible_linker_generated_def : symbol_definition option) = (if a.symbol_is_generated_by_linker iref.ref_symname then (* can we find a definition by this name? *) ((match Pmap.lookup lowest_idx idx_to_img with None -> failwith "no lowest idx found" | Some img2 -> (match List.filter (fun def -> def.def_symname = iref.ref_symname) (defined_symbols instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict img2) with [] -> None | [def] -> Some(def) | _ -> failwith ("first linkable has multiple defs of name `" ^ (iref.ref_symname ^ "'")) ) )) else None) in (* If the binding has no def, we always use the def we have. * If the binding has a def, we use our def only if the policy is AlwaysDefine. *) (*let _ = errs ("Do we override binding " ^ (show b_idx) ^ ", symbol named `" ^ iref.ref_symname ^ "'? ") in*) (* FIXME: check real semantics of defining symbols like '_GLOBAL_OFFSET_TABLE_' in linker script or input objects. * This is really just a guess. *) let new_b_and_maybe_new_def = ((match (maybe_idef, possible_script_defs, possible_linker_generated_def) with | (_, [], None) -> (*let _ = errln "no" in *) (((iref_idx, iref, iref_item), maybe_idef), None) | (None, [], Some(def)) -> (*let _ = errln "yes (was undefined)" in*) (((iref_idx, iref, iref_item), Some(lowest_idx, def, first_linkable_item)), Some(def)) | (_, [(def, AlwaysDefine)], _) -> (*let _ = errln "yes (linker script provides unconditional def)" in*) (((iref_idx, iref, iref_item), Some (control_script_linkable_idx, def, control_script_linkable_item)), Some(def)) | (Some existing_def, ([(def, ProvideIfUsed)]), _) -> (*let _ = errln "no" in*) (((iref_idx, iref, iref_item), Some existing_def), None) | (None, [(def, ProvideIfUsed)], _) -> (*let _ = errln "yes (linker script provides if-used def)" in*) (((iref_idx, iref, iref_item), Some (control_script_linkable_idx, def, control_script_linkable_item)), Some(def)) | (_, pair1 :: pair2 :: more, _) -> (*let _ = errln "error" in*) failwith "ambiguous symbol binding in linker control script" )) in (b_idx, new_b_and_maybe_new_def) ) b_list_initial ) initial_bindings_by_name) in let (new_symbol_defs_map : (string, ( ( symbol_definition option)list)) Pmap.map) = (Pmap.map (fun b_pair_list -> Lem_list.map (fun (b_idx, (new_b, maybe_new_def)) -> maybe_new_def) b_pair_list) updated_bindings_and_new_defs) in let (new_symbol_defs_by_name : (string, ( symbol_definition list)) Pmap.map) = (Pmap.map (fun v -> Lem_list.mapMaybe id0 v) new_symbol_defs_map) in (* { List.mapMaybe id maybe_def_list | forall ((_, maybe_def_list) IN (Map.toSet new_symbol_defs_map)) | true } in*) (*let new_symbol_defs = List.concat (Set_extra.toList new_symbol_def_list_set) in*) let updated_bindings = (Pmap.map (fun b_pair_list -> Lem_list.map (fun (b_idx, (new_b, maybe_new_def)) -> (b_idx, new_b)) b_pair_list) updated_bindings_and_new_defs) in (new_symbol_defs_by_name, updated_bindings) ) in (*let _ = errln ("For __fini_array_end, we have " ^ (let all_bs = match Map.lookup "__fini_array_end" bindings_by_name with Just l -> l | Nothing -> [] end in ((show (length all_bs)) ^ " bindings, of which " ^ (show (length (List.filter (fun (bi, ((ref_idx, ref, ref_item), maybe_def)) -> match maybe_def with Just _ -> true | _ -> false end ) all_bs))) ^ " have defs"))) in*) let outputs_by_name = (let insert_fun = (fun m -> (fun (OutputSectionSpec(guard, maybe_addr, name1, compos), script_idx) -> Pmap.add name1 ((OutputSectionSpec (guard, maybe_addr, name1, compos)), script_idx) m)) in List.fold_left insert_fun (Pmap.empty compare) outputs) in (* Print the link map's "discarded input sections" output. *) (*let _ = Missing_pervasives.outln "\nDiscarded input sections\n" in*) let discard_line = (fun i -> ((match i with InputSection(s) -> let lpadded_secname = (" " ^ s.secname) in lpadded_secname ^ ((space_padding_and_maybe_newline( (Nat_big_num.of_int 16)) lpadded_secname) ^ ("0x0000000000000000" (* FIXME *) ^ (" 0x" ^ ((hex_string_of_natural s.isec.elf64_section_size) ^ (" " ^ (s.fname ^ "\n")))))) | Common(idx1, fname1, img2, def) -> "" (* don't print discard lines for discarded commons *) ))) in (*let _ = Missing_pervasives.outs (List.foldl (fun str -> (fun input -> (str ^ (discard_line input)))) "" (reverse discards)) in*) let outputs_by_name_after_gc = (compute_def_use_and_gc (AllocatedSectionsMap outputs_by_name)) in (*let _ = Missing_pervasives.outs "\nMemory Configuration\n\nName Origin Length Attributes\n*default* 0x0000000000000000 0xffffffffffffffff\n" in let _ = Missing_pervasives.outln "\nLinker script and memory map\n" in*) (* FIXME: print LOAD and START_GROUP trace *) let (img2, outputs_by_name_with_position) = (build_image a alloc_map empty_elf_memory_image( (Nat_big_num.of_int 0)) outputs_by_name_after_gc bindings_by_name labelled_script control_script_linkable_idx linker_defs_by_name) in (*let _ = errln ("Final image has " ^ (show (Map.size img.elements)) ^ " elements and " ^ (show (Set.size img.by_tag)) ^ " metadata tags, of which " ^ ( let (section_tags, section_ranges) = elf_memory_image_section_ranges img in let section_tags_bare = List.map (fun tag -> match tag with | FileFeature(ElfSection(idx, isec)) -> (idx, isec) | _ -> failwith "not section tag" end) section_tags in show (length section_tags_bare) ) ^ " are sections.") in*) (* The link map output for the section/address assignment basically mirrors our notion of * output section composition. In the following: 0x0000000000400000 PROVIDE (__executable_start, 0x400000) 0x0000000000400190 . = (0x400000 + SIZEOF_HEADERS) .interp *(.interp) .note.ABI-tag 0x0000000000400190 0x20 .note.ABI-tag 0x0000000000400190 0x20 crt1.o .note.gnu.build-id 0x00000000004001b0 0x24 *(.note.gnu.build-id) .note.gnu.build-id 0x00000000004001b0 0x24 crt1.o .hash *(.hash) .gnu.hash *(.gnu.hash) ... we can see that - symbol provision, holes and output sections all get lines - each output section appears with its name left-aligned, and its address, if any, appearing afterwards; if so, the section's total size also follows. - each input query is printed verbatim, e.g. "*(.note.gnu.build-id)" - underneath this, a line is printed for each input section that was included, with its address and size. This can spill onto a second line in the usual way. - holes are shown as "*fill*" - provided symbols are shown as in the linker script source. PROBLEM: we don't have the script in source form, so we can't print the queries verbatim. I should really annotate each query with its source form; when the script is parsed from source, this can be inserted automatically. For the moment, what to do? I could annotate each script element manually. For the moment, for diffing purposes, filter out lines with asterisks. *) (img2, bindings_by_name))
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>