Changeset 5156


Ignore:
Timestamp:
Sep 14, 2016, 2:56:54 PM (3 years ago)
Author:
nmedfort
Message:

Work on multiplexing and distribution passes + a few AST modification bug fixes.

Location:
icGREP/icgrep-devel/icgrep
Files:
1 added
22 edited

Legend:

Unmodified
Added
Removed
  • icGREP/icgrep-devel/icgrep/CMakeLists.txt

    r5154 r5156  
    7676SET(PABLO_SRC ${PABLO_SRC} pablo/optimizers/pablo_simplifier.cpp pablo/optimizers/codemotionpass.cpp)
    7777IF(ENABLE_MULTIPLEXING)
    78 SET(PABLO_SRC ${PABLO_SRC} pablo/optimizers/distributivepass.cpp pablo/passes/flattenassociativedfg.cpp pablo/passes/factorizedfg.cpp)
    79 SET(PABLO_SRC ${PABLO_SRC} pablo/optimizers/schedulingprepass.cpp pablo/optimizers/pablo_automultiplexing.cpp pablo/optimizers/pablo_bddminimization.cpp)
     78SET(PABLO_SRC ${PABLO_SRC} pablo/optimizers/booleanreassociationpass.cpp pablo/optimizers/distributivepass.cpp pablo/passes/flattenassociativedfg.cpp pablo/passes/factorizedfg.cpp)
     79SET(PABLO_SRC ${PABLO_SRC} pablo/optimizers/schedulingprepass.cpp pablo/optimizers/pablo_automultiplexing.cpp)
    8080ENDIF()
    8181
     
    151151
    152152IF(ENABLE_MULTIPLEXING)
    153 message(STATUS "Enabling Multiplexing")
    154 SET(BUDDY_ROOT "${CMAKE_SOURCE_DIR}/../buddy-2.4/src")
    155 SET(BUDDY_SOURCES ${BUDDY_ROOT}/bddop.cpp ${BUDDY_ROOT}/cache.cpp ${BUDDY_ROOT}/imatrix.cpp ${BUDDY_ROOT}/kernel.cpp)
    156 SET(BUDDY_SOURCES ${BUDDY_SOURCES} ${BUDDY_ROOT}/prime.cpp ${BUDDY_ROOT}/pairs.cpp ${BUDDY_ROOT}/reorder.cpp ${BUDDY_ROOT}/tree.cpp)
    157 add_library(BUDDY ${BUDDY_SOURCES})
    158 include_directories(${BUDDY_ROOT})
    159 target_link_libraries (PabloADT BUDDY)
    160 SET(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DENABLE_MULTIPLEXING")
    161 ENDIF()
     153    message(STATUS "Enabling Multiplexing")
     154    find_package(Z3 REQUIRED)
     155    include_directories(${Z3_INCLUDE_DIRS})
     156    target_link_libraries(PabloADT ${Z3_LIBRARIES})
     157    SET(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DENABLE_MULTIPLEXING")
     158ENDIF()
     159
    162160
    163161include_directories("${PROJECT_SOURCE_DIR}")
     
    176174    if(COMPILER_SUPPORTS_GNU11)
    177175      set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=gnu++11")
    178     else() 
    179       CHECK_CXX_COMPILER_FLAG("-std=gnu++0x" COMPILER_SUPPORTS_GNU0X)   
     176    else()
     177      CHECK_CXX_COMPILER_FLAG("-std=gnu++0x" COMPILER_SUPPORTS_GNU0X)
    180178      if(COMPILER_SUPPORTS_GNU0X)
    181179        set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=gnu++0x")
     
    202200ENDIF()
    203201
    204 IF (PRINT_TIMING_INFORMATION)   
     202IF (PRINT_TIMING_INFORMATION)
    205203    SET(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DPRINT_TIMING_INFORMATION")
    206204ENDIF()
    207205
    208206SET(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS} -O3 -DNDEBUG")
    209 SET(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS} -g -fsanitize=address -fno-omit-frame-pointer")
     207SET(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS} -g") # -fsanitize=address -fno-omit-frame-pointer
    210208
    211209add_test(
  • icGREP/icgrep-devel/icgrep/UCD/ucd_compiler.cpp

    r5081 r5156  
    128128    {0x10000, 0x10FFFF}};
    129129
    130 const UCDCompiler::RangeList UCDCompiler::noIfHierachy = {{0x10000, 0x10FFFF}};
     130const UCDCompiler::RangeList UCDCompiler::noIfHierachy = {{0x80, 0x10FFFF}};
    131131
    132132/** ------------------------------------------------------------------------------------------------------------- *
  • icGREP/icgrep-devel/icgrep/icgrep-devel.files

    r5037 r5156  
    12951295wc.cpp
    12961296util/ispc.h
     1297pablo/builder.cpp
     1298pablo/builder.hpp
     1299pablo/carry_data.cpp
     1300pablo/carry_data.h
     1301pablo/carry_manager.cpp
     1302pablo/carry_manager.h
     1303pablo/codegenstate.cpp
     1304pablo/codegenstate.h
     1305pablo/expression_map.hpp
     1306pablo/function.cpp
     1307pablo/function.h
     1308pablo/pabloAST.cpp
     1309pablo/pabloAST.h
     1310pablo/pablo_compiler.cpp
     1311pablo/pablo_compiler.h
     1312pablo/pablo_kernel.cpp
     1313pablo/pablo_kernel.h
     1314pablo/pablo_toolchain.cpp
     1315pablo/pablo_toolchain.h
     1316pablo/pe_advance.h
     1317pablo/pe_and.h
     1318pablo/pe_call.h
     1319pablo/pe_count.h
     1320pablo/pe_infile.h
     1321pablo/pe_integer.h
     1322pablo/pe_lookahead.h
     1323pablo/pe_matchstar.h
     1324pablo/pe_next.h
     1325pablo/pe_not.h
     1326pablo/pe_ones.h
     1327pablo/pe_or.h
     1328pablo/pe_scanthru.h
     1329pablo/pe_sel.h
     1330pablo/pe_setithbit.h
     1331pablo/pe_string.h
     1332pablo/pe_var.h
     1333pablo/pe_xor.h
     1334pablo/pe_zeroes.h
     1335pablo/printer_pablos.cpp
     1336pablo/printer_pablos.h
     1337pablo/ps_assign.h
     1338pablo/ps_if.cpp
     1339pablo/ps_if.h
     1340pablo/ps_while.cpp
     1341pablo/ps_while.h
     1342pablo/symbol_generator.cpp
     1343pablo/symbol_generator.h
     1344cc/cc_compiler.cpp
     1345cc/cc_compiler.h
     1346IDISA/idisa_avx_builder.cpp
     1347IDISA/idisa_avx_builder.h
     1348IDISA/idisa_builder.cpp
     1349IDISA/idisa_builder.h
     1350IDISA/idisa_i64_builder.cpp
     1351IDISA/idisa_i64_builder.h
     1352IDISA/idisa_sse_builder.cpp
     1353IDISA/idisa_sse_builder.h
     1354IDISA/idisa_target.cpp
     1355IDISA/idisa_target.h
     1356kernels/deletion.cpp
     1357kernels/deletion.h
     1358kernels/interface.cpp
     1359kernels/interface.h
     1360kernels/kernel.cpp
     1361kernels/kernel.h
     1362kernels/p2s_kernel.cpp
     1363kernels/p2s_kernel.h
     1364kernels/pipeline.cpp
     1365kernels/pipeline.h
     1366kernels/s2p_kernel.cpp
     1367kernels/s2p_kernel.h
     1368kernels/scanmatchgen.cpp
     1369kernels/scanmatchgen.h
     1370kernels/stdout_kernel.cpp
     1371kernels/stdout_kernel.h
     1372kernels/streamset.cpp
     1373kernels/streamset.h
     1374kernels/symboltablepipeline.cpp
     1375kernels/symboltablepipeline.h
     1376pablo/analysis/pabloverifier.cpp
     1377pablo/analysis/pabloverifier.hpp
     1378pablo/optimizers/booleanreassociationpass.cpp
     1379pablo/optimizers/booleanreassociationpass.h
     1380pablo/optimizers/codemotionpass.cpp
     1381pablo/optimizers/codemotionpass.h
     1382pablo/optimizers/distributivepass.cpp
     1383pablo/optimizers/distributivepass.h
     1384pablo/optimizers/graph-facade.hpp
     1385pablo/optimizers/pablo_automultiplexing.cpp
     1386pablo/optimizers/pablo_automultiplexing.hpp
     1387pablo/optimizers/pablo_bddminimization.cpp
     1388pablo/optimizers/pablo_bddminimization.h
     1389pablo/optimizers/pablo_simplifier.cpp
     1390pablo/optimizers/pablo_simplifier.hpp
     1391pablo/optimizers/schedulingprepass.cpp
     1392pablo/optimizers/schedulingprepass.h
     1393pablo/passes/factorizedfg.cpp
     1394pablo/passes/factorizedfg.h
     1395pablo/passes/flattenassociativedfg.cpp
     1396pablo/passes/flattenassociativedfg.h
     1397pablo/passes/flattenif.cpp
     1398pablo/passes/flattenif.hpp
     1399pablo/builder.cpp
     1400pablo/builder.hpp
     1401pablo/carry_data.cpp
     1402pablo/carry_data.h
     1403pablo/carry_manager.cpp
     1404pablo/carry_manager.h
     1405pablo/codegenstate.cpp
     1406pablo/codegenstate.h
     1407pablo/expression_map.hpp
     1408pablo/function.cpp
     1409pablo/function.h
     1410pablo/pablo_compiler.cpp
     1411pablo/pablo_compiler.h
     1412pablo/pablo_kernel.cpp
     1413pablo/pablo_kernel.h
     1414pablo/pablo_toolchain.cpp
     1415pablo/pablo_toolchain.h
     1416pablo/pabloAST.cpp
     1417pablo/pabloAST.h
     1418pablo/pe_advance.h
     1419pablo/pe_and.h
     1420pablo/pe_call.h
     1421pablo/pe_count.h
     1422pablo/pe_infile.h
     1423pablo/pe_integer.h
     1424pablo/pe_lookahead.h
     1425pablo/pe_matchstar.h
     1426pablo/pe_next.h
     1427pablo/pe_not.h
     1428pablo/pe_ones.h
     1429pablo/pe_or.h
     1430pablo/pe_scanthru.h
     1431pablo/pe_sel.h
     1432pablo/pe_setithbit.h
     1433pablo/pe_string.h
     1434pablo/pe_var.h
     1435pablo/pe_xor.h
     1436pablo/pe_zeroes.h
     1437pablo/printer_pablos.cpp
     1438pablo/printer_pablos.h
     1439pablo/ps_assign.h
     1440pablo/ps_if.cpp
     1441pablo/ps_if.h
     1442pablo/ps_while.cpp
     1443pablo/ps_while.h
     1444pablo/symbol_generator.cpp
     1445pablo/symbol_generator.h
     1446re/parsefailure.cpp
     1447re/parsefailure.h
     1448re/printer_re.cpp
     1449re/printer_re.h
     1450re/re_alt.h
     1451re/re_analysis.cpp
     1452re/re_analysis.h
     1453re/re_any.h
     1454re/re_assertion.h
     1455re/re_cc.cpp
     1456re/re_cc.h
     1457re/re_compiler.cpp
     1458re/re_compiler.h
     1459re/re_diff.cpp
     1460re/re_diff.h
     1461re/re_end.h
     1462re/re_intersect.cpp
     1463re/re_intersect.h
     1464re/re_memoizer.hpp
     1465re/re_name.h
     1466re/re_name_resolve.cpp
     1467re/re_name_resolve.h
     1468re/re_nullable.cpp
     1469re/re_nullable.h
     1470re/re_parser.cpp
     1471re/re_parser.h
     1472re/re_re.cpp
     1473re/re_re.h
     1474re/re_rep.cpp
     1475re/re_rep.h
     1476re/re_seq.h
     1477re/re_simplifier.cpp
     1478re/re_simplifier.h
     1479re/re_start.h
     1480re/re_toolchain.cpp
     1481re/re_toolchain.h
     1482UCD/Blocks.h
     1483UCD/CaseFolding_txt.cpp
     1484UCD/CaseFolding_txt.h
     1485UCD/DerivedAge.h
     1486UCD/DerivedBidiClass.h
     1487UCD/DerivedBinaryProperties.h
     1488UCD/DerivedCombiningClass.h
     1489UCD/DerivedCoreProperties.h
     1490UCD/DerivedDecompositionType.h
     1491UCD/DerivedGeneralCategory.h
     1492UCD/DerivedJoiningGroup.h
     1493UCD/DerivedJoiningType.h
     1494UCD/DerivedNumericType.h
     1495UCD/EastAsianWidth.h
     1496UCD/GraphemeBreakProperty.h
     1497UCD/HangulSyllableType.h
     1498UCD/LineBreak.h
     1499UCD/PropertyAliases.h
     1500UCD/PropertyObjects.cpp
     1501UCD/PropertyObjects.h
     1502UCD/PropertyObjectTable.h
     1503UCD/PropertyValueAliases.h
     1504UCD/PropList.h
     1505UCD/resolve_properties.cpp
     1506UCD/resolve_properties.h
     1507UCD/ScriptExtensions.h
     1508UCD/Scripts.h
     1509UCD/SentenceBreakProperty.h
     1510UCD/ucd_compiler.cpp
     1511UCD/ucd_compiler.hpp
     1512UCD/unicode_set.cpp
     1513UCD/unicode_set.h
     1514UCD/UnicodeNameData.cpp
     1515UCD/UnicodeNameData.h
     1516UCD/WordBreakProperty.h
     1517util/papi_helper.hpp
     1518util/slab_allocator.h
     1519grep_engine.cpp
     1520grep_engine.h
     1521hrtime.h
     1522icgrep.cpp
     1523object_cache.cpp
     1524object_cache.h
     1525symboltable.cpp
     1526toolchain.cpp
     1527toolchain.h
     1528u8u16.cpp
     1529utf16_encoder.cpp
     1530utf16_encoder.h
     1531utf8_encoder.cpp
     1532utf8_encoder.h
     1533utf_encoding.h
     1534wc.cpp
     1535pablo/optimizers/maxsat.hpp
     1536cc/cc_compiler.cpp
     1537cc/cc_compiler.h
     1538IDISA/CudaDriver.h
     1539IDISA/idisa_avx_builder.cpp
     1540IDISA/idisa_avx_builder.h
     1541IDISA/idisa_builder.cpp
     1542IDISA/idisa_builder.h
     1543IDISA/idisa_i64_builder.cpp
     1544IDISA/idisa_i64_builder.h
     1545IDISA/idisa_nvptx_builder.cpp
     1546IDISA/idisa_nvptx_builder.h
     1547IDISA/idisa_sse_builder.cpp
     1548IDISA/idisa_sse_builder.h
     1549IDISA/idisa_target.cpp
     1550IDISA/idisa_target.h
     1551IDISA/llvm2ptx.h
     1552kernels/deletion.cpp
     1553kernels/deletion.h
     1554kernels/interface.cpp
     1555kernels/interface.h
     1556kernels/kernel.cpp
     1557kernels/kernel.h
     1558kernels/p2s_kernel.cpp
     1559kernels/p2s_kernel.h
     1560kernels/pipeline.cpp
     1561kernels/pipeline.h
     1562kernels/s2p_kernel.cpp
     1563kernels/s2p_kernel.h
     1564kernels/scanmatchgen.cpp
     1565kernels/scanmatchgen.h
     1566kernels/stdout_kernel.cpp
     1567kernels/stdout_kernel.h
     1568kernels/streamset.cpp
     1569kernels/streamset.h
     1570kernels/symboltablepipeline.cpp
     1571kernels/symboltablepipeline.h
     1572pablo/analysis/pabloverifier.cpp
     1573pablo/analysis/pabloverifier.hpp
     1574pablo/optimizers/booleanreassociationpass.cpp
     1575pablo/optimizers/booleanreassociationpass.h
     1576pablo/optimizers/codemotionpass.cpp
     1577pablo/optimizers/codemotionpass.h
     1578pablo/optimizers/distributivepass.cpp
     1579pablo/optimizers/distributivepass.h
     1580pablo/optimizers/graph-facade.hpp
     1581pablo/optimizers/maxsat.hpp
     1582pablo/optimizers/pablo_automultiplexing.cpp
     1583pablo/optimizers/pablo_automultiplexing.hpp
     1584pablo/optimizers/pablo_bddminimization.cpp
     1585pablo/optimizers/pablo_bddminimization.h
     1586pablo/optimizers/pablo_simplifier.cpp
     1587pablo/optimizers/pablo_simplifier.hpp
     1588pablo/optimizers/schedulingprepass.cpp
     1589pablo/optimizers/schedulingprepass.h
     1590pablo/passes/factorizedfg.cpp
     1591pablo/passes/factorizedfg.h
     1592pablo/passes/flattenassociativedfg.cpp
     1593pablo/passes/flattenassociativedfg.h
     1594pablo/passes/flattenif.cpp
     1595pablo/passes/flattenif.hpp
     1596pablo/builder.cpp
     1597pablo/builder.hpp
     1598pablo/carry_data.cpp
     1599pablo/carry_data.h
     1600pablo/carry_manager.cpp
     1601pablo/carry_manager.h
     1602pablo/codegenstate.cpp
     1603pablo/codegenstate.h
     1604pablo/expression_map.hpp
     1605pablo/function.cpp
     1606pablo/function.h
     1607pablo/pablo_compiler.cpp
     1608pablo/pablo_compiler.h
     1609pablo/pablo_kernel.cpp
     1610pablo/pablo_kernel.h
     1611pablo/pablo_toolchain.cpp
     1612pablo/pablo_toolchain.h
     1613pablo/pabloAST.cpp
     1614pablo/pabloAST.h
     1615pablo/pe_advance.h
     1616pablo/pe_and.h
     1617pablo/pe_call.h
     1618pablo/pe_count.h
     1619pablo/pe_infile.h
     1620pablo/pe_integer.h
     1621pablo/pe_lookahead.h
     1622pablo/pe_matchstar.h
     1623pablo/pe_next.h
     1624pablo/pe_not.h
     1625pablo/pe_ones.h
     1626pablo/pe_or.h
     1627pablo/pe_scanthru.h
     1628pablo/pe_sel.h
     1629pablo/pe_setithbit.h
     1630pablo/pe_string.h
     1631pablo/pe_var.h
     1632pablo/pe_xor.h
     1633pablo/pe_zeroes.h
     1634pablo/printer_pablos.cpp
     1635pablo/printer_pablos.h
     1636pablo/ps_assign.h
     1637pablo/ps_if.cpp
     1638pablo/ps_if.h
     1639pablo/ps_while.cpp
     1640pablo/ps_while.h
     1641pablo/symbol_generator.cpp
     1642pablo/symbol_generator.h
     1643re/parsefailure.cpp
     1644re/parsefailure.h
     1645re/printer_re.cpp
     1646re/printer_re.h
     1647re/re_alt.h
     1648re/re_analysis.cpp
     1649re/re_analysis.h
     1650re/re_any.h
     1651re/re_assertion.h
     1652re/re_cc.cpp
     1653re/re_cc.h
     1654re/re_compiler.cpp
     1655re/re_compiler.h
     1656re/re_diff.cpp
     1657re/re_diff.h
     1658re/re_end.h
     1659re/re_intersect.cpp
     1660re/re_intersect.h
     1661re/re_memoizer.hpp
     1662re/re_name.h
     1663re/re_name_resolve.cpp
     1664re/re_name_resolve.h
     1665re/re_nullable.cpp
     1666re/re_nullable.h
     1667re/re_parser.cpp
     1668re/re_parser.h
     1669re/re_re.cpp
     1670re/re_re.h
     1671re/re_rep.cpp
     1672re/re_rep.h
     1673re/re_seq.h
     1674re/re_simplifier.cpp
     1675re/re_simplifier.h
     1676re/re_start.h
     1677re/re_toolchain.cpp
     1678re/re_toolchain.h
     1679UCD/Blocks.h
     1680UCD/CaseFolding_txt.cpp
     1681UCD/CaseFolding_txt.h
     1682UCD/DerivedAge.h
     1683UCD/DerivedBidiClass.h
     1684UCD/DerivedBinaryProperties.h
     1685UCD/DerivedCombiningClass.h
     1686UCD/DerivedCoreProperties.h
     1687UCD/DerivedDecompositionType.h
     1688UCD/DerivedGeneralCategory.h
     1689UCD/DerivedJoiningGroup.h
     1690UCD/DerivedJoiningType.h
     1691UCD/DerivedNumericType.h
     1692UCD/EastAsianWidth.h
     1693UCD/GraphemeBreakProperty.h
     1694UCD/HangulSyllableType.h
     1695UCD/LineBreak.h
     1696UCD/PropertyAliases.h
     1697UCD/PropertyObjects.cpp
     1698UCD/PropertyObjects.h
     1699UCD/PropertyObjectTable.h
     1700UCD/PropertyValueAliases.h
     1701UCD/PropList.h
     1702UCD/resolve_properties.cpp
     1703UCD/resolve_properties.h
     1704UCD/ScriptExtensions.h
     1705UCD/Scripts.h
     1706UCD/SentenceBreakProperty.h
     1707UCD/ucd_compiler.cpp
     1708UCD/ucd_compiler.hpp
     1709UCD/unicode_set.cpp
     1710UCD/unicode_set.h
     1711UCD/UnicodeNameData.cpp
     1712UCD/UnicodeNameData.h
     1713UCD/WordBreakProperty.h
     1714util/papi_helper.hpp
     1715util/slab_allocator.h
     1716generate_predefined_ucd_functions.cpp
     1717grep_engine.cpp
     1718grep_engine.h
     1719hrtime.h
     1720icgrep.cpp
     1721object_cache.cpp
     1722object_cache.h
     1723symboltable.cpp
     1724toolchain.cpp
     1725toolchain.h
     1726u8u16.cpp
     1727utf16_encoder.cpp
     1728utf16_encoder.h
     1729utf8_encoder.cpp
     1730utf8_encoder.h
     1731utf_encoding.h
     1732wc.cpp
     1733grep_engine.cpp
     1734grep_engine.h
     1735object_cache.cpp
     1736object_cache.h
     1737toolchain.cpp
     1738toolchain.h
     1739IDISA/CudaDriver.h
     1740IDISA/idisa_avx_builder.cpp
     1741IDISA/idisa_avx_builder.h
     1742IDISA/idisa_builder.cpp
     1743IDISA/idisa_builder.h
     1744IDISA/idisa_i64_builder.cpp
     1745IDISA/idisa_i64_builder.h
     1746IDISA/idisa_nvptx_builder.cpp
     1747IDISA/idisa_nvptx_builder.h
     1748IDISA/idisa_sse_builder.cpp
     1749IDISA/idisa_sse_builder.h
     1750IDISA/idisa_target.cpp
     1751IDISA/idisa_target.h
     1752IDISA/llvm2ptx.h
     1753kernels/deletion.cpp
     1754kernels/deletion.h
     1755kernels/interface.cpp
     1756kernels/interface.h
     1757kernels/kernel.cpp
     1758kernels/kernel.h
     1759kernels/p2s_kernel.cpp
     1760kernels/p2s_kernel.h
     1761kernels/pipeline.cpp
     1762kernels/pipeline.h
     1763kernels/s2p_kernel.cpp
     1764kernels/s2p_kernel.h
     1765kernels/scanmatchgen.cpp
     1766kernels/scanmatchgen.h
     1767kernels/stdout_kernel.cpp
     1768kernels/stdout_kernel.h
     1769kernels/streamset.cpp
     1770kernels/streamset.h
     1771kernels/symboltablepipeline.cpp
     1772kernels/symboltablepipeline.h
     1773pablo/analysis/pabloverifier.cpp
     1774pablo/analysis/pabloverifier.hpp
     1775pablo/optimizers/booleanreassociationpass.cpp
     1776pablo/optimizers/booleanreassociationpass.h
     1777pablo/optimizers/codemotionpass.cpp
     1778pablo/optimizers/codemotionpass.h
     1779pablo/optimizers/distributivepass.cpp
     1780pablo/optimizers/distributivepass.h
     1781pablo/optimizers/graph-facade.hpp
     1782pablo/optimizers/maxsat.hpp
     1783pablo/optimizers/pablo_automultiplexing.cpp
     1784pablo/optimizers/pablo_automultiplexing.hpp
     1785pablo/optimizers/pablo_bddminimization.cpp
     1786pablo/optimizers/pablo_bddminimization.h
     1787pablo/optimizers/pablo_simplifier.cpp
     1788pablo/optimizers/pablo_simplifier.hpp
     1789pablo/optimizers/schedulingprepass.cpp
     1790pablo/optimizers/schedulingprepass.h
     1791pablo/passes/factorizedfg.cpp
     1792pablo/passes/factorizedfg.h
     1793pablo/passes/flattenassociativedfg.cpp
     1794pablo/passes/flattenassociativedfg.h
     1795pablo/passes/flattenif.cpp
     1796pablo/passes/flattenif.hpp
     1797pablo/builder.cpp
     1798pablo/builder.hpp
     1799pablo/carry_data.cpp
     1800pablo/carry_data.h
     1801pablo/carry_manager.cpp
     1802pablo/carry_manager.h
     1803pablo/codegenstate.cpp
     1804pablo/codegenstate.h
     1805pablo/expression_map.hpp
     1806pablo/function.cpp
     1807pablo/function.h
     1808pablo/pablo_compiler.cpp
     1809pablo/pablo_compiler.h
     1810pablo/pablo_kernel.cpp
     1811pablo/pablo_kernel.h
     1812pablo/pablo_toolchain.cpp
     1813pablo/pablo_toolchain.h
     1814pablo/pabloAST.cpp
     1815pablo/pabloAST.h
     1816pablo/pe_advance.h
     1817pablo/pe_and.h
     1818pablo/pe_call.h
     1819pablo/pe_count.h
     1820pablo/pe_infile.h
     1821pablo/pe_integer.h
     1822pablo/pe_lookahead.h
     1823pablo/pe_matchstar.h
     1824pablo/pe_next.h
     1825pablo/pe_not.h
     1826pablo/pe_ones.h
     1827pablo/pe_or.h
     1828pablo/pe_scanthru.h
     1829pablo/pe_sel.h
     1830pablo/pe_setithbit.h
     1831pablo/pe_string.h
     1832pablo/pe_var.h
     1833pablo/pe_xor.h
     1834pablo/pe_zeroes.h
     1835pablo/printer_pablos.cpp
     1836pablo/printer_pablos.h
     1837pablo/ps_assign.h
     1838pablo/ps_if.cpp
     1839pablo/ps_if.h
     1840pablo/ps_while.cpp
     1841pablo/ps_while.h
     1842pablo/symbol_generator.cpp
     1843pablo/symbol_generator.h
     1844util/papi_helper.hpp
     1845util/slab_allocator.h
  • icGREP/icgrep-devel/icgrep/icgrep.cpp

    r5154 r5156  
    2121
    2222#include <iostream> // MEEE
     23
     24#ifdef PRINT_TIMING_INFORMATION
     25#include <hrtime.h>
     26#include <util/papi_helper.hpp>
     27#endif
     28
    2329static cl::OptionCategory LegacyGrepOptions("A. Standard Grep Options",
    2430                                       "These are standard grep options intended for compatibility with typical grep usage.");
     
    228234
    229235    if (Threads <= 1) {
     236
     237        #ifdef PRINT_TIMING_INFORMATION
     238        // PAPI_RES_STL, PAPI_STL_CCY, PAPI_FUL_CCY, PAPI_MEM_WCY
     239        // PAPI_RES_STL, PAPI_BR_MSP, PAPI_LST_INS, PAPI_L1_TCM
     240        papi::PapiCounter<4> papiCounters({PAPI_RES_STL, PAPI_STL_CCY, PAPI_FUL_CCY, PAPI_MEM_WCY});
     241        #endif
    230242        for (unsigned i = 0; i != inputFiles.size(); ++i) {
     243            #ifdef PRINT_TIMING_INFORMATION
     244            papiCounters.start();
     245            const timestamp_t execution_start = read_cycle_counter();
     246            #endif
    231247            grepEngine.doGrep(inputFiles[i], i, CountOnly, total_CountOnly, UTF_16);
     248            #ifdef PRINT_TIMING_INFORMATION
     249            const timestamp_t execution_end = read_cycle_counter();
     250            papiCounters.stop();
     251            std::cerr << "EXECUTION TIME: " << inputFiles[i] << ":" << "CYCLES|" << (execution_end - execution_start) << papiCounters << std::endl;
     252            #endif
    232253        }       
    233254    } else if (Threads > 1) {
  • icGREP/icgrep-devel/icgrep/pablo/analysis/pabloverifier.cpp

    r5082 r5156  
    1919 ** ------------------------------------------------------------------------------------------------------------- */
    2020template<typename VectorType>
    21 bool checkVector(const Statement * value, const VectorType & vector) {
     21inline bool checkVector(const PabloAST * const value, const VectorType & vector, size_t & uses) {
    2222    for (auto escapedValue : vector) {
    2323        if (escapedValue == value) {
     24            ++uses;
    2425            return false;
    2526        }
     
    2829}
    2930
    30 void verifyUseDefInformation(const PabloBlock * block, const ScopeSet & validScopes) {
    31     for (const Statement * stmt : *block) {
    32         for (const PabloAST * use : stmt->users()) {
    33             if (LLVM_LIKELY(isa<Statement>(use))) {
     31void testUsers(const PabloAST * expr, const ScopeSet & validScopes) {
     32    if (isa<Count>(expr)) { // !! matchedLineCount is not being correctly added to the function !!
     33        return;
     34    }
     35    size_t uses = 0;
     36    SmallSet<const PabloAST *> verified;
     37    for (const PabloAST * use : expr->users()) {
     38        if (LLVM_LIKELY(isa<Statement>(use))) {
     39            if (LLVM_LIKELY(verified.count(use) == 0)) {
    3440                const Statement * const user = cast<Statement>(use);
    3541                // test whether this user is in a block in the program
     
    4046                    PabloPrinter::print(user, str);
    4147                    str << " is a user of ";
    42                     PabloPrinter::print(stmt, str);
     48                    PabloPrinter::print(expr, str);
    4349                    if (user->getParent() == nullptr) {
    4450                        str << " but is not in any scope.";
     
    4854                    throw std::runtime_error(str.str());
    4955                }
     56                // expr may be used more than once by the same user.
    5057                bool notFound = true;
    5158                for (unsigned i = 0; i != user->getNumOperands(); ++i) {
    52                     if (user->getOperand(i) == stmt) {
     59                    if (user->getOperand(i) == expr) {
    5360                        notFound = false;
     61                        ++uses;
     62                    }
     63                }
     64                if (const If * ifNode = dyn_cast<If>(expr)) {
     65                    notFound &= checkVector(user, ifNode->getDefined(), uses);
     66                } else if (const If * ifNode = dyn_cast<If>(user)) {
     67                    notFound &= checkVector(expr, ifNode->getDefined(), uses);
     68                } else if (const While * whileNode = dyn_cast<While>(expr)) {
     69                    notFound &= checkVector(user, whileNode->getVariants(), uses);
     70                } else if (const While * whileNode = dyn_cast<While>(user)) {
     71                    notFound &= checkVector(expr, whileNode->getVariants(), uses);
     72                } else if (isa<Next>(expr) && isa<Assign>(use)) {
     73                    notFound &= (use != cast<Next>(expr)->getInitial());
     74                }
     75                if (LLVM_UNLIKELY(notFound)) {
     76                    std::string tmp;
     77                    raw_string_ostream str(tmp);
     78                    str << "PabloVerifier: use-def error: ";
     79                    PabloPrinter::print(expr, str);
     80                    str << " is not a definition of ";
     81                    PabloPrinter::print(use, str);
     82                    throw std::runtime_error(str.str());
     83                }
     84                verified.insert(use);
     85            }
     86        } else if (LLVM_UNLIKELY(isa<PabloFunction>(use))) {
     87            if (LLVM_LIKELY(verified.count(use) == 0)) {
     88                const PabloFunction * f = cast<PabloFunction>(use);
     89                bool isParameter = false;
     90                bool isResult = false;
     91                for (unsigned i = 0; i != f->getNumOfParameters(); ++i) {
     92                    if (f->getParameter(i) == expr) {
     93                        isParameter = true;
    5494                        break;
    5595                    }
    5696                }
    57                 if (LLVM_UNLIKELY(notFound)) {
    58                     if (const If * ifNode = dyn_cast<If>(stmt)) {
    59                         notFound = checkVector(user, ifNode->getDefined());
    60                     } else if (const If * ifNode = dyn_cast<If>(user)) {
    61                         notFound = checkVector(stmt, ifNode->getDefined());
    62                     } else if (const While * whileNode = dyn_cast<While>(stmt)) {
    63                         notFound = checkVector(user, whileNode->getVariants());
    64                     } else if (const While * whileNode = dyn_cast<While>(user)) {
    65                         notFound = checkVector(stmt, whileNode->getVariants());
    66                     } else if (isa<Next>(stmt) && isa<Assign>(use)) {
    67                         notFound = (use != cast<Next>(stmt)->getInitial());
    68                     }
    69                     if (LLVM_UNLIKELY(notFound)) {
    70                         std::string tmp;
    71                         raw_string_ostream str(tmp);
    72                         str << "PabloVerifier: use-def error: ";
    73                         PabloPrinter::print(stmt, str);
    74                         str << " is not a definition of ";
    75                         PabloPrinter::print(use, str);
    76                         throw std::runtime_error(str.str());
    77                     }
    78                 }
    79             }
    80         }
    81         for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
    82             const PabloAST * const def = stmt->getOperand(i);
    83             bool notFound = true;
    84             for (const PabloAST * use : def->users()) {
    85                 if (use == stmt) {
    86                     notFound = false;
    87                     break;
    88                 }
    89             }
    90             if (LLVM_UNLIKELY(notFound)) {
    91                 std::string tmp;
    92                 raw_string_ostream str(tmp);
    93                 str << "PabloVerifier: def-use error: ";
    94                 PabloPrinter::print(stmt, str);
    95                 str << " is not recorded in ";
    96                 PabloPrinter::print(def, str);
    97                 str << "'s user list";
    98                 throw std::runtime_error(str.str());
    99             }
    100         }
     97                for (unsigned i = 0; i != f->getNumOfResults(); ++i) {
     98                    if (f->getResult(i) == expr) {
     99                        isResult = true;
     100                        break;
     101                    }
     102                }
     103                if (LLVM_UNLIKELY(!(isParameter ^ isResult))) {
     104                    std::string tmp;
     105                    raw_string_ostream str(tmp);
     106                    str << "PabloVerifier: use-def error: ";
     107                    PabloPrinter::print(expr, str);
     108                    if (isParameter && isResult) {
     109                        str << " is both a parameter and result of ";
     110                    } else {
     111                        str << " is not a parameter or result of ";
     112                    }
     113                    PabloPrinter::print(f, str);
     114                    throw std::runtime_error(str.str());
     115                }
     116                ++uses;
     117                verified.insert(use);
     118            }
     119        } else {
     120            std::string tmp;
     121            raw_string_ostream str(tmp);
     122            str << "PabloVerifier: use-def error: expression ";
     123            PabloPrinter::print(use, str);
     124            str << " is incorrectly reported as a user of ";
     125            PabloPrinter::print(expr, str);
     126            throw std::runtime_error(str.str());
     127        }
     128    }
     129    if (LLVM_UNLIKELY(uses != expr->getNumUses())) {
     130        std::string tmp;
     131        raw_string_ostream str(tmp);
     132        str << "PabloVerifier: use-def error: ";
     133        PabloPrinter::print(expr, str);
     134        str << " is reported having " << expr->getNumUses() << " user(s)"
     135            << " but was observed having " << uses << " user(s)";
     136        throw std::runtime_error(str.str());
     137    }
     138}
     139
     140void testDefs(const Statement * stmt) {
     141    for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
     142        const PabloAST * const def = stmt->getOperand(i);
     143        bool notFound = true;
     144        for (const PabloAST * use : def->users()) {
     145            if (use == stmt) {
     146                notFound = false;
     147                break;
     148            }
     149        }
     150        if (LLVM_UNLIKELY(notFound)) {
     151            std::string tmp;
     152            raw_string_ostream str(tmp);
     153            str << "PabloVerifier: def-use error: ";
     154            PabloPrinter::print(stmt, str);
     155            str << " is not recorded in ";
     156            PabloPrinter::print(def, str);
     157            str << "'s user list";
     158            throw std::runtime_error(str.str());
     159        }
     160    }
     161}
     162
     163void verifyUseDefInformation(const PabloBlock * block, const ScopeSet & validScopes) {
     164    for (const Statement * stmt : *block) {
     165        testUsers(stmt, validScopes);
     166        testDefs(stmt);
    101167        if (LLVM_UNLIKELY(isa<If>(stmt) || isa<While>(stmt))) {
    102168            verifyUseDefInformation(isa<If>(stmt) ? cast<If>(stmt)->getBody() : cast<While>(stmt)->getBody(), validScopes);
     
    117183    ScopeSet validScopes;
    118184    gatherValidScopes(function.getEntryBlock(), validScopes);
     185    for (unsigned i = 0; i < function.getNumOfParameters(); ++i) {
     186        testUsers(function.getParameter(i), validScopes);
     187    }
     188    for (unsigned i = 0; i < function.getNumOfResults(); ++i) {
     189        testDefs(function.getResult(i));
     190    }
    119191    verifyUseDefInformation(function.getEntryBlock(), validScopes);
    120192}
     
    189261    PabloPrinter::print(stmt, str);
    190262    str << " branches into a scope block that reports ";
    191     PabloPrinter::print(stmt, str);
     263    PabloPrinter::print(branch, str);
    192264    str << " as its branching statement.";
    193265    throw std::runtime_error(str.str());
  • icGREP/icgrep-devel/icgrep/pablo/carry_manager.cpp

    r5142 r5156  
    4545   
    4646    Value * cdArrayPtr = iBuilder->CreateGEP(mSelf, {ConstantInt::get(iBuilder->getSizeTy(), 0), mKernelBuilder->getScalarIndex("carries")});
    47 #ifndef NDEBUG
    48     iBuilder->CallPrintInt("cdArrayPtr", iBuilder->CreatePtrToInt(cdArrayPtr, iBuilder->getSizeTy()));
    49 #endif
     47//#ifndef NDEBUG
     48//    iBuilder->CallPrintInt("cdArrayPtr", iBuilder->CreatePtrToInt(cdArrayPtr, iBuilder->getSizeTy()));
     49//#endif
    5050    mCarryPackBasePtr = iBuilder->CreateBitCast(cdArrayPtr, PointerType::get(mCarryPackType, 0));
    5151    mCarryBitBlockPtr = iBuilder->CreateBitCast(cdArrayPtr, PointerType::get(mBitBlockType, 0));
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/booleanreassociationpass.cpp

    r5152 r5156  
    1414#include <llvm/Support/CommandLine.h>
    1515#include "maxsat.hpp"
     16
     17//  noif-dist-mult-dist-50 \p{Cham}(?<!\p{Mc})
    1618
    1719using namespace boost;
     
    273275    Z3_context ctx = Z3_mk_context(cfg);
    274276    Z3_del_config(cfg);
    275     Z3_solver solver = Z3_mk_solver(ctx);
    276     Z3_solver_inc_ref(ctx, solver);
    277 
    278     BooleanReassociationPass brp(ctx, solver, function);
     277
     278    Z3_params params = Z3_mk_params(ctx);
     279    Z3_params_inc_ref(ctx, params);
     280    Z3_params_set_bool(ctx, params, Z3_mk_string_symbol(ctx, "pull_cheap_ite"), true);
     281    Z3_params_set_bool(ctx, params, Z3_mk_string_symbol(ctx, "local_ctx"), true);
     282
     283    Z3_tactic ctx_solver_simplify = Z3_mk_tactic(ctx, "ctx-solver-simplify");
     284    Z3_tactic_inc_ref(ctx, ctx_solver_simplify);
     285
     286    BooleanReassociationPass brp(ctx, params, ctx_solver_simplify, function);
    279287    brp.processScopes(function);
    280288
    281     Z3_solver_dec_ref(ctx, solver);
     289    Z3_params_dec_ref(ctx, params);
     290    Z3_tactic_dec_ref(ctx, ctx_solver_simplify);
    282291    Z3_del_context(ctx);
     292
     293    PabloVerifier::verify(function, "post-reassociation");
    283294
    284295    Simplifier::optimize(function);
     
    308319 ** ------------------------------------------------------------------------------------------------------------- */
    309320void BooleanReassociationPass::processScopes(PabloBlock * const block, CharacterizationMap & map) {
    310     Z3_solver_push(mContext, mSolver);
    311321    for (Statement * stmt = block->front(); stmt; ) {
    312322        if (LLVM_UNLIKELY(isa<If>(stmt))) {
     
    335345            stmt = characterize(stmt, map);
    336346        }
    337     }
     347    }   
    338348    distributeScope(block, map);
    339     Z3_solver_pop(mContext, mSolver, 1);
    340349}
    341350
     
    385394        return stmt->getNextNode();
    386395    }
    387     node = Z3_simplify(mContext, node); assert (node);
     396    node = simplify(node); assert (node);
    388397    PabloAST * const replacement = map.findKey(node);
    389398    if (LLVM_LIKELY(replacement == nullptr)) {
     
    399408 * @brief processScope
    400409 ** ------------------------------------------------------------------------------------------------------------- */
    401 inline void BooleanReassociationPass::distributeScope(PabloBlock * const block, CharacterizationMap & map) {
     410inline void BooleanReassociationPass::distributeScope(PabloBlock * const block, CharacterizationMap & C) {
    402411    Graph G;
    403412    try {
    404         transformAST(block, map, G);
     413        mBlock = block;
     414        transformAST(C, G);
    405415    } catch (std::runtime_error err) {
    406         printGraph(G, "G");
     416        printGraph(G, "E");
     417        throw err;
     418    } catch (std::exception err) {
     419        printGraph(G, "E");
    407420        throw err;
    408421    }
     
    415428 * are "flattened" (i.e., allowed to have any number of inputs.)
    416429 ** ------------------------------------------------------------------------------------------------------------- */
    417 void BooleanReassociationPass::transformAST(PabloBlock * const block, CharacterizationMap & C, Graph & G) {
     430void BooleanReassociationPass::transformAST(CharacterizationMap & C, Graph & G) {
     431
    418432    StatementMap S;
     433
    419434    // Compute the base def-use graph ...
    420     for (Statement * stmt : *block) {
     435    for (Statement * stmt : *mBlock) {
    421436
    422437        const Vertex u = makeVertex(stmt->getClassTypeId(), stmt, S, G, C.get(stmt));
     
    433448                const Vertex v = makeVertex(TypeId::Var, def, C, S, G);
    434449                add_edge(def, u, v, G);
    435                 resolveNestedUsages(block, def, v, C, S, G, stmt);
     450                resolveNestedUsages(def, v, C, S, G, stmt);
    436451            }
    437452        } else if (LLVM_UNLIKELY(isa<While>(stmt))) {
     
    447462                remove_edge(v, u, G);
    448463                add_edge(var, u, v, G);
    449                 resolveNestedUsages(block, var, v, C, S, G, stmt);
    450             }
    451         } else {           
    452             resolveNestedUsages(block, stmt, u, C, S, G, stmt);
    453         }
    454     }
    455 
    456     if (redistributeGraph(C, S, G)) {
     464                resolveNestedUsages(var, v, C, S, G, stmt);
     465            }
     466        } else {
     467            resolveNestedUsages(stmt, u, C, S, G, stmt);
     468        }
     469    }
     470
     471//    printGraph(G, "G");
     472
     473    VertexMap M;
     474    if (redistributeGraph(C, M, G)) {
    457475        factorGraph(G);
    458         rewriteAST(block, G);
     476
     477//        printGraph(G, "H");
     478
     479        rewriteAST(C, M, G);
    459480        mModified = true;
    460481    }
     
    465486 * @brief resolveNestedUsages
    466487 ** ------------------------------------------------------------------------------------------------------------- */
    467 void BooleanReassociationPass::resolveNestedUsages(PabloBlock * const block, PabloAST * const expr, const Vertex u,
     488void BooleanReassociationPass::resolveNestedUsages(PabloAST * const expr, const Vertex u,
    468489                                                   CharacterizationMap & C, StatementMap & S, Graph & G,
    469490                                                   const Statement * const ignoreIfThis) const {
     
    472493        if (LLVM_LIKELY(user != expr && isa<Statement>(user))) {
    473494            PabloBlock * parent = cast<Statement>(user)->getParent(); assert (parent);
    474             if (LLVM_UNLIKELY(parent != block)) {
     495            if (LLVM_UNLIKELY(parent != mBlock)) {
    475496                for (;;) {
    476                     if (parent->getParent() == block) {
     497                    if (parent->getParent() == mBlock) {
    477498                        Statement * const branch = parent->getBranch();
    478499                        if (LLVM_UNLIKELY(branch != ignoreIfThis)) {
     
    757778 * Apply the distribution law to reduce computations whenever possible.
    758779 ** ------------------------------------------------------------------------------------------------------------- */
    759 bool BooleanReassociationPass::redistributeGraph(CharacterizationMap & C, StatementMap & M, Graph & G) const {
     780bool BooleanReassociationPass::redistributeGraph(CharacterizationMap & C, VertexMap & M, Graph & G) const {
    760781
    761782    bool modified = false;
     
    763784    DistributionGraph H;
    764785
    765     contractGraph(M, G);
     786    contractGraph(G);
    766787
    767788    for (;;) {
     
    829850            H.clear();
    830851
    831             contractGraph(M, G);
     852            contractGraph(G);
    832853        }
    833854
    834855        // Although exceptionally unlikely, it's possible that if we can reduce the graph, we could
    835856        // further simplify it. Restart the process if and only if we succeed.
    836         if (LLVM_UNLIKELY(reduceGraph(C, M, G))) {
    837             if (LLVM_UNLIKELY(contractGraph(M, G))) {
     857        if (reduceGraph(C, M, G)) {
     858            if (LLVM_UNLIKELY(contractGraph(G))) {
    838859                H.clear();
    839860                continue;
     
    865886
    866887/** ------------------------------------------------------------------------------------------------------------- *
     888 * @brief unique_source
     889 ** ------------------------------------------------------------------------------------------------------------- */
     890inline bool has_unique_source(const Vertex u, const Graph & G) {
     891    if (in_degree(u, G) > 0) {
     892        graph_traits<Graph>::in_edge_iterator i, end;
     893        std::tie(i, end) = in_edges(u, G);
     894        const Vertex v = source(*i, G);
     895        while (++i != end) {
     896            if (source(*i, G) != v) {
     897                return false;
     898            }
     899        }
     900        return true;
     901    }
     902    return false;
     903}
     904
     905/** ------------------------------------------------------------------------------------------------------------- *
     906 * @brief unique_target
     907 ** ------------------------------------------------------------------------------------------------------------- */
     908inline bool has_unique_target(const Vertex u, const Graph & G) {
     909    if (out_degree(u, G) > 0) {
     910        graph_traits<Graph>::out_edge_iterator i, end;
     911        std::tie(i, end) = out_edges(u, G);
     912        const Vertex v = target(*i, G);
     913        while (++i != end) {
     914            if (target(*i, G) != v) {
     915                return false;
     916            }
     917        }
     918        return true;
     919    }
     920    return false;
     921}
     922
     923
     924/** ------------------------------------------------------------------------------------------------------------- *
    867925 * @brief contractGraph
    868926 ** ------------------------------------------------------------------------------------------------------------- */
    869 bool BooleanReassociationPass::contractGraph(StatementMap & M, Graph & G) const {
     927bool BooleanReassociationPass::contractGraph(Graph & G) const {
    870928
    871929    bool contracted = false;
     
    881939        } else if (LLVM_LIKELY(out_degree(u, G) > 0)) {
    882940            if (isAssociative(G[u])) {
    883                 if (LLVM_UNLIKELY(in_degree(u, G) == 1)) {
     941                if (LLVM_UNLIKELY(has_unique_source(u, G))) {
    884942                    // We have a redundant node here that'll simply end up being a duplicate
    885943                    // of the input value. Remove it and add any of its outgoing edges to its
     
    888946                    const Vertex v = source(ei, G);
    889947                    for (auto ej : make_iterator_range(out_edges(u, G))) {
    890                         const Vertex w = target(ej, G);
    891                         add_edge(G[ei], v, w, G);
    892                     }
    893                     removeVertex(u, M, G);
     948                        add_edge(G[ej], v, target(ej, G), G);
     949                    }
     950//                    if (LLVM_UNLIKELY(getValue(G[v]) == nullptr && getValue(G[u]) != nullptr)) {
     951//                        getValue(G[v]) = getValue(G[u]);
     952//                    }
     953                    removeVertex(u, G);
    894954                    contracted = true;
    895                 } else if (LLVM_UNLIKELY(out_degree(u, G) == 1)) {
     955                } else if (LLVM_UNLIKELY(has_unique_target(u, G))) {
    896956                    // Otherwise if we have a single user, we have a similar case as above but
    897957                    // we can only merge this vertex into the outgoing instruction if they are
     
    901961                    if (LLVM_UNLIKELY(getType(G[v]) == getType(G[u]))) {
    902962                        for (auto ej : make_iterator_range(in_edges(u, G))) {
    903                             add_edge(G[ei], source(ej, G), v, G);
     963                            add_edge(G[ej], source(ej, G), v, G);
    904964                        }
    905                         removeVertex(u, M, G);
     965                        if (LLVM_UNLIKELY(getValue(G[v]) == nullptr && getValue(G[u]) != nullptr)) {
     966                            getValue(G[v]) = getValue(G[u]);
     967                        }
     968                        removeVertex(u, G);
    906969                        contracted = true;
    907                     }                   
     970                    }
    908971                }
    909972            }
    910973        } else if (LLVM_UNLIKELY(isNonEscaping(G[u]))) {
    911             removeVertex(u, M, G);
     974            removeVertex(u, G);
    912975            contracted = true;
    913976        }
     
    933996 * @brief reduceGraph
    934997 ** ------------------------------------------------------------------------------------------------------------- */
    935 bool BooleanReassociationPass::reduceGraph(CharacterizationMap & C, StatementMap & S, Graph & G) const {
     998bool BooleanReassociationPass::reduceVertex(const Vertex u, CharacterizationMap & C, VertexMap & M, Graph & G, const bool use_expensive_simplification) const {
    936999
    9371000    bool reduced = false;
    9381001
    939     VertexMap M;
     1002    assert (isReducible(G[u]));
     1003
     1004    Z3_ast node = getDefinition(G[u]);
     1005    if (isAssociative(G[u])) {
     1006        const TypeId typeId = getType(G[u]);
     1007        if (node == nullptr) {
     1008            const auto n = in_degree(u, G); assert (n > 1);
     1009            Z3_ast operands[n];
     1010            unsigned i = 0;
     1011            for (auto e : make_iterator_range(in_edges(u, G))) {
     1012                const Vertex v = source(e, G);
     1013                assert (getDefinition(G[v]));
     1014                operands[i++] = getDefinition(G[v]);
     1015            }
     1016            switch (typeId) {
     1017                case TypeId::And:
     1018                    node = Z3_mk_and(mContext, n, operands);
     1019                    break;
     1020                case TypeId::Or:
     1021                    node = Z3_mk_or(mContext, n, operands);
     1022                    break;
     1023                case TypeId::Xor:
     1024                    node = Z3_mk_xor(mContext, operands[0], operands[1]);
     1025                    for (unsigned i = 2; LLVM_UNLIKELY(i < n); ++i) {
     1026                        node = Z3_mk_xor(mContext, node, operands[i]);
     1027                    }
     1028                    break;
     1029                default: llvm_unreachable("unexpected type id");
     1030            }
     1031            assert (node);
     1032            getDefinition(G[u]) = node;
     1033        }
     1034
     1035        graph_traits<Graph>::in_edge_iterator begin, end;
     1036restart:if (in_degree(u, G) > 1) {
     1037            std::tie(begin, end) = in_edges(u, G);
     1038            for (auto i = begin; ++i != end; ) {
     1039                const auto v = source(*i, G);
     1040                for (auto j = begin; j != i; ++j) {
     1041                    const auto w = source(*j, G);
     1042                    Z3_ast operands[2] = { getDefinition(G[v]), getDefinition(G[w]) };
     1043                    Z3_ast test = nullptr;
     1044                    switch (typeId) {
     1045                        case TypeId::And:
     1046                            test = Z3_mk_and(mContext, 2, operands); break;
     1047                        case TypeId::Or:
     1048                            test = Z3_mk_or(mContext, 2, operands); break;
     1049                        case TypeId::Xor:
     1050                            test = Z3_mk_xor(mContext, operands[0], operands[1]); break;
     1051                        default:
     1052                            llvm_unreachable("impossible type id");
     1053                    }
     1054                    assert (test);
     1055                    test = simplify(test, use_expensive_simplification);
     1056
     1057                    bool replacement = false;
     1058                    Vertex x = 0;
     1059                    const auto f = M.find(test);
     1060                    if (LLVM_UNLIKELY(f != M.end())) {
     1061                        x = f->second;
     1062                        assert (getDefinition(G[x]) == test);
     1063                        replacement = true;
     1064                    } else {
     1065                        PabloAST * const factor = C.findKey(test);
     1066                        if (LLVM_UNLIKELY(!inCurrentBlock(factor, mBlock))) {
     1067                            x = makeVertex(TypeId::Var, factor, G, test);
     1068                            M.emplace(test, x);
     1069                            replacement = true;
     1070                        }
     1071                    }
     1072
     1073                    if (LLVM_UNLIKELY(replacement)) {
     1074
     1075                        // note: unless both edges carry an Pablo AST replacement value, they will converge into a single edge.
     1076                        PabloAST * const r1 = G[*i];
     1077                        PabloAST * const r2 = G[*j];
     1078
     1079                        remove_edge(*i, G);
     1080                        remove_edge(*j, G);
     1081
     1082                        if (LLVM_UNLIKELY(r1 && r2)) {
     1083                            add_edge(r1, x, u, G);
     1084                            add_edge(r2, x, u, G);
     1085                        } else {
     1086                            add_edge(r1 ? r1 : r2, x, u, G);
     1087                        }
     1088
     1089                        reduced = true;
     1090                        goto restart;
     1091                    }
     1092                }
     1093            }
     1094        }
     1095    }
     1096
     1097    if (LLVM_UNLIKELY(node == nullptr)) {
     1098        throw std::runtime_error("No Z3 characterization for vertex " + std::to_string(u));
     1099    }
     1100
     1101    auto f = M.find(node);
     1102    if (LLVM_LIKELY(f == M.end())) {
     1103        M.emplace(node, u);
     1104    } else if (isAssociative(G[u])) {
     1105        const Vertex v = f->second;
     1106        for (auto e : make_iterator_range(out_edges(u, G))) {
     1107            add_edge(G[e], v, target(e, G), G);
     1108        }
     1109        removeVertex(u, G);
     1110        reduced = true;
     1111    }
     1112
     1113    return reduced;
     1114}
     1115
     1116/** ------------------------------------------------------------------------------------------------------------- *
     1117 * @brief reduceGraph
     1118 ** ------------------------------------------------------------------------------------------------------------- */
     1119bool BooleanReassociationPass::reduceGraph(CharacterizationMap & C, VertexMap & M, Graph & G) const {
     1120
     1121    bool reduced = false;
     1122
    9401123    circular_buffer<Vertex> ordering(num_vertices(G));
    9411124
    9421125    topological_sort(G, std::front_inserter(ordering)); // topological ordering
     1126
     1127    M.clear();
    9431128
    9441129    // first contract the graph
    9451130    for (const Vertex u : ordering) {
    9461131        if (isReducible(G[u])) {
    947             Z3_ast & node = getDefinition(G[u]);
    948             if (isAssociative(G[u])) {
    949                 const TypeId typeId = getType(G[u]);
    950                 if (node == nullptr) {
    951                     const auto n = in_degree(u, G); assert (n > 1);
    952                     Z3_ast operands[n];
    953                     unsigned i = 0;
    954                     for (auto e : make_iterator_range(in_edges(u, G))) {
    955                         const Vertex v = source(e, G);
    956                         assert (getDefinition(G[v]));
    957                         operands[i++] = getDefinition(G[v]);
    958                     }
    959                     switch (typeId) {
    960                         case TypeId::And:
    961                             node = Z3_mk_and(mContext, n, operands);
    962                             break;
    963                         case TypeId::Or:
    964                             node = Z3_mk_or(mContext, n, operands);
    965                             break;
    966                         case TypeId::Xor:
    967                             node = Z3_mk_xor(mContext, operands[0], operands[1]);
    968                             for (unsigned i = 2; LLVM_UNLIKELY(i < n); ++i) {
    969                                 node = Z3_mk_xor(mContext, node, operands[i]);
    970                             }
    971                             break;
    972                         default: llvm_unreachable("unexpected type id");
    973                     }
    974 
    975                     assert (node);
    976                     node = Z3_simplify(mContext, node);
    977                 }
    978                 graph_traits<Graph>::in_edge_iterator begin, end;
    979 restart:        if (in_degree(u, G) > 1) {
    980                     std::tie(begin, end) = in_edges(u, G);
    981                     for (auto i = begin; ++i != end; ) {
    982                         const auto v = source(*i, G);
    983                         for (auto j = begin; j != i; ++j) {
    984                             const auto w = source(*j, G);
    985                             Z3_ast operands[2] = { getDefinition(G[v]), getDefinition(G[w]) };
    986                             assert (operands[0]);
    987                             assert (operands[1]);
    988                             Z3_ast test = nullptr;
    989                             switch (typeId) {
    990                                 case TypeId::And:
    991                                     test = Z3_mk_and(mContext, 2, operands); break;
    992                                 case TypeId::Or:
    993                                     test = Z3_mk_or(mContext, 2, operands); break;
    994                                 case TypeId::Xor:
    995                                     test = Z3_mk_xor(mContext, operands[0], operands[1]); break;
    996                                 default:
    997                                     llvm_unreachable("impossible type id");
    998                             }
    999                             assert (test);
    1000                             test = Z3_simplify(mContext, test);
    1001                             PabloAST * const factor = C.findKey(test);
    1002                             if (LLVM_UNLIKELY(factor != nullptr)) {
    1003                                 const Vertex a = makeVertex(TypeId::Var, factor, S, G, test);
    1004                                 // note: unless both edges carry an Pablo AST replacement value, they will converge into a single edge.
    1005                                 PabloAST * const r1 = G[*i];
    1006                                 PabloAST * const r2 = G[*j];
    1007 
    1008                                 remove_edge(*i, G);
    1009                                 remove_edge(*j, G);
    1010 
    1011                                 if (LLVM_UNLIKELY(r1 && r2)) {
    1012                                     add_edge(r1, a, u, G);
    1013                                     add_edge(r2, a, u, G);
    1014                                 } else {
    1015                                     add_edge(r1 ? r1 : r2, a, u, G);
    1016                                 }
    1017 
    1018 //                                errs() << " -- subsituting (" << a << ',' << u << ")=" << Z3_ast_to_string(mContext, test)
    1019 //                                       << " for (" << v << ',' << u << ")=" << Z3_ast_to_string(mContext, getDefinition(G[v]));
    1020 
    1021 //                                switch (typeId) {
    1022 //                                    case TypeId::And:
    1023 //                                        errs() << " ∧ "; break;
    1024 //                                    case TypeId::Or:
    1025 //                                        errs() << " √ ";  break;
    1026 //                                    case TypeId::Xor:
    1027 //                                        errs() << " ⊕ ";  break;
    1028 //                                    default:
    1029 //                                        llvm_unreachable("impossible type id");
    1030 //                                }
    1031 
    1032 //                                errs() << "(" << w << ',' << u << ")=" << Z3_ast_to_string(mContext, getDefinition(G[w]))
    1033 //                                       << "\n";
    1034 
    1035                                 reduced = true;
    1036                                 goto restart;
    1037                             }
    1038                         }
    1039                     }
    1040                 }
    1041             }
    1042 
    1043             if (LLVM_UNLIKELY(node == nullptr)) {
    1044                 throw std::runtime_error("No Z3 characterization for vertex " + std::to_string(u));
    1045             }
    1046 
    1047             auto f = M.find(node);
    1048             if (LLVM_LIKELY(f == M.end())) {
    1049                 M.emplace(node, u);
    1050             } else if (isAssociative(G[u])) {
    1051                 const Vertex v = f->second;
    1052 
    1053 //                errs() << " -- subsituting " << u << ":=\n" << Z3_ast_to_string(mContext, getDefinition(G[u]))
    1054 //                       << "\n for " << v << ":=\n" << Z3_ast_to_string(mContext, getDefinition(G[v])) << "\n";
    1055 
    1056                 for (auto e : make_iterator_range(out_edges(u, G))) {
    1057                     add_edge(G[e], v, target(e, G), G);
    1058                 }
    1059                 removeVertex(u, S, G);
     1132            if (reduceVertex(u, C, M, G, false)) {
    10601133                reduced = true;
    10611134            }
     
    10781151    bool modified = false;
    10791152
    1080     for (auto i = factors.begin(); ++i != factors.end(); ) {
    1081         assert (getType(G[*i]) == typeId);
    1082         for (auto ei : make_iterator_range(in_edges(*i, G))) {
     1153    for (unsigned i = 1; i < factors.size(); ++i) {
     1154        assert (getType(G[factors[i]]) == typeId);
     1155        for (auto ei : make_iterator_range(in_edges(factors[i], G))) {
    10831156            I.push_back(source(ei, G));
    10841157        }
    10851158        std::sort(I.begin(), I.end());
    1086         for (auto j = factors.begin(); j != i; ++j) {
    1087             for (auto ej : make_iterator_range(in_edges(*j, G))) {
     1159        for (unsigned j = 0; j < i; ++j) {
     1160            for (auto ej : make_iterator_range(in_edges(factors[j], G))) {
    10881161                J.push_back(source(ej, G));
    10891162            }
     
    10951168            const auto n = K.size();
    10961169            if (n > 1) {
    1097                 Vertex a = *i;
    1098                 Vertex b = *j;
     1170                Vertex a = factors[i];
     1171                Vertex b = factors[j];
    10991172                if (LLVM_UNLIKELY(in_degree(a, G) == n || in_degree(b, G) == n)) {
    11001173                    if (in_degree(a, G) != n) {
     
    11651238 * @brief rewriteAST
    11661239 ** ------------------------------------------------------------------------------------------------------------- */
    1167 void BooleanReassociationPass::rewriteAST(PabloBlock * const block, Graph & G) {
     1240bool BooleanReassociationPass::rewriteAST(CharacterizationMap & C, VertexMap & M, Graph & G) {
    11681241
    11691242    using line_t = long long int;
     
    11721245
    11731246    Z3_config cfg = Z3_mk_config();
    1174     Z3_set_param_value(cfg, "MODEL", "true");
     1247    Z3_set_param_value(cfg, "model", "true");
    11751248    Z3_context ctx = Z3_mk_context(cfg);
    11761249    Z3_del_config(cfg);
     
    11801253    std::vector<Z3_ast> mapping(num_vertices(G), nullptr);
    11811254
    1182     flat_map<PabloAST *, Z3_ast> M;
     1255    flat_map<PabloAST *, Z3_ast> V;
    11831256
    11841257    // Generate the variables
     
    11891262        const auto var = Z3_mk_fresh_const(ctx, nullptr, ty);
    11901263        Z3_ast constraint = nullptr;
    1191         if (in_degree(u, G) == 0) {
    1192             constraint = Z3_mk_eq(ctx, var, ZERO);
    1193         } else {
     1264        if (in_degree(u, G) > 0) {
    11941265            constraint = Z3_mk_gt(ctx, var, ZERO);
    1195         }
    1196         Z3_solver_assert(ctx, solver, constraint);
    1197 
     1266            Z3_solver_assert(ctx, solver, constraint);
     1267        }       
    11981268        PabloAST * const expr = getValue(G[u]);
    1199         if (expr) {
    1200             const bool added = M.emplace(expr, var).second;
    1201             assert ("G contains duplicate vertices for the same statement!" && added);
     1269        if (inCurrentBlock(expr, mBlock)) {
     1270            V.emplace(expr, var);
    12021271        }
    12031272        mapping[u] = var;
     
    12151284    // Compute the soft ordering constraints
    12161285    std::vector<Z3_ast> ordering(0);
    1217     ordering.reserve(2 * M.size() - 1);
     1286    ordering.reserve(V.size() - 1);
    12181287
    12191288    Z3_ast prior = nullptr;
    12201289    unsigned gap = 1;
    1221     for (Statement * stmt : *block) {
    1222         auto f = M.find(stmt);
    1223         if (f != M.end()) {
     1290    for (Statement * stmt : *mBlock) {
     1291        auto f = V.find(stmt);
     1292        if (f != V.end()) {
    12241293            Z3_ast const node = f->second;
    12251294            if (prior) {
    1226                 ordering.push_back(Z3_mk_lt(ctx, prior, node));
     1295//                ordering.push_back(Z3_mk_lt(ctx, prior, node)); // increases the cost by 6 - 10x
    12271296                Z3_ast ops[2] = { node, prior };
    12281297                ordering.push_back(Z3_mk_le(ctx, Z3_mk_sub(ctx, 2, ops), Z3_mk_int(ctx, gap, ty)));
    12291298            } else {
    12301299                ordering.push_back(Z3_mk_eq(ctx, node, Z3_mk_int(ctx, gap, ty)));
    1231 
    12321300            }
    12331301            prior = node;
     
    12701338    std::sort(S.begin(), S.end(), [&L](const Vertex u, const Vertex v){ return L[u] < L[v]; });
    12711339
    1272     block->setInsertPoint(nullptr);
     1340    mBlock->setInsertPoint(nullptr);
    12731341
    12741342    std::vector<Vertex> T;
     
    12881356            }
    12891357
    1290             Statement * ip = block->getInsertPoint();
    1291             ip = ip ? ip->getNextNode() : block->front();
     1358            Statement * ip = mBlock->getInsertPoint();
     1359            ip = ip ? ip->getNextNode() : mBlock->front();
    12921360
    12931361            const auto typeId = getType(G[u]);
    12941362
    1295             T.reserve(in_degree(u, G));
    1296             for (const auto e : make_iterator_range(in_edges(u, G))) {
    1297                 T.push_back(source(e, G));
    1298             }
    1299 
    1300             // Then sort them by their line position (noting any incoming value will either be 0 or MAX_INT)
    1301             std::sort(T.begin(), T.end(), [&L](const Vertex u, const Vertex v){ return L[u] < L[v]; });
    1302             if (LoadEarly) {
    1303                 block->setInsertPoint(nullptr);
    1304             }
    1305 
    1306             circular_buffer<PabloAST *> Q(2); // in_degree(u, G));
    1307             for (auto u : T) {
    1308                 PabloAST * expr = getValue(G[u]);
    1309                 if (LLVM_UNLIKELY(expr == nullptr)) {
    1310                     throw std::runtime_error("Vertex " + std::to_string(u) + " does not have an expression!");
    1311                 }
    1312                 Q.push_back(expr);
    1313                 if (Q.size() > 1) {
    1314 
    1315                     PabloAST * e1 = Q.front(); Q.pop_front();
    1316                     PabloAST * e2 = Q.front(); Q.pop_front();
    1317 
    1318                     if (in_degree(u, G) > 0) {
    1319                         if (LLVM_UNLIKELY(!dominates(e1, e2))) {
    1320                             std::string tmp;
    1321                             raw_string_ostream out(tmp);
    1322                             out << "e1: ";
    1323                             PabloPrinter::print(e1, out);
    1324                             out << " does not dominate e2: ";
    1325                             PabloPrinter::print(e2, out);
    1326                             throw std::runtime_error(out.str());
     1363            PabloAST * expr = nullptr;
     1364
     1365            for (;;) {
     1366
     1367                T.reserve(in_degree(u, G));
     1368                for (const auto e : make_iterator_range(in_edges(u, G))) {
     1369                    T.push_back(source(e, G));
     1370                }
     1371
     1372                // Then sort them by their line position (noting any incoming value will either be 0 or MAX_INT)
     1373                std::sort(T.begin(), T.end(), [&L](const Vertex u, const Vertex v){ return L[u] < L[v]; });
     1374
     1375                if (LoadEarly) {
     1376                    mBlock->setInsertPoint(nullptr);
     1377                }
     1378
     1379                bool done = true;
     1380
     1381                PabloAST * join = nullptr;
     1382
     1383                for (auto v : T) {
     1384                    expr = getValue(G[v]);
     1385                    if (LLVM_UNLIKELY(expr == nullptr)) {
     1386                        throw std::runtime_error("Vertex " + std::to_string(v) + " does not have an expression!");
     1387                    }
     1388                    if (join) {
     1389
     1390                        if (in_degree(v, G) > 0) {
     1391
     1392                            assert (L[v] > 0 && L[v] < MAX_INT);
     1393
     1394                            Statement * dom = cast<Statement>(expr);
     1395                            for (;;) {
     1396                                PabloBlock * const parent = dom->getParent();
     1397                                if (parent == mBlock) {
     1398                                    break;
     1399                                }
     1400                                dom = parent->getBranch(); assert(dom);
     1401                            }
     1402                            mBlock->setInsertPoint(dom);
     1403
     1404                            assert (dominates(join, expr));
     1405                            assert (dominates(expr, ip));
     1406                            assert (dominates(dom, ip));
    13271407                        }
    1328                         assert (dominates(e1, e2));
    1329                         assert (dominates(e2, ip));
    1330                         Statement * dom = cast<Statement>(expr);
    1331                         for (;;) {
    1332                             PabloBlock * const parent = dom->getParent();
    1333                             if (parent == block) {
    1334                                 block->setInsertPoint(dom);
     1408
     1409                        Statement * const currIP = mBlock->getInsertPoint();
     1410
     1411                        switch (typeId) {
     1412                            case TypeId::And:
     1413                                expr = mBlock->createAnd(join, expr); break;
     1414                            case TypeId::Or:
     1415                                expr = mBlock->createOr(join, expr); break;
     1416                            case TypeId::Xor:
     1417                                expr = mBlock->createXor(join, expr); break;
     1418                            default:
     1419                                llvm_unreachable("Invalid TypeId!");
     1420                        }
     1421
     1422                        // If the insertion point hasn't "moved" then we didn't make a new statement
     1423                        // and thus must have unexpectidly reused a prior statement (or Var.)
     1424                        if (LLVM_UNLIKELY(currIP == mBlock->getInsertPoint())) {
     1425                            if (LLVM_LIKELY(reduceVertex(u, C, M, G, true))) {
     1426                                done = false;
    13351427                                break;
    13361428                            }
    1337                             dom = parent->getBranch(); assert(dom);
     1429                            throw std::runtime_error("Unable to reduce vertex " + std::to_string(u));
    13381430                        }
    1339                         assert (dominates(dom, ip));
    1340                     }
    1341 
    1342                     switch (typeId) {
    1343                         case TypeId::And:
    1344                             expr = block->createAnd(e1, e2); break;
    1345                         case TypeId::Or:
    1346                             expr = block->createOr(e1, e2); break;
    1347                         case TypeId::Xor:
    1348                             expr = block->createXor(e1, e2); break;
    1349                         default: break;
    1350                     }
    1351                     Q.push_front(expr);
    1352                 }
    1353             }
    1354 
    1355             assert (Q.size() == 1);
    1356 
    1357             T.clear();
    1358 
    1359             block->setInsertPoint(ip->getPrevNode());
    1360 
    1361             PabloAST * const replacement = Q.front(); assert (replacement);
     1431                    }
     1432                    join = expr;
     1433                }
     1434
     1435                T.clear();
     1436
     1437                if (done) {
     1438                    break;
     1439                }
     1440            }
     1441
     1442
     1443            PabloAST * const replacement = expr; assert (replacement);
     1444
     1445            mBlock->setInsertPoint(ip->getPrevNode());
     1446
    13621447            for (auto e : make_iterator_range(out_edges(u, G))) {
    13631448                if (G[e]) {
     
    13721457
    13731458        assert (stmt);
    1374         assert (inCurrentBlock(stmt, block));
    13751459
    13761460        if (LLVM_UNLIKELY(isa<If>(stmt) || isa<While>(stmt))) {
     
    13821466        }
    13831467
    1384         block->insert(cast<Statement>(stmt));
     1468        mBlock->insert(cast<Statement>(stmt));
    13851469        L[u] = count++; // update the line count with the actual one.
    13861470    }
     
    13891473    Z3_del_context(ctx);
    13901474
    1391     Statement * const end = block->getInsertPoint(); assert (end);
     1475    Statement * const end = mBlock->getInsertPoint(); assert (end);
    13921476    for (;;) {
    13931477        Statement * const next = end->getNextNode();
     
    13951479            break;
    13961480        }
     1481
     1482        #ifndef NDEBUG
     1483        for (PabloAST * user : next->users()) {
     1484            if (isa<Statement>(user) && dominates(user, next)) {
     1485                std::string tmp;
     1486                raw_string_ostream out(tmp);
     1487                out << "Erasing ";
     1488                PabloPrinter::print(next, out);
     1489                out << " erroneously modifies live statement ";
     1490                PabloPrinter::print(cast<Statement>(user), out);
     1491                throw std::runtime_error(out.str());
     1492            }
     1493        }
     1494        #endif
    13971495        next->eraseFromParent(true);
    13981496    }
    13991497
    14001498    #ifndef NDEBUG
    1401     PabloVerifier::verify(mFunction, "post-reassociation");
     1499    PabloVerifier::verify(mFunction, "mid-reassociation");
    14021500    #endif
    14031501
     1502    return true;
    14041503}
    14051504
     
    14821581
    14831582/** ------------------------------------------------------------------------------------------------------------- *
     1583 * @brief simplify
     1584 ** ------------------------------------------------------------------------------------------------------------- */
     1585Z3_ast BooleanReassociationPass::simplify(Z3_ast node, bool use_expensive_minimization) const {
     1586
     1587    assert (node);
     1588
     1589    node = Z3_simplify_ex(mContext, node, mParams);
     1590
     1591    if (use_expensive_minimization) {
     1592
     1593        Z3_goal g = Z3_mk_goal(mContext, true, false, false);
     1594        Z3_goal_inc_ref(mContext, g);
     1595
     1596        Z3_goal_assert(mContext, g, node);
     1597
     1598        Z3_apply_result r = Z3_tactic_apply(mContext, mTactic, g);
     1599        Z3_apply_result_inc_ref(mContext, r);
     1600
     1601        assert (Z3_apply_result_get_num_subgoals(mContext, r) == 1);
     1602
     1603        Z3_goal h = Z3_apply_result_get_subgoal(mContext, r, 0);
     1604        Z3_goal_inc_ref(mContext, h);
     1605
     1606        const unsigned n = Z3_goal_size(mContext, h);
     1607
     1608        if (n == 1) {
     1609            node = Z3_goal_formula(mContext, h, 0);
     1610        } else if (n > 1) {
     1611            Z3_ast operands[n];
     1612            for (unsigned i = 0; i < n; ++i) {
     1613                operands[i] = Z3_goal_formula(mContext, h, i);
     1614            }
     1615            node = Z3_mk_and(mContext, n, operands);
     1616        }
     1617        Z3_goal_dec_ref(mContext, h);
     1618    }
     1619    return node;
     1620}
     1621
     1622/** ------------------------------------------------------------------------------------------------------------- *
    14841623 * @brief add
    14851624 ** ------------------------------------------------------------------------------------------------------------- */
     
    15261665 * @brief constructor
    15271666 ** ------------------------------------------------------------------------------------------------------------- */
    1528 inline BooleanReassociationPass::BooleanReassociationPass(Z3_context ctx, Z3_solver solver, PabloFunction & f)
     1667inline BooleanReassociationPass::BooleanReassociationPass(Z3_context ctx, Z3_params params, Z3_tactic tactic, PabloFunction & f)
    15291668: mContext(ctx)
    1530 , mSolver(solver)
     1669, mParams(params)
     1670, mTactic(tactic)
    15311671, mFunction(f)
    15321672, mModified(false) {
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/booleanreassociationpass.h

    r5152 r5156  
    3333        inline CharacterizationMap() : mPredecessor(nullptr) {}
    3434        inline CharacterizationMap(CharacterizationMap & predecessor) : mPredecessor(&predecessor) {}
     35        CharacterizationMap * predecessor() const { return mPredecessor; }
    3536    private:
    3637        CharacterizationMap * const     mPredecessor;
     
    4142protected:
    4243
    43     BooleanReassociationPass(Z3_context ctx, Z3_solver solver, PabloFunction & f);
     44    BooleanReassociationPass(Z3_context ctx, Z3_params params, Z3_tactic tactic, PabloFunction & f);
    4445    bool processScopes(PabloFunction & function);
    4546    void processScopes(PabloBlock * const block, CharacterizationMap & map);
    46     void distributeScope(PabloBlock * const block, CharacterizationMap & map);
     47    void distributeScope(PabloBlock * const block, CharacterizationMap & C);
    4748
    48     void transformAST(PabloBlock * const block, CharacterizationMap & C, Graph & G);
    49     void resolveNestedUsages(PabloBlock * const block, PabloAST * const expr, const Vertex u, CharacterizationMap &C, StatementMap & S, Graph & G, const Statement * const ignoreIfThis = nullptr) const;
     49    void transformAST(CharacterizationMap & C, Graph & G);
     50    void resolveNestedUsages(PabloAST * const expr, const Vertex u, CharacterizationMap &C, StatementMap & S, Graph & G, const Statement * const ignoreIfThis = nullptr) const;
    5051
    51     bool contractGraph(StatementMap & M, Graph & G) const;
     52    bool contractGraph(Graph & G) const;
    5253
    53     bool reduceGraph(CharacterizationMap & C, StatementMap & S, Graph & G) const;
     54    bool reduceVertex(const Vertex u, CharacterizationMap & C, VertexMap & M, Graph & G, const bool use_expensive_simplification) const;
     55    bool reduceGraph(CharacterizationMap & C, VertexMap & M, Graph & G) const;
    5456
    5557    bool factorGraph(const PabloAST::ClassTypeId typeId, Graph & G, std::vector<Vertex> & factors) const;
     
    6264    void removeVertex(const Vertex u, Graph & G) const;
    6365
    64     bool redistributeGraph(CharacterizationMap & C, StatementMap & M, Graph & G) const;
     66    bool redistributeGraph(CharacterizationMap & C, VertexMap & M, Graph & G) const;
    6567
    66     void rewriteAST(PabloBlock * const block, Graph & G);
     68    bool rewriteAST(CharacterizationMap & C, VertexMap &M, Graph & G);
    6769
    6870    Statement * characterize(Statement * const stmt, CharacterizationMap & map);
     71
     72    Z3_ast simplify(Z3_ast node, bool use_expensive_minimization = false) const;
    6973
    7074    Z3_ast makeVar() const;
    7175
    7276private:
     77    PabloBlock *                mBlock;
    7378    Z3_context const            mContext;
    74     Z3_solver const             mSolver;
     79    Z3_params const             mParams;
     80    Z3_tactic const             mTactic;
    7581    Z3_ast                      mInFile;
    7682    PabloFunction &             mFunction;
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_automultiplexing.cpp

    r5119 r5156  
    44#include <pablo/printer_pablos.h>
    55#include <boost/container/flat_set.hpp>
     6#include <boost/container/flat_map.hpp>
    67#include <boost/numeric/ublas/matrix.hpp>
    78#include <boost/circular_buffer.hpp>
     
    1617#include <functional>
    1718#include <llvm/Support/CommandLine.h>
     19#include "maxsat.hpp"
    1820
    1921using namespace llvm;
     
    2426static cl::OptionCategory MultiplexingOptions("Multiplexing Optimization Options", "These options control the Pablo Multiplexing optimization pass.");
    2527
    26 #ifdef NDEBUG
    27 #define INITIAL_SEED_VALUE (std::random_device()())
    28 #else
    29 #define INITIAL_SEED_VALUE (83234827342)
    30 #endif
    31 
    32 static cl::opt<std::mt19937::result_type> Seed("multiplexing-seed", cl::init(INITIAL_SEED_VALUE),
    33                                         cl::desc("randomization seed used when performing any non-deterministic operations."),
    34                                         cl::cat(MultiplexingOptions));
    35 
    36 #undef INITIAL_SEED_VALUE
    37 
    3828static cl::opt<unsigned> WindowSize("multiplexing-window-size", cl::init(100),
    3929                                        cl::desc("maximum sequence distance to consider for candidate set."),
     
    4333namespace pablo {
    4434
    45 Z3_bool maxsat(Z3_context ctx, Z3_solver solver, std::vector<Z3_ast> & soft);
    46 
    4735using TypeId = PabloAST::ClassTypeId;
    4836
     
    5341bool MultiplexingPass::optimize(PabloFunction & function) {
    5442
    55     PabloVerifier::verify(function, "pre-multiplexing");
    56 
    57     errs() << "PRE-MULTIPLEXING\n==============================================\n";
    58     PabloPrinter::print(function, errs());
    5943
    6044    Z3_config cfg = Z3_mk_config();
     
    6448    Z3_solver_inc_ref(ctx, solver);
    6549
    66     MultiplexingPass mp(function, Seed, ctx, solver);
     50    MultiplexingPass mp(function, ctx, solver);
    6751
    6852    mp.optimize();
     
    7155    Z3_del_context(ctx);
    7256
     57    #ifndef NDEBUG
    7358    PabloVerifier::verify(function, "post-multiplexing");
     59    #endif
    7460
    7561    Simplifier::optimize(function);
    76 
    77     errs() << "POST-MULTIPLEXING\n==============================================\n";
    78     PabloPrinter::print(function, errs());
    7962
    8063    return true;
     
    8770void MultiplexingPass::optimize() {
    8871    // Map the constants and input variables
    89 
    90     add(PabloBlock::createZeroes(), Z3_mk_false(mContext));
    91     add(PabloBlock::createOnes(), Z3_mk_true(mContext));
     72    add(PabloBlock::createZeroes(), Z3_mk_false(mContext), -1);
     73    add(PabloBlock::createOnes(), Z3_mk_true(mContext), -1);
    9274    for (unsigned i = 0; i < mFunction.getNumOfParameters(); ++i) {
    93         make(mFunction.getParameter(i));
    94     }
    95 
     75        add(mFunction.getParameter(i), makeVar(), -1);
     76    }
    9677    optimize(mFunction.getEntryBlock());
    9778}
     
    142123    if (generateCandidateSets(begin, end)) {
    143124        selectMultiplexSetsGreedy();
    144         eliminateSubsetConstraints();
     125        // eliminateSubsetConstraints();
    145126        multiplexSelectedSets(block, begin, end);
    146127    }
     
    152133inline bool MultiplexingPass::equals(Z3_ast a, Z3_ast b) {
    153134    Z3_solver_push(mContext, mSolver);
    154     Z3_ast test = Z3_mk_eq(mContext, a, b); // try using check assumption instead?
     135    Z3_ast test = Z3_mk_eq(mContext, a, b);
    155136    Z3_inc_ref(mContext, test);
    156137    Z3_solver_assert(mContext, mSolver, test);
     
    164145 * @brief handle_unexpected_statement
    165146 ** ------------------------------------------------------------------------------------------------------------- */
    166 static void handle_unexpected_statement(Statement * const stmt) {
     147static void handle_unexpected_statement(const Statement * const stmt) {
    167148    std::string tmp;
    168149    raw_string_ostream err(tmp);
     
    175156 * @brief characterize
    176157 ** ------------------------------------------------------------------------------------------------------------- */
    177 inline Z3_ast MultiplexingPass::characterize(Statement * const stmt) {
     158Z3_ast MultiplexingPass::characterize(const Statement * const stmt, const bool deref) {
    178159
    179160    const size_t n = stmt->getNumOperands(); assert (n > 0);
    180     Z3_ast operands[n] = {};
     161    Z3_ast operands[n];
    181162    for (size_t i = 0; i < n; ++i) {
    182163        PabloAST * op = stmt->getOperand(i);
    183         if (LLVM_LIKELY(isa<Statement>(op) || isa<Var>(op))) {
    184             operands[i] = get(op, true);
    185         }
     164        if (LLVM_UNLIKELY(isa<Integer>(op) || isa<String>(op))) {
     165            continue;
     166        }
     167        operands[i] = get(op, deref);
    186168    }
    187169
     
    206188                node = temp;
    207189            }
    208             return add(stmt, node);
     190            return add(stmt, node, stmt->getNumUses());
    209191        case TypeId::Not:
    210192            node = Z3_mk_not(mContext, node);
     
    220202        case TypeId::MatchStar:
    221203        case TypeId::Count:
    222             return make(stmt);
     204            node = makeVar();
     205            break;
    223206        default:
    224207            handle_unexpected_statement(stmt);
    225208    }
    226209    Z3_inc_ref(mContext, node);
    227     return add(stmt, node);
     210    return add(stmt, node, stmt->getNumUses());
    228211}
    229212
     
    232215 * @brief characterize
    233216 ** ------------------------------------------------------------------------------------------------------------- */
    234 inline Z3_ast MultiplexingPass::characterize(Advance * const adv, Z3_ast Ik) {
     217inline Z3_ast MultiplexingPass::characterize(const Advance * const adv, Z3_ast Ik) {
    235218    const auto k = mNegatedAdvance.size();
    236219
    237220    assert (adv);
    238221    assert (mConstraintGraph[k] == adv);
    239 
    240     bool unconstrained[k] = {};
     222    std::vector<bool> unconstrained(k);
    241223
    242224    Z3_solver_push(mContext, mSolver);
     
    265247 and Aj ⊂ Ai, Aj ∩ Ak = âˆ
    266248.
    267                 for (auto e : make_iterator_range(in_edges(i, mSubsetGraph))) {
    268                     unconstrained[source(e, mSubsetGraph)] = true;
    269                 }
     249//                for (auto e : make_iterator_range(in_edges(i, mSubsetGraph))) {
     250//                    unconstrained[source(e, mSubsetGraph)] = true;
     251//                }
    270252                unconstrained[i] = true;
    271             } else if (equals(Ii, IiIk)) {
     253            }/* else if (equals(Ii, IiIk)) {
    272254                // If Ii = Ii ∩ Ik then Ii ⊆ Ik. Record this in the subset graph with the arc (i, k).
    273255                // Note: the AST will be modified to make these mutually exclusive if Ai and Ak end up in
     
    291273                }
    292274                unconstrained[i] = true;
    293             }
     275            }*/
    294276            Z3_dec_ref(mContext, IiIk);
    295277            Z3_solver_pop(mContext, mSolver, 1);
     
    299281    Z3_solver_pop(mContext, mSolver, 1);
    300282
    301     Z3_ast Ak0 = make(adv);
     283    Z3_ast Ak0 = makeVar();
    302284    Z3_inc_ref(mContext, Ak0);
    303285    Z3_ast Nk = Z3_mk_not(mContext, Ak0);
     
    331313            continue; // note: if these Advances are transitively dependent, an edge will still exist.
    332314        }
    333         add_edge(i, k, mConstraintGraph);
     315        const auto ei = add_edge(i, k, mConstraintGraph);
     316        // if this is not a new edge, it must have a dependency constraint.
     317        if (ei.second) {
     318            mConstraintGraph[ei.first] = ConstraintType::Inclusive;
     319        }
    334320    }
    335321    // To minimize the number of BDD computations, we store the negated variable instead of negating it each time.
     
    340326        Z3_dec_ref(mContext, Ak0);
    341327    }
    342     return add(adv, Ak);
     328    return add(adv, Ak, -1);
    343329}
    344330
     
    350336    // clean up any unneeded refs / characterizations.
    351337    for (auto i = mCharacterization.begin(); i != mCharacterization.end(); ) {
    352         const CharacterizationRef & r = std::get<1>(*i);
    353         const auto e = i++;
    354         if (LLVM_UNLIKELY(std::get<1>(r) == 0)) {
    355             Z3_dec_ref(mContext, std::get<0>(r));
    356             mCharacterization.erase(e);
    357         }
    358     }
    359 
     338        const auto ref = i->second;
     339        auto next = i; ++next;
     340        if (LLVM_UNLIKELY(ref.second == 0)) {
     341            assert (isa<Statement>(i->first));
     342            Z3_dec_ref(mContext, ref.first);
     343            mCharacterization.erase(i);
     344        }
     345        i = next;
     346    }
    360347    for (Z3_ast var : mNegatedAdvance) {
    361348        Z3_dec_ref(mContext, var);
     
    416403        for (unsigned j = 0; j < i; ++j) {
    417404            if (G(i, j)) {
    418                 add_edge(j, i, mConstraintGraph);
     405                mConstraintGraph[add_edge(j, i, mConstraintGraph).first] = ConstraintType::Dependency;
    419406            }
    420407        }
    421408        for (unsigned j = i + 1; j < advances; ++j) {
    422409            if (G(i, j)) {
    423                 add_edge(j, i, mConstraintGraph);
     410                mConstraintGraph[add_edge(j, i, mConstraintGraph).first] = ConstraintType::Dependency;
    424411            }
    425412        }
     
    431418    return last;
    432419}
    433 
    434420
    435421/** ------------------------------------------------------------------------------------------------------------- *
     
    443429    }
    444430    assert (num_vertices(mConstraintGraph) == n);
    445 
    446     // The naive way to handle this would be to compute a DNF formula consisting of the
    447     // powerset of all independent (candidate) sets of G, assign a weight to each, and
    448     // try to maximally satisfy the clauses. However, this would be extremely costly to
    449     // compute let alone solve as we could easily generate O(2^100) clauses for a complex
    450     // problem. Further the vast majority of clauses would be false in the end.
    451 
    452     // Moreover, for every set that can Advance is contained in would need a unique
    453     // variable and selector. In other words:
    454 
    455     // Suppose Advance A has a selector variable I. If I is true, then A must be in ONE set.
    456     // Assume A could be in m sets. To enforce this, there are m(m - 1)/2 clauses:
    457 
    458     //   (¬A_1 √ ¬A_2 √ ¬I), (¬A_1 √ ¬A_3 √ ¬I), ..., (¬A_m-1 √ ¬A_m √ ¬I)
    459 
    460     // m here is be equivalent to number of independent sets in the constraint graph G
    461     // that contains A.
    462 
    463     // If two sets have a DEPENDENCY constraint between them, it will introduce a cyclic
    464     // relationship even if those sets are legal on their own. Thus we'd also need need
    465     // hard constraints between all constrained variables related to the pair of Advances.
    466 
    467     // Instead, we only try to solve for one set at a time. This eliminate the need for
    468     // the above constraints and computing m but this process to be closer to a simple
    469     // greedy search.
    470 
    471     // We do want to weight whether to include or exclude an item in a set but what should
    472     // this be? The weight must be related to the elements already in the set. If our goal
    473     // is to balance the perturbation of the AST with the reduction in # of Advances, the
    474     // cost of inclusion / exclusion could be proportional to the # of instructions that
    475     // it increases / decreases the span by --- but how many statements is an Advance worth?
    476 
    477     // What if instead we maintain a queue of advances and discard any that are outside of
    478     // the current window?
    479431
    480432    mCandidateGraph = CandidateGraph(n);
     
    486438    Z3_solver solver = Z3_mk_solver(ctx);
    487439    Z3_solver_inc_ref(ctx, solver);
    488     std::vector<Z3_ast> N(n);
     440
     441    std::vector<Z3_ast> V(n);
    489442    for (unsigned i = 0; i < n; ++i) {
    490         N[i] = Z3_mk_fresh_const(ctx, nullptr, Z3_mk_bool_sort(ctx)); assert (N[i]);
     443        V[i] = Z3_mk_fresh_const(ctx, nullptr, Z3_mk_bool_sort(ctx)); assert (V[i]);
    491444    }
    492445    std::vector<std::pair<unsigned, unsigned>> S;
     
    502455                // try to compute a maximal set for this given set of Advances
    503456                if (S.size() > 2) {
    504                     generateCandidateSets(ctx, solver, S, N);
     457                    generateCandidateSets(ctx, solver, S, V);
    505458                }
    506459                // erase any that preceed our window
    507                 for (auto i = S.begin();;) {
    508                     if (++i == S.end() || (line - std::get<0>(*i)) <= WindowSize) {
    509                         S.erase(S.begin(), i);
    510                         break;
    511                     }
    512                 }
     460                auto end = S.begin();
     461                while (++end != S.end() && ((line - std::get<0>(*end)) > WindowSize));
     462                S.erase(S.begin(), end);
    513463            }
    514464            for (unsigned j : make_iterator_range(adjacent_vertices(i, mConstraintGraph))) {
    515                 Z3_ast disj[2] = { Z3_mk_not(ctx, N[j]), Z3_mk_not(ctx, N[i]) };
     465                Z3_ast disj[2] = { Z3_mk_not(ctx, V[j]), Z3_mk_not(ctx, V[i]) };
    516466                Z3_solver_assert(ctx, solver, Z3_mk_or(ctx, 2, disj));
    517467            }
     
    521471    }
    522472    if (S.size() > 2) {
    523         generateCandidateSets(ctx, solver, S, N);
     473        generateCandidateSets(ctx, solver, S, V);
    524474    }
    525475
     
    533483 * @brief generateCandidateSets
    534484 ** ------------------------------------------------------------------------------------------------------------- */
    535 void MultiplexingPass::generateCandidateSets(Z3_context ctx, Z3_solver solver, const std::vector<std::pair<unsigned, unsigned>> & S, const std::vector<Z3_ast> & N) {
     485void MultiplexingPass::generateCandidateSets(Z3_context ctx, Z3_solver solver, const std::vector<std::pair<unsigned, unsigned>> & S, const std::vector<Z3_ast> & V) {
    536486    assert (S.size() > 2);
    537487    assert (std::get<0>(S.front()) < std::get<0>(S.back()));
    538488    assert ((std::get<0>(S.back()) - std::get<0>(S.front())) <= WindowSize);
     489
    539490    Z3_solver_push(ctx, solver);
    540     const auto n = N.size();
    541     std::vector<Z3_ast> assumptions(S.size());
    542     for (unsigned i = 0, j = 0; i < n; ++i) {
    543         if (LLVM_UNLIKELY(j < S.size() && std::get<1>(S[j]) == i)) { // in our window range
    544             assumptions[j++] = N[i];
    545         } else {
    546             Z3_solver_assert(ctx, solver, Z3_mk_not(ctx, N[i]));
    547         }
    548     }
    549     if (maxsat(ctx, solver, assumptions) != Z3_L_FALSE) {
    550         Z3_model m = Z3_solver_get_model(ctx, solver);
    551         Z3_model_inc_ref(ctx, m);
    552         const auto k = add_vertex(mCandidateGraph); assert(k >= N.size());
    553         Z3_ast TRUE = Z3_mk_true(ctx);
    554         Z3_ast FALSE = Z3_mk_false(ctx);
    555         for (const auto i : S) {
    556             Z3_ast value;
    557             if (LLVM_UNLIKELY(Z3_model_eval(ctx, m, N[std::get<1>(i)], 1, &value) != Z3_TRUE)) {
    558                 throw std::runtime_error("Unexpected Z3 error when attempting to obtain value from constraint model!");
    559             }
    560             if (value == TRUE) {
    561                 add_edge(std::get<1>(i), k, mCandidateGraph);
    562             } else if (LLVM_UNLIKELY(value != FALSE)) {
    563                 throw std::runtime_error("Unexpected Z3 error constraint model value is a non-terminal!");
    564             }
    565         }
    566         Z3_model_dec_ref(ctx, m);
    567     }
     491
     492    const auto n = V.size();
     493    std::vector<unsigned> M(S.size());
     494    for (unsigned i = 0; i < S.size(); ++i) {
     495        M[i] = std::get<1>(S[i]);
     496    }
     497
     498    for (;;) {
     499
     500        std::vector<Z3_ast> assumptions(M.size());
     501        unsigned j = 0;
     502        for (unsigned i = 0; i < n; ++i) {
     503            if (LLVM_UNLIKELY((j < M.size()) && (M[j] == i))) { // in our window range
     504                assumptions[j++] = V[i]; assert (V[i]);
     505            } else {
     506                Z3_solver_assert(ctx, solver, Z3_mk_not(ctx, V[i]));
     507            }
     508        }
     509        assert (j == M.size());
     510
     511        if (maxsat(ctx, solver, assumptions) >= 0) {
     512            Z3_model m = Z3_solver_get_model(ctx, solver);
     513            Z3_model_inc_ref(ctx, m);
     514            const auto k = add_vertex(mCandidateGraph); assert(k >= V.size());
     515            Z3_ast TRUE = Z3_mk_true(ctx);
     516            for (auto i = M.begin(); i != M.end(); ) {
     517                Z3_ast value;
     518                if (LLVM_UNLIKELY(Z3_model_eval(ctx, m, V[*i], 1, &value) != Z3_TRUE)) {
     519                    throw std::runtime_error("Unexpected Z3 error when attempting to obtain value from constraint model!");
     520                }
     521                if (value == TRUE) {
     522                    add_edge(*i, k, mCandidateGraph);
     523                    Z3_solver_assert(ctx, solver, Z3_mk_not(ctx, V[*i]));
     524                    i = M.erase(i);
     525                } else {
     526                    ++i;
     527                }
     528            }
     529            Z3_model_dec_ref(ctx, m);
     530            if (M.size() > 2) {
     531                continue;
     532            }
     533        }
     534        break;
     535    }
     536
    568537    Z3_solver_pop(ctx, solver, 1);
    569538}
     
    602571    const size_t n = num_vertices(mCandidateGraph) - m;
    603572
    604     bool chosen[n] = {};
     573    std::vector<bool> chosen(n);
    605574
    606575    for (;;) {
     
    711680}
    712681
    713 ///** ------------------------------------------------------------------------------------------------------------- *
    714 // * Topologically sort the sequence of instructions whilst trying to adhere as best as possible to the original
    715 // * program sequence.
    716 // ** ------------------------------------------------------------------------------------------------------------- */
    717 //inline bool topologicalSort(Z3_context ctx, Z3_solver solver, const std::vector<Z3_ast> & nodes, const int limit) {
    718 //    const auto n = nodes.size();
    719 //    if (LLVM_UNLIKELY(n == 0)) {
    720 //        return true;
    721 //    }
    722 //    if (LLVM_UNLIKELY(Z3_solver_check(ctx, solver) == Z3_L_FALSE)) {
    723 //        return false;
    724 //    }
    725 
    726 //    Z3_ast aux_vars[n];
    727 //    Z3_ast assumptions[n];
    728 //    Z3_ast ordering[n];
    729 //    int increments[n];
    730 
    731 //    Z3_sort boolTy = Z3_mk_bool_sort(ctx);
    732 //    Z3_sort intTy = Z3_mk_int_sort(ctx);
    733 //    Z3_ast one = Z3_mk_int(ctx, 1, intTy);
    734 
    735 //    for (unsigned i = 0; i < n; ++i) {
    736 //        aux_vars[i] = Z3_mk_fresh_const(ctx, nullptr, boolTy);
    737 //        assumptions[i] = Z3_mk_not(ctx, aux_vars[i]);
    738 //        Z3_ast num = one;
    739 //        if (i > 0) {
    740 //            Z3_ast prior_plus_one[2] = { nodes[i - 1], one };
    741 //            num = Z3_mk_add(ctx, 2, prior_plus_one);
    742 //        }
    743 //        ordering[i] = Z3_mk_eq(ctx, nodes[i], num);
    744 //        increments[i] = 1;
    745 //    }
    746 
    747 //    unsigned unsat = 0;
    748 
    749 //    for (;;) {
    750 //        Z3_solver_push(ctx, solver);
    751 //        for (unsigned i = 0; i < n; ++i) {
    752 //            Z3_ast constraint[2] = {ordering[i], aux_vars[i]};
    753 //            Z3_solver_assert(ctx, solver, Z3_mk_or(ctx, 2, constraint));
    754 //        }
    755 //        if (LLVM_UNLIKELY(Z3_solver_check_assumptions(ctx, solver, n, assumptions) != Z3_L_FALSE)) {
    756 //            errs() << " SATISFIABLE!  (" << unsat << " of " << n << ")\n";
    757 //            return true; // done
    758 //        }
    759 //        Z3_ast_vector core = Z3_solver_get_unsat_core(ctx, solver); assert (core);
    760 //        unsigned m = Z3_ast_vector_size(ctx, core); assert (m > 0);
    761 
    762 //        errs() << " UNSATISFIABLE " << m << "  (" << unsat << " of " << n <<")\n";
    763 
    764 //        for (unsigned j = 0; j < m; j++) {
    765 //            // check whether assumption[i] is in the core or not
    766 //            bool not_found = true;
    767 //            for (unsigned i = 0; i < n; i++) {
    768 //                if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) {
    769 
    770 //                    const auto k = increments[i];
    771 
    772 //                    errs() << " -- " << i << " @k=" << k << "\n";
    773 
    774 //                    if (k < limit) {
    775 //                        Z3_ast gap = Z3_mk_int(ctx, 1UL << k, intTy);
    776 //                        Z3_ast num = gap;
    777 //                        if (LLVM_LIKELY(i > 0)) {
    778 //                            Z3_ast prior_plus_gap[2] = { nodes[i - 1], gap };
    779 //                            num = Z3_mk_add(ctx, 2, prior_plus_gap);
    780 //                        }
    781 //                        Z3_dec_ref(ctx, ordering[i]);
    782 //                        ordering[i] = Z3_mk_le(ctx, num, nodes[i]);
    783 //                    } else if (k == limit && i > 0) {
    784 //                        ordering[i] = Z3_mk_le(ctx, nodes[i - 1], nodes[i]);
    785 //                    } else {
    786 //                        assumptions[i] = aux_vars[i]; // <- trivially satisfiable
    787 //                        ++unsat;
    788 //                    }
    789 //                    increments[i] = k + 1;
    790 //                    not_found = false;
    791 //                    break;
    792 //                }
    793 //            }
    794 //            if (LLVM_UNLIKELY(not_found)) {
    795 //                throw std::runtime_error("Unexpected Z3 failure when attempting to locate unsatisfiable ordering constraint!");
    796 //            }
    797 //        }
    798 //        Z3_solver_pop(ctx, solver, 1);
    799 //    }
    800 //    llvm_unreachable("maxsat wrongly reported this being unsatisfiable despite being able to satisfy the hard constraints!");
    801 //    return false;
    802 //}
    803 
    804 ///** ------------------------------------------------------------------------------------------------------------- *
    805 // * Topologically sort the sequence of instructions whilst trying to adhere as best as possible to the original
    806 // * program sequence.
    807 // ** ------------------------------------------------------------------------------------------------------------- */
    808 //inline bool topologicalSort(Z3_context ctx, Z3_solver solver, const std::vector<Z3_ast> & nodes, const int limit) {
    809 //    const auto n = nodes.size();
    810 //    if (LLVM_UNLIKELY(n == 0)) {
    811 //        return true;
    812 //    }
    813 //    if (LLVM_UNLIKELY(Z3_solver_check(ctx, solver) == Z3_L_FALSE)) {
    814 //        return false;
    815 //    }
    816 
    817 //    Z3_ast aux_vars[n];
    818 //    Z3_ast assumptions[n];
    819 
    820 //    Z3_sort boolTy = Z3_mk_bool_sort(ctx);
    821 //    Z3_ast one = Z3_mk_int(ctx, 1, Z3_mk_int_sort(ctx));
    822 
    823 //    for (unsigned i = 0; i < n; ++i) {
    824 //        aux_vars[i] = Z3_mk_fresh_const(ctx, nullptr, boolTy);
    825 //        assumptions[i] = Z3_mk_not(ctx, aux_vars[i]);
    826 //        Z3_ast num = one;
    827 //        if (i > 0) {
    828 //            Z3_ast prior_plus_one[2] = { nodes[i - 1], one };
    829 //            num = Z3_mk_add(ctx, 2, prior_plus_one);
    830 //        }
    831 //        Z3_ast ordering = Z3_mk_eq(ctx, nodes[i], num);
    832 //        Z3_ast constraint[2] = {ordering, aux_vars[i]};
    833 //        Z3_solver_assert(ctx, solver, Z3_mk_or(ctx, 2, constraint));
    834 //    }
    835 
    836 //    for (unsigned k = 0; k < n; ) {
    837 //        if (LLVM_UNLIKELY(Z3_solver_check_assumptions(ctx, solver, n, assumptions) != Z3_L_FALSE)) {
    838 //            errs() << " SATISFIABLE!\n";
    839 //            return true; // done
    840 //        }
    841 //        Z3_ast_vector core = Z3_solver_get_unsat_core(ctx, solver); assert (core);
    842 //        unsigned m = Z3_ast_vector_size(ctx, core); assert (m > 0);
    843 
    844 //        k += m;
    845 
    846 //        errs() << " UNSATISFIABLE " << m << " (" << k << ")\n";
    847 
    848 //        for (unsigned j = 0; j < m; j++) {
    849 //            // check whether assumption[i] is in the core or not
    850 //            bool not_found = true;
    851 //            for (unsigned i = 0; i < n; i++) {
    852 //                if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) {
    853 //                    assumptions[i] = aux_vars[i];
    854 //                    not_found = false;
    855 //                    break;
    856 //                }
    857 //            }
    858 //            if (LLVM_UNLIKELY(not_found)) {
    859 //                throw std::runtime_error("Unexpected Z3 failure when attempting to locate unsatisfiable ordering constraint!");
    860 //            }
    861 //        }
    862 //    }
    863 //    llvm_unreachable("maxsat wrongly reported this being unsatisfiable despite being able to satisfy the hard constraints!");
    864 //    return false;
    865 //}
    866 
    867 
    868682/** ------------------------------------------------------------------------------------------------------------- *
    869683 * @brief addWithHardConstraints
     
    942756    assert (!end || isa<If>(end) || isa<While>(end));
    943757
     758    // TODO: should we test whether sets overlap and merge the computations together?
     759
    944760    Z3_config cfg = Z3_mk_config();
    945761    Z3_set_param_value(cfg, "MODEL", "true");
     
    959775            PabloAST * muxed[m];
    960776            PabloAST * muxed_n[m];
     777            PabloAST * demuxed[n];
    961778
    962779            // The multiplex set graph is a DAG with edges denoting the set relationships of our independent sets.
     
    966783                assert ("Not all inputs are in the same block!" && (input[i]->getParent() == block));
    967784                assert ("Not all inputs advance by the same amount!" && (input[i]->getOperand(1) == input[0]->getOperand(1)));
    968                 assert ("Inputs are not in sequential order!" && (i == 0 || (i > 0 && dominates(input[i - 1], input[i]))));
    969785                ++i;
    970786            }
    971787
    972             Statement * const A1 = input[0];
    973             Statement * const An = input[n - 1]->getNextNode();
    974 
    975             Statement * const ip = A1->getPrevNode(); // save our insertion point prior to modifying the AST
     788            // We can't trust the AST will be in the original order as we can multiplex a region of the program
     789            // more than once.
     790            Statement * initial = nullptr, * sentinal = nullptr;
     791            for (Statement * stmt : *block) {
     792                if (isa<Advance>(stmt)) {
     793                    for (unsigned i = 0; i < n; ++i) {
     794                        if (stmt == input[i]) {
     795                            initial = initial ? initial : stmt;
     796                            sentinal = stmt;
     797                            break;
     798                        }
     799                    }
     800                }
     801            }
     802            assert (initial);
     803
     804            Statement * const ip = initial->getPrevNode(); // save our insertion point prior to modifying the AST
     805            sentinal = sentinal->getNextNode();
    976806
    977807            Z3_solver_push(ctx, solver);
     
    983813            Z3_ast one = Z3_mk_int(ctx, 1, Z3_mk_int_sort(ctx));
    984814            std::vector<Z3_ast> ordering;
    985 //            std::vector<Z3_ast> nodes;
    986 
    987             for (Statement * stmt = A1; stmt != An; stmt = stmt->getNextNode()) { assert (stmt != ip);
     815
     816            for (Statement * stmt = initial; stmt != sentinal; stmt = stmt->getNextNode()) { assert (stmt != ip);
    988817                Z3_ast node = addWithHardConstraints(ctx, solver, block, stmt, M);
    989818                // compute the soft ordering constraints
     
    997826                    ordering.push_back(Z3_mk_lt(ctx, prior, node));
    998827                }
    999 
    1000 
    1001 //                for (Z3_ast prior : nodes) {
    1002 //                    Z3_solver_assert(ctx, solver, Z3_mk_not(ctx, Z3_mk_eq(ctx, prior, node)));
    1003 //                }
    1004  //               nodes.push_back(node);
    1005 
    1006 
    1007828                prior = node;
    1008829            }
    1009 
    1010             // assert (nodes.size() <= WindowSize);
    1011830
    1012831            block->setInsertPoint(block->back()); // <- necessary for domination check!
     
    1054873                }
    1055874                assert (replacement);
    1056                 PabloAST * const demuxed = Q.front(); Q.clear();
     875                demuxed[i] = Q.front(); Q.clear();
    1057876
    1058877                const auto f = M.find(input[i]);
     
    1060879                Z3_solver_assert(ctx, solver, Z3_mk_eq(ctx, f->second, replacement));
    1061880                M.erase(f);
    1062 
    1063                 input[i]->replaceWith(demuxed);
    1064                 assert (M.count(input[i]) == 0);
    1065881            }
    1066882
    1067883            assert (M.count(ip) == 0);
    1068884
    1069             if (LLVM_UNLIKELY(maxsat(ctx, solver, ordering) != Z3_L_TRUE)) {
    1070                 throw std::runtime_error("Unexpected Z3 failure when attempting to topologically sort the AST!");
    1071             }
    1072 
    1073             Z3_model model = Z3_solver_get_model(ctx, solver);
    1074             Z3_model_inc_ref(ctx, model);
    1075 
    1076             std::vector<std::pair<long long int, Statement *>> I;
    1077 
    1078             for (const auto i : M) {
    1079                 Z3_ast value;
    1080                 if (LLVM_UNLIKELY(Z3_model_eval(ctx, model, std::get<1>(i), Z3_L_TRUE, &value) != Z3_L_TRUE)) {
    1081                     throw std::runtime_error("Unexpected Z3 error when attempting to obtain value from model!");
    1082                 }
    1083                 long long int line;
    1084                 if (LLVM_UNLIKELY(Z3_get_numeral_int64(ctx, value, &line) != Z3_L_TRUE)) {
    1085                     throw std::runtime_error("Unexpected Z3 error when attempting to convert model value to integer!");
    1086                 }
    1087                 I.emplace_back(line, std::get<0>(i));
    1088             }
    1089 
    1090             Z3_model_dec_ref(ctx, model);
    1091 
    1092             std::sort(I.begin(), I.end());
    1093 
    1094             block->setInsertPoint(ip);
    1095             for (auto i : I) {
    1096                 block->insert(std::get<1>(i));
     885            const auto satisfied = maxsat(ctx, solver, ordering);
     886
     887            if (LLVM_UNLIKELY(satisfied >= 0)) {
     888
     889                Z3_model model = Z3_solver_get_model(ctx, solver);
     890                Z3_model_inc_ref(ctx, model);
     891
     892                std::vector<std::pair<long long int, Statement *>> I;
     893
     894                for (const auto i : M) {
     895                    Z3_ast value;
     896                    if (LLVM_UNLIKELY(Z3_model_eval(ctx, model, std::get<1>(i), Z3_L_TRUE, &value) != Z3_L_TRUE)) {
     897                        throw std::runtime_error("Unexpected Z3 error when attempting to obtain value from model!");
     898                    }
     899                    long long int line;
     900                    if (LLVM_UNLIKELY(Z3_get_numeral_int64(ctx, value, &line) != Z3_L_TRUE)) {
     901                        throw std::runtime_error("Unexpected Z3 error when attempting to convert model value to integer!");
     902                    }
     903                    I.emplace_back(line, std::get<0>(i));
     904                }
     905
     906                Z3_model_dec_ref(ctx, model);
     907
     908                std::sort(I.begin(), I.end());
     909
     910                block->setInsertPoint(ip);
     911                for (auto i : I) {
     912                    block->insert(std::get<1>(i));
     913                }
     914
     915                for (unsigned i = 0; i < n; ++i) {
     916                    input[i]->replaceWith(demuxed[i], true, true);
     917                    auto ref = mCharacterization.find(input[i]);
     918                    assert (ref != mCharacterization.end());
     919                    add(demuxed[i], std::get<0>(ref->second), -1);
     920                }
     921
     922            } else { // fatal error; delete any statements we created.
     923
     924                for (unsigned i = 0; i < n; ++i) {
     925                    if (LLVM_LIKELY(isa<Statement>(demuxed[i]))) {
     926                        cast<Statement>(demuxed[i])->eraseFromParent(true);
     927                    }
     928                }
     929
    1097930            }
    1098931
     
    1103936    Z3_solver_dec_ref(ctx, solver);
    1104937    Z3_del_context(ctx);
    1105 
    1106 }
    1107 
    1108 ///** ------------------------------------------------------------------------------------------------------------- *
    1109 // * @brief multiplexSelectedSets
    1110 // ** ------------------------------------------------------------------------------------------------------------- */
    1111 //inline void MultiplexingPass::multiplexSelectedSets(PabloBlock * const block, Statement * const begin, Statement * const end) {
    1112 
    1113 //    assert ("begin cannot be null!" && begin);
    1114 //    assert (begin->getParent() == block);
    1115 //    assert (!end || end->getParent() == block);
    1116 //    assert (!end || isa<If>(end) || isa<While>(end));
    1117 
    1118 //    Statement * const ip = begin->getPrevNode(); // save our insertion point prior to modifying the AST
    1119 
    1120 //    Z3_config cfg = Z3_mk_config();
    1121 //    Z3_set_param_value(cfg, "MODEL", "true");
    1122 //    Z3_context ctx = Z3_mk_context(cfg);
    1123 //    Z3_del_config(cfg);
    1124 //    Z3_solver solver = Z3_mk_solver(ctx);
    1125 //    Z3_solver_inc_ref(ctx, solver);
    1126 
    1127 //    const auto first_set = num_vertices(mConstraintGraph);
    1128 //    const auto last_set = num_vertices(mCandidateGraph);
    1129 
    1130 //    // Compute the hard and soft constraints for any part of the AST that we are not intending to modify.
    1131 //    flat_map<Statement *, Z3_ast> M;
    1132 
    1133 //    Z3_ast prior = nullptr;
    1134 //    Z3_ast one = Z3_mk_int(ctx, 1, Z3_mk_int_sort(ctx));
    1135 //    std::vector<Z3_ast> ordering;
    1136 
    1137 //    for (Statement * stmt = begin; stmt != end; stmt = stmt->getNextNode()) { assert (stmt != ip);
    1138 //        Z3_ast node = addWithHardConstraints(ctx, solver, block, stmt, M);
    1139 //        // compute the soft ordering constraints
    1140 //        Z3_ast num = one;
    1141 //        if (prior) {
    1142 //            Z3_ast prior_plus_one[2] = { prior, one };
    1143 //            num = Z3_mk_add(ctx, 2, prior_plus_one);
    1144 //        }
    1145 //        ordering.push_back(Z3_mk_eq(ctx, node, num));
    1146 //        prior = node;
    1147 //    }
    1148 
    1149 //    block->setInsertPoint(block->back()); // <- necessary for domination check!
    1150 
    1151 //    errs() << "---------------------------------------------\n";
    1152 
    1153 //    for (auto idx = first_set; idx != last_set; ++idx) {
    1154 //        const size_t n = degree(idx, mCandidateGraph);
    1155 //        if (n) {
    1156 //            const size_t m = log2_plus_one(n); assert (n > 2 && m < n);
    1157 //            Advance * input[n];
    1158 //            PabloAST * muxed[m];
    1159 //            PabloAST * muxed_n[m];
    1160 
    1161 //            errs() << n << " -> " << m << "\n";
    1162 
    1163 //            // The multiplex set graph is a DAG with edges denoting the set relationships of our independent sets.
    1164 //            unsigned i = 0;
    1165 //            for (const auto u : make_iterator_range(adjacent_vertices(idx, mCandidateGraph))) {
    1166 //                input[i] = mConstraintGraph[u];
    1167 //                assert ("Not all inputs are in the same block!" && (input[i]->getParent() == block));
    1168 //                assert ("Not all inputs advance by the same amount!" && (input[i]->getOperand(1) == input[0]->getOperand(1)));
    1169 //                ++i;
    1170 //            }
    1171 
    1172 //            circular_buffer<PabloAST *> Q(n);
    1173 
    1174 //            /// Perform n-to-m Multiplexing
    1175 //            for (size_t j = 0; j != m; ++j) {
    1176 //                std::ostringstream prefix;
    1177 //                prefix << "mux" << n << "to" << m << '.' << (j);
    1178 //                assert (Q.empty());
    1179 //                for (size_t i = 0; i != n; ++i) {
    1180 //                    if (((i + 1) & (1UL << j)) != 0) {
    1181 //                        Q.push_back(input[i]->getOperand(0));
    1182 //                    }
    1183 //                }
    1184 //                while (Q.size() > 1) {
    1185 //                    PabloAST * a = Q.front(); Q.pop_front();
    1186 //                    PabloAST * b = Q.front(); Q.pop_front();
    1187 //                    PabloAST * expr = block->createOr(a, b);
    1188 //                    addWithHardConstraints(ctx, solver, block, expr, M, ip);
    1189 //                    Q.push_back(expr);
    1190 //                }
    1191 //                PabloAST * const muxing = Q.front(); Q.clear();
    1192 //                muxed[j] = block->createAdvance(muxing, input[0]->getOperand(1), prefix.str());
    1193 //                addWithHardConstraints(ctx, solver, block, muxed[j], M, ip);
    1194 //                muxed_n[j] = block->createNot(muxed[j]);
    1195 //                addWithHardConstraints(ctx, solver, block, muxed_n[j], M, ip);
    1196 //            }
    1197 
    1198 //            /// Perform m-to-n Demultiplexing
    1199 //            for (size_t i = 0; i != n; ++i) {
    1200 //                // Construct the demuxed values and replaces all the users of the original advances with them.
    1201 //                assert (Q.empty());
    1202 //                for (size_t j = 0; j != m; ++j) {
    1203 //                    Q.push_back((((i + 1) & (1UL << j)) != 0) ? muxed[j] : muxed_n[j]);
    1204 //                }
    1205 //                Z3_ast replacement = nullptr;
    1206 //                while (Q.size() > 1) {
    1207 //                    PabloAST * const a = Q.front(); Q.pop_front();
    1208 //                    PabloAST * const b = Q.front(); Q.pop_front();
    1209 //                    PabloAST * expr = block->createAnd(a, b);
    1210 //                    replacement = addWithHardConstraints(ctx, solver, block, expr, M, ip);
    1211 //                    Q.push_back(expr);
    1212 //                }
    1213 //                assert (replacement);
    1214 //                PabloAST * const demuxed = Q.front(); Q.clear();
    1215 
    1216 //                const auto f = M.find(input[i]);
    1217 //                assert (f != M.end());
    1218 //                Z3_solver_assert(ctx, solver, Z3_mk_eq(ctx, f->second, replacement));
    1219 //                M.erase(f);
    1220 
    1221 //                input[i]->replaceWith(demuxed);
    1222 //                assert (M.count(input[i]) == 0);
    1223 //            }
    1224 //        }
    1225 //    }
    1226 
    1227 //    assert (M.count(ip) == 0);
    1228 
    1229 //    // if (LLVM_UNLIKELY(maxsat(ctx, solver, ordering) == Z3_L_FALSE)) {
    1230 //    if (LLVM_UNLIKELY(Z3_solver_check(ctx, solver) != Z3_L_TRUE)) {
    1231 //        throw std::runtime_error("Unexpected Z3 failure when attempting to topologically sort the AST!");
    1232 //    }
    1233 
    1234 //    Z3_model m = Z3_solver_get_model(ctx, solver);
    1235 //    Z3_model_inc_ref(ctx, m);
    1236 
    1237 //    std::vector<std::pair<long long int, Statement *>> Q;
    1238 
    1239 //    errs() << "-----------------------------------------------------------\n";
    1240 
    1241 //    for (const auto i : M) {
    1242 //        Z3_ast value;
    1243 //        if (Z3_model_eval(ctx, m, std::get<1>(i), Z3_L_TRUE, &value) != Z3_L_TRUE) {
    1244 //            throw std::runtime_error("Unexpected Z3 error when attempting to obtain value from model!");
    1245 //        }
    1246 //        long long int line;
    1247 //        if (Z3_get_numeral_int64(ctx, value, &line) != Z3_L_TRUE) {
    1248 //            throw std::runtime_error("Unexpected Z3 error when attempting to convert model value to integer!");
    1249 //        }
    1250 //        Q.emplace_back(line, std::get<0>(i));
    1251 //    }
    1252 
    1253 //    Z3_model_dec_ref(ctx, m);
    1254 //    Z3_solver_dec_ref(ctx, solver);
    1255 //    Z3_del_context(ctx);
    1256 
    1257 //    std::sort(Q.begin(), Q.end());
    1258 
    1259 //    block->setInsertPoint(ip);
    1260 //    for (auto i : Q) {
    1261 //        block->insert(std::get<1>(i));
    1262 //    }
    1263 //}
     938}
    1264939
    1265940/** ------------------------------------------------------------------------------------------------------------- *
     
    1300975    assert (expr);
    1301976    auto f = mCharacterization.find(expr);
    1302     assert (f != mCharacterization.end());
    1303     auto & val = f->second;
     977    if (LLVM_UNLIKELY(f == mCharacterization.end())) {
     978        characterize(cast<Statement>(expr), false);
     979        f = mCharacterization.find(expr);
     980        assert (f != mCharacterization.end());
     981    }
     982    CharacterizationRef & ref = f->second;
    1304983    if (deref) {
    1305         unsigned & refs = std::get<1>(val);
    1306         assert (refs > 0);
    1307         --refs;
    1308     }
    1309     return std::get<0>(val);
     984        if (LLVM_LIKELY(std::get<1>(ref)) > 0) {
     985            std::get<1>(ref) -= 1;
     986        }
     987    }
     988    return std::get<0>(ref);
    1310989}
    1311990
     
    1313992 * @brief make
    1314993 ** ------------------------------------------------------------------------------------------------------------- */
    1315 inline Z3_ast MultiplexingPass::make(const PabloAST * const expr) {
    1316     assert (expr);
     994inline Z3_ast MultiplexingPass::makeVar() {
    1317995    Z3_ast node = Z3_mk_fresh_const(mContext, nullptr, Z3_mk_bool_sort(mContext));
    1318996    Z3_inc_ref(mContext, node);
    1319     return add(expr, node);
     997    return node;
    1320998}
    1321999
     
    13231001 * @brief add
    13241002 ** ------------------------------------------------------------------------------------------------------------- */
    1325 inline Z3_ast MultiplexingPass::add(const PabloAST * const expr, Z3_ast node) {   
    1326     mCharacterization.insert(std::make_pair(expr, std::make_pair(node, expr->getNumUses())));
     1003inline Z3_ast MultiplexingPass::add(const PabloAST * const expr, Z3_ast node, const size_t refs) {
     1004    mCharacterization.insert(std::make_pair(expr, std::make_pair(node, refs)));
    13271005    return node;
    13281006}
     
    13311009 * @brief constructor
    13321010 ** ------------------------------------------------------------------------------------------------------------- */
    1333 inline MultiplexingPass::MultiplexingPass(PabloFunction & f, const RNG::result_type seed, Z3_context context, Z3_solver solver)
     1011inline MultiplexingPass::MultiplexingPass(PabloFunction & f, Z3_context context, Z3_solver solver)
    13341012: mContext(context)
    13351013, mSolver(solver)
    13361014, mFunction(f)
    1337 , mRNG(seed)
    13381015, mConstraintGraph(0)
    13391016{
     
    13411018}
    13421019
    1343 
    1344 inline Z3_ast mk_binary_or(Z3_context ctx, Z3_ast in_1, Z3_ast in_2) {
    1345     Z3_ast args[2] = { in_1, in_2 };
    1346     return Z3_mk_or(ctx, 2, args);
    1347 }
    1348 
    1349 inline Z3_ast mk_ternary_or(Z3_context ctx, Z3_ast in_1, Z3_ast in_2, Z3_ast in_3) {
    1350     Z3_ast args[3] = { in_1, in_2, in_3 };
    1351     return Z3_mk_or(ctx, 3, args);
    1352 }
    1353 
    1354 inline Z3_ast mk_binary_and(Z3_context ctx, Z3_ast in_1, Z3_ast in_2) {
    1355     Z3_ast args[2] = { in_1, in_2 };
    1356     return Z3_mk_and(ctx, 2, args);
    1357 }
    1358 
    1359 ///**
    1360 //   \brief Create a full adder with inputs \c in_1, \c in_2 and \c cin.
    1361 //   The output of the full adder is stored in \c out, and the carry in \c c_out.
    1362 //*/
    1363 //inline std::pair<Z3_ast, Z3_ast> mk_full_adder(Z3_context ctx, Z3_ast in_1, Z3_ast in_2, Z3_ast cin) {
    1364 //    Z3_ast out = Z3_mk_xor(ctx, Z3_mk_xor(ctx, in_1, in_2), cin);
    1365 //    Z3_ast cout = mk_ternary_or(ctx, mk_binary_and(ctx, in_1, in_2), mk_binary_and(ctx, in_1, cin), mk_binary_and(ctx, in_2, cin));
    1366 //    return std::make_pair(out, cout);
    1367 //}
    1368 
    1369 /**
    1370    \brief Create an adder for inputs of size \c num_bits.
    1371    The arguments \c in1 and \c in2 are arrays of bits of size \c num_bits.
    1372 
    1373    \remark \c result must be an array of size \c num_bits + 1.
    1374 */
    1375 void mk_adder(Z3_context ctx, const unsigned num_bits, Z3_ast * in_1, Z3_ast * in_2, Z3_ast * result) {
    1376     Z3_ast cin = Z3_mk_false(ctx);
    1377     for (unsigned i = 0; i < num_bits; i++) {
    1378         result[i] = Z3_mk_xor(ctx, Z3_mk_xor(ctx, in_1[i], in_2[i]), cin);
    1379         cin = mk_ternary_or(ctx, mk_binary_and(ctx, in_1[i], in_2[i]), mk_binary_and(ctx, in_1[i], cin), mk_binary_and(ctx, in_2[i], cin));
    1380     }
    1381     result[num_bits] = cin;
    1382 }
    1383 
    1384 /**
    1385    \brief Given \c num_ins "numbers" of size \c num_bits stored in \c in.
    1386    Create floor(num_ins/2) adder circuits. Each circuit is adding two consecutive "numbers".
    1387    The numbers are stored one after the next in the array \c in.
    1388    That is, the array \c in has size num_bits * num_ins.
    1389    Return an array of bits containing \c ceil(num_ins/2) numbers of size \c (num_bits + 1).
    1390    If num_ins/2 is not an integer, then the last "number" in the output, is the last "number" in \c in with an appended "zero".
    1391 */
    1392 unsigned mk_adder_pairs(Z3_context ctx, const unsigned num_bits, const unsigned num_ins, Z3_ast * in, Z3_ast * out) {
    1393     unsigned out_num_bits = num_bits + 1;
    1394     Z3_ast * _in          = in;
    1395     Z3_ast * _out         = out;
    1396     unsigned out_num_ins  = (num_ins % 2 == 0) ? (num_ins / 2) : (num_ins / 2) + 1;
    1397     for (unsigned i = 0; i < num_ins / 2; i++) {
    1398         mk_adder(ctx, num_bits, _in, _in + num_bits, _out);
    1399         _in  += num_bits;
    1400         _in  += num_bits;
    1401         _out += out_num_bits;
    1402     }
    1403     if (num_ins % 2 != 0) {
    1404         for (unsigned i = 0; i < num_bits; i++) {
    1405             _out[i] = _in[i];
    1406         }
    1407         _out[num_bits] = Z3_mk_false(ctx);
    1408     }
    1409     return out_num_ins;
    1410 }
    1411 
    1412 /**
    1413    \brief Return the \c idx bit of \c val.
    1414 */
    1415 inline bool get_bit(unsigned val, unsigned idx) {
    1416     return (val & (1U << (idx & 31))) != 0;
    1417 }
    1418 
    1419 /**
    1420    \brief Given an integer val encoded in n bits (boolean variables), assert the constraint that val <= k.
    1421 */
    1422 void assert_le_one(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * val)
    1423 {
    1424     Z3_ast i1, i2;
    1425     Z3_ast not_val = Z3_mk_not(ctx, val[0]);
    1426     assert (get_bit(1, 0));
    1427     Z3_ast out = Z3_mk_true(ctx);
    1428     for (unsigned i = 1; i < n; i++) {
    1429         not_val = Z3_mk_not(ctx, val[i]);
    1430         if (get_bit(1, i)) {
    1431             i1 = not_val;
    1432             i2 = out;
    1433         }
    1434         else {
    1435             i1 = Z3_mk_false(ctx);
    1436             i2 = Z3_mk_false(ctx);
    1437         }
    1438         out = mk_ternary_or(ctx, i1, i2, mk_binary_and(ctx, not_val, out));
    1439     }
    1440     Z3_solver_assert(ctx, s, out);
    1441 }
    1442 
    1443 /**
    1444    \brief Create a counter circuit to count the number of "ones" in lits.
    1445    The function returns an array of bits (i.e. boolean expressions) containing the output of the circuit.
    1446    The size of the array is stored in out_sz.
    1447 */
    1448 void mk_counter_circuit(Z3_context ctx, Z3_solver solver, unsigned n, Z3_ast * lits) {
    1449     unsigned k = 1;
    1450     assert (n != 0);
    1451     Z3_ast aux_array_1[n + 1];
    1452     Z3_ast aux_array_2[n + 1];
    1453     Z3_ast * aux_1 = aux_array_1;
    1454     Z3_ast * aux_2 = aux_array_2;
    1455     std::memcpy(aux_1, lits, sizeof(Z3_ast) * n);
    1456     while (n > 1) {
    1457         assert (aux_1 != aux_2);
    1458         n = mk_adder_pairs(ctx, k++, n, aux_1, aux_2);
    1459         std::swap(aux_1, aux_2);
    1460     }
    1461     assert_le_one(ctx, solver, k, aux_1);
    1462 }
    1463 
    1464 /** ------------------------------------------------------------------------------------------------------------- *
    1465  * Fu & Malik procedure for MaxSAT. This procedure is based on unsat core extraction and the at-most-one constraint.
    1466  ** ------------------------------------------------------------------------------------------------------------- */
    1467 Z3_bool maxsat(Z3_context ctx, Z3_solver solver, std::vector<Z3_ast> & soft) {
    1468     if (LLVM_UNLIKELY(Z3_solver_check(ctx, solver) == Z3_L_FALSE)) {
    1469         return Z3_L_FALSE;
    1470     }
    1471     if (LLVM_UNLIKELY(soft.empty())) {
    1472         return true;
    1473     }
    1474 
    1475     const auto n = soft.size();
    1476     const auto ty = Z3_mk_bool_sort(ctx);
    1477     Z3_ast aux_vars[n];
    1478     Z3_ast assumptions[n];
    1479 
    1480     for (unsigned i = 0; i < n; ++i) {
    1481         aux_vars[i] = Z3_mk_fresh_const(ctx, nullptr, ty);
    1482         Z3_solver_assert(ctx, solver, mk_binary_or(ctx, soft[i], aux_vars[i]));
    1483     }
    1484 
    1485     for (;;) {
    1486         // create assumptions
    1487         for (unsigned i = 0; i < n; i++) {
    1488             // Recall that we asserted (soft_cnstrs[i] \/ aux_vars[i])
    1489             // So using (NOT aux_vars[i]) as an assumption we are actually forcing the soft_cnstrs[i] to be considered.
    1490             assumptions[i] = Z3_mk_not(ctx, aux_vars[i]);
    1491         }
    1492         if (Z3_solver_check_assumptions(ctx, solver, n, assumptions) != Z3_L_FALSE) {
    1493             return Z3_L_TRUE; // done
    1494         } else {
    1495             Z3_ast_vector core = Z3_solver_get_unsat_core(ctx, solver);
    1496             unsigned m = Z3_ast_vector_size(ctx, core);
    1497             Z3_ast block_vars[m];
    1498             unsigned k = 0;
    1499             // update soft-constraints and aux_vars
    1500             for (unsigned i = 0; i < n; i++) {
    1501                 // check whether assumption[i] is in the core or not
    1502                 for (unsigned j = 0; j < m; j++) {
    1503                     if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) {
    1504                         // assumption[i] is in the unsat core... so soft_cnstrs[i] is in the unsat core
    1505                         Z3_ast block_var = Z3_mk_fresh_const(ctx, nullptr, ty);
    1506                         Z3_ast new_aux_var = Z3_mk_fresh_const(ctx, nullptr, ty);
    1507                         soft[i] = mk_binary_or(ctx, soft[i], block_var);
    1508                         aux_vars[i] = new_aux_var;
    1509                         block_vars[k] = block_var;
    1510                         ++k;
    1511                         // Add new constraint containing the block variable.
    1512                         // Note that we are using the new auxiliary variable to be able to use it as an assumption.
    1513                         Z3_solver_assert(ctx, solver, mk_binary_or(ctx, soft[i], new_aux_var) );
    1514                         break;
    1515                     }
    1516                 }
    1517 
    1518             }
    1519             if (k > 1) {
    1520                 mk_counter_circuit(ctx, solver, k, block_vars);
    1521             }
    1522         }
    1523     }
    1524     llvm_unreachable("unreachable");
    1525     return Z3_L_FALSE;
    1526 }
    1527 
    15281020} // end of namespace pablo
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_automultiplexing.hpp

    r5119 r5156  
    88#include <boost/graph/adjacency_matrix.hpp>
    99#include <boost/container/flat_set.hpp>
    10 #include <boost/container/flat_map.hpp>
    11 #include <boost/numeric/ublas/matrix.hpp>
    12 #include <random>
    1310#include <stdint.h>
    1411#include <llvm/ADT/DenseMap.h>
    15 #include <llvm/ADT/DenseSet.h>
    16 #include <llvm/ADT/SmallVector.h>
    1712#include <z3.h>
    18 #include <stack>
    1913
    2014namespace pablo {
     
    2519class MultiplexingPass {
    2620
    27     using CharacterizationRef = std::pair<Z3_ast, unsigned>;
     21    using CharacterizationRef = std::pair<Z3_ast, size_t>;
    2822    using CharacterizationMap = llvm::DenseMap<const PabloAST *, CharacterizationRef>;
    2923
    30     using ConstraintGraph = boost::adjacency_matrix<boost::undirectedS, Advance *>;
     24    enum class ConstraintType : uint8_t {
     25        Dependency,
     26        Inclusive
     27    };
     28
     29    using ConstraintGraph = boost::adjacency_matrix<boost::undirectedS, Advance *, ConstraintType>;
    3130    using ConstraintVertex = ConstraintGraph::vertex_descriptor;
    3231    using Constraints = std::vector<ConstraintVertex>;
    33     using ConstraintMap = boost::container::flat_map<Advance *, ConstraintVertex>;
    34 
    35     using RNG = std::mt19937;
    36     using IntDistribution = std::uniform_int_distribution<RNG::result_type>;
    3732
    3833    using CandidateGraph = boost::adjacency_list<boost::setS, boost::vecS, boost::undirectedS>;
     
    4136    using SubsetGraph = boost::adjacency_list<boost::hash_setS, boost::vecS, boost::bidirectionalS>;
    4237
    43     using CliqueGraph = boost::adjacency_list<boost::hash_setS, boost::vecS, boost::undirectedS>;
    44     using CliqueSet = boost::container::flat_set<CliqueGraph::vertex_descriptor>;
    45     using CliqueSets = boost::container::flat_set<std::vector<CliqueGraph::vertex_descriptor>>;
    46 
    47     using AdvanceVector = std::vector<Advance *>;
    48     using AdvanceRank = std::vector<int>;
    4938    using AdvanceVariable = std::vector<Z3_ast>;
    5039
     
    6251    void optimize();
    6352    void optimize(PabloBlock * const block);
    64     Z3_ast characterize(Statement * const stmt);
    65     Z3_ast characterize(Advance * const adv, Z3_ast Ik);
     53    Z3_ast characterize(const Statement * const stmt, const bool deref = true);
     54    Z3_ast characterize(const Advance * const adv, Z3_ast Ik);
    6655    void multiplex(PabloBlock * const block, Statement * const begin, Statement * const end);
    6756
     
    7766
    7867
    79     Z3_ast make(const PabloAST * const expr);
    80     Z3_ast add(const PabloAST * const expr, Z3_ast node);
     68    Z3_ast makeVar();
     69    Z3_ast add(const PabloAST * const expr, Z3_ast node, const size_t refs);
    8170    Z3_ast & get(const PabloAST * const expr, const bool deref = false);
    8271    bool equals(Z3_ast a, Z3_ast b);
    8372
    84     MultiplexingPass(PabloFunction & f, const RNG::result_type seed, Z3_context context, Z3_solver solver);
     73    MultiplexingPass(PabloFunction & f, Z3_context context, Z3_solver solver);
    8574
    8675private:
     
    8978    Z3_solver                   mSolver;
    9079    PabloFunction &             mFunction;
    91     RNG                         mRNG;
    9280
    9381    CharacterizationMap         mCharacterization;
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_simplifier.cpp

    r4959 r5156  
    7575    if (LLVM_LIKELY(isa<And>(var) || isa<Or>(var))) {
    7676        // Apply an implicit distribution + identity law whenever possible
    77         //    (P ∧ Q) √ (P ∧ ¬Q) = P √ (Q ∧ ¬Q) ⇔ (P √ Q) ∧ (P √ ¬Q) = P ∧ (Q √ ¬Q) ⇔ P
     77        //    (P ∧ Q) √ (P ∧ ¬Q) = P √ (Q ∧ ¬Q) ⇔ P
    7878        const TypeId typeId = isa<And>(var) ? TypeId::Or : TypeId::And;
    7979        for (unsigned i = 1; i < var->getNumOperands(); ++i) {
    8080            if (var->getOperand(i)->getClassTypeId() == typeId) {
    8181                Variadic * const Vi = cast<Variadic>(var->getOperand(i));
    82                 assert (std::is_sorted(Vi->begin(), Vi->end()));
     82                if (LLVM_UNLIKELY(!std::is_sorted(Vi->begin(), Vi->end()))) {
     83                    std::sort(Vi->begin(), Vi->end());
     84                }
    8385                for (unsigned j = 0; j < i; ++j) {
    8486                    assert (var->getOperand(i) == Vi);
    8587                    if (var->getOperand(j)->getClassTypeId() == typeId) {
    8688                        Variadic * const Vj = cast<Variadic>(var->getOperand(j));
    87                         assert (std::is_sorted(Vj->begin(), Vj->end()));
     89                        if (LLVM_UNLIKELY(!std::is_sorted(Vj->begin(), Vj->end()))) {
     90                            std::sort(Vj->begin(), Vj->end());
     91                        }
    8892                        if (Vi->getNumOperands() == Vj->getNumOperands()) {
    8993                            // If vi and vj differ by precisely one operand, say di and dj, and di ⇔ ¬dj, we can apply this rule.
     
    308312 ** ------------------------------------------------------------------------------------------------------------- */
    309313inline bool Simplifier::isSuperfluous(const Assign * const assign) {
    310     for (const PabloAST * user : assign->users()) {
    311         if (LLVM_UNLIKELY(isa<PabloFunction>(user) || isa<Next>(user))) {
    312             return false;
    313         } else if (isa<If>(user)) {
    314             if (LLVM_UNLIKELY(cast<If>(user)->getCondition() == assign)) {
    315                 continue;
    316             } else if (isa<Assign>(assign->getExpression())) {
    317                 continue;
    318             }
    319             return false;
     314    if (LLVM_LIKELY(isa<Statement>(assign->getExpression()))) {
     315        for (const PabloAST * user : assign->users()) {
     316            if (LLVM_UNLIKELY(isa<PabloFunction>(user) || isa<Next>(user))) {
     317                return false;
     318            } else if (isa<If>(user)) {
     319                if (LLVM_UNLIKELY(cast<If>(user)->getCondition() == assign)) {
     320                    continue;
     321                } else if (isa<Assign>(assign->getExpression())) {
     322                    continue;
     323                }
     324                return false;
     325            }
    320326        }
    321327    }
     
    421427 * as replacements. Let the DCE remove the unnecessary statements with the finalized Def-Use information.
    422428 ** ------------------------------------------------------------------------------------------------------------- */
    423 void Simplifier::redundancyElimination(PabloBlock * const block, ExpressionTable * predecessor) {
     429void Simplifier::redundancyElimination(PabloFunction & function, PabloBlock * const block, ExpressionTable * predecessor) {
    424430    ExpressionTable encountered(predecessor);
    425431    Statement * stmt = block->front();
    426432
    427433    while (stmt) {
    428 
    429434        if (Assign * assign = dyn_cast<Assign>(stmt)) {
    430435            // If we have an Assign whose users do not contain an If or Next node, we can replace its users with
     
    456461
    457462            // Process the If body
    458             redundancyElimination(cast<If>(stmt)->getBody(), &encountered);
     463            redundancyElimination(function, cast<If>(stmt)->getBody(), &encountered);
    459464
    460465            // If we ended up removing all of the defined variables, delete the If node.
     
    495500                continue;
    496501            }
    497             redundancyElimination(whileNode->getBody(), &encountered);
     502            redundancyElimination(function, whileNode->getBody(), &encountered);
    498503            removeIdenticalEscapedValues(whileNode->getVariants());
    499504            // If the condition's Next state is Zero, we can eliminate the loop after copying the internal
     
    541546 * @brief deadCodeElimination
    542547 ** ------------------------------------------------------------------------------------------------------------- */
    543 void Simplifier::deadCodeElimination(PabloBlock * const block) {
     548void Simplifier::dce(PabloBlock * const block) {
    544549    Statement * stmt = block->front();
    545550    while (stmt) {
    546551        if (LLVM_UNLIKELY(isa<If>(stmt))) {
    547             deadCodeElimination(cast<If>(stmt)->getBody());
     552            dce(cast<If>(stmt)->getBody());
    548553        } else if (LLVM_UNLIKELY(isa<While>(stmt))) {
    549             deadCodeElimination(cast<While>(stmt)->getBody());
     554            dce(cast<While>(stmt)->getBody());
    550555        } else if (LLVM_UNLIKELY(unused(stmt))){
    551556            stmt = stmt->eraseFromParent(true);
     
    615620 ** ------------------------------------------------------------------------------------------------------------- */
    616621bool Simplifier::optimize(PabloFunction & function) {
    617     redundancyElimination(function.getEntryBlock());
     622    redundancyElimination(function, function.getEntryBlock());
     623    strengthReduction(function.getEntryBlock());
     624    dce(function.getEntryBlock());
    618625    #ifndef NDEBUG
    619     PabloVerifier::verify(function, "post-eliminate-redundant-code");
    620     #endif
    621     strengthReduction(function.getEntryBlock());
    622     #ifndef NDEBUG
    623     PabloVerifier::verify(function, "post-strength-reduction");
    624     #endif
    625     deadCodeElimination(function.getEntryBlock());
    626     #ifndef NDEBUG
    627     PabloVerifier::verify(function, "post-dead-code-elimination");
     626    PabloVerifier::verify(function, "post-simplification");
    628627    #endif
    629628    return true;
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_simplifier.hpp

    r4927 r5156  
    1414public:
    1515    static bool optimize(PabloFunction & function);
     16    static void dce(PabloBlock * const block);
    1617protected:
    1718    Simplifier() = default;
    1819private:
    19     static void redundancyElimination(PabloBlock * const block, ExpressionTable * predecessor = nullptr);
     20    static void redundancyElimination(PabloFunction & function, PabloBlock * const block, ExpressionTable * predecessor = nullptr);
    2021    static PabloAST * fold(Variadic * var, PabloBlock * const block);
    2122    static PabloAST * fold(Statement * const stmt, PabloBlock * const block);
    22     static void deadCodeElimination(PabloBlock * const block);
    2323    static void strengthReduction(PabloBlock * const block);
    2424    static bool isSuperfluous(const Assign * const assign);
  • icGREP/icgrep-devel/icgrep/pablo/pabloAST.cpp

    r5042 r5156  
    1010#include <pablo/printer_pablos.h>
    1111#include <llvm/ADT/SmallVector.h>
     12#include <boost/container/flat_set.hpp>
     13
     14using namespace boost::container;
    1215
    1316namespace pablo {
     
    2225 *  false may be returned i some cases when the exprs are equivalent.
    2326 ** ------------------------------------------------------------------------------------------------------------- */
    24 bool equals(const PabloAST * expr1, const PabloAST * expr2) {
     27bool equals(const PabloAST * const expr1, const PabloAST * const expr2) {
    2528    assert (expr1 && expr2);
    2629    if (expr1 == expr2) {
     
    103106
    104107/** ------------------------------------------------------------------------------------------------------------- *
     108 * @brief addUser
     109 ** ------------------------------------------------------------------------------------------------------------- */
     110void PabloAST::addUser(PabloAST * const user) {
     111    assert (user);
     112    // Note: for the rare situation that this node is used multiple times by the same statement, duplicates are allowed.
     113    mUsers.insert(std::lower_bound(mUsers.begin(), mUsers.end(), user), user);
     114}
     115
     116/** ------------------------------------------------------------------------------------------------------------- *
     117 * @brief removeUser
     118 ** ------------------------------------------------------------------------------------------------------------- */
     119void PabloAST::removeUser(PabloAST * const user) {
     120    assert (user);
     121    const auto pos = std::lower_bound(mUsers.begin(), mUsers.end(), user);
     122    if (LLVM_UNLIKELY(pos == mUsers.end() || *pos != user)) {
     123        std::string tmp;
     124        raw_string_ostream out(tmp);
     125        out << "Cannot remove user ";
     126        PabloPrinter::print(user, out);
     127        out << " from ";
     128        PabloPrinter::print(this, out);
     129        out << " because it's not in its user list!";
     130        throw std::runtime_error(out.str());
     131    }
     132    mUsers.erase(pos);
     133}
     134
     135
     136/** ------------------------------------------------------------------------------------------------------------- *
    105137 * @brief checkEscapedValueList
    106138 ** ------------------------------------------------------------------------------------------------------------- */
     
    108140inline void Statement::checkEscapedValueList(Statement * const branch, PabloAST * const from, PabloAST * const to, ValueList & list) {
    109141    if (LLVM_LIKELY(isa<ValueType>(from))) {
    110         auto f = std::find(list.begin(), list.end(), cast<ValueType>(from));
     142        const auto f = std::find(list.begin(), list.end(), cast<ValueType>(from));
    111143        if (LLVM_LIKELY(f != list.end())) {
    112144            branch->removeUser(from);
    113145            from->removeUser(branch);
    114             if (LLVM_LIKELY(isa<ValueType>(to))) {
    115                 if (std::count(list.begin(), list.end(), cast<ValueType>(to)) == 0) {
    116                     *f = cast<ValueType>(to);
    117                     branch->addUser(to);
    118                     to->addUser(branch);
    119                     return;
     146            if (LLVM_UNLIKELY(isa<ValueType>(to))) {
     147                if (LLVM_LIKELY(std::find(list.begin(), list.end(), cast<ValueType>(to)) == list.end())) {
     148                    PabloBlock * parent = cast<ValueType>(to)->getParent();
     149                    for (;;) {
     150                        if (parent == cast<ValueType>(from)->getParent()) {
     151                            *f = cast<ValueType>(to);
     152                            branch->addUser(to);
     153                            to->addUser(branch);
     154                            return;
     155                        }
     156                        parent = parent->getParent();
     157                        if (parent == nullptr) {
     158                            break;
     159                        }
     160                    }
    120161                }
    121162            }
     
    254295 ** ------------------------------------------------------------------------------------------------------------- */
    255296Statement * Statement::eraseFromParent(const bool recursively) {
    256     // remove this statement from its operands' users list
    257     for (unsigned i = 0; i != mOperands; ++i) {
    258         mOperand[i]->removeUser(this);
    259     }
     297
    260298    SmallVector<Statement *, 1> redundantBranches;
    261299    // If this is an If or While statement, we'll have to remove the statements within the
     
    300338    if (recursively) {
    301339        for (unsigned i = 0; i != mOperands; ++i) {
    302             PabloAST * const op = mOperand[i];
    303             if (LLVM_LIKELY(isa<Statement>(op))) {
    304                 if (op->getNumUses() == 0) {
    305                     cast<Statement>(op)->eraseFromParent(true);
    306                 }
    307             }
     340            PabloAST * const op = mOperand[i]; assert (op);
     341            op->removeUser(this);
     342            if (LLVM_UNLIKELY(op->getNumUses() == 0 && isa<Statement>(op))) {
     343                cast<Statement>(op)->eraseFromParent(true);
     344            }
     345            mOperand[i] = nullptr;
    308346        }
    309347        if (LLVM_UNLIKELY(redundantBranches.size() != 0)) {
     
    321359                return nullptr;
    322360            }
     361        }
     362    } else { // just remove this statement from its operands' users list
     363        for (unsigned i = 0; i != mOperands; ++i) {
     364            PabloAST * const op = mOperand[i]; assert (op);
     365            op->removeUser(this);
     366            mOperand[i] = nullptr;
    323367        }
    324368    }
     
    413457}
    414458
    415 }
     459/** ------------------------------------------------------------------------------------------------------------- *
     460 * @brief dominates
     461 *
     462 * Does a precede (dominate) b?
     463 ** ------------------------------------------------------------------------------------------------------------- */
     464bool dominates(const PabloAST * const expr1, const PabloAST * const expr2) {
     465    if (LLVM_UNLIKELY(expr1 == nullptr || expr2 == nullptr)) {
     466        return (expr2 == nullptr);
     467    } else if (LLVM_LIKELY(isa<Statement>(expr1))) {
     468        const Statement * stmt1 = cast<Statement>(expr1);
     469        assert ("expr1 is not in any block!" && stmt1->getParent());
     470        if (isa<Statement>(expr2)) {
     471            const Statement * stmt2 = cast<Statement>(expr2);
     472            assert ("expr2 is not in any block!" && stmt2->getParent());
     473
     474            while (stmt1->getParent() != stmt2->getParent()) {
     475
     476                // Statement 1 preceeds Statement 2 if the branch leading to Statement 2
     477                // succeeds Statement 1.
     478
     479                // But if Statement 1 escapes its block, it may still succeed Statement 2
     480                // if and only if Statement 1 is an Assign or Next node whose outermost
     481                // branch succeeds Statement 1. It is not enough to simply traverse back
     482                // arbritarily. Test.
     483
     484                if (LLVM_UNLIKELY(isa<Assign>(stmt1))) {
     485                    for (const PabloAST * user : stmt1->users()) {
     486                        if (isa<If>(user)) {
     487                            for (const Assign * def : cast<If>(user)->getDefined()) {
     488                                if (def == stmt1) {
     489                                    const Statement * test = stmt1;
     490                                    for (;;) {
     491                                        if (test->getParent() == stmt2->getParent()) {
     492                                            stmt1 = test;
     493                                            goto check;
     494                                        }
     495                                        test = test->getParent()->getBranch();
     496                                        if (test == nullptr) {
     497                                            break;
     498                                        }
     499                                    }
     500                                }
     501                            }
     502                        }
     503                    }
     504                } else if (LLVM_UNLIKELY(isa<Next>(stmt1))) {
     505                    for (const PabloAST * user : stmt1->users()) {
     506                        if (isa<While>(user)) {
     507                            for (const Next * var : cast<While>(user)->getVariants()) {
     508                                if (var == stmt1) {
     509                                    const Statement * test = stmt1;
     510                                    for (;;) {
     511                                        if (test->getParent() == stmt2->getParent()) {
     512                                            stmt1 = test;
     513                                            goto check;
     514                                        }
     515                                        test = test->getParent()->getBranch();
     516                                        if (test == nullptr) {
     517                                            break;
     518                                        }
     519                                    }
     520                                }
     521                            }
     522                        }
     523                    }
     524                }
     525
     526                stmt2 = stmt2->getParent()->getBranch();
     527                if (stmt2 == nullptr) {
     528                    return false;
     529                }
     530
     531            }
     532
     533check:      assert(stmt1->getParent() == stmt2->getParent());
     534
     535            const Statement * temp1 = stmt1, * temp2 = stmt2;
     536            while (temp1 && temp2) {
     537                if (temp1 == stmt2) {
     538                    return true;
     539                } else if (temp2 == stmt1) {
     540                    return false;
     541                }
     542                temp1 = temp1->getNextNode();
     543                temp2 = temp2->getNextNode();
     544            }
     545            return (temp2 == nullptr);
     546        }
     547        return false;
     548    }
     549    return true;
     550}
     551
     552
     553}
  • icGREP/icgrep-devel/icgrep/pablo/pabloAST.h

    r5063 r5156  
    143143};
    144144
    145 bool equals(const PabloAST * expr1, const PabloAST *expr2);
     145bool equals(const PabloAST * const expr1, const PabloAST * const expr2);
     146
     147bool dominates(const PabloAST * const expr1, const PabloAST * const expr2);
    146148
    147149class StatementList;
     
    603605
    604606/** ------------------------------------------------------------------------------------------------------------- *
    605  * @brief addUser
    606  ** ------------------------------------------------------------------------------------------------------------- */
    607 inline void PabloAST::addUser(PabloAST * const user) {
    608     assert (user);   
    609     // Note: for the rare situation that this node is used multiple times by the same statement, duplicates are allowed.
    610     mUsers.insert(std::lower_bound(mUsers.begin(), mUsers.end(), user), user);
    611 }
    612 
    613 /** ------------------------------------------------------------------------------------------------------------- *
    614  * @brief removeUser
    615  ** ------------------------------------------------------------------------------------------------------------- */
    616 inline void PabloAST::removeUser(PabloAST * const user) {
    617     assert (user);
    618     const auto pos = std::lower_bound(mUsers.begin(), mUsers.end(), user);
    619     assert ("Could not find user to remove!" && (pos != mUsers.end() && *pos == user));
    620     mUsers.erase(pos);
    621 }
    622 
    623 /** ------------------------------------------------------------------------------------------------------------- *
    624607 * @brief deleteOperand
    625608 ** ------------------------------------------------------------------------------------------------------------- */
  • icGREP/icgrep-devel/icgrep/pablo/pablo_compiler.cpp

    r5141 r5156  
    2121#include <llvm/Support/Debug.h>
    2222
    23 
    2423namespace pablo {
    2524
     
    4948   
    5049void PabloCompiler::compile(Function * doBlockFunction) {
     50
    5151    // Make sure that we generate code into the right module.
    5252    mMod = iBuilder->getModule();
     
    7070        outputSet_ptr = mKernelBuilder->getStreamSetBlockPtr(mSelf, outputName, blockNo);
    7171    }
     72
     73    mMarkerMap.emplace(PabloBlock::createZeroes(), iBuilder->allZeroes());
     74    mMarkerMap.emplace(PabloBlock::createOnes(), iBuilder->allOnes());
    7275    for (unsigned j = 0; j < mPabloFunction->getNumOfParameters(); ++j) {
    7376        Value * inputVal = iBuilder->CreateGEP(inputSet_ptr, {iBuilder->getInt32(0), iBuilder->getInt32(j)});
     
    8992    }
    9093    iBuilder->CreateRetVoid();
    91 
    9294   
    9395    #ifdef PRINT_TIMING_INFORMATION
     
    9597    std::cerr << "PABLO COMPILATION TIME: " << (pablo_compilation_end - pablo_compilation_start) << std::endl;
    9698    #endif
    97 
    9899}
    99100
     
    225226    for (const Next * n : nextNodes) {
    226227        PHINode * phi = iBuilder->CreatePHI(mBitBlockType, 2, n->getName()->value());
    227         auto f = mMarkerMap.find(n->getInitial());
     228        auto f = mMarkerMap.find(n->getInitial());       
    228229        assert (f != mMarkerMap.end());
    229230        phi->addIncoming(f->second, whileEntryBlock);
  • icGREP/icgrep-devel/icgrep/pablo/pablo_toolchain.cpp

    r5032 r5156  
    1919#include <pablo/optimizers/pablo_automultiplexing.hpp>
    2020#include <pablo/optimizers/pablo_bddminimization.h>
     21#include <pablo/optimizers/booleanreassociationpass.h>
    2122#include <pablo/optimizers/distributivepass.h>
    2223#include <pablo/optimizers/schedulingprepass.h>
     
    2829#include <llvm/Support/CommandLine.h>
    2930#include <llvm/Support/FileSystem.h>
    30 
     31#ifdef PRINT_TIMING_INFORMATION
     32#include <hrtime.h>
     33#endif
    3134
    3235namespace pablo {
     
    3437
    3538static cl::OptionCategory PabloOptions("Pablo Options", "These options control printing, generation and instrumentation of Pablo intermediate code.");
    36 const cl::OptionCategory * pablo_toolchain_flags() {return &PabloOptions;};
     39
     40const cl::OptionCategory * pablo_toolchain_flags() {
     41    return &PabloOptions;
     42}
    3743   
    3844   
     
    205211    }
    206212#ifdef ENABLE_MULTIPLEXING
    207     if (PabloOptimizationsOptions.isSet(EnableLowering) || PabloOptimizationsOptions.isSet(EnablePreDistribution) || PabloOptimizationsOptions.isSet(EnablePostDistribution)) {
    208         READ_CYCLE_COUNTER(coalescing_start);
    209         CanonicalizeDFG::transform(*function);
    210         READ_CYCLE_COUNTER(coalescing_end);
    211     }
     213//    if (PabloOptimizationsOptions.isSet(EnableLowering) || PabloOptimizationsOptions.isSet(EnablePreDistribution) || PabloOptimizationsOptions.isSet(EnablePostDistribution)) {
     214//        READ_CYCLE_COUNTER(coalescing_start);
     215//        CanonicalizeDFG::transform(*function);
     216//        READ_CYCLE_COUNTER(coalescing_end);
     217//    }
    212218    if (PabloOptimizationsOptions.isSet(EnablePreDistribution)) {
    213219        READ_CYCLE_COUNTER(pre_distribution_start);
    214         DistributivePass::optimize(*function);
     220        BooleanReassociationPass::optimize(*function);
    215221        READ_CYCLE_COUNTER(pre_distribution_end);
    216222    }
     
    219225        MultiplexingPass::optimize(*function);
    220226        READ_CYCLE_COUNTER(multiplexing_end);
    221         if (PabloOptimizationsOptions.isSet(EnableLowering) || PabloOptimizationsOptions.isSet(EnablePreDistribution) || PabloOptimizationsOptions.isSet(EnablePostDistribution)) {
    222             CanonicalizeDFG::transform(*function);
    223         }
     227//        if (PabloOptimizationsOptions.isSet(EnableLowering) || PabloOptimizationsOptions.isSet(EnablePreDistribution) || PabloOptimizationsOptions.isSet(EnablePostDistribution)) {
     228//            CanonicalizeDFG::transform(*function);
     229//        }
    224230    }
    225231    if (PabloOptimizationsOptions.isSet(EnablePostDistribution)) {
    226232        READ_CYCLE_COUNTER(post_distribution_start);
    227         DistributivePass::optimize(*function);
     233        BooleanReassociationPass::optimize(*function);
    228234        READ_CYCLE_COUNTER(post_distribution_end);
    229235    }
     
    244250    distribution = SUMMARIZE_VARIADIC_DISTRIBUTION(function);
    245251    #endif
    246     if (PabloOptimizationsOptions.isSet(EnableLowering) || PabloOptimizationsOptions.isSet(EnablePreDistribution) || PabloOptimizationsOptions.isSet(EnablePostDistribution)) {
    247         READ_CYCLE_COUNTER(lowering_start);
    248         FactorizeDFG::transform(*function);
    249         READ_CYCLE_COUNTER(lowering_end);
    250     }
    251     if (PabloOptimizationsOptions.isSet(EnablePrePassScheduling)) {
    252         READ_CYCLE_COUNTER(scheduling_start);
    253         SchedulingPrePass::optimize(*function);
    254         READ_CYCLE_COUNTER(scheduling_end);
    255     }
     252//    if (PabloOptimizationsOptions.isSet(EnableLowering) || PabloOptimizationsOptions.isSet(EnablePreDistribution) || PabloOptimizationsOptions.isSet(EnablePostDistribution)) {
     253//        READ_CYCLE_COUNTER(lowering_start);
     254//        FactorizeDFG::transform(*function);
     255//        READ_CYCLE_COUNTER(lowering_end);
     256//    }
     257//    if (PabloOptimizationsOptions.isSet(EnablePrePassScheduling)) {
     258//        READ_CYCLE_COUNTER(scheduling_start);
     259//        SchedulingPrePass::optimize(*function);
     260//        READ_CYCLE_COUNTER(scheduling_end);
     261//    }
    256262#endif
    257263#ifdef PRINT_TIMING_INFORMATION
     
    277283    std::cerr << "  PRE-DISTRIBUTION TIME: " << (pre_distribution_end - pre_distribution_start) << std::endl;
    278284    std::cerr << "  MULTIPLEXING TIME: " << (multiplexing_end - multiplexing_start) << std::endl;
    279     std::cerr << "  MULTIPLEXING SEED: " << MultiplexingPass::SEED << std::endl;
    280     std::cerr << "  MULTIPLEXING NODES USED: " << MultiplexingPass::NODES_USED << std::endl;
    281     std::cerr << "  MULTIPLEXING NODES ALLOCATED: " << MultiplexingPass::NODES_ALLOCATED << std::endl;
    282285    std::cerr << "  LOWERING TIME: " << (lowering_end - lowering_start) << std::endl;
    283286    std::cerr << "  FLATTENIF TIME: " << (flattenif_end - flattenif_start) << std::endl;
  • icGREP/icgrep-devel/icgrep/pablo/passes/factorizedfg.cpp

    r4927 r5156  
    88#include <boost/circular_buffer.hpp>
    99#include <boost/graph/adjacency_list.hpp>
     10#include <boost/type_traits/ice.hpp>
    1011#include <boost/graph/adjacency_matrix.hpp>
    1112#include <queue>
  • icGREP/icgrep-devel/icgrep/pablo/pe_next.h

    r4876 r5156  
    1818        return false;
    1919    }
    20     inline const Assign * getInitial() const {
    21         return cast<const Assign>(getOperand(1));
     20    inline PabloAST * getInitial() const {
     21        return getOperand(1);
    2222    }
    2323    inline PabloAST * getExpr() const {
  • icGREP/icgrep-devel/icgrep/pablo/printer_pablos.cpp

    r5043 r5156  
    154154    } else if (isa<Integer>(expr)) {
    155155        out << cast<Integer>(expr)->value();
     156    } else if (isa<Prototype>(expr)) {
     157        out << cast<Prototype>(expr)->getName();
     158    } else if (isa<PabloFunction>(expr)) {
     159        out << cast<PabloFunction>(expr)->getName();
    156160    } else {
    157161        out << "???";
  • icGREP/icgrep-devel/icgrep/pablo/ps_if.cpp

    r5037 r5156  
    6060
    6161PabloBlock * If::setBody(PabloBlock * body) {
     62    body->setBranch(this);
    6263    body->setParent(mBody->getParent());
    6364    std::swap(mBody, body);
  • icGREP/icgrep-devel/icgrep/pablo/ps_while.cpp

    r5037 r5156  
    3131
    3232PabloBlock * While::setBody(PabloBlock * body) {
     33    body->setBranch(this);
    3334    body->setParent(mBody->getParent());
    3435    std::swap(mBody, body);
  • icGREP/icgrep-devel/icgrep/toolchain.cpp

    r5151 r5156  
    3838static cl::opt<std::string> IROutputFilename("dump-generated-IR-output", cl::init(""), cl::desc("output IR filename"), cl::cat(CodeGenOptions));
    3939static cl::opt<bool> DumpASM("DumpASM", cl::init(false), cl::desc("Print Assembly Code."), cl::cat(CodeGenOptions));
     40static cl::opt<std::string> ASMOutputFilename("asm-output", cl::init(""), cl::desc("output ASM filename"), cl::cat(CodeGenOptions));
    4041static cl::opt<bool> AsmVerbose("asm-verbose",
    4142                                cl::desc("Add comments to directives."),
     
    126127
    127128    llvm::SmallString<128> Str;
    128     llvm::raw_svector_ostream dest(Str);
    129 
    130     if (TM->addPassesToEmitFile( PM , dest , llvm::TargetMachine::CGFT_AssemblyFile ) ) {
    131       std::cout << "addPassesToEmitFile failed\n";
    132       exit(1);
     129    llvm::raw_svector_ostream dest(Str);
     130
     131    if (TM->addPassesToEmitFile(PM, dest, llvm::TargetMachine::CGFT_AssemblyFile ) ) {
     132        throw std::runtime_error("LLVM error: addPassesToEmitFile failed.");
    133133    }
    134134    PM.run(*m);
    135     std::cerr << std::string( Str.c_str() ) << "\n";
     135
     136    if (codegen::ASMOutputFilename.empty()) {
     137        errs() << Str;
     138    } else {
     139        std::error_code error;
     140        llvm::raw_fd_ostream out(codegen::ASMOutputFilename, error, sys::fs::OpenFlags::F_None);
     141        out << Str;
     142    }
    136143}
    137144
Note: See TracChangeset for help on using the changeset viewer.