Spaces:
Running
Running
File size: 200,170 Bytes
c61ccee |
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 2789 2790 2791 2792 2793 2794 2795 2796 2797 2798 2799 2800 2801 2802 2803 2804 2805 2806 2807 2808 2809 2810 2811 2812 2813 2814 2815 2816 2817 2818 2819 2820 2821 2822 2823 2824 2825 2826 2827 2828 2829 2830 2831 2832 2833 2834 2835 2836 2837 2838 2839 2840 2841 2842 2843 2844 2845 2846 2847 2848 2849 2850 2851 2852 2853 2854 2855 2856 2857 2858 2859 2860 2861 2862 2863 2864 2865 2866 2867 2868 2869 2870 2871 2872 2873 2874 2875 2876 2877 2878 2879 2880 2881 2882 2883 2884 2885 2886 2887 2888 2889 2890 2891 2892 2893 2894 2895 2896 2897 2898 2899 2900 2901 2902 2903 2904 2905 2906 2907 2908 2909 2910 2911 2912 2913 2914 2915 2916 2917 2918 2919 2920 2921 2922 2923 2924 2925 2926 2927 2928 2929 2930 2931 2932 2933 2934 2935 2936 2937 2938 2939 2940 2941 2942 2943 2944 2945 2946 2947 2948 2949 2950 2951 2952 2953 2954 2955 2956 2957 2958 2959 2960 2961 2962 2963 2964 2965 2966 2967 2968 2969 2970 2971 2972 2973 2974 2975 2976 2977 2978 2979 2980 2981 2982 2983 2984 2985 2986 2987 2988 2989 2990 2991 2992 2993 2994 2995 2996 2997 2998 2999 3000 3001 3002 3003 3004 3005 3006 3007 3008 3009 3010 3011 3012 3013 3014 3015 3016 3017 3018 3019 3020 3021 3022 3023 3024 3025 3026 3027 3028 3029 3030 3031 3032 3033 3034 3035 3036 3037 3038 3039 3040 3041 3042 3043 3044 3045 3046 3047 3048 3049 3050 3051 3052 3053 3054 3055 3056 3057 3058 3059 3060 3061 3062 3063 3064 3065 3066 3067 3068 3069 3070 3071 3072 3073 3074 3075 3076 3077 3078 3079 3080 3081 3082 3083 3084 3085 3086 3087 3088 3089 3090 3091 3092 3093 3094 3095 3096 3097 3098 3099 3100 3101 3102 3103 3104 3105 3106 3107 3108 3109 3110 3111 3112 3113 3114 3115 3116 3117 3118 3119 3120 3121 3122 3123 3124 3125 3126 3127 3128 3129 3130 3131 3132 3133 3134 3135 3136 3137 3138 3139 3140 3141 3142 3143 3144 3145 3146 3147 3148 3149 3150 3151 3152 3153 3154 3155 3156 3157 3158 3159 3160 3161 3162 3163 3164 3165 3166 3167 3168 3169 3170 3171 3172 3173 3174 3175 3176 3177 3178 3179 3180 3181 3182 3183 3184 3185 3186 3187 3188 3189 3190 3191 3192 3193 3194 3195 3196 3197 3198 3199 3200 3201 3202 3203 3204 3205 3206 3207 3208 3209 3210 3211 3212 3213 3214 3215 3216 3217 3218 3219 3220 3221 3222 3223 3224 3225 3226 3227 3228 3229 3230 3231 3232 3233 3234 3235 3236 3237 3238 3239 3240 3241 3242 3243 3244 3245 3246 3247 3248 3249 3250 3251 3252 3253 3254 3255 3256 3257 3258 3259 3260 3261 3262 3263 3264 3265 3266 3267 3268 3269 3270 3271 3272 3273 3274 3275 3276 3277 3278 3279 3280 3281 3282 3283 3284 3285 3286 3287 3288 3289 3290 3291 3292 3293 3294 3295 3296 3297 3298 3299 3300 3301 3302 3303 3304 3305 3306 3307 3308 3309 3310 3311 3312 3313 3314 3315 3316 3317 3318 3319 3320 3321 3322 3323 3324 3325 3326 3327 3328 3329 3330 3331 3332 3333 3334 3335 3336 3337 3338 3339 3340 3341 3342 3343 3344 3345 3346 3347 3348 3349 3350 3351 3352 3353 3354 3355 3356 3357 3358 3359 3360 3361 3362 3363 3364 3365 3366 3367 3368 3369 3370 3371 3372 3373 3374 3375 3376 3377 3378 3379 3380 3381 3382 3383 3384 3385 3386 3387 3388 3389 3390 3391 3392 3393 3394 3395 3396 3397 3398 3399 3400 3401 3402 3403 3404 3405 3406 3407 3408 3409 3410 3411 3412 3413 3414 3415 3416 3417 3418 3419 3420 3421 3422 3423 3424 3425 3426 3427 3428 3429 3430 3431 3432 3433 3434 3435 3436 3437 3438 3439 3440 3441 3442 3443 3444 3445 3446 3447 3448 3449 3450 3451 3452 3453 3454 3455 3456 3457 3458 3459 3460 3461 3462 3463 3464 3465 3466 3467 3468 3469 3470 3471 3472 3473 3474 3475 3476 3477 3478 3479 3480 3481 3482 3483 3484 3485 3486 3487 3488 3489 3490 3491 3492 3493 3494 3495 3496 3497 3498 3499 3500 3501 3502 3503 3504 3505 3506 3507 3508 3509 3510 3511 3512 3513 3514 3515 3516 3517 3518 3519 3520 3521 3522 3523 3524 3525 3526 3527 3528 3529 3530 3531 3532 3533 3534 3535 3536 3537 3538 3539 3540 3541 3542 3543 3544 3545 3546 3547 3548 3549 3550 3551 3552 3553 3554 3555 3556 3557 3558 3559 3560 3561 3562 3563 3564 3565 3566 3567 3568 3569 3570 3571 3572 3573 3574 3575 3576 3577 3578 3579 3580 3581 3582 3583 3584 3585 3586 3587 3588 3589 3590 3591 3592 3593 3594 3595 3596 3597 3598 3599 3600 3601 3602 3603 3604 3605 3606 3607 3608 3609 3610 3611 3612 3613 3614 3615 3616 3617 3618 3619 3620 3621 3622 3623 3624 3625 3626 3627 3628 3629 3630 3631 3632 3633 3634 3635 3636 3637 3638 3639 3640 3641 3642 3643 3644 3645 3646 3647 3648 3649 3650 3651 3652 3653 3654 3655 3656 3657 3658 3659 3660 3661 3662 3663 3664 3665 3666 3667 3668 3669 3670 3671 3672 3673 3674 3675 3676 3677 3678 3679 3680 3681 3682 3683 3684 3685 3686 3687 3688 3689 3690 3691 3692 3693 3694 3695 3696 3697 3698 3699 3700 3701 3702 3703 3704 3705 3706 3707 3708 3709 3710 3711 3712 3713 3714 3715 3716 3717 3718 3719 3720 3721 3722 3723 3724 3725 3726 3727 3728 3729 3730 3731 3732 3733 3734 3735 3736 3737 3738 3739 3740 3741 3742 3743 3744 3745 3746 3747 3748 3749 3750 3751 3752 3753 3754 3755 3756 3757 3758 3759 3760 3761 3762 3763 3764 3765 3766 3767 3768 3769 3770 3771 3772 3773 3774 3775 3776 3777 3778 3779 3780 3781 3782 3783 3784 3785 3786 3787 3788 3789 3790 3791 3792 3793 3794 3795 3796 3797 3798 3799 3800 3801 3802 3803 3804 3805 3806 3807 3808 3809 3810 3811 3812 3813 3814 3815 3816 3817 3818 3819 3820 3821 3822 3823 3824 3825 3826 3827 3828 3829 3830 3831 3832 3833 3834 3835 3836 3837 3838 3839 3840 3841 3842 3843 3844 3845 3846 3847 3848 3849 3850 3851 3852 3853 3854 3855 3856 3857 3858 3859 3860 3861 3862 3863 3864 3865 3866 3867 3868 3869 3870 3871 3872 3873 3874 3875 3876 3877 3878 3879 3880 3881 3882 3883 3884 3885 3886 3887 3888 3889 3890 3891 3892 3893 3894 3895 3896 3897 3898 3899 3900 3901 3902 3903 3904 3905 3906 3907 3908 3909 3910 3911 3912 3913 3914 3915 3916 3917 3918 3919 3920 3921 3922 3923 3924 3925 3926 3927 3928 3929 3930 3931 3932 3933 3934 3935 3936 3937 3938 3939 3940 3941 3942 3943 3944 3945 3946 3947 3948 3949 3950 3951 3952 3953 3954 3955 3956 3957 3958 3959 3960 3961 3962 3963 3964 3965 3966 3967 3968 3969 3970 3971 3972 3973 3974 3975 3976 3977 3978 3979 3980 3981 3982 3983 3984 3985 3986 3987 3988 3989 3990 3991 3992 3993 3994 3995 3996 3997 3998 3999 4000 4001 4002 4003 4004 4005 4006 4007 4008 4009 4010 4011 4012 4013 4014 4015 4016 4017 4018 4019 4020 4021 4022 4023 4024 4025 4026 4027 4028 4029 4030 4031 4032 4033 4034 4035 4036 4037 4038 4039 4040 4041 4042 4043 4044 4045 4046 4047 4048 4049 4050 4051 4052 4053 4054 4055 4056 4057 4058 4059 4060 4061 4062 4063 4064 4065 4066 4067 4068 4069 4070 4071 4072 4073 4074 4075 4076 4077 4078 4079 4080 4081 4082 4083 4084 4085 4086 4087 4088 4089 4090 4091 4092 4093 4094 4095 4096 4097 4098 4099 4100 4101 4102 4103 4104 4105 4106 4107 4108 4109 4110 4111 4112 4113 4114 4115 4116 4117 4118 4119 4120 4121 4122 4123 4124 4125 4126 4127 4128 4129 4130 4131 4132 4133 4134 4135 4136 4137 4138 4139 4140 4141 4142 4143 4144 4145 4146 4147 4148 4149 4150 4151 4152 4153 4154 4155 4156 4157 4158 4159 4160 4161 4162 4163 4164 4165 4166 4167 4168 4169 4170 4171 4172 4173 4174 4175 4176 4177 4178 4179 4180 4181 4182 4183 4184 4185 4186 4187 4188 4189 4190 4191 4192 4193 4194 4195 4196 4197 4198 4199 4200 4201 4202 4203 4204 4205 4206 4207 4208 4209 4210 4211 4212 4213 4214 4215 4216 4217 4218 4219 4220 4221 4222 4223 4224 4225 4226 4227 4228 4229 4230 4231 4232 4233 4234 4235 4236 4237 4238 4239 4240 4241 4242 4243 4244 4245 4246 4247 4248 4249 4250 4251 4252 4253 4254 4255 4256 4257 4258 4259 4260 4261 4262 4263 4264 4265 4266 4267 4268 4269 4270 4271 4272 4273 4274 4275 4276 4277 4278 4279 4280 4281 4282 4283 4284 4285 4286 4287 4288 4289 4290 4291 4292 4293 4294 4295 4296 4297 4298 4299 4300 4301 4302 4303 4304 4305 4306 4307 4308 4309 4310 4311 4312 4313 4314 4315 4316 4317 4318 4319 4320 4321 4322 4323 4324 4325 4326 4327 4328 4329 4330 4331 4332 4333 4334 4335 4336 4337 4338 4339 4340 4341 4342 4343 4344 4345 4346 4347 4348 4349 4350 4351 4352 4353 4354 4355 4356 4357 4358 4359 4360 4361 4362 4363 |
# mypy: ignore-errors
"""
``torch.fx.experimental.symbolic_shapes`` provides interfaces for interacting with
our symbolic shapes reasoning system that is used heavily in torch.compile. Although
this is not generally considered public API, when writing framework code in PyTorch
as well as extensions to PyTorch (e.g., in custom operator implementations), you may
need to make use of these APIs to setup dynamic shapes support appropriately.
"""
import builtins
import collections
import functools
import inspect
import itertools
import logging
import math
import operator
import re
import sys
import threading
import traceback
from collections import defaultdict
from contextlib import contextmanager
from dataclasses import dataclass, field
from enum import Enum
from functools import lru_cache
from typing import (
Any,
cast,
Callable,
Dict,
Iterable,
List,
Optional,
Sequence,
Set,
Tuple,
Type,
Union,
TYPE_CHECKING
)
from typing_extensions import TypeAlias
import torch
import torch.fx
import torch.fx.traceback as fx_traceback
from torch.fx.experimental import _config as config
from torch.fx.experimental.recording import (
FakeTensorMeta,
ShapeEnvEvent,
record_shapeenv_event,
replay_shape_env_events,
shape_env_check_state_equal
)
from torch.fx.experimental.sym_node import SymNode, SymTypes
# NB: The sym_* functions are used via getattr() and must be imported here.
from torch import SymBool, SymFloat, SymInt
from torch._guards import ShapeGuard, Source, TracingContext
from torch.utils._python_dispatch import is_traceable_wrapper_subclass
from torch.utils._sympy.functions import FloorDiv, Mod, IsNonOverlappingAndDenseIndicator
from torch.utils._sympy.solve import try_solve
from torch.utils._sympy.value_ranges import bound_sympy, SymPyValueRangeAnalysis, ValueRanges, ValueRangeError
from torch.utils._sympy.singleton_int import SingletonInt
from torch.utils._traceback import format_frame, CapturedTraceback
from torch._utils_internal import signpost_event
from torch._subclasses.meta_utils import is_sparse_any
from torch._logging import LazyString
if TYPE_CHECKING:
from torch._dynamo.source import TensorPropertySource
InputList = List
DimList = List
log = logging.getLogger(__name__)
class GuardOnDataDependentSymNode(RuntimeError):
pass
import sympy
from sympy.printing.str import StrPrinter
from sympy.printing.precedence import precedence, PRECEDENCE
aten = torch._ops.ops.aten # type: ignore[has-type]
__all__ = [
"has_symbolic_sizes_strides", "create_contiguous", "ShapeEnv", "is_concrete_int",
"guard_int", "guard_float", "guard_scalar", "canonicalize_bool_expr",
"hint_int", "SYMPY_INTERP", "free_symbols", "is_symbol_binding_fx_node",
"is_concrete_bool", "is_nested_int", "SHAPEENV_EVENT_KEY", "CURRENT_NODE_KEY",
"has_free_symbols", "sym_eq", "SymbolicContext", "StatelessSymbolicContext",
"StatefulSymbolicContext", "SubclassSymbolicContext", "statically_known_true",
"guard_size_oblivious",
]
# FX node metadata keys for symbolic shape FX graph.
SHAPEENV_EVENT_KEY = "shapeenv_event"
CURRENT_NODE_KEY = "current_node"
# These are modules that contain generic code for interacting with ShapeEnv
# which are unlikely to identify a particular interesting guard statement
@lru_cache(None)
def uninteresting_files() -> Set[str]:
import torch._inductor.sizevars
import torch._library.abstract_impl
import torch._subclasses.meta_utils
import torch._subclasses.fake_tensor
mods = [
sys.modules[__name__],
torch.fx.experimental.recording,
torch.fx.experimental.sym_node,
torch.fx.interpreter,
torch,
torch._inductor.sizevars,
torch._library.abstract_impl,
torch._subclasses.meta_utils,
torch._subclasses.fake_tensor,
]
return {inspect.getfile(m) for m in mods}
# We don't bother with the metaclass as all of the dispatching logic happens
# entirely from Python
#
# Didn't bother with ancestors for now, unlikely to have multiple modes for
# symints right now
class ConstraintViolationError(RuntimeError):
pass
def has_symbolic_sizes_strides(elem) -> bool:
return elem._has_symbolic_sizes_strides
Int = Union[torch.SymInt, int]
def create_contiguous(shape: Sequence[Int]) -> List[Int]:
strides: List[Int] = [1]
for dim in reversed(shape[:-1]):
strides.append(dim * strides[-1])
return list(reversed(strides))
def hint_int(a: Union[torch.SymInt, int], fallback: Optional[int] = None) -> int:
"""
Retrieve the hint for an int (based on the underlying real values as observed
at runtime). If no hint is available (e.g., because data dependent shapes),
if fallback is not None, use that instead (otherwise raise an error).
"""
if isinstance(a, torch.SymInt):
return a.node.require_hint(fallback)
assert type(a) is int, a
return a
Scalar = Union[torch.SymInt, torch.SymFloat, torch.SymBool, int, float, bool]
def has_hint(a: Scalar) -> bool:
if isinstance(a, SymTypes):
return a.node.has_hint()
return True
def is_concrete_int(a: Union[int, SymInt]) -> bool:
r""" Utility to check if underlying object
in SymInt is concrete value. Also returns
true if integer is passed in.
Args:
a (SymInt or int): Object to test if it int
"""
assert isinstance(a, (SymInt, int))
if isinstance(a, int):
return True
if isinstance(a.node.expr, sympy.core.numbers.Integer):
return True
return False
# In obscure Meta only situations, sympy.logic.boolalg doesn't exist at runtime.
# So make sure only type checker evaluates this alias.
# Xref: https://www.internalfb.com/diff/D53324783
SympyBoolean: TypeAlias = "sympy.logic.boolalg.Boolean"
def guard_size_oblivious(expr: Union[torch.SymBool, bool]) -> bool:
"""
Perform a guard on a symbolic boolean expression in a size oblivious way.
This is typically used when a non-oblivious test would result in a guard
on a data dependent value of which we don't know the value of at compile time.
When a guard is tested this way, we may diverge in behavior from how regular
PyTorch semantics would treat it. For more information, see
https://github.com/pytorch/pytorch/pull/118579
"""
if isinstance(expr, torch.SymBool):
return expr.node.guard_size_oblivious("", 0)
else:
assert isinstance(expr, bool)
return expr
def canonicalize_bool_expr(expr: SympyBoolean) -> SympyBoolean:
r""" Canonicalize a boolean expression by transforming it into a lt / le
inequality and moving all the non-constant terms to the rhs.
We canonicalize And / Ors / Not via cnf and then canonicalize their subexpr
recursively
nb. sympy.Rel.canonical is not good enough https://github.com/sympy/sympy/issues/25924
Args:
expr (sympy.Expr): Expression to canonicalize
"""
# Canonicalise an inequality by transforming it into a lt / le
# inequality and moving all the non-constant terms to the rhs
# We canonicalise And / Ors / Not via cnf
# nb. Relational.canonical in sympy is broken
# https://github.com/sympy/sympy/issues/25924
if not isinstance(expr, (sympy.Rel, sympy.And, sympy.Or, sympy.Not, sympy.Eq, sympy.Ne)):
return expr
if isinstance(expr, (sympy.And, sympy.Or, sympy.Not)):
expr = sympy.logic.boolalg.to_cnf(expr)
return _canonicalize_bool_expr_impl(expr)
def _canonicalize_bool_expr_impl(expr: SympyBoolean) -> SympyBoolean:
"""
After canonicalization, we are guaranteed to have eliminated Ge/Gt relations
(rewriting them to Le/Lt, respectively).
"""
if isinstance(expr, (sympy.And, sympy.Or)):
return type(expr)(*map(canonicalize_bool_expr, expr.args))
opposite = {sympy.Gt: sympy.Lt, sympy.Ge: sympy.Le}
if isinstance(expr, tuple(opposite.keys())):
lhs = expr.rhs - expr.lhs
t = opposite[type(expr)]
else:
assert isinstance(expr, (sympy.Lt, sympy.Le, sympy.Eq, sympy.Ne))
lhs = expr.lhs - expr.rhs
t = type(expr)
rhs = 0
if isinstance(lhs, sympy.Add):
cts = []
variables = []
for term in lhs.args:
if term.is_number:
cts.append(term)
else:
variables.append(term)
lhs = sympy.Add(*variables)
rhs = -sympy.Add(*cts)
return t(lhs, rhs)
def is_concrete_bool(a: Union[bool, SymBool]) -> bool:
r""" Utility to check if underlying object
in SymBool is concrete value. Also returns
true if integer is passed in.
Args:
a (SymBool or bool): Object to test if it bool
"""
assert isinstance(a, (SymBool, bool))
if isinstance(a, bool):
return True
if isinstance(a.node.expr, (sympy.logic.boolalg.BooleanTrue, sympy.logic.boolalg.BooleanFalse)):
return True
return False
def is_nested_int(s):
return isinstance(s, torch.SymInt) and s.node.is_nested_int()
def _iterate_exprs(val: Union[SymInt, torch.Tensor]) -> Iterable[sympy.Basic]:
if isinstance(val, SymTypes):
# This allow applies to the jagged layout NestedTensor case as
# nested ints are not symbolic
if is_symbolic(val):
yield val.node.expr
elif isinstance(val, sympy.Basic):
yield val
elif isinstance(val, (int, float, bool)):
pass
elif is_sparse_any(val):
yield from _iterate_exprs(val.size())
elif isinstance(val, torch.Tensor):
yield from _iterate_exprs(val.size())
yield from _iterate_exprs(val.stride())
yield from _iterate_exprs(val.storage_offset())
elif isinstance(val, (tuple, list)):
for s in val:
yield from _iterate_exprs(s)
elif val is None:
pass
else:
raise AssertionError(f"cannot extract sympy expressions from {val} {type(val)}")
def free_symbols(val: Union[SymInt, torch.Tensor]) -> Set[sympy.Symbol]:
if val is None:
return set()
itr = _iterate_exprs(val)
# we need at least 1 to call union, so we hand code the identity
try:
first_expr = next(itr)
except StopIteration:
return set()
return first_expr.free_symbols.union(*(e.free_symbols for e in itr))
def has_free_symbols(val: Union[SymInt, torch.Tensor]) -> bool:
"""Faster version of bool(free_symbols(val))"""
return not all(e.is_number for e in _iterate_exprs(val))
# Like free_symbols, but filtered to only report unbacked symbols
def free_unbacked_symbols(x):
# NB: keep synced with is_unbacked_symint
return {s for s in free_symbols(x) if s.name.startswith(("u", "f"))}
# WARNING: Don't use this on Dynamo produced graphs, they don't have meta
# setup!
def is_symbol_binding_fx_node(node) -> Optional[sympy.Symbol]:
if (
node.op == "placeholder" and
"val" in node.meta and
isinstance(node.meta["val"], torch.SymInt) and
isinstance(node.meta["val"].node.expr, sympy.Symbol)
):
return node.meta["val"].node.expr
return None
def find_symbol_binding_fx_nodes(graph):
return {
node.meta["val"].node.expr: node
for node in graph.nodes
if is_symbol_binding_fx_node(node)
}
def definitely_true(a):
"""
Returns True only if we can tell that a is True, possibly introducing
a guard in the process. If a depends on some unbacked SymInt, we may
return False even though there may exist a possible value of the SymInt
that would cause the expression to return True.
When is it appropriate to use definitely_true? First, if you can use
a higher level combinator like parallel_or/parallel_and, prefer using
those instead, they are definitely safe (modulo short-circuiting).
Second, it can be used if the program would behave equivalently if
definitely_true always returned False (parallel_or/parallel_and are
examples of this pattern, modulo short-circuiting). Finally, it even
be OK if the program wouldn't behave equivalently, so long as the
change is semantics preserving. It can be semantics preserving if
the program errors in more cases than it did previously (but otherwise
behaves identically), or if it changes some quantity in a way that
doesn't matter (e.g., strides often fall in this bucket.)
"""
if isinstance(a, SymBool):
if a.node.has_hint():
return guard_bool(a)
else:
return False
return bool(a)
def definitely_false(a):
"""
Returns True only if we can tell that a is False, possibly introducing
a guard in the process. If a depends on some unbacked SymInt, we may
return False even though there may exist a possible value of the SymInt
that would cause the expression a to be False. See definitely_true
for more usage guidance.
"""
if isinstance(a, SymBool):
if a.node.has_hint():
return not guard_bool(a)
else:
return False
return not bool(a)
def statically_known_true(x: Union[bool, SymBool]) -> bool:
"""Returns True if x can be simplified to a constant and is true.
.. note::
This function doesn't introduce new guards, so the expression may end
up evaluating to true at runtime even if this function returns False.
Args:
x (bool, SymBool): The expression to try statically evaluating
"""
if isinstance(x, SymBool):
expr = x.node.expr
shape_env = x.node.shape_env
try:
simplified = shape_env._maybe_evaluate_static(expr)
if simplified is not None:
return bool(simplified)
except Exception:
log.debug("Could not simplify %s", expr)
return False
assert isinstance(x, bool)
return x
def parallel_or(*args):
"""
Evaluate the logical OR of several arguments, avoiding guarding on
unbacked SymInts if another argument is definitely True.
"""
if any(statically_known_true(a) for a in args):
return True
if any(definitely_true(a) for a in args):
return True
return any(args)
def parallel_and(*args):
"""
Evaluate the logical FALSE of several arguments, avoiding guarding on
unbacked SymInts if another argument is definitely False.
"""
if any(statically_known_true(torch.sym_not(a)) for a in args):
return False
if any(definitely_false(a) for a in args):
return False
return all(args)
def sym_eq(x, y):
"""
Like ==, but when run on list/tuple, it will recursively test equality
and use sym_and to join the results together, without guarding.
"""
if (isinstance(x, tuple) and isinstance(y, tuple)) or (isinstance(x, list) and isinstance(y, list)):
if len(x) != len(y):
return False
return functools.reduce(operator.and_, map(sym_eq, x, y), True)
elif isinstance(x, (int, torch.SymInt)) and isinstance(y, (int, torch.SymInt)):
return x == y
else:
raise AssertionError(f"unexpected sym_eq between {type(x)} {type(y)}")
def guard_scalar(a):
if isinstance(a, (SymBool, bool)):
return guard_bool(a)
elif isinstance(a, (SymInt, int)):
return guard_int(a)
elif isinstance(a, (SymFloat, float)):
return guard_float(a)
else:
raise AssertionError(f"unrecognized scalar {a}")
@record_shapeenv_event()
def _constrain_symbol_range(shape_env, s: sympy.Symbol, compiler_min: int, compiler_max: int):
upd_vr = ValueRanges(compiler_min, compiler_max)
old_vr = shape_env.var_to_range.get(s, ValueRanges.unknown())
new_vr = shape_env.var_to_range[s] = old_vr & upd_vr
if new_vr != old_vr:
log.info("_constrain_symbol_range %s [%s, %s]", s, new_vr.lower, new_vr.upper)
def _advise_is_size(a):
"""
Don't use this directly; use torch._check_is_size instead.
This is a softer version of _constrain_range_for_size (with min=0,
max=Inf). Instead of forcibly constraining a variable (and erroring if we
failed to constrain it), it will simply advise us that a size is
constrained in some way. We will always defer a runtime assert for this
constraint if we cannot prove it at compile-time, but we we only
*sometimes* learn useful extra information at compile-time with this
information. This is in contrast to constrain_range_for_size, where if
you don't call that on a fresh unbacked symint, chances are we will choke.
TODO: Make Dynamo handle this appropriately if this is seen in Dynamo-ed
code. Right now this is only really used in code with AOTAutograd trace
through, so it is not a big problem that this isn't supported, but in
principle all of this code should be Dynamo'able too.
TODO: I didn't support min/max because I didn't have a use case where this
actually helped. In principle we can support it, it just makes the
implementation below more complicated.
"""
# This must always succeed, because the sole allowed caller _check_is_size
# was responsible for expect_true'ing this
assert a >= 0
# NB: it's important not to constrain range for size for *hinted* SymInts,
# because it is not only unsound, it will immediately trip our asserts
# that hints have to be consistent with static analysis! If you somehow
# have an unbounded SymInt that later constrains to 1, this will be
# inconsistent with the range
if (
isinstance(a, SymInt)
and isinstance(a.node, SymNode)
and not a.node.has_hint()
and isinstance(a.node.expr, sympy.Symbol)
):
_constrain_range_for_size(a)
@record_shapeenv_event()
def _constrain_range_for_size(a, min: Optional[int] = None, max: Optional[int] = None):
"""
This function is NOT INTENDED to be used by itself.
"""
if isinstance(a, (SymFloat, SymBool)):
raise ValueError("Constraining SymFloat/SymBool is nyi")
assert isinstance(a, SymInt), "can only constrain range for SymInt"
assert isinstance(a.node.expr, sympy.Symbol), "constraining non-Symbols NYI"
if min is None:
min = 0
if max is None:
max = sympy.oo
if max < min:
raise ValueError(
"Maximum value to constrain_as_size can't be less than the specified min value, "
"received min={min} and max={max}"
)
_constrain_symbol_range(
a.node.shape_env,
a.node.expr,
compiler_min=min,
compiler_max=max,
)
a.node.shape_env.size_like.add(a.node.expr)
# inclusive both ways
@record_shapeenv_event()
def constrain_range(a, *, min: Optional[int], max: Optional[int] = None):
"""
Applies a constraint that the passed in SymInt must lie between min-max
inclusive-inclusive, WITHOUT introducing a guard on the SymInt (meaning
that it can be used on unbacked SymInts). If min/max are None, we assume
that the dimension is unbounded in that direction. Repeated application
of constrain_range intersects the ranges. This is a fairly low level API
that doesn't have a lot of safety guarantees (TODO: provide higher level
APIs).
Currently, we use this API in the following circumstance: when we allocate
an unbacked SymInt, denoting an integer quantity which is data dependent,
we ordinarily do not know anything about what values it may take. This
means that any sort of guard on it will immediately fail. However, in
many cases, we know something about the unbacked SymInt: for example, we
know that nonzero(x).size(0) must be >= 0. We use constrain_range to
narrow the possible range, declaring that negative symbols are impossible.
This permits to definitely answer True to queries like 'nnz >= 0', even if
we don't know what the actual (hinted) value of 'nnz' is. In fact, we
actually use constrain_range to unsoundly discharge common guards: for an
unbacked SymInt produced by nonzero, we will also assume that it is not
equal to 0/1 (even though these are perfectly possible values at runtime),
because we generally expect graphs that are valid for N=2 to also be valid
for N=1.
"""
if min is None:
min = -sympy.oo
if max is None:
max = sympy.oo
if max < min:
raise ValueError(
"Maximum value to constrain_as_size can't be less than the specified min value, "
"received min={min} and max={max}"
)
if isinstance(a, int):
if not (min <= a <= max):
raise ValueError(f"Invalid value {a} for range [{min}:{max}]")
return
if isinstance(a.node.expr, sympy.Integer):
if not (min <= int(a.node.expr) <= max):
raise ValueRangeError(f"Invalid value {int(a.node.expr)} for range [{min}:{max}]")
return
assert isinstance(a.node.expr, sympy.Symbol), "constraining non-Symbols NYI"
# TODO: Shouldn't we install a guard if the symbol is backed? Or is the
# semantics that this is an "unchecked" assert (but it this actually
# something useful? Might be better to restrict only for unbacked
# SymInt).
_constrain_symbol_range(
a.node.shape_env,
a.node.expr,
compiler_min=min,
compiler_max=max,
)
@record_shapeenv_event()
def constrain_unify(a, b):
"""
Given two SymInts, constrain them so that they must be equal. NB:
this will not work with SymInts that represent nontrivial expressions
(yet!)
"""
# TODO: this does not install a deferred runtime assert yet
# TODO: Maybe dedupe this with _maybe_guard_rel?
if not isinstance(a, SymInt):
if not isinstance(b, SymInt):
assert a == b
else:
assert isinstance(b.node.expr, sympy.Symbol), "constraining non-Symbols NYI"
shape_env = b.node.shape_env
shape_env.replacements[b.node.expr] = sympy.Integer(a)
else:
# TODO: Actually, we can support this as long as one of them is a symbol.
# NB: We can't actually do "unification" as our operators are not
# injective
assert isinstance(a.node.expr, sympy.Symbol), "constraining non-Symbols NYI"
shape_env = a.node.shape_env
if not isinstance(b, SymInt):
shape_env.replacements[a.node.expr] = sympy.Integer(b)
else:
assert a.node.shape_env is b.node.shape_env
assert isinstance(b.node.expr, sympy.Symbol), "constraining non-Symbols NYI"
new_var = shape_env._find(a.node.expr)
shape_env.replacements[b.node.expr] = new_var
# Assume that a boolean is true for the purposes of subsequent symbolic
# reasoning. This will keep track of corresponding runtime checks to verify
# that the result is upheld: either as a regular guard, or as a special set
# of asserts which are triggered when an unbacked SymInt is allocated.
#
# DO NOT use this function for these cases:
#
# - This is inappropriate for "branching" conditions (where both
# true and false result in valid programs). We will always assume
# the condition evaluates true, and so it will never be possible
# to trace the false condition when you use it. For true branching
# on unbacked SymInts, you must use torch.cond; if you incorrectly
# use expect_true in this case, you will make the false branch
# unreachable (as we will simply assume that only the true branch
# is ever exercised).
#
# - This is inappropriate for situations where you know some other system
# invariant guarantees that this property holds, since you don't
# really need to insert a runtime check in that case. Use something
# like constrain_range in that case.
#
# This API has a hitch. To avoid having to reimplement error reporting
# capabilities, this function CAN return False. The invariant is that
# the surrounding code must raise an error when this function returns
# False. This is quite low level, so we recommend using other functions
# like check() which enforce this in a more intuitive way.
#
# By the way, this name is a nod to the __builtin_expect macro,
# which is used similarly (but unlike __builtin_expect, you MUST fail
# in the unlikely branch.) (I think expect is a good name; in recent
# versions of C++, this is replaced with [[likely]], which is weaker
# and not accurate for this function!)
def expect_true(a, skip: int = 0):
if isinstance(a, SymBool):
# TODO: check perf implications of this
frame = inspect.currentframe()
for _ in range(skip + 1): # always run this loop at least once
frame = frame.f_back
return a.node.expect_true(frame.f_code.co_filename, frame.f_lineno)
assert type(a) is bool, a
return a
def guard_bool(a):
if isinstance(a, SymBool):
return a.node.guard_bool("", 0) # NB: uses Python backtrace
assert type(a) is bool, a
return a
def guard_int(a):
if isinstance(a, SymInt):
return a.node.guard_int("", 0) # NB: uses Python backtrace
assert type(a) is int, a
return a
def guard_float(a):
if isinstance(a, SymFloat):
return a.node.guard_float("", 0) # NB: uses Python backtrace
assert isinstance(a, float), a
return a
# Given a GraphModule, return all the FakeTensors for all the placeholders
def fx_placeholder_vals(gm):
return [n.meta['val'] for n in gm.graph.nodes if n.op == "placeholder"]
def fx_placeholder_targets(gm):
return [n.target for n in gm.graph.nodes if n.op == "placeholder"]
# Given a GraphModule and arguments to run it with, evaluate that the guards
# for its associated ShapeEnv are satisfied by the passed arguments. This
# WILL check for duck sizing.
def eval_guards(gm, *args, ignore_static=True):
return gm.shape_env.evaluate_guards_for_args(fx_placeholder_vals(gm), args, ignore_static=ignore_static)
def bind_symbols(gm, *args):
return gm.shape_env.bind_symbols(fx_placeholder_vals(gm), args)
def _assert_bound_is_rational(expr: sympy.Expr, bound: ValueRanges):
"""
We assert that the bounds are either Boolean, or not finite, or can be computed
in exact prevision via rational arithmetic.
The only exception to this is the rare case when the user calls `sqrt(s0)`
sqrt is turned into sympy.Pow so we just match for that (it matches more things, but still)
"""
assert bound.lower.is_rational or bound.lower.is_Boolean or not bound.lower.is_finite or expr.has(sympy.Pow), (bound, expr)
assert bound.upper.is_rational or bound.upper.is_Boolean or not bound.upper.is_finite or expr.has(sympy.Pow), (bound, expr)
class DimDynamic(Enum):
"""
Controls how to perform symbol allocation for a dimension. It is always
sound to default this to DYNAMIC, but the policies DUCK and STATIC can
result in better trace-time and compile-time performance, as they reduce
the number of allocated symbols and generally make your graph more static.
NB: If we notice you've applied a constraint to the dimension, we will
force it to DYNAMIC for simplicity.
DimDynamic is controlled by a variety of higher level UX features.
Currently:
- In eager mode, the default policy is DUCK.
- The default is changed to STATIC with assume_static_by_default.
- An individual dim is marked DYNAMIC if you mark_dynamic_dim.
- In export mode, the default policy is STATIC.
- An individual dim is marked DYNAMIC if you mention it as dynamic_dim
in the constraints kwarg.
"""
# Treat the dimension symbolically
DYNAMIC = 0
# Treat the dimension symbolically, but if its hint matches another
# dynamic dimension, unify the two symbols ("duck sizing")
DUCK = 1
# Treat the dimension statically based on its hint
STATIC = 2
# NB: These constraints affect both clients and backends: given some
# constraint C, the client must pass inputs that satisfy the constraint,
# while a backend must not introduce guards BEYOND this constraint.
# For clarity, we document the implications on both sides for both the client
# and the backend.
#
# NB: These constraints are on a *single* dimension. In principle, we could
# also have multi-dimension constraints, but our guess is that this is not
# actually useful and so we are not supporting it right now.
#
# NB: Strict constraints are typically only suitable for export, as in eager
# a backend like inductor may validly introduce extra, discretionary guards
# to improve performance of code. A StrictMinMaxConstraint would be brittle
# under future optimizations performed by inductor; we don't guarantee
# eager code with StrictMinMaxConstraint will keep working in the future!
@dataclass(frozen=True)
class Constraint:
warn_only: bool
@dataclass(frozen=True)
class StrictMinMaxConstraint(Constraint):
"""
For clients: the size at this dimension must be within 'vr' (which
specifies a lower and upper bound, inclusive-inclusive) AND it
must be non-negative and should not be 0 or 1 (but see NB below).
For backends: there must not be any guards on this dimension which
are not implied by the given lower and upper bound. Regardless of
the lower bound, the backend can assume the size is non-negative
and that it is not 0 or 1.
An unbounded StrictMinMaxConstraint can be thought of as a strict version
of "RelaxedUnspecConstraint".
NB: Export will often unsoundly assume that a graph works for 0/1, even
though at trace time we assumed size is not 0 or 1. The idea is that
if we produce a graph that works for a range of values, it will be OK
for N=0/1 too.
"""
vr: ValueRanges
def render(self, source: Source):
"""Format the constrain equation"""
# TODO: better printing for -oo and oo
return f"{self.vr.lower} <= {source.name()} <= {self.vr.upper}"
@dataclass(frozen=True)
class RelaxedUnspecConstraint(Constraint):
"""
For clients: no explicit constraint; constraint is whatever is implicitly
inferred by guards from tracing.
For backends: there must exist at least TWO possible values for the
size at this dimension which satisfy the guards for this dimension.
In other words, this constraint helps us distinguish between "we don't
care if this dimension specializes or not" versus "this dimension must be
unspecialized." However, this constraint doesn't say very much about what
specialization is permitted; for example, if we guard on a size being
even, this would still be acceptable under an unspec constraint. This
makes RelaxedUnspecConstraint useful for eager mode, where your backend compiler
may add constraints to otherwise dynamic dimensions; we can't assert that
there are NO guards as this is brittle because compilers should be able to
add extra constraints. If you want to assert that there are no guards,
use StrictMinMaxConstraint with an unbounded ValueRanges.
"""
def render(self, source: Source):
return f"RelaxedUnspecConstraint({source.name()})"
# NB: None here indicates the client constraint is whatever is implicitly
# inferred by guards from tracing, and that a backend can add whatever guards
# it wants (including fully specializing the value).
DimConstraint = Union[StrictMinMaxConstraint, RelaxedUnspecConstraint, None]
@dataclass(frozen=True)
class EqualityConstraint(Constraint):
"""
Represent and decide various kinds of equality constraints between input sources.
A "source pair" is a pair of input sources for dynamic dimensions that
are specified equal. We represent `source_pairs` in a union-find forest
so that we can efficiently check whether two such sources are transitively equal.
A "derived equality" relates an input source to an expression over a root.
The root can be another input source, corresponding to some dynamic dimension,
or a phantom symbol that does not directly represent any dynamic dimension. We
represent `derived_equalities` involving input sources in a transitively-closed map
so that we can efficiently check whether an input source is transitively equal to
a given expression over another input source.
(NOTE: In contrast, it is easy to decide whether an input source is transitively equal
to a given expression over a phantom symbol; such expressions are already in canonical
form and so the problem reduces to symbolic expression equality.)
"""
source_pairs: List[Tuple[Source, Source]]
derived_equalities: List[Tuple[Source, Union[Source, sympy.Symbol], Callable[[sympy.Expr], sympy.Expr]]]
phantom_symbols: List[sympy.Symbol]
def __post_init__(self):
"""Pre-processing to answer queries `is_equal` and `is_derived` below.
Example: Suppose we are given:
source_pairs [a = b, b = c]
derived_equalities [d = c + 1, e = d - 1]
We first construct a union find with source_pairs:
_parents = {a: a, b: a, c: a}
Then we compute canonical symbolic expressions, recursively applying derived_equalities
until we bottom out:
_defs = {d: c + 1, e: (c + 1) - 1 aka c}
"""
# self._parents is a map from input sources to input sources where, conceptually,
# these are directed edges in a union-find forest
_parents: Dict[Source, Source] = {}
object.__setattr__(self, "_parents", _parents)
# self._defs is a map from input sources to "canonical" symbolic expressions,
# i.e., unary expressions with symbols that corresponds to regular Dims (i.e.,
# not derived Dims)
_defs: Dict[Source, sympy.Expr] = {}
object.__setattr__(self, "_defs", _defs)
for source1, source2 in self.source_pairs:
# preprocess into a union-find forest
self._union(self._find(source1), self._find(source2))
for source, root, fn in self.derived_equalities:
# preprocess into a transitively-closed map
# NOTE(avik): we reuse the union-find forest for canonicalizing input sources
if isinstance(root, sympy.Symbol):
self._defs[self._find(source)] = fn(root)
else:
self._defs[self._find(source)] = fn(self._rewrite(root))
def _find(self, source):
# chase edges to find the root of this equivalence class
if source in self._parents:
return self._find(self._parents[source])
else:
return source
def _union(self, root1, root2):
# merge two equivalence classes by adding an edge from one root to the other
if root1 != root2:
self._parents[root1] = root2
def _rewrite(self, src):
# always represent the given source by the root of its equivalence class
src = self._find(src)
if src in self._defs:
# simply look up the definition if it exists
# NOTE(avik): This works because definitions are always transitively-closed;
# otherwise we would have to do recursive rewriting.
return self._defs[src]
else:
# otherwise, create a symbol representing the source
return sympy.Symbol(src.name())
def is_equal(self, source1, source2):
return (
# check whether source1 and source2 have the same root
self._find(source1) == self._find(source2) or
# check whether source1 is derived equal to source2
self.is_derived(source1, source2, lambda x: x)
)
def is_derived(self, src, symbol_src, fn):
# check whether both src and symbol_src have the same definition
return self._rewrite(src) == fn(self._rewrite(symbol_src))
def _assert_symbol_context(symbolic_context):
assert isinstance(symbolic_context, SymbolicContext), "Invalid symbolic_context object"
assert type(symbolic_context) is not SymbolicContext, "Illegal usage of symbolic_context ABC"
@dataclass(frozen=True)
class SymbolicContext:
"""
Data structure specifying how we should create symbols in
``create_symbolic_sizes_strides_storage_offset``; e.g., should
they be static or dynamic.
This is an abstract base class because we are probably going to add
another version of this that says "use exactly these SymInts, don't
allocate fresh symbols."
"""
pass
@dataclass(frozen=True)
class StatelessSymbolicContext(SymbolicContext):
"""
Create symbols in ``create_symbolic_sizes_strides_storage_offset`` via
a symbolic_context determination as given by ``DimDynamic`` and ``DimConstraint``.
This will cause fresh symbols to be allocated
"""
dynamic_sizes: DimList[DimDynamic]
constraint_sizes: DimList[DimConstraint] = None
# If the tensor is a view, this should be populated for the base. It contains
# information on how to allocate symbols when recursively fakeifying the base
# during view fake-ification.
view_base_context: Optional[SymbolicContext] = None
# TODO: add storage offset and stride symbolic_context
def __post_init__(self):
if self.constraint_sizes is None:
object.__setattr__(self, 'constraint_sizes', [None] * len(self.dynamic_sizes))
# note [Tensor Fakification and Symbol Caching]
#
# As of the time of this note, dynamo creates a fresh fake tensor mode for backends.
# The reason we do this is because there are certain classes of operations, namely,
# metadata mutations, that change tensor size, stride, etc. This means that the fake tensor
# state at the end of a dynamo trace is different than the fake tensor state at the beginning
# of a trace. Backends like aot_autograd need a fresh fake tensor to correctly track metadata mutation,
# view relationships, etc.
#
# As we create a new fake mode, we also lose the memoization that comes with it. Rather than
# transfer the memoization cache, we instead transfer the shape env. However, with this
# comes nuance - as dynamo is selective in how it makes symbolic shapes. Due to strategies in
# automatic dynamic and constraints, the policy for which dims are dynamic is nuanced and varies across
# recompilations.
#
# In order to preserve the symbolic decisions made during dynamo tensor fakification, we pass
# a StatefulSymbolicContext at creation time. This object is tracked, per tensor, on the TracingContext.
# The lifecycle of this object should match the lifecycle of the original dynamo tracked tensor, and it is
# safe to reuse this object as many times as necessary to create a fake tensor. Fake tensors
# created with new fake modes should produce the same exact symbols as the original, providing the same shape_env
# is used.
# TODO(voz): Shape env validation
@dataclass(frozen=True)
class StatefulSymbolicContext(StatelessSymbolicContext):
"""
Create symbols in ``create_symbolic_sizes_strides_storage_offset`` via
a symbolic_context determination as given by a cache of Source:Symbol. A cache hit
will reuse a stored symbol, and a cache miss will write to this cache.
This behaves like StatelessSymbolicContext, except the cache supersedes the
other values - dynamic_sizes and constraint_sizes will not be read if we cache
hit.
It is the cache owners responsibility to maintain the lifecycle of the cache
w/r/t different shape_envs, clearing, etc.
"""
tensor_source: Source = None
# Why is this keyd on int first?
# That integer is actually the id of the shape_env. This cache short-circuits symbol
# creation, and we must store it per shape env. Now, while tracing invariants are a single
# shape env per tracing context, and every new frame gets a new shape_env. So where would we have
# multiple shape envs? The answer lies in recording. When we are replaying, replay_shape_env_events
# is invoked, and creates a new shape_env. Replaying events against this new shape_env will
# cause it to fail with unknown symbols, as the symbols cached here will skip creation, and never
# get recorded in var_to_val, etc.
# TODO(voz): consider a weakref to the shape_env here
shape_env_to_source_to_symbol_cache : Dict[int, Dict["TensorPropertySource", "sympy.Expr"]] = None
def __post_init__(self):
# The None default is annoying, but required because of dataclass limitations
assert self.tensor_source is not None
if not self.shape_env_to_source_to_symbol_cache:
object.__setattr__(self, 'shape_env_to_source_to_symbol_cache', {})
@dataclass(frozen=True)
class SubclassSymbolicContext(StatefulSymbolicContext):
"""
The correct symbolic context for a given inner tensor of a traceable tensor subclass
may differ from that of the outer symbolic context. This structure allows for this
flexibility, with inner symbolic contexts mapped via attr -> symbolic context.
"""
inner_contexts: Dict[str, SymbolicContext] = None
def __post_init__(self):
super().__post_init__()
if self.inner_contexts is None:
self.inner_contexts = {}
def is_symbolic(val: Union[int, SymInt, float, SymFloat, bool, SymBool]) -> bool:
if isinstance(val, (int, float, bool)):
return False
return val.node.is_symbolic()
IndicatorTypes = (IsNonOverlappingAndDenseIndicator,)
@lru_cache(256)
def safe_expand(r):
if hasattr(r, 'expand'):
try:
return sympy.expand(r)
except RecursionError:
log.warning("RecursionError in sympy.expand(%s)", r)
return r
else:
return r
def error():
raise AssertionError("shouldn't be hit")
# TODO: Deduplicate this with torch/_prims_common/__init__.py
def eval_is_non_overlapping_and_dense(sizes, strides):
return int(guard_bool(_eval_is_non_overlapping_and_dense(sizes, strides)))
def _eval_is_non_overlapping_and_dense(sizes, strides):
dim = len(sizes)
# Short-circuits for tensors of rank one, which are
# non-overlapping and "dense" if their stride is one
# or it is a 0/1 element tensor
if dim == 1:
return strides[0] == 1 or sizes[0] < 2
# Checks that there exists a permutation of the strides s.t. the tensor would be contiguous
# Sorts (length, stride) pairs by stride
lengths_and_strides = sorted(
zip(sizes, strides), key=operator.itemgetter(1)
)
# Unlike the C++ code, we don't move the 0/1 size dimensions to the
# end. So we have to keep going for this code.
expected_stride = 1
for length, stride in lengths_and_strides:
if length == 1:
continue
if stride != expected_stride:
return False
expected_stride *= length
return True
def cast_symbool_to_symint_guardless(symbool: torch.SymBool) -> torch.SymInt:
int_sym = sympy.Piecewise((1, symbool.node.expr), (0, True))
return symbool.node.shape_env.create_symintnode(int_sym, hint=int(symbool.node.require_hint()))
SYMPY_INTERP = {
'Abs': operator.abs,
'Eq': operator.eq,
'Ne': operator.ne,
'Gt': operator.gt,
'Lt': operator.lt,
'Le': operator.le,
'Ge': operator.ge,
'Min': min,
'Max': max,
'Mod': operator.mod,
'FloorDiv': operator.floordiv,
'TrueDiv': operator.truediv,
'IsNonOverlappingAndDenseIndicator': eval_is_non_overlapping_and_dense,
'floor': math.floor,
'ceiling': math.ceil,
'cast_symbool_to_symint_guardless': cast_symbool_to_symint_guardless,
'Round': builtins.round,
'RoundDecimal': builtins.round,
}
def _lru_cache(fn, maxsize=None):
"""
Wrapper around lru_cache that clears when new info about shapes has been
updated.
Use lru_cache if the output is always the same, regardless of the
constraints we know now (i.e. evaluate_expr)
Use _lru_cache otherwise.
Also note that this depends on _update_version_counter being called on the
shape environment whenever the constraints are updated, otherwise the cache
will not be cleared.
"""
fn_cache = lru_cache(maxsize)(fn)
prior_version = 0
if config.validate_shape_env_version_key:
prior_key = None
@functools.wraps(fn)
def wrapper(self, *args, **kwargs):
nonlocal prior_version, prior_key
if prior_key is None:
prior_key = self._get_key()
if prior_version != self._version_counter:
fn_cache.cache_clear()
prior_version = self._version_counter
prior_key = self._get_key()
else:
assert prior_key == self._get_key(), \
"ShapeEnv cache key changed without version being updated!"
return fn_cache(self, *args, **kwargs)
else:
@functools.wraps(fn)
def wrapper(self, *args, **kwargs):
nonlocal prior_version
if prior_version != self._version_counter:
fn_cache.cache_clear()
prior_version = self._version_counter
return fn_cache(self, *args, **kwargs)
wrapper.cache_clear = fn_cache.cache_clear
wrapper.cache_info = fn_cache.cache_info # type: ignore[attr-defined]
return wrapper
# This is pretty similar to ShapeGuard but it also comes with a message,
# and is exclusively used for things that MUST be true (unlike guards,
# which can evaluate False, in which case you just choose not to use
# a particular specialization)
@dataclass(frozen=True)
class RuntimeAssert:
expr: sympy.Expr
msg: str = field(repr=False)
stack: str = field(repr=False)
class ShapeGuardPrinter(StrPrinter):
def __init__(
self,
symbol_to_source,
source_ref,
var_to_sources,
):
super().__init__()
self.symbol_to_source = symbol_to_source
self.source_ref = source_ref
self.var_to_sources = var_to_sources
def _print_Not(self, expr):
return 'not %s' % (self.parenthesize(expr.args[0], PRECEDENCE["Not"]))
def _print_And(self, expr):
return self.stringify(expr.args, " and ", PRECEDENCE["And"])
def _print_Or(self, expr):
return self.stringify(expr.args, " or ", PRECEDENCE["Or"])
def _print_Symbol(self, expr) -> str:
assert isinstance(expr, sympy.Symbol), str(type(expr))
def repr_symbol_to_source():
return repr({
symbol: [s.name() for s in sources]
for symbol, sources in self.symbol_to_source.items()
})
assert self.symbol_to_source.get(expr), (
f"{expr} (could be from {[s.name() for s in self.var_to_sources[expr]]}) "
f"not in {repr_symbol_to_source()}. If this assert is failing, it could be "
"due to the issue described in https://github.com/pytorch/pytorch/pull/90665"
)
return self.source_ref(self.symbol_to_source[expr][0])
class LoggingShapeGuardPrinter(ShapeGuardPrinter):
def __init__(self, var_to_sources):
super().__init__(var_to_sources, lambda n: n.name(), var_to_sources)
class DynamicDimConstraintPrinter(StrPrinter):
"""
Printer for dynamic dim constraints.
- Instead of t.size()[d] it prints dynamic_dim(t, d)
- Instead of Eq(_, _), Mod(_, _), etc. it prints _ == _, _ % _, etc.
We use this to suggest code for specifying dynamic dim constraints.
"""
def __init__(self, symbol_to_source, source_name_to_debug_name):
super().__init__()
self.symbol_to_source = symbol_to_source
self.source_name_to_debug_name = source_name_to_debug_name
def print_source(self, source) -> str:
if self.source_name_to_debug_name:
return source.name()
return f"dynamic_dim({source.base.name()}, {source.idx})"
def _print_Symbol(self, expr) -> str:
assert isinstance(expr, sympy.Symbol), str(type(expr))
assert self.symbol_to_source.get(expr), (
f"Unknown symbol {expr} created by constraints solver"
)
return self.print_source(self.symbol_to_source[expr][0])
def _print_Relational(self, expr):
return '{} {} {}'.format(
self.parenthesize(expr.lhs, precedence(expr)),
expr.rel_op,
self.parenthesize(expr.rhs, precedence(expr))
)
class DimConstraints:
"""
Custom solver for a system of constraints on symbolic dimensions.
Solutions are "static" values or simplified "dynamic" constraints.
"""
def __init__(self, symbol_to_source, var_to_val, marked_dynamic, source_name_to_debug_name):
# We try to solve systems of inequalities with 1 free variable.
self._univariate_inequalities: Dict[sympy.Symbol, Set[sympy.Expr]] = defaultdict(set)
# Among them, we prioritize solving for a free variable that has equalities.
# NOTE: _symbols_with_equalities is always a subset of _univariate_inequalities.keys()
# and removing a symbol from the former => removing it from the latter.
self._symbols_with_equalities: Set[sympy.Symbol] = set()
# A solution of a free variable with equalities becomes a substitution.
# We use these substitutions to simplify other constraints.
# NOTE: removing a symbol from _symbols_with_equalities => adding it to _substitutions.
self._substitutions: Dict[sympy.Symbol, sympy.Integer] = {}
# In general, constraints may have // and % operations.
# Of course, // can be expressed in terms of / and %.
# Our inequality solver can handle / but not %. So we need to transform them away.
# We do so by using the values of variables as hints to evaluate %.
# For soundness we record additional congruence guards and solve them separately.
self._var_to_val: Dict[sympy.Symbol, sympy.Integer] = var_to_val
self._congruences: Set[sympy.Expr] = defaultdict(set)
# We do not try to (directly) solve inequalities with > 1 free variables.
# NOTE: free variables in these inequalities cannot also be in _substitutions.
self._multivariate_inequalities: Set[sympy.Expr] = set()
# We park external equalities between free variables here.
self._symbolic_equivalences: List[Tuple[Source, sympy.Expr]] = []
# Solutions come in two forms:
# - (static) specializations
# - (dynamic) inequalities / congruences
self._static_results: Set[str] = set()
self._dynamic_results: Set[str] = set()
# printer for solutions
self._dcp = DynamicDimConstraintPrinter(symbol_to_source, source_name_to_debug_name)
# inconsistencies found on substituting with concrete values / static solutions
self._inconsistencies: List[str] = []
# symbols that are marked dynamic
self._marked_dynamic = marked_dynamic
def rewrite_with_congruences(self, s, expr):
"""
Eliminate expressions of the form b // d and b % d while adding congruences of the form b % d == k.
This leaves rational operators (in particular of the form b / d) that our inequality solver can handle.
We solve the added congruences separately (using our congruence solver, see below).
"""
def mod_handler(*args):
# Suppose that we have an expression of the form b % d with free variable s.
# Using the value of s as a "hint," we can evaluate b % d to a value k.
# Then we can rewrite b % d to k while adding the guard b % d == k.
# NOTE(avik): This abstraction is provably sound but, in general, incomplete. It is complete IFF
# the original expression always evaluates to a constant value (i.e., it does not vary with s).
# In other words,
# - solutions of s with the rewritten expression are guaranteed to also be solutions of s with
# the original expression;
# - while it may be possible to find solutions of s with the original expression that are not
# solutions with the rewritten expression, in that case the original expression cannot evaluate
# to the same value for all solutions of s.
#
# Should we be worried about this incompleteness? No, because of the following reasons:
# 1. It unblocks dramatic simplification that would not be otherwise possible with current tech
# (i.e., "don't let perfect be the enemy of the good").
# 2. We already have a tradition of using hints to add guards in the compiler for making progress.
# 3. We have not yet seen a counterexample arise in practice! In particular, any congruence guards
# we generate (or simplify to) seem to be of the form b % d == k where k is a constant.
#
# Here's a theoretical counterexample: 3*s % (s + 1) == s - 2, that is satisfied by all s >= 2.
# With any hint (say) s = k, we'd rewrite this to: 3*s % (s + 1) == k - 2. But, substituting, we
# would then get k - 2 == s - 2, and thus s = k as the (only, constant) solution!
base, divisor = args
base, divisor = self.rewrite_with_congruences(s, base), self.rewrite_with_congruences(s, divisor)
mod_reduced = base.subs(self._var_to_val) % divisor.subs(self._var_to_val)
congruence = (base - mod_reduced) % divisor
if congruence != 0:
self._congruences[s].add(congruence)
return mod_reduced
def floor_div_handler(*args):
# Suppose that we have an expression of the form b // d with free variable s.
# Using the value of s, we can evaluate b % d to a value k.
# Then we can rewrite b // d to (b - k) / d, while adding the guard b % d == k.
# NOTE(avik): This is exactly equivalent to rewriting b // d as (b - (b % d)) / d
# and eliminating b % d as above.
base, divisor = args
base, divisor = self.rewrite_with_congruences(s, base), self.rewrite_with_congruences(s, divisor)
mod_reduced = base.subs(self._var_to_val) % divisor.subs(self._var_to_val)
congruence = (base - mod_reduced) % divisor
if congruence != 0:
self._congruences[s].add(congruence)
return (base - mod_reduced) / divisor
if expr.has(Mod):
expr = expr.replace(Mod, mod_handler)
if expr.has(FloorDiv):
expr = expr.replace(FloorDiv, floor_div_handler)
return expr
def add(self, expr) -> bool:
"""Add an expression to the set of constraints.
Return whether the expression is a trivial constraint (i.e., an obvious tautology).
"""
if expr == sympy.true:
return True
orig_expr = expr
orig_reduced = orig_expr.subs(self._var_to_val)
# TODO(avik): https://github.com/pytorch/pytorch/issues/101093
# It is possible that `expr` will fail the consistency check because of
# precision errors. Specifically, on substituting its free symbols with
# their concrete values, we might end up comparing floats. Until we have
# a fix for this issue, we delay raising such failures. See solve().
if orig_reduced == sympy.false:
self._inconsistencies.append(f"{orig_expr} is inconsistent!")
if isinstance(expr, sympy.Ne):
# we're not going to do anything useful with these, so drop them
return False
free_symbols = expr.free_symbols
assert free_symbols, f"Did not expect constraint with no free variables: {expr}"
if len(free_symbols) > 1:
# multivariate: record and move on
self._multivariate_inequalities.add(expr)
else:
# univariate: can solve these immediately
s = next(iter(free_symbols))
# eliminate // and % (see documentation of `rewrite_with_congruences` above)
old_n_congruences = len(self._congruences[s])
expr = self.rewrite_with_congruences(s, expr)
new_n_congruences = len(self._congruences[s])
if expr == sympy.true:
return old_n_congruences == new_n_congruences
reduced = expr.subs(self._var_to_val)
if reduced == sympy.false:
self._inconsistencies.append(
f"{expr}, obtained by rewriting {orig_expr} with congruences, "
"is inconsistent!"
)
if isinstance(expr, sympy.Eq):
# special status for symbols that have equalities (see `solve` below)
self._symbols_with_equalities.add(s)
self._univariate_inequalities[s].add(expr)
return False
def add_equality(self, source, expr):
"""Add an equality constraint"""
if expr.is_number:
# specialization, right here
self._static_results.add(f"{source.name()} == {expr}")
else:
# these will resolve to either specializations or dynamic equality constraints
self._symbolic_equivalences.append((source, expr))
def _reduce_congruences(self):
reduced_congruences = {}
for s, congruences in self._congruences.items():
remainder_modulus_pairs = []
congruences_to_check = set()
for congruence in congruences:
base, divisor = congruence.args
# We are given a congruence of the form base % divisor == 0 with a free variable s. So:
# - we transform this into an equation of the form base = divisor * tmp;
# - we solve this equation for s to get a linear solution with free variable tmp.
tmp = sympy.Symbol("tmp", integer=True)
symbol, solution = sympy.solve_linear(base - divisor * tmp, symbols=[s])
# See https://docs.sympy.org/latest/modules/solvers/solvers.html#sympy.solvers.solvers.solve_linear
# for how to interpret the results.
if s == symbol:
# This means the solution is of the form s = modulus*tmp + remainder.
modulus, remainder = sympy.polys.polytools.div(solution, tmp)
if isinstance(modulus, sympy.Integer) and isinstance(remainder, sympy.Integer):
# Make sure 0 <= remainder <= modulus.
remainder = remainder % modulus
remainder_modulus_pairs.append((remainder, modulus))
continue
# This means that we did not get a unique solution to the equation.
# No problem, we will check it.
congruences_to_check.add(congruence)
# Finally we solve for a congruence s such that s = r_i mod m_i for each (r_i, m_i).
# The solution will be a congruence of the form s = r mod m.
# NOTE(avik): Since the given m_i may not be pairwise coprime, we can't just use CRT.
if remainder_modulus_pairs:
remainder, modulus = sympy.ntheory.modular.solve_congruence(*remainder_modulus_pairs)
reduced_congruences[s] = {(s - remainder) % modulus}
substitution = {s: modulus * sympy.Symbol("tmp", integer=True) + remainder}
reduced_congruences[s].update(
congruence for congruence in congruences_to_check
if not sympy.checksol(congruence, substitution)
)
else:
reduced_congruences[s] = congruences_to_check
return reduced_congruences
def _raise_inconsistencies(self):
if self._inconsistencies:
msg = "\n".join(self._inconsistencies)
self._inconsistencies.clear()
raise ValueError(f"The following inconsistencies were found:\n{msg}")
def _force_specialization(self, s):
val = self._var_to_val[s]
self._static_results.add(f"{self._dcp.symbol_to_source[s][0].name()} == {val}")
self._substitutions[s] = val
def _specialize_divisor_symbols(self):
for expr in self._multivariate_inequalities:
for atom in expr.atoms(FloorDiv, Mod):
_, divisor = atom.args
for s in divisor.free_symbols:
self._force_specialization(s)
multivariate_inequalities = self._multivariate_inequalities
self._multivariate_inequalities = set()
for expr in multivariate_inequalities:
self.add(expr.subs(self._substitutions))
self._raise_inconsistencies()
self._univariate_inequalities = {
s: exprs
for s, exprs in self._univariate_inequalities.items()
if s not in self._substitutions
}
self._congruences = {
s: congruences
for s, congruences in self._congruences.items()
if s not in self._substitutions
}
def solve(self, disable_congruences=True, disable_equivalences=True):
"""Solve the system of constraint equations to find simplified constraints
"""
self._raise_inconsistencies()
# as long as there are symbols with equalities, solve for them
# NOTE(avik): this is guaranteed to terminate (#iterations <= #symbols)
while self._symbols_with_equalities:
s = self._symbols_with_equalities.pop()
exprs = self._univariate_inequalities.pop(s)
solution = sympy.solvers.inequalities.reduce_inequalities(exprs, s)
if isinstance(solution, sympy.And):
solution = next((arg for arg in solution.args if isinstance(arg, sympy.Eq)), solution)
assert isinstance(solution, sympy.Eq), f"Expected an equality constraint for {s}, got {solution}"
symbol, val = solution.args
assert symbol == s, f"Expected a constraint on {s} instead of on {symbol}"
# because this is univariate, the solution is a specialization
self._static_results.add(f"{self._dcp.symbol_to_source[s][0].name()} == {val}")
# add this as a substitution to simplify other constraints
self._substitutions[s] = val
# simplify multivariate inequalities: some of them will now become univariate!
multivariate_inequalities = self._multivariate_inequalities
self._multivariate_inequalities = set()
for expr in multivariate_inequalities:
self.add(expr.subs(s, self._substitutions[s]))
self._raise_inconsistencies()
self._specialize_divisor_symbols()
# solve linear congruences
# NOTE(avik): We do not need to solve them for symbols that have already been specialized.
reduced_congruences = self._reduce_congruences()
for s, congruences in reduced_congruences.items():
for congruence in congruences:
# any congruence that cannot be checked becomes a dynamic constraint as well
if s not in self._substitutions or not sympy.checksol(congruence, {s: self._substitutions[s]}):
if self._is_supported_congruence(congruence):
base, divisor = congruence.args
tmp_name = f"_{self._dcp.source_name_to_debug_name[self._dcp.symbol_to_source[s][0].name()]}"
tmp = sympy.Symbol(tmp_name, integer=True)
from torch._dynamo.source import ConstantSource
self._dcp.symbol_to_source[tmp] = [ConstantSource(tmp_name)]
r = try_solve(sympy.Eq(base, divisor * tmp), s)
self._dynamic_results.add(self._dcp.doprint(sympy.Eq(s, r[1])))
elif disable_congruences:
self._force_specialization(s)
self._univariate_inequalities.pop(s, None)
# remaining symbols have only pure inequalities (no equalities)
for s, exprs in self._univariate_inequalities.items():
try:
solution = sympy.solvers.inequalities.reduce_inequalities(exprs, s)
# because this is univariate, the solution is a dynamic (range) constraint
if isinstance(solution, sympy.Or):
solution = next(iter(arg for arg in solution.args if arg.subs(self._var_to_val)))
if isinstance(solution, sympy.And):
for arg in solution.args:
self._dynamic_results.add(self._dcp.doprint(arg))
else:
self._dynamic_results.add(self._dcp.doprint(solution))
except (NotImplementedError, AssertionError) as e:
log.warning("Failed to reduce inequalities: %s", e)
for expr in exprs:
self._dynamic_results.add(self._dcp.doprint(expr))
# simplify symbolic equivalences: some of them will now become specializations!
symbolic_equivalences = self._symbolic_equivalences
self._symbolic_equivalences = []
for source, expr in symbolic_equivalences:
if disable_equivalences and not self._is_supported_equivalence(expr):
for s in expr.free_symbols:
self._force_specialization(s)
sexpr = self._dcp._print_Symbol(s)
self._dynamic_results = {r for r in self._dynamic_results if sexpr not in r}
self.add_equality(source, expr.subs(self._substitutions))
# remaining symbolic equivalences become dynamic equality constraints
for source, expr in self._symbolic_equivalences:
self._dynamic_results.add(f"{self._dcp.print_source(source)} == {self._dcp.doprint(expr)}")
@classmethod
def _is_supported_equivalence(cls, expr):
# Currently supported Dim ops are linear expressions with integer coefficients.
# So check that expr only contains +, *, ints, and a single occurrence of a symbol.
# (See also documentation of dynamic_shapes._DerivedDim.)
if isinstance(expr, (sympy.Add, sympy.Mul)):
lhs, rhs = expr.args
return (
(cls._is_supported_equivalence(lhs) and isinstance(rhs, sympy.Integer)) or
(isinstance(lhs, sympy.Integer) and cls._is_supported_equivalence(rhs))
)
return isinstance(expr, sympy.Symbol)
@classmethod
def _is_supported_congruence(cls, congruence):
base, divisor = congruence.args
# Congruences that can be currently expressed with supported Dim ops are
# of the form (x + a) % b == 0, where x is a Dim and a and b are constants.
# This allows us to derive x as b*y - a for some Dim y.
# (See also documentation of dynamic_shapes._DerivedDim.)
if isinstance(base, sympy.Add):
lhs, rhs = base.args
cond = (
(isinstance(lhs, sympy.Symbol) and isinstance(rhs, sympy.Integer)) or
(isinstance(lhs, sympy.Integer) and isinstance(rhs, sympy.Symbol))
)
else:
cond = isinstance(base, sympy.Symbol)
cond = cond and isinstance(divisor, sympy.Integer)
return cond
def forced_specializations(self):
"""Returns a dictionary of the names of symbols to their specialized value
"""
def debug_name(src):
name = src.name()
if self._dcp.source_name_to_debug_name:
return f"{self._dcp.source_name_to_debug_name[name]} = {name}"
else:
return name
return {
debug_name(self._dcp.symbol_to_source[s][0]): val
for s, val in self._substitutions.items()
if s in self._marked_dynamic
}
def remove_redundant_dynamic_results(self):
"""Remove constraints of the form 2 <= dynamic_dim(...) as 2 is the default
lower bound.
"""
candidates_for_removal = []
dynamic_results = set()
for dc in self._dynamic_results:
# Instead of 2 <= dynamic_dim(...) simply suggest dynamic_dim(...).
# There is no change in behavior since 2 is the default lower bound.
dc_ = re.sub(r"2 <= dynamic_dim(.+)", r"dynamic_dim\1", dc)
if dc != dc_:
candidates_for_removal.append(dc_)
else:
dynamic_results.add(dc_)
for dc in candidates_for_removal:
# remove dynamic_dim(t, 0) as a constraint when dynamic_dim(t, 0) also
# appears as part of another constraint
found = False
for other_dc in dynamic_results:
if dc in other_dc:
found = True
if not found:
dynamic_results.add(dc)
self._dynamic_results = dynamic_results
def prettify_results(
self,
original_signature: inspect.Signature,
constraint_violation_error=None,
forced_specializations=None,
):
"""Format a message for constraint violation erros"""
if self._dcp.source_name_to_debug_name:
def transform(s):
for k, v in self._dcp.source_name_to_debug_name.items():
s = s.replace(k, v)
return s
results = defaultdict(dict)
def flip(op):
if op == "<=":
return ">="
if op == ">=":
return "<="
if op == "<":
return ">"
if op == ">":
return "<"
assert op == "=="
return op
def relation_with_digit(expr, op, digit):
if op == "<=":
results[expr]["max"] = digit
elif op == "<":
results[expr]["max"] = digit - 1
elif op == ">=":
results[expr]["min"] = digit
elif op == ">":
results[expr]["min"] = digit + 1
else:
assert op == "=="
results[expr]["eq"] = digit
for s in self._static_results.union(self._dynamic_results):
t = transform(s)
if t == s:
continue
left, op, right = re.split(r"( == | <= | >= | < | > )", t)
op = op.strip()
if op == "==" and left == right:
continue
if right.isdigit():
relation_with_digit(left, op, int(right))
elif left.isdigit():
relation_with_digit(right, flip(op), int(left))
else:
assert op == "=="
results[left]["eq"] = sympy.sympify(right)
buf = ""
debug_names = set()
if forced_specializations:
debug_names.update(k.split(" = ")[0] for k in forced_specializations.keys())
buf += (
f"Specializations unexpectedly required ({', '.join(debug_names)})! "
"For more information, run with TORCH_LOGS=\"+dynamic\".\n"
)
for s, val in forced_specializations.items():
buf += f" - {s} must be specialized to {val} because the guards generated for it are too complex.\n"
dims = []
others = []
match = None
if constraint_violation_error:
match = re.search(r"Constraints violated \((.*)\)", constraint_violation_error.args[0])
if match is not None:
debug_names.update(match.expand(r'\1').split(', '))
for k, c in sorted(results.items()):
# if k not in debug_names:
# continue
if "eq" in c:
other = c["eq"]
if isinstance(other, int):
others.append(f"{k} = None # {other}")
elif self._is_supported_equivalence(other):
s = next(iter(other.free_symbols))
if s not in results:
modulus, remainder = sympy.polys.polytools.div(other, s)
c_min = c.get("min", 2)
min_ = math.ceil((c_min - remainder) / modulus)
c_max = c.get("max", sys.maxsize - 1)
max_ = math.floor((c_max - remainder) / modulus)
dims.append(f"{s} = Dim('{s}', min={min_}, max={max_}) # {c_min} <= {other} <= {c_max}")
others.append(f"{k} = {other}")
else:
min_ = c.get("min", None)
if min_ == 2:
min_ = None
max_ = c.get("max", None)
if min_ is not None and max_ is not None:
dims.append(f"{k} = Dim('{k}', min={min_}, max={max_})")
elif min_ is not None:
dims.append(f"{k} = Dim('{k}', min={min_})")
elif max_ is not None:
dims.append(f"{k} = Dim('{k}', max={max_})")
else:
dims.append(f"{k} = Dim('{k}')")
buf += "\nSuggested fixes:\n "
buf += "\n ".join(dims + others)
return buf
# Note: Model inputs are wrapped as LocalSource in dynamo.
# LocalSource.name() wraps the name with L[""]. We use regular
# expression to do the replacement to avoid traversing up
# the source hierarchy manually.
def extract_and_rewrite_local(dc):
match = re.search(r"L\['(.+?)'\]", dc)
if match is None:
return
arg = match.expand(r'\1')
dc = re.sub(r"L\['(.+?)'\]", r'\1', dc)
return arg, dc
def group(results, args_index):
groups = defaultdict(list)
for dc in results:
local = extract_and_rewrite_local(dc)
if local is None:
# This can happen, e.g., with `assume_constant_result`.
# In that case, we drop the constraint.
# TODO(avik) Maybe we should generate an assertion here?
continue
arg, dc = local
if arg in args_index:
groups[args_index[arg]].append(dc)
else:
# This can happen, e.g., with decorators that change the signature.
# In that case, we drop the constraint. Seems hard to do better. :/
# TODO(avik) Maybe warn that `arg` in not in `signature`?
continue
sorted_groups = []
for idx, dcs in sorted(groups.items()):
_, arg = idx
sorted_groups.append((arg, sorted(dcs)))
return sorted_groups
signature = original_signature.replace(return_annotation=inspect.Signature.empty)
args_index = {}
for i, arg in enumerate(signature.parameters.keys()):
args_index[arg] = (i, arg)
def print_results(grouped, indent, result_fn):
nonlocal buf
space = False
for arg, results in grouped:
if space:
buf += "\n"
else:
space = True
buf += f"\n{indent}# {arg}:"
for result in results:
buf += f"\n{indent}{result_fn(result)}"
buf = ""
if forced_specializations:
buf += (
"Some dynamic dimensions need to be specialized because "
"the constraints inferred for them are too complex to specify.\n"
)
for s, val in forced_specializations.items():
buf += f" - {s}, which was marked dynamic, must be specialized to {val}.\n"
indent = 4 * " "
if self._static_results:
grouped_static_results = group(self._static_results, args_index)
buf += "\nThe following dimensions have been specialized and CANNOT be dynamic."
buf += f"\n```\ndef specializations{str(signature)}:"
print_results(
grouped_static_results,
indent,
lambda result: f"assert {result}",
)
buf += "\n```\n"
if self._dynamic_results:
grouped_dynamic_results = group(self._dynamic_results, args_index)
buf += "\nThe following dimensions CAN be dynamic."
buf += "\nPlease use the following code to specify the constraints they must satisfy:"
buf += f"\n```\ndef specify_constraints{str(signature)}:"
buf += f"\n{indent}return ["
print_results(
grouped_dynamic_results,
indent * 2,
lambda result: f"{result},",
)
buf += f"\n{indent}]\n```\n"
return buf
TLS = threading.local()
class ShapeEnv:
# This is a wrapper over the actual __init__ function.
#
# Where to add a new constructor parameter to ShapeEnv?
# =====================================================
# This __init__ function should be used only for parameters related to event recording.
# These are parameters that we don't wish to pass down the road to new ShapeEnv instances
# created from replaying events.
#
# If you wish to add a parameter to the constructor of ShapeEnv, unrelated to event
# recording, do so in the _init function.
def __init__(
self, *,
should_record_events: Optional[bool] = None,
tracked_fakes: Optional[List[Any]] = None,
**kwargs
) -> None:
self._init(**kwargs)
# Disable event recording when replaying.
kwargs["should_record_events"] = False
from torch.fx.experimental.validator import translation_validation_enabled
self._translation_validation_enabled = translation_validation_enabled()
# If not specified, enable event recording if both:
# - Translation validation is on
# - Translation validation bisection is not disabled
self.should_record_events = (
should_record_events
if should_record_events is not None
else (
self._translation_validation_enabled
and not config.translation_validation_no_bisect
)
)
# Enable event recording check if both:
# - It should record events
# - The recording check is enabled
self.check_recorded_events = (
self.should_record_events and config.check_shape_env_recorded_events
)
# This will make sure we only record the top-level function call.
self.is_recording = not self.should_record_events
# Keep track of the list of tracked fakes.
self.tracked_fakes = tracked_fakes
# List of events for reconstructing ShapeEnv at arbitrary points in time.
self.events: List[ShapeEnvEvent] = (
[ShapeEnvEvent(ShapeEnv, kwargs=kwargs)] if self.should_record_events else []
)
# Pro-tip: if you add new field to ShapeEnv, this affects some accept
# tests. Accept their output with:
#
# EXPECTTEST_ACCEPT=1 python test/dynamo/test_dynamic_shapes.py -k test_shape_env_equal
#
def _init(
self, *,
allow_scalar_outputs=True,
allow_dynamic_output_shape_ops=True,
# NB: These are legacy configuration that help us make good choices
# when the constraint/dynamic dims are not explicitly passed to us.
# Ideally we will fix all call sites to be explicit and not have
# implicit choices, but this apparently was pretty involved.
assume_static_by_default=False,
# Note - On 0/1 specialization
#
# The following options affect decisions we make about eager
# specialization. Disabling them will increase trace time (as we do
# more symbolic reasoning) and can also harm the quality of generated
# code (because inductor may not be able to specialize for bounds
# being equal--although if we later respecialize because of a guard,
# your code may be just as good as it was before.)
#
# When True, eagerly specialize input sizes which have 0/1.
specialize_zero_one=True,
# When True, assume input sizes which have the same size are
# symbolically equal.
duck_shape=True,
# For debugging
co_fields=None,
# XXX Add any new settings that could affect FakeTensor evaluation
# to: torch._subclasses.fake_tensor._ShapeEnvSettings
):
# Not directly used by ShapeEnv; indirectly used by FakeTensor
self.allow_scalar_outputs = allow_scalar_outputs
self.allow_dynamic_output_shape_ops = allow_dynamic_output_shape_ops
self.guards: List[ShapeGuard] = []
# Maps symbolic ints to their original concrete values
# Currently populated from tensors
self.var_to_val: Dict[sympy.Symbol, sympy.Integer] = {}
# Maps symbolic ints to their min/max range. These ranges
# are conservative: the int MUST fall in the range, but the
# range may contain ints which may not actually appear in
# practice
self.var_to_range: Dict[sympy.Symbol, ValueRanges] = {}
self.source_name_to_debug_name: Dict[str, str] = {}
self.var_to_sources: Dict[sympy.Symbol, List[Source]] = {}
self.var_to_stack: Dict[sympy.Symbol, CapturedTraceback] = {}
# Maps from sympy ints to expressions representing them
# Populated from equality guards (i.e. a.shape[0] == b.shape[0])
self.replacements: Dict[sympy.Symbol, sympy.Expr] = {}
# Set holds a % b expressions that evaluate to 0.
self.divisible: Set[sympy.Expr] = set()
# Set that holds "size-like" symbols. When we perform
# "size-oblivious" tests, these can be assumed to be >= 2.
self.size_like: Set[sympy.Symbol] = set()
# Duck-shaping says that if two input tensors have the same size,
# they get assigned the same symbolic variable
self.val_to_var: Dict[int, sympy.Expr] = {}
if specialize_zero_one:
self.val_to_var = {0: sympy.Integer(0), 1: sympy.Integer(1)}
self.unbacked_symfloat_counter = itertools.count()
self.unbacked_symint_counter = itertools.count()
# Similar to guards, but these MUST evaluate to true and can
# only be evaluated at runtime midway through (i.e., they always
# involve unbacked symints)
#
# For efficiency reasons, we index in the following way. Suppose you have
# a runtime assert i0 + i1 <= s1. We pick the most recently allocated
# symbol in the source expression and add the assert to the list for
# that symbol e.g., {i1: [i0 + i1 <= s1]}.
#
# We access the runtime asserts in two situations:
#
# - When we are guarding on an expression, we will attempt to
# statically evaluate it, in case the unbacked SymInts can
# simplify away. If we have a runtime assert, we may be able
# to discharge the guard entirely. We only need to attempt
# runtime asserts that mention freevars of the expression in
# question.
#
# - When we are performing codegen (in Inductor for eager, or
# when finalizing the export FX graph), we need to know what
# extra runtime asserts to insert. Whenever an unbacked
# SymInt comes into scope, all runtime asserts involving it
# become eligible for insertion (so long as all of their other
# free unbacked symbols are also in scope). We technically
# can handle any choice of key by kicking inexpressible asserts
# to the next unbacked symbol to wait on, but if we choose the
# latest key, an assert will only show up at the moment when
# we can actually codegen it.
self.deferred_runtime_asserts: Dict[sympy.Symbol, List[RuntimeAssert]] = {}
# This exists so we can efficiently invalidate the cache (it's used as
# part of the cache key); otherwise we'd have to iterate through
# deferred_runtime_asserts to compute its length
self.num_deferred_runtime_asserts = 0
self.assume_static_by_default = assume_static_by_default
self.specialize_zero_one = specialize_zero_one
self.duck_shape = duck_shape
self.log = log
self.log.debug("create_env")
self.frozen = False
self.dim_constraints: Optional[DimConstraints] = None
self.counter = collections.Counter()
# Mapping from sympy.Symbol to the number of guards which mention this
# symbol
self.symbol_guard_counter = collections.Counter()
# A selection of important fields on co_field; solely used for
# signpost_event
self.co_fields = co_fields if co_fields else {}
# Version counter used to invalidate cached values
self._prev_cache_key = self._get_key()
self._version_counter = 0
# Cache for FX nodes.
# Maps an already built node a tuple of:
# 1. node's target
# 2. list of arguments
# This drastically reduces the size of the FX graph, avoiding
# duplicated nodes.
self.fx_node_cache: Dict[Tuple[Callable, Tuple[Any, ...]], torch.fx.Node] = {}
self.source_to_symbol: Dict[str, sympy.Symbol] = {}
from torch.fx.experimental.validator import translation_validation_enabled
self._translation_validation_enabled = translation_validation_enabled()
if self._translation_validation_enabled:
from torch.fx.experimental.validator import TranslationValidator
self.validator = TranslationValidator()
self.graph = torch.fx.Graph()
# Create an output graph and start inserting before that.
# This is needed when 'deepcopy'-ing this object.
self.graph.inserting_before(self.graph.output(None))
# Mapping of each node name to the node itself.
#
# This is useful for matching an FX node from a recorded ShapeEnv.graph
# to the FX node of the ShapeEnv we are running the event on.
#
# Whenever you add a node to self.graph, you must add a mapping to this
# variable. Otherwise, the built FX graph on the replayed ShapeEnv will
# not be valid.
self.name_to_node: Dict[str, torch.fx.Node] = {}
def check_equal(self, other: "ShapeEnv") -> None:
"""Compare another ShapeEnv for equivalence
"""
# ShapeEnv fields that are not relevant for the outcome of
# ShapeEnv.produce_guards call:
# - Debugging variables
# - Translation validation related variables
# - Events recording related variables
non_state_variable_names = (
"counter",
"log",
"var_to_stack",
"fx_node_cache",
"graph",
"validator",
"check_recorded_events",
"should_record_events",
"is_recording",
"tracked_fakes",
"events",
"source_name_to_debug_name",
"_prev_cache_key",
"_version_counter",
)
# Mapping of the value of each to-be-compared field into the values that
# should actually be compared.
#
# You should modify this if, for example, the field that holds state and
# debugging information. e.g. ShapeGuard holds the actual guard (sympy.Expr)
# and the stack when it was added to the set of guards. In order to compare
# it, we throw away the stack information.
def map_value(key: str, value: Any) -> Any:
if key in ("unbacked_symfloat_counter", "unbacked_symint_counter"):
from copy import copy
# For itertools.count(), we compare the next integer returned
# by the count iterators. Not that we need to copy the iterator
# first. Otherwise we are mutating the object.
return next(copy(value))
elif key == "guards":
# Transform the list of ShapeGuard into a list of expressions.
return [g.expr for g in value]
elif key == "deferred_runtime_asserts":
# Transform the list of RuntimeAsserts into a list of expressions.
return {s: [ra.expr for ra in ras] for s, ras in value.items()}
elif key == "name_to_node":
# Compare just the set of keys is the same.
return set(value.keys())
elif key == "symbol_guard_counter":
# Skip this for comparisons
return None
return value
shape_env_check_state_equal(self, other, non_state_variable_names, map_value)
def _snapshot_tracked_fakes(self) -> Optional[List[Any]]:
if self.tracked_fakes is None:
return None
from torch._dynamo.variables.builder import TrackedFake
def maybe_transform_fake(fake: TrackedFake):
inner_fake = fake.fake \
if isinstance(fake.fake, torch.SymInt) \
else FakeTensorMeta.from_fake(fake.fake)
# Even though TrackedFake accepts either a Union[SymInt, FakeTensor], here we give it a
# FakeTensorMeta for two reasons:
# 1. this is all the information we need when recording ShapeEnvEvents.
# 2. it works even if each TrackedFake changes its metadata.
return TrackedFake(inner_fake, fake.source, fake.symbolic_context) # type: ignore[arg-type]
return [maybe_transform_fake(fake) for fake in self.tracked_fakes]
def _last_event_index(self) -> int:
return len(self.events) - 1
@contextmanager
def _recording(self):
self.is_recording = True
try:
yield
finally:
self.is_recording = False
@record_shapeenv_event()
def freeze(self):
"""Freeze this ShapeEnv to stop accumulating guards
A frozen ShapeEnv will ignore any further guards generated on it and
only emit a warning which may lead to accuracy problems.
"""
self.frozen = True
def _create_symbol_for_source(self, source: Source) -> Optional[sympy.Symbol]:
if not self._translation_validation_enabled:
return None
srcname = source.name()
if source not in self.source_to_symbol:
self.source_to_symbol[srcname] = sympy.Symbol(srcname, integer=True)
return self.source_to_symbol[srcname]
def _add_z3var(self, symbol: sympy.Symbol, type: Type) -> None:
if self._translation_validation_enabled:
self.validator.add_var(symbol, type)
def _add_target_expr(self, expr) -> None:
if self._translation_validation_enabled:
self.validator.add_target_expr(expr)
def _add_assertion(self, expr) -> None:
if self._translation_validation_enabled:
self.validator.add_assertion(expr)
def _check_translation_validate(self) -> None:
if self._translation_validation_enabled:
self.validator.validate()
@record_shapeenv_event()
def _create_fx_call_function(
self,
op: Callable,
args: Tuple,
) -> Tuple[Optional[torch.fx.Node], bool]:
# Cache this tuple in order to avoid duplicated nodes.
node_key = (op, args)
# Flags whether the returned node was cached or not.
fresh = False
if self._translation_validation_enabled and node_key not in self.fx_node_cache:
from torch.fx.experimental.validator import z3op
# Presence of None in the arguments implies that we should ignore this operation.
if any(a is None for a in args):
# We check if we are not mixing SymNode that should not be ignored
# (fx_node is not None) with those that should (fx_node is None).
assert all(not isinstance(a, torch.fx.Node) for a in args)
return None, fresh
fresh = True
lifted_op = z3op(op, self.validator)
# If translation validation is enabled, all arguments must have its
# own FX node.
assert all(a is not None for a in args), f"missing arg in FX graph ({op.__name__}): {args}"
node = self.fx_node_cache[node_key] = self.graph.call_function(lifted_op, args)
self.name_to_node[node.name] = node
return self.fx_node_cache.get(node_key, None), fresh
def _create_fx_placeholder_and_z3var(
self,
symbol: sympy.Symbol,
type: Type,
) -> Optional[torch.fx.Node]:
if not self._translation_validation_enabled:
return None
node_key = (self.graph.placeholder, (symbol,))
# Check if we haven't added this symbol already.
# If so, skip the placeholder creation, as it
# generates invalid Python code.
if node_key not in self.fx_node_cache:
# Add a Z3 variable according to 'type'.
self._add_z3var(symbol, type)
# Create the FX placeholder out of a mangled name.
mangled_name = re.sub(r'[^a-zA-Z0-9]', '_', re.sub(r'[()]', '', symbol.name))
node = self.fx_node_cache[node_key] = self.graph.placeholder(mangled_name)
self.name_to_node[node.name] = node
# Attach the 'symbol' to the placeholder so that we can retrieve
# the Z3 variable later.
node.meta["symbol"] = symbol
return self.fx_node_cache[node_key]
def _remove_fx_node(self, node: Optional[torch.fx.Node]) -> None:
if self._translation_validation_enabled and node is not None:
self.name_to_node.pop(node.name)
self.graph.erase_node(node)
def _add_fx_node_metadata(self, node: torch.fx.Node) -> None:
from torch._dynamo.utils import get_current_node
if self.should_record_events:
node.meta[SHAPEENV_EVENT_KEY] = self._last_event_index()
node.meta[CURRENT_NODE_KEY] = get_current_node()
def _suppress_guards_tls(self):
return getattr(TLS, "suppress_guards", False)
@record_shapeenv_event()
def _suppress_guards_enter(self):
TLS.suppress_guards = True
@record_shapeenv_event()
def _suppress_guards_exit(self):
TLS.suppress_guards = False
@contextmanager
def suppress_guards(self):
"""Context manager to ignore all guards generated inside"""
self._suppress_guards_enter()
try:
yield
finally:
self._suppress_guards_exit()
def _get_key(self):
"""
Defines the current "state" of the guards we've accumulated in this ShapeEnv.
Determines when we need to invalidate our cache
"""
return (len(self.replacements), len(self.divisible), self.num_deferred_runtime_asserts)
def _update_version_counter(self):
# The shape environment is queried orders of magnitude more often than
# it is changed, so we summarise the cache key into a linearly
# increasing version counter which is cheaper to check in _lru_cache
# Only update version counter if the state actually changed
cur_key = self._get_key()
if self._prev_cache_key != cur_key:
self._prev_cache_key = cur_key
self._version_counter += 1
def _produce_dyn_sizes(self,
ex_size: Sequence[int],
source: Source,
symbolic_context: SymbolicContext
) -> List[sympy.Expr]:
return self._produce_dyn_sizes_from_int_tuple(tuple(ex_size), source, symbolic_context)
def _produce_dyn_sizes_from_int_tuple(self,
tensor_size: Tuple[int],
source: Source,
symbolic_context: SymbolicContext,
) -> List[sympy.Expr]:
assert all(not is_symbolic(val) for val in tensor_size), f"Expect size to be a plain tuple of ints but got {tensor_size}"
from torch._dynamo.source import TensorPropertySource, TensorProperty
_assert_symbol_context(symbolic_context)
dynamic_dims = symbolic_context.dynamic_sizes
constraint_dims = symbolic_context.constraint_sizes
size = []
for i, val in enumerate(tensor_size):
size.append(self.create_symbol(
val,
TensorPropertySource(source, TensorProperty.SIZE, i),
dynamic_dims[i],
constraint_dims[i],
symbolic_context=symbolic_context
))
return size
def create_symbolic_sizes_strides_storage_offset(
self,
ex: torch.Tensor,
source: Source,
*,
symbolic_context: Optional[SymbolicContext] = None,
):
"""
Returns a list of symbolic sizes and strides for the given tensor.
We try our best to express stride in terms of the sizes, so as to not
introduce new symbolic variables.
"""
# Dynamo may want to wrap FakeTensors with SymInt sizes up e.g. make_fx(opt_f(), tracing_mode="symbolic").
# We create symbols in shape_env using the backed hints behind SymInt.
# Case 1: when SymInt is backed, dynamo can proceed with FakeTensors that have concrete shape.
# produce_guards will trigger specializations on the outer stuff
# Case 2: when the SymInt is unbacked, we will throw an data dependent error in require_hint().
#
# It's probably good for now but it's important to note that this approach has implications for
# the original shape_env when checking guards in different order.
# Example:
# ---------
# Consider a function "opt_f" as shown below:
# @torch.compile()
# def opt_f(x: bool, y: Tensor):
# if x == True:
# return y + torch.randn([4])
# else:
# return y
# Depending on the sequence of calls, we might install two different sets of guards:
# 1. opt_f(False, y):
# - "x == False" (always works for any size y)
# 2. opt_f(True, y):
# - Triggers recompilation and results in guards like:
# - "x == True and y.size(0) == 4"
# - (or "y.size(0) == 4 and x == True")
# The order of checking the guards matters. In this specific example:
# If True branch guard check precedes False branch and for True branch, y.size(0) check precedes x == True,
# we may have an unnessary shape speciliazation for y.
def maybe_specialize_sym_int_with_hint(maybe_sym) -> int:
assert isinstance(maybe_sym, (int, torch.SymInt))
if is_symbolic(maybe_sym):
assert maybe_sym.node.shape_env is not self, \
"expect the symbol is created from an shape env other than current one."
return maybe_sym.node.require_hint()
return maybe_sym
ex_size = tuple(maybe_specialize_sym_int_with_hint(sz) for sz in ex.size())
ex_stride = tuple(maybe_specialize_sym_int_with_hint(sd) for sd in ex.stride())
ex_storage_offset = maybe_specialize_sym_int_with_hint(ex.storage_offset())
return self._create_symbolic_sizes_strides_storage_offset(
ex_size,
ex_stride,
ex_storage_offset,
[_is_dim_dynamic(ex, i) for i in range(ex.dim())],
source,
symbolic_context=symbolic_context,
)
@record_shapeenv_event()
def _create_symbolic_sizes_strides_storage_offset(
self,
ex_size: Sequence[int],
ex_stride: Sequence[int],
ex_storage_offset: int,
is_dim_dynamic: Sequence[bool],
source: Source,
*,
symbolic_context: Optional[SymbolicContext] = None,
):
dim = len(ex_size)
# Reimplement the legacy behavior
if symbolic_context is None:
constraint_dims = [None] * dim
dynamic_dims = []
for i in range(dim):
# NB: This is encapsulation breaking! Legacy behavior was
# bad.
if is_dim_dynamic[i]:
r = DimDynamic.DYNAMIC
elif self.assume_static_by_default:
r = DimDynamic.STATIC
else:
r = DimDynamic.DUCK
dynamic_dims.append(r)
dynamic_dims = [DimDynamic.DUCK] * dim
# symbolic_context is None - set one
symbolic_context = StatelessSymbolicContext(dynamic_sizes=dynamic_dims, constraint_sizes=constraint_dims)
# We got a StatelessSymbolicContext
_assert_symbol_context(symbolic_context)
constraint_dims = symbolic_context.constraint_sizes
dynamic_dims = symbolic_context.dynamic_sizes
# TODO: make this configurable from outside symbolic_context; we made a symbolic_context
# decision here where if all sizes are static, we are going to
# specialize all of the inner strides/offset too. We don't have to
# do this, and arguably we should ALWAYS allow for dynamic offset,
# this is cheap.
# TODO: This should be DYNAMIC, using DUCK for BC
dynamic_strides_offset = DimDynamic.STATIC if all(r == DimDynamic.STATIC for r in dynamic_dims) else DimDynamic.DUCK
assert len(dynamic_dims) == dim, f"{len(dynamic_dims)} != {dim}"
assert len(constraint_dims) == dim
from torch._dynamo.source import TensorPropertySource, TensorProperty
size: List[sympy.Expr] = self._produce_dyn_sizes_from_int_tuple(ex_size, source, symbolic_context)
stride: List[Optional[sympy.Expr]] = [None] * len(size)
for i, val in enumerate(ex_stride):
if val in (0, 1):
stride[i] = sympy.Integer(val)
while any(x is None for x in stride):
candidates = {
ex_size[i] * ex_stride[i]: size[i] * stride[i]
for i in range(len(size))
if stride[i] is not None and ex_stride[i] >= 0
}
# iterate over unbound strides in sorted order
def _nested_int_aware_sort(tup):
return (
# Order nested ints by their coefficients.
# 1 here to order nested ints after non-nested-ints.
(1, tup[0].node.nested_int_coeff(), tup[1]) if is_nested_int(tup[0])
else (0, *tup)
)
val_list = sorted(
[(ex_stride[i], i) for i in range(len(stride)) if stride[i] is None],
key=_nested_int_aware_sort,
)
for _, i in val_list:
if stride[i] is None and ex_stride[i] in candidates:
stride[i] = candidates[ex_stride[i]]
candidates[ex_size[i] * ex_stride[i]] = size[i] * stride[i]
if any(x is None for x in stride):
# bind the smallest unbound stride to a new variable
val, i = min(
[
(ex_stride[i], i)
for i in range(len(stride))
if stride[i] is None
], key=_nested_int_aware_sort
)
stride[i] = self.create_symbol(
val,
TensorPropertySource(source, TensorProperty.STRIDE, i),
dynamic_dim=dynamic_strides_offset,
constraint_dim=None,
symbolic_context=symbolic_context,
)
assert all(x is not None for x in stride)
sym_sizes = [
self.create_symintnode(
sym,
hint=hint,
source=TensorPropertySource(source, TensorProperty.SIZE, i),
)
for i, (sym, hint) in enumerate(zip(size, ex_size))
]
sym_stride = []
for i, stride_expr in enumerate(stride):
# NB: Don't duck size the stride; instead use the expression
# we computed
assert stride_expr is not None
sym_stride.append(self.create_symintnode(
stride_expr, hint=ex_stride[i], source=TensorPropertySource(source, TensorProperty.STRIDE, i)))
sym_storage_offset = self.create_symintnode(
self.create_symbol(
ex_storage_offset,
TensorPropertySource(source, TensorProperty.STORAGE_OFFSET),
dynamic_dim=dynamic_strides_offset,
constraint_dim=None,
symbolic_context=symbolic_context
),
hint=ex_storage_offset,
source=TensorPropertySource(source, TensorProperty.STORAGE_OFFSET))
return tuple(sym_sizes), tuple(sym_stride), sym_storage_offset
@record_shapeenv_event()
def create_symintnode(
self,
sym: "sympy.Expr",
*,
hint: Optional[int],
source: Optional[Source] = None,
):
"""Create a SymInt value from a symbolic expression
If you know what the current hint value of the SymInt to be created
is, pass it into hint. Otherwise, pass None and we will make our best
guess
"""
source_name = source.name() if source else None
if self._translation_validation_enabled and source is not None:
# Create a new symbol for this source.
symbol = self._create_symbol_for_source(source)
assert symbol is not None
# Create a new FX placeholder and Z3 variable for 'symbol'.
fx_node = self._create_fx_placeholder_and_z3var(symbol, int)
# Add an equality assertion for the newly created symbol and 'sym'.
self._add_assertion(sympy.Eq(symbol, sym))
else:
fx_node = None
if isinstance(sym, sympy.Integer):
if hint is not None:
assert int(sym) == hint
out = int(sym)
else:
out = SymInt(SymNode(sym, self, int, hint, fx_node=fx_node))
return out
@record_shapeenv_event()
def create_unspecified_symint_and_symbol(self, value, source, dynamic_dim):
"""Create a SymInt wrapping a new unspecified symbol"""
return self.create_symintnode(
self.create_unspecified_symbol(
value,
source=source,
dynamic_dim=dynamic_dim,
),
hint=value,
source=source,
)
def create_symboolnode(self, sym: "sympy.Expr"):
"""Create a SymBool object from a sympy boolean expression"""
# This function is only being used in serialization, so we do not track it
# for validation.
return SymBool(SymNode(sym, self, bool, None))
def _log_create_unbacked_symbol(self, prefix: str, symbol, vr: ValueRanges):
is_debug = config.extended_debug_create_symbol is not None and str(symbol) in config.extended_debug_create_symbol.split(',')
fsummary, maybe_user_loc, maybe_extra_debug = self._get_stack_summary(is_debug)
log.info(
"%s %s [%s, %s]%s (%s)%s",
prefix, symbol, vr.lower, vr.upper, maybe_user_loc, format_frame(fsummary), maybe_extra_debug, stack_info=is_debug
)
@record_shapeenv_event()
def create_unbacked_symfloat(self):
"""Create a symbolic float without a hint value
"""
symbol: sympy.Symbol = sympy.Symbol(f"f{next(self.unbacked_symfloat_counter)}")
self.counter["create_unbacked_symbol"] += 1
self.var_to_stack[symbol] = CapturedTraceback.extract(skip=1)
vr = self.var_to_range[symbol] = ValueRanges.unknown()
# Create a new FX placeholder and Z3 variable for 'symbol'.
fx_node = self._create_fx_placeholder_and_z3var(symbol, float)
self._log_create_unbacked_symbol("create_unbacked_symfloat", symbol, vr)
return SymFloat(SymNode(symbol, self, float, None, fx_node=fx_node))
@record_shapeenv_event()
def create_unbacked_symint(self):
"""Create a symbolic integer without a hint value
"""
symbol: sympy.Symbol = sympy.Symbol(f"u{next(self.unbacked_symint_counter)}", integer=True)
self.counter["create_unbacked_symbol"] += 1
self.var_to_stack[symbol] = CapturedTraceback.extract(skip=1)
vr = self.var_to_range[symbol] = self._default_unspecified_value_range()
# Create a new FX placeholder and Z3 variable for 'symbol'.
fx_node = self._create_fx_placeholder_and_z3var(symbol, int)
self._log_create_unbacked_symbol("create_unbacked_symint", symbol, vr)
return SymInt(SymNode(symbol, self, int, None, fx_node=fx_node))
def is_unbacked_symint(self, symbol: sympy.Symbol) -> bool:
"""Check if a sympy symbol matches the naming convention for unbacked symbols
"""
# NB: keep synced with free_unbacked_symbols
return str(symbol).startswith("u")
@record_shapeenv_event()
def create_unbacked_symbool(self):
"""Create a symbolic boolean without a hint value
"""
symbol: sympy.Symbol = sympy.Symbol(f"u{next(self.unbacked_symint_counter)}", integer=True)
self.counter["create_unbacked_symbol"] += 1
self.var_to_stack[symbol] = CapturedTraceback.extract(skip=1)
vr = self.var_to_range[symbol] = ValueRanges(0, 1)
# Create a new FX placeholder and Z3 variable for 'symbol'.
fx_node = self._create_fx_placeholder_and_z3var(symbol, bool)
self._log_create_unbacked_symbol("create_unbacked_symbool", symbol, vr)
return SymBool(SymNode(sympy.Eq(symbol, 1), self, bool, None, fx_node=fx_node))
@record_shapeenv_event()
def create_unspecified_symbol(
self,
val: Union[int, SymInt],
source: Source,
dynamic_dim: DimDynamic = DimDynamic.DUCK,
constraint_dim: DimConstraint = None, # NB: includes None
) -> "sympy.Expr":
"""Create a symbol with an unspecified value
Compared to standard symbols we do not assume the value is positive,
nor do we specialze on zero or one values.
"""
# 'positive' is None for unspecified symbols, since we can't
# assume that it will be neither positive nor negative.
# We don't want to specialize zero one val for unspecified symbol
# so that we can always get a new symbol despite val.
return self.create_symbol(
val,
source,
dynamic_dim,
constraint_dim,
positive=None,
do_not_specialize_zero_one=True,
symbolic_context=None)
@record_shapeenv_event()
def create_symbol(
self,
val: int,
source: Source,
dynamic_dim: DimDynamic = DimDynamic.DUCK,
constraint_dim: DimConstraint = None, # NB: includes None
positive: Optional[bool] = True,
do_not_specialize_zero_one: bool = False,
symbolic_context=None,
) -> "sympy.Expr":
"""Create a new symbol which is tracked by this ShapeEnv
"""
# see note [Tensor Fakification and Symbol Caching]
source_name = source.name()
if (isinstance(symbolic_context, StatefulSymbolicContext)
and id(self) not in symbolic_context.shape_env_to_source_to_symbol_cache):
symbolic_context.shape_env_to_source_to_symbol_cache[id(self)] = {}
if (isinstance(symbolic_context, StatefulSymbolicContext)
and source_name
and (source_name in symbolic_context.shape_env_to_source_to_symbol_cache[id(self)])):
return symbolic_context.shape_env_to_source_to_symbol_cache[id(self)][source_name]
if do_not_specialize_zero_one:
specialize_zero_one = False
else:
specialize_zero_one = self.specialize_zero_one
assert isinstance(source, Source), f"{type(source)} {source}"
assert not (positive and val < 0), f"positive set for negative value: {val}"
# It's always sound to allocate a symbol as DYNAMIC. If the user
# constrained the symbol, force the symbolic_context to DYNAMIC, because our
# constraint code will do weird stuff if, e.g., it's duck shaped
if constraint_dim is not None:
dynamic_dim = DimDynamic.DYNAMIC
if dynamic_dim is DimDynamic.STATIC:
out = sympy.Integer(val)
if isinstance(symbolic_context, StatefulSymbolicContext) and source_name:
symbolic_context.shape_env_to_source_to_symbol_cache[id(self)][source_name] = out
return out
elif dynamic_dim is DimDynamic.DUCK:
# duck_shape can be used to globally turn off duck shaping, even
# if it was requested
duck = self.duck_shape
elif dynamic_dim is DimDynamic.DYNAMIC:
duck = False
else:
raise AssertionError(f"unhandled dynamic_dim {dynamic_dim}")
if val in (0, 1) and specialize_zero_one:
r = self.val_to_var[val]
elif not duck or val not in self.val_to_var:
# If we're not duck shaping, we always create a new symbol
# Even if we're duck shaping, if we haven't seen this particular
# value before, we also create a new symbol
sympy_expr = sympy.Symbol(f"s{len(self.var_to_val)}", positive=positive, integer=True)
# We always associate vars to vals
if isinstance(val, int):
self.var_to_val[sympy_expr] = sympy.Integer(val)
else:
# Only used for jagged layout nested tensors
self.var_to_val[sympy_expr] = SingletonInt(val.node.nested_int(), coeff=val.node.nested_int_coeff())
# Do the appending later, because we always want to populate this
self.var_to_sources[sympy_expr] = []
# Create a Z3 variable for the new symbol.
self._add_z3var(sympy_expr, int)
if duck:
# Make sure to reuse this symbol for subsequent duck shaping
self.val_to_var[val] = sympy_expr
if isinstance(val, int):
if positive:
# Add assertions for the newly created symbols
self._add_assertion(sympy_expr > 1)
# Apply default range, which assumes not zero-one
self.var_to_range[sympy_expr] = self._default_value_range()
else:
self.var_to_range[sympy_expr] = self._default_unspecified_value_range()
# Small performance optimization: if we have a min-max constraint,
# we can proactively narrow to that range
if isinstance(constraint_dim, StrictMinMaxConstraint):
assert not duck
self.var_to_range[sympy_expr] &= constraint_dim.vr
vr = self.var_to_range[sympy_expr]
if val not in vr:
raise ConstraintViolationError(f"{val} not in range [{vr.lower}, {vr.upper}]")
range_str = f"[{vr.lower}, {vr.upper}]"
else:
# Skip var_range logic for SingletonInt
# Only used for jagged layout nested tensors
range_str = ""
r = sympy_expr
is_debug = (
config.extended_debug_create_symbol is not None and
str(sympy_expr) in config.extended_debug_create_symbol.split(',')
)
fsummary, maybe_user_loc, maybe_extra_debug = self._get_stack_summary(is_debug)
self.log.info(
"create_symbol %s = %s for %s %s%s (%s)%s",
sympy_expr, val, source.name(), range_str,
maybe_user_loc, format_frame(fsummary), maybe_extra_debug, stack_info=is_debug
)
self.counter["create_symbol"] += 1
else:
# This implements duck-shaping: input sizes that match are assigned
# the same symint
r = self.val_to_var[val]
self.log.debug("create_symbol %s duck sized %s", r, source.name())
if isinstance(r, sympy.Symbol):
r_sources = self.var_to_sources[r]
r_sources.append(source)
if not source.is_ephemeral() and r_sources[0].is_ephemeral():
# prefer non-ephemeral source first since it may be guarded on later
r_sources[0], r_sources[-1] = r_sources[-1], r_sources[0]
# This ensures we get zeros in symbol_guard_counts, which makes
# some queries simpler (since we will accumulate mass on 0 this
# way)
self.symbol_guard_counter[r] = 0
if isinstance(symbolic_context, StatefulSymbolicContext) and source_name:
symbolic_context.shape_env_to_source_to_symbol_cache[id(self)][source_name] = r
return r
def _debug_name(self, source):
src_name = source.name()
return self.source_name_to_debug_name.get(src_name, src_name)
def _render_range_for_constraint_violation(self, source, c):
if isinstance(c, StrictMinMaxConstraint):
lower, upper = c.vr.lower, c.vr.upper
default = self._default_value_range()
if lower <= default.lower:
lower = None
if upper >= default.upper:
upper = None
c_render = f"{self._debug_name(source)} = {source.name()} in the specified range"
if lower is not None and upper is not None:
c_render += f" {lower} <= {self._debug_name(source)} <= {upper}"
elif lower is None and upper is not None:
c_render += f" {self._debug_name(source)} <= {upper}"
elif lower is not None and upper is None:
c_render += f" {lower} <= {self._debug_name(source)}"
return c_render
return c.render(source)
def produce_guards(
self,
placeholders,
sources,
source_ref=lambda n: n.name(),
*,
input_contexts: Optional[DimList[SymbolicContext]] = None,
# Encodes user-specified input shape equations of the form s = s' and s = fn(s').
# (See docs on EqualityConstraint for details of the encoding.)
equalities_inputs: Optional[EqualityConstraint] = None,
_simplified=False,
# Indicates if we should produce guards for known static values.
ignore_static=True,
) -> List[str]:
"""
Generates a list of guards strings which, when evaluated in a context that
defines tensors for all the sources, returns True or False depending
on if the guards in the list evaluated to True or not. Primarily used by Dynamo,
but this is also helpful for manual testing of guards (see
evaluate_guards_for_args)
For convenience in testing, a source is allowed to be a str,
in which case we will assume it is a LocalSource
simplified lets you omit duck sizing, equality and 0/1 guards.
This is useful for testing when you don't care about the boilerplate
guards, and it may be helpful for user output too (be careful though;
some equality guards are nontrivial! It would be nice to get simplified
output to print them too). It's private because it's not
intended for normal use
"""
self.log.info("produce_guards")
# Check if we get to the same ShapeEnv state by replaying the recorded events.
# This will create a new ShapeEnv instance, and call all recorded function
# calls on this new instance. Finally, it will check whether this new instance
# has equal state.
#
# It's important that we do it in the begining of this function, since it modifies
# self.dim_constraints through its execution. Changes that happen in this method
# aren't interesting, since this is the function call we wish to reproduce at the
# end. If we wish to simply reproduce ShapeEnv instances even after this call,
# this method should also be recorded.
if self.check_recorded_events:
shape_env = replay_shape_env_events(self.events)
self.check_equal(shape_env)
assert len(placeholders) == len(sources), f"len({placeholders}) != len({sources})"
Tensorlike = (torch.Tensor, FakeTensorMeta)
def _create_no_constraints_context(t):
return StatelessSymbolicContext(
# Ignored; only the constraints part is relevant below.
dynamic_sizes=[DimDynamic.DYNAMIC] * t.dim(),
constraint_sizes=[None] * t.dim()
)
# Expand optional inputs, or verify invariants are upheld
if input_contexts is None:
input_contexts = [
_create_no_constraints_context(t) if isinstance(t, Tensorlike)
else None for t in placeholders
]
else:
assert len(input_contexts) == len(placeholders)
for i, (t, context) in enumerate(zip(placeholders, input_contexts)):
if isinstance(t, Tensorlike):
if context is None:
input_contexts[i] = _create_no_constraints_context(t)
else:
assert isinstance(t, (SymInt, int))
assert not isinstance(context, list)
# It took a lot of sweat to figure out the algorithm here. Let's
# explain how it works.
#
# The ShapeEnv lifecycle looks something like this:
#
# - For each input, you either generate a fresh Sympy symbol (s0) to
# represent its value (a binding site), or you reuse some
# preexisting symbol or expression, skipping the symbol allocation
# (e.g., duck sizing to a preexisting symbol, or expressing a
# stride as a multiplication of a separate stride and size.)
# Naively, you might expect to bind a fresh Sympy symbol for
# every input, but this is fairly wasteful as most of these
# symbols immediately simplify away, and if you don't eagerly
# specialize, e.g., 0/1 symbols, you end up with very complicated
# expressions that are not optimizable in practice.
#
# - You perform some compute on these symbols, occasionally
# introducing guards on boolean expressions on these symbols.
# In particular, whenever we guard on equality (_maybe_guard_rel),
# we can simplify shapes; e.g., when s0 == s1 * 2, we can now
# replace all occurrences of s0 with s1 * 2. Sometimes, a
# boolean expression evaluation doesn't introduce a guard, as
# the guard is already entailed by the simplifications we have
# applied.
#
# - In the end, you have a bunch of replacements (saying how to
# simplify shapes) and a bunch of guards (all the equality guards
# are trivial, because they're covered by the replacements).
#
# From the ShapeEnv, we must generate a Python expression that, when
# evaluated on a set of inputs, tells us whether or not these boolean
# expressions would have evaluated in the same way. However,
# we cannot easily compute this, as we elide recording boolean
# expressions when we think they are vacuously true. Thus, we seek
# an approximation: we must generate an expression, if true, would have
# produced an "equivalent" ShapeEnv, which would answer guard
# expressions in the same way.
#
# Our notion of equivalence is a bit subtle. For example, consider
# the ShapeEnv created from an input of size (5, 4) versus (4, 4)
# (no other guards.) Duck sizing would generate (s0, s1) in the first
# case but (s0, s0) in the second. We do NOT assume that size
# variables are disjoint; so in fact a graph that assumes the input
# could be (s0, s1) subsumes (s0, s0) (setting s0 == s1), but not
# vice versa. However, consider an analogous case (1,) versus (2,).
# Duck sizing generates (1,) and (s0,); the (s0,) graph does NOT
# subsume the (1,) graph because we assume that any size variables
# is NOT 0/1 (and make simplifications according to this; e.g., if
# we queried s0 == 0, we would immediately return False without
# returning a guard.)
#
# So, it is perhaps easier to flip things on their head: the guard
# expressions we generate here say what simplifications are valid,
# and what are not. Below, we explain each of the guard expressions
# we generate
# TODO: Make this more efficient by binding all the size/stride/offsets
# to locals before performing tests on them.
from torch._dynamo.source import TensorPropertySource, TensorProperty, NegateSource
# Actual codegen must be delayed as we don't necessarily know what
# the symbol mapping is
input_guards = []
symbol_to_source = collections.defaultdict(list)
symbol_to_constraints = collections.defaultdict(set)
constraint_violations : List[Tuple[bool, Callable[[], str]]] = []
def record_constraint_violation(warn_only, debug_name, msg, hint=None):
constraint_violations.append(
(warn_only, debug_name, lambda: f"{msg}{hint()}" if hint else msg)
)
def is_dim(src):
return isinstance(src, TensorPropertySource) and src.prop is TensorProperty.SIZE
if equalities_inputs:
source_index = {}
for i, src in enumerate(sources):
source_index[src.name()] = i
def get_expression(tensor_dim_src):
fake = placeholders[source_index[tensor_dim_src.base.name()]]
symint = fake.shape[tensor_dim_src.idx]
if isinstance(symint, torch.SymInt):
return symint.node.expr
else:
assert type(symint) is int, f"Expected int, got {type(symint)}"
return symint
for src1, src2 in equalities_inputs.source_pairs:
expr1, expr2 = get_expression(src1), get_expression(src2)
# Check whether given input shape values satisfy a specified equation s = s'.
# - Raise when the equation was violated by the given input shape values.
# - Otherwise issue a guard to constrain them.
concrete_val = self.evaluate_expr(sympy.Eq(expr1, expr2))
if not concrete_val:
raise ConstraintViolationError(
f"{src1.name()} = {expr1.subs(self.var_to_val)}"
" is not equal to "
f"{src2.name()} = {expr2.subs(self.var_to_val)}"
)
for src, root, fn in equalities_inputs.derived_equalities:
expr1 = get_expression(src)
# recall that root is either a phantom symbol or an input source
expr2, debug_name = (
(root, self.var_to_sources[root][0].name()) if isinstance(root, sympy.Symbol)
else (get_expression(root), self._debug_name(root))
)
expr2_ = fn(expr2)
# Check whether given input shape values satisfy a specified equation s = fn(s').
# - Raise when the equation was violated by the given input shape values.
# - Otherwise issue a guard to constrain them.
concrete_val = self.evaluate_expr(sympy.Eq(expr1, expr2_))
if not concrete_val:
raise ConstraintViolationError(
f"Expected input {src.name()} to be equal to "
f"{fn(sympy.Symbol(debug_name))}, "
f"where {debug_name} = {expr2.subs(self.var_to_val)}, "
f"but got {expr1.subs(self.var_to_val)}"
)
for phantom_symbol in equalities_inputs.phantom_symbols:
# we created additional phantom symbols that are not input shape dimensions
symbol_to_source[phantom_symbol].extend(self.var_to_sources[phantom_symbol])
# How do we know what the value of s0 is? Fresh variables can only be
# bound by inputs, so there MUST be some other input which binds the
# variable. If there is no such input, this is an error in our
# system. We record where all symbols come from, to help you diagnose
# why those symbols didn't occur.
#
# In fact, generally speaking it is only possible for the "outermost"
# user of a ShapeEnv to evaluate the guards, because some inputs may
# not be available to inner levels. For example, Dynamo can guard on
# tensors that never actually become graph arguments (they are
# pruned). In this case, only Dynamo knows about these arguments.
def track_symint(source, val, constraint=None):
log.debug("track_symint %s %s %s", LazyString(source.name), val, constraint)
assert not isinstance(val, SymInt) or is_symbolic(val)
if isinstance(val, SymInt) and val.node.maybe_as_int() is not None:
val = val.node.maybe_as_int()
if isinstance(val, SymInt):
s = val.node.expr
if isinstance(s, sympy.Symbol):
symbol_to_source[s].append(source)
if constraint is not None:
symbol_to_constraints[s].add(constraint)
elif isinstance(-s, sympy.Symbol):
symbol_to_source[-s].append(NegateSource(source))
else:
constraint_violated = False
if isinstance(constraint, StrictMinMaxConstraint):
# try inferring the ranges of the expr s
sym_vrs = {x: self.var_to_range.get(x, None) for x in s.free_symbols}
if all(vr is not None for vr in sym_vrs.values()):
expr_vr = bound_sympy(s, sym_vrs)
if expr_vr != constraint.vr:
# the expr and constrain ranges don't match
constraint_violated = True
else:
# some of the free symbols in s don't have ranges
constraint_violated = True
elif isinstance(constraint, RelaxedUnspecConstraint):
if s.is_number:
i = int(s)
# Don't complain about 0/1 specialization, we
# expect to have to compile in this case anyway
if i not in (0, 1):
constraint_violated = True
if constraint_violated:
def hint(s):
sexpr = ShapeGuardPrinter(symbol_to_source, source_ref, self.var_to_sources).doprint(s)
return f"{sexpr}."
var_with_range = self._render_range_for_constraint_violation(source, constraint)
msg = (
f"Not all values of {var_with_range} are valid because "
f"{self._debug_name(source)} was inferred to be equal to "
)
record_constraint_violation(
constraint.warn_only,
self._debug_name(source),
msg,
hint=functools.partial(hint, s),
)
input_guards.append((source, s))
else:
s = sympy.Integer(val)
input_guards.append((source, s))
constraint_violated = False
if isinstance(constraint, StrictMinMaxConstraint):
constraint_violated = True
elif isinstance(constraint, RelaxedUnspecConstraint):
# Don't complain about 0/1 specialization, we
# expect to have to compile in this case anyway
if val not in (0, 1):
constraint_violated = True
if constraint_violated:
var_with_range = self._render_range_for_constraint_violation(source, constraint)
msg = (
f"Not all values of {var_with_range} are valid because "
f"{self._debug_name(source)} was inferred to be a constant ({val})."
)
record_constraint_violation(constraint.warn_only, self._debug_name(source), msg)
for t, source, context in zip(placeholders, sources, input_contexts):
if isinstance(source, str):
from torch._dynamo.source import LocalSource
source = LocalSource(source)
assert isinstance(source, Source)
if t is None:
continue
if isinstance(t, (SymInt, int)):
track_symint(source, t)
continue
assert isinstance(t, Tensorlike)
if is_traceable_wrapper_subclass(t):
from torch._dynamo.source import AttrSource
assert isinstance(context, SubclassSymbolicContext)
# For subclasses, we need to track symints on BOTH the outer
# and inner tensors.
sources_tensors_constraints = [
(source, t, context.constraint_sizes)
]
attrs, _ = t.__tensor_flatten__()
for attr in attrs:
inner_t = getattr(t, attr)
inner_context = context.inner_contexts[attr]
sources_tensors_constraints.append((
AttrSource(source, attr),
inner_t,
inner_context.constraint_sizes
))
else:
sources_tensors_constraints = [(source, t, context.constraint_sizes)]
for src, curr_t, constraint in sources_tensors_constraints:
if is_sparse_any(curr_t):
for i, ss in enumerate(curr_t.size()):
property_source = TensorPropertySource(src, TensorProperty.SIZE, i)
track_symint(property_source, ss, constraint[i])
else:
for i, ss in enumerate(curr_t.size()):
property_source = TensorPropertySource(src, TensorProperty.SIZE, i)
track_symint(property_source, ss, constraint[i])
for i, ss in enumerate(curr_t.stride()):
track_symint(TensorPropertySource(src, TensorProperty.STRIDE, i), ss)
track_symint(TensorPropertySource(src, TensorProperty.STORAGE_OFFSET), curr_t.storage_offset())
# 1. Every input must equal the final simplified symbolic expression
# stored on the placeholder. Given a placeholder (s0*2, s1),
# if we have an input (2, 3), we must show s0*2 == 2 and s1 == 3.
# This does a lot of work: it covers duck sizing and equality guards.
exprs = []
self.dim_constraints = DimConstraints(
symbol_to_source,
self.var_to_val,
set(symbol_to_constraints.keys()),
self.source_name_to_debug_name,
)
if not _simplified:
for source, expr in input_guards:
if self._translation_validation_enabled:
# Ignore sources that were not turned into SymInts.
srcname = source.name()
if srcname in self.source_to_symbol:
self._add_target_expr(sympy.Eq(self.source_to_symbol[srcname], expr))
# Small optimization
if (
isinstance(expr, sympy.Symbol) and
symbol_to_source.get(expr) and
source == symbol_to_source[expr][0]
):
continue
# This logic excludes static values found on tensors from guarding, because
# dynamo's check_tensor_fn does that (see guards.cpp).
# However, for non tensor sources, we still need to guard here.
if ignore_static and isinstance(source, TensorPropertySource):
if expr.is_number:
self.log.debug("Skipping guard %s", f"{source_ref(source)} == {expr}")
continue
if is_dim(source):
self.dim_constraints.add_equality(source, expr)
sexpr = ShapeGuardPrinter(symbol_to_source, source_ref, self.var_to_sources).doprint(expr)
exprs.append(f"{source_ref(source)} == {sexpr}")
if (
isinstance(source, TensorPropertySource)
and source.prop is TensorProperty.SIZE
and equalities_inputs
and len(expr.free_symbols) == 1
):
symbol = next(iter(expr.free_symbols))
if (
isinstance(expr, sympy.Symbol) and
expr in symbol_to_constraints and
not equalities_inputs.is_equal(source, symbol_to_source[expr][0])
):
msg = (
f"The values of {self._debug_name(source)} = {source.name()} and "
f"{self._debug_name(symbol_to_source[expr][0])} = {symbol_to_source[expr][0].name()} "
"must always be equal."
)
record_constraint_violation(equalities_inputs.warn_only, self._debug_name(source), msg)
if (
not isinstance(expr, sympy.Symbol) and
symbol in symbol_to_constraints and
not equalities_inputs.is_derived(source, symbol_to_source[symbol][0], lambda x: expr.subs(symbol, x))
):
src = symbol_to_source[symbol][0]
msg = (
f"The values of {self._debug_name(source)} = {source.name()} must always be related to "
f"the values of {self._debug_name(src)} = {src.name()} by "
f"{self._debug_name(source)} = {expr.subs(symbol, sympy.sympify(self._debug_name(src)))}."
)
record_constraint_violation(equalities_inputs.warn_only, self._debug_name(source), msg)
# NB: Not necessary to report constraint violations here:
# constraints are guaranteed to be on symbols (we've already
# caught constants and non-atomic expressions), so we only
# have relational constraints, but we don't support those
# at the moment
# 2. Every guard must evaluate to True (but remember many guards
# like s0 == s1*2 because trivial due to simplification)
issued = set()
def issue_guard(guard: ShapeGuard) -> None:
expr = self.simplify(guard.expr)
# Avoid re-issueing the same guard.
if expr in issued:
return
issued.add(expr)
try:
is_trivial = False
if any(is_dim(source) for s in expr.free_symbols for source in symbol_to_source[s]):
is_trivial = self.dim_constraints.add(expr)
guard_expr = ShapeGuardPrinter(symbol_to_source, source_ref, self.var_to_sources).doprint(expr)
exprs.append(guard_expr)
self._add_target_expr(expr)
# A non-relational constraint on a single sizevar can violate
# a constraint
if not is_trivial and len(expr.free_symbols) == 1:
symbol = next(iter(expr.free_symbols))
source = symbol_to_source[symbol][0]
constraints = symbol_to_constraints[symbol]
for c in constraints:
if isinstance(c, StrictMinMaxConstraint):
var_with_range = self._render_range_for_constraint_violation(source, c)
msg = (
f"Not all values of {var_with_range} "
f"satisfy the generated guard {guard_expr}."
)
record_constraint_violation(c.warn_only, self._debug_name(source), msg)
elif isinstance(c, RelaxedUnspecConstraint):
# This is fine, we allow guards here as long as it
# didn't constrain it to one value (we don't
# actually know this; this depends on our
# ValueRanges reasoning capability)
pass
else:
raise AssertionError(f"unrecognized constraint {c}")
except Exception:
self.log.warning("Failing guard allocated at: \n%s", ''.join(guard.stack.format()))
raise
# First, issue all the non-trivial guards.
for guard in self.guards:
if self._maybe_evaluate_static(guard.expr) is not None:
continue
issue_guard(guard)
# 3. Every symbol must be within its value range (this handles 0/1
# specialization too).
for symbol, sources in symbol_to_source.items():
r = self.var_to_range.get(symbol)
if r is None:
if symbol not in self.var_to_range:
continue
r = self.var_to_range[symbol]
assert sources
assert symbol.is_integer
bounds = []
if r.lower != -sympy.oo:
if any(is_dim(source) for source in sources):
self.dim_constraints.add(sympy.Ge(symbol, r.lower))
# Only print lower bound in simplified mode if it is not the
# default
if not _simplified or r.lower != self._default_value_range().lower:
bounds.append(str(r.lower))
bounds.append(source_ref(sources[0]))
# NB: This looks like an off-by-one error but it's not: the
# upper bound may be sys.maxsize - 1 because we intentionally
# exclude sys.maxsize from our bounds to deal with direct
# == INT_MAX guards, but it's still dumb to actually test it.
# Note that you can be off by a pretty large constant and it
# won't matter because sizes in practice will be no where near
# the 64-bit limit.
if r.upper != sympy.oo and r.upper < sys.maxsize - 1:
if any(is_dim(source) for source in sources):
self.dim_constraints.add(sympy.Le(symbol, r.upper))
# nontrivial upper bound is always interesting
bounds.append(str(r.upper))
if len(bounds) > 1:
exprs.append(" <= ".join(bounds))
# Check constraints
constraints = symbol_to_constraints[symbol]
for c in constraints:
if isinstance(c, StrictMinMaxConstraint):
# NB: By default, we have a restrictive range
# 2 <= s0 <= sys.maxsize - 1. But export users generally
# expect to be able to specify nice ranges like [0, oo]
if not (c.vr & self._default_value_range()).issubset(r):
source = sources[0]
expr = sympy.And(sympy.Le(r.lower, symbol), sympy.Le(symbol, r.upper))
guard_expr = ShapeGuardPrinter(symbol_to_source, source_ref, self.var_to_sources).doprint(expr)
var_with_range = self._render_range_for_constraint_violation(source, c)
msg = (
f"Not all values of {var_with_range} satisfy the generated guard {guard_expr}"
)
record_constraint_violation(
c.warn_only,
self._debug_name(source),
msg,
)
if constraint_violations:
warn_msgs = []
error_msgs = []
debug_names = set()
for warn_only, debug_name, msg in constraint_violations:
if warn_only:
msg = f" {len(warn_msgs) + 1}. {msg()}"
warn_msgs.append(msg)
else:
msg = f" - {msg()}"
error_msgs.append(msg)
debug_names.add(debug_name)
if len(error_msgs) > 0:
debug_names = ', '.join(debug_names)
err = '\n'.join(error_msgs)
raise ConstraintViolationError(
f"Constraints violated ({debug_names})! "
"For more information, run with TORCH_LOGS=\"+dynamic\".\n"
f"{err}"
)
elif len(warn_msgs) > 0:
log.debug("%s Warning only constraints violated", len(warn_msgs))
signpost_event(
"dynamic",
"produce_guards",
{
**self.co_fields,
**self.counter,
"num_guards": len(exprs),
"free_symbols": sum(1 for v in symbol_to_source.values() if v),
# The keys are meaningless from an aggregate perspective, so
# don't include them. Biggest first.
"symbol_guard_counts": sorted(self.symbol_guard_counter.values(), reverse=True),
},
)
if self._translation_validation_enabled:
from torch.fx.experimental.validator import PopulateValidator
# Add all deferred runtime assertions; these are not technically
# handled by produce_guards but we need to put them in the target
# set
for ras in self.deferred_runtime_asserts.values():
for ra in ras:
self._add_target_expr(ra.expr)
# Add value range bound guards for all symbols with no trivial bounds.
# Reason: '_maybe_evaluate_static' may eliminate guards based on the
# refined value ranges.
for sym, vr in self.var_to_range.items():
if vr.lower != -sympy.oo:
self._add_target_expr(sympy.Le(vr.lower, sym))
if vr.upper != sympy.oo:
self._add_target_expr(sympy.Le(sym, vr.upper))
# Before validating, populate the input of the validator with the
# built FX graph.
with fx_traceback.preserve_node_meta():
PopulateValidator(self.graph, self.validator).run()
self._check_translation_validate()
return exprs
def produce_guards_expression(self, placeholders, ignore_static=True):
"""
Expected to be used with evaluate_guards_expression(). Produces the guards
for the given placeholders and returns a string expression to be evaluated
by evaluate_guards_expression given concrete values for the placeholders.
"""
from torch._dynamo.source import LocalSource
arg_names = [f"t{i}" for i in range(len(placeholders))]
guards = self.produce_guards(placeholders, [LocalSource(a) for a in arg_names], ignore_static=ignore_static)
if guards:
return " and ".join(guards)
return None
def evaluate_guards_expression(self, code, args):
"""
Expected to be used with produce_guards_expression(). Evaluates an expression
generated by produce_guards_expression for the given concrete args.
"""
arg_names = [f"t{i}" for i in range(len(args))]
return eval(code, SYMPY_INTERP, {"L": dict(zip(arg_names, args))})
def evaluate_guards_for_args(self, placeholders, args, *, ignore_static=True):
"""Generate guards for a graph's placeholder values and evaluate the guards with args
"""
code = self.produce_guards_expression(placeholders, ignore_static=ignore_static)
if code:
return self.evaluate_guards_expression(code, args)
return True
def bind_symbols(self, placeholders, args):
"""
Given a paired list of placeholders (fake tensors with
symbolic sizes) and concrete arguments (regular tensors
with real sizes), returns a dictionary mapping each
symbol to its real value. So for example, if you
have a placeholder with size (s0, s1), binding
(2, 4) to it will give you {s0: 2, s1: 4}. This is
not guaranteed to bind ALL symbols in the ShapeEnv;
we can't bind a symbol if it doesn't occur in any placeholder,
and symbols that already have replacements won't get bindings.
This is a little duplicative with evaluate_guards but
it's different enough that it seemed cleanest to make
another copy. This assumes the guards are already checked,
though if it's cheap we'll check for shenanigans
"""
bindings: Dict[sympy.Symbol, int] = {}
def bind_symint(arg, val):
if isinstance(val, SymInt):
s = val.node.expr
if isinstance(s, sympy.Symbol):
if s in bindings:
assert bindings[s] == arg, f"{bindings[s]} != {arg}"
else:
bindings[s] = arg
elif isinstance(-s, sympy.Symbol):
if -s in bindings:
assert bindings[-s] == -arg, f"{bindings[-s]} != {-arg}"
else:
bindings[-s] = -arg
for t, arg in zip(placeholders, args):
if t is None:
continue
if isinstance(t, SymInt):
bind_symint(arg, t)
continue
assert isinstance(t, torch.Tensor)
for i, s in enumerate(t.size()):
bind_symint(arg.size(i), s)
for i, s in enumerate(t.stride()):
bind_symint(arg.stride(i), s)
bind_symint(arg.storage_offset(), t.storage_offset())
return bindings
def get_nontrivial_guards(self):
"""Returns a list of guard expressions that aren't statically known (i.e. not trivial)"""
return [self.simplify(guard.expr) for guard in self.guards if self._maybe_evaluate_static(guard.expr) is None]
def format_guards(self, verbose=False):
"""Format this shape env's guard expressions with optional traceback info if verbose"""
def format_tb(tb):
if not verbose:
return ""
return f"\n Guarded at:\n{''.join(' ' + l for l in tb.format())}"
return '\n'.join(f" - {guard.expr}{format_tb(guard.stack)}" for guard in self.guards)
def bound_sympy(self, expr: sympy.Expr, size_oblivious: bool = False) -> ValueRanges:
"""Given a sympy expression, computes a ValueRanges bound for what values it can be"""
var_to_range = {x: self.var_to_range.get(x, None) for x in expr.free_symbols}
if size_oblivious:
# Clamp values of size-like variables
for x in self.size_like & var_to_range.keys():
if var_to_range[x] is not None:
var_to_range[x] &= ValueRanges(2, sympy.oo)
return bound_sympy(expr, var_to_range)
@_lru_cache
def _maybe_evaluate_static(
self, expr: "sympy.Expr", *, unbacked_only: bool = False, compute_hint: bool = False,
expect_rational=True, size_oblivious: bool = False
) -> "Optional[sympy.Expr]":
"""
Tries to evaluate expr without introducing guards
If unbacked_only == True, then we only do substitutions on
unbacked SymInts (leaving regular hinted integers alone). This could
result in an expression that still contains backed SymInts, which you
could then potentially guard on.
Use compute_hint == True if you are trying to compute a non-binding
hint for the particular hint values of backed SymInts, e.g., if
s0 happens to be 3 this run, compute_hint will subsitute s0 with 3.
"""
expr = self.simplify(expr)
if compute_hint:
expr = expr.xreplace(self.var_to_val)
expr = canonicalize_bool_expr(expr)
symbols = list(expr.free_symbols)
# Apply known runtime asserts
for s in symbols:
# Unbacked symints only
if s in self.var_to_val:
continue
subst = {}
def add_expr(expr):
# Expr and negation
subst[canonicalize_bool_expr(expr)] = sympy.true
subst[canonicalize_bool_expr(sympy.Not(expr))] = sympy.false
if isinstance(expr, sympy.Rel):
# multiplying by -1 changes the direction of the inequality
dual = type(expr)(-expr.rhs, -expr.lhs)
subst[canonicalize_bool_expr(dual)] = sympy.true
subst[canonicalize_bool_expr(sympy.Not(dual))] = sympy.false
for e in itertools.chain(self.guards, self.deferred_runtime_asserts.get(s, ())):
e = e.expr
if compute_hint:
e = canonicalize_bool_expr(e.xreplace(self.var_to_val))
add_expr(e)
# Other relational expressions this expression implies
if isinstance(e, sympy.Eq):
add_expr(sympy.Le(e.lhs, e.rhs))
add_expr(sympy.Ge(e.lhs, e.rhs))
elif isinstance(e, sympy.Lt):
add_expr(sympy.Le(e.lhs, e.rhs))
add_expr(sympy.Ne(e.lhs, e.rhs))
# NB: this helps us deal with And/Or connectives
expr = expr.subs(subst)
# Simplify making use of value range lower bound
new_shape_env = {}
new_range_env = {}
for idx, k in enumerate(symbols):
if isinstance(self.var_to_val.get(k, None), SingletonInt):
# Skip var_to_range logic for SingletonInt which is only used
# for jagged layout NestedTensors today
continue
vr = self.var_to_range[k]
if size_oblivious and k in self.size_like:
lower = max(2, vr.lower)
else:
lower = vr.lower
# Don't do anything if we don't have a nontrivial lower bound
# Also don't do anything if we asked only to simplify unbacked
# SymInt
if (
lower < (-sys.maxsize - 1) // 2 or
(unbacked_only and k in self.var_to_val)
):
new_range_env[k] = vr
continue
# Positive means >= 1
# Positive - 1 means >= 0
# Positive + lower - 1 means >= lower
# The new symbol 's' is "too low", so when we substitute it in
# we have to increase it by offset (and conversely, the new
# variables have to have their value range bounds adjusted as
# well)
s = sympy.Symbol(f"shape_{idx}", positive=True, integer=True)
offset = lower - 1
new_shape_env[k] = s + offset
new_range_env[s] = SymPyValueRangeAnalysis.add(vr, -offset)
def replace(expr, repl):
return expr.xreplace(repl)
try:
new_expr = replace(expr, new_shape_env)
except RecursionError:
log.warning("RecursionError in sympy.xreplace(%s, %s)", expr, new_shape_env)
self.counter["sympy_recursion_error"] += 1
return None
floor_div_replace = {}
for atom in new_expr.atoms(FloorDiv):
floor_div_replace[atom] = sympy.floor(atom.args[0] / atom.args[1])
new_expr = safe_expand(new_expr.xreplace(floor_div_replace))
# TODO: when unbacked_only, can sometimes early return even when there
# are still free symbols
if new_expr.is_number:
return new_expr
# Check if the range can solve it statically
out = bound_sympy(new_expr, new_range_env)
if expect_rational:
_assert_bound_is_rational(new_expr, out)
if out.is_singleton():
return out.lower
return new_expr if unbacked_only else None
@_lru_cache
def replace(self, expr: "sympy.Expr") -> "sympy.Expr":
"""Apply symbol replacements to any symbols in the given expression
"""
replacements = {s: self._find(cast(sympy.Symbol, s)) for s in expr.free_symbols}
return safe_expand(expr.xreplace(replacements))
@_lru_cache
def _update_divisible(self):
new_divisible = set()
for k in self.divisible:
res = self.replace(k)
if not res.is_number:
new_divisible.add(k)
self.divisible = new_divisible
self._update_version_counter()
@_lru_cache
def simplify(self, expr: "sympy.Expr") -> "sympy.Expr":
"""Use known constraints and replacements to simplify the given expr
"""
expr = self.replace(expr)
# TODO it would seem that this pass is not necessary given the
# below replacement of // with /, but for nested FloorDivs
# the non-recursive replacement doesn't work, and
# recursive makes it hard to look up divisibility,
# because existing divisibility info has FloorDiv in it, not /
# for now just do a separate pass to catch common nested case
if expr.has(FloorDiv):
self._update_divisible()
div_replacements = {}
for atom in expr.atoms(FloorDiv):
base, divisor = atom.args
if isinstance(divisor, FloorDiv):
base1, divisor1 = divisor.args
if self.replace(Mod(base, divisor)) in self.divisible and \
base == base1 and self.replace(Mod(base1, divisor1)) in self.divisible:
div_replacements[atom] = divisor1
expr = expr.xreplace(div_replacements)
expr = safe_expand(expr)
if expr.has(FloorDiv):
div_replacements = {}
pows = expr.atoms(sympy.Pow)
rationals = expr.atoms(sympy.Rational).difference(expr.atoms(sympy.Integer))
for fd in expr.atoms(FloorDiv):
base, divisor = fd.args
if self.replace(Mod(base, divisor)) in self.divisible:
div_replacements[fd] = base / divisor
new_expr = expr.xreplace(div_replacements)
new_expr = safe_expand(new_expr)
new_pows = new_expr.atoms(sympy.Pow)
new_rationals = new_expr.atoms(sympy.Rational).difference(new_expr.atoms(sympy.Integer))
# divisions simplified away
if new_pows.issubset(pows) and new_rationals.issubset(rationals):
expr = new_expr
return expr
@lru_cache(256)
def size_hint(self, expr: "sympy.Expr", *, allow_none=False):
"""
Gets a size hint for a given expression from the underlying shapes we had.
Does not introduce a guard, so only use this when you can guarantee that
your code is still valid for arbitrary shapes (such as optimization decisions)
"""
result_expr = safe_expand(expr).xreplace(self.var_to_val)
if not result_expr.is_number:
from torch.utils._sympy.singleton_int import SingletonInt
if isinstance(result_expr, SingletonInt):
return None
r = self._maybe_evaluate_static(result_expr, compute_hint=True)
if r is not None:
return r
if allow_none:
return None
raise self._make_data_dependent_error(result_expr, expr)
return result_expr
# NB: keep in sync with size_hint
@lru_cache(256)
def has_hint(self, expr: "sympy.Expr"):
result_expr = safe_expand(expr).xreplace(self.var_to_val)
return result_expr.is_number or self._maybe_evaluate_static(result_expr) is not None
def _make_data_dependent_error(self, expr, unhinted_expr, *, size_oblivious_result: Optional[bool] = None):
# TODO: in a Dynamo context, having user code, and having the
# name of the local, will be much better
size_like_symbols = []
for s in expr.free_symbols:
stacktrace = ''.join(self.var_to_stack[s].format())
self.log.debug("Data dependent variable '%s' allocated at:\n%s", s, stacktrace)
if s in self.size_like:
size_like_symbols.append(s)
size_oblivious_result_msg = ""
if size_oblivious_result is not None:
size_oblivious_result_msg = (
f"ATTENTION: guard_size_oblivious would fix the error, evaluating expression to {size_oblivious_result}.\n"
"Maybe you need to add guard_size_oblivious to framework code, see doc below for more guidance.\n\n"
)
fsummary, maybe_user_loc, maybe_extra_debug = self._get_stack_summary(True)
return GuardOnDataDependentSymNode(
f"Could not guard on data-dependent expression {expr} (unhinted: {unhinted_expr}). "
f"(Size-like symbols: {', '.join(map(str, size_like_symbols)) or 'none'})\n\n"
f"{size_oblivious_result_msg}"
"Potential framework code culprit (scroll up for full backtrace):\n"
f"{''.join(traceback.StackSummary.from_list([fsummary]).format())}\n"
"For more information, run with TORCH_LOGS=\"dynamic\"\n"
"For extended logs when we create symbols, also add "
f"TORCHDYNAMO_EXTENDED_DEBUG_CREATE_SYMBOL=\"{','.join(map(str, expr.free_symbols))}\"\n"
"If you suspect the guard was triggered from C++, add TORCHDYNAMO_EXTENDED_DEBUG_CPP=1\n"
"For more debugging help, see "
"https://docs.google.com/document/d/1HSuTTVvYH1pTew89Rtpeu84Ht3nQEFTYhAX3Ypa_xJs/edit?usp=sharing\n" +
maybe_extra_debug
# TODO: Help text about how to use our runtime tests to fix this
# problem
)
def _set_replacement(self, a: "sympy.Symbol", tgt: "sympy.Expr", msg: str) -> None:
"""
Adds or updates a replacement for a symbol.
Use this instead of `self.replacements[a] = tgt`.
"""
# Precondition: a == tgt
assert isinstance(a, sympy.Symbol)
# Handles nested tensor symbolic variables which don't have
# var_to_range bounds
tgt_bound = None
if a in self.var_to_range:
src_bound = self.var_to_range[a]
# If you have x in [2, maxint], then 2*x in [4, 2*maxint].
# But we don't really care that the max bound says we can
# go beyond the maximum integer size, because we aren't
# using bigints anyway. Arguably, ValueRanges should know
# to do this truncation automaticaly (to avoid doing
# bigint compute in range analysis), but right now it doesn't
# so we need to get rid of some unnecessary precision.
int_range = ValueRanges(-sys.maxsize - 1, sys.maxsize - 1)
def issubset(x, y):
return (x & int_range).issubset(y & int_range)
# First, refine the value range of a based on the computed value range
# of tgt. This is always OK to do, even if we decide not to do the
# substitution in the end. This might be a no-op, if a already has
# a tighter bound
tgt_bound = self.bound_sympy(tgt)
self.var_to_range[a] = src_bound & tgt_bound
# Next, check if we can update the range of free symbols in tgt
# based on the range in a. But only do it if:
# - the source bound non-trivially improves over what we get out of
# the existing bounds.
# - the replacement is univariate and we can invert the tgt expression
if not issubset(tgt_bound, src_bound) and len(tgt.free_symbols) == 1:
b = next(iter(tgt.free_symbols))
# Try to invert the equality
r = try_solve(sympy.Eq(a, tgt), b, floordiv_inequality=False)
if r is not None:
b_bound = self.bound_sympy(r[1])
self.var_to_range[b] = b_bound & self.var_to_range[b]
tgt_bound = self.bound_sympy(tgt)
assert issubset(tgt_bound, src_bound)
# TODO: Should we propagate size-like-ness?
#
# Pros: if u0 is size-like, intuitively u0 == u1 should cause u1
# to become size-like.
#
# Cons: if u0 is size-like, what about u0 - 1 == u1? You CAN'T
# propagate in this case, because what if u0 == 0, then u1 is negative
# and clearly isn't a size. So, at minimum, any f(x) whose value
# range isn't [0, inf] given x in [0, inf] cannot propagate
# size-like-ness. But there are many situations where you could
# imagine u1 is going to be size-like and actually you just didn't
# have a refined enough value range on u0. Since even innocuous
# looking arithmetic operations can destroy size-like-ness, it's
# best to not propagate it at all and force the user to annotate it
# as necessary.
#
# Compromise: we preserve size-like-ness only for exact equality
# and nothing else.
if a in self.size_like and isinstance(tgt, sympy.Symbol):
self.size_like.add(tgt)
elif isinstance(tgt, sympy.Symbol) and tgt in self.size_like:
self.size_like.add(a)
# Now, decide if we will do the substitution.
#
# - If the source has a non-trivial range, only substitute if
# we preserve this range. Note that we may have propagated
# the src_range to free variables in tgt when tgt is univariate
# and we could find an inverse, which helps us achieve this.
# This ensures we never "forget" about user defined ranges,
# even if they end up being defined on composite formulas
# like s0 + s1.
#
# - If the variable is unbacked, only substitute if the substitution
# would preserve the bounds also under size-like-ness conditions.
if not issubset(tgt_bound, src_bound):
self.log.debug("skipped set_replacement %s = %s (%s) [%s not subset of %s]", a, tgt, msg, tgt_bound, src_bound)
return
elif a in self.size_like:
tgt_bound_so = self.bound_sympy(tgt, size_oblivious=True)
# This is morally equivalent to self.bound_sympy(a, size_oblivious=True)
# but handles substitutions like u0 == 0
src_bound_so = self.var_to_range[a]
if src_bound_so.upper >= 2:
src_bound_so &= ValueRanges(2, sympy.oo)
if not issubset(tgt_bound_so, src_bound_so):
self.log.debug("skipped set_replacement %s = %s (%s) "
"[%s not subset of %s (size-oblivious conditions)]", a, tgt, msg, tgt_bound_so, src_bound_so)
return
if config.print_specializations and isinstance(tgt, (sympy.Integer, sympy.Float)):
# specializing to a constant, which is likely unexpected
# NOTE(avik): It is possible that we try logging the same specialization multiple times, e.g.,
# when adding a to self.replacements, and again when simplifying an expression containing a.
# Thus to avoid duplication, checking whether a is in self.replacements isn't enough; if it is,
# it must not already map to `tgt`. Fortunately this check is cheap because `tgt` is a constant.
if a not in self.replacements or tgt != self.replacements[a]:
self.log.warning("Specializing %s to %s", self.var_to_sources[a][0].name(), tgt)
self.log.debug("SPECIALIZATION", stack_info=True)
log.info("set_replacement %s = %s (%s) %s", a, tgt, msg, tgt_bound)
self.replacements[a] = tgt
self._update_version_counter()
# When specializing 'a == tgt', the equality should be also conveyed to
# Z3, in case an expression uses 'a'.
self._add_target_expr(sympy.Eq(a, tgt))
def _add_divisible(self, expr: "sympy.Expr"):
self.divisible.add(expr)
self._update_version_counter()
@_lru_cache
@record_shapeenv_event()
def _find(self, a: "sympy.Symbol") -> "sympy.Expr":
"""
Implements a DSU-like algorithm to find the variable that represents a
Also handles transitive non-identity replacements.
a: b + c
c: d
"""
if a not in self.replacements:
return a
res = self.replacements[a]
cur_replace = {s: self._find(s) for s in res.free_symbols}
self._set_replacement(a, self.replacements[a].xreplace(cur_replace), "find")
return self.replacements[a]
@lru_cache(256)
def _maybe_guard_rel(self, expr: "sympy.Rel") -> None:
"""
The relational guard is guarded to be true. Use this information to
simplify shapes (i.e. a == b or a % 5 == 0)
"""
assert isinstance(expr, sympy.Rel)
# A good example of what goes wrong if you don't do this is
# python test/functorch/test_aotdispatch.py -k
# test_aot_autograd_symbolic_module_exhaustive_nn_LazyConv3d_cpu_float32
if isinstance(expr, sympy.Ne):
return
free = list(expr.free_symbols)
assert len(free) > 0, f"The expression should not be static by this point: {expr}"
# In case of really gnarly expression, we don't blow up
if len(free) > 5:
return
# Prioritize unbacked symints for solving by ordering them last.
# Prefer to simplify out lexicographically higher symbols (i.e. simplify out s4 over s3).
# (NB: this unfortunately isn't strictly equivalent to simplifying out newer symbols)
# Prefer to simplify out symbols with ephemeral sources.
def _smart_symbol_sort(x):
has_only_ephemeral_sources = (
x in self.var_to_sources and all(s.is_ephemeral() for s in self.var_to_sources[x])
)
size = self.size_hint(x, allow_none=True) or sys.maxsize
name = x.name
# 1 puts ephemeral sourced symbols first when sorting in reverse
return (1 if has_only_ephemeral_sources else 0, size, name)
free = sorted(free, key=_smart_symbol_sort, reverse=True) # type: ignore[attr-defined]
lhs = expr.lhs
rhs = expr.rhs
self._refine_ranges(expr)
# The rest of this stuff is for equality only
if not isinstance(expr, sympy.Eq):
return
if not expr.has(Mod):
try:
floor_div_atoms = lhs.atoms(FloorDiv).union(rhs.atoms(FloorDiv))
if len(floor_div_atoms) > 0 and any(a.divisor != 1 for a in floor_div_atoms):
raise NotImplementedError
# short-circuit when no solving is needed
if isinstance(lhs, sympy.Symbol) and free_unbacked_symbols(lhs):
self._set_replacement(lhs, self._find(rhs), "trivial_lhs")
elif isinstance(rhs, sympy.Symbol) and free_unbacked_symbols(rhs):
self._set_replacement(rhs, self._find(lhs), "trivial_rhs")
else:
r = try_solve(expr, free[0], floordiv_inequality=False)
if r is not None and all(t.is_integer for t in sympy.preorder_traversal(r[1])):
new_var = self._find(r[1])
ok = False
if self.is_unbacked_symint(free[0]):
# If you have i0 + i1 + i2 = s0, don't substitute i2 =
# s0 - i0 - i1. Arguably this should be OK but the
# runtime assert machinery is very delicate right now
# so this causes things to fail e.g.,
# test_split_unbacked_sizes
ok = len(free_unbacked_symbols(new_var)) <= 1
msg = "solve_unbacked"
else:
# Never substitute backed with unbacked
ok = len(free_unbacked_symbols(new_var)) == 0
msg = "solve_backed"
if ok:
self._set_replacement(cast(sympy.Symbol, free[0]), new_var, msg)
except NotImplementedError:
pass
if expr.has(Mod):
mod_expr = next(iter(expr.atoms(Mod)))
try:
r = try_solve(expr, mod_expr, floordiv_inequality=False)
if r is not None and r[1] == 0:
self._add_divisible(mod_expr)
# This is a little bit of extra logic to make things like
# torch.empty(i0, q).view(c, -1, q) work out
p, q = mod_expr.args
if isinstance(q, sympy.Number) and isinstance(p, sympy.Mul) and len(p.args) == 2:
c, i0 = p.args
# Given Mod(c * i0, q) == 0
if (
isinstance(c, sympy.Number) and
isinstance(i0, sympy.Symbol) and
self.is_unbacked_symint(i0)
):
# We have Mod(i0, q / c) == 0, which means we can
# rewrite i0 as (q / gcd(q, c)) * i1
d = q / sympy.gcd(q, c)
i1 = self.create_unbacked_symint().node.expr
# Propagate the value ranges. It doesn't really
# matter if we use truediv or floordiv, because we
# have established divisibility.
self.var_to_range[i1] = SymPyValueRangeAnalysis.truediv(
self.var_to_range[i0], ValueRanges.wrap(d)
)
# Propagate size-like-ness
if i0 in self.size_like:
self.size_like.add(i1)
self._set_replacement(i0, d * i1, "divisibility")
except NotImplementedError:
pass
return
# See: Note - On 0/1 specialization
# NB: sys.maxsize is NOT allowed for sizes, because we use MAX_INT
# as a sentinel sometimes. Your sizevar isn't going to be
# anywhere near the max 64-bit integer anyway.
def _default_value_range(self) -> ValueRanges:
lower = 2 if self.specialize_zero_one else 0
return ValueRanges(lower, sys.maxsize - 1)
def _default_unspecified_value_range(self) -> ValueRanges:
return ValueRanges(-sys.maxsize - 1, sys.maxsize)
@_lru_cache
def _simplify_floor_div(self, expr):
floor_divs = tuple(expr.atoms(FloorDiv))
# we expect floor_divs to be exact,
# and thus add the guards for the exact floordivs,
# even if tracing doesn't require them otherwise
for fd in reversed(floor_divs):
base, divisor = fd.args
mod_expr = Mod(base, divisor)
eq_expr = sympy.Eq(mod_expr, 0)
# add necessary mod guards
self.evaluate_expr(eq_expr)
return self.simplify(expr)
# We're about to add a guard/runtime assert, check if the ShapeEnv is frozen
# and if so issue a warning
def _check_frozen(self, expr, concrete_val):
if self.frozen:
self.counter["ignored_backward_guard"] += 1
signpost_event(
"dynamic",
"evaluate_expr_frozen",
{
**self.co_fields,
"ignored_guard": f"{expr} == {concrete_val}",
# no version = original state (this signpost is expected)
# version 2 = dynamic backwards is eagerly compiled
"version": 2,
},
)
log.warning("Ignored guard %s == %s, this could result in accuracy problems", expr, concrete_val)
def _get_stack_summary(self, is_debug: bool = False):
fsummary = None
frame = inspect.currentframe()
try:
while frame is not None:
if frame.f_code.co_filename not in uninteresting_files():
fsummary = traceback.FrameSummary(
frame.f_code.co_filename,
frame.f_lineno,
frame.f_code.co_name,
)
break
frame = frame.f_back
finally:
del frame
# NB: this stack is truncated, but it's fine because the main
# stack_info will give you the rest of the info you need
maybe_user_loc = ""
user_tb = TracingContext.extract_stack()
if user_tb:
maybe_user_loc = " at " + format_frame(user_tb[-1])
maybe_extra_debug = ""
if is_debug and user_tb:
maybe_extra_debug = (
'\nUser Stack (most recent call last):\n' +
' (snipped, see stack below for prefix)\n' +
''.join(traceback.format_list(user_tb))
)
if is_debug and config.extended_debug_cpp:
cpp_stack = CapturedTraceback.extract(cpp=True)
maybe_extra_debug += "\nC++ stack trace:\n" + ''.join(cpp_stack.format())
return fsummary, maybe_user_loc, maybe_extra_debug
def _log_guard(self, prefix: str, g, forcing_spec: bool):
if self.log.isEnabledFor(logging.INFO):
str_g = str(g)
is_debug = config.extended_debug_guard_added is not None and str_g == config.extended_debug_guard_added
fsummary, maybe_user_loc, maybe_extra_debug = self._get_stack_summary(is_debug)
self.log.info(
"%s %s [guard added]%s (%s)%s",
prefix if not forcing_spec else f"{prefix} (forcing_spec)",
str_g,
maybe_user_loc,
format_frame(fsummary),
maybe_extra_debug,
stack_info=is_debug,
)
@lru_cache(256)
@record_shapeenv_event(save_tracked_fakes=True)
def evaluate_expr(self, orig_expr: "sympy.Expr", hint=None, fx_node=None,
expect_rational=True, size_oblivious: bool = False, *, forcing_spec: bool = False):
"""
Given an expression, evaluates it, adding guards if necessary
"""
# TODO: split conjunctions and evaluate them separately
@lru_cache(None)
def compute_concrete_val():
if hint is None:
return self.size_hint(orig_expr)
else:
return sympy.sympify(hint)
# Check if:
# 1. 'translation_validation' is set
# 2. the corresponding 'fx_node' is not 'None'
# 3. the guard should not be suppressed
#
# If all of the above check, we create an FX node representing the
# actual expression to be guarded.
node = None
fresh = False
if (
self._translation_validation_enabled
and fx_node is not None
and not self._suppress_guards_tls()
and not size_oblivious
):
concrete_val = compute_concrete_val()
if concrete_val is sympy.true:
node, fresh = self._create_fx_call_function(torch._assert, (fx_node,))
elif concrete_val is sympy.false:
neg, _ = self._create_fx_call_function(operator.not_, (fx_node,))
node, fresh = self._create_fx_call_function(torch._assert, (neg,))
else:
eql, _ = self._create_fx_call_function(operator.eq, (fx_node, concrete_val))
node, fresh = self._create_fx_call_function(torch._assert, (eql,))
assert node is not None
# If this is a fresh node, we have to remember the event index that
# corresponds to this assertion node.
# Reason: so that, given an assertion node, we can replay the ShapeEnv
# events until the point where this assertion node was freshly created.
if fresh:
self._add_fx_node_metadata(node)
# After creating the FX node corresponding to orig_expr, we must make sure that
# no error will be raised until the end of this function.
#
# Reason: the translation validation may become invalid otherwise.
#
# If an error is raised before the end of this function, we remove the FX node
# inserted, and re-raise the error.
guard = None
tb = None
try:
if orig_expr.is_number:
self.log.debug("eval %s [trivial]", orig_expr)
# NB: don't test float as there may be precision issues
if isinstance(hint, (int, bool)):
assert orig_expr == hint, f"{orig_expr} != {hint}"
return orig_expr
expr = orig_expr
static_expr = self._maybe_evaluate_static(expr,
expect_rational=expect_rational,
size_oblivious=size_oblivious)
if static_expr is not None:
self.log.debug("eval %s == %s [statically known]", orig_expr, static_expr)
# NB: don't test float as there may be precision issues
if isinstance(hint, (int, bool)):
assert static_expr == hint, f"{static_expr} != {hint}"
return static_expr
if not (expr.free_symbols <= self.var_to_val.keys()):
# TODO: dedupe this with _maybe_evaluate_static
# Attempt to eliminate the unbacked SymInt
new_expr = self._maybe_evaluate_static(expr, unbacked_only=True)
if not (new_expr.free_symbols <= self.var_to_val.keys()):
size_oblivious_result = None
if not size_oblivious:
size_oblivious_result = self._maybe_evaluate_static(
expr,
expect_rational=expect_rational,
size_oblivious=True
)
raise self._make_data_dependent_error(
expr.xreplace(self.var_to_val),
expr,
size_oblivious_result=size_oblivious_result
)
expr = new_expr
concrete_val = compute_concrete_val()
self._check_frozen(expr, concrete_val)
if (
config.inject_EVALUATE_EXPR_flip_equality_TESTING_ONLY
and isinstance(hint, bool)
and isinstance(expr, (sympy.Eq, sympy.Ne))
):
expr = sympy.Not(expr)
# Turn this into a boolean expression, no longer need to consult
# concrete_val
suppress_maybe_guard_rel = False
if concrete_val is sympy.true:
g = expr
elif concrete_val is sympy.false:
g = sympy.Not(expr)
else:
# WARNING: we cannot actually do simplifications on guards
# on floating point values, because Sympy generally does not
# think expressions on integers can ever be equal to floating
# point (e.g., sympy.Eq(s0/6, 0.5) evaluates to False). Without
# very clear algebraic laws that hold for floating point, such
# simplifications are error prone anyway, so be sure not to
# maybe_guard_rel in those cases.
if not isinstance(concrete_val, sympy.Integer):
suppress_maybe_guard_rel = True
g = sympy.Eq(expr, concrete_val) # type: ignore[arg-type]
if isinstance(g, sympy.Rel):
# TODO: If we successfully eliminate a symbol via equality, it
# is not actually necessary to save a guard for the equality,
# as we will implicitly generate a guard when we match that
# input against the symbol. Probably the easiest way to
# implement this is to have maybe_guard_rel return a bool
# saying if it "subsumed" the guard (and therefore the guard
# is no longer necessary)
self._maybe_guard_rel(g)
if not self._suppress_guards_tls():
stack = CapturedTraceback.extract(skip=1)
guard = ShapeGuard(g, stack)
# TODO: deal with duplicate guards somehow
self.guards.append(guard)
except Exception:
if fresh:
self._remove_fx_node(node)
raise
else:
if not self._suppress_guards_tls():
assert guard is not None
self._log_guard("eval", g, forcing_spec=forcing_spec)
for s in g.free_symbols:
self.symbol_guard_counter[s] += 1
# Forcing_spec to avoid infinite recursion
if (
not forcing_spec and
config.symbol_guard_limit_before_specialize is not None and
self.symbol_guard_counter[s] > config.symbol_guard_limit_before_specialize
):
# Force specialization
self.log.info(
"symbol_guard_limit_before_specialize=%s exceeded on %s",
config.symbol_guard_limit_before_specialize,
s
)
self.evaluate_expr(s, forcing_spec=True)
else:
self.log.debug("eval %s [guard suppressed]", g)
return concrete_val
def cleanup(self):
"""
Break reference cycles.
This destroys the stacks. If you really want to keep them, we
just need some way to break references on code objects.
"""
for g in self.guards:
g.stack.cleanup()
for s in self.var_to_stack.values():
s.cleanup()
for ras in self.deferred_runtime_asserts.values():
for ra in ras:
ra.stack.cleanup()
@record_shapeenv_event(save_tracked_fakes=True)
def defer_runtime_assert(self, orig_expr: "sympy.Expr", msg, fx_node=None):
"""Create an assert that is checked at runtime
Args:
orig_expr (sympy.Expr): Boolean expression to assert is true
msg (str): Message to display on assertion failure
fx_node (Optional, torch.fx.Node): node in ``self.graph`` corresponding
to the expression, if applicable
"""
expr = orig_expr
# TODO: split conjunctions and evaluate them separately
static_expr = self._maybe_evaluate_static(expr)
if static_expr is not None:
self.log.debug("runtime_assert %s == %s [statically known]", orig_expr, static_expr)
return static_expr
# Attempt to eliminate the unbacked SymInt
new_expr = self._maybe_evaluate_static(expr, unbacked_only=True)
if new_expr.free_symbols <= self.var_to_val.keys():
# Do a normal guard
return self.evaluate_expr(new_expr, fx_node=fx_node)
# NB: Don't use new_expr as expr; it could contain gunk like shape0
# which we don't want to guard on
# OK, we're definitely doing a runtime assert now
if (
self._translation_validation_enabled
and fx_node is not None
and not self._suppress_guards_tls()
):
node, fresh = self._create_fx_call_function(torch._assert, (fx_node,))
assert node is not None
if fresh:
self._add_fx_node_metadata(node)
self._check_frozen(expr, sympy.true)
# eliminate symbols on equality tests / refine ranges
if isinstance(expr, sympy.Rel):
self._maybe_guard_rel(expr)
if not self._suppress_guards_tls():
# canonicalise to remove equations that are trivially equal
orig_expr = expr
expr = canonicalize_bool_expr(expr)
stack = CapturedTraceback.extract(skip=1)
ra = RuntimeAssert(expr, msg, stack)
# TODO: Do this in a way that is less janky than int(s.name[1:])
cands = sorted([s for s in expr.free_symbols if s.name.startswith("u")], key=lambda s: int(s.name[1:]))
self.deferred_runtime_asserts.setdefault(cands[-1], []).append(ra)
self.num_deferred_runtime_asserts += 1
self._update_version_counter()
self._log_guard("runtime_assert", orig_expr, forcing_spec=False)
else:
self.log.debug("runtime_assert %s [guard suppressed]", expr)
return True
# Refines the ranges of the variables present in 'guard'.
#
# This function tries to refine the range of the variables inside
# 'guard' by reasoning about it. Specifically, when 'guard' is a
# 'sympy.Relational' operation.
#
# It does mainly 3 things:
# 1. Tries to isolate a variable in the left-hand side
# 2. Compute the value range of the right-hand side
# 3. Update the value range of the variable, if better
def _refine_ranges(self, expr: sympy.Expr) -> None:
expr = self.simplify(expr)
for symbol in expr.free_symbols:
assert isinstance(symbol, sympy.Symbol)
if isinstance(self.var_to_val.get(symbol, None), SingletonInt):
# Skip var_to_range logic for SingletonInt which is only used
# for jagged layout NestedTensors today
continue
r = try_solve(expr, symbol)
if r is None or not (symbol.is_integer and r[1].is_integer):
# Range refinement only supports integer symbols for now.
# There are lots of SymPy bugs when it comes to comparing
# reals and integers, so we skip that for now.
continue
r_expr, rhs = r
vr = self.var_to_range[symbol]
lower, upper = vr.lower, vr.upper
rhs_vr = bound_sympy(rhs, self.var_to_range)
_assert_bound_is_rational(rhs, rhs_vr)
# Let's suppose that we have a preexisting range for x [0, 100].
# Now, we issue a guard x > y, where the range for y is [50, 150].
# Then, lower = 0, rhs_vr.lower = 50 and therefore refinement can happen,
# refining x to [51, 100], since x must be greater than y, but the lowest
# y could be is 50.
#
# sympy.Eq may update both lower and upper bounds.
# sympy.G{t,e} may update the lower bound, only.
# sympy.L{t,e} may update the upper bound, only.
if lower < rhs_vr.lower and isinstance(r_expr, (sympy.Eq, sympy.Ge, sympy.Gt)):
# Strictly greater relations allow us to refine a bit more, since
# x < y implies that the lower bound for x is: y + 1.
lower = rhs_vr.lower + int(isinstance(r_expr, sympy.Gt))
if upper > rhs_vr.upper and isinstance(r_expr, (sympy.Eq, sympy.Le, sympy.Lt)):
upper = rhs_vr.upper - int(isinstance(r_expr, sympy.Lt))
# Do nothing if the new value range is no better than what we already have.
if vr == ValueRanges(lower, upper):
continue
# Updates the range and the guards corresponding to each bound of the symbol.
self.var_to_range[symbol] = ValueRanges(lower, upper)
# Clears the cache, since this update can change the result.
self._maybe_evaluate_static.cache_clear()
def _is_int(expr):
return isinstance(expr, SymInt) and expr.node.expr.is_number
# WARNING: This is legacy, DO NOT USE
def _is_dim_dynamic(t, d):
return hasattr(t, "_dynamo_dynamic_indices") and d in t._dynamo_dynamic_indices
|