diff --git a/CMakeLists.txt b/CMakeLists.txt index 7284d5b0d1e4bc5cccecac5f7cbd0c37816314c2..273b98fe93fe5f883caa5731af66baa35cc85278 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -20,12 +20,12 @@ set(SOURCES "src/lruzdd.cpp" ) -add_subdirectory(cudd) -add_subdirectory(extra) - # script project(${PLUGIN}) +add_subdirectory(cudd) +add_subdirectory(extra) + # look for OTAWA if(NOT OTAWA_CONFIG) find_program(OTAWA_CONFIG otawa-config DOC "path to otawa-config") @@ -56,14 +56,15 @@ add_library(${PLUGIN} SHARED ${SOURCES}) set_property(TARGET ${PLUGIN} PROPERTY PREFIX "") set_property(TARGET ${PLUGIN} PROPERTY COMPILE_FLAGS "${OTAWA_CFLAGS} --std=c++11 -g -Wall -Wextra -pedantic") -add_dependencies(${PLUGIN} libcudd) -add_dependencies(${PLUGIN} libextra) +add_dependencies(${PLUGIN} cudd) +add_dependencies(${PLUGIN} extra) target_include_directories(${PLUGIN} PUBLIC "${CMAKE_SOURCE_DIR}/include") -target_link_libraries(${PLUGIN} PUBLIC "${OTAWA_LDFLAGS}" cudd_core cudd_epd cudd_st cudd_util extra) +target_link_libraries(${PLUGIN} PUBLIC "${OTAWA_LDFLAGS}" cudd extra) # installation set(PLUGIN_PATH "${OTAWA_PREFIX}/lib/otawa/${NAMESPACE}") install(TARGETS ${PLUGIN} LIBRARY DESTINATION ${PLUGIN_PATH}) install(DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/include/lruzdd" DESTINATION "${OTAWA_PREFIX}/include") install(FILES ${PLUGIN}.eld DESTINATION ${PLUGIN_PATH}) + diff --git a/cudd/CMakeLists.txt b/cudd/CMakeLists.txt index 6c05ef9367b3798cb678e600e454414cb218eab2..384b50b35fc0c649aff7afd7c060112e6347cb41 100644 --- a/cudd/CMakeLists.txt +++ b/cudd/CMakeLists.txt @@ -1,15 +1,13 @@ -set(CUDD_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/cudd-2.3.1/cudd/libcudd.a) -set(EPD_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/cudd-2.3.1/epd/libepd.a) -set(ST_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/cudd-2.3.1/st/libst.a) -set(UTIL_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/cudd-2.3.1/util/libutil.a) +set(CUDD_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/cudd/lib/libcudd.a) add_custom_command( OUTPUT ${CUDD_LIB_FILE} - COMMAND ${CMAKE_COMMAND} -E tar xzf ${CMAKE_CURRENT_SOURCE_DIR}/cudd-2.3.1.tar.gz - COMMAND patch -p0 -i ${CMAKE_CURRENT_SOURCE_DIR}/cudd-2.3.1.patch - COMMAND cd cudd-2.3.1 && rm -r include - COMMAND cd cudd-2.3.1 && ./setup.sh - COMMAND make -C cudd-2.3.1 + COMMAND rm -rf cudd + COMMAND git clone https://github.com/kozross/cudd + COMMAND cd cudd && autoreconf -i + COMMAND cd cudd && ./configure CC=${CMAKE_C_COMPILER} CFLAGS=-fPIC --prefix=${CMAKE_CURRENT_BINARY_DIR}/cudd + COMMAND make -C cudd + COMMAND make -C cudd install WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/ ) @@ -18,45 +16,24 @@ add_custom_target( DEPENDS ${CUDD_LIB_FILE} ) -#add_custom_target( -# compile_cudd -# COMMAND ${CMAKE_COMMAND} -E tar xzf ${CMAKE_CURRENT_SOURCE_DIR}/cudd-2.3.1.tar.gz -# COMMAND patch -p0 -i ${CMAKE_CURRENT_SOURCE_DIR}/cudd-2.3.1.patch -# COMMAND cd cudd-2.3.1 && rm -r include -# COMMAND cd cudd-2.3.1 && ./setup.sh -# COMMAND make -C cudd-2.3.1 -# WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/ -#) - -set(HEADERS_FOLDER ${CMAKE_CURRENT_BINARY_DIR}/cudd-2.3.1/include) -file(MAKE_DIRECTORY ${HEADERS_FOLDER}) - -add_library(cudd_core STATIC IMPORTED GLOBAL) -add_library(cudd_epd STATIC IMPORTED GLOBAL) -add_library(cudd_st STATIC IMPORTED GLOBAL) -add_library(cudd_util STATIC IMPORTED GLOBAL) - -set_target_properties(cudd_core - PROPERTIES - IMPORTED_LOCATION ${CUDD_LIB_FILE} - INTERFACE_INCLUDE_DIRECTORIES ${HEADERS_FOLDER} +#set(HEADERS_FOLDER ${CMAKE_CURRENT_BINARY_DIR}/cudd-2.3.1/include) +SET(CUDD_INCLUDE_DIR + "${CMAKE_CURRENT_BINARY_DIR}/cudd/cudd/" + "${CMAKE_CURRENT_BINARY_DIR}/cudd/st/" + "${CMAKE_CURRENT_BINARY_DIR}/cudd/epd/" + "${CMAKE_CURRENT_BINARY_DIR}/cudd/util/" + "${CMAKE_CURRENT_BINARY_DIR}/cudd/dddmp/" + "${CMAKE_CURRENT_BINARY_DIR}/cudd/mtr/" + "${CMAKE_CURRENT_BINARY_DIR}/cudd/nanotrav/" + "${CMAKE_CURRENT_BINARY_DIR}/cudd/" ) -set_target_properties(cudd_epd - PROPERTIES - IMPORTED_LOCATION ${EPD_LIB_FILE} - INTERFACE_INCLUDE_DIRECTORIES ${HEADERS_FOLDER} -) +file(MAKE_DIRECTORY ${CUDD_INCLUDE_DIR}) -set_target_properties(cudd_st - PROPERTIES - IMPORTED_LOCATION ${ST_LIB_FILE} - INTERFACE_INCLUDE_DIRECTORIES ${HEADERS_FOLDER} -) +add_library(cudd STATIC IMPORTED GLOBAL) -set_target_properties(cudd_util - PROPERTIES - IMPORTED_LOCATION ${UTIL_LIB_FILE} - INTERFACE_INCLUDE_DIRECTORIES ${HEADERS_FOLDER} +set_target_properties(cudd PROPERTIES + IMPORTED_LOCATION ${CUDD_LIB_FILE} + INTERFACE_INCLUDE_DIRECTORIES "${CUDD_INCLUDE_DIR}" ) diff --git a/cudd/cudd-2.3.1.patch b/cudd/cudd-2.3.1.patch deleted file mode 100644 index e8ff848fbe2064a35fedef5d05f4c3c133132b97..0000000000000000000000000000000000000000 --- a/cudd/cudd-2.3.1.patch +++ /dev/null @@ -1,76 +0,0 @@ -diff -r -c cudd-2.3.1/Makefile cudd-2.3.1/Makefile -*** cudd-2.3.1/Makefile 2001-05-18 02:54:26.000000000 +0200 ---- cudd-2.3.1/Makefile 2018-05-24 15:35:42.034516245 +0200 -*************** -*** 42,48 **** - #ICFLAGS = - # These two are typical settings for optimized code with gcc. - #ICFLAGS = -g -O6 -Wall -! ICFLAGS = -g -O6 - - # Use XCFLAGS to specify machine-dependent compilation flags. - # For some platforms no special flags are needed. ---- 42,49 ---- - #ICFLAGS = - # These two are typical settings for optimized code with gcc. - #ICFLAGS = -g -O6 -Wall -! #ICFLAGS = -g -O6 -! ICFLAGS = -g -O6 -fPIC - - # Use XCFLAGS to specify machine-dependent compilation flags. - # For some platforms no special flags are needed. -*************** -*** 52,58 **** - # Linux - # - # Gcc 2.8.1 or higher on i686. -! XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD - # - #========================== - # Solaris ---- 53,60 ---- - # Linux - # - # Gcc 2.8.1 or higher on i686. -! #XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD -! XCFLAGS = -malign-double -DHAVE_IEEE_754 -DBSD - # - #========================== - # Solaris -diff -r -c cudd-2.3.1/util/pipefork.c cudd-2.3.1/util/pipefork.c -*** cudd-2.3.1/util/pipefork.c 2001-03-19 11:59:06.000000000 +0100 ---- cudd-2.3.1/util/pipefork.c 2018-05-24 15:38:43.370514254 +0200 -*************** -*** 40,50 **** - int forkpid, waitPid; - int topipe[2], frompipe[2]; - char buffer[1024]; -- #if (defined __hpux) || (defined __osf__) || (defined _IBMR2) || (defined __SVR4) || (defined __CYGWIN32__) - int status; -- #else -- union wait status; -- #endif - - /* create the PIPES... - * fildes[0] for reading from command ---- 40,46 ---- -diff -r -c cudd-2.3.1/util/util.h cudd-2.3.1/util/util.h -*** cudd-2.3.1/util/util.h 2001-02-14 19:08:51.000000000 +0100 ---- cudd-2.3.1/util/util.h 2018-05-24 15:35:42.018516245 +0200 -*************** -*** 138,144 **** - /* most machines don't give us a header file for these */ - #if (defined(__STDC__) || defined(__cplusplus) || defined(ultrix)) && !defined(MNEMOSYNE) || defined(__SVR4) - # include -! EXTERN void free ARGS((void *)); - #else - # ifndef _IBMR2 - extern VOID_OR_INT abort(), exit(); ---- 138,144 ---- - /* most machines don't give us a header file for these */ - #if (defined(__STDC__) || defined(__cplusplus) || defined(ultrix)) && !defined(MNEMOSYNE) || defined(__SVR4) - # include -! /* EXTERN void free ARGS((void *)); */ - #else - # ifndef _IBMR2 - extern VOID_OR_INT abort(), exit(); diff --git a/cudd/cudd-2.3.1.tar.gz b/cudd/cudd-2.3.1.tar.gz deleted file mode 100644 index 2c5dbd5d42d96a41ae379e77609f6edda73f77a2..0000000000000000000000000000000000000000 Binary files a/cudd/cudd-2.3.1.tar.gz and /dev/null differ diff --git a/extra/CMakeLists.txt b/extra/CMakeLists.txt index f10b96f065c7bec803f081c511e2484f0c3f620e..70e9d48b93b85b4e96021cc2609bbdfcd453e245 100644 --- a/extra/CMakeLists.txt +++ b/extra/CMakeLists.txt @@ -1,30 +1,23 @@ -set(EXTRA_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/extra20/libextra.a) -add_custom_command( - OUTPUT ${EXTRA_LIB_FILE} - COMMAND ${CMAKE_COMMAND} -E tar xzf ${CMAKE_CURRENT_SOURCE_DIR}/extra20a.tar.gz - COMMAND patch -p0 -i ${CMAKE_CURRENT_SOURCE_DIR}/extra20.patch - COMMAND make -C extra20 - WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/ +add_library(extra STATIC + src/maxDotProduct.c + src/maxUnion.c + src/minDotProduct.c + src/minUnion.c + src/notSubSet.c + src/notSupSet.c + src/emptyBelongs.c ) -add_custom_target( - libextra - DEPENDS ${EXTRA_LIB_FILE} +set_target_properties(extra + PROPERTIES + PUBLIC_HEADER extra.h + POSITION_INDEPENDENT_CODE ON ) +target_link_libraries(extra cudd) -add_dependencies(libextra libcudd) - -set(HEADERS_FOLDER ${CMAKE_CURRENT_BINARY_DIR}/extra20/) -file(MAKE_DIRECTORY ${HEADERS_FOLDER}) - -set(EXTRA_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/extra20/libextra.a) +target_include_directories(extra PUBLIC include) -add_library(extra STATIC IMPORTED GLOBAL) +add_dependencies(extra libcudd) -set_target_properties(extra - PROPERTIES - IMPORTED_LOCATION ${EXTRA_LIB_FILE} - INTERFACE_INCLUDE_DIRECTORIES ${HEADERS_FOLDER} -) diff --git a/extra/README b/extra/README new file mode 100644 index 0000000000000000000000000000000000000000..7e9be889a2466b792a20468169dd4e2c4c95b834 --- /dev/null +++ b/extra/README @@ -0,0 +1 @@ +Most of the code in this directory was taken from the extra library of Alan Mishchenko. diff --git a/extra/extra20.patch b/extra/extra20.patch deleted file mode 100644 index 7ad3faf8029db1df4bc416d62e288a5c4d7c2e1a..0000000000000000000000000000000000000000 --- a/extra/extra20.patch +++ /dev/null @@ -1,40 +0,0 @@ -diff -r -c extra20/Makefile extra20/Makefile -*** extra20/Makefile 2003-10-11 12:25:38.000000000 +0200 ---- extra20/Makefile 2018-05-04 16:25:52.535788756 +0200 -*************** -*** 4,11 **** - .SILENT: - - # modify these macros to point to your include and lib directory -! INCDIR = /u/alanmi/local/include/ -! LIBDIR = /u/alanmi/local/lib/ - - # modify this line to compile with compilers other than g++ - CC = gcc ---- 4,11 ---- - .SILENT: - - # modify these macros to point to your include and lib directory -! INCDIR = ../../cudd/cudd-2.3.1/include/ -! LIBDIR = /tmp/ - - # modify this line to compile with compilers other than g++ - CC = gcc -*************** -*** 25,31 **** - #CFLAGS = -c -O -D_UNIX -D_HP_ - - # these are compiler flags for SunOS -! CFLAGS = -c -O -D_UNIX - - #LFLAGS = -pg -Wall - LFLAGS = ---- 25,32 ---- - #CFLAGS = -c -O -D_UNIX -D_HP_ - - # these are compiler flags for SunOS -! #CFLAGS = -c -O -D_UNIX -! CFLAGS = -c -O -D_UNIX -fPIC - - #LFLAGS = -pg -Wall - LFLAGS = diff --git a/extra/extra20a.tar.gz b/extra/extra20a.tar.gz deleted file mode 100644 index b5b2ac4f852f42147b36bf2d35b94f771bbe961c..0000000000000000000000000000000000000000 Binary files a/extra/extra20a.tar.gz and /dev/null differ diff --git a/extra/include/extra.h b/extra/include/extra.h new file mode 100644 index 0000000000000000000000000000000000000000..00daf0b9dcbeb50305ee882723ddd09296fb0dbb --- /dev/null +++ b/extra/include/extra.h @@ -0,0 +1,26 @@ +#ifndef EXTRA_H +#define EXTRA_H + +#include +#include +#include + +extern int Extra_zddEmptyBelongs( DdManager *dd, DdNode* zS ); + +extern DdNode * Extra_zddMaxUnion( DdManager *dd, DdNode * S, DdNode * T ); +extern DdNode * extraZddMaxUnion( DdManager *dd, DdNode * S, DdNode * T ); +extern DdNode * Extra_zddMinUnion( DdManager *dd, DdNode * S, DdNode * T ); +extern DdNode * extraZddMinUnion( DdManager *dd, DdNode * S, DdNode * T ); + +extern DdNode * Extra_zddMaxDotProduct( DdManager *dd, DdNode * S, DdNode * T ); +extern DdNode * extraZddMaxDotProduct( DdManager *dd, DdNode * S, DdNode * T ); +extern DdNode * Extra_zddMinDotProduct( DdManager *dd, DdNode * S, DdNode * T ); +extern DdNode * extraZddMinDotProduct( DdManager *dd, DdNode * S, DdNode * T ); + +extern DdNode * Extra_zddNotSubSet( DdManager *dd, DdNode * X, DdNode * Y ); +extern DdNode * extraZddNotSubSet( DdManager *dd, DdNode * X, DdNode * Y ); +extern DdNode * Extra_zddNotSupSet( DdManager *dd, DdNode * X, DdNode * Y ); +extern DdNode * extraZddNotSupSet( DdManager *dd, DdNode * X, DdNode * Y ); + +#endif // EXTRA_H + diff --git a/extra/src/emptyBelongs.c b/extra/src/emptyBelongs.c new file mode 100644 index 0000000000000000000000000000000000000000..e65177bd77ef53362c0e9df332195dc56d972484 --- /dev/null +++ b/extra/src/emptyBelongs.c @@ -0,0 +1,14 @@ +#include + +int +Extra_zddEmptyBelongs( + DdManager *dd, + DdNode* zS ) +{ + while ( zS->index != CUDD_MAXINDEX ) + zS = cuddE( zS ); + return (int)( zS == DD_ONE(dd) ); + +} /* end of Extra_zddEmptyBelongs */ + + diff --git a/extra/src/maxDotProduct.c b/extra/src/maxDotProduct.c new file mode 100644 index 0000000000000000000000000000000000000000..82a87568e36ce2207f5018942a5ef7ed53b4f379 --- /dev/null +++ b/extra/src/maxDotProduct.c @@ -0,0 +1,166 @@ +#include + +/**Function******************************************************************** + + Synopsis [Computes the maximal of the DotProduct of the union of two sets represented by ZDDs.] + + Description [This procedure assumes that the arguments are already + maximal.] + + SideEffects [] + + SeeAlso [Extra_zddDotProduct Extra_zddMaximal Extra_zddMinCrossProduct] + +******************************************************************************/ +DdNode * +Extra_zddMaxDotProduct( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddMaxDotProduct(dd, S, T); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddMaxDotProduct */ + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddMaxDotProduct.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddMaxDotProduct( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *zRes; + int TopS, TopT; + statLine(dd); + + /* consider terminal cases */ + if ( S == DD_ZERO(dd) || T == DD_ZERO(dd) ) + return DD_ZERO(dd); + if ( S == DD_ONE(dd) ) + return T; + if ( T == DD_ONE(dd) ) + return S; + + /* the operation is commutative - normalize the problem */ + TopS = dd->permZ[S->index]; + TopT = dd->permZ[T->index]; + + if ( TopS > TopT || (TopS == TopT && (unsigned)S > (unsigned)T) ) + return extraZddMaxDotProduct(dd, T, S); + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddMaxDotProduct, S, T); + if (zRes) + return zRes; + else + { + DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp; + if ( TopS == TopT ) + { + /* compute the union of two cofactors of T (T0+T1) */ + zTemp = extraZddMaxUnion(dd, cuddE(T), cuddT(T) ); + if ( zTemp == NULL ) + return NULL; + cuddRef( zTemp ); + + /* compute MaxDotProduct with the top element for subsets (S1, T0+T1) */ + zSet0 = extraZddMaxDotProduct(dd, cuddT(S), zTemp ); + if ( zSet0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zTemp); + return NULL; + } + cuddRef( zSet0 ); + Cudd_RecursiveDerefZdd(dd, zTemp); + + /* compute MaxDotProduct with the top element for subsets (S0, T1) */ + zSet1 = extraZddMaxDotProduct(dd, cuddE(S), cuddT(T) ); + if ( zSet1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + return NULL; + } + cuddRef( zSet1 ); + + /* compute the union of these two partial results (zSet0 + zSet1) */ + zRes1 = extraZddMaxUnion(dd, zSet0, zSet1 ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + + /* compute MaxDotProduct for subsets without the top-most element */ + zRes0 = extraZddMaxDotProduct(dd, cuddE(S), cuddE(T) ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddRef( zRes0 ); + } + else /* if ( TopS < TopT ) */ + { + /* compute MaxDotProduct with the top element for subsets (S1, T) */ + zRes1 = extraZddMaxDotProduct(dd, cuddT(S), T ); + if ( zRes1 == NULL ) + return NULL; + cuddRef( zRes1 ); + + /* compute MaxDotProduct for subsets without the top-most element */ + zRes0 = extraZddMaxDotProduct(dd, cuddE(S), T ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddRef( zRes0 ); + } + + /* remove subsets without this element covered by subsets with this element */ + zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zTemp); + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddRef( zRes0 ); + Cudd_RecursiveDerefZdd(dd, zTemp); + + /* create the new node */ + zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddMaxDotProduct, S, T, zRes); + return zRes; + } +} /* end of extraZddMaxDotProduct */ + diff --git a/extra/src/maxUnion.c b/extra/src/maxUnion.c new file mode 100644 index 0000000000000000000000000000000000000000..4b4a37501079e5ae1d51c991d297ca3d24d78b0c --- /dev/null +++ b/extra/src/maxUnion.c @@ -0,0 +1,141 @@ +#include + +/**Function******************************************************************** + + Synopsis [Computes the maximal of the union of two sets represented by ZDDs.] + + Description [This procedure assumes that the arguments are already + maximal. This is why Maximal(X) is not computed in the bottom cases + MaxUnion(X, {}) = MaxUnion({}, X) = Maximal(X), and X is returned.] + + SideEffects [] + + SeeAlso [Extra_zddMaximal Extra_zddMimimal Extra_zddMinUnion] + +******************************************************************************/ + +DdNode * +Extra_zddMaxUnion( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddMaxUnion(dd, S, T); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddMaxUnion */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddMaxUnion.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddMaxUnion( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *zRes; + int TopS, TopT; + statLine(dd); + + /* consider terminal cases */ + if ( S == DD_ZERO(dd) ) + return T; + if ( T == DD_ZERO(dd) ) + return S; + if ( S == T ) + return S; + if ( S == DD_ONE(dd) ) + return T; + if ( T == DD_ONE(dd) ) + return S; + + /* the operation is commutative - normalize the problem */ + TopS = dd->permZ[S->index]; + TopT = dd->permZ[T->index]; + + if ( TopS > TopT || (TopS == TopT && (unsigned)S > (unsigned)T) ) + return extraZddMaxUnion(dd, T, S); + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddMaxUnion, S, T); + if (zRes) + return zRes; + else + { + DdNode *zSet0, *zSet1, *zRes0, *zRes1; + + if ( TopS == TopT ) + { + /* compute maximal for subsets without the top-most element */ + zSet0 = extraZddMaxUnion(dd, cuddE(S), cuddE(T) ); + if ( zSet0 == NULL ) + return NULL; + cuddRef( zSet0 ); + + /* compute maximal for subsets with the top-most element */ + zSet1 = extraZddMaxUnion(dd, cuddT(S), cuddT(T) ); + if ( zSet1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + return NULL; + } + cuddRef( zSet1 ); + } + else /* if ( TopS < TopT ) */ + { + /* compute maximal for subsets without the top-most element */ + zSet0 = extraZddMaxUnion(dd, cuddE(S), T ); + if ( zSet0 == NULL ) + return NULL; + cuddRef( zSet0 ); + + /* subset with this element is just the cofactor of S */ + zSet1 = cuddT(S); + cuddRef( zSet1 ); + } + + /* remove subsets without this element covered by subsets with this element */ + zRes0 = extraZddNotSubSet(dd, zSet0, zSet1); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + return NULL; + } + cuddRef( zRes0 ); + Cudd_RecursiveDerefZdd(dd, zSet0); + + /* subset with this element remains unchanged */ + zRes1 = zSet1; + + /* create the new node */ + zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddMaxUnion, S, T, zRes); + return zRes; + } +} /* end of extraZddMaxUnion */ + diff --git a/extra/src/minDotProduct.c b/extra/src/minDotProduct.c new file mode 100644 index 0000000000000000000000000000000000000000..79953a268f2f9fe96b3bb1d62b64a8b257705b8b --- /dev/null +++ b/extra/src/minDotProduct.c @@ -0,0 +1,142 @@ +#include + +DdNode *Extra_zddMinDotProduct( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddMinDotProduct(dd, S, T); + } while (dd->reordered == 1); + return(res); + +} /* end of zddMinDotProduct */ + +DdNode * +extraZddMinDotProduct( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *zRes; + int TopS, TopT; + statLine(dd); + + /* consider terminal cases */ + if ( S == DD_ZERO(dd) || T == DD_ZERO(dd) ) + return DD_ZERO(dd); + if ( S == DD_ONE(dd) ) + return T; + if ( T == DD_ONE(dd) ) + return S; + + /* the operation is commutative - normalize the problem */ + TopS = dd->permZ[S->index]; + TopT = dd->permZ[T->index]; + + if ( TopS > TopT || (TopS == TopT && (unsigned long)S > (unsigned long)T) ) + return extraZddMinDotProduct(dd, T, S); + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddMinDotProduct, S, T); + if (zRes) + return zRes; + else + { + DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp; + if ( TopS == TopT ) + { + /* compute the union of two cofactors of T (T0+T1) */ + zTemp = extraZddMinUnion(dd, cuddE(T), cuddT(T) ); + if ( zTemp == NULL ) + return NULL; + cuddRef( zTemp ); + + /* compute MinDotProduct with the top element for subsets (S1, T0+T1) */ + zSet0 = extraZddMinDotProduct(dd, cuddT(S), zTemp ); + if ( zSet0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zTemp); + return NULL; + } + cuddRef( zSet0 ); + Cudd_RecursiveDerefZdd(dd, zTemp); + + /* compute MinDotProduct with the top element for subsets (S0, T1) */ + zSet1 = extraZddMinDotProduct(dd, cuddE(S), cuddT(T) ); + if ( zSet1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + return NULL; + } + cuddRef( zSet1 ); + + /* compute the union of these two partial results (zSet0 + zSet1) */ + zRes1 = extraZddMinUnion(dd, zSet0, zSet1 ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + + /* compute MinDotProduct for subsets without the top-most element */ + zRes0 = extraZddMinDotProduct(dd, cuddE(S), cuddE(T) ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddRef( zRes0 ); + } + else /* if ( TopS < TopT ) */ + { + /* compute MinDotProduct with the top element for subsets (S1, T) */ + zRes1 = extraZddMinDotProduct(dd, cuddT(S), T ); + if ( zRes1 == NULL ) + return NULL; + cuddRef( zRes1 ); + + /* compute MinDotProduct for subsets without the top-most element */ + zRes0 = extraZddMinDotProduct(dd, cuddE(S), T ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddRef( zRes0 ); + } + + /* remove subsets with this element covering subsets without this element */ + zRes1 = extraZddNotSupSet(dd, zTemp = zRes1, zRes0); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zTemp); + Cudd_RecursiveDerefZdd(dd, zRes0); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd(dd, zTemp); + + /* create the new node */ + zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddMinDotProduct, S, T, zRes); + return zRes; + } +} /* end of extraZddMinDotProduct */ + diff --git a/extra/src/minUnion.c b/extra/src/minUnion.c new file mode 100644 index 0000000000000000000000000000000000000000..dee51023be4d41e87dad48c917067fdfe43e6ff5 --- /dev/null +++ b/extra/src/minUnion.c @@ -0,0 +1,136 @@ +#include + +/**Function******************************************************************** + + Synopsis [Computes the minimal of the union of two sets represented by ZDDs.] + + Description [This procedure assumes that the arguments are already + minimal.] + + SideEffects [] + + SeeAlso [Extra_zddMaximal Extra_zddMimimal Extra_zddMaxUnion] + +******************************************************************************/ +DdNode * +Extra_zddMinUnion( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddMinUnion(dd, S, T); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddMinUnion */ + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddMinUnion.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddMinUnion( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *zRes; + int TopS, TopT; + statLine(dd); + + /* consider terminal cases */ + if ( S == DD_ZERO(dd) ) + return T; + if ( T == DD_ZERO(dd) ) + return S; + if ( S == T ) + return S; + /* the empty combination, if present, is the only minimal combination */ + if ( Extra_zddEmptyBelongs(dd, S) || Extra_zddEmptyBelongs(dd, T) ) + return DD_ONE(dd); + + /* the operation is commutative - normalize the problem */ + TopS = dd->permZ[S->index]; + TopT = dd->permZ[T->index]; + + if ( TopS > TopT || (TopS == TopT && (unsigned)S > (unsigned)T) ) + return extraZddMinUnion(dd, T, S); + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddMinUnion, S, T); + if (zRes) + return(zRes); + else + { + DdNode *zSet0, *zSet1, *zRes0, *zRes1; + if ( TopS == TopT ) + { + /* compute maximal for subsets without the top-most element */ + zSet0 = extraZddMinUnion(dd, cuddE(S), cuddE(T) ); + if ( zSet0 == NULL ) + return NULL; + cuddRef( zSet0 ); + + /* compute maximal for subsets with the top-most element */ + zSet1 = extraZddMinUnion(dd, cuddT(S), cuddT(T) ); + if ( zSet1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + return NULL; + } + cuddRef( zSet1 ); + } + else /* if ( TopS < TopT ) */ + { + /* compute maximal for subsets without the top-most element */ + zSet0 = extraZddMinUnion(dd, cuddE(S), T ); + if ( zSet0 == NULL ) + return NULL; + cuddRef( zSet0 ); + + /* subset with this element is just the cofactor of S */ + zSet1 = cuddT(S); + cuddRef( zSet1 ); + } + + /* subset without this element remains unchanged */ + zRes0 = zSet0; + + /* remove subsets with this element that contain subsets without this element */ + zRes1 = extraZddNotSupSet(dd, zSet1, zSet0); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd(dd, zSet1); + + /* create the new node */ + zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddMinUnion, S, T, zRes); + return zRes; + } +} /* end of extraZddMinUnion */ + diff --git a/extra/src/notSubSet.c b/extra/src/notSubSet.c new file mode 100644 index 0000000000000000000000000000000000000000..dab87a3f4b0fdf192cc1fb8d8ef3a6dbe9debe21 --- /dev/null +++ b/extra/src/notSubSet.c @@ -0,0 +1,159 @@ +#include + +/**Function******************************************************************** + + Synopsis [Computes subsets in X that are not contained in any of the subsets of Y.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_zddSubSet, Extra_zddSupSet, Extra_zddNotSupSet] + +******************************************************************************/ +DdNode * +Extra_zddNotSubSet( + DdManager * dd, + DdNode * X, + DdNode * Y) +{ + DdNode *res; + int autoDynZ; + + autoDynZ = dd->autoDynZ; + dd->autoDynZ = 0; + + do { + dd->reordered = 0; + res = extraZddNotSubSet(dd, X, Y); + } while (dd->reordered == 1); + dd->autoDynZ = autoDynZ; + return(res); + +} /* end of Extra_zddNotSubSet */ + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddNotSubSet.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode* extraZddNotSubSet( DdManager *dd, DdNode *X, DdNode *Y ) +{ + DdNode *zRes; + statLine(dd); + /* any comb is a subset of itself */ + if ( X == Y ) + return DD_ZERO(dd); + /* combs in X are notsubsets of non-existant combs in Y */ + if ( Y == DD_ZERO(dd) ) + return X; + /* only {()} is the subset of {()} */ + if ( Y == DD_ONE(dd) ) /* remove empty combination from X */ + return cuddZddDiff( dd, X, DD_ONE(dd) ); + /* if X is empty, the result is empty */ + if ( X == DD_ZERO(dd) ) + return DD_ZERO(dd); + /* the empty comb is contained in all combs of Y */ + if ( X == DD_ONE(dd) ) + return DD_ZERO(dd); + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddNotSubSet, X, Y); + if (zRes) + return(zRes); + else + { + DdNode *zRes0, *zRes1, *zTemp; + int TopLevelX = dd->permZ[ X->index ]; + int TopLevelY = dd->permZ[ Y->index ]; + + if ( TopLevelX < TopLevelY ) + { + /* compute combs of X without var that are notsubsets of combs with Y */ + zRes0 = extraZddNotSubSet( dd, cuddE( X ), Y ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + /* combs of X with var cannot be subsets of combs without var in Y */ + zRes1 = cuddT( X ); + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddDeref( zRes0 ); + } + else if ( TopLevelX == TopLevelY ) + { + /* merge combs of Y with and without var */ + zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) ); + if ( zTemp == NULL ) + return NULL; + cuddRef( zTemp ); + + /* compute combs of X without var that are notsubsets of combs is Temp */ + zRes0 = extraZddNotSubSet( dd, cuddE( X ), zTemp ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + return NULL; + } + cuddRef( zRes0 ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + + /* combs of X with var that are notsubsets of combs in Y with var */ + zRes1 = extraZddNotSubSet( dd, cuddT( X ), cuddT( Y ) ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + else /* if ( TopLevelX > TopLevelY ) */ + { + /* merge combs of Y with and without var */ + zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) ); + if ( zTemp == NULL ) + return NULL; + cuddRef( zTemp ); + + /* compute combs that are notsubsets of Temp */ + zRes = extraZddNotSubSet( dd, X, zTemp ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + cuddDeref( zRes ); + } + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddNotSubSet, X, Y, zRes); + return zRes; + } +} /* end of extraZddNotSubSet */ + diff --git a/extra/src/notSupSet.c b/extra/src/notSupSet.c new file mode 100644 index 0000000000000000000000000000000000000000..95ce627aa122304be4e31afbafc75c270ccd61db --- /dev/null +++ b/extra/src/notSupSet.c @@ -0,0 +1,155 @@ +#include + +/**Function******************************************************************** + + Synopsis [Computes subsets in X that do not contain any of the subsets of Y.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_zddSubSet, Extra_zddSupSet, Extra_zddNotSubSet] + +******************************************************************************/ +DdNode * +Extra_zddNotSupSet( + DdManager * dd, + DdNode * X, + DdNode * Y) +{ + DdNode *res; + int autoDynZ; + + autoDynZ = dd->autoDynZ; + dd->autoDynZ = 0; + + do { + dd->reordered = 0; + res = extraZddNotSupSet(dd, X, Y); + } while (dd->reordered == 1); + dd->autoDynZ = autoDynZ; + return(res); + +} /* end of Extra_zddNotSupSet */ + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddNotSupSet.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode* extraZddNotSupSet( DdManager *dd, DdNode *X, DdNode *Y ) +{ + DdNode *zRes; + statLine(dd); + /* any comb is a superset of itself */ + if ( X == Y ) + return DD_ZERO(dd); + /* no comb in X is superset of non-existing combs */ + if ( Y == DD_ZERO(dd) ) + return X; + /* any comb in X is the superset of the empty comb */ + if ( Extra_zddEmptyBelongs( dd, Y ) ) + return DD_ZERO(dd); + /* if X is empty, the result is empty */ + if ( X == DD_ZERO(dd) ) + return DD_ZERO(dd); + /* if X is the empty comb (and Y does not contain it!), return it */ + if ( X == DD_ONE(dd) ) + return DD_ONE(dd); + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddNotSupSet, X, Y); + if (zRes) + return(zRes); + else + { + DdNode *zRes0, *zRes1, *zTemp; + int TopLevelX = dd->permZ[ X->index ]; + int TopLevelY = dd->permZ[ Y->index ]; + + if ( TopLevelX < TopLevelY ) + { + /* combinations of X without label that are supersets of combinations of Y */ + zRes0 = extraZddNotSupSet( dd, cuddE( X ), Y ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + /* combinations of X with label that are supersets of combinations of Y */ + zRes1 = extraZddNotSupSet( dd, cuddT( X ), Y ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + else if ( TopLevelX == TopLevelY ) + { + /* combs of X without var that are not supersets of combs of Y without var */ + zRes0 = extraZddNotSupSet( dd, cuddE( X ), cuddE( Y ) ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + /* merge combs of Y with and without var */ + zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) ); + if ( zTemp == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zTemp ); + + /* combs of X with label that are supersets of combs in Temp */ + zRes1 = extraZddNotSupSet( dd, cuddT( X ), zTemp ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + else /* if ( TopLevelX > TopLevelY ) */ + { + /* combs of X that are supersets of combs of Y without label */ + zRes = extraZddNotSupSet( dd, X, cuddE( Y ) ); + if ( zRes == NULL ) return NULL; + } + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddNotSupSet, X, Y, zRes); + return zRes; + } +} /* end of extraZddNotSupSet */ + diff --git a/lruzdd.eld b/lruzdd.eld index a0b414667acabd9d3d4069193f06134b1fbcc7c8..4b7b0961bea14679bfbb9e953d7381711a954d36 100644 --- a/lruzdd.eld +++ b/lruzdd.eld @@ -1,5 +1,5 @@ [elm-plugin] name=lruzdd -deps=otawa/icat3;otawalru;lrumc +deps=otawa/icat3;lrupreanalysis;lruexact description=Perform an exact May/Must analysis of L1 I cache author=Valentin Touzeau diff --git a/src/ClassificationBuilder.cpp b/src/ClassificationBuilder.cpp index 839795948128398e3610ac212cbcfe0c8d38ebc3..131e285fedfd6ca3684c3dfdbabfeaae4886b160 100644 --- a/src/ClassificationBuilder.cpp +++ b/src/ClassificationBuilder.cpp @@ -4,7 +4,7 @@ #include #include -#include +#include using namespace otawa; @@ -29,7 +29,7 @@ protected: BasicBlock* bb = b->toBasic(); - for(Block::EdgeIter edgeIter(bb->ins()); edgeIter; ++edgeIter) { + for(Block::EdgeIter edgeIter(bb->ins()); edgeIter(); ++edgeIter) { Edge* e = *edgeIter; Bag& bag = icache::ACCESSES(e).ref(); processBag(bag); @@ -53,11 +53,11 @@ protected: ASSERT((hCat != HitCategory::AH || mCat != MissCategory::AM) && "Access cannot be AH and AM"); if(hCat == HitCategory::AH) - otawalru::EXACT_CATEGORY(access) = otawalru::ExactCategory::AH; + lruexact::EXACT_CATEGORY(access) = lruexact::ExactCategory::AH; else if(mCat == MissCategory::AM) - otawalru::EXACT_CATEGORY(access) = otawalru::ExactCategory::AM; + lruexact::EXACT_CATEGORY(access) = lruexact::ExactCategory::AM; else - otawalru::EXACT_CATEGORY(access) = otawalru::ExactCategory::DU; + lruexact::EXACT_CATEGORY(access) = lruexact::ExactCategory::DU; } }; @@ -65,7 +65,7 @@ p::declare ClassificationBuilder::reg = p::init("lruzdd::ClassificationBuilder", .require(icache::ACCESSES_FEATURE) .require(EXACT_MAY_ANALYSIS_FEATURE) .require(EXACT_MUST_ANALYSIS_FEATURE) - .provide(otawalru::LRU_CLASSIFICATION_FEATURE) + .provide(lruexact::LRU_CLASSIFICATION_FEATURE) .make(); } // namespace lruzdd diff --git a/src/MayAnalysis/GlobalMayAnalysis.cpp b/src/MayAnalysis/GlobalMayAnalysis.cpp index 8e4b3f0df43ce8696c28776daf1f28d21bf2e16a..8620e74de04659f934bd72f1ce7a6a34354c7aea 100644 --- a/src/MayAnalysis/GlobalMayAnalysis.cpp +++ b/src/MayAnalysis/GlobalMayAnalysis.cpp @@ -29,7 +29,6 @@ #include #include #include -#include #include "../ZDD/ZDDManager.h" #include "../ZDD/MayAbstractValuePolicy.h" #include "../ZDD/ZDDMayDomainPolicy.h" @@ -67,8 +66,8 @@ public: inline store_t& store(void) { return m_store; } void update(const Bag& accs, t& d) { - for(auto acc = *accs; acc; acc++) - m_domain.update(acc, d); + for(auto acc = *accs; acc(); acc++) + m_domain.update(*acc, d); } void update(Block* v, t& d) { @@ -77,7 +76,7 @@ public: t s; // update and join along edges - for(auto e = m_graph.preds(v); e; e++) { + for(auto e = m_graph.preds(v); e(); e++) { Block *w = e->source(); m_domain.copy(s, m_store.get(w)); @@ -90,7 +89,7 @@ public: // apply edge { - const Bag& accs = icache::ACCESSES(e); + const Bag& accs = icache::ACCESSES(*e); if(accs.count() > 0) update(accs, s); } @@ -155,9 +154,9 @@ protected: } auto end = std::chrono::system_clock::now(); - auto elapsed = std::chrono::duration_cast(end - start); + auto elapsed = std::chrono::duration_cast(end - start); if(logFor(LOG_FUN)) - log << "\tExact Global May Analysis running time: " << elapsed.count() << " s" << io::endl; + log << "\tExact Global May Analysis running time: " << elapsed.count() << " ms" << io::endl; // for(int i = 0; i < m_coll->size(); ++i) { // const icat3::LBlockSet& s = (*m_coll)[i]; @@ -193,8 +192,8 @@ private: ai::SimpleAI ana(ada); ana.run(); - for(CFGCollection::BlockIter b(m_cfgs); b; b++) - classifyBlock(lb, ada.domain(), b, ada.store().get(b)); + for(CFGCollection::BlockIter b(m_cfgs); b(); b++) + classifyBlock(lb, ada.domain(), *b, ada.store().get(*b)); //ada.store().clear(); } @@ -208,8 +207,8 @@ private: Bag& bAccs = icache::ACCESSES(b).ref(); GlobalMayAdapter::t save = classifyAccesses(b, focus, man, bAccs); - for(Block::EdgeIter e = b->outs(); e; e++) { - Bag& eAccs = icache::ACCESSES(e).ref(); + for(Block::EdgeIter e = b->outs(); e(); e++) { + Bag& eAccs = icache::ACCESSES(*e).ref(); man.restart(save); classifyAccesses(b, focus, man, eAccs); } diff --git a/src/MayAnalysis/MayAnalysis.cpp b/src/MayAnalysis/MayAnalysis.cpp index 9156c0c9dc233773666a3d7ef9bd8a8a52b3a91e..2e5ac2962e0929920e7c626239d87cbf0bf2bc8a 100644 --- a/src/MayAnalysis/MayAnalysis.cpp +++ b/src/MayAnalysis/MayAnalysis.cpp @@ -29,7 +29,7 @@ #include #include #include -#include +#include #include "../ZDD/MayAbstractValuePolicy.h" #include "../ZDD/ZDDMayDomainPolicy.h" #include "../GeneratorsSet/GSMayAbstractValuePolicy.h" @@ -65,8 +65,8 @@ public: inline store_t& store(void) { return m_store; } void update(const Bag& accs, t& d) { - for(auto acc = *accs; acc; acc++) - m_domain.update(acc, d); + for(auto acc = *accs; acc(); acc++) + m_domain.update(*acc, d); } void update(Block* v, t& d) { @@ -75,7 +75,7 @@ public: t s; // update and join along edges - for(auto e = m_graph.preds(v); e; e++) { + for(auto e = m_graph.preds(v); e(); e++) { Block *w = e->source(); m_domain.copy(s, m_store.get(w)); @@ -88,7 +88,7 @@ public: // apply edge { - const Bag& accs = icache::ACCESSES(e); + const Bag& accs = icache::ACCESSES(*e); if(accs.count() > 0) update(accs, s); } @@ -145,13 +145,13 @@ protected: auto start = std::chrono::system_clock::now(); std::set toRefine; - for(CFGCollection::BlockIter b(m_cfgs); b; b++) { + for(CFGCollection::BlockIter b(m_cfgs); b(); b++) { if(!b->isBasic()) continue; BasicBlock* bb = b->toBasic(); - for(Block::EdgeIter edgeIter(bb->ins()); edgeIter; ++edgeIter) { + for(Block::EdgeIter edgeIter(bb->ins()); edgeIter(); ++edgeIter) { Edge* e = *edgeIter; Bag& bag = icache::ACCESSES(e).ref(); processBag(toRefine, bag); @@ -164,9 +164,9 @@ protected: processLBlock(lb); auto end = std::chrono::system_clock::now(); - auto elapsed = std::chrono::duration_cast(end - start); + auto elapsed = std::chrono::duration_cast(end - start); if(logFor(LOG_FUN)) - log << "\tExact May Analysis running time: " << elapsed.count() << " s" << io::endl; + log << "\tExact May Analysis running time: " << elapsed.count() << " ms" << io::endl; // for(int i = 0; i < m_coll->size(); ++i) { // const icat3::LBlockSet& s = (*m_coll)[i]; @@ -185,17 +185,17 @@ private: void processBag(std::set& set, Bag& bag) { for(int i = 0; i < bag.size(); ++i) { - lrumc::RefinementCategory refCat = lrumc::REFINEMENT_CATEGORY(bag[i]); + lruexact::RefinementCategory refCat = lruexact::REFINEMENT_CATEGORY(bag[i]); MissCategory e = MissCategory::NC; - if(refCat == lrumc::RefinementCategory::CLASSIFIED && + if(refCat == lruexact::RefinementCategory::CLASSIFIED && icat3::CATEGORY(bag[i]) == icat3::AM) e = MissCategory::AM; MISS_CATEGORY(bag[i]) = e; - if(refCat == lrumc::RefinementCategory::AM_CANDIDATE || - refCat == lrumc::RefinementCategory::AH_AM_CANDIDATE) + if(refCat == lruexact::RefinementCategory::AM_CANDIDATE || + refCat == lruexact::RefinementCategory::AH_AM_CANDIDATE) set.insert(icat3::LBLOCK(&bag[i])); } } @@ -209,8 +209,8 @@ private: ai::SimpleAI ana(ada); ana.run(); - for(CFGCollection::BlockIter b(m_cfgs); b; b++) - classifyBlock(lb, ada.domain(), b, ada.store().get(b)); + for(CFGCollection::BlockIter b(m_cfgs); b(); b++) + classifyBlock(lb, ada.domain(), *b, ada.store().get(*b)); ada.store().clear(); } @@ -224,8 +224,8 @@ private: Bag& bAccs = icache::ACCESSES(b).ref(); MayAdapter::t save = classifyAccesses(b, focus, man, bAccs); - for(Block::EdgeIter e = b->outs(); e; e++) { - Bag& eAccs = icache::ACCESSES(e).ref(); + for(Block::EdgeIter e = b->outs(); e(); e++) { + Bag& eAccs = icache::ACCESSES(*e).ref(); man.restart(save); classifyAccesses(b, focus, man, eAccs); } @@ -267,7 +267,7 @@ private: p::declare MayAnalysis::reg = p::init("lruzdd::MayAnalysis", Version(1, 0, 0)) .require(icat3::LBLOCKS_FEATURE) - .require(lrumc::REFINEMENT_CATEGORY_FEATURE) + .require(lruexact::REFINEMENT_CATEGORY_FEATURE) .require(COLLECTED_CFG_FEATURE) .provide(EXACT_MAY_ANALYSIS_FEATURE) .make(); diff --git a/src/MustAnalysis/GlobalMustAnalysis.cpp b/src/MustAnalysis/GlobalMustAnalysis.cpp index c90be5de5b55941b507a21f1c14fd797bdc9e2a9..cd63cce25bc58604022011ee8d4b2f96413db392 100644 --- a/src/MustAnalysis/GlobalMustAnalysis.cpp +++ b/src/MustAnalysis/GlobalMustAnalysis.cpp @@ -29,7 +29,6 @@ #include #include #include -#include #include "../ZDD/ZDDManager.h" #include "../ZDD/MustAbstractValuePolicy.h" #include "../ZDD/ZDDMustDomainPolicy.h" @@ -67,8 +66,8 @@ public: inline store_t& store(void) { return m_store; } void update(const Bag& accs, t& d) { - for(auto acc = *accs; acc; acc++) - m_domain.update(acc, d); + for(auto acc = *accs; acc(); acc++) + m_domain.update(*acc, d); } void update(Block* v, t& d) { @@ -77,7 +76,7 @@ public: t s; // update and join along edges - for(auto e = m_graph.preds(v); e; e++) { + for(auto e = m_graph.preds(v); e(); e++) { Block *w = e->source(); m_domain.copy(s, m_store.get(w)); @@ -90,7 +89,7 @@ public: // apply edge { - const Bag& accs = icache::ACCESSES(e); + const Bag& accs = icache::ACCESSES(*e); if(accs.count() > 0) update(accs, s); } @@ -155,9 +154,9 @@ protected: } auto end = std::chrono::system_clock::now(); - auto elapsed = std::chrono::duration_cast(end - start); + auto elapsed = std::chrono::duration_cast(end - start); if(logFor(LOG_FUN)) - log << "\tExact Global Must Analysis running time: " << elapsed.count() << " s" << io::endl; + log << "\tExact Global Must Analysis running time: " << elapsed.count() << " ms" << io::endl; // for(int i = 0; i < m_coll->size(); ++i) { // const icat3::LBlockSet& s = (*m_coll)[i]; @@ -193,8 +192,8 @@ private: ai::SimpleAI ana(ada); ana.run(); - for(CFGCollection::BlockIter b(m_cfgs); b; b++) - classifyBlock(lb, ada.domain(), b, ada.store().get(b)); + for(CFGCollection::BlockIter b(m_cfgs); b(); b++) + classifyBlock(lb, ada.domain(), *b, ada.store().get(*b)); //ada.store().clear(); } @@ -208,8 +207,8 @@ private: Bag& bAccs = icache::ACCESSES(b).ref(); GlobalMustAdapter::t save = classifyAccesses(b, focus, man, bAccs); - for(Block::EdgeIter e = b->outs(); e; e++) { - Bag& eAccs = icache::ACCESSES(e).ref(); + for(Block::EdgeIter e = b->outs(); e(); e++) { + Bag& eAccs = icache::ACCESSES(*e).ref(); man.restart(save); classifyAccesses(b, focus, man, eAccs); } diff --git a/src/MustAnalysis/MustAnalysis.cpp b/src/MustAnalysis/MustAnalysis.cpp index d351d962435c57d401b5dd2fcb63440fb3ce345b..0cd1ffb17920367f7da8ed49e79ea34c714fbdaa 100644 --- a/src/MustAnalysis/MustAnalysis.cpp +++ b/src/MustAnalysis/MustAnalysis.cpp @@ -29,7 +29,7 @@ #include #include #include -#include +#include #include "../ZDD/MustAbstractValuePolicy.h" #include "../ZDD/ZDDMustDomainPolicy.h" #include "../GeneratorsSet/GSMustAbstractValuePolicy.h" @@ -65,8 +65,8 @@ public: inline store_t& store(void) { return m_store; } void update(const Bag& accs, t& d) { - for(auto acc = *accs; acc; acc++) - m_domain.update(acc, d); + for(auto acc = *accs; acc(); acc++) + m_domain.update(*acc, d); } void update(Block* v, t& d) { @@ -75,7 +75,7 @@ public: t s; // update and join along edges - for(auto e = m_graph.preds(v); e; e++) { + for(auto e = m_graph.preds(v); e(); e++) { Block *w = e->source(); m_domain.copy(s, m_store.get(w)); @@ -88,7 +88,7 @@ public: // apply edge { - const Bag& accs = icache::ACCESSES(e); + const Bag& accs = icache::ACCESSES(*e); if(accs.count() > 0) update(accs, s); } @@ -145,13 +145,13 @@ protected: auto start = std::chrono::system_clock::now(); std::set toRefine; - for(CFGCollection::BlockIter b(m_cfgs); b; b++) { + for(CFGCollection::BlockIter b(m_cfgs); b(); b++) { if(!b->isBasic()) continue; BasicBlock* bb = b->toBasic(); - for(Block::EdgeIter edgeIter(bb->ins()); edgeIter; ++edgeIter) { + for(Block::EdgeIter edgeIter(bb->ins()); edgeIter(); ++edgeIter) { Edge* e = *edgeIter; Bag& bag = icache::ACCESSES(e).ref(); processBag(toRefine, bag); @@ -164,9 +164,9 @@ protected: processLBlock(lb); auto end = std::chrono::system_clock::now(); - auto elapsed = std::chrono::duration_cast(end - start); + auto elapsed = std::chrono::duration_cast(end - start); if(logFor(LOG_FUN)) - log << "\tExact Must Analysis running time: " << elapsed.count() << " s" << io::endl; + log << "\tExact Must Analysis running time: " << elapsed.count() << " ms" << io::endl; // for(int i = 0; i < m_coll->size(); ++i) { // const icat3::LBlockSet& s = (*m_coll)[i]; @@ -185,17 +185,17 @@ private: void processBag(std::set& set, Bag& bag) { for(int i = 0; i < bag.size(); ++i) { - lrumc::RefinementCategory refCat = lrumc::REFINEMENT_CATEGORY(bag[i]); + lruexact::RefinementCategory refCat = lruexact::REFINEMENT_CATEGORY(bag[i]); HitCategory e = HitCategory::NC; - if(refCat == lrumc::RefinementCategory::CLASSIFIED && + if(refCat == lruexact::RefinementCategory::CLASSIFIED && icat3::CATEGORY(bag[i]) == icat3::AH) e = HitCategory::AH; HIT_CATEGORY(bag[i]) = e; - if(refCat == lrumc::RefinementCategory::AH_CANDIDATE || - refCat == lrumc::RefinementCategory::AH_AM_CANDIDATE) + if(refCat == lruexact::RefinementCategory::AH_CANDIDATE || + refCat == lruexact::RefinementCategory::AH_AM_CANDIDATE) set.insert(icat3::LBLOCK(&bag[i])); } } @@ -209,8 +209,8 @@ private: ai::SimpleAI ana(ada); ana.run(); - for(CFGCollection::BlockIter b(m_cfgs); b; b++) - classifyBlock(lb, ada.domain(), b, ada.store().get(b)); + for(CFGCollection::BlockIter b(m_cfgs); b(); b++) + classifyBlock(lb, ada.domain(), *b, ada.store().get(*b)); ada.store().clear(); } @@ -224,8 +224,8 @@ private: Bag& bAccs = icache::ACCESSES(b).ref(); MustAdapter::t save = classifyAccesses(b, focus, man, bAccs); - for(Block::EdgeIter e = b->outs(); e; e++) { - Bag& eAccs = icache::ACCESSES(e).ref(); + for(Block::EdgeIter e = b->outs(); e(); e++) { + Bag& eAccs = icache::ACCESSES(*e).ref(); man.restart(save); classifyAccesses(b, focus, man, eAccs); } @@ -267,7 +267,7 @@ private: p::declare MustAnalysis::reg = p::init("lruzdd::MustAnalysis", Version(1, 0, 0)) .require(icat3::LBLOCKS_FEATURE) - .require(lrumc::REFINEMENT_CATEGORY_FEATURE) + .require(lruexact::REFINEMENT_CATEGORY_FEATURE) .require(COLLECTED_CFG_FEATURE) .provide(EXACT_MUST_ANALYSIS_FEATURE) .make(); diff --git a/src/ZDD/ZDD.cpp b/src/ZDD/ZDD.cpp index 27be4c58f3550702d917236fb18f64bd4337fde1..bc98a70eb05b3ed176572a2c290112763834dabf 100644 --- a/src/ZDD/ZDD.cpp +++ b/src/ZDD/ZDD.cpp @@ -5,8 +5,6 @@ extern "C" { #include -DdNode *zddMinDotProduct(DdManager* dd, DdNode* S, DdNode* T); -DdNode* ZddMinDotProduct(DdManager* dd, DdNode* S, DdNode* T); } @@ -127,11 +125,11 @@ ZDD ZDD::minDotProduct(const ZDD& other) const // TODO: Reduce at each step (code Extra_zddMinDotProduct) // TODO: Check failure -// DdNode* res = zddMinDotProduct(_manager->getManager(), _zdd, other._zdd); - DdNode* u = Extra_zddDotProduct(_manager->getManager(), _zdd, other._zdd); - Cudd_Ref(u); - DdNode* res = Extra_zddMinimal(_manager->getManager(), u); - Cudd_Deref(u); + DdNode* res = Extra_zddMinDotProduct(_manager->getManager(), _zdd, other._zdd); +// DdNode* u = Extra_zddDotProduct(_manager->getManager(), _zdd, other._zdd); +// Cudd_Ref(u); +// DdNode* res = Extra_zddMinimal(_manager->getManager(), u); +// Cudd_Deref(u); return ZDD(_manager, res); } @@ -190,148 +188,4 @@ void ZDD::printDotToFile(char* filename, char* function) const } // namespace lruzdd -extern "C" -{ - -DdNode *zddMinDotProduct( - DdManager * dd, - DdNode * S, - DdNode * T) -{ - DdNode *res; - do { - dd->reordered = 0; - res = ZddMinDotProduct(dd, S, T); - } while (dd->reordered == 1); - return(res); - -} /* end of zddMinDotProduct */ - -DdNode * -ZddMinDotProduct( - DdManager * dd, - DdNode * S, - DdNode * T) -{ - DdNode *zRes; - int TopS, TopT; - statLine(dd); - - /* consider terminal cases */ - if ( S == z0 || T == z0 ) - return z0; - if ( S == z1 ) - return T; - if ( T == z1 ) - return S; - - /* the operation is commutative - normalize the problem */ - TopS = dd->permZ[S->index]; - TopT = dd->permZ[T->index]; - - if ( TopS > TopT || (TopS == TopT && (unsigned long)S > (unsigned long)T) ) - return ZddMinDotProduct(dd, T, S); - - /* check cache */ - zRes = cuddCacheLookup2Zdd(dd, ZddMinDotProduct, S, T); - if (zRes) - return zRes; - else - { - DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp; - if ( TopS == TopT ) - { - /* compute the union of two cofactors of T (T0+T1) */ - zTemp = extraZddMinUnion(dd, cuddE(T), cuddT(T) ); - if ( zTemp == NULL ) - return NULL; - cuddRef( zTemp ); - - /* compute MinDotProduct with the top element for subsets (S1, T0+T1) */ - zSet0 = ZddMinDotProduct(dd, cuddT(S), zTemp ); - if ( zSet0 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zTemp); - return NULL; - } - cuddRef( zSet0 ); - Cudd_RecursiveDerefZdd(dd, zTemp); - - /* compute MinDotProduct with the top element for subsets (S0, T1) */ - zSet1 = ZddMinDotProduct(dd, cuddE(S), cuddT(T) ); - if ( zSet1 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zSet0); - return NULL; - } - cuddRef( zSet1 ); - - /* compute the union of these two partial results (zSet0 + zSet1) */ - zRes1 = extraZddMinUnion(dd, zSet0, zSet1 ); - if ( zRes1 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zSet0); - Cudd_RecursiveDerefZdd(dd, zSet1); - return NULL; - } - cuddRef( zRes1 ); - Cudd_RecursiveDerefZdd(dd, zSet0); - Cudd_RecursiveDerefZdd(dd, zSet1); - - /* compute MinDotProduct for subsets without the top-most element */ - zRes0 = ZddMinDotProduct(dd, cuddE(S), cuddE(T) ); - if ( zRes0 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zRes1); - return NULL; - } - cuddRef( zRes0 ); - } - else /* if ( TopS < TopT ) */ - { - /* compute MinDotProduct with the top element for subsets (S1, T) */ - zRes1 = ZddMinDotProduct(dd, cuddT(S), T ); - if ( zRes1 == NULL ) - return NULL; - cuddRef( zRes1 ); - - /* compute MinDotProduct for subsets without the top-most element */ - zRes0 = ZddMinDotProduct(dd, cuddE(S), T ); - if ( zRes0 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zRes1); - return NULL; - } - cuddRef( zRes0 ); - } - - /* remove subsets with this element covering subsets without this element */ - zRes1 = extraZddNotSupSet(dd, zTemp = zRes1, zRes0); - if ( zRes1 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zTemp); - Cudd_RecursiveDerefZdd(dd, zRes0); - return NULL; - } - cuddRef( zRes1 ); - Cudd_RecursiveDerefZdd(dd, zTemp); - - /* create the new node */ - zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zRes0 ); - Cudd_RecursiveDerefZdd( dd, zRes1 ); - return NULL; - } - cuddDeref( zRes0 ); - cuddDeref( zRes1 ); - - /* insert the result into cache */ - cuddCacheInsert2(dd, ZddMinDotProduct, S, T, zRes); - return zRes; - } -} /* end of extraZddMinDotProduct */ - -} diff --git a/src/extra.h b/src/extra.h deleted file mode 100644 index 4159fcd4e0ba1c0262358b5c291b5d1c442cdd07..0000000000000000000000000000000000000000 --- a/src/extra.h +++ /dev/null @@ -1,4 +0,0 @@ -extern "C" -{ -#include -}