diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5ed08f3a1756867c18241faf6399e8a58f036105..66806e70a888b16879579b9d279d1ba512187f9b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -12,7 +12,7 @@ set(CMAKE_CXX_EXTENSIONS OFF)
# Add compiler flags
if(CMAKE_COMPILER_IS_GNUCC)
- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -std=c++14")
+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -O0 -g3 -fpermissive -std=c++17 -pthread")
endif()
@@ -22,11 +22,7 @@ message(STATUS "Building Petri Net parser ...")
include_directories("${PARSER_DIR}/src")
add_subdirectory(${PARSER_DIR})
-# add sylvan
-message(STATUS "Building Sylvan ...")
-set(SYLVAN_DIR "${CMAKE_SOURCE_DIR}/third-party/sylvan")
-include_directories(${SYLVAN_DIR})
-add_subdirectory(${SYLVAN_DIR})
+
# build spot if it is not installed on the system
find_library(SPOT_LIBRARY "spot")
@@ -40,7 +36,7 @@ if(NOT SPOT_LIBRARY)
ExternalProject_Add(SpotLibrary
PREFIX ${SPOT_DIR}
- URL http://www.lrde.epita.fr/dload/spot/spot-2.9.tar.gz
+ URL http://www.lrde.epita.fr/dload/spot/spot-2.9.4.tar.gz
DOWNLOAD_NO_PROGRESS YES
CONFIGURE_COMMAND ./configure --disable-doxygen --disable-python --enable-silent-rules --silent --prefix=<INSTALL_DIR>
BUILD_COMMAND make -j
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 759b2b3fdb27fb58ba3005404da1455546b3b3cb..2672d0438ec6b1f9253e75119d0b26ef50704980 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -27,18 +27,12 @@ add_executable(mc-sog main.cpp
NewNet.h
CommonSOG.cpp
CommonSOG.h
- DistributedSOG.cpp
- DistributedSOG.h
- HybridSOG.cpp
- HybridSOG.h
- threadSOG.cpp
- threadSOG.h
LDDGraph.cpp
LDDGraph.h
LDDState.cpp
LDDState.h
TransSylvan.cpp
- sylvan_sog.c
+
SpotSogState.cpp
SpotSogState.h
SpotSogIterator.cpp
@@ -53,24 +47,18 @@ add_executable(mc-sog main.cpp
SogKripke.h
ModelCheckBaseMT.cpp
ModelCheckBaseMT.h
- ModelCheckLace.cpp
- ModelCheckLace.h
+
SogKripkeTh.cpp
SogKripkeTh.h
SogKripkeStateTh.cpp
SogKripkeStateTh.h
SogKripkeIteratorTh.cpp
SogKripkeIteratorTh.h
- ModelCheckerTh.cpp
- ModelCheckerTh.h
+
stacksafe.cpp
stacksafe.h
SafeDequeue.cpp
SafeDequeue.h
- ModelCheckerThV2.cpp
- ModelCheckerThV2.h
- MCHybridSOG.cpp
- MCHybridSOG.h
HybridKripke.cpp
HybridKripke.h
HybridKripkeIterator.cpp
@@ -79,12 +67,16 @@ add_executable(mc-sog main.cpp
HybridKripkeState.h
SylvanWrapper.cpp
SylvanWrapper.h
- )
+ SylvanCacheWrapper.cpp SylvanCacheWrapper.h
+ ModelCheckerCPPThread.cpp ModelCheckerCPPThread.h
+ ModelCheckerTh.cpp ModelCheckerTh.h
+ threadSOG.cpp threadSOG.h
+ HybridSOG.cpp HybridSOG.h
+ MCHybridSOG.cpp MCHybridSOG.h)
target_link_libraries(mc-sog
bddx
spot
- sylvan
RdP
${MPI_LIBRARIES}
${OPENSSL_LIBRARIES}
diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index ea44c8242996cedcacf5b69d070b235821e9cfd2..6ef58343684d375b591961dca8b6932e7c620bd7 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -1,11 +1,10 @@
+#include <string>
+#include "SylvanWrapper.h"
#include "CommonSOG.h"
-#include "sylvan.h"
-#include "sylvan_seq.h"
-#include <sylvan_sog.h>
-#include <sylvan_int.h>
+
#include <stack>
-#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
+
const vector<class Place> *_places = NULL;
CommonSOG::CommonSOG() {
@@ -28,10 +27,9 @@ MDD CommonSOG::Accessible_epsilon(MDD From) {
M1 = M2;
for (Set::const_iterator i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) {
//fireTransition
-
MDD succ = fireTransition(M2, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
- M2 = lddmc_union_mono(M2, succ);
+ M2 = SylvanWrapper::lddmc_union_mono(M2, succ);
}
@@ -62,7 +60,7 @@ MDD CommonSOG::ImageForward(MDD From) {
MDD Res = lddmc_false;
for (Set::const_iterator i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) {
MDD succ = fireTransition(From, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
- Res = lddmc_union_mono(Res, succ);
+ Res = SylvanWrapper::lddmc_union_mono(Res, succ);
}
return Res;
}
@@ -73,16 +71,16 @@ MDD CommonSOG::Canonize(MDD s, unsigned int level) {
if (level > m_nbPlaces || s == lddmc_false) {
return lddmc_false;
}
- if (isSingleMDD(s)) {
+ if (SylvanWrapper::isSingleMDD(s)) {
return s;
}
MDD s0 = lddmc_false, s1 = lddmc_false;
bool res = false;
do {
- if (get_mddnbr(s, level) > 1) {
- s0 = ldd_divide_rec(s, level);
- s1 = ldd_minus(s, s0);
+ if (SylvanWrapper::get_mddnbr(s, level) > 1) {
+ s0 = SylvanWrapper::ldd_divide_rec(s, level);
+ s1 = SylvanWrapper::ldd_minus(s, s0);
res = true;
} else {
level++;
@@ -100,9 +98,9 @@ MDD CommonSOG::Canonize(MDD s, unsigned int level) {
Reach = s1;
do {
// cout<<"premiere boucle interne \n";
- Front = ldd_minus(ImageForward(Front), Reach);
- Reach = lddmc_union_mono(Reach, Front);
- s0 = ldd_minus(s0, Front);
+ Front = SylvanWrapper::ldd_minus(ImageForward(Front), Reach);
+ Reach = SylvanWrapper::lddmc_union_mono(Reach, Front);
+ s0 = SylvanWrapper::ldd_minus(s0, Front);
} while ((Front != lddmc_false) && (s0 != lddmc_false));
}
if ((s0 != lddmc_false) && (s1 != lddmc_false)) {
@@ -110,16 +108,16 @@ MDD CommonSOG::Canonize(MDD s, unsigned int level) {
Reach = s0;
do {
// cout<<"deuxieme boucle interne \n";
- Front = ldd_minus(ImageForward(Front), Reach);
- Reach = lddmc_union_mono(Reach, Front);
- s1 = ldd_minus(s1, Front);
+ Front = SylvanWrapper::ldd_minus(ImageForward(Front), Reach);
+ Reach = SylvanWrapper::lddmc_union_mono(Reach, Front);
+ s1 = SylvanWrapper::ldd_minus(s1, Front);
} while (Front != lddmc_false && s1 != lddmc_false);
}
MDD Repr = lddmc_false;
- if (isSingleMDD(s0)) {
+ if (SylvanWrapper::isSingleMDD(s0)) {
Repr = s0;
} else {
@@ -127,10 +125,10 @@ MDD CommonSOG::Canonize(MDD s, unsigned int level) {
}
- if (isSingleMDD(s1)) {
- Repr = lddmc_union_mono(Repr, s1);
+ if (SylvanWrapper::isSingleMDD(s1)) {
+ Repr = SylvanWrapper::lddmc_union_mono(Repr, s1);
} else {
- Repr = lddmc_union_mono(Repr, Canonize(s1, level));
+ Repr = SylvanWrapper::lddmc_union_mono(Repr, Canonize(s1, level));
}
@@ -173,22 +171,22 @@ bool CommonSOG::Set_Div(MDD &M) const {
Reached = lddmc_false;
From = M;
do {
-
+ Reached = lddmc_false;
for (i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) {
-
MDD To = fireTransition(From, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
- Reached = lddmc_union_mono(Reached, To);
- //Reached=To;
+ Reached = SylvanWrapper::lddmc_union_mono(Reached, To);
}
if (Reached == From) {
- return true;
+ MDD Reached_obs=lddmc_false;
+ for (i = m_observable.begin(); !(i == m_observable.end()) && (Reached_obs==lddmc_false); i++) {
+ Reached_obs= fireTransition(From, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
+ }
+ if (Reached_obs==lddmc_false) return true;
+ return false;
}
From = Reached;
- Reached = lddmc_false;
-
- } while (Reached != lddmc_false && Reached != lddmc_true);
-
+ } while (Reached != lddmc_false);
return false;
}
@@ -205,13 +203,7 @@ bool CommonSOG::Set_Bloc(MDD &M) const {
//BLOCAGE
}
-string CommonSOG::getTransition(int pos) {
- return m_graph->getTransition(pos);
-}
-string CommonSOG::getPlace(int pos) {
- return m_graph->getPlace(pos);
-}
LDDGraph *CommonSOG::m_graph;
struct elt_t {
@@ -222,76 +214,17 @@ struct elt_t {
};
MDD CommonSOG::fireTransition(MDD cmark, MDD minus, MDD plus) {
- return lddmc_firing_mono(cmark,minus,plus);
- // for an empty set of source states, or an empty transition relation, return the empty set
-
- MDD result;
- mddnode_t n_cmark, n_plus, n_minus;
- uint32_t value, value_minus, value_plus;
- std::stack<elt_t> lstack;
- elt_t elt;
- elt.cmark = cmark;
- elt.plus = plus;
- elt.minus = minus;
- elt.level = 0;
- lstack.push(elt);
- result = lddmc_false;
- uint32_t *currentMarking = new uint32_t[m_nbPlaces];
- elt_t relt;
- bool goDown = false;
- //MDD temp;
- while (!lstack.empty() || goDown) {
- if (!goDown) {
- elt = lstack.top();
- lstack.pop();
- n_cmark = GETNODE(elt.cmark);
- n_minus = GETNODE(elt.minus);
- n_plus = GETNODE(elt.plus);
- value = mddnode_getvalue(n_cmark);
- value_minus = mddnode_getvalue(n_minus);
- value_plus = mddnode_getvalue(n_plus);
- } else goDown = false;
-
- //cout << "Level : " << elt.level << endl;
- //cout << "Current : " << value << " Minus : " << value_minus << " Plus : " << value_plus << endl;
- if (value >= value_minus) {
- *(currentMarking + elt.level) = value - value_minus + value_plus;
- if (elt.level == m_nbPlaces - 1) {
- MDD b = ldd_cube(currentMarking, m_nbPlaces);
- result = lddmc_union_mono(result, b);
- } else { // Goto next level and push right
- if (mddnode_getright(n_cmark) != lddmc_false) { // Look for another node in the same level
- relt = elt;
- relt.cmark = mddnode_getright(n_cmark);
- lstack.push(relt);
- }
- //} while (temp>lddmc_true);
- if (elt.level < m_nbPlaces - 1) { // Go down
- elt.level++;
- elt.cmark = mddnode_getdown(n_cmark);
- n_cmark = GETNODE(elt.cmark);
- elt.minus = mddnode_getdown(n_minus);
- n_minus = GETNODE(elt.minus);
- elt.plus = mddnode_getdown(n_plus);
- n_plus = GETNODE(elt.plus);
- goDown = true;
- value = mddnode_getvalue(n_cmark);
- value_minus = mddnode_getvalue(n_minus);
- value_plus = mddnode_getvalue(n_plus);
- }
- }
- } else {
- // Look for another node in the same level
- elt.cmark = mddnode_getright(n_cmark);
- while (elt.cmark>lddmc_true && !goDown) {
- n_cmark = GETNODE(elt.cmark);
- value = mddnode_getvalue(n_cmark);
- if (value >= value_minus) goDown = true; else elt.cmark = mddnode_getright(n_cmark);
- }
+ return SylvanWrapper::lddmc_firing_mono(cmark,minus,plus);
+}
- }
- }
- delete[]currentMarking;
+//string_view CommonSOG::getTransition(int pos) {
+ // cout<<"yes it is : "<<m_transitions.at(pos).name<<endl;
+ // cout<<"Ok "<<m_graph->getTransition(pos)<<endl;
+// return string_view {m_transitions.at(pos).name};
+//}
- return result;
+string_view CommonSOG::getPlace(int pos) {
+ // cout<<"yes it is : "<<m_transitions.at(pos).name<<endl;
+ // cout<<"Ok "<<m_graph->getPlace(pos)<<endl;
+ return string_view {m_graph->getPlace(pos)};
}
\ No newline at end of file
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index e5136a0c038b0413f48cb58213c00bec26b3f46e..5f6f7e166a4e6247d32bba1565d0f2f2fc905c5a 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -28,17 +28,23 @@ class CommonSOG
vector<TransSylvan>* getTBRelation();
Set * getNonObservable();
unsigned int getPlacesCount();
- set<uint16_t> & getPlaceProposition() {return m_place_proposition;}
- string getTransition(int pos);
- string getPlace(int pos);
+ inline set<uint16_t> & getPlaceProposition() {return m_place_proposition;}
+ inline string_view getTransition(int pos) {
+ {
+ return string_view {m_transitions.at(pos).name};
+ }
+ }
+ string_view getPlace(int pos);
+
+
protected:
NewNet* m_net;
int m_nbPlaces = 0;
static LDDGraph *m_graph;
vector<TransSylvan> m_tb_relation;
MDD m_initialMarking;
- map<string, uint16_t> m_transitionName;
- map<uint16_t,string> m_placeName;
+ map<string, uint16_t> * m_transitionName;
+ map<uint16_t,string> * m_placeName;
Set m_observable;
Set m_nonObservable;
Set InterfaceTrans;
diff --git a/src/HybridKripke.cpp b/src/HybridKripke.cpp
index ad06063e81ae32c176c928064f6d714e73ceeb00..9194765858bd6a9e4d83d65b2d7c3771b8ed1eb9 100644
--- a/src/HybridKripke.cpp
+++ b/src/HybridKripke.cpp
@@ -79,9 +79,11 @@ HybridKripkeIterator* HybridKripke::succ_iter(const spot::state* s) const {
it->recycle(*st,cond);
return it;
}
+#ifdef TESTENABLE
SylvanWrapper::m_agg++;
SylvanWrapper::m_Size+=ss->getSize();
cout<<"Expolored states : "<<SylvanWrapper::m_Size<<" , Explored agg : "<<SylvanWrapper::m_agg<<" , Avg per agg : " <<SylvanWrapper::m_Size/SylvanWrapper::m_agg<<endl;
+#endif
return new HybridKripkeIterator(*st,cond);
}
@@ -93,13 +95,13 @@ bdd HybridKripke::state_condition(const spot::state* s) const
list<uint16_t>* marked_place=ss->getMarkedPlaces();
bdd result=bddtrue;
for (auto it=marked_place->begin();it!=marked_place->end();it++) {
- string name=m_net->getPlaceName(*it);
+ string name=string(m_net->getPlaceName(*it));
spot::formula f=spot::formula::ap(name);
result&=bdd_ithvar((dict_->var_map.find(f))->second);
}
list<uint16_t>* unmarked_place=ss->getUnmarkedPlaces();
for (auto it=unmarked_place->begin();it!=unmarked_place->end();it++) {
- string name=m_net->getPlaceName(*it);
+ string name=string(m_net->getPlaceName(*it));
spot::formula f=spot::formula::ap(name);
result&=!bdd_ithvar((dict_->var_map.find(f))->second);
}
diff --git a/src/HybridKripkeIterator.cpp b/src/HybridKripkeIterator.cpp
index 7202533a5693ea7e09dc3d892d80b4f2cac50bb3..579cbb77078fdd334968833d6cb1b110fc3bb8ab 100644
--- a/src/HybridKripkeIterator.cpp
+++ b/src/HybridKripkeIterator.cpp
@@ -41,7 +41,7 @@ bdd HybridKripkeIterator::cond() const {
//cout<<"entering "<<__func__<<endl;
succ_t succ_elt=m_current_state->getListSucc()->at(m_current_edge);
if (succ_elt.transition==-1) return bddtrue;
- string name=m_net->getTransitionName(succ_elt.transition);
+ string name=string(m_net->getTransitionName(succ_elt.transition));
spot::bdd_dict *p=m_dict_ptr->get();
spot::formula f=spot::formula::ap(name);
bdd result=bdd_ithvar((p->var_map.find(f))->second);
diff --git a/src/HybridSOG.cpp b/src/HybridSOG.cpp
index cd4f52f2b3f87583972063642a1aadd6cdbd5302..b626ccfd50df21f315dc623a9753a659fa71abf6 100644
--- a/src/HybridSOG.cpp
+++ b/src/HybridSOG.cpp
@@ -4,13 +4,8 @@
using namespace std;
#include <stdio.h>
-#include "sylvan_seq.h"
-#include "sylvan_sog.h"
-#include <sylvan_int.h>
-
-using namespace sylvan;
#include <openssl/md5.h>
-#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
+
#define LENGTH_ID 16
//#define LENGTH_MSG 180
@@ -55,16 +50,10 @@ HybridSOG::HybridSOG(const NewNet &R,bool init)
{
- lace_init(1, 0);
- lace_startup(0, NULL, NULL);
-
- // Simple Sylvan initialization, also initialize MDD support
- sylvan_set_limits(2LL<<31, 2, 1); // sylvan_set_limits(2LL<<31, 2, 1);
- //sylvan_set_sizes(1LL<<27, 1LL<<31, 1LL<<20, 1LL<<22);
-
- sylvan_init_package();
- sylvan_init_ldd();
- sylvan_gc_enable();
+ SylvanWrapper::sylvan_set_limits ( 16LL<<30, 8, 0 );
+ SylvanWrapper::sylvan_init_package();
+ SylvanWrapper::sylvan_init_ldd();
+ SylvanWrapper::init_gc_seq();
m_net=&R;
m_init=init;
@@ -72,14 +61,14 @@ HybridSOG::HybridSOG(const NewNet &R,bool init)
int i, domain;
vector<Place>::const_iterator it_places;
- init_gc_seq();
+
//_______________
m_transitions=R.transitions;
m_observable=R.Observable;
m_nonObservable=R.NonObservable;
m_place_proposition=R.m_formula_place;
- m_transitionName=R.transitionName;
- m_placeName=R.m_placePosName;
+ m_transitionName=&R.transitionName;
+ m_placeName=&R.m_placePosName;
InterfaceTrans=R.InterfaceTrans;
m_nbPlaces=R.places.size();
@@ -92,8 +81,8 @@ HybridSOG::HybridSOG(const NewNet &R,bool init)
{
liste_marques[i] =it_places->marking;
}
- m_initialMarking=lddmc_cube(liste_marques,R.places.size());
- ldd_refs_push(m_initialMarking);
+ m_initialMarking=SylvanWrapper::lddmc_cube(liste_marques,R.places.size());
+ //# ldd_refs_push(m_initialMarking);
delete []liste_marques;
// place names
@@ -129,11 +118,11 @@ HybridSOG::HybridSOG(const NewNet &R,bool init)
postc[it->first] = postc[it->first] + it->second;
}
- MDD _minus=lddmc_cube(prec,m_nbPlaces);
- ldd_refs_push(_minus);
+ MDD _minus=SylvanWrapper::lddmc_cube(prec,m_nbPlaces);
+ //#ldd_refs_push(_minus);
- MDD _plus=lddmc_cube(postc,m_nbPlaces);
- ldd_refs_push(_plus);
+ MDD _plus=SylvanWrapper::lddmc_cube(postc,m_nbPlaces);
+ //#ldd_refs_push(_plus);
m_tb_relation.push_back(TransSylvan(_minus,_plus));
}
//sylvan_gc_seq();
@@ -170,10 +159,10 @@ void *HybridSOG::doCompute()
LDDState *c=new LDDState;
MDD Complete_meta_state=Accessible_epsilon(m_initialMarking);
c->m_lddstate=Complete_meta_state;
- ldd_refs_push(Complete_meta_state);
+ //#ldd_refs_push(Complete_meta_state);
// MDD reduced_initialstate=Canonize(Complete_meta_state,0);
- convert_wholemdd_stringcpp(Complete_meta_state,*chaine);
+ SylvanWrapper::convert_wholemdd_stringcpp(Complete_meta_state,*chaine);
//DisplayMessage(chaine->c_str());
//write_to_dot("normal.dot",Complete_meta_state);
//exit(0);
@@ -209,7 +198,7 @@ void *HybridSOG::doCompute()
initialstate=Canonize(Complete_meta_state,0);
}
//#endif // REDUCE
- convert_wholemdd_stringcpp(initialstate,*chaine);
+ SylvanWrapper::convert_wholemdd_stringcpp(initialstate,*chaine);
pthread_mutex_lock(&m_spin_msg[0]);
@@ -312,17 +301,17 @@ void *HybridSOG::doCompute()
MDD ldd_reachedclass=Accessible_epsilon(get_successor(e.first.second,t));
- ldd_refs_push(ldd_reachedclass);
+ //#ldd_refs_push(ldd_reachedclass);
if (id_thread==1)
- if (isGCRequired())
+ if (SylvanWrapper::isGCRequired())
{
pthread_mutex_lock(&m_gc_mutex);
#ifdef DEBUG_GC
displayMDDTableInfo();
#endif // DEBUG_GC
- sylvan_gc_seq();
+ //# sylvan_gc_seq();
#ifdef DEBUG_GC
displayMDDTableInfo();
@@ -340,7 +329,7 @@ void *HybridSOG::doCompute()
//MDD Reduced=ldd_reachedclass;
string* message_to_send1=new string();
- convert_wholemdd_stringcpp(ldd_reachedclass,*message_to_send1);
+ SylvanWrapper::convert_wholemdd_stringcpp(ldd_reachedclass,*message_to_send1);
get_md5(*message_to_send1,Identif);
@@ -410,7 +399,7 @@ void *HybridSOG::doCompute()
#endif
//MDD Reduced=ldd_reachedclass;
string* message_to_send2=new string();
- convert_wholemdd_stringcpp(reached,*message_to_send2);
+ SylvanWrapper::convert_wholemdd_stringcpp(reached,*message_to_send2);
get_md5(*message_to_send2,Identif);
@@ -479,7 +468,7 @@ void *HybridSOG::doCompute()
pthread_mutex_lock(&m_spin_stack[min_charge]);
m_st[min_charge].push(Pair(couple(Agregate,MState),fire));
pthread_mutex_unlock(&m_spin_stack[min_charge]);
- ldd_refs_push(MState);
+ //#ldd_refs_push(MState);
m_charge[min_charge]++;
}
@@ -884,8 +873,8 @@ MDD HybridSOG::decodage_message(const char *chaine)
list_marq[j]=(uint32_t)((unsigned char)chaine[index]-1);
index++;
}
- MDD N=lddmc_cube(list_marq,m_nbPlaces);
- M=lddmc_union_mono(M,N);
+ MDD N=SylvanWrapper::lddmc_cube(list_marq,m_nbPlaces);
+ M=SylvanWrapper::lddmc_union_mono(M,N);
}
return M;
}
@@ -921,48 +910,7 @@ void * HybridSOG::threadHandler(void *context)
return ((HybridSOG*)context)->doCompute();
}
-void HybridSOG::convert_wholemdd_stringcpp(MDD cmark,string &res)
-{
- typedef pair<string,MDD> Pair_stack;
- vector<Pair_stack> local_stack;
-
- unsigned int compteur=0;
- MDD explore_mdd=cmark;
-
- string chaine;
-
- res=" ";
- local_stack.push_back(Pair_stack(chaine,cmark));
- do
- {
- Pair_stack element=local_stack.back();
- chaine=element.first;
- explore_mdd=element.second;
- local_stack.pop_back();
- compteur++;
- while ( explore_mdd!= lddmc_false && explore_mdd!=lddmc_true)
- {
- mddnode_t n_val = GETNODE(explore_mdd);
- if (mddnode_getright(n_val)!=lddmc_false)
- {
- local_stack.push_back(Pair_stack(chaine,mddnode_getright(n_val)));
- }
- unsigned int val = mddnode_getvalue(n_val);
- chaine.push_back((unsigned char)(val)+1);
- explore_mdd=mddnode_getdown(n_val);
- }
- /*printchaine(&chaine);printf("\n");*/
- res+=chaine;
- }
- while (local_stack.size()!=0);
- //delete chaine;
-
- compteur=(compteur<<1) | 1;
- res[1]=(unsigned char)((compteur>>8)+1);
- res[0]=(unsigned char)(compteur & 255);
-
-}
void HybridSOG::get_md5(const string& chaine,unsigned char *md_chaine)
diff --git a/src/HybridSOG.h b/src/HybridSOG.h
index 323a19b0ef32ea5eb79666494807363caa286e8d..6e2e395d6e4025ef4549c37ad3f75d150e82c186 100644
--- a/src/HybridSOG.h
+++ b/src/HybridSOG.h
@@ -88,9 +88,6 @@ private:
int m_charge[128];
int m_init;
-
- /// Convert an MDD to a string caracter (for the send)
- void convert_wholemdd_stringcpp(MDD cmark, string &chaine);
/// Convert a string caracter to an MDD
MDD decodage_message(const char *chaine);
/// there is a message to receive?
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index a09fa9d909a69e59574458e1d3f4d789ff859af7..99e8ad6783782b892a5abdabf6170af7cfc687e7 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -1,5 +1,5 @@
#include "LDDGraph.h"
-#include <sylvan.h>
+
#include <string.h>
#include <map>
#include "SylvanWrapper.h"
@@ -15,9 +15,7 @@ void LDDGraph::setInitialState(LDDState *c) {
}
-LDDState *LDDGraph::getInitialState() const {
- return m_GONodes.at(0);
-}
+
/*----------------------find()----------------*/
LDDState *LDDGraph::find(LDDState *c) {
@@ -133,7 +131,7 @@ int LDDGraph::NbBddNode(LDDState *S, size_t &nb) {
void LDDGraph::printCompleteInformation() {
long count_ldd = 0L;
for (MetaLDDNodes::const_iterator i = m_GONodes.begin(); !(i == m_GONodes.end()); i++) {
- count_ldd += lddmc_nodecount((*i)->m_lddstate);
+ count_ldd += SylvanWrapper::lddmc_nodecount((*i)->m_lddstate);
m_nbMarking+= SylvanWrapper::getMarksCount((*i)->m_lddstate);
}
cout << "\n\nGRAPH SIZE : \n";
@@ -215,18 +213,24 @@ LDDState *LDDGraph::getLDDStateById(unsigned int id) {
return m_GONodes.at(id);
}
-string LDDGraph::getTransition(uint16_t pos) {
+string_view LDDGraph::getTransition(uint16_t pos) {
map<string, uint16_t>::iterator it = m_transition->begin();
+
while (it != m_transition->end()) {
- if (it->second == pos)
+
+ if (it->second == pos) {
+ //cout<<"first : "<<it->first<<endl;
+
return it->first;
+ }
it++;
}
+
return it->first;
}
-string LDDGraph::getPlace(uint16_t pos) {
+string_view LDDGraph::getPlace(uint16_t pos) {
return m_places->find(pos)->second;
}
diff --git a/src/LDDGraph.h b/src/LDDGraph.h
old mode 100644
new mode 100755
index fbc991610080f2355d4f04e5f5cb4322209ccfec..1d7413b8115cdd0d1e18113203354171044ab188
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -23,8 +23,8 @@ class LDDGraph
CommonSOG *m_constructor;
public:
CommonSOG* getConstructor() {return m_constructor;}
- string getTransition(uint16_t pos);
- string getPlace(uint16_t pos);
+ string_view getTransition(uint16_t pos);
+ string_view getPlace(uint16_t pos);
void setPlace(map<uint16_t,string>& list_places);
void setTransition(map<string,uint16_t>& list_transitions);
MetaLDDNodes m_GONodes;
@@ -51,7 +51,10 @@ class LDDGraph
void insert(LDDState*);
LDDGraph(CommonSOG *constuctor) {m_nbArcs=m_nbMarking=0;m_constructor=constuctor;}
void setInitialState(LDDState*); //Define the initial state of this graph
- LDDState* getInitialState() const;
+ //LDDState* getInitialState() const;
+ LDDState *getInitialState() const {
+ return m_GONodes.at(0);
+ }
void printCompleteInformation();
virtual ~LDDGraph();
};
diff --git a/src/LDDState.cpp b/src/LDDState.cpp
index 8d51f374b2845e98972704c650e90f3208642219..0028e856038a1d92181db7383d5df9e7b16dd65f 100644
--- a/src/LDDState.cpp
+++ b/src/LDDState.cpp
@@ -1,10 +1,9 @@
-#include <sylvan.h>
-#include <sylvan_int.h>
#include "LDDState.h"
#include "LDDGraph.h"
#include <iostream>
-#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
+#include "SylvanWrapper.h"
+
LDDState::~LDDState()
{
//dtor
@@ -30,20 +29,16 @@ vector<pair<LDDState*, int>>* LDDState::getSuccessors() {
vector<uint16_t> LDDState::getMarkedPlaces(set<uint16_t>& lplacesAP) {
vector<uint16_t> result;
MDD mdd=m_lddstate;
- uint16_t depth=0;
- while (mdd>lddmc_true)
- {
- //printf("mddd : %d \n",mdd);
- mddnode_t node=GETNODE(mdd);
- if (lplacesAP.find(depth)!=lplacesAP.end())
- if (mddnode_getvalue(node)==1) {
+ int depth=0;
+ for (auto & iter : lplacesAP) {
+ mddnode_t node=SylvanWrapper::GETNODE(mdd);
+ for (; depth < iter; depth++) {
+ mdd=SylvanWrapper::mddnode_getdown(node);
+ node=SylvanWrapper::GETNODE(mdd);
+ }
+ if (SylvanWrapper::mddnode_getvalue(node)!=0) {
result.push_back(depth);
-
}
-
- mdd=mddnode_getdown(node);
- depth++;
-
}
return result;
}
@@ -51,20 +46,35 @@ vector<uint16_t> LDDState::getMarkedPlaces(set<uint16_t>& lplacesAP) {
vector<uint16_t> LDDState::getUnmarkedPlaces(set<uint16_t>& lplacesAP) {
vector<uint16_t> result;
MDD mdd=m_lddstate;
-
- uint16_t depth=0;
+ int depth=0;
+ for (auto & iter : lplacesAP) {
+ mddnode_t node=SylvanWrapper::GETNODE(mdd);
+ for (; depth < iter; depth++) {
+ mdd=SylvanWrapper::mddnode_getdown(node);
+ node=SylvanWrapper::GETNODE(mdd);
+ }
+ if (SylvanWrapper::mddnode_getvalue(node)==0) {
+ result.push_back(depth);
+ }
+ }
+ return result;
+ /*cout<<"Display begin"<<endl;
+ for (auto & iter : lplacesAP)
+ cout<<iter<<endl;
+ cout<<"Display end"<<endl;*/
+ /*uint16_t depth=0;
while (mdd>lddmc_true)
{
//printf("mddd : %d \n",mdd);
- mddnode_t node=GETNODE(mdd);
+ mddnode_t node=SylvanWrapper::GETNODE(mdd);
if (lplacesAP.find(depth)!=lplacesAP.end())
- if (mddnode_getvalue(node)==0) {
+ if (SylvanWrapper::mddnode_getvalue(node)==0) {
result.push_back(depth);
}
- mdd=mddnode_getdown(node);
+ mdd=SylvanWrapper::mddnode_getdown(node);
depth++;
}
- return result;
+ return result;*/
}
diff --git a/src/LDDState.h b/src/LDDState.h
old mode 100644
new mode 100755
index a56dbe4afbbed7069e3cfef96a2160b7c7de848f..e261f9e4ab62207cfc29e84d4874cd5b57cdf0c6
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -1,12 +1,12 @@
#ifndef LDDSTATE_H
#define LDDSTATE_H
-#include <sylvan.h>
+
#include <set>
#include <vector>
#include <string>
-
+#include "SylvanWrapper.h"
using namespace std;
-using namespace sylvan;
+
typedef set<int> Set;
class LDDState {
@@ -34,7 +34,7 @@ class LDDState {
bool isVirtual() {return m_virtual;}
void setVirtual(){m_virtual=true;}
void setDiv(bool di) {m_boucle=di;}
- bool isDiv() {return m_boucle;}
+ inline bool isDiv() {return m_boucle;}
void setDeadLock(bool de) {m_blocage=de;}
bool isDeadLock() {return m_blocage;}
inline void setVisited() {m_visited=true;}
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index 7986e0506a5aee8e2e213d158331ecee53ea4ecc..957c9cca2ed918b7f584d563d5120e86a4387acb 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -3,13 +3,9 @@
#include <cstdio>
-#include "sylvan_sog.h"
-#include "sylvan_seq.h"
-#include <sylvan_int.h>
-#include "SylvanWrapper.h"
#include <openssl/md5.h>
-#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
+
#define LENGTH_ID 16
//#define LENGTH_MSG 180
@@ -25,25 +21,19 @@
#define TAG_ACK_SUCC 11
#define TAG_NOTCOMPLETED 20
//#define DEBUG_GC 1
-using namespace sylvan;
+
using namespace std;
MCHybridSOG::MCHybridSOG ( const NewNet &R,MPI_Comm &comm_world,bool init )
{
m_comm_world=comm_world;
- lace_init ( 1, 0 );
- lace_startup ( 0, NULL, NULL );
-
- //sylvan_set_limits ( 16LL<<30, 8, 0 );
- sylvan_set_limits ( 16LL<<30, 8, 0 );
-
- //sylvan_set_limits ( 2LL<<31, 2, 1 ); // sylvan_set_limits(2LL<<31, 2, 1);
- //sylvan_set_sizes(1LL<<27, 1LL<<31, 1LL<<20, 1LL<<22);
+ SylvanWrapper::sylvan_set_limits ( 16LL<<30, 8, 0 );
- sylvan_init_package();
- sylvan_init_ldd();
- sylvan_gc_enable();
- displayMDDTableInfo();
+ //sylvan_init_package();
+ SylvanWrapper::sylvan_init_package();
+ SylvanWrapper::sylvan_init_ldd();
+ SylvanWrapper::init_gc_seq();
+ SylvanWrapper::displayMDDTableInfo();
m_net=&R;
m_init=init;
@@ -51,14 +41,14 @@ MCHybridSOG::MCHybridSOG ( const NewNet &R,MPI_Comm &comm_world,bool init )
int i, domain;
vector<Place>::const_iterator it_places;
- init_gc_seq();
+ //#init_gc_seq();
//_______________
m_transitions=R.transitions;
m_observable=R.Observable;
m_nonObservable=R.NonObservable;
m_place_proposition=R.m_formula_place;
- m_transitionName=R.transitionName;
- m_placeName=R.m_placePosName;
+ m_transitionName=&R.transitionName;
+ m_placeName=&R.m_placePosName;
InterfaceTrans=R.InterfaceTrans;
m_nbPlaces=R.places.size();
@@ -70,8 +60,8 @@ MCHybridSOG::MCHybridSOG ( const NewNet &R,MPI_Comm &comm_world,bool init )
for ( i=0,it_places=R.places.begin(); it_places!=R.places.end(); i++,it_places++ ) {
liste_marques[i] =it_places->marking;
}
- m_initialMarking=lddmc_cube ( liste_marques,R.places.size() );
- ldd_refs_push ( m_initialMarking );
+ m_initialMarking=SylvanWrapper::lddmc_cube ( liste_marques,R.places.size() );
+ //#ldd_refs_push ( m_initialMarking );
delete []liste_marques;
// place names
@@ -102,11 +92,11 @@ MCHybridSOG::MCHybridSOG ( const NewNet &R,MPI_Comm &comm_world,bool init )
postc[it->first] = postc[it->first] + it->second;
}
- MDD _minus=lddmc_cube ( prec,m_nbPlaces );
- ldd_refs_push ( _minus );
+ MDD _minus=SylvanWrapper::lddmc_cube ( prec,m_nbPlaces );
+ //#ldd_refs_push ( _minus );
- MDD _plus=lddmc_cube ( postc,m_nbPlaces );
- ldd_refs_push ( _plus );
+ MDD _plus=SylvanWrapper::lddmc_cube ( postc,m_nbPlaces );
+ //#ldd_refs_push ( _plus );
m_tb_relation.push_back ( TransSylvan ( _minus,_plus ) );
}
//sylvan_gc_seq();
@@ -135,17 +125,21 @@ void *MCHybridSOG::doCompute()
/****************************************** initial state ********************************************/
if ( task_id==0 && id_thread==0 ) {
string* chaine=new string();
+
+
LDDState *c=new LDDState;
MDD Complete_meta_state=Accessible_epsilon ( m_initialMarking );
c->m_lddstate=Complete_meta_state;
- ldd_refs_push ( Complete_meta_state );
+ //#ldd_refs_push ( Complete_meta_state );
// MDD reduced_initialstate=Canonize(Complete_meta_state,0);
- convert_wholemdd_stringcpp ( Complete_meta_state,*chaine );
+
+ SylvanWrapper::convert_wholemdd_stringcpp ( Complete_meta_state,*chaine );
get_md5 ( *chaine,Identif );
//lddmc_getsha(Complete_meta_state, Identif);
uint16_t destination= ( uint16_t ) ( Identif[0]%n_tasks );
c->setProcess ( destination );
if ( destination==0 ) {
+
m_nbmetastate++;
Set fire=firable_obs ( Complete_meta_state );
m_st[1].push ( Pair ( couple ( c,Complete_meta_state ),fire ) );
@@ -159,8 +153,11 @@ void *MCHybridSOG::doCompute()
m_graph->insertSHA ( c );
memcpy ( c->m_SHA2,Identif,16 );
initialstate=Canonize ( Complete_meta_state,0 );
+
//#endif // REDUCE
- convert_wholemdd_stringcpp ( initialstate,*chaine );
+ SylvanWrapper::convert_wholemdd_stringcpp ( initialstate,*chaine );
+
+
pthread_mutex_lock ( &m_spin_msg[0] );
m_msg[0].push ( MSG ( chaine,destination ) );
pthread_mutex_unlock ( &m_spin_msg[0] );
@@ -229,18 +226,20 @@ void *MCHybridSOG::doCompute()
int t = * ( e.second.begin() );
e.second.erase ( t );
reached_class=new LDDState();
+
+
MDD ldd_reachedclass=Accessible_epsilon ( get_successor ( e.first.second,t ) );
- ldd_refs_push ( ldd_reachedclass );
+ //#ldd_refs_push ( ldd_reachedclass );
if ( id_thread==1 )
//displayMDDTableInfo();
- if ( isGCRequired() ) {
+ if ( SylvanWrapper::isGCRequired() ) {
m_gc_mutex.lock();
#ifdef DEBUG_GC
displayMDDTableInfo();
#endif // DEBUG_GC
- sylvan_gc_seq();
+ // sylvan_gc_seq();
#ifdef DEBUG_GC
displayMDDTableInfo();
@@ -258,7 +257,7 @@ void *MCHybridSOG::doCompute()
//MDD Reduced=ldd_reachedclass;
string* message_to_send1=new string();
- convert_wholemdd_stringcpp ( ldd_reachedclass,*message_to_send1 );
+ SylvanWrapper::convert_wholemdd_stringcpp ( ldd_reachedclass,*message_to_send1 );
get_md5 ( *message_to_send1,Identif );
@@ -312,12 +311,12 @@ void *MCHybridSOG::doCompute()
#ifndef REDUCE
reached=Canonize ( ldd_reachedclass,0 );
- ldd_refs_push ( ldd_reachedclass );
+//# ldd_refs_push ( ldd_reachedclass );
#endif
//MDD Reduced=ldd_reachedclass;
string* message_to_send2=new string();
- convert_wholemdd_stringcpp ( reached,*message_to_send2 );
+ SylvanWrapper::convert_wholemdd_stringcpp ( reached,*message_to_send2 );
m_graph->addArc();
m_graph_mutex.lock();
e.first.first->Successors.insert ( e.first.first->Successors.begin(),LDDEdge ( reached_class,t ) );
@@ -359,13 +358,13 @@ void *MCHybridSOG::doCompute()
Agregate->m_lddstate=MState;
if ( !m_graph->insertFind( Agregate ) ) {
//cout<<"enter D"<<endl;
- ldd_refs_push ( MState );
+ //#ldd_refs_push ( MState );
Agregate->setDiv ( Set_Div ( MState ) );
Agregate->setDeadLock ( Set_Bloc ( MState ) );
Agregate->setProcess ( task_id );
//m_graph_mutex.lock();
string* chaine=new string();
- convert_wholemdd_stringcpp ( MState,*chaine );
+ SylvanWrapper::convert_wholemdd_stringcpp ( MState,*chaine );
get_md5 ( *chaine,Identif );
delete chaine;
memcpy ( Agregate->m_SHA2,Identif,16 );
@@ -416,15 +415,15 @@ void MCHybridSOG::read_message()
//cout<<"message tag :"<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
if ( m_status.MPI_TAG==TAG_ASK_STATE ) {
//cout<<"TAG ASKSTATE received by task "<<task_id<<" from "<<m_status.MPI_SOURCE<<endl;
- char mess[25];
+ char mess[17];
MPI_Recv ( mess,16,MPI_BYTE,m_status.MPI_SOURCE,m_status.MPI_TAG,MPI_COMM_WORLD,&m_status );
bool res;
m_waitingAgregate=false;
size_t pos=m_graph->findSHAPos ( mess,res );
if ( !res ) {
-
+ //cout<<"Not found"<<endl;
m_waitingAgregate=true;
- memcpy ( m_id_md5,mess,16 ); // Added for stats
+ memcpy ( m_id_md5,mess,16 );
} else {
sendPropToMC ( pos );
}
@@ -471,7 +470,6 @@ void MCHybridSOG::read_message()
// cout<<"TAG INITIAL received by task "<<task_id<<endl;
MPI_Recv ( &v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status );
LDDState *i_agregate=m_graph->getInitialState();
-
char message[22];
memcpy ( message,i_agregate->getSHAValue(),16 );
uint16_t id_p=i_agregate->getProcess();
@@ -638,8 +636,8 @@ MDD MCHybridSOG::decodage_message ( const char *chaine )
list_marq[j]= ( uint32_t ) ( ( unsigned char ) chaine[index]-1 );
index++;
}
- MDD N=lddmc_cube ( list_marq,m_nbPlaces );
- M=lddmc_union_mono ( M,N );
+ MDD N=SylvanWrapper::lddmc_cube ( list_marq,m_nbPlaces );
+ M=SylvanWrapper::lddmc_union_mono ( M,N );
}
return M;
}
@@ -649,44 +647,7 @@ void * MCHybridSOG::threadHandler ( void *context )
return ( ( MCHybridSOG* ) context )->doCompute();
}
-void MCHybridSOG::convert_wholemdd_stringcpp ( MDD cmark,string &res )
-{
- typedef pair<string,MDD> Pair_stack;
- vector<Pair_stack> local_stack;
-
- unsigned int compteur=0;
- MDD explore_mdd=cmark;
-
- string chaine;
-
- res=" ";
- local_stack.push_back ( Pair_stack ( chaine,cmark ) );
- do {
- Pair_stack element=local_stack.back();
- chaine=element.first;
- explore_mdd=element.second;
- local_stack.pop_back();
- compteur++;
- while ( explore_mdd!= lddmc_false && explore_mdd!=lddmc_true ) {
- mddnode_t n_val = GETNODE ( explore_mdd );
- if ( mddnode_getright ( n_val ) !=lddmc_false ) {
- local_stack.push_back ( Pair_stack ( chaine,mddnode_getright ( n_val ) ) );
- }
- unsigned int val = mddnode_getvalue ( n_val );
- chaine.push_back ( ( unsigned char ) ( val )+1 );
- explore_mdd=mddnode_getdown ( n_val );
- }
- /*printchaine(&chaine);printf("\n");*/
- res+=chaine;
- } while ( local_stack.size() !=0 );
- //delete chaine;
-
- compteur= ( compteur<<1 ) | 1;
- res[1]= ( unsigned char ) ( ( compteur>>8 )+1 );
- res[0]= ( unsigned char ) ( compteur & 255 );
-
-}
void MCHybridSOG::get_md5 ( const string& chaine,unsigned char *md_chaine )
@@ -722,7 +683,7 @@ void MCHybridSOG::sendSuccToMC()
MPI_Send ( mess_tosend,message_size,MPI_BYTE,n_tasks, TAG_ACK_SUCC,MPI_COMM_WORLD );
}
-
+/*
set<uint16_t> MCHybridSOG::getMarkedPlaces ( LDDState *agg )
{
set<uint16_t> result;
@@ -741,8 +702,9 @@ set<uint16_t> MCHybridSOG::getMarkedPlaces ( LDDState *agg )
}
return result;
-}
+}*/
+/*
set<uint16_t> MCHybridSOG::getUnmarkedPlaces ( LDDState *agg )
{
set<uint16_t> result;
@@ -763,17 +725,16 @@ set<uint16_t> MCHybridSOG::getUnmarkedPlaces ( LDDState *agg )
}
return result;
-}
+}*/
// Send propositions to Model checker
void MCHybridSOG::sendPropToMC ( size_t pos )
{
LDDState *agg=m_graph->getLDDStateById ( pos );
- uint64_t size=SylvanWrapper::getMarksCount(agg->m_lddstate); // Added for stats
- set<uint16_t> marked_places=getMarkedPlaces ( agg );
- set<uint16_t> unmarked_places=getUnmarkedPlaces ( agg );
+ vector<uint16_t> marked_places=agg->getMarkedPlaces ( m_place_proposition );
+ vector<uint16_t> unmarked_places=agg->getUnmarkedPlaces ( m_place_proposition );
uint16_t s_mp=marked_places.size();
uint16_t s_up=unmarked_places.size();
- char mess_to_send[8+s_mp*2+s_up*2+5+8]; // 8 Added for stats
+ char mess_to_send[8+s_mp*2+s_up*2+5];
memcpy ( mess_to_send,&pos,8 );
//cout<<"************* Pos to send :"<<pos<<endl;
size_t indice=8;
@@ -793,7 +754,5 @@ void MCHybridSOG::sendPropToMC ( size_t pos )
divblock=divblock | ( agg->isDeadLock() <<1 );
memcpy ( mess_to_send+indice,&divblock,1 );
indice++;
- memcpy(mess_to_send+indice,&size,8); // Added for stats
- indice+=8;
MPI_Send ( mess_to_send,indice,MPI_BYTE,n_tasks, TAG_ACK_STATE, MPI_COMM_WORLD );
}
diff --git a/src/MCHybridSOG.h b/src/MCHybridSOG.h
index b4e5c3fef766e288b098dd0cb5c30e6312bcfa34..db2b5c5a644b2a49db8d9ff361044d553c7714af 100644
--- a/src/MCHybridSOG.h
+++ b/src/MCHybridSOG.h
@@ -89,10 +89,9 @@ private:
// int n_tasks, task_id;
int m_charge[128];
- int m_init;
+ int m_init;
+
- /// Convert an MDD to a string caracter (for the send)
- void convert_wholemdd_stringcpp(MDD cmark, string &chaine);
/// Convert a string caracter to an MDD
MDD decodage_message(const char *chaine);
/// there is a message to receive?
@@ -117,8 +116,8 @@ private:
int m_nbsend = 0, m_nbrecv = 0;
MPI_Status m_status;
- set<uint16_t> getUnmarkedPlaces(LDDState *agg);
- set<uint16_t> getMarkedPlaces(LDDState *agg);
+ /*set<uint16_t> getUnmarkedPlaces(LDDState *agg);
+ set<uint16_t> getMarkedPlaces(LDDState *agg);*/
};
diff --git a/src/ModelCheckBaseMT.cpp b/src/ModelCheckBaseMT.cpp
index c756b69a27eb522eff4c54fe0c0940b662f2ea7e..5a5d01fd343cf72bb06a385cd5e6094b24c1ca28 100644
--- a/src/ModelCheckBaseMT.cpp
+++ b/src/ModelCheckBaseMT.cpp
@@ -1,11 +1,7 @@
#include "ModelCheckBaseMT.h"
-#include "sylvan.h"
-#include "sylvan_seq.h"
-#include <sylvan_sog.h>
-#include <sylvan_int.h>
+#include "SylvanWrapper.h"
-using namespace sylvan;
ModelCheckBaseMT::ModelCheckBaseMT(const NewNet &R,int nbThread)
{
m_nb_thread=nbThread;
@@ -16,8 +12,8 @@ void ModelCheckBaseMT::loadNet()
{
m_graph=new LDDGraph(this);
preConfigure();
- m_graph->setTransition(m_transitionName);
- m_graph->setPlace(m_placeName);
+ m_graph->setTransition(*m_transitionName);
+ m_graph->setPlace(*m_placeName);
}
ModelCheckBaseMT::~ModelCheckBaseMT()
diff --git a/src/ModelCheckerCPPThread.cpp b/src/ModelCheckerCPPThread.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..d49fb1966f18c9adf158a4e8d4c930b8ac687a0b
--- /dev/null
+++ b/src/ModelCheckerCPPThread.cpp
@@ -0,0 +1,218 @@
+#include "ModelCheckerCPPThread.h"
+//#include "sylvan.h"
+//#include <sylvan_int.h>
+#include <functional>
+#include <iostream>
+#include <unistd.h>
+
+#include "SylvanWrapper.h"
+#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
+
+using namespace std;
+
+ModelCheckerCPPThread::ModelCheckerCPPThread ( const NewNet &R, int nbThread ) :
+ ModelCheckBaseMT ( R, nbThread )
+{
+}
+size_t
+getMaxMemoryV3()
+{
+ long pages = sysconf ( _SC_PHYS_PAGES );
+ long page_size = sysconf ( _SC_PAGE_SIZE );
+ return pages * page_size;
+}
+void ModelCheckerCPPThread::preConfigure()
+{
+
+ /*lace_init ( 1, 0 );
+ lace_startup ( 0, NULL, NULL );
+ size_t max = 16LL<<34;
+ if ( max > getMaxMemoryV3() ) {
+ max = getMaxMemoryV3() /10*9;
+ }*/
+ SylvanWrapper::sylvan_set_limits ( 16LL<<30, 8, 0 );
+
+ //sylvan_init_package();
+ SylvanWrapper::sylvan_init_package();
+ SylvanWrapper::sylvan_init_ldd();
+ SylvanWrapper::init_gc_seq();
+ SylvanWrapper::displayMDDTableInfo();
+
+ vector<Place>::const_iterator it_places;
+ m_transitions = m_net->transitions;
+ m_observable = m_net->Observable;
+ m_place_proposition = m_net->m_formula_place;
+ m_nonObservable = m_net->NonObservable;
+
+ m_transitionName = &m_net->transitionName;
+ m_placeName = &m_net->m_placePosName;
+
+ InterfaceTrans = m_net->InterfaceTrans;
+
+ cout << "Nombre de places : " << m_nbPlaces << endl;
+ cout << "Derniere place : " << m_net->places[m_nbPlaces - 1].name << endl;
+
+ uint32_t *liste_marques = new uint32_t[m_net->places.size()];
+ uint32_t i;
+ for ( i = 0, it_places = m_net->places.begin(); it_places != m_net->places.end(); i++, it_places++ ) {
+ liste_marques[i] = it_places->marking;
+ }
+
+ m_initialMarking = SylvanWrapper::lddmc_cube ( liste_marques, m_net->places.size() );
+
+ SylvanWrapper::lddmc_refs_push ( m_initialMarking );
+ uint32_t *prec = new uint32_t[m_nbPlaces];
+ uint32_t *postc = new uint32_t[m_nbPlaces];
+ // Transition relation
+ for ( vector<Transition>::const_iterator t = m_net->transitions.begin(); t != m_net->transitions.end(); t++ ) {
+ // Initialisation
+ for ( i = 0; i < m_nbPlaces; i++ ) {
+ prec[i] = 0;
+ postc[i] = 0;
+ }
+ // Calculer les places adjacentes a la transition t
+ set<int> adjacentPlace;
+ for ( vector<pair<int, int> >::const_iterator it = t->pre.begin(); it != t->pre.end(); it++ ) {
+ adjacentPlace.insert ( it->first );
+ prec[it->first] = prec[it->first] + it->second;
+ //printf("It first %d \n",it->first);
+ //printf("In prec %d \n",prec[it->first]);
+ }
+ // arcs post
+ for ( vector<pair<int, int> >::const_iterator it = t->post.begin(); it != t->post.end(); it++ ) {
+ adjacentPlace.insert ( it->first );
+ postc[it->first] = postc[it->first] + it->second;
+
+ }
+ for ( set<int>::const_iterator it = adjacentPlace.begin(); it != adjacentPlace.end(); it++ ) {
+ MDD Precond = lddmc_true;
+ Precond = Precond & ( ( *it ) >= prec[*it] );
+ }
+
+ MDD _minus = SylvanWrapper::lddmc_cube ( prec, m_nbPlaces );
+ SylvanWrapper::lddmc_refs_push ( _minus );
+ MDD _plus = SylvanWrapper::lddmc_cube ( postc, m_nbPlaces );
+ SylvanWrapper::lddmc_refs_push ( _plus );
+ m_tb_relation.push_back ( TransSylvan ( _minus, _plus ) );
+ }
+ delete[] prec;
+ delete[] postc;
+ ComputeTh_Succ();
+
+
+}
+
+
+
+
+void ModelCheckerCPPThread::Compute_successors()
+{
+ int id_thread;
+
+ id_thread = m_id_thread++;
+
+ //cout<<" I'm here thread id " <<m_id_thread<<endl;
+ Set fire;
+
+ if ( id_thread == 0 ) {
+ LDDState *c = new LDDState;
+ MDD Complete_meta_state=Accessible_epsilon ( m_initialMarking );
+ /*SylvanWrapper::getMarksCount(Complete_meta_state);
+ exit(0);*/
+
+ SylvanWrapper::lddmc_refs_push ( Complete_meta_state );
+
+ fire = firable_obs ( Complete_meta_state );
+ c->m_lddstate = Complete_meta_state;
+ c->setDeadLock ( Set_Bloc ( Complete_meta_state ) );
+ c->setDiv ( Set_Div ( Complete_meta_state ) );
+ m_graph->setInitialState ( c );
+ m_graph->insert ( c );
+ m_common_stack.push ( Pair ( couple ( c, Complete_meta_state ), fire ) );
+ m_condStack.notify_one();
+ m_finish_initial = true;
+ }
+ LDDState *reached_class;
+ //pthread_barrier_wait ( &m_barrier_builder );
+ Pair e;
+ do {
+ std::unique_lock<std::mutex> lk ( m_mutexStack );
+ m_condStack.wait(lk,std::bind(&ModelCheckerCPPThread::hasToProcess,this));
+ lk.unlock();
+
+ if ( m_common_stack.try_pop ( e ) && !m_finish ) {
+ while ( !e.second.empty() && !m_finish ) {
+ int t = *e.second.begin();
+ e.second.erase ( t );
+ MDD reduced_meta = Accessible_epsilon ( get_successor ( e.first.second, t ) );
+ SylvanWrapper::lddmc_refs_push ( reduced_meta );
+ reached_class = new LDDState();
+ reached_class->m_lddstate = reduced_meta;
+ LDDState *pos = m_graph->find ( reached_class );
+ if ( !pos ) {
+ m_graph->addArc();
+ m_graph->insert ( reached_class );
+ fire = firable_obs ( reduced_meta );
+ reached_class->setDeadLock ( Set_Bloc ( reduced_meta ) );
+ reached_class->setDiv ( Set_Div ( reduced_meta ) );
+ m_common_stack.push ( Pair ( couple ( reached_class, reduced_meta ), fire ) );
+ m_condStack.notify_one();
+ m_graph_mutex.lock();
+ e.first.first->Successors.insert ( e.first.first->Successors.begin(), LDDEdge ( reached_class, t ) );
+ reached_class->Predecessors.insert ( reached_class->Predecessors.begin(), LDDEdge ( e.first.first, t ) );
+ m_graph_mutex.unlock();
+ } else {
+ delete reached_class;
+ m_graph->addArc();
+ m_graph_mutex.lock();
+ e.first.first->Successors.insert ( e.first.first->Successors.begin(), LDDEdge ( pos, t ) );
+ pos->Predecessors.insert ( pos->Predecessors.begin(), LDDEdge ( e.first.first, t ) );
+ m_graph_mutex.unlock();
+ }
+
+ }
+ e.first.first->setCompletedSucc();m_condBuild.notify_one();
+ } //end advance
+
+ } while ( !m_finish );
+
+
+}
+
+void ModelCheckerCPPThread::threadHandler ( void *context )
+{
+ SylvanWrapper::lddmc_refs_init();
+ ( ( ModelCheckerCPPThread* ) context )->Compute_successors();
+}
+
+void ModelCheckerCPPThread::ComputeTh_Succ()
+{
+
+ m_id_thread = 0;
+
+ pthread_barrier_init ( &m_barrier_builder, NULL, m_nb_thread + 1 );
+
+ m_finish=false;
+ for ( int i = 0; i < m_nb_thread; i++ ) {
+ int rc;
+ m_list_thread[i]= new thread ( threadHandler,this );
+ if ( m_list_thread==nullptr ) {
+ cout << "error: pthread_create, rc: " << rc << endl;
+ }
+ }
+}
+
+ModelCheckerCPPThread::~ModelCheckerCPPThread()
+{
+ m_finish = true;
+ m_condStack.notify_all();
+ //pthread_barrier_wait ( &m_barrier_builder );
+ for ( int i = 0; i < m_nb_thread; i++ ) {
+ m_list_thread[i]->join();
+ delete m_list_thread[i];
+ }
+
+}
+bool ModelCheckerCPPThread::hasToProcess() const {
+ return m_finish || !m_common_stack.empty();
+}
diff --git a/src/ModelCheckerCPPThread.h b/src/ModelCheckerCPPThread.h
new file mode 100644
index 0000000000000000000000000000000000000000..204e6c085fba978f3ad41ec5b6f8479c62e8dee2
--- /dev/null
+++ b/src/ModelCheckerCPPThread.h
@@ -0,0 +1,36 @@
+#ifndef ModelCheckerCPPThread_H
+#define ModelCheckerCPPThread_H
+#include "ModelCheckBaseMT.h"
+#include "stacksafe.h"
+#include "SafeDequeue.h"
+#include <atomic>
+#include <thread>
+#include <mutex>
+#include <condition_variable>
+typedef pair<LDDState *, int> couple_th;
+typedef stack<pair<LDDState *,int>> pile_t;
+/*
+ * Multi-threading with C++14 Library
+ */
+class ModelCheckerCPPThread : public ModelCheckBaseMT
+{
+public:
+ ModelCheckerCPPThread(const NewNet &R,int nbThread);
+ ~ModelCheckerCPPThread();
+ static void threadHandler(void *context);
+ void Compute_successors();
+ void ComputeTh_Succ();
+private:
+ void preConfigure();
+ bool hasToProcess() const;
+
+ SafeDequeue<Pair> m_common_stack;
+ atomic<uint8_t> m_id_thread;
+ std::mutex m_mutex;
+ pthread_barrier_t m_barrier_builder;
+ volatile bool m_finish=false;
+ std::condition_variable m_condStack;
+ std::mutex m_mutexStack;
+ thread* m_list_thread[128];
+};
+#endif
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 10ce48cc82ace9b3f71c478295c62b4074d5c8ed..397209979bd5112387319491a8e816df1dc2c6af 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -1,11 +1,6 @@
#include "ModelCheckerTh.h"
+#include <unistd.h>
-#include "sylvan.h"
-#include "sylvan_seq.h"
-#include <sylvan_sog.h>
-#include <sylvan_int.h>
-
-using namespace sylvan;
ModelCheckerTh::ModelCheckerTh(const NewNet &R, int nbThread) :
ModelCheckBaseMT(R, nbThread) {
@@ -19,19 +14,15 @@ getMaxMemory()
}
void ModelCheckerTh::preConfigure() {
- lace_init(1, 0);
- lace_startup(0, NULL, NULL);
- size_t max = 16LL<<30;
- if (max > getMaxMemory()) max = getMaxMemory()/10*9;
- sylvan_set_limits(16LL<<29, 8, 0);
-
- sylvan_init_package();
- sylvan_init_ldd();
- displayMDDTableInfo();
+ SylvanWrapper::sylvan_set_limits ( 16LL<<29, 8, 0 );
+ SylvanWrapper::sylvan_init_package();
+ SylvanWrapper::sylvan_init_ldd();
+ SylvanWrapper::init_gc_seq();
+ SylvanWrapper::displayMDDTableInfo();
vector<Place>::const_iterator it_places;
- init_gc_seq();
+ //init_gc_seq();
m_transitions = m_net->transitions;
@@ -39,8 +30,8 @@ void ModelCheckerTh::preConfigure() {
m_place_proposition = m_net->m_formula_place;
m_nonObservable = m_net->NonObservable;
- m_transitionName = m_net->transitionName;
- m_placeName = m_net->m_placePosName;
+ m_transitionName = &m_net->transitionName;
+ m_placeName = &m_net->m_placePosName;
InterfaceTrans = m_net->InterfaceTrans;
@@ -53,8 +44,8 @@ void ModelCheckerTh::preConfigure() {
liste_marques[i] = it_places->marking;
}
- m_initialMarking = lddmc_cube(liste_marques, m_net->places.size());
- ldd_refs_push(m_initialMarking);
+ m_initialMarking = SylvanWrapper::lddmc_cube(liste_marques, m_net->places.size());
+ //ldd_refs_push(m_initialMarking);
uint32_t *prec = new uint32_t[m_nbPlaces];
uint32_t *postc = new uint32_t[m_nbPlaces];
// Transition relation
@@ -83,10 +74,10 @@ void ModelCheckerTh::preConfigure() {
Precond = Precond & ((*it) >= prec[*it]);
}
- MDD _minus = lddmc_cube(prec, m_nbPlaces);
- ldd_refs_push(_minus);
- MDD _plus = lddmc_cube(postc, m_nbPlaces);
- ldd_refs_push(_plus);
+ MDD _minus = SylvanWrapper::lddmc_cube(prec, m_nbPlaces);
+ //#ldd_refs_push(_minus);
+ MDD _plus = SylvanWrapper::lddmc_cube(postc, m_nbPlaces);
+ //#ldd_refs_push(_plus);
m_tb_relation.push_back(TransSylvan(_minus, _plus));
}
delete[] prec;
@@ -104,7 +95,7 @@ void* ModelCheckerTh::Compute_successors() {
if (id_thread == 0) {
LDDState *c = new LDDState;
MDD Complete_meta_state=Accessible_epsilon(m_initialMarking);
- ldd_refs_push(Complete_meta_state);
+ //#ldd_refs_push(Complete_meta_state);
fire = firable_obs(Complete_meta_state);
c->m_lddstate = Complete_meta_state;
@@ -150,7 +141,7 @@ void* ModelCheckerTh::Compute_successors() {
}
#endif
MDD reduced_meta = Accessible_epsilon(get_successor(e.first.second, t));
- ldd_refs_push(reduced_meta);
+ //#ldd_refs_push(reduced_meta);
reached_class = new LDDState();
reached_class->m_lddstate = reduced_meta;
//pthread_spin_lock(&m_accessible);
@@ -253,4 +244,3 @@ bool ModelCheckerTh::isNotTerminated() {
}
return !res;
}
-
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index 23fb2923d9634409bf1bef6f8fcb852dcdafdcaa..a94b6c74b01c45a2b71d10f9ce6360683dd95748 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -14,7 +14,6 @@ public:
static void *threadHandler(void *context);
void *Compute_successors();
void ComputeTh_Succ();
-
private:
void preConfigure();
bool isNotTerminated();
diff --git a/src/NewNet.cpp b/src/NewNet.cpp
index 5b2e4b6c51ff7f3cbc3244ffcffdd2f063edf6c3..b73c7574631b6e82200d4e184fa799ea981266a7 100644
--- a/src/NewNet.cpp
+++ b/src/NewNet.cpp
@@ -84,7 +84,7 @@ NewNet::NewNet(const char *f, const char *Formula_trans, const char *Int_trans)
{
places.clear();
transitions.clear();
- placeName.clear();
+ m_placeName.clear();
transitionName.clear();
}
if (strlen(Formula_trans) > 0)
@@ -132,7 +132,7 @@ NewNet::NewNet(const char *f, const set<string> & f_trans)
{
places.clear();
transitions.clear();
- placeName.clear();
+ m_placeName.clear();
transitionName.clear();
}
if (f_trans.size() > 0)
@@ -165,7 +165,7 @@ void NewNet::setListObservable(const set<string> & list_t)
{
int pos_trans(TRANSITIONS T, string trans);
Observable.clear();
- for (auto it=placeName.begin();it!=placeName.end();it++) {
+ for (auto it=m_placeName.begin();it!=m_placeName.end();it++) {
pair<int,string> elt((*it).second,(*it).first);
m_placePosName.insert(elt);
}
@@ -183,9 +183,8 @@ void NewNet::setListObservable(const set<string> & list_t)
{
cout<<"Error: "<<*i<<" is not a transition!"<<endl;
// Check if the proposition corresponds to a place
- map<string, uint16_t>::iterator pi = placeName.find(*i);
- if (pi!=placeName.end())
- cout<<"Place was found!"<<endl;
+ map<string, uint16_t>::iterator pi = m_placeName.find(*i);
+ assert (pi!=m_placeName.end());
m_formula_place.insert(pi->second);
m_lplaceAP.insert(*i);
// Adding adjacent transitions of a place as observable transitions
@@ -207,7 +206,7 @@ void NewNet::setListObservable(const set<string> & list_t)
else
{
Formula_Trans.insert(pos);
- map<string,uint16_t>::iterator ti=transitionName.find(*i);
+ map<string ,uint16_t>::iterator ti=transitionName.find(*i);
Observable.insert(pos);
}
}
@@ -365,10 +364,10 @@ ostream &operator<<(ostream &os, const Set &s)
/*----------------------------------------------------------------------*/
bool NewNet::addPlace(const string &place, int marking, int capacity)
{
- map<string, uint16_t>::const_iterator pi = placeName.find(place);
- if (pi == placeName.end())
+ map<string , uint16_t>::const_iterator pi = m_placeName.find(place);
+ if (pi == m_placeName.end())
{
- placeName[place] = places.size();
+ m_placeName[string(place)] = places.size();
Place p(place, marking, capacity);
places.push_back(p);
return true;
@@ -379,10 +378,10 @@ bool NewNet::addPlace(const string &place, int marking, int capacity)
bool NewNet::addQueue(const string &place, int capacity)
{
- map<string, uint16_t>::const_iterator pi = placeName.find(place);
- if (pi == placeName.end())
+ map<string , uint16_t>::const_iterator pi = m_placeName.find(place);
+ if (pi == m_placeName.end())
{
- placeName[place] = places.size();
+ m_placeName[place] = places.size();
Place p(place, -1, capacity);
places.push_back(p);
return true;
@@ -393,10 +392,10 @@ bool NewNet::addQueue(const string &place, int capacity)
bool NewNet::addLossQueue(const string &place, int capacity)
{
- map<string, uint16_t>::const_iterator pi = placeName.find(place);
- if (pi == placeName.end())
+ map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
+ if (pi == m_placeName.end())
{
- placeName[place] = places.size();
+ m_placeName[place] = places.size();
Place p(place, -2, capacity);
places.push_back(p);
return true;
@@ -422,8 +421,8 @@ bool NewNet::addTrans(const string &trans)
bool NewNet::addPre(const string &place, const string &trans, int valuation)
{
int p, t;
- map<string, uint16_t>::const_iterator pi = placeName.find(place);
- if (pi == placeName.end() || places[pi->second].isQueue())
+ map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
+ if (pi == m_placeName.end() || places[pi->second].isQueue())
return false;
else
p = pi->second;
@@ -440,8 +439,8 @@ bool NewNet::addPre(const string &place, const string &trans, int valuation)
bool NewNet::addPost(const string &place, const string &trans, int valuation)
{
int p, t;
- map<string, uint16_t>::const_iterator pi = placeName.find(place);
- if (pi == placeName.end() || places[pi->second].isQueue())
+ map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
+ if (pi == m_placeName.end() || places[pi->second].isQueue())
return false;
else
p = pi->second;
@@ -458,12 +457,12 @@ bool NewNet::addPost(const string &place, const string &trans, int valuation)
bool NewNet::addPreQueue(const string &place, const string &trans, int valuation)
{
int p, t;
- map<string, uint16_t>::const_iterator pi = placeName.find(place);
- if (pi == placeName.end() || !places[pi->second].isQueue())
+ map<string , uint16_t>::const_iterator pi = m_placeName.find(place);
+ if (pi == m_placeName.end() || !places[pi->second].isQueue())
return false;
else
p = pi->second;
- map<string, uint16_t>::const_iterator ti = transitionName.find(trans);
+ map<string , uint16_t>::const_iterator ti = transitionName.find(trans);
if (ti == transitionName.end())
return false;
else
@@ -477,12 +476,12 @@ bool NewNet::addPostQueue(const string &place, const string &trans,
int valuation)
{
int p, t;
- map<string, uint16_t>::const_iterator pi = placeName.find(place);
- if (pi == placeName.end() || !places[pi->second].isQueue())
+ map<string , uint16_t>::const_iterator pi = m_placeName.find(place);
+ if (pi == m_placeName.end() || !places[pi->second].isQueue())
return false;
else
p = pi->second;
- map<string, uint16_t>::const_iterator ti = transitionName.find(trans);
+ map<string , uint16_t>::const_iterator ti = transitionName.find(trans);
if (ti == transitionName.end())
return false;
else
@@ -496,8 +495,8 @@ bool NewNet::addInhibitor(const string &place, const string &trans,
int valuation)
{
int p, t;
- map<string, uint16_t>::const_iterator pi = placeName.find(place);
- if (pi == placeName.end())
+ map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
+ if (pi == m_placeName.end())
return false;
else
p = pi->second;
@@ -515,8 +514,8 @@ bool NewNet::addPreAuto(const string &place, const string &trans,
const string &valuation)
{
int p, t, v;
- map<string, uint16_t>::const_iterator pi = placeName.find(place);
- if (pi == placeName.end() || places[pi->second].isQueue())
+ map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
+ if (pi == m_placeName.end() || places[pi->second].isQueue())
return false;
else
p = pi->second;
@@ -525,8 +524,8 @@ bool NewNet::addPreAuto(const string &place, const string &trans,
return false;
else
t = ti->second;
- map<string, uint16_t>::const_iterator pv = placeName.find(valuation);
- if (pv == placeName.end() || places[pv->second].isQueue())
+ map<string, uint16_t>::const_iterator pv = m_placeName.find(valuation);
+ if (pv == m_placeName.end() || places[pv->second].isQueue())
return false;
else
v = pv->second;
@@ -539,8 +538,8 @@ bool NewNet::addPostAuto(const string &place, const string &trans,
const string &valuation)
{
int p, t, v;
- map<string, uint16_t>::const_iterator pi = placeName.find(place);
- if (pi == placeName.end() || places[pi->second].isQueue())
+ map<string, uint16_t>::const_iterator pi = m_placeName.find(place);
+ if (pi == m_placeName.end() || places[pi->second].isQueue())
return false;
else
p = pi->second;
@@ -549,8 +548,8 @@ bool NewNet::addPostAuto(const string &place, const string &trans,
return false;
else
t = ti->second;
- map<string, uint16_t>::const_iterator pv = placeName.find(valuation);
- if (pv == placeName.end() || places[pi->second].isQueue())
+ map<string, uint16_t>::const_iterator pv = m_placeName.find(valuation);
+ if (pv == m_placeName.end() || places[pi->second].isQueue())
return false;
else
v = pv->second;
@@ -562,8 +561,8 @@ bool NewNet::addPostAuto(const string &place, const string &trans,
bool NewNet::addReset(const string &place, const string &trans)
{
int p, t;
- auto pi = placeName.find(place);
- if (pi == placeName.end())
+ auto pi = m_placeName.find(place);
+ if (pi == m_placeName.end())
return false;
else
p = pi->second;
diff --git a/src/NewNet.h b/src/NewNet.h
index 8341cf38abf3fbd2be968cfc56401652bcb2b265..d394cc8e3754fe2326c6a6f7821ebdc18596404a 100644
--- a/src/NewNet.h
+++ b/src/NewNet.h
@@ -69,7 +69,7 @@ class NewNet : public RdPMonteur {
/* Attributs */
vector<class Place> places;
vector<class Transition> transitions;
- map<string, uint16_t> placeName;
+ map<string, uint16_t> m_placeName;
map<string, uint16_t> transitionName;
Set Observable;
Set NonObservable;
@@ -106,14 +106,13 @@ class NewNet : public RdPMonteur {
int nbTransition() const { return transitions.size(); };
set<string>& getListTransitionAP() {return m_ltransitionAP;}
set<string>& getListPlaceAP() {return m_lplaceAP;}
- string& getPlaceName(size_t pos) { return m_placePosName.find(pos)->second;}
- string& getTransitionName(size_t pos) { return m_transitionPosName.find(pos)->second;}
+ string_view getPlaceName(size_t pos) { return m_placePosName.find(pos)->second;}
+ string_view getTransitionName(size_t pos) { return m_transitionPosName.find(pos)->second;}
map<uint16_t,string> m_placePosName;
private:
map<uint16_t,string> m_transitionPosName;
-
set<string> m_ltransitionAP;
set<string> m_lplaceAP;
diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp
index d8229149513944a4e85c1a209d11fc3778be760c..27bd925a14ac24d891e9c19c31db997d2cbb1c76 100644
--- a/src/SogKripke.cpp
+++ b/src/SogKripke.cpp
@@ -58,13 +58,13 @@ bdd SogKripke::state_condition(const spot::state* s) const
bdd result=bddtrue;
// Marked places
for (auto it=marked_place.begin();it!=marked_place.end();it++) {
- string name=m_sog->getPlace(*it);
+ string name=string(m_sog->getPlace(*it));
spot::formula f=spot::formula::ap(name);
result&=bdd_ithvar((dict_->var_map.find(f))->second);
}
vector<uint16_t> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_sog->getConstructor()->getPlaceProposition());
for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) {
- string name=m_sog->getPlace(*it);
+ string name=string(m_sog->getPlace(*it));
spot::formula f=spot::formula::ap(name);
result&=!bdd_ithvar((dict_->var_map.find(f))->second);
}
diff --git a/src/SogKripkeIterator.cpp b/src/SogKripkeIterator.cpp
index f7de0915f81eb897c7b40e16ea8c039dbf1779d3..0cd41ae59bb71dc3080a32db07e5313749eac7d0 100644
--- a/src/SogKripkeIterator.cpp
+++ b/src/SogKripkeIterator.cpp
@@ -45,7 +45,7 @@ SogKripkeState* SogKripkeIterator::dst() const
bdd SogKripkeIterator::cond() const {
if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
- string name=m_graph->getTransition(m_lsucc.at(m_current_edge).second);
+ string name=string(m_graph->getTransition(m_lsucc.at(m_current_edge).second));
//cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
spot::bdd_dict *p=m_dict_ptr->get();
diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
index 44356a32e7a64f8b0319f33a6720e2263f5a59e5..7b09c764d8bb9a01c1a0467b35acd5ac881d577d 100644
--- a/src/SogKripkeIteratorTh.cpp
+++ b/src/SogKripkeIteratorTh.cpp
@@ -54,10 +54,10 @@ bdd SogKripkeIteratorTh::cond() const
if ( m_lsucc.at ( m_current_edge ).second==-1 ) {
return bddtrue;
}
- string name=m_builder->getTransition ( m_lsucc.at ( m_current_edge ).second );
+ spot::formula f=spot::formula::ap (string(m_builder->getTransition ( m_lsucc.at ( m_current_edge ).second )));
spot::bdd_dict *p=m_dict_ptr->get();
- spot::formula f=spot::formula::ap ( name );
bdd result=bdd_ithvar ( ( p->var_map.find ( f ) )->second );
+ //cout<<"leaving "<<__func__<<endl;
return result & spot::kripke_succ_iterator::cond();
}
diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
index ee2f5bae67cf28feb7b60a9e78ba40f9ccb70c6c..6f727c434d6786e00ad90de87250be6d8d5f59e8 100644
--- a/src/SogKripkeTh.cpp
+++ b/src/SogKripkeTh.cpp
@@ -59,10 +59,10 @@ SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const {
bdd cond = state_condition(ss);
if (iter_cache_)
{
- auto it = static_cast<SogKripkeIteratorTh*>(iter_cache_);
+ /*auto it = static_cast<SogKripkeIteratorTh*>(iter_cache_);
iter_cache_ = nullptr; // empty the cache
it->recycle(aggregate, cond);
- return it;
+ return it;*/
}
return new SogKripkeIteratorTh(aggregate,cond);
@@ -81,20 +81,21 @@ bdd SogKripkeTh::state_condition(const spot::state* s) const
auto ss = static_cast<const SogKripkeStateTh*>(s);
vector<uint16_t> marked_place = ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
-
+#ifdef TESTENABLE
SylvanWrapper::m_Size+=SylvanWrapper::getMarksCount(ss->getLDDState()->getLDDValue());
SylvanWrapper::m_agg++;
cout<<"Expolored states : "<<SylvanWrapper::m_Size<<" , Explored agg : "<<SylvanWrapper::m_agg<<" , Avg per agg : " <<SylvanWrapper::m_Size/SylvanWrapper::m_agg<<endl;
+#endif
bdd result=bddtrue;
// Marked places
for (auto it=marked_place.begin();it!=marked_place.end();it++) {
- string name=m_builder->getPlace(*it);
+ string name=string(m_builder->getPlace(*it));
spot::formula f=spot::formula::ap(name);
result&=bdd_ithvar((dict_->var_map.find(f))->second);
}
vector<uint16_t> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_builder->getPlaceProposition());
for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) {
- string name=m_builder->getPlace(*it);
+ string name=string(m_builder->getPlace(*it));
spot::formula f=spot::formula::ap(name);
result&=!bdd_ithvar((dict_->var_map.find(f))->second);
}
diff --git a/src/SogKripkeTh.h b/src/SogKripkeTh.h
index 46c06ce67e8461050fecebef7082edb3189854e1..f482a0ea57793331960b2ae6c24e0a1cbaefc20e 100644
--- a/src/SogKripkeTh.h
+++ b/src/SogKripkeTh.h
@@ -17,14 +17,9 @@ class SogKripkeTh: public spot::kripke {
SogKripkeIteratorTh* succ_iter(const spot::state* s) const override;
std::string format_state(const spot::state* s) const override;
bdd state_condition(const spot::state* s) const override;
-
ModelCheckBaseMT *m_builder;
- protected:
- private:
- std::map<int, int> place_prop;
- //LDDGraph* m_sog;
};
#endif // SOGKRIPKE_H_INCLUDED
diff --git a/src/SogTwa.h b/src/SogTwa.h
index 5a39479ed0d8a71ebec8141115bb36ce3f343128..21a3a35d2d976533736f0ceb5c7f29598a60f87b 100644
--- a/src/SogTwa.h
+++ b/src/SogTwa.h
@@ -13,7 +13,6 @@ class SogTwa : public spot::twa
SpotSogIterator* succ_iter(const spot::state* s) const override;
std::string format_state(const spot::state* s) const override;
- protected:
private:
LDDGraph* m_sog;
diff --git a/src/SpotSogIterator.cpp b/src/SpotSogIterator.cpp
index 62b14d346834652a355a888de088864cfbe32862..ae61c6374b317de2060b94026dcbfdeb644b8d7f 100644
--- a/src/SpotSogIterator.cpp
+++ b/src/SpotSogIterator.cpp
@@ -45,7 +45,7 @@ SpotSogState* SpotSogIterator::dst() const
bdd SpotSogIterator::cond() const {
if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
- string name=m_graph->getTransition(m_lsucc.at(m_current_edge).second);
+ string name=string(m_graph->getTransition(m_lsucc.at(m_current_edge).second));
//cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
spot::bdd_dict *p=m_dict_ptr->get();
diff --git a/src/SylvanCacheWrapper.cpp b/src/SylvanCacheWrapper.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..83680b6dde6bf537993236c159faa4a9d3ca8c95
--- /dev/null
+++ b/src/SylvanCacheWrapper.cpp
@@ -0,0 +1,148 @@
+//
+// Created by chiheb on 25/09/2020.
+//
+#include <string.h> // memset
+#include <sys/mman.h> // for mmap
+#include <cstdlib>
+#include <cstdio>
+#include <cstdint>
+#include <cerrno>
+#include "SylvanCacheWrapper.h"
+
+#ifndef compiler_barrier
+#define compiler_barrier() { asm volatile("" ::: "memory"); }
+#endif
+
+#ifndef cas
+#define cas(ptr, old, new) (__sync_bool_compare_and_swap((ptr),(old),(new)))
+#endif
+
+void SylvanCacheWrapper::cache_create(size_t _cache_size, size_t _max_size)
+{
+#if CACHE_MASK
+ // Cache size must be a power of 2
+ if (__builtin_popcountll(_cache_size) != 1 || __builtin_popcountll(_max_size) != 1) {
+ fprintf(stderr, "cache_create: Table size must be a power of 2!\n");
+ exit(1);
+ }
+#endif
+
+ m_cache_size = _cache_size;
+ m_cache_max = _max_size;
+#if CACHE_MASK
+ cache_mask = cache_size - 1;
+#endif
+
+ if (m_cache_size > m_cache_max) {
+ fprintf(stderr, "cache_create: Table size must be <= max size!\n");
+ exit(1);
+ }
+
+ m_cache_table = (cache_entry_t)mmap(0, m_cache_max * sizeof(struct cache_entry), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);
+ m_cache_status = (uint32_t*)mmap(0, m_cache_max * sizeof(uint32_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);
+
+ if (m_cache_table == (cache_entry_t)-1 || m_cache_status == (uint32_t*)-1) {
+ fprintf(stderr, "cache_create: Unable to allocate memory: %s!\n", strerror(errno));
+ exit(1);
+ }
+
+ m_next_opid = 512LL << 40;
+}
+
+/**
+ * dd must be MTBDD, d2/d3 can be anything
+ */
+int __attribute__((unused))
+SylvanCacheWrapper::cache_get3(uint64_t opid, uint64_t dd, uint64_t d2, uint64_t d3, uint64_t *res)
+{
+ return cache_get(dd | opid, d2, d3, res);
+}
+
+int SylvanCacheWrapper::cache_get(uint64_t a, uint64_t b, uint64_t c, uint64_t *res)
+{
+ const uint64_t hash = cache_hash(a, b, c);
+#if CACHE_MASK
+ volatile uint32_t *s_bucket = m_cache_status + (hash & m_cache_mask);
+ cache_entry_t bucket = m_cache_table + (hash & m_cache_mask);
+#else
+ volatile uint32_t *s_bucket = m_cache_status + (hash % m_cache_size);
+ cache_entry_t bucket = m_cache_table + (hash % m_cache_size);
+#endif
+ const uint32_t s = *s_bucket;
+ compiler_barrier();
+ // abort if locked or if part of a 2-part cache entry
+ if (s & 0xc0000000) return 0;
+ // abort if different hash
+ if ((s ^ (hash>>32)) & 0x3fff0000) return 0;
+ // abort if key different
+ if (bucket->a != a || bucket->b != b || bucket->c != c) return 0;
+ *res = bucket->res;
+ compiler_barrier();
+ // abort if status field changed after compiler_barrier()
+ return *s_bucket == s ? 1 : 0;
+}
+
+/* Rotating 64-bit FNV-1a hash */
+uint64_t SylvanCacheWrapper::cache_hash(uint64_t a, uint64_t b, uint64_t c)
+{
+ const uint64_t prime = 1099511628211;
+ uint64_t hash = 14695981039346656037LLU;
+ hash = (hash ^ (a>>32));
+ hash = (hash ^ a) * prime;
+ hash = (hash ^ b) * prime;
+ hash = (hash ^ c) * prime;
+ return hash;
+}
+
+/**
+ * dd must be MTBDD, d2/d3 can be anything
+ */
+int __attribute__((unused))
+SylvanCacheWrapper::cache_put3(uint64_t opid, uint64_t dd, uint64_t d2, uint64_t d3, uint64_t res)
+{
+ return cache_put(dd | opid, d2, d3, res);
+}
+
+int SylvanCacheWrapper::cache_put(uint64_t a, uint64_t b, uint64_t c, uint64_t res)
+{
+ const uint64_t hash = cache_hash(a, b, c);
+#if CACHE_MASK
+ volatile uint32_t *s_bucket = cache_status + (hash & cache_mask);
+ cache_entry_t bucket = cache_table + (hash & cache_mask);
+#else
+ volatile uint32_t *s_bucket = m_cache_status + (hash % m_cache_size);
+ cache_entry_t bucket = m_cache_table + (hash % m_cache_size);
+#endif
+ const uint32_t s = *s_bucket;
+ // abort if locked
+ if (s & 0x80000000) return 0;
+ // abort if hash identical -> no: in iscasmc this occasionally causes timeouts?!
+ const uint32_t hash_mask = (hash>>32) & 0x3fff0000;
+ // if ((s & 0x7fff0000) == hash_mask) return 0;
+ // use cas to claim bucket
+ const uint32_t new_s = ((s+1) & 0x0000ffff) | hash_mask;
+ if (!cas(s_bucket, s, new_s | 0x80000000)) return 0;
+ // cas succesful: write data
+ bucket->a = a;
+ bucket->b = b;
+ bucket->c = c;
+ bucket->res = res;
+ compiler_barrier();
+ // after compiler_barrier(), unlock status field
+ *s_bucket = new_s;
+ return 1;
+}
+
+
+
+
+
+
+
+
+
+size_t SylvanCacheWrapper::m_cache_size; // power of 2
+size_t SylvanCacheWrapper::m_cache_max;
+cache_entry_t SylvanCacheWrapper::m_cache_table;
+uint32_t* SylvanCacheWrapper::m_cache_status;
+uint64_t SylvanCacheWrapper::m_next_opid;
\ No newline at end of file
diff --git a/src/SylvanCacheWrapper.h b/src/SylvanCacheWrapper.h
new file mode 100644
index 0000000000000000000000000000000000000000..3502e6dffc3cfea11d28d7d048e7df861c8dc87b
--- /dev/null
+++ b/src/SylvanCacheWrapper.h
@@ -0,0 +1,87 @@
+//
+// Created by chiheb on 25/09/2020.
+//
+
+#ifndef PMC_SOG_SYLVANCACHEWRAPPER_H
+#define PMC_SOG_SYLVANCACHEWRAPPER_H
+
+/**
+ * Literals for cache
+ */
+
+#ifdef __cplusplus
+extern "C" {
+#endif /* __cplusplus */
+
+// MDD operations
+static const uint64_t CACHE_MDD_RELPROD = (20LL<<40);
+static const uint64_t CACHE_MDD_MINUS = (21LL<<40);
+static const uint64_t CACHE_MDD_UNION = (22LL<<40);
+static const uint64_t CACHE_MDD_INTERSECT = (23LL<<40);
+static const uint64_t CACHE_MDD_PROJECT = (24LL<<40);
+static const uint64_t CACHE_MDD_JOIN = (25LL<<40);
+static const uint64_t CACHE_MDD_MATCH = (26LL<<40);
+static const uint64_t CACHE_MDD_RELPREV = (27LL<<40);
+static const uint64_t CACHE_MDD_SATCOUNT = (28LL<<40);
+static const uint64_t CACHE_MDD_DIVIDE = (29LL<<40);
+static const uint64_t CACHE_LDD_MINUS = (30LL<<40);
+static const uint64_t CACHE_LDD_FIRE = (31LL<<40);
+static const uint64_t CACHE_LDD_UNION = (32LL<<40);
+
+
+#ifdef __cplusplus
+}
+#endif /* __cplusplus */
+
+
+
+
+
+
+
+/**
+ * This cache is designed to store a,b,c->res, with a,b,c,res 64-bit integers.
+ *
+ * Each cache bucket takes 32 bytes, 2 per cache line.
+ * Each cache status bucket takes 4 bytes, 16 per cache line.
+ * Therefore, size 2^N = 36*(2^N) bytes.
+ */
+
+struct __attribute__((packed)) cache6_entry {
+ uint64_t a;
+ uint64_t b;
+ uint64_t c;
+ uint64_t res;
+ uint64_t d;
+ uint64_t e;
+ uint64_t f;
+ uint64_t res2;
+};
+typedef struct cache6_entry *cache6_entry_t;
+
+struct __attribute__((packed)) cache_entry {
+ uint64_t a;
+ uint64_t b;
+ uint64_t c;
+ uint64_t res;
+};
+
+typedef struct cache_entry *cache_entry_t;
+class SylvanCacheWrapper {
+public:
+ static void cache_create(size_t _cache_size, size_t _max_size);
+ static int __attribute__((unused)) cache_get3(uint64_t opid, uint64_t dd, uint64_t d2, uint64_t d3, uint64_t *res);
+ static int __attribute__((unused)) cache_put3(uint64_t opid, uint64_t dd, uint64_t d2, uint64_t d3, uint64_t res);
+ static int cache_put(uint64_t a, uint64_t b, uint64_t c, uint64_t res);
+ static int cache_get(uint64_t a, uint64_t b, uint64_t c, uint64_t *res);
+private:
+ static size_t m_cache_size; // power of 2
+ static size_t m_cache_max;
+ static cache_entry_t m_cache_table;
+ static uint32_t* m_cache_status;
+ static uint64_t m_next_opid;
+ static uint64_t cache_hash(uint64_t a, uint64_t b, uint64_t c);
+};
+
+
+#endif //PMC_SOG_SYLVANCACHEWRAPPER_H
diff --git a/src/SylvanWrapper.cpp b/src/SylvanWrapper.cpp
index 2fb461ffc21c4b7db17aa10506143f3bf5c28037..7fdfb8e605d032d3cf5e48ceb13fd65d8c791411 100644
--- a/src/SylvanWrapper.cpp
+++ b/src/SylvanWrapper.cpp
@@ -3,51 +3,992 @@
//
-#include "sylvan.h"
-#include "LDDState.h"
-#include <sylvan_int.h>
-#include "sylvan_seq.h"
-//#include <sylvan_sog.h>
-
+//#include "sylvan.h"
+// #include "LDDState.h"
#include <functional>
+#include <vector>
+#include <cassert>
+#include <cstring> // memset
+#include <sys/mman.h> // for mmap
#include <iostream>
-#include <fstream>
-
+#include <string>
+#include "SylvanCacheWrapper.h"
#include "SylvanWrapper.h"
-#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
-using namespace sylvan;
+
+
+#define DECLARE_THREAD_LOCAL(name, type) __thread type name
+#define INIT_THREAD_LOCAL(name)
+#define SET_THREAD_LOCAL(name, value) name = value
+#define LOCALIZE_THREAD_LOCAL(name, type)
+
+DECLARE_THREAD_LOCAL(my_region, uint64_t);
+DECLARE_THREAD_LOCAL(lddmc_refs_key, lddmc_refs_internal_t);
+//lddmc_refs_internal_t lddmc_refs_key;
using namespace std;
+MDD lddmc_false = 0;
+MDD lddmc_true = 1;
+
-uint64_t SylvanWrapper::m_Size=0;
-uint64_t SylvanWrapper::m_agg=0;
/**************************************
* Computes number of markings in an MDD
* @param cmark : an MDD
*/
-uint64_t SylvanWrapper::getMarksCount ( MDD cmark )
-{
+uint64_t SylvanWrapper::getMarksCount(MDD cmark) {
//typedef pair<string,MDD> Pair_stack;
vector<MDD> local_stack;
- uint64_t compteur=0;
- MDD explore_mdd=cmark;
- local_stack.push_back ( cmark );
+ uint64_t compteur = 0;
+ MDD explore_mdd;
+ local_stack.push_back(cmark);
do {
- explore_mdd=local_stack.back();
+ explore_mdd = local_stack.back();
local_stack.pop_back();
compteur++;
- while ( explore_mdd!= lddmc_false && explore_mdd!=lddmc_true ) {
- mddnode_t n_val = GETNODE ( explore_mdd );
- if ( mddnode_getright ( n_val ) !=lddmc_false ) {
- local_stack.push_back ( mddnode_getright ( n_val ) );
+ while (explore_mdd != lddmc_false && explore_mdd != lddmc_true) {
+ mddnode_t n_val = GETNODE(explore_mdd);
+ if (mddnode_getright(n_val) != lddmc_false) {
+ local_stack.push_back(mddnode_getright(n_val));
}
- unsigned int val = mddnode_getvalue ( n_val );
- explore_mdd=mddnode_getdown ( n_val );
+ //unsigned int val = mddnode_getvalue ( n_val );
+ explore_mdd = mddnode_getdown(n_val);
}
- } while ( local_stack.size() !=0 );
+ } while (!local_stack.empty());
return compteur;
}
+
+
+llmsset2_t SylvanWrapper::llmsset_create(size_t initial_size, size_t max_size) {
+ llmsset2_t dbs = nullptr;
+ if (posix_memalign((void **) &dbs, LINE_SIZE, sizeof(struct llmsset2)) != 0) {
+ fprintf(stderr, "llmsset_create: Unable to allocate memory!\n");
+ exit(1);
+ }
+
+#if LLMSSET_MASK
+ /* Check if initial_size and max_size are powers of 2 */
+ if (__builtin_popcountll(initial_size) != 1) {
+ fprintf(stderr, "llmsset_create: initial_size is not a power of 2!\n");
+ exit(1);
+ }
+
+ if (__builtin_popcountll(max_size) != 1) {
+ fprintf(stderr, "llmsset_create: max_size is not a power of 2!\n");
+ exit(1);
+ }
+#endif
+
+ if (initial_size > max_size) {
+ fprintf(stderr, "llmsset_create: initial_size > max_size!\n");
+ exit(1);
+ }
+
+ // minimum size is now 512 buckets (region size, but of course, n_workers * 512 is suggested as minimum)
+
+ if (initial_size < 512) {
+ fprintf(stderr, "llmsset_create: initial_size too small!\n");
+ exit(1);
+ }
+
+ dbs->max_size = max_size;
+ llmsset_set_size(dbs, initial_size);
+
+ /* This implementation of "resizable hash table" allocates the max_size table in virtual memory,
+ but only uses the "actual size" part in real memory */
+
+ dbs->table = (uint64_t *) mmap(nullptr, dbs->max_size * 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1,
+ 0);
+ dbs->data = (uint8_t *) mmap(nullptr, dbs->max_size * 16, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1,
+ 0);
+
+ /* Also allocate bitmaps. Each region is 64*8 = 512 buckets.
+ Overhead of bitmap1: 1 bit per 4096 bucket.
+ Overhead of bitmap2: 1 bit per bucket.
+ Overhead of bitmapc: 1 bit per bucket. */
+
+ dbs->bitmap1 = (uint64_t *) mmap(0, dbs->max_size / (512 * 8), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS,
+ -1, 0);
+ dbs->bitmap2 = (uint64_t *) mmap(0, dbs->max_size / 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);
+ dbs->bitmapc = (uint64_t *) mmap(0, dbs->max_size / 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);
+
+ if (dbs->table == (uint64_t *) -1 || dbs->data == (uint8_t *) -1 || dbs->bitmap1 == (uint64_t *) -1 ||
+ dbs->bitmap2 == (uint64_t *) -1 || dbs->bitmapc == (uint64_t *) -1) {
+ fprintf(stderr, "llmsset_create: Unable to allocate memory: %s!\n", strerror(errno));
+ exit(1);
+ }
+
+#if defined(madvise) && defined(MADV_RANDOM)
+ madvise(dbs->table, dbs->max_size * 8, MADV_RANDOM);
+#endif
+
+ // forbid first two positions (index 0 and 1)
+ dbs->bitmap2[0] = 0xc000000000000000LL;
+
+ dbs->hash_cb = NULL;
+ dbs->equals_cb = NULL;
+ dbs->create_cb = NULL;
+ dbs->destroy_cb = NULL;
+
+ // yes, ugly. for now, we use a global thread-local value.
+ // that is a problem with multiple tables.
+ // so, for now, do NOT use multiple tables!!
+
+ /*LACE_ME;*/
+ INIT_THREAD_LOCAL(my_region);
+
+ llmsset_reset_region();
+
+ return dbs;
+}
+
+
+void SylvanWrapper::llmsset_reset_region() {
+ LOCALIZE_THREAD_LOCAL(my_region, uint64_t);
+ my_region = (uint64_t) -1; // no region
+ SET_THREAD_LOCAL(my_region, my_region);
+}
+
+/**
+ * Set the table size of the set.
+ * Typically called during garbage collection, after clear and before rehash.
+ * Returns 0 if dbs->table_size > dbs->max_size!
+ */
+void SylvanWrapper::llmsset_set_size(llmsset2_t dbs, size_t size) {
+ /* check bounds (don't be rediculous) */
+ if (size > 128 && size <= dbs->max_size) {
+ dbs->table_size = size;
+#if LLMSSET_MASK
+ /* Warning: if size is not a power of two, you will get interesting behavior */
+ dbs->mask = dbs->table_size - 1;
+#endif
+ /* Set threshold: number of cache lines to probe before giving up on node insertion */
+ dbs->threshold = 192 - 2 * __builtin_clzll(dbs->table_size);
+ }
+}
+
+void
+SylvanWrapper::sylvan_set_limits(size_t memorycap, int table_ratio, int initial_ratio) {
+ if (table_ratio > 10 || table_ratio < -10) {
+ fprintf(stderr, "sylvan_set_limits: table_ratio unreasonable (between -10 and 10)\n");
+ exit(1);
+ }
+
+ size_t max_t = 1;
+ size_t max_c = 1;
+ if (table_ratio > 0) {
+ max_t <<= table_ratio;
+ } else {
+ max_c <<= -table_ratio;
+ }
+
+ size_t cur = max_t * 24 + max_c * 36;
+ if (cur > memorycap) {
+ fprintf(stderr, "sylvan_set_limits: memory cap incompatible with requested table ratio\n");
+ }
+
+ while (2 * cur < memorycap && max_t < 0x0000040000000000) {
+ max_t *= 2;
+ max_c *= 2;
+ cur *= 2;
+ }
+
+ if (initial_ratio < 0) {
+ fprintf(stderr, "sylvan_set_limits: initial_ratio unreasonable (may not be negative)\n");
+ exit(1);
+ }
+
+ size_t min_t = max_t, min_c = max_c;
+ while (initial_ratio > 0 && min_t > 0x1000 && min_c > 0x1000) {
+ min_t >>= 1;
+ min_c >>= 1;
+ initial_ratio--;
+ }
+
+ m_table_min = min_t;
+ m_table_max = max_t;
+ m_cache_min = min_c;
+ m_cache_max = max_c;
+}
+
+/**
+ * Initializes Sylvan.
+ */
+void SylvanWrapper::sylvan_init_package(void) {
+ if (m_table_max == 0) {
+ fprintf(stderr, "sylvan_init_package error: table sizes not set (sylvan_set_sizes or sylvan_set_limits)!");
+ exit(1);
+ }
+
+ /* Create tables */
+ m_nodes = llmsset_create(m_table_min, m_table_max);
+ SylvanCacheWrapper::cache_create(m_cache_min, m_cache_max);
+
+ /* Initialize garbage collection */
+ m_gc = 0;
+
+ /***************** Not yet **************************************/
+//#if SYLVAN_AGGRESSIVE_RESIZE
+// main_hook = TASK(sylvan_gc_aggressive_resize);
+//#else
+// main_hook = TASK(sylvan_gc_normal_resize);
+//#endif
+
+
+ //sylvan_stats_init();
+}
+
+void SylvanWrapper::sylvan_init_ldd() {
+ /*sylvan_register_quit(lddmc_quit);
+ sylvan_gc_add_mark(TASK(lddmc_gc_mark_external_refs));
+ sylvan_gc_add_mark(TASK(lddmc_gc_mark_protected));
+ sylvan_gc_add_mark(TASK(lddmc_gc_mark_serialize));*/
+ //m_lddmc_protected_created=0; // Should be initialized in the constructor
+ refs_create(&m_lddmc_refs, 1024);
+ if (!m_lddmc_protected_created) {
+ protect_create(&m_lddmc_protected, 4096);
+ m_lddmc_protected_created = 1;
+ }
+
+ //LACE_ME;
+ lddmc_refs_init();
+}
+
+void SylvanWrapper::lddmc_refs_init_task() {
+ lddmc_refs_internal_t s = (lddmc_refs_internal_t) malloc(sizeof(struct lddmc_refs_internal));
+ s->pcur = s->pbegin = (const MDD **) malloc(sizeof(MDD *) * 1024);
+ s->pend = s->pbegin + 1024;
+ s->rcur = s->rbegin = (MDD *) malloc(sizeof(MDD) * 1024);
+ s->rend = s->rbegin + 1024;
+ /* s->scur = s->sbegin = (lddmc_refs_task_t)malloc(sizeof(struct lddmc_refs_task) * 1024);
+ s->send = s->sbegin + 1024;*/
+ SET_THREAD_LOCAL(lddmc_refs_key, s);
+}
+
+void SylvanWrapper::lddmc_refs_init() {
+ INIT_THREAD_LOCAL(lddmc_refs_key);
+ lddmc_refs_init_task();
+ // sylvan_gc_add_mark(TASK(lddmc_refs_mark));
+}
+
+
+void SylvanWrapper::refs_create(refs_table2_t *tbl, size_t _refs_size) {
+ if (__builtin_popcountll(_refs_size) != 1) {
+ fprintf(stderr, "refs: Table size must be a power of 2!\n");
+ exit(1);
+ }
+
+ tbl->refs_size = _refs_size;
+ tbl->refs_table = (uint64_t *) mmap(0, tbl->refs_size * sizeof(uint64_t), PROT_READ | PROT_WRITE,
+ MAP_PRIVATE | MAP_ANON, -1, 0);
+ if (tbl->refs_table == (uint64_t *) -1) {
+ fprintf(stderr, "refs: Unable to allocate memory: %s!\n", strerror(errno));
+ exit(1);
+ }
+}
+
+void SylvanWrapper::protect_create(refs_table2_t *tbl, size_t _refs_size) {
+ if (__builtin_popcountll(_refs_size) != 1) {
+ fprintf(stderr, "refs: Table size must be a power of 2!\n");
+ exit(1);
+ }
+
+ tbl->refs_size = _refs_size;
+ tbl->refs_table = (uint64_t *) mmap(0, tbl->refs_size * sizeof(uint64_t), PROT_READ | PROT_WRITE,
+ MAP_PRIVATE | MAP_ANON, -1, 0);
+ if (tbl->refs_table == (uint64_t *) -1) {
+ fprintf(stderr, "refs: Unable to allocate memory: %s!\n", strerror(errno));
+ exit(1);
+ }
+}
+
+size_t SylvanWrapper::llmsset_get_size(const llmsset2_t dbs) {
+ return dbs->table_size;
+}
+
+/*
+ * Initialize GC
+ */
+void SylvanWrapper::init_gc_seq() {
+ m_sequentiel_refs = lddmc_refs_key;
+}
+
+/*
+ * Return sizes
+ */
+size_t SylvanWrapper::seq_llmsset_count_marked(llmsset2_t dbs) {
+ return llmsset_count_marked_seq(dbs, 0, dbs->table_size);
+}
+
+//********************************************
+size_t SylvanWrapper::llmsset_count_marked_seq(llmsset2_t dbs, size_t first, size_t count) {
+ if (count > 512) {
+ size_t split = count / 2;
+
+ size_t right = llmsset_count_marked_seq(dbs, first + split, count - split);
+ size_t left = llmsset_count_marked_seq(dbs, first, split);
+ return left + right;
+ } else {
+ size_t result = 0;
+ uint64_t *ptr = dbs->bitmap2 + (first / 64);
+ if (count == 512) {
+ result += __builtin_popcountll(ptr[0]);
+ result += __builtin_popcountll(ptr[1]);
+ result += __builtin_popcountll(ptr[2]);
+ result += __builtin_popcountll(ptr[3]);
+ result += __builtin_popcountll(ptr[4]);
+ result += __builtin_popcountll(ptr[5]);
+ result += __builtin_popcountll(ptr[6]);
+ result += __builtin_popcountll(ptr[7]);
+ } else {
+ uint64_t mask = 0x8000000000000000LL >> (first & 63);
+ for (size_t k = 0; k < count; k++) {
+ if (*ptr & mask) result += 1;
+ mask >>= 1;
+ if (mask == 0) {
+ ptr++;
+ mask = 0x8000000000000000LL;
+ }
+ }
+ }
+ return result;
+ }
+}
+
+void SylvanWrapper::displayMDDTableInfo() {
+ printf("%zu of %zu buckets filled!\n", seq_llmsset_count_marked(m_nodes), llmsset_get_size(m_nodes));
+}
+
+MDD SylvanWrapper::lddmc_cube(uint32_t *values, size_t count) {
+ if (count == 0) return lddmc_true;
+ return lddmc_makenode(*values, lddmc_cube(values + 1, count - 1), lddmc_false);
+}
+
+MDD SylvanWrapper::lddmc_makenode(uint32_t value, MDD ifeq, MDD ifneq) {
+ if (ifeq == lddmc_false) return ifneq;
+
+
+ assert(ifneq != lddmc_true);
+ if (ifneq != lddmc_false) assert(value < mddnode_getvalue(LDD_GETNODE(ifneq)));
+
+ struct mddnode n;
+ mddnode_make(&n, value, ifneq, ifeq);
+
+ int created;
+ uint64_t index = llmsset_lookup(m_nodes, n.a, n.b, &created);
+ if (index == 0) {
+ /* lddmc_refs_push(ifeq);
+ lddmc_refs_push(ifneq);*/
+
+ // sylvan_gc();/*********************************************************************************************/
+ /*lddmc_refs_pop(1);*/
+
+ index = llmsset_lookup(m_nodes, n.a, n.b, &created);
+ if (index == 0) {
+ fprintf(stderr, "MDD Unique table full, %zu of %zu buckets filled!\n", seq_llmsset_count_marked(m_nodes),
+ llmsset_get_size(m_nodes));
+ exit(1);
+ }
+ }
+
+ /*if (created) {
+ sylvan_stats_count(LDD_NODES_CREATED);
+
+ }
+ else sylvan_stats_count(LDD_NODES_REUSED);*/
+
+ return (MDD) index;
+}
+
+mddnode_t SylvanWrapper::LDD_GETNODE(MDD mdd) {
+ return ((mddnode_t) llmsset_index_to_ptr(m_nodes, mdd));
+}
+
+inline uint64_t
+SylvanWrapper::llmsset_lookup2(const llmsset2_t dbs, uint64_t a, uint64_t b, int *created, const int custom) {
+ uint64_t hash_rehash = 14695981039346656037LLU;
+ if (custom) hash_rehash = dbs->hash_cb(a, b, hash_rehash);
+ else hash_rehash = llmsset_hash(a, b, hash_rehash);
+
+ const uint64_t step = (((hash_rehash >> 20) | 1) << 3);
+ const uint64_t hash = hash_rehash & MASK_HASH;
+ uint64_t idx, last, cidx = 0;
+ int i = 0;
+
+#if LLMSSET_MASK
+ last = idx = hash_rehash & dbs->mask;
+#else
+ last = idx = hash_rehash % dbs->table_size;
+#endif
+
+ for (;;) {
+ volatile uint64_t *bucket = dbs->table + idx;
+ uint64_t v = *bucket;
+
+ if (v == 0) {
+ if (cidx == 0) {
+ // Claim data bucket and write data
+ cidx = claim_data_bucket(dbs);
+ if (cidx == (uint64_t) -1) return 0; // failed to claim a data bucket
+ if (custom) dbs->create_cb(&a, &b);
+ uint64_t *d_ptr = ((uint64_t *) dbs->data) + 2 * cidx;
+ d_ptr[0] = a;
+ d_ptr[1] = b;
+ }
+ if (cas(bucket, 0, hash | cidx)) {
+ if (custom) set_custom_bucket(dbs, cidx, custom);
+ *created = 1;
+ m_g_created++;
+ return cidx;
+ } else {
+ v = *bucket;
+ }
+ }
+
+ if (hash == (v & MASK_HASH)) {
+ uint64_t d_idx = v & MASK_INDEX;
+ uint64_t *d_ptr = ((uint64_t *) dbs->data) + 2 * d_idx;
+ if (custom) {
+ if (dbs->equals_cb(a, b, d_ptr[0], d_ptr[1])) {
+ if (cidx != 0) {
+ dbs->destroy_cb(a, b);
+ release_data_bucket(dbs, cidx);
+ }
+ *created = 0;
+ return d_idx;
+ }
+ } else {
+ if (d_ptr[0] == a && d_ptr[1] == b) {
+ if (cidx != 0) release_data_bucket(dbs, cidx);
+ *created = 0;
+ return d_idx;
+ }
+ }
+ }
+
+ //sylvan_stats_count(LLMSSET_LOOKUP);
+
+ // find next idx on probe sequence
+ idx = (idx & CL_MASK) | ((idx + 1) & CL_MASK_R);
+ if (idx == last) {
+ if (++i == dbs->threshold) return 0; // failed to find empty spot in probe sequence
+
+ // go to next cache line in probe sequence
+ hash_rehash += step;
+
+#if LLMSSET_MASK
+ last = idx = hash_rehash & dbs->mask;
+#else
+ last = idx = hash_rehash % dbs->table_size;
+#endif
+ }
+ }
+}
+
+uint64_t SylvanWrapper::llmsset_lookup(const llmsset2_t dbs, const uint64_t a, const uint64_t b, int *created) {
+ return llmsset_lookup2(dbs, a, b, created, 0);
+}
+
+uint64_t SylvanWrapper::llmsset_hash(const uint64_t a, const uint64_t b, const uint64_t seed) {
+ // The FNV-1a hash for 64 bits
+ const uint64_t prime = 1099511628211;
+ uint64_t hash = seed;
+ hash = (hash ^ a) * prime;
+ hash = (hash ^ b) * prime;
+ return hash ^ (hash >> 32);
+}
+
+
+uint64_t SylvanWrapper::claim_data_bucket(const llmsset2_t dbs) {
+ LOCALIZE_THREAD_LOCAL(my_region, uint64_t);
+ //printf("%d \n",my_region);
+ //printf("Value of my region %d \n",my_region);
+ for (;;) {
+ if (my_region != (uint64_t) -1) {
+ // find empty bucket in region <my_region>
+ //printf("My region : %d\n",my_region);
+ uint64_t *ptr = dbs->bitmap2 + (my_region * 8);
+ int i = 0;
+ for (; i < 8;) {
+ uint64_t v = *ptr;
+ if (v != 0xffffffffffffffffLL) {
+ int j = __builtin_clzll(~v);
+ *ptr |= (0x8000000000000000LL >> j);
+ return (8 * my_region + i) * 64 + j;
+ }
+ i++;
+ ptr++;
+ }
+ } else {
+ //printf("yep!");
+ // special case on startup or after garbage collection"
+ // my_region += (lace_get_worker()->worker*(dbs->table_size/(64*8)))/lace_workers();
+ }
+ uint64_t count = dbs->table_size / (64 * 8);
+ for (;;) {
+ // check if table maybe full
+ if (count-- == 0) return (uint64_t) -1;
+
+ my_region += 1;
+ if (my_region >= (dbs->table_size / (64 * 8))) my_region = 0;
+
+ // try to claim it
+ uint64_t *ptr = dbs->bitmap1 + (my_region / 64);
+ uint64_t mask = 0x8000000000000000LL >> (my_region & 63);
+ uint64_t v;
+ restart:
+ v = *ptr;
+ if (v & mask) continue; // taken
+ if (cas(ptr, v, v | mask)) break;
+ else goto restart;
+ }
+ SET_THREAD_LOCAL(my_region, my_region);
+ }
+}
+
+void SylvanWrapper::release_data_bucket(const llmsset2_t dbs, uint64_t index) {
+ uint64_t *ptr = dbs->bitmap2 + (index / 64);
+ uint64_t mask = 0x8000000000000000LL >> (index & 63);
+ *ptr &= ~mask;
+}
+
+
+void SylvanWrapper::set_custom_bucket(const llmsset2_t dbs, uint64_t index, int on) {
+ uint64_t *ptr = dbs->bitmapc + (index / 64);
+ uint64_t mask = 0x8000000000000000LL >> (index & 63);
+ if (on) *ptr |= mask;
+ else *ptr &= ~mask;
+}
+
+MDD __attribute__((unused)) SylvanWrapper::lddmc_refs_push(MDD lddmc) {
+ LOCALIZE_THREAD_LOCAL(lddmc_refs_key, lddmc_refs_internal_t);
+ *(lddmc_refs_key->rcur++) = lddmc;
+ if (lddmc_refs_key->rcur == lddmc_refs_key->rend) return lddmc_refs_refs_up(lddmc_refs_key, lddmc);
+ else return lddmc;
+}
+
+void __attribute__((unused)) SylvanWrapper::lddmc_refs_pop(long amount) {
+ LOCALIZE_THREAD_LOCAL(lddmc_refs_key, lddmc_refs_internal_t);
+ lddmc_refs_key->rcur -= amount;
+}
+
+
+MDD __attribute__((noinline)) SylvanWrapper::lddmc_refs_refs_up(lddmc_refs_internal_t lddmc_refs_key, MDD res) {
+
+ long size = lddmc_refs_key->rend - lddmc_refs_key->rbegin;
+ lddmc_refs_key->rbegin = (MDD *) realloc(lddmc_refs_key->rbegin, sizeof(MDD) * size * 2);
+ lddmc_refs_key->rcur = lddmc_refs_key->rbegin + size;
+ lddmc_refs_key->rend = lddmc_refs_key->rbegin + (size * 2);
+ return res;
+}
+
+size_t SylvanWrapper::lddmc_nodecount(MDD mdd) {
+ size_t result = lddmc_nodecount_mark(mdd);
+ lddmc_nodecount_unmark(mdd);
+ return result;
+}
+
+void SylvanWrapper::lddmc_nodecount_unmark(MDD mdd) {
+ if (mdd <= lddmc_true) return;
+ mddnode_t n = LDD_GETNODE(mdd);
+ if (mddnode_getmark(n)) {
+ mddnode_setmark(n, 0);
+ lddmc_nodecount_unmark(mddnode_getright(n));
+ lddmc_nodecount_unmark(mddnode_getdown(n));
+ }
+}
+
+/**
+ * Count number of nodes in MDD
+ */
+
+size_t SylvanWrapper::lddmc_nodecount_mark(MDD mdd) {
+ if (mdd <= lddmc_true) return 0;
+ mddnode_t n = LDD_GETNODE(mdd);
+ if (mddnode_getmark(n)) return 0;
+ mddnode_setmark(n, 1);
+ return 1 + lddmc_nodecount_mark(mddnode_getdown(n)) + lddmc_nodecount_mark(mddnode_getright(n));
+}
+
+MDD SylvanWrapper::lddmc_union_mono(MDD a, MDD b) {
+ /* Terminal cases */
+ if (a == b) return a;
+ if (a == lddmc_false) return b;
+ if (b == lddmc_false) return a;
+ assert(a != lddmc_true && b != lddmc_true); // expecting same length
+
+ /* Test gc */
+ // LACE_ME;
+ // sylvan_gc_test();
+
+ //sylvan_stats_count(LDD_UNION);
+
+ /* Improve cache behavior */
+ if (a < b) {
+ MDD tmp = b;
+ b = a;
+ a = tmp;
+ }
+
+ /* Access cache */
+ MDD result;
+ if (SylvanCacheWrapper::cache_get3(CACHE_LDD_UNION, a, b, 0,&result)) {
+ // std::cout<<"Cache succeeded!"<<std::endl;
+ return result;
+ }
+
+
+ /* Get nodes */
+ mddnode_t na = GETNODE(a);
+ mddnode_t nb = GETNODE(b);
+
+ const int na_copy = mddnode_getcopy(na) ? 1 : 0;
+ const int nb_copy = mddnode_getcopy(nb) ? 1 : 0;
+ const uint32_t na_value = mddnode_getvalue(na);
+ const uint32_t nb_value = mddnode_getvalue(nb);
+
+ /* Perform recursive calculation */
+ if (na_copy && nb_copy) {
+
+ MDD right = lddmc_union_mono(mddnode_getright(na), mddnode_getright(nb));
+ MDD down = lddmc_union_mono(mddnode_getdown(na), mddnode_getdown(nb));
+ result = lddmc_make_copynode(down, right);
+ } else if (na_copy) {
+ MDD right = lddmc_union_mono(mddnode_getright(na), b);
+ result = lddmc_make_copynode(mddnode_getdown(na), right);
+ } else if (nb_copy) {
+ MDD right = lddmc_union_mono(a, mddnode_getright(nb));
+ result = lddmc_make_copynode(mddnode_getdown(nb), right);
+ } else if (na_value < nb_value) {
+ MDD right = lddmc_union_mono(mddnode_getright(na), b);
+ result = lddmc_makenode(na_value, mddnode_getdown(na), right);
+ } else if (na_value == nb_value) {
+
+ MDD right = lddmc_union_mono(mddnode_getright(na), mddnode_getright(nb));
+
+ MDD down = lddmc_union_mono(mddnode_getdown(na), mddnode_getdown(nb));
+ result = lddmc_makenode(na_value, down, right);
+ } else /* na_value > nb_value */
+ {
+ MDD right = lddmc_union_mono(a, mddnode_getright(nb));
+ result = lddmc_makenode(nb_value, mddnode_getdown(nb), right);
+ }
+
+
+ SylvanCacheWrapper::cache_put3(CACHE_LDD_UNION, a, b, 0, result);
+
+ return result;
+}
+
+MDD SylvanWrapper::lddmc_make_copynode(MDD ifeq, MDD ifneq) {
+ struct mddnode n;
+ mddnode_makecopy(&n, ifneq, ifeq);
+
+ int created;
+ uint64_t index = llmsset_lookup(m_nodes, n.a, n.b, &created);
+ if (index == 0) {
+ //lddmc_refs_push(ifeq);
+ //lddmc_refs_push(ifneq);
+ /*LACE_ME;
+ sylvan_gc();*/
+ //lddmc_refs_pop(1);
+
+ index = llmsset_lookup(m_nodes, n.a, n.b, &created);
+ if (index == 0) {
+ fprintf(stderr, "MDD Unique table full, %zu of %zu buckets filled!\n", seq_llmsset_count_marked(m_nodes),
+ llmsset_get_size(m_nodes));
+ exit(1);
+ }
+ }
+
+ /*if (created) sylvan_stats_count(LDD_NODES_CREATED);
+ else sylvan_stats_count(LDD_NODES_REUSED);*/
+
+ return (MDD) index;
+}
+
+
+bool SylvanWrapper::isSingleMDD(MDD mdd) {
+ mddnode_t node;
+
+ while (mdd > lddmc_true) {
+ node = GETNODE(mdd);
+ if (mddnode_getright(node) != lddmc_false) return false;
+ mdd = mddnode_getdown(node);
+ }
+ return true;
+}
+
+// Renvoie le nbre de noeuds à un niveau donné
+int SylvanWrapper::get_mddnbr(MDD mdd, int level) {
+ mddnode_t node;
+ for (int j = 0; j < level; j++) {
+ node = GETNODE(mdd);
+ mdd = mddnode_getdown(node);
+ }
+ int i = 0;
+
+ while (mdd != lddmc_false) {
+ mddnode_t r = GETNODE(mdd);
+ mdd = mddnode_getright(r);
+ i++;
+ }
+ return i;
+}
+
+MDD SylvanWrapper::ldd_divide_internal(MDD a, int current_level, int level) {
+ /* Terminal cases */
+
+ if (a == lddmc_false) return lddmc_false;
+ if (a == lddmc_true) return lddmc_true;
+
+ MDD result;
+ if (SylvanCacheWrapper::cache_get3(CACHE_MDD_DIVIDE, a, current_level, level, &result))
+ {
+ return result;
+ }
+
+ mddnode_t node_a = GETNODE(a);
+ const uint32_t na_value = mddnode_getvalue(node_a);
+
+
+ /* Perform recursive calculation */
+ if (current_level <= level) {
+
+ MDD down = ldd_divide_internal(mddnode_getdown(node_a), current_level + 1, level);
+ MDD right = lddmc_false;
+ result = lddmc_makenode(na_value, down, right);
+ } else {
+ MDD right = ldd_divide_internal(mddnode_getright(node_a), current_level, level);
+ MDD down = ldd_divide_internal(mddnode_getdown(node_a), current_level + 1, level);
+ result = lddmc_makenode(na_value, down, right);
+ }
+
+ SylvanCacheWrapper::cache_put3(CACHE_MDD_DIVIDE, a, current_level, level, result);
+ return result;
+}
+
+
+MDD SylvanWrapper::ldd_divide_rec(MDD a, int level) {
+ return ldd_divide_internal(a, 0, level);
+}
+
+MDD SylvanWrapper::ldd_minus(MDD a, MDD b) {
+ /* Terminal cases */
+ if (a == b) return lddmc_false;
+ if (a == lddmc_false) return lddmc_false;
+ if (b == lddmc_false) return a;
+ assert(b != lddmc_true);
+ assert(a != lddmc_true); // Universe is unknown!! // Possibly depth issue?
+
+ /* Test gc */
+ //sylvan_gc_test();
+
+ // sylvan_stats_count(LDD_MINUS);
+
+ MDD result;
+ if (SylvanCacheWrapper::cache_get(CACHE_LDD_MINUS, a, b, &result)) {
+ return result;
+ }
+ /* Get nodes */
+ mddnode_t na = GETNODE(a);
+ mddnode_t nb = GETNODE(b);
+ uint32_t na_value = mddnode_getvalue(na);
+ uint32_t nb_value = mddnode_getvalue(nb);
+
+ /* Perform recursive calculation */
+ if (na_value < nb_value) {
+ MDD right = ldd_minus(mddnode_getright(na), b);
+ result = lddmc_makenode(na_value, mddnode_getdown(na), right);
+ } else if (na_value == nb_value) {
+// lddmc_refs_spawn(SPAWN(lddmc_minus, mddnode_getright(na), mddnode_getright(nb)));
+ MDD down = ldd_minus(mddnode_getdown(na), mddnode_getdown(nb));
+ // lddmc_refs_push(down);
+ MDD right = ldd_minus(mddnode_getright(na), mddnode_getright(nb));
+ //lddmc_refs_pop(1);
+ result = lddmc_makenode(na_value, down, right);
+ } else /* na_value > nb_value */
+ {
+ result = ldd_minus(a, mddnode_getright(nb));
+ }
+ SylvanCacheWrapper::cache_put(CACHE_LDD_MINUS, a, b, result);
+ return result;
+}
+
+
+MDD SylvanWrapper::lddmc_firing_mono(MDD cmark, MDD minus, MDD plus) {
+ // for an empty set of source states, or an empty transition relation, return the empty set
+ if (cmark == lddmc_true) return lddmc_true;
+ if (minus == lddmc_false || plus == lddmc_false) return lddmc_false;
+
+ MDD result;
+ MDD _cmark = cmark, _minus = minus, _plus = plus;
+
+ if (SylvanCacheWrapper::cache_get3(CACHE_LDD_FIRE, cmark, minus, plus, &result)) {
+ return result;
+ }
+ MDD cache_cmark=cmark;
+ mddnode_t n_cmark = GETNODE(_cmark);
+ mddnode_t n_plus = GETNODE(_plus);
+ mddnode_t n_minus = GETNODE(_minus);
+
+
+ result = lddmc_false;
+
+ for (;;) {
+ uint32_t value;
+ value = mddnode_getvalue(n_cmark);
+ uint32_t value_minus = mddnode_getvalue(n_minus);
+ uint32_t value_plus = mddnode_getvalue(n_plus);
+ if (value >= value_minus) {
+ MDD result2 =
+ lddmc_makenode(value - value_minus + value_plus,
+ lddmc_firing_mono(mddnode_getdown(n_cmark), mddnode_getdown(n_minus),
+ mddnode_getdown(n_plus)), lddmc_false);
+
+
+ if (result2 != lddmc_false) result = lddmc_union_mono(result, result2);
+ }
+ cmark = mddnode_getright(n_cmark);
+ if (cmark == lddmc_false) break;
+ n_cmark = GETNODE(cmark);
+ }
+ SylvanCacheWrapper::cache_put3(CACHE_LDD_FIRE, cache_cmark, minus, plus, result);
+ return result;
+}
+
+// so: proj: -2 (end; quantify rest), -1 (end; keep rest), 0 (quantify), 1 (keep)
+MDD SylvanWrapper::lddmc_project( const MDD mdd, const MDD proj)
+{
+ if (mdd == lddmc_false) return lddmc_false; // projection of empty is empty
+ if (mdd == lddmc_true) return lddmc_true; // projection of universe is universe...
+ mddnode_t p_node = GETNODE(proj);
+ uint32_t p_val = mddnode_getvalue(p_node);
+ if (p_val == (uint32_t)-1) return mdd;
+ if (p_val == (uint32_t)-2) return lddmc_true; // because we always end with true.
+
+ MDD result;
+ if (SylvanCacheWrapper::cache_get3(CACHE_MDD_PROJECT, mdd, proj, 0, &result))
+ {
+ return result;
+ }
+
+ mddnode_t n = LDD_GETNODE(mdd);
+
+ if (p_val == 1) // keep
+ {
+ MDD down = lddmc_project( mddnode_getdown(n), mddnode_getdown(p_node));
+ //lddmc_refs_push(down);
+ // MDD right = lddmc_refs_sync(SYNC(lddmc_project));
+ //lddmc_refs_pop(1);
+ result = lddmc_makenode(mddnode_getvalue(n), down, right);
+ } else // quantify
+ {
+ if (mddnode_getdown(n) == lddmc_true) // assume lowest level
+ {
+ result = lddmc_true;
+ }
+ else
+ {
+ int count = 0;
+ result = lddmc_false;
+ MDD p_down = mddnode_getdown(p_node), _mdd=mdd;
+ while (1)
+ {
+ //lddmc_refs_spawn(SPAWN(lddmc_project, mddnode_getdown(n), p_down));
+ MDD down= lddmc_project (mddnode_getdown(n), p_down);
+ result = lddmc_union_mono(result, down);
+ count++;
+ _mdd = mddnode_getright(n);
+ assert(_mdd != lddmc_true);
+ if (_mdd == lddmc_false) break;
+ n = LDD_GETNODE(_mdd);
+ }
+
+
+ }
+ }
+
+ SylvanCacheWrapper::cache_put3(CACHE_MDD_PROJECT, mdd, proj, 0, result);
+ return result;
+}
+
+int SylvanWrapper::isGCRequired()
+{
+ return (m_g_created>llmsset_get_size(m_nodes)/2);
+}
+
+void SylvanWrapper::convert_wholemdd_stringcpp(MDD cmark,string &res)
+{
+ typedef pair<string,MDD> Pair_stack;
+ vector<Pair_stack> local_stack;
+
+ unsigned int compteur=0;
+ MDD explore_mdd=cmark;
+
+ string chaine;
+
+ res=" ";
+ local_stack.push_back(Pair_stack(chaine,cmark));
+ do
+ {
+ Pair_stack element=local_stack.back();
+ chaine=element.first;
+ explore_mdd=element.second;
+ local_stack.pop_back();
+ compteur++;
+ while ( explore_mdd!= lddmc_false && explore_mdd!=lddmc_true)
+ {
+ mddnode_t n_val = GETNODE(explore_mdd);
+ if (mddnode_getright(n_val)!=lddmc_false)
+ {
+ local_stack.push_back(Pair_stack(chaine,mddnode_getright(n_val)));
+ }
+ unsigned int val = mddnode_getvalue(n_val);
+
+ chaine.push_back((unsigned char)(val)+1);
+ explore_mdd=mddnode_getdown(n_val);
+ }
+ /*printchaine(&chaine);printf("\n");*/
+ res+=chaine;
+ }
+ while (local_stack.size()!=0);
+ //delete chaine;
+
+ compteur=(compteur<<1) | 1;
+ res[1]=(unsigned char)((compteur>>8)+1);
+ res[0]=(unsigned char)(compteur & 255);
+
+}
+
+
+
+
+
+
+size_t SylvanWrapper::m_table_min = 0;
+size_t SylvanWrapper::m_table_max = 0;
+size_t SylvanWrapper::m_cache_min = 0;
+size_t SylvanWrapper::m_cache_max = 0;
+/**
+ * This variable is used for a cas flag so only one gc runs at one time
+ */
+volatile int SylvanWrapper::m_gc;
+llmsset2_t SylvanWrapper::m_nodes;
+/**
+ * External refrences
+ */
+refs_table2_t SylvanWrapper::m_lddmc_refs;
+refs_table2_t SylvanWrapper::m_lddmc_protected;
+int SylvanWrapper::m_lddmc_protected_created = 0;
+
+/*
+ * Internal references
+ */
+lddmc_refs_internal_t SylvanWrapper::m_sequentiel_refs;
+//lddmc_refs_internal_t SylvanWrapper::m_lddmc_refs_key;
+
+/** Sylvan table**/
+uint32_t SylvanWrapper::m_g_created;
\ No newline at end of file
diff --git a/src/SylvanWrapper.h b/src/SylvanWrapper.h
index 8988d9b302dad91adec34fb34d4be91f06a69731..325cd8260a7eead3f8cb8f76b939a3b16c223edc 100644
--- a/src/SylvanWrapper.h
+++ b/src/SylvanWrapper.h
@@ -4,13 +4,256 @@
#ifndef PMC_SOG_SYLVANWRAPPER_H
#define PMC_SOG_SYLVANWRAPPER_H
+#include <cstdint>
+#include <cstddef>
+/**
+ * Lockless hash table (set) to store 16-byte keys.
+ * Each unique key is associated with a 42-bit number.
+ *
+ * The set has support for stop-the-world garbage collection.
+ * Methods llmsset_clear, llmsset_mark and llmsset_rehash implement garbage collection.
+ * During their execution, llmsset_lookup is not allowed.
+ *
+ * WARNING: Originally, this table is designed to allow multiple tables.
+ * However, this is not compatible with thread local storage for now.
+ * Do not use multiple tables.
+ */
+
+/**
+ * hash(a, b, seed)
+ * equals(lhs_a, lhs_b, rhs_a, rhs_b)
+ * create(a, b) -- with a,b pointers, allows changing pointers on create of node,
+ * but must keep hash/equals same!
+ * destroy(a, b)
+ */
+
+
+typedef uint64_t (*llmsset_hash_cb)(uint64_t, uint64_t, uint64_t);
+
+typedef int (*llmsset_equals_cb)(uint64_t, uint64_t, uint64_t, uint64_t);
+
+typedef void (*llmsset_create_cb)(uint64_t *, uint64_t *);
+
+typedef void (*llmsset_destroy_cb)(uint64_t, uint64_t);
+
+
+typedef uint64_t MDD; // Note: low 40 bits only
+extern MDD lddmc_false; //= 0;
+extern MDD lddmc_true;// = 1;
+
+typedef struct llmsset2 {
+ uint64_t *table; // table with hashes
+ uint8_t *data; // table with values
+ uint64_t *bitmap1; // ownership bitmap (per 512 buckets)
+ uint64_t *bitmap2; // bitmap for "contains data"
+ uint64_t *bitmapc; // bitmap for "use custom functions"
+ size_t max_size; // maximum size of the hash table (for resizing)
+ size_t table_size; // size of the hash table (number of slots) --> power of 2!
+#if LLMSSET_MASK
+ size_t mask; // size-1
+#endif
+ size_t f_size;
+ llmsset_hash_cb hash_cb; // custom hash function
+ llmsset_equals_cb equals_cb; // custom equals function
+ llmsset_create_cb create_cb; // custom create function
+ llmsset_destroy_cb destroy_cb; // custom destroy function
+ int16_t threshold; // number of iterations for insertion until returning error
+} *llmsset2_t;
+
+/**
+ * LDD node structure
+ *
+ * RmRR RRRR RRRR VVVV | VVVV DcDD DDDD DDDD (little endian - in memory)
+ * VVVV RRRR RRRR RRRm | DDDD DDDD DDDc VVVV (big endian)
+ */
+typedef struct __attribute__((packed)) mddnode {
+ uint64_t a, b;
+} *mddnode_t; // 16 bytes
+
+/**
+ * Implementation of external references
+ * Based on a hash table for 40-bit non-null values, linear probing
+ * Use tombstones for deleting, higher bits for reference count
+ */
+typedef struct {
+ uint64_t *refs_table; // table itself
+ size_t refs_size; // number of buckets
+
+ /* helpers during resize operation */
+ volatile uint32_t refs_control; // control field
+ uint64_t *refs_resize_table; // previous table
+ size_t refs_resize_size; // size of previous table
+ size_t refs_resize_part; // which part is next
+ size_t refs_resize_done; // how many parts are done
+} refs_table2_t;
+/************************************** From lace.h******/
+
+
+
+typedef struct lddmc_refs_internal {
+ const MDD **pbegin, **pend, **pcur;
+ MDD *rbegin, *rend, *rcur;
+} *lddmc_refs_internal_t;
+
+
+#ifndef cas
+#define cas(ptr, old, new) (__sync_bool_compare_and_swap((ptr),(old),(new)))
+#endif
+/* Typical cacheline size of system architectures */
+#ifndef LINE_SIZE
+#define LINE_SIZE 64
+#endif
+// The LINE_SIZE is defined in lace.h
+static const uint64_t CL_MASK = ~(((LINE_SIZE) / 8) - 1);
+static const uint64_t CL_MASK_R = ((LINE_SIZE) / 8) - 1;
+/* 40 bits for the index, 24 bits for the hash */
+#define MASK_INDEX ((uint64_t)0x000000ffffffffff)
+#define MASK_HASH ((uint64_t)0xffffff0000000000)
+
+class SylvanWrapper {
+public:
+ static uint64_t getMarksCount(MDD cmark);
+
+ static llmsset2_t llmsset_create(size_t initial_size, size_t max_size);
+
+ static void llmsset_set_size(llmsset2_t dbs, size_t size);
+
+ static void sylvan_set_limits(size_t memorycap, int table_ratio, int initial_ratio);
+
+ static void sylvan_init_package(void);
+
+ static mddnode_t GETNODE(MDD mdd) { return ((mddnode_t) llmsset_index_to_ptr(m_nodes, mdd)); }
+
+ static void *llmsset_index_to_ptr(const llmsset2_t dbs, size_t index) {
+ return dbs->data + index * 16;
+ }
+
+ // Explore basic operations : to isolated to another file
+ static inline uint64_t __attribute__((unused)) mddnode_getright(mddnode_t n) {
+ return (n->a & 0x0000ffffffffffff) >> 1;
+ }
+
+ static inline uint32_t __attribute__((unused)) mddnode_getvalue(mddnode_t n) {
+ return *(uint32_t *) ((uint8_t *) n + 6);
+ }
+
+ static inline uint64_t __attribute__((unused)) mddnode_getdown(mddnode_t n) {
+ return n->b >> 17;
+ }
+
+ static void sylvan_init_ldd();
+
+ static void refs_create(refs_table2_t *tbl, size_t _refs_size);
+
+ static void protect_create(refs_table2_t *tbl, size_t _refs_size);
+
+ static void init_gc_seq();
+
+ static size_t llmsset_get_size(const llmsset2_t dbs);
+
+ static size_t seq_llmsset_count_marked(llmsset2_t dbs);
+
+ static size_t llmsset_count_marked_seq(llmsset2_t dbs, size_t first, size_t count);
+
+ static void displayMDDTableInfo();
+
+ static MDD lddmc_cube(uint32_t *values, size_t count);
+
+ static MDD lddmc_makenode(uint32_t value, MDD ifeq, MDD ifneq);
+
+ static mddnode_t LDD_GETNODE(MDD mdd);
+
+ static MDD __attribute__((unused)) lddmc_refs_push(MDD lddmc);
+
+ static void __attribute__((unused)) lddmc_refs_pop(long amount);
+
+ static MDD __attribute__((noinline)) lddmc_refs_refs_up(lddmc_refs_internal_t lddmc_refs_key, MDD res);
+
+ static size_t lddmc_nodecount(MDD mdd);
+
+ static MDD lddmc_union_mono(MDD a, MDD b);
+
+ static bool isSingleMDD(MDD mdd);
+
+ static int get_mddnbr(MDD mdd, int level);
+
+ static MDD ldd_divide_rec(MDD a, int level);
+
+ static MDD ldd_divide_internal(MDD a, int current_level, int level);
+
+ static MDD ldd_minus(MDD a, MDD b);
+
+ static MDD lddmc_firing_mono(MDD cmark, MDD minus, MDD plus);
+
+ static size_t lddmc_nodecount_mark(MDD mdd);
+
+ static void lddmc_nodecount_unmark(MDD mdd);
+
+ static MDD lddmc_make_copynode(MDD ifeq, MDD ifneq);
+
+ static void lddmc_refs_init();
+
+ static void lddmc_refs_init_task();
+
+ // sylvan_int.h
+ static inline void __attribute__((unused))
+ mddnode_makecopy(mddnode_t n, uint64_t right, uint64_t down) {
+ n->a = right << 1;
+ n->b = ((down << 1) | 1) << 16;
+ }
+
+ static inline uint8_t __attribute__((unused)) mddnode_getcopy(mddnode_t n) {
+ return n->b & 0x10000 ? 1 : 0;
+ }
+
+ static inline uint8_t __attribute__((unused)) mddnode_getmark(mddnode_t n) {
+ return n->a & 1;
+ }
+
+ static inline void __attribute__((unused)) mddnode_setmark(mddnode_t n, uint8_t mark) {
+ n->a = (n->a & 0xfffffffffffffffe) | (mark ? 1 : 0);
+ }
+
+ //sylvan_table.c
+ static inline void __attribute__((unused))
+ mddnode_make(mddnode_t n, uint32_t value, uint64_t right, uint64_t down) {
+ n->a = right << 1;
+ n->b = down << 17;
+ *(uint32_t *) ((uint8_t *) n + 6) = value;
+ }
+
+ static inline uint64_t
+ llmsset_lookup2(const llmsset2_t dbs, uint64_t a, uint64_t b, int *created, const int custom);
+
+ static uint64_t llmsset_lookup(const llmsset2_t dbs, const uint64_t a, const uint64_t b, int *created);
+
+ static uint64_t llmsset_hash(const uint64_t a, const uint64_t b, const uint64_t seed);
+
+ static uint64_t claim_data_bucket(const llmsset2_t dbs);
+
+ static void release_data_bucket(const llmsset2_t dbs, uint64_t index);
+
+ static void set_custom_bucket(const llmsset2_t dbs, uint64_t index, int on);
+
+ static void llmsset_reset_region();
+ static MDD lddmc_project( const MDD mdd, const MDD proj);
+ static int isGCRequired();
+ static void convert_wholemdd_stringcpp(MDD cmark,std::string &res);
+private:
+ static llmsset2_t m_nodes;
+ static size_t m_table_min, m_table_max, m_cache_min, m_cache_max;
+ static volatile int m_gc;
+
+ static refs_table2_t m_lddmc_refs; // External references
+ static refs_table2_t m_lddmc_protected;// External references
+ static int m_lddmc_protected_created;// External references
+
+ static lddmc_refs_internal_t m_sequentiel_refs;
+ //static lddmc_refs_internal_t m_lddmc_refs_key; // This is local to a thread
+
+ static uint32_t m_g_created;
- class SylvanWrapper {
- public:
- static uint64_t getMarksCount ( MDD cmark );
- static uint64_t m_Size;
- static uint64_t m_agg;
};
diff --git a/src/TransSylvan.cpp b/src/TransSylvan.cpp
index c532bbbdefa953c2df8829db2e6838264e2079fa..c72581f05ccdd6ec3767888f9bcddc91380cd9be 100644
--- a/src/TransSylvan.cpp
+++ b/src/TransSylvan.cpp
@@ -1,3 +1,7 @@
+#include <cstdint>
+#include <cstddef>
+#include <string>
+#include "SylvanWrapper.h"
#include "TransSylvan.h"
TransSylvan::TransSylvan(const MDD &_minus, const MDD &_plus):m_minus(_minus),m_plus(_plus)
diff --git a/src/TransSylvan.h b/src/TransSylvan.h
index 0db9fcd2c3dc01d33c735057959b1cd63cc79737..0c9849c431a8700ea0a764de31386cd87ecb8676 100755
--- a/src/TransSylvan.h
+++ b/src/TransSylvan.h
@@ -1,7 +1,8 @@
#ifndef TRANSSYLVAN_H
-#include <sylvan.h>
#define TRANSSYLVAN_H
-using namespace sylvan;
+
+
+
class TransSylvan {
public:
TransSylvan(const MDD &_minus, const MDD &_plus);
diff --git a/src/main.cpp b/src/main.cpp
index 9b6e7cd38036d8d4d90e052265cdf0352a1463cb..c20e178cbf04f210890c79c044ba73120d42a540 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -6,15 +6,13 @@
#include <fstream>
#include <mpi.h>
-#include "DistributedSOG.h"
+
+#include "LDDGraph.h"
+#include "ModelCheckerCPPThread.h"
+#include "ModelCheckerTh.h"
#include "threadSOG.h"
#include "HybridSOG.h"
#include "MCHybridSOG.h"
-#include "LDDGraph.h"
-#include "ModelCheckLace.h"
-#include "ModelCheckerTh.h"
-#include "ModelCheckerThV2.h"
-
#include <spot/misc/version.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/tl/parse.hh>
@@ -119,277 +117,284 @@ int main(int argc, char **argv) {
MPI_Comm_size(MPI_COMM_WORLD, &n_tasks);
MPI_Comm_rank(MPI_COMM_WORLD, &task_id);
- if (n_tasks == 1) {
- if (n_tasks == 1 && (!strcmp(argv[1], "otfL") || !strcmp(argv[1], "otfC") || !strcmp(argv[1], "otfP"))) {
- cout << "Performing on the fly Model checking..." << endl;
- if (!strcmp(argv[1], "otfP"))
- cout << "Multi-threaded algorithm based on Pthread library!" << endl;
- else if (!strcmp(argv[1], "otfL"))
- cout << "Multi-threaded algorithm based on Lace framework!" << endl;
- else
+
+ if (n_tasks == 1) {
+ if (n_tasks == 1 && (!strcmp(argv[1], "otfL") || !strcmp(argv[1], "otfC") || !strcmp(argv[1], "otfP"))) {
+ cout << "Performing on the fly Model checking..." << endl;
+ if (!strcmp(argv[1], "otfP"))
+ cout << "Multi-threaded algorithm based on Pthread library!" << endl;
+ else if (!strcmp(argv[1], "otfL"))
+ cout << "Multi-threaded algorithm based on Lace framework!" << endl;
+ else
cout << "Multi-threaded algorithm based on C++ Thread library!" << endl;
- cout << "Building automata for not(formula)\n";
- auto d = spot::make_bdd_dict();
-
- spot::twa_graph_ptr af = spot::translator(d).run(not_f);
- cout << "Formula automata built.\n";
- /*cout << "Want to save the graph in a dot file ?";
- char c;
- cin >> c;
- if (c == 'y') {
- fstream file;
- string st(formula);
- st += ".dot";
- file.open(st.c_str(), fstream::out);
- spot::print_dot(file, af);
- file.close();
- }
- cout << "Loading net information..." << endl;*/
- ModelCheckBaseMT *mcl;
- if (!strcmp(argv[1], "otfL"))
- mcl = new ModelCheckLace(Rnewnet, nb_th);
- else if (!strcmp(argv[1], "otfP"))
- mcl = new ModelCheckerTh(Rnewnet, nb_th);
- else
- mcl = new ModelCheckerThV2(Rnewnet, nb_th);
- mcl->loadNet();
- auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
- cout << "Performing on the fly Modelchecking" << endl;
- if (strcmp(algorithm, "")) {
- cout << "Spot emptiness check algorithm : "<<algorithm<< endl;
- shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(k,af);
- //spot::couvreur99_check_shy check = spot::couvreur99_check_shy(product);
- /****************************/
- const char *err;
- spot::emptiness_check_instantiator_ptr echeck_inst = spot::make_emptiness_check_instantiator(algorithm, &err);
-
- if (!echeck_inst) {
- cerr << "Failed to parse argument near `" << err << "'" << endl;
- cerr << "Spot unknown emptiness algorithm" << endl;
- exit(2);
- }
- auto startTime = std::chrono::steady_clock::now();
- spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
- bool res = (echptr->check() == 0);
- auto finalTime = std::chrono::steady_clock::now();
- displayTime(startTime, finalTime);
- displayCheckResult(res);
- /****************************/
-
-
-
- /*auto startTime = std::chrono::steady_clock::now();
- bool res = (check.check() == 0);
- auto finalTime = std::chrono::steady_clock::now();
- displayTime(startTime, finalTime);
- displayCheckResult(res);*/
-
- } else {
- auto startTime = std::chrono::steady_clock::now();
- bool res = (k->intersecting_run(af) == 0);
- auto finalTime = std::chrono::steady_clock::now();
- displayTime(startTime, finalTime);
- displayCheckResult(res);
- /*
- if (!resauto run = k->intersecting_run(af)) {
- cout << "formula is violated by the following run:\n" << *run << endl;
- cout << "==================================" << endl;
- /*run->highlight(5); // 5 is a color number.
- fstream file;
- file.open("violated.dot",fstream::out);
- cout<<"Property is violated!"<<endl;
- cout<<"Check the dot file."<<endl;
- spot::print_dot(file, k, ".kA");
- file.close();*/
- /*} else {
- std::cout << "formula is verified\n";
- auto finalTime = std::chrono::high_resolution_clock::now();
- displayTime(startTime, finalTime);
-
- }*/
- }
-
- delete mcl;
- }
-
- else {
- cout << "number of task = 1 \n " << endl;
- bool uselace = (!strcmp(argv[1], "lc")) || (!strcmp(argv[1], "l"));
- threadSOG DR(Rnewnet, nb_th, uselace);
- LDDGraph g(&DR);
-
- if (nb_th == 1) {
- cout << "******************Sequential version******************* \n" << endl;
- DR.computeSeqSOG(g);
- g.printCompleteInformation();
- } else {
- cout << "*******************Multithread version****************** \n" << endl;
- if (!strcmp(argv[1], "p")) {
- cout << "Construction with pthread library." << endl;
- cout << "Count of threads to be created: " << nb_th << endl;
- DR.computeDSOG(g, false);
- g.printCompleteInformation();
- } else if (!strcmp(argv[1], "pc")) {
- cout << "Canonized construction with pthread library." << endl;
- cout << "Count of threads to be created: " << nb_th << endl;
- DR.computeDSOG(g, true);
- g.printCompleteInformation();
- } else if (!strcmp(argv[1], "l")) {
- cout << "Construction with lace framework." << endl;
- cout << "Count of workers to be created: " << nb_th << endl;
- DR.computeSOGLace(g);
- g.printCompleteInformation();
- } else if (!strcmp(argv[1], "lc")) {
- cout << "Canonised construction with lace framework." << endl;
- cout << "Count of workers to be created: " << nb_th << endl;
- DR.computeSOGLaceCanonized(g);
- g.printCompleteInformation();
- }
+ cout << "Building automata for not(formula)\n";
+ auto d = spot::make_bdd_dict();
+
+ spot::twa_graph_ptr af = spot::translator(d).run(not_f);
+ cout << "Formula automata built.\n";
+ /*cout << "Want to save the graph in a dot file ?";
+ char c;
+ cin >> c;
+ if (c == 'y') {
+ fstream file;
+ string st(formula);
+ st += ".dot";
+ file.open(st.c_str(), fstream::out);
+ spot::print_dot(file, af);
+ file.close();
+ }
+ cout << "Loading net information..." << endl;*/
+ ModelCheckBaseMT *mcl;
+ /*if (!strcmp(argv[1], "otfL"))
+ mcl = new ModelCheckLace(Rnewnet, nb_th);
+ else*/
+ if (!strcmp(argv[1], "otfP"))
+ mcl = new ModelCheckerTh(Rnewnet, nb_th);
+ else
+ mcl = new ModelCheckerCPPThread(Rnewnet, nb_th);
+ mcl->loadNet();
+ auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
+ cout << "Performing on the fly Modelchecking" << endl;
+ if (strcmp(algorithm, "")) {
+ cout << "Spot emptiness check algorithm : "<<algorithm<< endl;
+ shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(k,af);
+ //spot::couvreur99_check_shy check = spot::couvreur99_check_shy(product);
+ /****************************/
+ const char *err;
+ spot::emptiness_check_instantiator_ptr echeck_inst = spot::make_emptiness_check_instantiator(algorithm, &err);
+
+ if (!echeck_inst) {
+ cerr << "Failed to parse argument near `" << err << "'" << endl;
+ cerr << "Spot unknown emptiness algorithm" << endl;
+ exit(2);
+ }
+ auto startTime = std::chrono::steady_clock::now();
+ spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
+ bool res = (echptr->check() == 0);
+ auto finalTime = std::chrono::steady_clock::now();
+ displayTime(startTime, finalTime);
+ displayCheckResult(res);
+ /****************************/
+
+ /*auto startTime = std::chrono::steady_clock::now();
+ bool res = (check.check() == 0);
+ auto finalTime = std::chrono::steady_clock::now();
+ displayTime(startTime, finalTime);
+ displayCheckResult(res);*/
+
+ } else {
+ auto startTime = std::chrono::steady_clock::now();
+ bool res = (k->intersecting_run(af) == 0);
+ auto finalTime = std::chrono::steady_clock::now();
+ displayTime(startTime, finalTime);
+ displayCheckResult(res);
/*
- cout << "Perform Model checking ?";
- char c;
- cin >> c;
- if (c == 'y') {
- cout << "Building automata for not(formula)\n";
- auto d = spot::make_bdd_dict();
- // d->register_ap("jbhkj");
- spot::twa_graph_ptr af = spot::translator(d).run(not_f);
- cout << "Formula automata built.\n";
- cout << "Want to save the graph in a dot file ?";
- cin >> c;
- if (c == 'y') {
- fstream file;
- string st(formula);
- st += ".dot";
- file.open(st.c_str(), fstream::out);
- spot::print_dot(file, af);
- file.close();
- }
- //auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP());
-
- spot::twa_graph_ptr k = spot::make_twa_graph(
- std::make_shared<SogKripke>(d, DR.getGraph(), Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP()),
- spot::twa::prop_set::all(), true);
-
- cout << "SOG translated to SPOT succeeded.." << endl;
- cout << "Want to save the graph in a dot file ?";
- cin >> c;
- if (c == 'y') {
- fstream file;
- string st(argv[3]);
- st += ".dot";
- file.open(st.c_str(), fstream::out);
- spot::print_dot(file, k, "ka");
- file.close();
- }
- if (auto run = k->intersecting_run(af)) {
- run->highlight(5);
- fstream file;
- file.open("violated.dot", fstream::out);
- cout << "Property is violated" << endl;
- cout << "Check the dot file to get a violation run" << endl;
- spot::print_dot(file, k, ".kA");
- file.close();
- } else
- std::cout << "formula is verified\n";
- }*/
-
- }
- }
+ if (!resauto run = k->intersecting_run(af)) {
+ cout << "formula is violated by the following run:\n" << *run << endl;
+ cout << "==================================" << endl;
+ /*run->highlight(5); // 5 is a color number.
+ fstream file;
+ file.open("violated.dot",fstream::out);
+ cout<<"Property is violated!"<<endl;
+ cout<<"Check the dot file."<<endl;
+ spot::print_dot(file, k, ".kA");
+ file.close();*/
+ /*} else {
+ std::cout << "formula is verified\n";
+ auto finalTime = std::chrono::high_resolution_clock::now();
+ displayTime(startTime, finalTime);
+
+ }*/
+ }
+ delete mcl;
+ }
+
+ else {
+ cout << "number of task = 1 \n " << endl;
+ bool uselace = (!strcmp(argv[1], "lc")) || (!strcmp(argv[1], "l"));
+ threadSOG DR(Rnewnet, nb_th, uselace);
+ LDDGraph g(&DR);
+
+ if (nb_th == 1) {
+ cout << "******************Sequential version******************* \n" << endl;
+ DR.computeSeqSOG(g);
+ g.printCompleteInformation();
+ } else {
+ cout << "*******************Multithread version****************** \n" << endl;
+ if (!strcmp(argv[1], "p")) {
+ cout << "Construction with pthread library." << endl;
+ cout << "Count of threads to be created: " << nb_th << endl;
+ DR.computeDSOG(g, false);
+ g.printCompleteInformation();
+ } else if (!strcmp(argv[1], "pc")) {
+ cout << "Canonized construction with pthread library." << endl;
+ cout << "Count of threads to be created: " << nb_th << endl;
+ DR.computeDSOG(g, true);
+ g.printCompleteInformation();
+ } /*else if (!strcmp(argv[1], "l")) {
+ cout << "Construction with lace framework." << endl;
+ cout << "Count of workers to be created: " << nb_th << endl;
+ DR.computeSOGLace(g);
+ g.printCompleteInformation();
+ } else if (!strcmp(argv[1], "lc")) {
+ cout << "Canonised construction with lace framework." << endl;
+ cout << "Count of workers to be created: " << nb_th << endl;
+ DR.computeSOGLaceCanonized(g);
+ g.printCompleteInformation();
+ }*/
+
+ cout << "Perform Model checking ?";
+ char c;
+ cin >> c;
+ if (c == 'y') {
+ cout << "Building automata for not(formula)\n";
+ auto d = spot::make_bdd_dict();
+
+ spot::twa_graph_ptr af = spot::translator(d).run(not_f);
+ cout << "Formula automata built.\n";
+ cout << "Want to save the graph in a dot file ?";
+ cin >> c;
+ if (c == 'y') {
+ fstream file;
+ string st(formula);
+ st += ".dot";
+ file.open(st.c_str(), fstream::out);
+ spot::print_dot(file, af);
+ file.close();
+ }
+ //auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP());
+
+ spot::twa_graph_ptr k = spot::make_twa_graph(
+ std::make_shared<SogKripke>(d, DR.getGraph(), Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP()),
+ spot::twa::prop_set::all(), true);
+
+ cout << "SOG translated to SPOT succeeded.." << endl;
+ cout << "Want to save the graph in a dot file ?";
+ cin >> c;
+ if (c == 'y') {
+ fstream file;
+ string st(argv[3]);
+ st += ".dot";
+ file.open(st.c_str(), fstream::out);
+ spot::print_dot(file, k, "ka");
+ file.close();
+ }
+ if (auto run = k->intersecting_run(af)) {
+ run->highlight(5);
+ fstream file;
+ file.open("violated.dot", fstream::out);
+ cout << "Property is violated" << endl;
+ cout << "Check the dot file to get a violation run" << endl;
+ spot::print_dot(file, k, ".kA");
+ file.close();
+ } else
+ std::cout << "formula is verified\n";
+ }
+
+ }
+ }
+
+
+ }
+
+ if (n_tasks > 1) {
+ if (nb_th > 1) {
+ if (task_id == 0)
+ cout << "**************Hybrid version**************** \n" << endl;
+ if (strcmp(argv[1], "otf")) {
+ HybridSOG DR(Rnewnet);
+ LDDGraph g(&DR);
+ if (task_id == 0)
+ cout << "Building the Distributed SOG by " << n_tasks << " processes..." << endl;
+ DR.computeDSOG(g);
+ } else {
+ n_tasks--;
+ if (task_id == n_tasks) {
+ cout << "Model checking on the fly..." << endl;
+ cout << " One process will perform Model checking" << endl;
+ cout << n_tasks << " process will build the Distributed SOG" << endl;
+ }
+ MPI_Comm gprocess;
+ MPI_Comm_split(MPI_COMM_WORLD, task_id == n_tasks ? 0 : 1, task_id, &gprocess);
+ //cout<<" Task id "<<task_id<<"/"<<n_tasks<<endl;
+ if (task_id != n_tasks) {
+ cout << "N task :" << n_tasks << endl;
+ MCHybridSOG DR(Rnewnet, gprocess, false);
+ LDDGraph g(&DR);
+ DR.computeDSOG(g);
+ } else {
+ cout << "************************************" << endl;
+ cout << "On the fly Model checker by process " << task_id << endl;
+ auto d = spot::make_bdd_dict();
+ spot::twa_graph_ptr af = spot::translator(d).run(not_f);
+ auto k = std::make_shared<HybridKripke>(d, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP(), Rnewnet);
+ if (strcmp(algorithm, "")) {
+ std::shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(af, k);
+ const char *err;
+ spot::emptiness_check_instantiator_ptr echeck_inst = spot::make_emptiness_check_instantiator(algorithm, &err);
+
+ if (!echeck_inst) {
+ cerr << "Failed to parse argument near `" << err << "'" << endl;
+ cerr << "Spot unknown emptiness algorithm" << endl;
+ exit(2);
+ }
+ else
+ cout<<"Spot emptiness check algorithm : "<<algorithm<<endl;
+ auto startTime = std::chrono::high_resolution_clock::now();
+ spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
+ bool res = (echptr->check() == 0);
+ auto finalTime = std::chrono::high_resolution_clock::now();
+ displayTime(startTime, finalTime);
+ displayCheckResult(res);
+ /*spot::couvreur99_check check = spot::couvreur99_check(product);
+ auto startTime = std::chrono::steady_clock::now();
+ bool res = (check.check() == 0);
+ auto finalTime = std::chrono::steady_clock::now();
+ displayTime(startTime, finalTime);
+ displayCheckResult(res);*/
+ } else {
+ auto startTime = std::chrono::steady_clock::now();
+ bool res = (k->intersecting_run(af) == 0);
+ auto finalTime = std::chrono::steady_clock::now();
+ displayTime(startTime, finalTime);
+ displayCheckResult(res);
+ }
+
+ /*if (auto run = k->intersecting_run(af))
+ {
+ std::cout << "formula is violated by the following run:\n"<<*run<<endl;
+ auto t2 = std::chrono::high_resolution_clock::now();
+ std::cout << "temps de verification "
+ << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
+ << " milliseconds\n";
+ cout<<"=================================="<<endl;
+ }
+ else
+ {
+ std::cout << "formula is verified\n";
+ auto t2 = std::chrono::high_resolution_clock::now();
+ std::cout << "temps de verification "
+ << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
+ << " milliseconds\n";
+
+ }*/
+ }
+ }
+ } else {
+ /*cout << "*************Distibuted version******************* \n" << endl;
+ {
+ DistributedSOG DR(Rnewnet);cout<<"Spot emptiness check algorithm : "<<algorithm<<endl;
+ LDDGraph g(nullptr);
+ DR.computeDSOG(g);
+ }*/
+ }
+ }
+
+
+
+
+
- }
- if (n_tasks > 1) {
- if (nb_th > 1) {
- if (task_id == 0)
- cout << "**************Hybrid version**************** \n" << endl;
- if (strcmp(argv[1], "otf")) {
- HybridSOG DR(Rnewnet);
- LDDGraph g(&DR);
- if (task_id == 0)
- cout << "Building the Distributed SOG by " << n_tasks << " processes..." << endl;
- DR.computeDSOG(g);
- } else {
- n_tasks--;
- if (task_id == n_tasks) {
- cout << "Model checking on the fly..." << endl;
- cout << " One process will perform Model checking" << endl;
- cout << n_tasks << " process will build the Distributed SOG" << endl;
- }
- MPI_Comm gprocess;
- MPI_Comm_split(MPI_COMM_WORLD, task_id == n_tasks ? 0 : 1, task_id, &gprocess);
- //cout<<" Task id "<<task_id<<"/"<<n_tasks<<endl;
- if (task_id != n_tasks) {
- cout << "N task :" << n_tasks << endl;
- MCHybridSOG DR(Rnewnet, gprocess, false);
- LDDGraph g(&DR);
- DR.computeDSOG(g);
- } else {
- cout << "************************************" << endl;
- cout << "On the fly Model checker by process " << task_id << endl;
- auto d = spot::make_bdd_dict();
- spot::twa_graph_ptr af = spot::translator(d).run(not_f);
- auto k = std::make_shared<HybridKripke>(d, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP(), Rnewnet);
- if (strcmp(algorithm, "")) {
- std::shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(af, k);
- const char *err;
- spot::emptiness_check_instantiator_ptr echeck_inst = spot::make_emptiness_check_instantiator(algorithm, &err);
-
- if (!echeck_inst) {
- cerr << "Failed to parse argument near `" << err << "'" << endl;
- cerr << "Spot unknown emptiness algorithm" << endl;
- exit(2);
- }
- else
- cout<<"Spot emptiness check algorithm : "<<algorithm<<endl;
- auto startTime = std::chrono::high_resolution_clock::now();
- spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
- bool res = (echptr->check() == 0);
- auto finalTime = std::chrono::high_resolution_clock::now();
- displayTime(startTime, finalTime);
- displayCheckResult(res);
- /*spot::couvreur99_check check = spot::couvreur99_check(product);
- auto startTime = std::chrono::steady_clock::now();
- bool res = (check.check() == 0);
- auto finalTime = std::chrono::steady_clock::now();
- displayTime(startTime, finalTime);
- displayCheckResult(res);*/
- } else {
- auto startTime = std::chrono::steady_clock::now();
- bool res = (k->intersecting_run(af) == 0);
- auto finalTime = std::chrono::steady_clock::now();
- displayTime(startTime, finalTime);
- displayCheckResult(res);
- }
-
- /*if (auto run = k->intersecting_run(af))
- {
- std::cout << "formula is violated by the following run:\n"<<*run<<endl;
- auto t2 = std::chrono::high_resolution_clock::now();
- std::cout << "temps de verification "
- << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
- << " milliseconds\n";
- cout<<"=================================="<<endl;
- }
- else
- {
- std::cout << "formula is verified\n";
- auto t2 = std::chrono::high_resolution_clock::now();
- std::cout << "temps de verification "
- << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
- << " milliseconds\n";
-
- }*/
- }
- }
- } else {
- cout << "*************Distibuted version******************* \n" << endl;
- {
- DistributedSOG DR(Rnewnet);cout<<"Spot emptiness check algorithm : "<<algorithm<<endl;
- LDDGraph g(nullptr);
- DR.computeDSOG(g);
- }
- }
- }
MPI_Finalize();
return (EXIT_SUCCESS);
diff --git a/src/sha2.c b/src/sha2.c
new file mode 100755
index 0000000000000000000000000000000000000000..69c7e7d5afaeb298f285170e687e9323864969f7
--- /dev/null
+++ b/src/sha2.c
@@ -0,0 +1,1052 @@
+/*
+ * FILE: sha2.c
+ * AUTHOR: Aaron D. Gifford - http://www.aarongifford.com/
+ *
+ * Copyright (c) 2000-2001, Aaron D. Gifford
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ * 3. Neither the name of the copyright holder nor the names of contributors
+ * may be used to endorse or promote products derived from this software
+ * without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTOR(S) ``AS IS'' AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTOR(S) BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+ * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+ * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+ * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+ * SUCH DAMAGE.
+ *
+ */
+
+#include <string.h> /* memcpy()/memset() or bcopy()/bzero() */
+#include <assert.h> /* assert() */
+#include "sha2.h"
+
+/*
+ * ASSERT NOTE:
+ * Some sanity checking code is included using assert(). On my FreeBSD
+ * system, this additional code can be removed by compiling with NDEBUG
+ * defined. Check your own systems manpage on assert() to see how to
+ * compile WITHOUT the sanity checking code on your system.
+ *
+ * UNROLLED TRANSFORM LOOP NOTE:
+ * You can define SHA2_UNROLL_TRANSFORM to use the unrolled transform
+ * loop version for the hash transform rounds (defined using macros
+ * later in this file). Either define on the command line, for example:
+ *
+ * cc -DSHA2_UNROLL_TRANSFORM -o sha2 sha2.c sha2prog.c
+ *
+ * or define below:
+ *
+ * #define SHA2_UNROLL_TRANSFORM
+ *
+ */
+
+
+/*** SHA-256/384/512 Machine Architecture Definitions *****************/
+/*
+ * BYTE_ORDER NOTE:
+ *
+ * Please make sure that your system defines BYTE_ORDER. If your
+ * architecture is little-endian, make sure it also defines
+ * LITTLE_ENDIAN and that the two (BYTE_ORDER and LITTLE_ENDIAN) are
+ * equivilent.
+ *
+ * If your system does not define the above, then you can do so by
+ * hand like this:
+ *
+ * #define LITTLE_ENDIAN 1234
+ * #define BIG_ENDIAN 4321
+ *
+ * And for little-endian machines, add:
+ *
+ * #define BYTE_ORDER LITTLE_ENDIAN
+ *
+ * Or for big-endian machines:
+ *
+ * #define BYTE_ORDER BIG_ENDIAN
+ *
+ * The FreeBSD machine this was written on defines BYTE_ORDER
+ * appropriately by including <sys/types.h> (which in turn includes
+ * <machine/endian.h> where the appropriate definitions are actually
+ * made).
+ */
+#if !defined(BYTE_ORDER) || (BYTE_ORDER != LITTLE_ENDIAN && BYTE_ORDER != BIG_ENDIAN)
+#error Define BYTE_ORDER to be equal to either LITTLE_ENDIAN or BIG_ENDIAN
+#endif
+
+/*
+ * Define the followingsha2_* types to types of the correct length on
+ * the native archtecture. Most BSD systems and Linux define u_intXX_t
+ * types. Machines with very recent ANSI C headers, can use the
+ * uintXX_t definintions from inttypes.h by defining SHA2_USE_INTTYPES_H
+ * during compile or in the sha.h header file.
+ *
+ * Machines that support neither u_intXX_t nor inttypes.h's uintXX_t
+ * will need to define these three typedefs below (and the appropriate
+ * ones in sha.h too) by hand according to their system architecture.
+ *
+ * Thank you, Jun-ichiro itojun Hagino, for suggesting using u_intXX_t
+ * types and pointing out recent ANSI C support for uintXX_t in inttypes.h.
+ */
+#ifdef SHA2_USE_INTTYPES_H
+
+typedef uint8_t sha2_byte; /* Exactly 1 byte */
+typedef uint32_t sha2_word32; /* Exactly 4 bytes */
+typedef uint64_t sha2_word64; /* Exactly 8 bytes */
+
+#else /* SHA2_USE_INTTYPES_H */
+
+typedef u_int8_t sha2_byte; /* Exactly 1 byte */
+typedef u_int32_t sha2_word32; /* Exactly 4 bytes */
+typedef u_int64_t sha2_word64; /* Exactly 8 bytes */
+
+#endif /* SHA2_USE_INTTYPES_H */
+
+
+/*** SHA-256/384/512 Various Length Definitions ***********************/
+/* NOTE: Most of these are in sha2.h */
+#define SHA256_SHORT_BLOCK_LENGTH (SHA256_BLOCK_LENGTH - 8)
+#define SHA384_SHORT_BLOCK_LENGTH (SHA384_BLOCK_LENGTH - 16)
+#define SHA512_SHORT_BLOCK_LENGTH (SHA512_BLOCK_LENGTH - 16)
+
+
+/*** ENDIAN REVERSAL MACROS *******************************************/
+#if BYTE_ORDER == LITTLE_ENDIAN
+#define REVERSE32(w,x) { \
+ sha2_word32 tmp = (w); \
+ tmp = (tmp >> 16) | (tmp << 16); \
+ (x) = ((tmp & 0xff00ff00UL) >> 8) | ((tmp & 0x00ff00ffUL) << 8); \
+}
+#define REVERSE64(w,x) { \
+ sha2_word64 tmp = (w); \
+ tmp = (tmp >> 32) | (tmp << 32); \
+ tmp = ((tmp & 0xff00ff00ff00ff00ULL) >> 8) | \
+ ((tmp & 0x00ff00ff00ff00ffULL) << 8); \
+ (x) = ((tmp & 0xffff0000ffff0000ULL) >> 16) | \
+ ((tmp & 0x0000ffff0000ffffULL) << 16); \
+}
+#endif /* BYTE_ORDER == LITTLE_ENDIAN */
+
+/*
+ * Macro for incrementally adding the unsigned 64-bit integer n to the
+ * unsigned 128-bit integer (represented using a two-element array of
+ * 64-bit words):
+ */
+#define ADDINC128(w,n) { \
+ (w)[0] += (sha2_word64)(n); \
+ if ((w)[0] < (n)) { \
+ (w)[1]++; \
+ } \
+}
+
+/*
+ * Macros for copying blocks of memory and for zeroing out ranges
+ * of memory. Using these macros makes it easy to switch from
+ * using memset()/memcpy() and using bzero()/bcopy().
+ *
+ * Please define either SHA2_USE_MEMSET_MEMCPY or define
+ * SHA2_USE_BZERO_BCOPY depending on which function set you
+ * choose to use:
+ */
+#if !defined(SHA2_USE_MEMSET_MEMCPY) && !defined(SHA2_USE_BZERO_BCOPY)
+/* Default to memset()/memcpy() if no option is specified */
+#define SHA2_USE_MEMSET_MEMCPY 1
+#endif
+#if defined(SHA2_USE_MEMSET_MEMCPY) && defined(SHA2_USE_BZERO_BCOPY)
+/* Abort with an error if BOTH options are defined */
+#error Define either SHA2_USE_MEMSET_MEMCPY or SHA2_USE_BZERO_BCOPY, not both!
+#endif
+
+#ifdef SHA2_USE_MEMSET_MEMCPY
+#define MEMSET_BZERO(p,l) memset((p), 0, (l))
+#define MEMCPY_BCOPY(d,s,l) memcpy((d), (s), (l))
+#endif
+#ifdef SHA2_USE_BZERO_BCOPY
+#define MEMSET_BZERO(p,l) bzero((p), (l))
+#define MEMCPY_BCOPY(d,s,l) bcopy((s), (d), (l))
+#endif
+
+
+/*** THE SIX LOGICAL FUNCTIONS ****************************************/
+/*
+ * Bit shifting and rotation (used by the six SHA-XYZ logical functions:
+ *
+ * NOTE: The naming of R and S appears backwards here (R is a SHIFT and
+ * S is a ROTATION) because the SHA-256/384/512 description document
+ * (see http://csrc.nist.gov/cryptval/shs/sha256-384-512.pdf) uses this
+ * same "backwards" definition.
+ */
+/* Shift-right (used in SHA-256, SHA-384, and SHA-512): */
+#define R(b,x) ((x) >> (b))
+/* 32-bit Rotate-right (used in SHA-256): */
+#define S32(b,x) (((x) >> (b)) | ((x) << (32 - (b))))
+/* 64-bit Rotate-right (used in SHA-384 and SHA-512): */
+#define S64(b,x) (((x) >> (b)) | ((x) << (64 - (b))))
+
+/* Two of six logical functions used in SHA-256, SHA-384, and SHA-512: */
+#define Ch(x,y,z) (((x) & (y)) ^ ((~(x)) & (z)))
+#define Maj(x,y,z) (((x) & (y)) ^ ((x) & (z)) ^ ((y) & (z)))
+
+/* Four of six logical functions used in SHA-256: */
+#define Sigma0_256(x) (S32(2, (x)) ^ S32(13, (x)) ^ S32(22, (x)))
+#define Sigma1_256(x) (S32(6, (x)) ^ S32(11, (x)) ^ S32(25, (x)))
+#define sigma0_256(x) (S32(7, (x)) ^ S32(18, (x)) ^ R(3 , (x)))
+#define sigma1_256(x) (S32(17, (x)) ^ S32(19, (x)) ^ R(10, (x)))
+
+/* Four of six logical functions used in SHA-384 and SHA-512: */
+#define Sigma0_512(x) (S64(28, (x)) ^ S64(34, (x)) ^ S64(39, (x)))
+#define Sigma1_512(x) (S64(14, (x)) ^ S64(18, (x)) ^ S64(41, (x)))
+#define sigma0_512(x) (S64( 1, (x)) ^ S64( 8, (x)) ^ R( 7, (x)))
+#define sigma1_512(x) (S64(19, (x)) ^ S64(61, (x)) ^ R( 6, (x)))
+
+/*** INTERNAL FUNCTION PROTOTYPES *************************************/
+/* NOTE: These should not be accessed directly from outside this
+ * library -- they are intended for private internal visibility/use
+ * only.
+ */
+void SHA512_Last(SHA512_CTX*);
+void SHA256_Transform(SHA256_CTX*, const sha2_word32*);
+void SHA512_Transform(SHA512_CTX*, const sha2_word64*);
+
+
+/*** SHA-XYZ INITIAL HASH VALUES AND CONSTANTS ************************/
+/* Hash constant words K for SHA-256: */
+static const sha2_word32 K256[64] = {
+ 0x428a2f98UL, 0x71374491UL, 0xb5c0fbcfUL, 0xe9b5dba5UL,
+ 0x3956c25bUL, 0x59f111f1UL, 0x923f82a4UL, 0xab1c5ed5UL,
+ 0xd807aa98UL, 0x12835b01UL, 0x243185beUL, 0x550c7dc3UL,
+ 0x72be5d74UL, 0x80deb1feUL, 0x9bdc06a7UL, 0xc19bf174UL,
+ 0xe49b69c1UL, 0xefbe4786UL, 0x0fc19dc6UL, 0x240ca1ccUL,
+ 0x2de92c6fUL, 0x4a7484aaUL, 0x5cb0a9dcUL, 0x76f988daUL,
+ 0x983e5152UL, 0xa831c66dUL, 0xb00327c8UL, 0xbf597fc7UL,
+ 0xc6e00bf3UL, 0xd5a79147UL, 0x06ca6351UL, 0x14292967UL,
+ 0x27b70a85UL, 0x2e1b2138UL, 0x4d2c6dfcUL, 0x53380d13UL,
+ 0x650a7354UL, 0x766a0abbUL, 0x81c2c92eUL, 0x92722c85UL,
+ 0xa2bfe8a1UL, 0xa81a664bUL, 0xc24b8b70UL, 0xc76c51a3UL,
+ 0xd192e819UL, 0xd6990624UL, 0xf40e3585UL, 0x106aa070UL,
+ 0x19a4c116UL, 0x1e376c08UL, 0x2748774cUL, 0x34b0bcb5UL,
+ 0x391c0cb3UL, 0x4ed8aa4aUL, 0x5b9cca4fUL, 0x682e6ff3UL,
+ 0x748f82eeUL, 0x78a5636fUL, 0x84c87814UL, 0x8cc70208UL,
+ 0x90befffaUL, 0xa4506cebUL, 0xbef9a3f7UL, 0xc67178f2UL
+};
+
+/* Initial hash value H for SHA-256: */
+static const sha2_word32 sha256_initial_hash_value[8] = {
+ 0x6a09e667UL,
+ 0xbb67ae85UL,
+ 0x3c6ef372UL,
+ 0xa54ff53aUL,
+ 0x510e527fUL,
+ 0x9b05688cUL,
+ 0x1f83d9abUL,
+ 0x5be0cd19UL
+};
+
+/* Hash constant words K for SHA-384 and SHA-512: */
+static const sha2_word64 K512[80] = {
+ 0x428a2f98d728ae22ULL, 0x7137449123ef65cdULL,
+ 0xb5c0fbcfec4d3b2fULL, 0xe9b5dba58189dbbcULL,
+ 0x3956c25bf348b538ULL, 0x59f111f1b605d019ULL,
+ 0x923f82a4af194f9bULL, 0xab1c5ed5da6d8118ULL,
+ 0xd807aa98a3030242ULL, 0x12835b0145706fbeULL,
+ 0x243185be4ee4b28cULL, 0x550c7dc3d5ffb4e2ULL,
+ 0x72be5d74f27b896fULL, 0x80deb1fe3b1696b1ULL,
+ 0x9bdc06a725c71235ULL, 0xc19bf174cf692694ULL,
+ 0xe49b69c19ef14ad2ULL, 0xefbe4786384f25e3ULL,
+ 0x0fc19dc68b8cd5b5ULL, 0x240ca1cc77ac9c65ULL,
+ 0x2de92c6f592b0275ULL, 0x4a7484aa6ea6e483ULL,
+ 0x5cb0a9dcbd41fbd4ULL, 0x76f988da831153b5ULL,
+ 0x983e5152ee66dfabULL, 0xa831c66d2db43210ULL,
+ 0xb00327c898fb213fULL, 0xbf597fc7beef0ee4ULL,
+ 0xc6e00bf33da88fc2ULL, 0xd5a79147930aa725ULL,
+ 0x06ca6351e003826fULL, 0x142929670a0e6e70ULL,
+ 0x27b70a8546d22ffcULL, 0x2e1b21385c26c926ULL,
+ 0x4d2c6dfc5ac42aedULL, 0x53380d139d95b3dfULL,
+ 0x650a73548baf63deULL, 0x766a0abb3c77b2a8ULL,
+ 0x81c2c92e47edaee6ULL, 0x92722c851482353bULL,
+ 0xa2bfe8a14cf10364ULL, 0xa81a664bbc423001ULL,
+ 0xc24b8b70d0f89791ULL, 0xc76c51a30654be30ULL,
+ 0xd192e819d6ef5218ULL, 0xd69906245565a910ULL,
+ 0xf40e35855771202aULL, 0x106aa07032bbd1b8ULL,
+ 0x19a4c116b8d2d0c8ULL, 0x1e376c085141ab53ULL,
+ 0x2748774cdf8eeb99ULL, 0x34b0bcb5e19b48a8ULL,
+ 0x391c0cb3c5c95a63ULL, 0x4ed8aa4ae3418acbULL,
+ 0x5b9cca4f7763e373ULL, 0x682e6ff3d6b2b8a3ULL,
+ 0x748f82ee5defb2fcULL, 0x78a5636f43172f60ULL,
+ 0x84c87814a1f0ab72ULL, 0x8cc702081a6439ecULL,
+ 0x90befffa23631e28ULL, 0xa4506cebde82bde9ULL,
+ 0xbef9a3f7b2c67915ULL, 0xc67178f2e372532bULL,
+ 0xca273eceea26619cULL, 0xd186b8c721c0c207ULL,
+ 0xeada7dd6cde0eb1eULL, 0xf57d4f7fee6ed178ULL,
+ 0x06f067aa72176fbaULL, 0x0a637dc5a2c898a6ULL,
+ 0x113f9804bef90daeULL, 0x1b710b35131c471bULL,
+ 0x28db77f523047d84ULL, 0x32caab7b40c72493ULL,
+ 0x3c9ebe0a15c9bebcULL, 0x431d67c49c100d4cULL,
+ 0x4cc5d4becb3e42b6ULL, 0x597f299cfc657e2aULL,
+ 0x5fcb6fab3ad6faecULL, 0x6c44198c4a475817ULL
+};
+
+/* Initial hash value H for SHA-384 */
+static const sha2_word64 sha384_initial_hash_value[8] = {
+ 0xcbbb9d5dc1059ed8ULL,
+ 0x629a292a367cd507ULL,
+ 0x9159015a3070dd17ULL,
+ 0x152fecd8f70e5939ULL,
+ 0x67332667ffc00b31ULL,
+ 0x8eb44a8768581511ULL,
+ 0xdb0c2e0d64f98fa7ULL,
+ 0x47b5481dbefa4fa4ULL
+};
+
+/* Initial hash value H for SHA-512 */
+static const sha2_word64 sha512_initial_hash_value[8] = {
+ 0x6a09e667f3bcc908ULL,
+ 0xbb67ae8584caa73bULL,
+ 0x3c6ef372fe94f82bULL,
+ 0xa54ff53a5f1d36f1ULL,
+ 0x510e527fade682d1ULL,
+ 0x9b05688c2b3e6c1fULL,
+ 0x1f83d9abfb41bd6bULL,
+ 0x5be0cd19137e2179ULL
+};
+
+/*
+ * Constant used by SHA256/384/512_End() functions for converting the
+ * digest to a readable hexadecimal character string:
+ */
+static const char *sha2_hex_digits = "0123456789abcdef";
+
+
+/*** SHA-256: *********************************************************/
+void SHA256_Init(SHA256_CTX* context) {
+ if (context == (SHA256_CTX*)0) {
+ return;
+ }
+ MEMCPY_BCOPY(context->state, sha256_initial_hash_value, SHA256_DIGEST_LENGTH);
+ MEMSET_BZERO(context->buffer, SHA256_BLOCK_LENGTH);
+ context->bitcount = 0;
+}
+
+#ifdef SHA2_UNROLL_TRANSFORM
+
+/* Unrolled SHA-256 round macros: */
+
+#if BYTE_ORDER == LITTLE_ENDIAN
+
+#define ROUND256_0_TO_15(a,b,c,d,e,f,g,h) \
+ REVERSE32(*data++, W256[j]); \
+ T1 = (h) + Sigma1_256(e) + Ch((e), (f), (g)) + \
+ K256[j] + W256[j]; \
+ (d) += T1; \
+ (h) = T1 + Sigma0_256(a) + Maj((a), (b), (c)); \
+ j++
+
+
+#else /* BYTE_ORDER == LITTLE_ENDIAN */
+
+#define ROUND256_0_TO_15(a,b,c,d,e,f,g,h) \
+ T1 = (h) + Sigma1_256(e) + Ch((e), (f), (g)) + \
+ K256[j] + (W256[j] = *data++); \
+ (d) += T1; \
+ (h) = T1 + Sigma0_256(a) + Maj((a), (b), (c)); \
+ j++
+
+#endif /* BYTE_ORDER == LITTLE_ENDIAN */
+
+#define ROUND256(a,b,c,d,e,f,g,h) \
+ s0 = W256[(j+1)&0x0f]; \
+ s0 = sigma0_256(s0); \
+ s1 = W256[(j+14)&0x0f]; \
+ s1 = sigma1_256(s1); \
+ T1 = (h) + Sigma1_256(e) + Ch((e), (f), (g)) + K256[j] + \
+ (W256[j&0x0f] += s1 + W256[(j+9)&0x0f] + s0); \
+ (d) += T1; \
+ (h) = T1 + Sigma0_256(a) + Maj((a), (b), (c)); \
+ j++
+
+void SHA256_Transform(SHA256_CTX* context, const sha2_word32* data) {
+ sha2_word32 a, b, c, d, e, f, g, h, s0, s1;
+ sha2_word32 T1, *W256;
+ int j;
+
+ W256 = (sha2_word32*)context->buffer;
+
+ /* Initialize registers with the prev. intermediate value */
+ a = context->state[0];
+ b = context->state[1];
+ c = context->state[2];
+ d = context->state[3];
+ e = context->state[4];
+ f = context->state[5];
+ g = context->state[6];
+ h = context->state[7];
+
+ j = 0;
+ do {
+ /* Rounds 0 to 15 (unrolled): */
+ ROUND256_0_TO_15(a,b,c,d,e,f,g,h);
+ ROUND256_0_TO_15(h,a,b,c,d,e,f,g);
+ ROUND256_0_TO_15(g,h,a,b,c,d,e,f);
+ ROUND256_0_TO_15(f,g,h,a,b,c,d,e);
+ ROUND256_0_TO_15(e,f,g,h,a,b,c,d);
+ ROUND256_0_TO_15(d,e,f,g,h,a,b,c);
+ ROUND256_0_TO_15(c,d,e,f,g,h,a,b);
+ ROUND256_0_TO_15(b,c,d,e,f,g,h,a);
+ } while (j < 16);
+
+ /* Now for the remaining rounds to 64: */
+ do {
+ ROUND256(a,b,c,d,e,f,g,h);
+ ROUND256(h,a,b,c,d,e,f,g);
+ ROUND256(g,h,a,b,c,d,e,f);
+ ROUND256(f,g,h,a,b,c,d,e);
+ ROUND256(e,f,g,h,a,b,c,d);
+ ROUND256(d,e,f,g,h,a,b,c);
+ ROUND256(c,d,e,f,g,h,a,b);
+ ROUND256(b,c,d,e,f,g,h,a);
+ } while (j < 64);
+
+ /* Compute the current intermediate hash value */
+ context->state[0] += a;
+ context->state[1] += b;
+ context->state[2] += c;
+ context->state[3] += d;
+ context->state[4] += e;
+ context->state[5] += f;
+ context->state[6] += g;
+ context->state[7] += h;
+
+ /* Clean up */
+ a = b = c = d = e = f = g = h = T1 = 0;
+}
+
+#else /* SHA2_UNROLL_TRANSFORM */
+
+void SHA256_Transform(SHA256_CTX* context, const sha2_word32* data) {
+ sha2_word32 a, b, c, d, e, f, g, h, s0, s1;
+ sha2_word32 T1, T2, *W256;
+ int j;
+
+ W256 = (sha2_word32*)context->buffer;
+
+ /* Initialize registers with the prev. intermediate value */
+ a = context->state[0];
+ b = context->state[1];
+ c = context->state[2];
+ d = context->state[3];
+ e = context->state[4];
+ f = context->state[5];
+ g = context->state[6];
+ h = context->state[7];
+
+ j = 0;
+ do {
+#if BYTE_ORDER == LITTLE_ENDIAN
+ /* Copy data while converting to host byte order */
+ REVERSE32(*data++,W256[j]);
+ /* Apply the SHA-256 compression function to update a..h */
+ T1 = h + Sigma1_256(e) + Ch(e, f, g) + K256[j] + W256[j];
+#else /* BYTE_ORDER == LITTLE_ENDIAN */
+ /* Apply the SHA-256 compression function to update a..h with copy */
+ T1 = h + Sigma1_256(e) + Ch(e, f, g) + K256[j] + (W256[j] = *data++);
+#endif /* BYTE_ORDER == LITTLE_ENDIAN */
+ T2 = Sigma0_256(a) + Maj(a, b, c);
+ h = g;
+ g = f;
+ f = e;
+ e = d + T1;
+ d = c;
+ c = b;
+ b = a;
+ a = T1 + T2;
+
+ j++;
+ } while (j < 16);
+
+ do {
+ /* Part of the message block expansion: */
+ s0 = W256[(j+1)&0x0f];
+ s0 = sigma0_256(s0);
+ s1 = W256[(j+14)&0x0f];
+ s1 = sigma1_256(s1);
+
+ /* Apply the SHA-256 compression function to update a..h */
+ T1 = h + Sigma1_256(e) + Ch(e, f, g) + K256[j] +
+ (W256[j&0x0f] += s1 + W256[(j+9)&0x0f] + s0);
+ T2 = Sigma0_256(a) + Maj(a, b, c);
+ h = g;
+ g = f;
+ f = e;
+ e = d + T1;
+ d = c;
+ c = b;
+ b = a;
+ a = T1 + T2;
+
+ j++;
+ } while (j < 64);
+
+ /* Compute the current intermediate hash value */
+ context->state[0] += a;
+ context->state[1] += b;
+ context->state[2] += c;
+ context->state[3] += d;
+ context->state[4] += e;
+ context->state[5] += f;
+ context->state[6] += g;
+ context->state[7] += h;
+}
+
+#endif /* SHA2_UNROLL_TRANSFORM */
+
+void SHA256_Update(SHA256_CTX* context, const sha2_byte *data, size_t len) {
+ unsigned int freespace, usedspace;
+
+ if (len == 0) {
+ /* Calling with no data is valid - we do nothing */
+ return;
+ }
+
+ /* Sanity check: */
+ assert(context != (SHA256_CTX*)0 && data != (sha2_byte*)0);
+
+ usedspace = (context->bitcount >> 3) % SHA256_BLOCK_LENGTH;
+ if (usedspace > 0) {
+ /* Calculate how much free space is available in the buffer */
+ freespace = SHA256_BLOCK_LENGTH - usedspace;
+
+ if (len >= freespace) {
+ /* Fill the buffer completely and process it */
+ MEMCPY_BCOPY(&context->buffer[usedspace], data, freespace);
+ context->bitcount += freespace << 3;
+ len -= freespace;
+ data += freespace;
+ SHA256_Transform(context, (sha2_word32*)context->buffer);
+ } else {
+ /* The buffer is not yet full */
+ MEMCPY_BCOPY(&context->buffer[usedspace], data, len);
+ context->bitcount += len << 3;
+ return;
+ }
+ }
+ while (len >= SHA256_BLOCK_LENGTH) {
+ /* Process as many complete blocks as we can */
+ SHA256_Transform(context, (sha2_word32*)data);
+ context->bitcount += SHA256_BLOCK_LENGTH << 3;
+ len -= SHA256_BLOCK_LENGTH;
+ data += SHA256_BLOCK_LENGTH;
+ }
+ if (len > 0) {
+ /* There's left-overs, so save 'em */
+ MEMCPY_BCOPY(context->buffer, data, len);
+ context->bitcount += len << 3;
+ }
+}
+
+void SHA256_Final(sha2_byte digest[], SHA256_CTX* context) {
+ sha2_word32 *d = (sha2_word32*)digest;
+ unsigned int usedspace;
+
+ /* Sanity check: */
+ assert(context != (SHA256_CTX*)0);
+
+ /* If no digest buffer is passed, we don't bother doing this: */
+ if (digest != (sha2_byte*)0) {
+ usedspace = (context->bitcount >> 3) % SHA256_BLOCK_LENGTH;
+#if BYTE_ORDER == LITTLE_ENDIAN
+ /* Convert FROM host byte order */
+ REVERSE64(context->bitcount,context->bitcount);
+#endif
+ if (usedspace > 0) {
+ /* Begin padding with a 1 bit: */
+ context->buffer[usedspace++] = 0x80;
+
+ if (usedspace <= SHA256_SHORT_BLOCK_LENGTH) {
+ /* Set-up for the last transform: */
+ MEMSET_BZERO(&context->buffer[usedspace], SHA256_SHORT_BLOCK_LENGTH - usedspace);
+ } else {
+ if (usedspace < SHA256_BLOCK_LENGTH) {
+ MEMSET_BZERO(&context->buffer[usedspace], SHA256_BLOCK_LENGTH - usedspace);
+ }
+ /* Do second-to-last transform: */
+ SHA256_Transform(context, (sha2_word32*)context->buffer);
+
+ /* And set-up for the last transform: */
+ MEMSET_BZERO(context->buffer, SHA256_SHORT_BLOCK_LENGTH);
+ }
+ } else {
+ /* Set-up for the last transform: */
+ MEMSET_BZERO(context->buffer, SHA256_SHORT_BLOCK_LENGTH);
+
+ /* Begin padding with a 1 bit: */
+ *context->buffer = 0x80;
+ }
+ /* Set the bit count: */
+ sha2_word64* ptr = (sha2_word64*)(&context->buffer[SHA256_SHORT_BLOCK_LENGTH]);
+ *ptr = context->bitcount;
+
+ /* Final transform: */
+ SHA256_Transform(context, (sha2_word32*)context->buffer);
+
+#if BYTE_ORDER == LITTLE_ENDIAN
+ {
+ /* Convert TO host byte order */
+ int j;
+ for (j = 0; j < 8; j++) {
+ REVERSE32(context->state[j],context->state[j]);
+ *d++ = context->state[j];
+ }
+ }
+#else
+ MEMCPY_BCOPY(d, context->state, SHA256_DIGEST_LENGTH);
+#endif
+ }
+
+ /* Clean up state data: */
+ MEMSET_BZERO(context, sizeof(SHA256_CTX));
+}
+
+char *SHA256_End(SHA256_CTX* context, char buffer[]) {
+ sha2_byte digest[SHA256_DIGEST_LENGTH], *d = digest;
+ int i;
+
+ /* Sanity check: */
+ assert(context != (SHA256_CTX*)0);
+
+ if (buffer != (char*)0) {
+ SHA256_Final(digest, context);
+
+ for (i = 0; i < SHA256_DIGEST_LENGTH; i++) {
+ *buffer++ = sha2_hex_digits[(*d & 0xf0) >> 4];
+ *buffer++ = sha2_hex_digits[*d & 0x0f];
+ d++;
+ }
+ *buffer = (char)0;
+ } else {
+ MEMSET_BZERO(context, sizeof(SHA256_CTX));
+ }
+ MEMSET_BZERO(digest, SHA256_DIGEST_LENGTH);
+ return buffer;
+}
+
+char* SHA256_Data(const sha2_byte* data, size_t len, char digest[SHA256_DIGEST_STRING_LENGTH]) {
+ SHA256_CTX context;
+
+ SHA256_Init(&context);
+ SHA256_Update(&context, data, len);
+ return SHA256_End(&context, digest);
+}
+
+
+/*** SHA-512: *********************************************************/
+void SHA512_Init(SHA512_CTX* context) {
+ if (context == (SHA512_CTX*)0) {
+ return;
+ }
+ MEMCPY_BCOPY(context->state, sha512_initial_hash_value, SHA512_DIGEST_LENGTH);
+ MEMSET_BZERO(context->buffer, SHA512_BLOCK_LENGTH);
+ context->bitcount[0] = context->bitcount[1] = 0;
+}
+
+#ifdef SHA2_UNROLL_TRANSFORM
+
+/* Unrolled SHA-512 round macros: */
+#if BYTE_ORDER == LITTLE_ENDIAN
+
+#define ROUND512_0_TO_15(a,b,c,d,e,f,g,h) \
+ REVERSE64(*data++, W512[j]); \
+ T1 = (h) + Sigma1_512(e) + Ch((e), (f), (g)) + \
+ K512[j] + W512[j]; \
+ (d) += T1, \
+ (h) = T1 + Sigma0_512(a) + Maj((a), (b), (c)), \
+ j++
+
+
+#else /* BYTE_ORDER == LITTLE_ENDIAN */
+
+#define ROUND512_0_TO_15(a,b,c,d,e,f,g,h) \
+ T1 = (h) + Sigma1_512(e) + Ch((e), (f), (g)) + \
+ K512[j] + (W512[j] = *data++); \
+ (d) += T1; \
+ (h) = T1 + Sigma0_512(a) + Maj((a), (b), (c)); \
+ j++
+
+#endif /* BYTE_ORDER == LITTLE_ENDIAN */
+
+#define ROUND512(a,b,c,d,e,f,g,h) \
+ s0 = W512[(j+1)&0x0f]; \
+ s0 = sigma0_512(s0); \
+ s1 = W512[(j+14)&0x0f]; \
+ s1 = sigma1_512(s1); \
+ T1 = (h) + Sigma1_512(e) + Ch((e), (f), (g)) + K512[j] + \
+ (W512[j&0x0f] += s1 + W512[(j+9)&0x0f] + s0); \
+ (d) += T1; \
+ (h) = T1 + Sigma0_512(a) + Maj((a), (b), (c)); \
+ j++
+
+void SHA512_Transform(SHA512_CTX* context, const sha2_word64* data) {
+ sha2_word64 a, b, c, d, e, f, g, h, s0, s1;
+ sha2_word64 T1, *W512 = (sha2_word64*)context->buffer;
+ int j;
+
+ /* Initialize registers with the prev. intermediate value */
+ a = context->state[0];
+ b = context->state[1];
+ c = context->state[2];
+ d = context->state[3];
+ e = context->state[4];
+ f = context->state[5];
+ g = context->state[6];
+ h = context->state[7];
+
+ j = 0;
+ do {
+ ROUND512_0_TO_15(a,b,c,d,e,f,g,h);
+ ROUND512_0_TO_15(h,a,b,c,d,e,f,g);
+ ROUND512_0_TO_15(g,h,a,b,c,d,e,f);
+ ROUND512_0_TO_15(f,g,h,a,b,c,d,e);
+ ROUND512_0_TO_15(e,f,g,h,a,b,c,d);
+ ROUND512_0_TO_15(d,e,f,g,h,a,b,c);
+ ROUND512_0_TO_15(c,d,e,f,g,h,a,b);
+ ROUND512_0_TO_15(b,c,d,e,f,g,h,a);
+ } while (j < 16);
+
+ /* Now for the remaining rounds up to 79: */
+ do {
+ ROUND512(a,b,c,d,e,f,g,h);
+ ROUND512(h,a,b,c,d,e,f,g);
+ ROUND512(g,h,a,b,c,d,e,f);
+ ROUND512(f,g,h,a,b,c,d,e);
+ ROUND512(e,f,g,h,a,b,c,d);
+ ROUND512(d,e,f,g,h,a,b,c);
+ ROUND512(c,d,e,f,g,h,a,b);
+ ROUND512(b,c,d,e,f,g,h,a);
+ } while (j < 80);
+
+ /* Compute the current intermediate hash value */
+ context->state[0] += a;
+ context->state[1] += b;
+ context->state[2] += c;
+ context->state[3] += d;
+ context->state[4] += e;
+ context->state[5] += f;
+ context->state[6] += g;
+ context->state[7] += h;
+
+ /* Clean up */
+ a = b = c = d = e = f = g = h = T1 = 0;
+}
+
+#else /* SHA2_UNROLL_TRANSFORM */
+
+void SHA512_Transform(SHA512_CTX* context, const sha2_word64* data) {
+ sha2_word64 a, b, c, d, e, f, g, h, s0, s1;
+ sha2_word64 T1, T2, *W512 = (sha2_word64*)context->buffer;
+ int j;
+
+ /* Initialize registers with the prev. intermediate value */
+ a = context->state[0];
+ b = context->state[1];
+ c = context->state[2];
+ d = context->state[3];
+ e = context->state[4];
+ f = context->state[5];
+ g = context->state[6];
+ h = context->state[7];
+
+ j = 0;
+ do {
+#if BYTE_ORDER == LITTLE_ENDIAN
+ /* Convert TO host byte order */
+ REVERSE64(*data++, W512[j]);
+ /* Apply the SHA-512 compression function to update a..h */
+ T1 = h + Sigma1_512(e) + Ch(e, f, g) + K512[j] + W512[j];
+#else /* BYTE_ORDER == LITTLE_ENDIAN */
+ /* Apply the SHA-512 compression function to update a..h with copy */
+ T1 = h + Sigma1_512(e) + Ch(e, f, g) + K512[j] + (W512[j] = *data++);
+#endif /* BYTE_ORDER == LITTLE_ENDIAN */
+ T2 = Sigma0_512(a) + Maj(a, b, c);
+ h = g;
+ g = f;
+ f = e;
+ e = d + T1;
+ d = c;
+ c = b;
+ b = a;
+ a = T1 + T2;
+
+ j++;
+ } while (j < 16);
+
+ do {
+ /* Part of the message block expansion: */
+ s0 = W512[(j+1)&0x0f];
+ s0 = sigma0_512(s0);
+ s1 = W512[(j+14)&0x0f];
+ s1 = sigma1_512(s1);
+
+ /* Apply the SHA-512 compression function to update a..h */
+ T1 = h + Sigma1_512(e) + Ch(e, f, g) + K512[j] +
+ (W512[j&0x0f] += s1 + W512[(j+9)&0x0f] + s0);
+ T2 = Sigma0_512(a) + Maj(a, b, c);
+ h = g;
+ g = f;
+ f = e;
+ e = d + T1;
+ d = c;
+ c = b;
+ b = a;
+ a = T1 + T2;
+
+ j++;
+ } while (j < 80);
+
+ /* Compute the current intermediate hash value */
+ context->state[0] += a;
+ context->state[1] += b;
+ context->state[2] += c;
+ context->state[3] += d;
+ context->state[4] += e;
+ context->state[5] += f;
+ context->state[6] += g;
+ context->state[7] += h;
+}
+
+#endif /* SHA2_UNROLL_TRANSFORM */
+
+void SHA512_Update(SHA512_CTX* context, const sha2_byte *data, size_t len) {
+ unsigned int freespace, usedspace;
+
+ if (len == 0) {
+ /* Calling with no data is valid - we do nothing */
+ return;
+ }
+
+ /* Sanity check: */
+ assert(context != (SHA512_CTX*)0 && data != (sha2_byte*)0);
+
+ usedspace = (context->bitcount[0] >> 3) % SHA512_BLOCK_LENGTH;
+ if (usedspace > 0) {
+ /* Calculate how much free space is available in the buffer */
+ freespace = SHA512_BLOCK_LENGTH - usedspace;
+
+ if (len >= freespace) {
+ /* Fill the buffer completely and process it */
+ MEMCPY_BCOPY(&context->buffer[usedspace], data, freespace);
+ ADDINC128(context->bitcount, freespace << 3);
+ len -= freespace;
+ data += freespace;
+ SHA512_Transform(context, (sha2_word64*)context->buffer);
+ } else {
+ /* The buffer is not yet full */
+ MEMCPY_BCOPY(&context->buffer[usedspace], data, len);
+ ADDINC128(context->bitcount, len << 3);
+ return;
+ }
+ }
+ while (len >= SHA512_BLOCK_LENGTH) {
+ /* Process as many complete blocks as we can */
+ SHA512_Transform(context, (sha2_word64*)data);
+ ADDINC128(context->bitcount, SHA512_BLOCK_LENGTH << 3);
+ len -= SHA512_BLOCK_LENGTH;
+ data += SHA512_BLOCK_LENGTH;
+ }
+ if (len > 0) {
+ /* There's left-overs, so save 'em */
+ MEMCPY_BCOPY(context->buffer, data, len);
+ ADDINC128(context->bitcount, len << 3);
+ }
+}
+
+void SHA512_Last(SHA512_CTX* context) {
+ unsigned int usedspace;
+
+ usedspace = (context->bitcount[0] >> 3) % SHA512_BLOCK_LENGTH;
+#if BYTE_ORDER == LITTLE_ENDIAN
+ /* Convert FROM host byte order */
+ REVERSE64(context->bitcount[0],context->bitcount[0]);
+ REVERSE64(context->bitcount[1],context->bitcount[1]);
+#endif
+ if (usedspace > 0) {
+ /* Begin padding with a 1 bit: */
+ context->buffer[usedspace++] = 0x80;
+
+ if (usedspace <= SHA512_SHORT_BLOCK_LENGTH) {
+ /* Set-up for the last transform: */
+ MEMSET_BZERO(&context->buffer[usedspace], SHA512_SHORT_BLOCK_LENGTH - usedspace);
+ } else {
+ if (usedspace < SHA512_BLOCK_LENGTH) {
+ MEMSET_BZERO(&context->buffer[usedspace], SHA512_BLOCK_LENGTH - usedspace);
+ }
+ /* Do second-to-last transform: */
+ SHA512_Transform(context, (sha2_word64*)context->buffer);
+
+ /* And set-up for the last transform: */
+ MEMSET_BZERO(context->buffer, SHA512_BLOCK_LENGTH - 2);
+ }
+ } else {
+ /* Prepare for final transform: */
+ MEMSET_BZERO(context->buffer, SHA512_SHORT_BLOCK_LENGTH);
+
+ /* Begin padding with a 1 bit: */
+ *context->buffer = 0x80;
+ }
+ /* Store the length of input data (in bits): */
+ sha2_word64 *ptr = (sha2_word64*)(&context->buffer[SHA512_SHORT_BLOCK_LENGTH]);
+ *ptr = context->bitcount[1];
+ ptr = (sha2_word64*)(&context->buffer[SHA512_SHORT_BLOCK_LENGTH+8]);
+ *ptr = context->bitcount[0];
+
+ /* Final transform: */
+ SHA512_Transform(context, (sha2_word64*)context->buffer);
+}
+
+void SHA512_Final(sha2_byte digest[], SHA512_CTX* context) {
+ sha2_word64 *d = (sha2_word64*)digest;
+
+ /* Sanity check: */
+ assert(context != (SHA512_CTX*)0);
+
+ /* If no digest buffer is passed, we don't bother doing this: */
+ if (digest != (sha2_byte*)0) {
+ SHA512_Last(context);
+
+ /* Save the hash data for output: */
+#if BYTE_ORDER == LITTLE_ENDIAN
+ {
+ /* Convert TO host byte order */
+ int j;
+ for (j = 0; j < 8; j++) {
+ REVERSE64(context->state[j],context->state[j]);
+ *d++ = context->state[j];
+ }
+ }
+#else
+ MEMCPY_BCOPY(d, context->state, SHA512_DIGEST_LENGTH);
+#endif
+ }
+
+ /* Zero out state data */
+ MEMSET_BZERO(context, sizeof(SHA512_CTX));
+}
+
+char *SHA512_End(SHA512_CTX* context, char buffer[]) {
+ sha2_byte digest[SHA512_DIGEST_LENGTH], *d = digest;
+ int i;
+
+ /* Sanity check: */
+ assert(context != (SHA512_CTX*)0);
+
+ if (buffer != (char*)0) {
+ SHA512_Final(digest, context);
+
+ for (i = 0; i < SHA512_DIGEST_LENGTH; i++) {
+ *buffer++ = sha2_hex_digits[(*d & 0xf0) >> 4];
+ *buffer++ = sha2_hex_digits[*d & 0x0f];
+ d++;
+ }
+ *buffer = (char)0;
+ } else {
+ MEMSET_BZERO(context, sizeof(SHA512_CTX));
+ }
+ MEMSET_BZERO(digest, SHA512_DIGEST_LENGTH);
+ return buffer;
+}
+
+char* SHA512_Data(const sha2_byte* data, size_t len, char digest[SHA512_DIGEST_STRING_LENGTH]) {
+ SHA512_CTX context;
+
+ SHA512_Init(&context);
+ SHA512_Update(&context, data, len);
+ return SHA512_End(&context, digest);
+}
+
+
+/*** SHA-384: *********************************************************/
+void SHA384_Init(SHA384_CTX* context) {
+ if (context == (SHA384_CTX*)0) {
+ return;
+ }
+ MEMCPY_BCOPY(context->state, sha384_initial_hash_value, SHA512_DIGEST_LENGTH);
+ MEMSET_BZERO(context->buffer, SHA384_BLOCK_LENGTH);
+ context->bitcount[0] = context->bitcount[1] = 0;
+}
+
+void SHA384_Update(SHA384_CTX* context, const sha2_byte* data, size_t len) {
+ SHA512_Update((SHA512_CTX*)context, data, len);
+}
+
+void SHA384_Final(sha2_byte digest[], SHA384_CTX* context) {
+ sha2_word64 *d = (sha2_word64*)digest;
+
+ /* Sanity check: */
+ assert(context != (SHA384_CTX*)0);
+
+ /* If no digest buffer is passed, we don't bother doing this: */
+ if (digest != (sha2_byte*)0) {
+ SHA512_Last((SHA512_CTX*)context);
+
+ /* Save the hash data for output: */
+#if BYTE_ORDER == LITTLE_ENDIAN
+ {
+ /* Convert TO host byte order */
+ int j;
+ for (j = 0; j < 6; j++) {
+ REVERSE64(context->state[j],context->state[j]);
+ *d++ = context->state[j];
+ }
+ }
+#else
+ MEMCPY_BCOPY(d, context->state, SHA384_DIGEST_LENGTH);
+#endif
+ }
+
+ /* Zero out state data */
+ MEMSET_BZERO(context, sizeof(SHA384_CTX));
+}
+
+char *SHA384_End(SHA384_CTX* context, char buffer[]) {
+ sha2_byte digest[SHA384_DIGEST_LENGTH], *d = digest;
+ int i;
+
+ /* Sanity check: */
+ assert(context != (SHA384_CTX*)0);
+
+ if (buffer != (char*)0) {
+ SHA384_Final(digest, context);
+
+ for (i = 0; i < SHA384_DIGEST_LENGTH; i++) {
+ *buffer++ = sha2_hex_digits[(*d & 0xf0) >> 4];
+ *buffer++ = sha2_hex_digits[*d & 0x0f];
+ d++;
+ }
+ *buffer = (char)0;
+ } else {
+ MEMSET_BZERO(context, sizeof(SHA384_CTX));
+ }
+ MEMSET_BZERO(digest, SHA384_DIGEST_LENGTH);
+ return buffer;
+}
+
+char* SHA384_Data(const sha2_byte* data, size_t len, char digest[SHA384_DIGEST_STRING_LENGTH]) {
+ SHA384_CTX context;
+
+ SHA384_Init(&context);
+ SHA384_Update(&context, data, len);
+ return SHA384_End(&context, digest);
+}
+
diff --git a/src/sha2.h b/src/sha2.h
new file mode 100755
index 0000000000000000000000000000000000000000..bf759ad45ba01030013d19832d4201a99e12dc8b
--- /dev/null
+++ b/src/sha2.h
@@ -0,0 +1,197 @@
+/*
+ * FILE: sha2.h
+ * AUTHOR: Aaron D. Gifford - http://www.aarongifford.com/
+ *
+ * Copyright (c) 2000-2001, Aaron D. Gifford
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ * 3. Neither the name of the copyright holder nor the names of contributors
+ * may be used to endorse or promote products derived from this software
+ * without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTOR(S) ``AS IS'' AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTOR(S) BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+ * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+ * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+ * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+ * SUCH DAMAGE.
+ *
+ * $Id: sha2.h,v 1.1 2001/11/08 00:02:01 adg Exp adg $
+ */
+
+#ifndef __SHA2_H__
+#define __SHA2_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+
+/*
+ * Import u_intXX_t size_t type definitions from system headers. You
+ * may need to change this, or define these things yourself in this
+ * file.
+ */
+#include <sys/types.h>
+
+#ifdef SHA2_USE_INTTYPES_H
+
+#include <inttypes.h>
+
+#endif /* SHA2_USE_INTTYPES_H */
+
+
+/*** SHA-256/384/512 Various Length Definitions ***********************/
+#define SHA256_BLOCK_LENGTH 64
+#define SHA256_DIGEST_LENGTH 32
+#define SHA256_DIGEST_STRING_LENGTH (SHA256_DIGEST_LENGTH * 2 + 1)
+#define SHA384_BLOCK_LENGTH 128
+#define SHA384_DIGEST_LENGTH 48
+#define SHA384_DIGEST_STRING_LENGTH (SHA384_DIGEST_LENGTH * 2 + 1)
+#define SHA512_BLOCK_LENGTH 128
+#define SHA512_DIGEST_LENGTH 64
+#define SHA512_DIGEST_STRING_LENGTH (SHA512_DIGEST_LENGTH * 2 + 1)
+
+
+/*** SHA-256/384/512 Context Structures *******************************/
+/* NOTE: If your architecture does not define either u_intXX_t types or
+ * uintXX_t (from inttypes.h), you may need to define things by hand
+ * for your system:
+ */
+#if 0
+typedef unsigned char u_int8_t; /* 1-byte (8-bits) */
+typedef unsigned int u_int32_t; /* 4-bytes (32-bits) */
+typedef unsigned long long u_int64_t; /* 8-bytes (64-bits) */
+#endif
+/*
+ * Most BSD systems already define u_intXX_t types, as does Linux.
+ * Some systems, however, like Compaq's Tru64 Unix instead can use
+ * uintXX_t types defined by very recent ANSI C standards and included
+ * in the file:
+ *
+ * #include <inttypes.h>
+ *
+ * If you choose to use <inttypes.h> then please define:
+ *
+ * #define SHA2_USE_INTTYPES_H
+ *
+ * Or on the command line during compile:
+ *
+ * cc -DSHA2_USE_INTTYPES_H ...
+ */
+#ifdef SHA2_USE_INTTYPES_H
+
+typedef struct _SHA256_CTX {
+ uint32_t state[8];
+ uint64_t bitcount;
+ uint8_t buffer[SHA256_BLOCK_LENGTH];
+} SHA256_CTX;
+typedef struct _SHA512_CTX {
+ uint64_t state[8];
+ uint64_t bitcount[2];
+ uint8_t buffer[SHA512_BLOCK_LENGTH];
+} SHA512_CTX;
+
+#else /* SHA2_USE_INTTYPES_H */
+
+typedef struct _SHA256_CTX {
+ u_int32_t state[8];
+ u_int64_t bitcount;
+ u_int8_t buffer[SHA256_BLOCK_LENGTH];
+} SHA256_CTX;
+typedef struct _SHA512_CTX {
+ u_int64_t state[8];
+ u_int64_t bitcount[2];
+ u_int8_t buffer[SHA512_BLOCK_LENGTH];
+} SHA512_CTX;
+
+#endif /* SHA2_USE_INTTYPES_H */
+
+typedef SHA512_CTX SHA384_CTX;
+
+
+/*** SHA-256/384/512 Function Prototypes ******************************/
+#ifndef NOPROTO
+#ifdef SHA2_USE_INTTYPES_H
+
+void SHA256_Init(SHA256_CTX *);
+void SHA256_Update(SHA256_CTX*, const uint8_t*, size_t);
+void SHA256_Final(uint8_t[SHA256_DIGEST_LENGTH], SHA256_CTX*);
+char* SHA256_End(SHA256_CTX*, char[SHA256_DIGEST_STRING_LENGTH]);
+char* SHA256_Data(const uint8_t*, size_t, char[SHA256_DIGEST_STRING_LENGTH]);
+
+void SHA384_Init(SHA384_CTX*);
+void SHA384_Update(SHA384_CTX*, const uint8_t*, size_t);
+void SHA384_Final(uint8_t[SHA384_DIGEST_LENGTH], SHA384_CTX*);
+char* SHA384_End(SHA384_CTX*, char[SHA384_DIGEST_STRING_LENGTH]);
+char* SHA384_Data(const uint8_t*, size_t, char[SHA384_DIGEST_STRING_LENGTH]);
+
+void SHA512_Init(SHA512_CTX*);
+void SHA512_Update(SHA512_CTX*, const uint8_t*, size_t);
+void SHA512_Final(uint8_t[SHA512_DIGEST_LENGTH], SHA512_CTX*);
+char* SHA512_End(SHA512_CTX*, char[SHA512_DIGEST_STRING_LENGTH]);
+char* SHA512_Data(const uint8_t*, size_t, char[SHA512_DIGEST_STRING_LENGTH]);
+
+#else /* SHA2_USE_INTTYPES_H */
+
+void SHA256_Init(SHA256_CTX *);
+void SHA256_Update(SHA256_CTX*, const u_int8_t*, size_t);
+void SHA256_Final(u_int8_t[SHA256_DIGEST_LENGTH], SHA256_CTX*);
+char* SHA256_End(SHA256_CTX*, char[SHA256_DIGEST_STRING_LENGTH]);
+char* SHA256_Data(const u_int8_t*, size_t, char[SHA256_DIGEST_STRING_LENGTH]);
+
+void SHA384_Init(SHA384_CTX*);
+void SHA384_Update(SHA384_CTX*, const u_int8_t*, size_t);
+void SHA384_Final(u_int8_t[SHA384_DIGEST_LENGTH], SHA384_CTX*);
+char* SHA384_End(SHA384_CTX*, char[SHA384_DIGEST_STRING_LENGTH]);
+char* SHA384_Data(const u_int8_t*, size_t, char[SHA384_DIGEST_STRING_LENGTH]);
+
+void SHA512_Init(SHA512_CTX*);
+void SHA512_Update(SHA512_CTX*, const u_int8_t*, size_t);
+void SHA512_Final(u_int8_t[SHA512_DIGEST_LENGTH], SHA512_CTX*);
+char* SHA512_End(SHA512_CTX*, char[SHA512_DIGEST_STRING_LENGTH]);
+char* SHA512_Data(const u_int8_t*, size_t, char[SHA512_DIGEST_STRING_LENGTH]);
+
+#endif /* SHA2_USE_INTTYPES_H */
+
+#else /* NOPROTO */
+
+void SHA256_Init();
+void SHA256_Update();
+void SHA256_Final();
+char* SHA256_End();
+char* SHA256_Data();
+
+void SHA384_Init();
+void SHA384_Update();
+void SHA384_Final();
+char* SHA384_End();
+char* SHA384_Data();
+
+void SHA512_Init();
+void SHA512_Update();
+void SHA512_Final();
+char* SHA512_End();
+char* SHA512_Data();
+
+#endif /* NOPROTO */
+
+#ifdef __cplusplus
+}
+#endif /* __cplusplus */
+
+#endif /* __SHA2_H__ */
+
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index 847cf0bb681b2c79422e47291506c82a5116458e..b06eda55111b7276c0af65e8b516146b31a44a97 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -5,19 +5,16 @@
//#define DEBUG_GC
#include "threadSOG.h"
-#include "sylvan.h"
-#include "sylvan_seq.h"
-#include <sylvan_sog.h>
-#include <sylvan_int.h>
-using namespace sylvan;
+
+/*
void write_to_dot(const char *ch,MDD m)
{
FILE *fp=fopen(ch,"w");
lddmc_fprintdot(fp,m);
fclose(fp);
-}
+}*/
/*************************************************/
@@ -29,23 +26,14 @@ void write_to_dot(const char *ch,MDD m)
threadSOG::threadSOG(const NewNet &R, int nbThread,bool uselace,bool init)
{
m_nb_thread=nbThread;
- if (uselace) {
- lace_init(m_nb_thread, 10000000);
- }
- else lace_init(1, 0);
- lace_startup(0, NULL, NULL);
-
- // Simple Sylvan initialization, also initialize MDD support
- //sylvan_set_sizes(1LL<<27, 1LL<<27, 1LL<<20, 1LL<<22);
- sylvan_set_limits(16LL<<30, 8, 0);
-
- //sylvan_set_limits(2LL<<30, 16, 3);
- //sylvan_set_sizes(1LL<<30, 2LL<<20, 1LL<<18, 1LL<<20);
- //sylvan_init_bdd(1);
- sylvan_init_package();
- sylvan_init_ldd();
- LACE_ME;
- displayMDDTableInfo();
+ uselace=uselace;
+ SylvanWrapper::sylvan_set_limits ( 16LL<<30, 8, 0 );
+
+ //sylvan_init_package();
+ SylvanWrapper::sylvan_init_package();
+ SylvanWrapper::sylvan_init_ldd();
+ SylvanWrapper::init_gc_seq();
+ SylvanWrapper::displayMDDTableInfo();
/*sylvan_gc_hook_pregc(TASK(gc_start));
sylvan_gc_hook_postgc(TASK(gc_end));
sylvan_gc_enable();*/
@@ -56,7 +44,7 @@ threadSOG::threadSOG(const NewNet &R, int nbThread,bool uselace,bool init)
vector<Place>::const_iterator it_places;
- init_gc_seq();
+
//_______________
@@ -65,12 +53,12 @@ threadSOG::threadSOG(const NewNet &R, int nbThread,bool uselace,bool init)
m_place_proposition=R.m_formula_place;
m_nonObservable=R.NonObservable;
- m_transitionName=R.transitionName;
- m_placeName=R.m_placePosName;
+ m_transitionName=&R.transitionName;
+ m_placeName=&R.m_placePosName;
- /* cout<<"Toutes les Transitions:"<<endl;
- map<string,uint16_t>::iterator it2=m_transitionName.begin();
- for (;it2!=m_transitionName.end();it2++) {
+ cout<<"Toutes les Transitions:"<<endl;
+ map<string,uint16_t>::iterator it2=m_transitionName->begin();
+ for (;it2!=m_transitionName->end();it2++) {
cout<<(*it2).first<<" : "<<(*it2).second<<endl;}
@@ -78,7 +66,7 @@ threadSOG::threadSOG(const NewNet &R, int nbThread,bool uselace,bool init)
cout<<"Transitions observables :"<<endl;
Set::iterator it=m_observable.begin();
for (;it!=m_observable.end();it++) {cout<<*it<<" ";}
- cout<<endl;*/
+ cout<<endl;
InterfaceTrans=R.InterfaceTrans;
m_nbPlaces=R.places.size();
cout<<"Nombre de places : "<<m_nbPlaces<<endl;
@@ -90,7 +78,7 @@ threadSOG::threadSOG(const NewNet &R, int nbThread,bool uselace,bool init)
liste_marques[i] =it_places->marking;
}
- m_initialMarking=lddmc_cube(liste_marques,R.places.size());
+ m_initialMarking=SylvanWrapper::lddmc_cube(liste_marques,R.places.size());
uint32_t *prec = new uint32_t[m_nbPlaces];
uint32_t *postc= new uint32_t [m_nbPlaces];
@@ -126,10 +114,10 @@ threadSOG::threadSOG(const NewNet &R, int nbThread,bool uselace,bool init)
Precond = Precond & ((*it) >= prec[*it]);
}
- MDD _minus=lddmc_cube(prec,m_nbPlaces);
- ldd_refs_push(_minus);
- MDD _plus=lddmc_cube(postc,m_nbPlaces);
- ldd_refs_push(_plus);
+ MDD _minus=SylvanWrapper::lddmc_cube(prec,m_nbPlaces);
+ //#ldd_refs_push(_minus);
+ MDD _plus=SylvanWrapper::lddmc_cube(postc,m_nbPlaces);
+ //#ldd_refs_push(_plus);
m_tb_relation.push_back(TransSylvan(_minus,_plus));
}
@@ -190,14 +178,14 @@ void threadSOG::computeSeqSOG(LDDGraph &g)
c->m_lddstate=Complete_meta_state;
//TabMeta[m_nbmetastate]=c->m_lddstate;
m_nbmetastate++;
- old_size=lddmc_nodecount(c->m_lddstate);
+
//max_meta_state_size=bdd_pathcount(Complete_meta_state);
st.push(Pair(couple(c,Complete_meta_state),fire));
g.setInitialState(c);
g.insert(c);
//LACE_ME;
- g.m_nbMarking+=lddmc_nodecount(c->m_lddstate);
+ g.m_nbMarking+=SylvanWrapper::lddmc_nodecount(c->m_lddstate);
do
{
m_NbIt++;
@@ -216,7 +204,7 @@ void threadSOG::computeSeqSOG(LDDGraph &g)
MDD Complete_meta_state=Accessible_epsilon(get_successor(e.first.second,t));
//MDD reduced_meta=Canonize(Complete_meta_state,0);
- ldd_refs_push(Complete_meta_state);
+ //#ldd_refs_push(Complete_meta_state);
//ldd_refs_push(reduced_meta);
//sylvan_gc_seq();
@@ -301,7 +289,7 @@ void * threadSOG::doCompute()
// cout<<bddtable<<M0<<endl;
MDD Complete_meta_state(Accessible_epsilon(m_initialMarking));
- ldd_refs_push(Complete_meta_state);
+ //#ldd_refs_push(Complete_meta_state);
// MDD canonised_initial=Canonize(Complete_meta_state,0);
//ldd_refs_push(canonised_initial);
fire=firable_obs(Complete_meta_state);
@@ -309,7 +297,7 @@ void * threadSOG::doCompute()
c->m_lddstate=Complete_meta_state;
//m_TabMeta[m_nbmetastate]=c->m_lddstate;
m_nbmetastate++;
- m_old_size=lddmc_nodecount(c->m_lddstate);
+ m_old_size=SylvanWrapper::lddmc_nodecount(c->m_lddstate);
//max_meta_state_size=bdd_pathcount(Complete_meta_state);
m_st[0].push(Pair(couple(c,Complete_meta_state),fire));
@@ -356,7 +344,7 @@ void * threadSOG::doCompute()
MDD Complete_meta_state=Accessible_epsilon(get_successor(e.first.second,t));
- ldd_refs_push(Complete_meta_state);
+ //#ldd_refs_push(Complete_meta_state);
//MDD reduced_meta=Canonize(Complete_meta_state,0);
//ldd_refs_push(reduced_meta);
@@ -367,7 +355,7 @@ void * threadSOG::doCompute()
// #ifdef DEBUG_GC
// displayMDDTableInfo();
// #endif // DEBUG_GC
- sylvan_gc_seq();
+ //# sylvan_gc_seq();
// #ifdef DEBUG_GC
// displayMDDTableInfo();
// #endif // DEBUG_GC
@@ -463,16 +451,16 @@ void * threadSOG::doComputeCanonized()
// cout<<bddtable<<M0<<endl;
MDD Complete_meta_state(Accessible_epsilon(m_initialMarking));
- ldd_refs_push(Complete_meta_state);
+ //#ldd_refs_push(Complete_meta_state);
MDD canonised_initial=Canonize(Complete_meta_state,0);
- ldd_refs_push(canonised_initial);
+ //#ldd_refs_push(canonised_initial);
fire=firable_obs(Complete_meta_state);
c->m_lddstate=canonised_initial;
//m_TabMeta[m_nbmetastate]=c->m_lddstate;
m_nbmetastate++;
- m_old_size=lddmc_nodecount(c->m_lddstate);
+ m_old_size=SylvanWrapper::lddmc_nodecount(c->m_lddstate);
//max_meta_state_size=bdd_pathcount(Complete_meta_state);
m_st[0].push(Pair(couple(c,Complete_meta_state),fire));
@@ -521,10 +509,10 @@ void * threadSOG::doComputeCanonized()
MDD Complete_meta_state=Accessible_epsilon(get_successor(e.first.second,t));
- ldd_refs_push(Complete_meta_state);
+ //#ldd_refs_push(Complete_meta_state);
MDD reduced_meta=Canonize(Complete_meta_state,0);
- ldd_refs_push(reduced_meta);
+ //#ldd_refs_push(reduced_meta);
if (id_thread==0)
{
@@ -532,7 +520,7 @@ void * threadSOG::doComputeCanonized()
// #ifdef DEBUG_GC
// displayMDDTableInfo();
// #endif // DEBUG_GC
- sylvan_gc_seq();
+ //# sylvan_gc_seq();
// #ifdef DEBUG_GC
// displayMDDTableInfo();
// #endif // DEBUG_GC
@@ -619,8 +607,8 @@ void threadSOG::computeDSOG(LDDGraph &g,bool canonised)
cout << "number of threads "<<m_nb_thread<<endl;
int rc;
m_graph=&g;
- m_graph->setTransition(m_transitionName);
- m_graph->setPlace(m_placeName);
+ m_graph->setTransition(*m_transitionName);
+ m_graph->setPlace(*m_placeName);
m_id_thread=0;
pthread_mutex_init(&m_mutex, NULL);
@@ -701,7 +689,7 @@ threadSOG::~threadSOG()
/******************* Functions computing SOG with Lace *****************/
/***** Saturation with Lace *********/
-
+/*
TASK_3 (MDD, ImageForwardLace,MDD, From, Set* , NonObservable, vector<TransSylvan>*, tb_relation)
{
MDD Res=lddmc_false;
@@ -762,14 +750,15 @@ TASK_3 (MDD, Accessible_epsilon_lace, MDD, From, Set*, nonObservable, vector<Tra
return M2;
}
-
+*/
/********************* Compute SOG with lace *********************************************/
+/*
void threadSOG::computeSOGLace(LDDGraph &g)
{
clock_gettime(CLOCK_REALTIME, &start);
Set fire;
m_graph=&g;
- m_graph->setTransition(m_transitionName);
+ m_graph->setTransition(*m_transitionName);
m_graph->setPlace(m_placeName);
m_nbmetastate=0;
m_MaxIntBdd=0;
@@ -850,16 +839,16 @@ void threadSOG::computeSOGLace(LDDGraph &g)
tps = (finish.tv_sec - start.tv_sec);
tps += (finish.tv_nsec - start.tv_nsec) / 1000000000.0;
std::cout << "TIME OF CONSTRUCTION OF THE SOG " << tps << " seconds\n";
-}
+}*/
/********************* Compute canonized SOG with lace *********************************************/
/******************************Canonizer with lace framework **********************************/
-TASK_DECL_3(MDD, lddmc_canonize,MDD, unsigned int, threadSOG *)
-#define lddmc_canonize(s,level,ds) CALL(lddmc_canonize, s, level,ds)
-
+/*TASK_DECL_3(MDD, lddmc_canonize,MDD, unsigned int, threadSOG *)
+#define lddmc_canonize(s,level,ds) CALL(lddmc_canonize, s, level,ds)*/
+/*
TASK_IMPL_3(MDD, lddmc_canonize,MDD, s,unsigned int, level, threadSOG * ,ds)
{
@@ -934,7 +923,7 @@ TASK_IMPL_3(MDD, lddmc_canonize,MDD, s,unsigned int, level, threadSOG * ,ds)
if (isSingleMDD(s1)) {
/*lddmc_refs_spawn(SPAWN(lddmc_canonize,s0,level,ds));
Repr=lddmc_refs_sync(SYNC(lddmc_canonize));*/
- Repr=CALL(lddmc_canonize,s0,level,ds);
+/* Repr=CALL(lddmc_canonize,s0,level,ds);
Repr=lddmc_union(Repr,s1);
}
else {
@@ -1045,7 +1034,7 @@ void threadSOG::computeSOGLaceCanonized(LDDGraph &g)
tps = (finish.tv_sec - start.tv_sec);
tps += (finish.tv_nsec - start.tv_nsec) / 1000000000.0;
std::cout << "TIME OF CONSTRUCTION OF THE SOG " << tps << " seconds\n";
-}
+}*/
diff --git a/third-party/sylvan b/third-party/sylvan
deleted file mode 160000
index 035a0aca68ec77dbfe8b48ed8c58c3ebf8a469bb..0000000000000000000000000000000000000000
--- a/third-party/sylvan
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 035a0aca68ec77dbfe8b48ed8c58c3ebf8a469bb