summaryrefslogtreecommitdiffstats
path: root/src/misc
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc')
-rw-r--r--src/misc/extra/extra.h4
-rw-r--r--src/misc/extra/extraBddMisc.c228
-rw-r--r--src/misc/hash/hashGen.h13
-rw-r--r--src/misc/st/st.c38
-rw-r--r--src/misc/st/st.h24
-rw-r--r--src/misc/st/stmm.c64
-rw-r--r--src/misc/st/stmm.h21
-rw-r--r--src/misc/util/abc_global.h12
-rw-r--r--src/misc/util/module.make4
-rw-r--r--src/misc/util/utilCex.c205
-rw-r--r--src/misc/util/utilCex.h72
-rw-r--r--src/misc/util/utilFile.c73
-rw-r--r--src/misc/util/utilSignal.c487
-rw-r--r--src/misc/util/utilSignal.h29
-rw-r--r--src/misc/util/util_hack.h47
15 files changed, 669 insertions, 652 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 240fee03..693c25bd 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -198,6 +198,8 @@ extern void Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, D
extern DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
extern DdNode * Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
extern DdNode * extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
+extern int Extra_bddVarIsInCube( DdNode * bCube, int iVar );
+extern DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
#ifndef ABC_PRB
#define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
@@ -611,7 +613,7 @@ extern char * Extra_UtilTildeExpand( char *fname );
extern char * Extra_UtilFileSearch( char *file, char *path, char *mode );
extern void (*Extra_UtilMMoutOfMemory)( long size );
-extern const char * globalUtilOptarg;
+extern const char * globalUtilOptarg;
extern int globalUtilOptind;
/**AutomaticEnd***************************************************************/
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 69309a4d..7d63980a 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -55,6 +55,8 @@ static DdNode * extraTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdN
static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute );
static DdNode * cuddBddPermuteRecur ARGS( ( DdManager * manager, DdHashTable * table, DdNode * node, int *permut ) );
+static DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
+
// file "cuddUtils.c"
static void ddSupportStep(DdNode *f, int *support);
static void ddClearFlag(DdNode *f);
@@ -1039,6 +1041,75 @@ DdNode * Extra_bddChangePolarity(
} /* end of Extra_bddChangePolarity */
+/**Function*************************************************************
+
+ Synopsis [Checks if the given variable belongs to the cube.]
+
+ Description [Return -1 if the var does not appear in the cube.
+ Otherwise, returns polarity (0 or 1) of the var in the cube.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Extra_bddVarIsInCube( DdNode * bCube, int iVar )
+{
+ DdNode * bCube0, * bCube1;
+ while ( Cudd_Regular(bCube)->index != CUDD_CONST_INDEX )
+ {
+ bCube0 = Cudd_NotCond( cuddE(Cudd_Regular(bCube)), Cudd_IsComplement(bCube) );
+ bCube1 = Cudd_NotCond( cuddT(Cudd_Regular(bCube)), Cudd_IsComplement(bCube) );
+ // make sure it is a cube
+ assert( (Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX) || // bCube0 == 0
+ (Cudd_IsComplement(bCube1) && Cudd_Regular(bCube1)->index == CUDD_CONST_INDEX) ); // bCube1 == 0
+ // quit if it is the last one
+ if ( Cudd_Regular(bCube)->index == iVar )
+ return (int)(Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX);
+ // get the next cube
+ if ( (Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX) )
+ bCube = bCube1;
+ else
+ bCube = bCube0;
+ }
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the AND of two BDD with different orders.]
+
+ Description [Derives the result of Boolean AND of bF and bG in ddF.
+ The array pPermute gives the mapping of variables of ddG into that of ddF.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute )
+{
+ DdHashTable * table;
+ DdNode * bRes;
+ do
+ {
+ ddF->reordered = 0;
+ table = cuddHashTableInit( ddF, 2, 256 );
+ if (table == NULL) return NULL;
+ bRes = extraBddAndPermute( table, ddF, bF, ddG, bG, pPermute );
+ if ( bRes ) cuddRef( bRes );
+ cuddHashTableQuit( table );
+ if ( bRes ) cuddDeref( bRes );
+//if ( ddF->reordered == 1 )
+//printf( "Reordering happened\n" );
+ }
+ while ( ddF->reordered == 1 );
+//printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d\n",
+// Cudd_DagSize(bF), Cudd_DagSize(bG), Cudd_DagSize(bRes),
+// Cudd_DagSize(bF) * Cudd_DagSize(bG) );
+ return ( bRes );
+}
+
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
@@ -1277,6 +1348,11 @@ extraTransferPermuteRecur(
if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )
return ( Cudd_NotCond( res, comple ) );
+ if ( ddS->TimeStop && ddS->TimeStop < clock() )
+ return NULL;
+ if ( ddD->TimeStop && ddD->TimeStop < clock() )
+ return NULL;
+
/* Recursive step. */
if ( Permute )
index = Permute[f->index];
@@ -1800,6 +1876,158 @@ DdNode * extraBddChangePolarity(
} /* end of extraBddChangePolarity */
+
+static int Counter = 0;
+
+/**Function*************************************************************
+
+ Synopsis [Computes the AND of two BDD with different orders.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute )
+{
+ DdNode * bF0, * bF1, * bG0, * bG1, * bRes0, * bRes1, * bRes, * bVar;
+ int LevF, LevG, Lev;
+
+ // if F == 0, return 0
+ if ( bF == Cudd_Not(ddF->one) )
+ return Cudd_Not(ddF->one);
+ // if G == 0, return 0
+ if ( bG == Cudd_Not(ddG->one) )
+ return Cudd_Not(ddF->one);
+ // if G == 1, return F
+ if ( bG == ddG->one )
+ return bF;
+ // cannot use F == 1, because the var order of G has to be changed
+
+ // check cache
+ if ( //(Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1) &&
+ (bRes = cuddHashTableLookup2(table, bF, bG)) )
+ return bRes;
+ Counter++;
+
+ if ( ddF->TimeStop && ddF->TimeStop < clock() )
+ return NULL;
+ if ( ddG->TimeStop && ddG->TimeStop < clock() )
+ return NULL;
+
+ // find the topmost variable in F and G using var order of F
+ LevF = cuddI( ddF, Cudd_Regular(bF)->index );
+ LevG = cuddI( ddF, pPermute ? pPermute[Cudd_Regular(bG)->index] : Cudd_Regular(bG)->index );
+ Lev = ABC_MIN( LevF, LevG );
+ assert( Lev < ddF->size );
+ bVar = ddF->vars[ddF->invperm[Lev]];
+
+ // cofactor
+ bF0 = (Lev < LevF) ? bF : Cudd_NotCond( cuddE(Cudd_Regular(bF)), Cudd_IsComplement(bF) );
+ bF1 = (Lev < LevF) ? bF : Cudd_NotCond( cuddT(Cudd_Regular(bF)), Cudd_IsComplement(bF) );
+ bG0 = (Lev < LevG) ? bG : Cudd_NotCond( cuddE(Cudd_Regular(bG)), Cudd_IsComplement(bG) );
+ bG1 = (Lev < LevG) ? bG : Cudd_NotCond( cuddT(Cudd_Regular(bG)), Cudd_IsComplement(bG) );
+
+ // call for cofactors
+ bRes0 = extraBddAndPermute( table, ddF, bF0, ddG, bG0, pPermute );
+ if ( bRes0 == NULL )
+ return NULL;
+ cuddRef( bRes0 );
+ // call for cofactors
+ bRes1 = extraBddAndPermute( table, ddF, bF1, ddG, bG1, pPermute );
+ if ( bRes1 == NULL )
+ {
+ Cudd_IterDerefBdd( ddF, bRes0 );
+ return NULL;
+ }
+ cuddRef( bRes1 );
+
+ // compose the result
+ bRes = cuddBddIteRecur( ddF, bVar, bRes1, bRes0 );
+ if ( bRes == NULL )
+ {
+ Cudd_IterDerefBdd( ddF, bRes0 );
+ Cudd_IterDerefBdd( ddF, bRes1 );
+ return NULL;
+ }
+ cuddRef( bRes );
+ Cudd_IterDerefBdd( ddF, bRes0 );
+ Cudd_IterDerefBdd( ddF, bRes1 );
+
+ // cache the result
+// if ( Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1 )
+ {
+ ptrint fanout = (ptrint)Cudd_Regular(bF)->ref * Cudd_Regular(bG)->ref;
+ cuddSatDec(fanout);
+ cuddHashTableInsert2( table, bF, bG, bRes, fanout );
+ }
+ cuddDeref( bRes );
+ return bRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Testbench.]
+
+ Description [This procedure takes BDD manager ddF and two BDDs
+ in this manager (bF and bG). It creates a new manager ddG,
+ transfers bG into it and then reorders it, resulting in bG2.
+ Then it tries to compute the product of bF and bG2 in ddF.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_TestAndPerm( DdManager * ddF, DdNode * bF, DdNode * bG )
+{
+ DdManager * ddG;
+ DdNode * bG2, * bRes1, * bRes2;
+ int clk;
+ // disable variable ordering in ddF
+ Cudd_AutodynDisable( ddF );
+
+ // create new BDD manager
+ ddG = Cudd_Init( ddF->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+ // transfer BDD into it
+ Cudd_ShuffleHeap( ddG, ddF->invperm );
+ bG2 = Extra_TransferLevelByLevel( ddF, ddG, bG ); Cudd_Ref( bG2 );
+ // reorder the new manager
+ Cudd_ReduceHeap( ddG, CUDD_REORDER_SYMM_SIFT, 1 );
+
+ // compute the result
+clk = clock();
+ bRes1 = Cudd_bddAnd( ddF, bF, bG ); Cudd_Ref( bRes1 );
+Abc_PrintTime( 1, "Runtime of Cudd_bddAnd ", clock() - clk );
+
+ // compute the result
+Counter = 0;
+clk = clock();
+ bRes2 = Extra_bddAndPermute( ddF, bF, ddG, bG2, NULL ); Cudd_Ref( bRes2 );
+Abc_PrintTime( 1, "Runtime of new procedure", clock() - clk );
+printf( "Recursive calls = %d\n", Counter );
+printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d ",
+ Cudd_DagSize(bF), Cudd_DagSize(bG), Cudd_DagSize(bRes2),
+ Cudd_DagSize(bF) * Cudd_DagSize(bG) );
+
+ if ( bRes1 == bRes2 )
+ printf( "Result verified.\n\n" );
+ else
+ printf( "Result is incorrect.\n\n" );
+
+ Cudd_RecursiveDeref( ddF, bRes1 );
+ Cudd_RecursiveDeref( ddF, bRes2 );
+ // quit the new manager
+ Cudd_RecursiveDeref( ddG, bG2 );
+ Extra_StopManager( ddG );
+
+ // re-enable variable ordering in ddF
+ Cudd_AutodynEnable( ddF, CUDD_REORDER_SYMM_SIFT );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/hash/hashGen.h b/src/misc/hash/hashGen.h
index 257b9dba..e26a3c84 100644
--- a/src/misc/hash/hashGen.h
+++ b/src/misc/hash/hashGen.h
@@ -50,14 +50,17 @@ struct Hash_Gen_Entry_t_
struct Hash_Gen_Entry_t_ * pNext;
};
+typedef int (*Hash_GenHashFunction_t)(void* key, int nBins);
+typedef int (*Hash_GenCompFunction_t)(void* key, void* data);
+
struct Hash_Gen_t_
{
int nSize;
int nBins;
- int (* fHash)(void *key, int nBins);
- int (* fComp)(void *key, void *data);
+ Hash_GenHashFunction_t fHash;
+ Hash_GenCompFunction_t fComp;
int fFreeKey;
- Hash_Gen_Entry_t ** pArray;
+ Hash_Gen_Entry_t ** pArray;
};
@@ -229,7 +232,7 @@ static inline void Hash_GenWriteEntry( Hash_Gen_t *p, void * key, void * data )
p->nSize++;
(*pLast) = pEntry = ABC_ALLOC( Hash_Gen_Entry_t, 1 );
pEntry->pNext = NULL;
- pEntry->key = key;
+ pEntry->key = (char *)key;
pEntry->data = data;
return;
@@ -271,7 +274,7 @@ static inline Hash_Gen_Entry_t * Hash_GenEntry( Hash_Gen_t *p, void * key, int f
p->nSize++;
(*pLast) = pEntry = ABC_ALLOC( Hash_Gen_Entry_t, 1 );
pEntry->pNext = NULL;
- pEntry->key = key;
+ pEntry->key = (char *)key;
pEntry->data = NULL;
return pEntry;
}
diff --git a/src/misc/st/st.c b/src/misc/st/st.c
index 9705b987..cadddb0b 100644
--- a/src/misc/st/st.c
+++ b/src/misc/st/st.c
@@ -79,7 +79,7 @@ st_init_table(st_compare_func_type compare, st_hash_func_type hash)
void
st_free_table(st_table *table)
{
- register st_table_entry *ptr, *next;
+ st_table_entry *ptr, *next;
int i;
for(i = 0; i < table->num_bins ; i++) {
@@ -110,10 +110,10 @@ st_free_table(st_table *table)
}
int
-st_lookup(st_table *table, register const char *key, char **value)
+st_lookup(st_table *table, const char *key, char **value)
{
int hash_val;
- register st_table_entry *ptr, **last;
+ st_table_entry *ptr, **last;
hash_val = do_hash(key, table);
@@ -130,10 +130,10 @@ st_lookup(st_table *table, register const char *key, char **value)
}
int
-st_lookup_int(st_table *table, register char *key, int *value)
+st_lookup_int(st_table *table, char *key, int *value)
{
int hash_val;
- register st_table_entry *ptr, **last;
+ st_table_entry *ptr, **last;
hash_val = do_hash(key, table);
@@ -167,11 +167,11 @@ st_lookup_int(st_table *table, register char *key, int *value)
}
int
-st_insert(register st_table *table, register const char *key, char *value)
+st_insert(st_table *table, const char *key, char *value)
{
int hash_val;
st_table_entry *newEntry;
- register st_table_entry *ptr, **last;
+ st_table_entry *ptr, **last;
hash_val = do_hash(key, table);
@@ -188,7 +188,7 @@ st_insert(register st_table *table, register const char *key, char *value)
if (newEntry == NULL) {
return ST_OUT_OF_MEM;
}
- newEntry->key = key;
+ newEntry->key = (char *)key;
newEntry->record = value;
newEntry->next = table->bins[hash_val];
table->bins[hash_val] = newEntry;
@@ -280,9 +280,9 @@ st_find(st_table *table, char *key, char ***slot)
}
static int
-rehash(register st_table *table)
+rehash(st_table *table)
{
- register st_table_entry *ptr, *next, **old_bins;
+ st_table_entry *ptr, *next, **old_bins;
int i, old_num_bins, hash_val, old_num_entries;
/* save old values */
@@ -371,11 +371,11 @@ st_copy(st_table *old_table)
}
int
-st_delete(register st_table *table, register const char **keyp, char **value)
+st_delete(st_table *table, const char **keyp, char **value)
{
int hash_val;
const char *key = *keyp;
- register st_table_entry *ptr, **last;
+ st_table_entry *ptr, **last;
hash_val = do_hash(key, table);
@@ -394,11 +394,11 @@ st_delete(register st_table *table, register const char **keyp, char **value)
}
int
-st_delete_int(register st_table *table, register long *keyp, char **value)
+st_delete_int(st_table *table, long *keyp, char **value)
{
int hash_val;
char *key = (char *) *keyp;
- register st_table_entry *ptr, **last;
+ st_table_entry *ptr, **last;
hash_val = do_hash(key, table);
@@ -417,7 +417,7 @@ st_delete_int(register st_table *table, register long *keyp, char **value)
}
int
-st_foreach(st_table *table, enum st_retval (*func)(const char *, char *, char *), char *arg)
+st_foreach(st_table *table, enum st_retval (*func)(char *, char *, char *), char *arg)
{
st_table_entry *ptr, **last;
enum st_retval retval;
@@ -447,8 +447,8 @@ st_foreach(st_table *table, enum st_retval (*func)(const char *, char *, char *)
int
st_strhash(const char *string, int modulus)
{
- register int val = 0;
- register int c;
+ int val = 0;
+ int c;
while ((c = *string++) != '\0') {
val = val*997 + c;
@@ -500,7 +500,7 @@ st_init_gen(st_table *table)
int
st_gen(st_generator *gen, const char **key_p, char **value_p)
{
- register int i;
+ int i;
if (gen->entry == NULL) {
/* try to find next entry */
@@ -527,7 +527,7 @@ st_gen(st_generator *gen, const char **key_p, char **value_p)
int
st_gen_int(st_generator *gen, const char **key_p, long *value_p)
{
- register int i;
+ int i;
if (gen->entry == NULL) {
/* try to find next entry */
diff --git a/src/misc/st/st.h b/src/misc/st/st.h
index 81bd461e..d16fc4b6 100644
--- a/src/misc/st/st.h
+++ b/src/misc/st/st.h
@@ -14,17 +14,35 @@
#ifndef ST_INCLUDED
#define ST_INCLUDED
-
#include "abc_global.h"
ABC_NAMESPACE_HEADER_START
+
+/* These are potential duplicates. */
+#ifndef EXTERN
+# ifdef __cplusplus
+# ifdef ABC_NAMESPACE
+# define EXTERN extern
+# else
+# define EXTERN extern "C"
+# endif
+# else
+# define EXTERN extern
+# endif
+#endif
+
+#ifndef ARGS
+#define ARGS(protos) protos
+#endif
+
+
typedef int (*st_compare_func_type)(const char*, const char*);
typedef int (*st_hash_func_type)(const char*, int);
typedef struct st_table_entry st_table_entry;
struct st_table_entry {
- const char *key;
+ char *key;
char *record;
st_table_entry *next;
};
@@ -53,7 +71,7 @@ struct st_generator {
enum st_retval {ST_CONTINUE, ST_STOP, ST_DELETE};
-typedef enum st_retval (*ST_PFSR)(const char *, char *, char *);
+typedef enum st_retval (*ST_PFSR)(char *, char *, char *);
typedef int (*ST_PFI)();
extern st_table *st_init_table_with_params (st_compare_func_type compare, st_hash_func_type hash, int size, int density, double grow_factor, int reorder_flag);
diff --git a/src/misc/st/stmm.c b/src/misc/st/stmm.c
index 9aed8b11..1305d5b0 100644
--- a/src/misc/st/stmm.c
+++ b/src/misc/st/stmm.c
@@ -79,7 +79,7 @@ void
stmm_free_table (stmm_table *table)
{
/*
- register stmm_table_entry *ptr, *next;
+ stmm_table_entry *ptr, *next;
int i;
for ( i = 0; i < table->num_bins; i++ )
{
@@ -95,7 +95,7 @@ stmm_free_table (stmm_table *table)
// no need to deallocate entries because they are in the memory manager now
// added by alanmi
if ( table->pMemMan )
- Extra_MmFixedStop (table->pMemMan);
+ Extra_MmFixedStop ((Extra_MmFixed_t *)table->pMemMan);
ABC_FREE(table->bins);
ABC_FREE(table);
}
@@ -111,7 +111,7 @@ stmm_clean (stmm_table *table)
// reset the parameters
table->num_entries = 0;
// restart the memory manager
- Extra_MmFixedRestart (table->pMemMan);
+ Extra_MmFixedRestart ((Extra_MmFixed_t *)table->pMemMan);
}
@@ -131,10 +131,10 @@ stmm_clean (stmm_table *table)
}
int
-stmm_lookup (stmm_table *table, register char *key, char **value)
+stmm_lookup (stmm_table *table, char *key, char **value)
{
int hash_val;
- register stmm_table_entry *ptr, **last;
+ stmm_table_entry *ptr, **last;
hash_val = do_hash (key, table);
@@ -153,10 +153,10 @@ stmm_lookup (stmm_table *table, register char *key, char **value)
}
int
-stmm_lookup_int (stmm_table *table, register char *key, int *value)
+stmm_lookup_int (stmm_table *table, char *key, int *value)
{
int hash_val;
- register stmm_table_entry *ptr, **last;
+ stmm_table_entry *ptr, **last;
hash_val = do_hash (key, table);
@@ -187,7 +187,7 @@ stmm_lookup_int (stmm_table *table, register char *key, int *value)
hash_val = do_hash(key,table);\
}\
\
- new = (stmm_table_entry *)Extra_MmFixedEntryFetch( table->pMemMan );\
+ new = (stmm_table_entry *)Extra_MmFixedEntryFetch( (Extra_MmFixed_t *)table->pMemMan );\
\
new->key = key;\
new->record = value;\
@@ -197,11 +197,11 @@ stmm_lookup_int (stmm_table *table, register char *key, int *value)
}
int
-stmm_insert (register stmm_table *table, register char *key, char *value)
+stmm_insert (stmm_table *table, char *key, char *value)
{
int hash_val;
stmm_table_entry *newEntry;
- register stmm_table_entry *ptr, **last;
+ stmm_table_entry *ptr, **last;
hash_val = do_hash (key, table);
@@ -216,7 +216,7 @@ stmm_insert (register stmm_table *table, register char *key, char *value)
}
// newEntry = ABC_ALLOC( stmm_table_entry, 1 );
- newEntry = (stmm_table_entry *) Extra_MmFixedEntryFetch (table->pMemMan);
+ newEntry = (stmm_table_entry *) Extra_MmFixedEntryFetch ((Extra_MmFixed_t *)table->pMemMan);
if (newEntry == NULL) {
return STMM_OUT_OF_MEM;
}
@@ -249,7 +249,7 @@ stmm_add_direct (stmm_table *table, char *key, char *value)
hash_val = do_hash (key, table);
// newEntry = ABC_ALLOC( stmm_table_entry, 1 );
- newEntry = (stmm_table_entry *) Extra_MmFixedEntryFetch (table->pMemMan);
+ newEntry = (stmm_table_entry *) Extra_MmFixedEntryFetch ((Extra_MmFixed_t *)table->pMemMan);
if (newEntry == NULL) {
return STMM_OUT_OF_MEM;
}
@@ -281,7 +281,7 @@ stmm_find_or_add (stmm_table *table, char *key, char ***slot)
}
// newEntry = ABC_ALLOC( stmm_table_entry, 1 );
- newEntry = (stmm_table_entry *) Extra_MmFixedEntryFetch (table->pMemMan);
+ newEntry = (stmm_table_entry *) Extra_MmFixedEntryFetch ((Extra_MmFixed_t *)table->pMemMan);
if (newEntry == NULL) {
return STMM_OUT_OF_MEM;
}
@@ -325,9 +325,9 @@ stmm_find (stmm_table *table, char *key, char ***slot)
}
static int
-rehash (register stmm_table *table)
+rehash (stmm_table *table)
{
- register stmm_table_entry *ptr, *next, **old_bins;
+ stmm_table_entry *ptr, *next, **old_bins;
int i, old_num_bins, hash_val, old_num_entries;
/* save old values */
@@ -390,18 +390,14 @@ stmm_copy (stmm_table *old_table)
}
// allocate the memory manager for the newEntry table
- newEntry_table->pMemMan =
- Extra_MmFixedStart (sizeof (stmm_table_entry));
+ newEntry_table->pMemMan = Extra_MmFixedStart (sizeof (stmm_table_entry));
for (i = 0; i < num_bins; i++) {
newEntry_table->bins[i] = NULL;
ptr = old_table->bins[i];
while (ptr != NULL) {
// newEntry = ABC_ALLOC( stmm_table_entry, 1 );
- newEntry =
- (stmm_table_entry *) Extra_MmFixedEntryFetch (newEntry_table->
- pMemMan);
-
+ newEntry = (stmm_table_entry *)Extra_MmFixedEntryFetch ((Extra_MmFixed_t *)newEntry_table->pMemMan);
if (newEntry == NULL) {
/*
for ( j = 0; j <= i; j++ )
@@ -415,7 +411,7 @@ stmm_copy (stmm_table *old_table)
}
}
*/
- Extra_MmFixedStop (newEntry_table->pMemMan);
+ Extra_MmFixedStop ((Extra_MmFixed_t *)newEntry_table->pMemMan);
ABC_FREE(newEntry_table->bins);
ABC_FREE(newEntry_table);
@@ -431,11 +427,11 @@ stmm_copy (stmm_table *old_table)
}
int
-stmm_delete (register stmm_table *table, register char **keyp, char **value)
+stmm_delete (stmm_table *table, char **keyp, char **value)
{
int hash_val;
char *key = *keyp;
- register stmm_table_entry *ptr, **last;
+ stmm_table_entry *ptr, **last;
hash_val = do_hash (key, table);
@@ -450,18 +446,18 @@ stmm_delete (register stmm_table *table, register char **keyp, char **value)
*value = ptr->record;
*keyp = ptr->key;
// ABC_FREE( ptr );
- Extra_MmFixedEntryRecycle (table->pMemMan, (char *) ptr);
+ Extra_MmFixedEntryRecycle ((Extra_MmFixed_t *)table->pMemMan, (char *) ptr);
table->num_entries--;
return 1;
}
int
-stmm_delete_int (register stmm_table *table, register long *keyp, char **value)
+stmm_delete_int (stmm_table *table, long *keyp, char **value)
{
int hash_val;
char *key = (char *) *keyp;
- register stmm_table_entry *ptr, **last;
+ stmm_table_entry *ptr, **last;
hash_val = do_hash (key, table);
@@ -476,7 +472,7 @@ stmm_delete_int (register stmm_table *table, register long *keyp, char **value)
*value = ptr->record;
*keyp = (long) ptr->key;
// ABC_FREE( ptr );
- Extra_MmFixedEntryRecycle (table->pMemMan, (char *) ptr);
+ Extra_MmFixedEntryRecycle ((Extra_MmFixed_t *)table->pMemMan, (char *) ptr);
table->num_entries--;
return 1;
@@ -505,7 +501,7 @@ stmm_foreach (stmm_table *table, enum stmm_retval (*func) (char *, char *, char
*last = ptr->next;
table->num_entries--; /* cstevens@ic */
// ABC_FREE( ptr );
- Extra_MmFixedEntryRecycle (table->pMemMan, (char *) ptr);
+ Extra_MmFixedEntryRecycle ((Extra_MmFixed_t *)table->pMemMan, (char *) ptr);
ptr = *last;
}
@@ -515,10 +511,10 @@ stmm_foreach (stmm_table *table, enum stmm_retval (*func) (char *, char *, char
}
int
-stmm_strhash (register const char *string, int modulus)
+stmm_strhash (const char *string, int modulus)
{
- register int val = 0;
- register int c;
+ int val = 0;
+ int c;
while ((c = *string++) != '\0') {
val = val * 997 + c;
@@ -570,7 +566,7 @@ stmm_init_gen (stmm_table *table)
int
stmm_gen (stmm_generator *gen, char **key_p, char **value_p)
{
- register int i;
+ int i;
if (gen->entry == NULL) {
/* try to find next entry */
@@ -597,7 +593,7 @@ stmm_gen (stmm_generator *gen, char **key_p, char **value_p)
int
stmm_gen_int (stmm_generator *gen, char **key_p, long *value_p)
{
- register int i;
+ int i;
if (gen->entry == NULL) {
/* try to find next entry */
diff --git a/src/misc/st/stmm.h b/src/misc/st/stmm.h
index c23c6942..eee90073 100644
--- a/src/misc/st/stmm.h
+++ b/src/misc/st/stmm.h
@@ -14,12 +14,27 @@
#ifndef STMM_INCLUDED
#define STMM_INCLUDED
+#include "abc_global.h"
-#include "extra.h"
+ABC_NAMESPACE_HEADER_START
+/* These are potential duplicates. */
+#ifndef EXTERN
+# ifdef __cplusplus
+# ifdef ABC_NAMESPACE
+# define EXTERN extern
+# else
+# define EXTERN extern "C"
+# endif
+# else
+# define EXTERN extern
+# endif
+#endif
-ABC_NAMESPACE_HEADER_START
+#ifndef ARGS
+#define ARGS(protos) protos
+#endif
typedef int (*stmm_compare_func_type)(const char*, const char*);
typedef int (*stmm_hash_func_type)(const char*, int);
@@ -47,7 +62,7 @@ struct stmm_table
stmm_table_entry **bins;
// memory manager to improve runtime and prevent memory fragmentation
// added by alanmi - January 16, 2003
- Extra_MmFixed_t *pMemMan;
+ void * pMemMan;
};
struct stmm_generator
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index aca9a509..1321f028 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -288,18 +288,6 @@ static inline void Abc_PrintMemoryP( int level, const char * pStr, int time, int
}
-// sequential counter-example
-typedef struct Abc_Cex_t_ Abc_Cex_t;
-struct Abc_Cex_t_
-{
- int iPo; // the zero-based number of PO, for which verification failed
- int iFrame; // the zero-based number of the time-frame, for which verificaiton failed
- int nRegs; // the number of registers in the miter
- int nPis; // the number of primary inputs in the miter
- int nBits; // the number of words of bit data used
- unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
-};
-
ABC_NAMESPACE_HEADER_END
#endif
diff --git a/src/misc/util/module.make b/src/misc/util/module.make
index c70d582a..776a1705 100644
--- a/src/misc/util/module.make
+++ b/src/misc/util/module.make
@@ -1 +1,3 @@
-SRC += src/misc/util/utilFile.c src/misc/util/utilSignal.c
+SRC += src/misc/util/utilCex.c \
+ src/misc/util/utilFile.c \
+ src/misc/util/utilSignal.c
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
new file mode 100644
index 00000000..a4cf5e33
--- /dev/null
+++ b/src/misc/util/utilCex.c
@@ -0,0 +1,205 @@
+/**CFile****************************************************************
+
+ FileName [utilCex.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Handling counter-examples.]
+
+ Synopsis [Handling counter-examples.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - Feburary 13, 2011.]
+
+ Revision [$Id: utilCex.c,v 1.00 2011/02/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <string.h>
+#include <stdlib.h>
+#include <assert.h>
+
+#include "abc_global.h"
+#include "utilCex.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Abc_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
+static inline int Abc_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
+static inline void Abc_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+ Synopsis [Allocates a counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Cex_t * Abc_CexAlloc( int nRegs, int nRealPis, int nFrames )
+{
+ Abc_Cex_t * pCex;
+ int nWords = Abc_BitWordNum( nRegs + nRealPis * nFrames );
+ pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
+ memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
+ pCex->nRegs = nRegs;
+ pCex->nPis = nRealPis;
+ pCex->nBits = nRegs + nRealPis * nFrames;
+ return pCex;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Make the trivial counter-example for the trivially asserted output.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Cex_t * Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int iFrameOut )
+{
+ Abc_Cex_t * pCex;
+ int iPo, iFrame;
+ assert( nRegs > 0 );
+ iPo = iFrameOut % nTruePos;
+ iFrame = iFrameOut / nTruePos;
+ // allocate the counter example
+ pCex = Abc_CexAlloc( nRegs, nTruePis, iFrame + 1 );
+ pCex->iPo = iPo;
+ pCex->iFrame = iFrame;
+ return pCex;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Cex_t * Abc_CexCreate( int nRegs, int nPis, int * pArray, int iFrame, int iPo, int fSkipRegs )
+{
+ Abc_Cex_t * pCex;
+ int i;
+ pCex = Abc_CexAlloc( nRegs, nPis, iFrame+1 );
+ pCex->iPo = iPo;
+ pCex->iFrame = iFrame;
+ if ( pArray == NULL )
+ return pCex;
+ if ( fSkipRegs )
+ {
+ for ( i = nRegs; i < pCex->nBits; i++ )
+ if ( pArray[i-nRegs] )
+ Abc_InfoSetBit( pCex->pData, i );
+ }
+ else
+ {
+ for ( i = 0; i < pCex->nBits; i++ )
+ if ( pArray[i] )
+ Abc_InfoSetBit( pCex->pData, i );
+ }
+ return pCex;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Make the trivial counter-example for the trivially asserted output.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew )
+{
+ Abc_Cex_t * pCex;
+ int i;
+ if ( nRegsNew == -1 )
+ nRegsNew = p->nRegs;
+ pCex = Abc_CexAlloc( nRegsNew, p->nPis, p->iFrame+1 );
+ pCex->iPo = p->iPo;
+ pCex->iFrame = p->iFrame;
+ for ( i = p->nRegs; i < p->nBits; i++ )
+ if ( Abc_InfoHasBit(p->pData, i) )
+ Abc_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs );
+ return pCex;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints out the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_CexPrint( Abc_Cex_t * p )
+{
+ int i, f, k;
+ printf( "Counter-example: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d\n",
+ p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits );
+ printf( "State : " );
+ for ( k = 0; k < p->nRegs; k++ )
+ printf( "%d", Abc_InfoHasBit(p->pData, k) );
+ printf( "\n" );
+ for ( f = 0; f <= p->iFrame; f++ )
+ {
+ printf( "Frame %2d : ", f );
+ for ( i = 0; i < p->nPis; i++ )
+ printf( "%d", Abc_InfoHasBit(p->pData, k++) );
+ printf( "\n" );
+ }
+ assert( k == p->nBits );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Frees the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_CexFree( Abc_Cex_t * p )
+{
+ ABC_FREE( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h
new file mode 100644
index 00000000..f0ee57b1
--- /dev/null
+++ b/src/misc/util/utilCex.h
@@ -0,0 +1,72 @@
+/**CFile****************************************************************
+
+ FileName [utilCex.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Handling sequential counter-examples.]
+
+ Synopsis [Handling sequential counter-examples.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - Feburary 13, 2011.]
+
+ Revision [$Id: utilCex.h,v 1.00 2011/02/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __UTIL_CEX_H__
+#define __UTIL_CEX_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+// sequential counter-example
+typedef struct Abc_Cex_t_ Abc_Cex_t;
+struct Abc_Cex_t_
+{
+ int iPo; // the zero-based number of PO, for which verification failed
+ int iFrame; // the zero-based number of the time-frame, for which verificaiton failed
+ int nRegs; // the number of registers in the miter
+ int nPis; // the number of primary inputs in the miter
+ int nBits; // the number of words of bit data used
+ unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== utilCex.c ===========================================================*/
+extern Abc_Cex_t * Abc_CexAlloc( int nRegs, int nTruePis, int nFrames );
+extern Abc_Cex_t * Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int iFrameOut );
+extern Abc_Cex_t * Abc_CexCreate( int nRegs, int nTruePis, int * pArray, int iFrame, int iPo, int fSkipRegs );
+extern Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew );
+extern void Abc_CexPrint( Abc_Cex_t * p );
+extern void Abc_CexFree( Abc_Cex_t * p );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/util/utilFile.c b/src/misc/util/utilFile.c
index 2c40c32c..69d84c29 100644
--- a/src/misc/util/utilFile.c
+++ b/src/misc/util/utilFile.c
@@ -25,6 +25,14 @@
#include <fcntl.h>
#include <sys/stat.h>
+#if defined(_MSC_VER)
+#include <Windows.h>
+#include <process.h>
+#include <io.h>
+#else
+#include <unistd.h>
+#endif
+
#include "abc_global.h"
ABC_NAMESPACE_IMPL_START
@@ -33,12 +41,6 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-#if defined(_MSC_VER)
-
-#include <Windows.h>
-#include <process.h>
-#include <io.h>
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -56,6 +58,7 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
static ABC_UINT64_T realTimeAbs() // -- absolute time in nano-seconds
{
+#if defined(_MSC_VER)
LARGE_INTEGER f, t;
double realTime_freq;
int ok;
@@ -65,20 +68,16 @@ static ABC_UINT64_T realTimeAbs() // -- absolute time in nano-seconds
ok = QueryPerformanceCounter(&t); assert(ok);
return (ABC_UINT64_T)(__int64)(((__int64)(((ABC_UINT64_T)t.LowPart | ((ABC_UINT64_T)t.HighPart << 32))) * realTime_freq * 1000000000));
-}
-
#endif
-
-
-
-// Opens a temporary file with given prefix and returns file descriptor (-1 on failure)
-// and a string containing the name of the file (to be freed by caller).
+}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Opens a temporary file.]
- Description []
+ Description [Opens a temporary file with given prefix and returns file
+ descriptor (-1 on failure) and a string containing the name of the file
+ (to be freed by caller).]
SideEffects []
@@ -87,9 +86,22 @@ static ABC_UINT64_T realTimeAbs() // -- absolute time in nano-seconds
***********************************************************************/
int tmpFile(const char* prefix, const char* suffix, char** out_name)
{
-#if !defined(_MSC_VER)
+#if defined(_MSC_VER)
+ int i, fd;
+ *out_name = (char*)malloc(strlen(prefix) + strlen(suffix) + 27);
+ for (i = 0; i < 10; i++){
+ sprintf(*out_name, "%s%I64X%d%s", prefix, realTimeAbs(), _getpid(), suffix);
+ fd = _open(*out_name, O_CREAT | O_EXCL | O_BINARY | O_RDWR, _S_IREAD | _S_IWRITE);
+ if (fd == -1){
+ free(*out_name);
+ *out_name = NULL;
+ }
+ return fd;
+ }
+ assert(0); // -- could not open temporary file
+ return 0;
+#else
int fd;
-
*out_name = (char*)malloc(strlen(prefix) + strlen(suffix) + 7);
assert(*out_name != NULL);
sprintf(*out_name, "%sXXXXXX", prefix);
@@ -98,7 +110,6 @@ int tmpFile(const char* prefix, const char* suffix, char** out_name)
free(*out_name);
*out_name = NULL;
}else{
-
// Kludge:
close(fd);
unlink(*out_name);
@@ -108,35 +119,11 @@ int tmpFile(const char* prefix, const char* suffix, char** out_name)
free(*out_name);
*out_name = NULL;
}
-
-// assert( 0 );
- // commented out because had problem with g++ saying that
- // close() and unlink() are not defined in the namespace
-
}
return fd;
-
-#else
- int i, fd;
- *out_name = (char*)malloc(strlen(prefix) + strlen(suffix) + 27);
- for (i = 0; i < 10; i++){
- sprintf(*out_name, "%s%I64X%d%s", prefix, realTimeAbs(), _getpid(), suffix);
- fd = _open(*out_name, O_CREAT | O_EXCL | O_BINARY | O_RDWR, _S_IREAD | _S_IWRITE);
- if (fd == -1){
- free(*out_name);
- *out_name = NULL;
- }
- return fd;
- }
- assert(0); // -- could not open temporary file
- return 0;
#endif
}
-
-//mmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmmm
-
-
/**Function*************************************************************
Synopsis []
@@ -165,8 +152,6 @@ int main(int argc, char** argv)
}
*/
-
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/util/utilSignal.c b/src/misc/util/utilSignal.c
index 6a793ce0..2886f69b 100644
--- a/src/misc/util/utilSignal.c
+++ b/src/misc/util/utilSignal.c
@@ -8,28 +8,26 @@
Synopsis []
- Author []
+ Author [Baruch Sterin]
Affiliation [UC Berkeley]
- Date []
+ Date [Ver. 1.0. Started - February 1, 2011.]
- Revision []
+ Revision [$Id: utilSignal.c,v 1.00 2011/02/01 00:00:00 alanmi Exp $]
***********************************************************************/
-#include <main.h>
+#include <stdio.h>
#include <stdlib.h>
-#include <signal.h>
#include "abc_global.h"
-#include "hashGen.h"
-
-#ifndef _MSC_VER
+#include "utilSignal.h"
+#ifdef _MSC_VER
+#define unlink _unlink
+#else
#include <unistd.h>
-#include <errno.h>
-#include <sys/types.h>
-#include <sys/wait.h>
+#endif
ABC_NAMESPACE_IMPL_START
@@ -37,485 +35,36 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static Hash_Gen_t* watched_pid_hash = NULL;
-static Hash_Gen_t* watched_tmp_files_hash = NULL;
-
-static sigset_t* old_procmask;
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-/**Function*************************************************************
-
- Synopsis []
-
- Description [Kills all watched child processes and remove all watched termporary files.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-void Util_SignalCleanup()
-{
- int i;
- Hash_Gen_Entry_t* pEntry;
-
- // kill all watched child processes
- Hash_GenForEachEntry(watched_pid_hash, pEntry, i)
- {
- pid_t pid = (pid_t)pEntry->key;
- pid_t ppid = (pid_t)pEntry->data;
-
- if (getpid() == ppid)
- {
- kill(pid, SIGINT);
- }
- }
-
- // remove watched temporary files
- Hash_GenForEachEntry(watched_tmp_files_hash, pEntry, i)
- {
- int fname = (const char*)pEntry->key;
- pid_t ppid = (pid_t)pEntry->data;
-
- if( getpid() == ppid )
- {
- remove(fname);
- }
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description [Sets up data structures needed for cleanup in signal handler.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-void Util_SignalStartHandler()
-{
- watched_pid_hash = Hash_GenAlloc(100, Hash_DefaultHashFuncInt, Hash_DefaultCmpFuncInt, 0);
- watched_tmp_files_hash = Hash_GenAlloc(100, Hash_DefaultHashFuncStr, strcmp, 1);
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description [Frees data structures used for clean up in signal handler.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-void Util_SignalResetHandler()
-{
- int i;
- Hash_Gen_Entry_t* pEntry;
-
- sigset_t procmask, old_procmask;
-
- sigemptyset(&procmask);
- sigaddset(&procmask, SIGINT);
-
- sigprocmask(SIG_BLOCK, &procmask, &old_procmask);
-
- Hash_GenFree(watched_pid_hash);
- watched_pid_hash = Hash_GenAlloc(100, Hash_DefaultHashFuncInt, Hash_DefaultCmpFuncInt, 0);
-
- Hash_GenFree(watched_tmp_files_hash);
- watched_tmp_files_hash = Hash_GenAlloc(100, Hash_DefaultHashFuncStr, strcmp, 1);
-
- sigprocmask(SIG_SETMASK, &old_procmask, NULL);
-}
-
-void Util_SignalStopHandler()
-{
- int i;
- Hash_Gen_Entry_t* pEntry;
-
- Hash_GenFree(watched_pid_hash);
- watched_pid_hash = NULL;
-
- Hash_GenFree(watched_tmp_files_hash);
- watched_tmp_files_hash = NULL;
-}
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description [Blocks SIGINT. For use when updating watched processes and temporary files to prevent race conditions with the signal handler.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-static int nblocks = 0;
-
-void Util_SignalBlockSignals()
-{
- sigset_t procmask;
-
- assert(nblocks==0);
- nblocks ++ ;
-
- sigemptyset(&procmask);
- sigaddset(&procmask, SIGINT);
-
- sigprocmask(SIG_BLOCK, &procmask, &old_procmask);
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description [Unblocks SIGINT after a call to Util_SignalBlockSignals.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-void Util_SignalUnblockSignals()
-{
- assert( nblocks==1);
- nblocks--;
-
- sigprocmask(SIG_SETMASK, &old_procmask, NULL);
-}
-
-
-static void watch_tmp_file(const char* fname)
-{
- if( watched_tmp_files_hash != NULL )
- {
- Hash_GenWriteEntry(watched_tmp_files_hash, Extra_UtilStrsav(fname), (void*)getpid() );
- }
-}
-
-static void unwatch_tmp_file(const char* fname)
-{
- if ( watched_tmp_files_hash )
- {
- assert( Hash_GenExists(watched_tmp_files_hash, fname) );
- Hash_GenRemove(watched_tmp_files_hash, fname);
- assert( !Hash_GenExists(watched_tmp_files_hash, fname) );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description [Adds a process id to the list of processes that should be killed in a signal handler.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-void Util_SignalAddChildPid(int pid)
-{
- if ( watched_pid_hash )
- {
- Hash_GenWriteEntry(watched_pid_hash, (void*)pid, (void*)getpid());
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description [Removes a process id from the list of processes that should be killed in a signal handler.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-void Util_SignalRemoveChildPid(int pid)
-{
- if ( watched_pid_hash )
- {
- Hash_GenRemove(watched_pid_hash, (void*)pid);
- }
-}
-
-// a dummy signal hanlder to make sure that SIGCHLD and SIGINT will cause sigsuspend() to return
-static int null_sig_handler(int signum)
-{
- return 0;
-}
-
-
-// enusre that sigsuspend() returns when signal signum occurs -- sigsuspend() does not return if a signal is ignored
-static void replace_sighandler(int signum, struct sigaction* old_sa, int replace_dfl)
-{
- sigaction(signum, NULL, old_sa);
-
- if( old_sa->sa_handler == SIG_IGN || old_sa->sa_handler==SIG_DFL && replace_dfl)
- {
- struct sigaction sa;
- memset(&sa, 0, sizeof(sa));
-
- sa.sa_handler = null_sig_handler;
-
- sigaction(signum, &sa, &old_sa);
- }
-}
-
-//
-static int do_waitpid(pid_t pid, sigset_t* old_procmask)
-{
- int status;
-
- struct sigaction sigint_sa;
- struct sigaction sigchld_sa;
- sigset_t waitmask;
-
- // ensure SIGINT and SIGCHLD are not blocked during sigsuspend()
- memcpy(&waitmask, old_procmask, sizeof(sigset_t));
-
- sigdelset(&waitmask, SIGINT);
- sigdelset(&waitmask, SIGCHLD);
-
- // ensure sigsuspend() returns if SIGINT or SIGCHLD occur, and save the current settings for SIGCHLD and SIGINT
-
- replace_sighandler(SIGINT, &sigint_sa, 0);
- replace_sighandler(SIGCHLD, &sigchld_sa, 1);
-
- for(;;)
- {
- int rc;
-
- // wait for a signal -- returns if SIGINT or SIGCHLD (or any other signal that is unblocked and not ignored) occur
- sigsuspend(&waitmask);
-
- // check if pid has terminated
- rc = waitpid(pid, &status, WNOHANG);
-
- // stop if terminated or some other error occurs
- if( rc > 0 || rc == -1 && errno!=EINTR )
- {
- break;
- }
- }
-
- // process is dead, should no longer be watched
- Util_SignalRemoveChildPid(pid);
-
- // restore original behavior of SIGINT and SIGCHLD
- sigaction(SIGINT, &sigint_sa, NULL);
- sigaction(SIGCHLD, &sigchld_sa, NULL);
-
- return status;
-}
-
-static int do_system(const char* cmd, sigset_t* old_procmask)
-{
- int pid;
-
- pid = fork();
-
- if (pid == -1)
- {
- // fork failed
- return -1;
- }
- else if( pid == 0)
- {
- // child process
- sigprocmask(SIG_SETMASK, old_procmask, NULL);
- execl("/bin/sh", "sh", "-c", cmd, NULL);
- _exit(127);
- }
-
- Util_SignalAddChildPid(pid);
-
- return do_waitpid(pid, old_procmask);
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description [Replaces system() with a function that allows SIGINT to interrupt.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-int Util_SignalSystem(const char* cmd)
-{
- int status;
-
- sigset_t procmask;
- sigset_t old_procmask;
-
- // if signal handler is not installed, run the original system()
- if ( ! watched_pid_hash && ! watched_tmp_files_hash )
- return system(cmd);
-
- // block SIGINT and SIGCHLD
- sigemptyset(&procmask);
-
- sigaddset(&procmask, SIGINT);
- sigaddset(&procmask, SIGCHLD);
-
- sigprocmask(SIG_BLOCK, &procmask, &old_procmask);
-
- // call the actual function
- status = do_system(cmd, &old_procmask);
-
- // restore signal block mask
- sigprocmask(SIG_SETMASK, &old_procmask, NULL);
- return status;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-#else /* #ifndef _MSC_VER */
-
-#include "abc_global.h"
-
-ABC_NAMESPACE_IMPL_START
-
-void Util_SignalCleanup()
-{
-}
-
-void Util_SignalStartHandler()
-{
-}
-
-void Util_SignalResetHandler()
-{
-}
-
-void Util_SignalStopHandler()
-{
-}
-
-void Util_SignalBlockSignals()
-{
-}
-
-void Util_SignalUnblockSignals()
-{
-}
-
-void watch_tmp_file(const char* fname)
-{
-}
-
-void unwatch_tmp_file(const char* fname)
-{
-}
-
-void Util_SignalAddChildPid(int pid)
-{
-}
-
-void Util_SignalRemoveChildPid(int pid)
-{
-}
+#ifndef ABC_PYTHON_EMBED
int Util_SignalSystem(const char* cmd)
{
return system(cmd);
}
-#endif /* #ifdef _MSC_VER */
-
int tmpFile(const char* prefix, const char* suffix, char** out_name);
-/**Function*************************************************************
-
- Synopsis []
-
- Description [Create a temporary file and add it to the list of files to be cleaned up in the signal handler.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name)
{
- int fd;
-
- Util_SignalBlockSignals();
-
- fd = tmpFile(prefix, suffix, out_name);
-
- if ( fd != -1 )
- {
- watch_tmp_file( *out_name );
- }
-
- Util_SignalUnblockSignals();
-
- return fd;
+ return tmpFile(prefix, suffix, out_name);
}
-/**Function*************************************************************
-
- Synopsis []
-
- Description [Remove a temporary file (and remove it from the watched files list.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
void Util_SignalTmpFileRemove(const char* fname, int fLeave)
{
- Util_SignalBlockSignals();
-
- unwatch_tmp_file(fname);
-
if (! fLeave)
{
- remove(fname);
+ unlink(fname);
}
-
- Util_SignalUnblockSignals();
}
+#endif /* ABC_PYTHON_EMBED */
+
ABC_NAMESPACE_IMPL_END
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/util/utilSignal.h b/src/misc/util/utilSignal.h
index d9802aa0..0ac87290 100644
--- a/src/misc/util/utilSignal.h
+++ b/src/misc/util/utilSignal.h
@@ -4,17 +4,17 @@
SystemName [ABC: Logic synthesis and verification system.]
- PackageName []
+ PackageName [Signal handling utilities.]
- Synopsis []
+ Synopsis [Signal handling utilities.]
- Author []
+ Author [Baruch Sterin]
Affiliation [UC Berkeley]
- Date []
+ Date [Ver. 1.0. Started - February 1, 2011.]
- Revision []
+ Revision [$Id: utilSignal.h,v 1.00 2011/02/01 00:00:00 alanmi Exp $]
***********************************************************************/
@@ -45,22 +45,9 @@ ABC_NAMESPACE_HEADER_START
/*=== utilSignal.c ==========================================================*/
-void Util_SignalCleanup();
-
-void Util_SignalStartHandler();
-void Util_SignalResetHandler();
-void Util_SignalStopHandler();
-
-void Util_SignalBlockSignals();
-void Util_SignalUnblockSignals();
-
-void Util_SignalAddChildPid(int pid);
-void Util_SignalRemoveChildPid(int pid);
-
-int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name);
-void Util_SignalTmpFileRemove(const char* fname, int fLeave);
-
-int Util_SignalSystem(const char* cmd);
+extern int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name);
+extern void Util_SignalTmpFileRemove(const char* fname, int fLeave);
+extern int Util_SignalSystem(const char* cmd);
ABC_NAMESPACE_HEADER_END
diff --git a/src/misc/util/util_hack.h b/src/misc/util/util_hack.h
index f7ad89f9..1a734f03 100644
--- a/src/misc/util/util_hack.h
+++ b/src/misc/util/util_hack.h
@@ -21,7 +21,6 @@
#ifndef __UTIL_HACK_H__
#define __UTIL_HACK_H__
-
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
@@ -31,50 +30,18 @@
#include "abc_global.h"
-
ABC_NAMESPACE_HEADER_START
+#define NIL(type) ((type *) 0)
-#ifndef EXTERN
-#define EXTERN extern
-#endif
-#define NIL(type) ((type *) 0)
-#define random rand
-#define srandom srand
-
-#define util_cpu_time Extra_CpuTime
-#define getSoftDataLimit Extra_GetSoftDataLimit
-#define util_getopt_reset Extra_UtilGetoptReset
-#define util_getopt Extra_UtilGetopt
-#define util_print_time Extra_UtilPrintTime
-#define util_strsav Extra_UtilStrsav
-#define util_tilde_expand Extra_UtilTildeExpand
-#define util_file_search Extra_UtilFileSearch
-#define MMoutOfMemory Extra_UtilMMoutOfMemory
-
-#define util_optarg globalUtilOptarg
-#define util_optind globalUtilOptind
-
-#ifndef ARGS
-#define ARGS(protos) protos
-#endif
-
-extern long Extra_CpuTime();
-extern int Extra_GetSoftDataLimit();
-extern void Extra_UtilGetoptReset();
-extern int Extra_UtilGetopt( int argc, char *argv[], const char *optstring );
-extern char * Extra_UtilPrintTime( long t );
-extern char * Extra_UtilStrsav( char *s );
-extern char * Extra_UtilTildeExpand( char *fname );
-extern char * Extra_UtilFileSearch( char *file, char *path, char *mode );
-
-extern char * globalUtilOptarg;
-extern int globalUtilOptind;
-
+#define util_cpu_time Extra_CpuTime
+#define getSoftDataLimit Extra_GetSoftDataLimit
+#define MMoutOfMemory Extra_UtilMMoutOfMemory
+extern long Extra_CpuTime();
+extern int Extra_GetSoftDataLimit();
+extern void (*Extra_UtilMMoutOfMemory)( long size );
ABC_NAMESPACE_HEADER_END
-
-
#endif
generated by cgit v1.2.3 (git 2.25.1) at 2025-08-21 03:12:51 +0000