Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit be178392 authored by otawa's avatar otawa
Browse files

Merge branch 'dev' into beta

parents d4d8549c ca015ae4
CMAKE_MINIMUM_REQUIRED(VERSION 2.6)
# configuration
set(PLUGIN "lrumc") # plugin name
set(PLUGIN "lruzdd") # plugin name
set(NAMESPACE "") # namespace
set(SOURCES "src/lrumc/lrumc.cpp"
"src/lrumc/MC/lrumc_MCProgramModelBuilding.cpp"
"src/lrumc/MC/lrumc_MCProgramModelSlicing.cpp"
"src/lrumc/MC/lrumc_MCProgramModelNode.cpp"
"src/lrumc/MC/lrumc_MCProgramModel.cpp"
"src/lrumc/MC/lrumc_MCCacheModel.cpp"
"src/lrumc/MC/lrumc_MCException.cpp"
"src/lrumc/MC/lrumc_MCNuxmvCommand.cpp"
"src/lrumc/MC/lrumc_MCInstance.cpp"
"src/lrumc/MC/lrumc_MCAnalysis.cpp"
"src/lrumc/MC/lrumc_MCQueryManager.cpp"
"src/lrumc/EM/lrumc_ExistMissDomain.cpp"
"src/lrumc/EM/lrumc_ExistMissAdapter.cpp"
"src/lrumc/EM/lrumc_ExistMissAnalysis.cpp"
"src/lrumc/EH/lrumc_ExistHitDomain.cpp"
"src/lrumc/EH/lrumc_ExistHitAdapter.cpp"
"src/lrumc/EH/lrumc_ExistHitAnalysis.cpp"
"src/lrumc/lrumc_ACSManager.cpp"
"src/lrumc/lrumc_DUCatBuilder.cpp"
set(SOURCES "src/lruzdd.cpp"
"src/MayAnalysis/MayAnalysis.cpp"
"src/MustAnalysis/MustAnalysis.cpp"
"src/MayAnalysis/GlobalMayAnalysis.cpp"
"src/MustAnalysis/GlobalMustAnalysis.cpp"
"src/ClassificationBuilder.cpp"
"src/ZDD/ZDD.cpp"
"src/ZDD/ZDDManager.cpp"
"src/ZDD/MustAbstractValuePolicy.cpp"
"src/ZDD/MayAbstractValuePolicy.cpp"
"src/GeneratorsSet/GSMayAbstractValuePolicy.cpp"
"src/GeneratorsSet/GSMustAbstractValuePolicy.cpp"
"src/ZDD/MustAbstractValuePolicy.cpp"
"src/ZDD/MayAbstractValuePolicy.cpp"
)
# 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")
......@@ -35,20 +33,38 @@ if(NOT OTAWA_CONFIG)
message(FATAL_ERROR "ERROR: otawa-config is required !")
endif()
endif()
file(COPY ${CMAKE_CURRENT_SOURCE_DIR}/${PLUGIN}.eld DESTINATION ${CMAKE_CURRENT_BINARY_DIR}/)
message(STATUS "otawa-config found at ${OTAWA_CONFIG}")
execute_process(COMMAND "${OTAWA_CONFIG}" --cflags OUTPUT_VARIABLE OTAWA_CFLAGS OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND "${OTAWA_CONFIG}" --libs --make-plug ${PLUGIN} -r OUTPUT_VARIABLE OTAWA_LDFLAGS OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND "${OTAWA_CONFIG}" --prefix OUTPUT_VARIABLE OTAWA_PREFIX OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND "${OTAWA_CONFIG}" --cflags
OUTPUT_VARIABLE OTAWA_CFLAGS
WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}"
OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND "${OTAWA_CONFIG}" --libs --make-plug ${PLUGIN} -r
OUTPUT_VARIABLE OTAWA_LDFLAGS
WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}"
OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND "${OTAWA_CONFIG}" --prefix
OUTPUT_VARIABLE OTAWA_PREFIX
WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}"
OUTPUT_STRIP_TRAILING_WHITESPACE)
# plugin definition
set(ORIGIN $ORIGIN)
include_directories("${CMAKE_SOURCE_DIR}" "include")
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")
target_link_libraries(${PLUGIN} "${OTAWA_LDFLAGS}")
set_property(TARGET ${PLUGIN} PROPERTY COMPILE_FLAGS "${OTAWA_CFLAGS} --std=c++11 -g -Wall -Wextra -pedantic")
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 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})
set(CUDD_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/cudd/lib/libcudd.a)
add_custom_command(
OUTPUT ${CUDD_LIB_FILE}
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}/
)
add_custom_target(
libcudd
DEPENDS ${CUDD_LIB_FILE}
)
#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/"
)
file(MAKE_DIRECTORY ${CUDD_INCLUDE_DIR})
add_library(cudd STATIC IMPORTED GLOBAL)
set_target_properties(cudd PROPERTIES
IMPORTED_LOCATION ${CUDD_LIB_FILE}
INTERFACE_INCLUDE_DIRECTORIES "${CUDD_INCLUDE_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
)
set_target_properties(extra
PROPERTIES
PUBLIC_HEADER extra.h
POSITION_INDEPENDENT_CODE ON
)
target_link_libraries(extra cudd)
target_include_directories(extra PUBLIC include)
add_dependencies(extra libcudd)
Most of the code in this directory was taken from the extra library of Alan Mishchenko.
#ifndef EXTRA_H
#define EXTRA_H
#include <stdio.h>
#include <cudd.h>
#include <cuddInt.h>
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
#include <extra.h>
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 */
#include <extra.h>
/**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 */
#include <extra.h>
/**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 */
#include <extra.h>
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 );