luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Command %ufar.

This commit is contained in:
Alan Mishchenko 2025-12-24 19:06:29 -08:00
parent 84fca2c3f0
commit 5cdded372a
19 changed files with 4450 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -36,7 +36,7 @@ MODULES := \
src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \
src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \
src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt src/opt/rar \
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd src/opt/eslim \
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd src/opt/eslim src/opt/ufar src/opt/untk src/opt/util \
src/sat/bsat src/sat/xsat src/sat/satoko src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc src/sat/glucose src/sat/glucose2 src/sat/kissat src/sat/cadical \
src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
src/bool/rsb src/bool/rpo \

2
src/base/main/mainInit.c
View File

@ -69,6 +69,7 @@ extern void Glucose_Init( Abc_Frame_t *pAbc );
extern void Glucose_End( Abc_Frame_t * pAbc );
extern void Glucose2_Init( Abc_Frame_t *pAbc );
extern void Glucose2_End( Abc_Frame_t * pAbc );
extern void Ufar_Init(Abc_Frame_t *pAbc);
static Abc_FrameInitializer_t* s_InitializerStart = NULL;
static Abc_FrameInitializer_t* s_InitializerEnd = NULL;
@ -123,6 +124,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
Cba_Init( pAbc );
Pla_Init( pAbc );
Test_Init( pAbc );
Ufar_Init( pAbc );
Glucose_Init( pAbc );
Glucose2_Init( pAbc );
for( p = s_InitializerStart ; p ; p = p->next )

336
src/opt/ufar/UfarCmd.cpp Executable file
View File

@ -0,0 +1,336 @@
/*
* UifCmd.cpp
*
* Created on: Aug 25, 2015
* Author: Yen-Sheng Ho
*/
#include "base/wlc/wlc.h"
#include "opt/ufar/UfarCmd.h"
#include "opt/ufar/UfarMgr.h"
#include "opt/untk/NtkNtk.h"
#include "opt/util/util.h"
#include <iostream>
#include <iomanip>
#include <climits>
#include <regex>
using namespace std;
static UFAR::UfarManager ufar_manager;
static int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAnalyzeCex( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCreateAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCreateMiter( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv );
static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Wlc_Ntk_t *)pAbc->pAbcWlc; }
static inline void Wlc_AbcFreeNtk( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc)); }
static inline void Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ) { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk; }
void Ufar_Init(Abc_Frame_t *pAbc)
{
//Cmd_CommandAdd( pAbc, "Word level Prove", "%%test", Abc_CommandTest, 0 );
//Cmd_CommandAdd( pAbc, "Word level Prove", "%%cex", Abc_CommandAnalyzeCex, 0 );
//Cmd_CommandAdd( pAbc, "Word level Prove", "%%abs", Abc_CommandCreateAbstraction, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%ufar", Abc_CommandProveUsingUif, 0 );
//Cmd_CommandAdd( pAbc, "Word level Prove", "%%miter", Abc_CommandCreateMiter, 0 );
}
static int Abc_CommandCreateMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Wlc_Ntk_t * pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0);
Wlc_AbcUpdateNtk(pAbc, pNew);
return 0;
}
static int Abc_CommandCreateAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Wlc_Ntk_t * pNew = ufar_manager.BuildCurrentAbstraction();
Wlc_AbcUpdateNtk(pAbc, pNew);
return 0;
}
static int Abc_CommandAnalyzeCex( Abc_Frame_t * pAbc, int argc, char ** argv )
{
if ( pAbc->pCex == NULL )
{
cout << "There is no CEX.\n";
return 0;
}
// ufar_manager.GetOperatorsInCex(pAbc->pCex);
ufar_manager.FindUifPairsUsingCex(pAbc->pCex);
return 0;
}
static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv )
{
if (Wlc_AbcGetNtk(pAbc) == NULL) {
cout << "There is no current design.\n";
return 0;
}
OptMgr opt_mgr(argv[0]);
opt_mgr.AddOpt("--norm", ufar_manager.params.fNorm ? "yes" : "no", "", "toggle using data type normalization");
opt_mgr.AddOpt("--adder", "no", "", "toggle including adders");
opt_mgr.AddOpt("--cexmin", ufar_manager.params.fCexMin ? "yes" : "no", "", "toggle using CEX minimization");
opt_mgr.AddOpt("--sim", "none", "str", "use simulation and specify its setting");
opt_mgr.AddOpt("-v", to_string(ufar_manager.params.iVerbosity), "num", "specify verbosity level");
opt_mgr.AddOpt("--seq", to_string(ufar_manager.params.nSeqLookBack), "num", "specify the number of look-back frames (0 = no sequential UIF)");
opt_mgr.AddOpt("--profile", "no", "", "dump time distribution");
opt_mgr.AddOpt("--pba_uif", ufar_manager.params.fPbaUif ? "yes" : "no", "", "toggle using proof-based refinement for UIF pairs");
opt_mgr.AddOpt("--lazysim", ufar_manager.params.fLazySim ? "yes" : "no", "", "toggle applying UIF pairs based on simulation");
opt_mgr.AddOpt("--pbasim", ufar_manager.params.fPbaSim ? "yes" : "no", "", "toggle combining pba and sim");
opt_mgr.AddOpt("--pbacex", ufar_manager.params.fPbaCex ? "yes" : "no", "", "toggle combining pba and cex");
opt_mgr.AddOpt("--satmin", ufar_manager.params.fSatMin ? "yes" : "no", "", "toggle using sat-min in pba");
opt_mgr.AddOpt("--cbawb", ufar_manager.params.fCbaWb ? "yes" : "no", "", "toggle using cex-based refinement for white boxing");
opt_mgr.AddOpt("--grey", ufar_manager.params.fGrey ? "yes" : "no", "", "toggle using grey-box constraints");
opt_mgr.AddOpt("--grey2", to_string(ufar_manager.params.nGrey), "float", "specify the greyness threshold");
opt_mgr.AddOpt("--dump", "none", "str", "specify file name");
opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name");
opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers");
opt_mgr.AddOpt("--dump_states", "none", "str", "specify the name for the states file");
opt_mgr.AddOpt("--read_states", "none", "str", "specify the name for the states file");
opt_mgr.AddOpt("--sp", ufar_manager.params.fSuper_prove ? "yes" : "no", "", "toggle using super_prove");
opt_mgr.AddOpt("--simp", ufar_manager.params.fSimple ? "yes" : "no", "", "toggle using simple (prove)");
opt_mgr.AddOpt("--syn", ufar_manager.params.fSyn ? "yes" : "no", "", "toggle using simple synthesis");
opt_mgr.AddOpt("--pth", ufar_manager.params.fPthread ? "yes" : "no", "", "toggle using pthreads");
opt_mgr.AddOpt("--onewb", to_string(ufar_manager.params.iOneWb), "int", "specify the mode for one-white-boxing");
opt_mgr.AddOpt("--timeout", to_string(ufar_manager.params.nTimeout), "num", "specify the timeout (sec)");
opt_mgr.AddOpt("--exp", to_string(ufar_manager.params.iExp), "int", "specify the exp mode");
opt_mgr.AddOpt("--miter", "yes", "", "toggle mitering the problem");
opt_mgr.AddOpt("--under", "-1", "num", "try under-approximation with the given size");
if(!opt_mgr.Parse(argc, argv)) {
opt_mgr.PrintUsage();
cout << "\n This command was developed by Yen-Sheng Ho at UC Berkeley in 2015.\n";
cout << " https://people.eecs.berkeley.edu/~alanmi/publications/2016/fmcad16_uif.pdf \n";
return 0;
}
if(opt_mgr["--norm"])
ufar_manager.params.fNorm ^= 1;
if(opt_mgr["--cexmin"])
ufar_manager.params.fCexMin ^= 1;
if(opt_mgr["--pba_uif"])
ufar_manager.params.fPbaUif ^= 1;
if(opt_mgr["--pbasim"])
ufar_manager.params.fPbaSim ^= 1;
if(opt_mgr["--pbacex"])
ufar_manager.params.fPbaCex ^= 1;
if(opt_mgr["--satmin"])
ufar_manager.params.fSatMin ^= 1;
if(opt_mgr["--cbawb"])
ufar_manager.params.fCbaWb ^= 1;
if(opt_mgr["--grey"])
ufar_manager.params.fGrey ^= 1;
if(opt_mgr["--grey2"])
ufar_manager.params.nGrey = stof(opt_mgr.GetOptVal("--grey2"));
if(opt_mgr["--sp"])
ufar_manager.params.fSuper_prove ^= 1;
if(opt_mgr["--simp"])
ufar_manager.params.fSimple ^= 1;
if(opt_mgr["--syn"])
ufar_manager.params.fSyn ^= 1;
if(opt_mgr["--pth"])
ufar_manager.params.fPthread ^= 1;
if(opt_mgr["--onewb"])
ufar_manager.params.iOneWb = stoi(opt_mgr.GetOptVal("--onewb"));
if(opt_mgr["--exp"])
ufar_manager.params.iExp = stoi(opt_mgr.GetOptVal("--exp"));
if(opt_mgr["--par"])
ufar_manager.params.parSetting = opt_mgr.GetOptVal("--par");
if(opt_mgr["--sim"])
ufar_manager.params.simSetting = opt_mgr.GetOptVal("--sim");
if(opt_mgr["--dump_states"]) {
smatch sub_match;
string option = opt_mgr.GetOptVal("--dump_states");
if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
ufar_manager.params.fileStatesOut = sub_match[1].str();
else
ufar_manager.params.fileStatesOut = opt_mgr.GetOptVal("--dump_states");
}
if(opt_mgr["--read_states"])
ufar_manager.params.fileStatesIn = opt_mgr.GetOptVal("--read_states");
if(opt_mgr["--lazysim"])
ufar_manager.params.fLazySim ^= 1;
if(opt_mgr["-v"])
ufar_manager.params.iVerbosity = stoi(opt_mgr.GetOptVal("-v"));
if(opt_mgr["--timeout"])
ufar_manager.params.nTimeout = stoi(opt_mgr.GetOptVal("--timeout"));
if(opt_mgr["--seq"])
ufar_manager.params.nSeqLookBack = stoi(opt_mgr.GetOptVal("--seq"));
if(opt_mgr["--dump-abs"]) {
smatch sub_match;
string option = opt_mgr.GetOptVal("--dump-abs");
if(regex_search(option, sub_match, regex(R"(/?(\w+)\.v$)")))
ufar_manager.params.fileAbs = sub_match[1].str();
else
ufar_manager.params.fileAbs = opt_mgr.GetOptVal("--dump");
}
if(opt_mgr["--dump"]) {
smatch sub_match;
string option = opt_mgr.GetOptVal("--dump");
if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
ufar_manager.params.fileName = sub_match[1].str();
else
ufar_manager.params.fileName = opt_mgr.GetOptVal("--dump");
}
// ufar_manager.DumpParams();
LogT::prefix = "UIF_PROVE";
set<unsigned> set_op_types;
set_op_types.insert(WLC_OBJ_ARI_MULTI);
if (opt_mgr["--adder"])
set_op_types.insert(WLC_OBJ_ARI_ADD);
if (!UFAR::HasOperator(Wlc_AbcGetNtk(pAbc), set_op_types)) {
cout << "There is no operator for UIF.\n";
return 0;
}
Wlc_Ntk_t * pNew = NULL;
timeval t1, t2;
gettimeofday(&t1, NULL);
if (!opt_mgr["--miter"]) {
if (Wlc_NtkPoNum(Wlc_AbcGetNtk(pAbc)) != 2) {
cout << "The current design doesn't have dual outputs.\n";
return 0;
}
pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0);
Wlc_AbcUpdateNtk(pAbc, pNew);
}
if (ufar_manager.params.fNorm) {
pNew = UFAR::NormalizeDataTypes(Wlc_AbcGetNtk(pAbc), set_op_types, true);
Wlc_AbcUpdateNtk(pAbc, pNew);
}
if (opt_mgr["--under"]) {
pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), stoi(opt_mgr.GetOptVal("--under")));
Wlc_AbcUpdateNtk(pAbc, pNew);
pNew = UFAR::MakeUnderApprox2(Wlc_AbcGetNtk(pAbc), set_op_types, stoi(opt_mgr.GetOptVal("--under")));
Wlc_AbcUpdateNtk(pAbc, pNew);
Wlc_WriteVer(Wlc_AbcGetNtk(pAbc), "UND.v", 0, 0);
}
Gia_Man_t * pGia = UFAR::BitBlast(Wlc_AbcGetNtk(pAbc));
Gia_ManPrintStats( pGia, NULL );
Gia_ManStop( pGia );
ufar_manager.Initialize(Wlc_AbcGetNtk(pAbc), set_op_types);
int ret = ufar_manager.PerformUIFProve(t1);
if (ret == 1) {
LOG(0) << "Proved by UIF (UNSAT).";
} else if (ret == 0) {
LOG(0) << "Falsified by UIF (SAT).";
} else {
LOG(0) << "Undecided by UIF.";
}
gettimeofday(&t2, NULL);
unsigned tTotal = elapsed_time_usec(t1, t2);
if(opt_mgr["--profile"]) {
auto log_profile = [&](const string& str, abctime t) {
LOG(1) << str << " time = " << fixed << setprecision(4) << setw(8) << (double)t/1000000 << " sec [" << setw(7) << (double)t/tTotal*100 << "%]";
};
log_profile("BLSolver ", ufar_manager.profile.tBLSolver);
log_profile("UifRefine ", ufar_manager.profile.tUifRefine);
log_profile("WbRefine ", ufar_manager.profile.tWbRefine);
log_profile("UifSim ", ufar_manager.profile.tUifSim);
log_profile("GbRefine ", ufar_manager.profile.tGbRefine);
}
LOG(0) << "Time = " << setprecision(5) << ((double) (tTotal) / 1000000) << " sec";
return 0;
}
static int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
LogT::prefix = "TEST::";
OptMgr opt_mgr(argv[0]);
opt_mgr.AddOpt("--ntk", "none", "str", "specify the file name (*.aig) for the input network");
opt_mgr.AddOpt("--adder", "no", "", "toggle including adders");
if(!opt_mgr.Parse(argc, argv)) {
opt_mgr.PrintUsage();
return 0;
}
set<unsigned> set_op_types;
set_op_types.insert(WLC_OBJ_ARI_MULTI);
if(opt_mgr["--adder"]) {
set_op_types.insert(WLC_OBJ_ARI_ADD);
}
Wlc_Ntk_t * pNew = UFAR::AddConstFlops(Wlc_AbcGetNtk(pAbc), set_op_types);
Wlc_AbcUpdateNtk(pAbc, pNew);
return 0;
#if 0
opt_mgr.AddOpt("--ntk", "none", "str", "specify the file name (*.aig) for the input network");
opt_mgr.AddOpt("--inv", "none", "str", "specify the file name (*.pla) for the invariant");
if(!opt_mgr.Parse(argc, argv)) {
opt_mgr.PrintUsage();
return 0;
}
string nameNtk = opt_mgr.GetOptVal("--ntk");
string nameInv = opt_mgr.GetOptVal("--inv");
UFAR::TestInvariant(nameNtk, nameInv);
#endif
#if 0
set<unsigned> set_op_types;
set_op_types.insert(WLC_OBJ_ARI_MULTI);
OptMgr opt_mgr(argv[0]);
opt_mgr.AddOpt("--cube", "no", "", "toggle using cubes for interpolants");
if(!opt_mgr.Parse(argc, argv)) {
opt_mgr.PrintUsage();
return 0;
}
UFAR::TestITP(Wlc_AbcGetNtk(pAbc), set_op_types, opt_mgr["--cube"]);
#endif
#if 0
if ( Wlc_AbcGetNtk(pAbc) == NULL ) {
cout << "There is no current design.\n";
return 0;
}
if (Wlc_NtkPoNum(Wlc_AbcGetNtk(pAbc)) != 2) {
cout << "The current design doesn't have dual outputs.\n";
return 0;
}
set<unsigned> set_op_types;
set_op_types.insert(WLC_OBJ_ARI_MULTI);
if (!UFAR::HasOperator(Wlc_AbcGetNtk(pAbc), set_op_types)) {
cout << "There is no operator for UIF.\n";
return 0;
}
Wlc_Ntk_t * pNew = NULL;
pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0);
Wlc_AbcUpdateNtk(pAbc, pNew);
pNew = UFAR::NormalizeDataTypes(Wlc_AbcGetNtk(pAbc), set_op_types, true);
Wlc_AbcUpdateNtk(pAbc, pNew);
ufar_manager.Initialize(Wlc_AbcGetNtk(pAbc), set_op_types);
ufar_manager.DumpMgrInfo();
pNew = ufar_manager.BuildCurrentAbstraction();
Wlc_AbcUpdateNtk(pAbc, pNew);
return 0;
#endif
}

23
src/opt/ufar/UfarCmd.h Executable file
View File

@ -0,0 +1,23 @@
/*
* UifCmd.h
*
* Created on: Aug 25, 2015
* Author: Yen-Sheng Ho
*/
#ifndef SRC_EXT2_UIF_UIFCMD_H_
#define SRC_EXT2_UIF_UIFCMD_H_
#include "base/main/mainInt.h"
#ifdef __cplusplus
extern "C" {
#endif
void Ufar_Init(Abc_Frame_t *pAbc);
#ifdef __cplusplus
}
#endif
#endif /* SRC_EXT2_UIF_UIFCMD_H_ */

1663
src/opt/ufar/UfarMgr.cpp Executable file
View File

File diff suppressed because it is too large Load Diff

144
src/opt/ufar/UfarMgr.h Executable file
View File

@ -0,0 +1,144 @@
/*
* UifMgr.h
*
* Created on: Aug 25, 2015
* Author: Yen-Sheng Ho
*/
#ifndef SRC_EXT2_UIF_UIFMGR_H_
#define SRC_EXT2_UIF_UIFMGR_H_
#include <set>
#include <string>
#include <vector>
#include <unordered_map>
#include <sstream>
#include <iostream>
#include <memory>
#include <sys/time.h>
typedef struct Wlc_Ntk_t_ Wlc_Ntk_t;
typedef struct Abc_Cex_t_ Abc_Cex_t;
typedef struct Gia_Man_t_ Gia_Man_t;
namespace UFAR {
using VecVecInt = std::vector<std::vector<int> >;
using VecVecStr = std::vector<std::vector<std::string> >;
using VecChar = std::vector<char>;
using VecStr = std::vector<std::string>;
using IntPair = std::pair<int, int>;
struct OperatorID;
struct UifPair;
struct Greyness;
using UIF_PAIR = UifPair;
class SimUifPairFinder;
class CexUifPairFinder;
class UfarManager {
public:
struct Params {
Params();
bool fCexMin;
bool fPbaUif;
bool fLazySim;
bool fPbaSim;
bool fPbaCex;
bool fSatMin;
bool fCbaWb;
bool fGrey;
float nGrey;
bool fNorm;
bool fSuper_prove;
bool fSimple;
bool fSyn;
bool fPthread;
int iOneWb;
int iExp;
unsigned nConstraintLimit;
unsigned iVerbosity;
unsigned nSeqLookBack;
unsigned nTimeout;
std::string simSetting;
std::string parSetting;
std::string fileName;
std::string fileAbs;
std::string fileStatesOut;
std::string fileStatesIn;
};
struct Profile {
Profile() : tBLSolver(0), tUifRefine(0), tWbRefine(0), tUifSim(0), tGbRefine(0) {}
unsigned tBLSolver;
unsigned tUifRefine;
unsigned tWbRefine;
unsigned tUifSim;
unsigned tGbRefine;
};
UfarManager();
~UfarManager();
void Initialize(Wlc_Ntk_t * pNtk, const std::set<unsigned>& types);
Wlc_Ntk_t * BuildCurrentAbstraction();
Wlc_Ntk_t * ApplyUifConstraints(Wlc_Ntk_t * pNtk, std::vector<int>& vec_ids);
void FindUifPairsUsingCex(Abc_Cex_t * pCex, Abc_Cex_t ** ppCex = NULL);
void FindUifPairsUsingSim();
void DetermineWhiteBoxes(Abc_Cex_t * pCex);
void DetermineGreyness(Abc_Cex_t * pCex);
int VerifyCurrentAbstraction(Abc_Cex_t ** ppCex);
int PerformUIFProve(const timeval& timer);
void DumpMgrInfo() const;
void DumpParams() const;
void GetOperatorsInCex(Abc_Cex_t *pCex, VecVecStr* pRes);
Params params;
Profile profile;
private:
Wlc_Ntk_t * _abstract_operators(Wlc_Ntk_t * pNtk, const std::vector<int>& vec_ids) const;
Wlc_Ntk_t * _introduce_choices(std::vector<unsigned>& vec_choice2idx, bool fBlack);
Wlc_Ntk_t * _introduce_bitwise_choices(std::vector<IntPair>& vec_choice2idx);
Wlc_Ntk_t * _set_up_constraints(std::vector<int>& vec_ids);
void _compute_core_choices(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, std::vector<unsigned>& vec_cores, int num_sel_pis);
void _simulate();
void _perform_proof_based_white_boxing(Abc_Cex_t * pCex);
void _perform_proof_based_grey_boxing(Abc_Cex_t * pCex);
void _perform_cex_based_white_boxing();
std::string _get_profile_uf_wb();
void _massage_state_b();
void _dump_states(const std::string& file);
void _read_states(const std::string& file);
void _shrink_final_abstraction();
Wlc_Ntk_t * _pOrigNtk;
std::vector<std::string> _vec_orig_names;
std::vector<int> _vec_op_ids;
std::vector<bool> _vec_op_blackbox_marks;
std::vector<std::vector<int> > _vec_vec_op_ffs;
std::vector<Greyness> _vec_op_greyness;
std::set<UIF_PAIR> _set_uif_pairs;
std::set<UIF_PAIR> _set_uif_sim_pairs;
std::set<OperatorID> _set_prev_ops;
Wlc_Ntk_t * _pAbsWithAuxPos;
std::unique_ptr<SimUifPairFinder> _p_sim_mgr;
std::unique_ptr<CexUifPairFinder> _p_cex_mgr;
std::ostringstream _oss;
struct timespec _timeout;
};
}
#endif /* SRC_EXT2_UIF_UIFMGR_H_ */

289
src/opt/ufar/UfarPth.cpp Executable file
View File

@ -0,0 +1,289 @@
#include "UfarPth.h"
#include "opt/util/util.h"
#include "opt/untk/NtkNtk.h"
#include "sat/bmc/bmc.h"
#include "proof/pdr/pdr.h"
#include "aig/gia/giaAig.h"
#include <pthread.h>
#include <unistd.h>
extern "C" {
Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pAig );
int Abc_NtkDarBmc3( Abc_Ntk_t * pAbcNtk, Saig_ParBmc_t * pBmcPars, int fOrDecomp );
Wla_Man_t * Wla_ManStart( Wlc_Ntk_t * pNtk, Wlc_Par_t * pPars );
void Wla_ManStop( Wla_Man_t * pWla );
int Wla_ManSolve( Wla_Man_t * pWla, Wlc_Par_t * pPars );
}
static volatile int g_nRunIds = 0; // the number of the last prover instance
int Ufar_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }
int Ufar_GetGlobalRunId() { return g_nRunIds; }
using namespace std;
namespace UFAR {
// mutext to control access to shared variables
pthread_mutex_t g_mutex;
// cv to control timer
pthread_cond_t g_cond;
struct Pth_Data_t
{
Pth_Data_t () : RunId(-1), pGia(NULL), pWlc(NULL), ppCex(NULL), RetValue(-1), engine(NULL) {}
void set ( const string * eng, int id, Wlc_Ntk_t * pWL, Gia_Man_t * pBL, Abc_Cex_t ** pp ) { engine = eng; RunId = id; pWlc = pWL; pGia = pBL; ppCex = pp; }
int RunId;
Gia_Man_t * pGia;
Wlc_Ntk_t * pWlc;
Abc_Cex_t ** ppCex;
int RetValue;
const string * engine;
};
class Solver {
public:
virtual ~Solver() {}
virtual int Solve() = 0;
virtual void SetCex( Abc_Cex_t ** ppCex ) = 0;
};
class PDR : public Solver {
public:
PDR( void * pArg ) {
Pth_Data_t * pData = (Pth_Data_t *)pArg;
_pAig = Gia_ManToAigSimple( pData->pGia );
Pdr_Par_t * pPdrPars = &_PdrPars;
Pdr_ManSetDefaultParams(pPdrPars);
pPdrPars->nConfLimit = 0;
pPdrPars->RunId = pData->RunId;
pPdrPars->pFuncStop = Ufar_CallBackToStop;
}
~PDR() { Aig_ManStop(_pAig); }
virtual int Solve() {
return Pdr_ManSolve( _pAig, &_PdrPars );
}
virtual void SetCex( Abc_Cex_t ** ppCex ) {
assert( _pAig->pSeqModel );
*(ppCex) = _pAig->pSeqModel;
_pAig->pSeqModel = NULL;
}
private:
Aig_Man_t * _pAig;
Pdr_Par_t _PdrPars;
};
class PDRA : public Solver {
public:
PDRA( void * pArg ) {
Pth_Data_t * pData = (Pth_Data_t *)pArg;
_pAig = Gia_ManToAigSimple( pData->pGia );
Pdr_Par_t * pPdrPars = &_PdrPars;
Pdr_ManSetDefaultParams(pPdrPars);
pPdrPars->nConfLimit = 0;
pPdrPars->RunId = pData->RunId;
pPdrPars->pFuncStop = Ufar_CallBackToStop;
pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction)
pPdrPars->fCtgs = 1; // use 'pdr -c' (improved generalization)
pPdrPars->fSkipDown = 0; // use 'pdr -n' (improved generalization)
pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
}
~PDRA() { Aig_ManStop(_pAig); }
virtual int Solve() {
return Pdr_ManSolve( _pAig, &_PdrPars );
}
virtual void SetCex( Abc_Cex_t ** ppCex ) {
assert( _pAig->pSeqModel );
*(ppCex) = _pAig->pSeqModel;
_pAig->pSeqModel = NULL;
}
private:
Aig_Man_t * _pAig;
Pdr_Par_t _PdrPars;
};
class BMC3 : public Solver {
public:
BMC3 ( void * pArg ) {
Pth_Data_t * pData = (Pth_Data_t *)pArg;
Aig_Man_t * pAig = Gia_ManToAigSimple( pData->pGia );
_pNtk = Abc_NtkFromAigPhase( pAig );
Aig_ManStop( pAig );
Saig_ParBmc_t * pBmcPars = &_Pars;
Saig_ParBmcSetDefaultParams( pBmcPars );
pBmcPars->RunId = pData->RunId;
pBmcPars->pFuncStop = Ufar_CallBackToStop;
}
~BMC3() { Abc_NtkDelete(_pNtk); }
virtual int Solve() {
return Abc_NtkDarBmc3( _pNtk, &_Pars, 0 );
}
virtual void SetCex( Abc_Cex_t ** ppCex ) {
assert( _pNtk->pSeqModel );
*(ppCex) = _pNtk->pSeqModel;
_pNtk->pSeqModel = NULL;
}
private:
Abc_Ntk_t * _pNtk;
Saig_ParBmc_t _Pars;
};
class PDRWLA : public Solver {
public:
PDRWLA( void * pArg ) {
Pth_Data_t * pData = (Pth_Data_t *)pArg;
Wlc_Ntk_t * pNtk = pData->pWlc;
Wlc_Par_t * pWlcPars = &_Pars;
Wlc_ManSetDefaultParams( pWlcPars );
pWlcPars->nBitsAdd = 8;
pWlcPars->nBitsMul = 4;
pWlcPars->nBitsMux = 8;
pWlcPars->fXorOutput = 0;
pWlcPars->nLimit = 50;
pWlcPars->fVerbose = 1;
pWlcPars->fProofRefine = 1;
pWlcPars->fHybrid = 0;
pWlcPars->fCheckCombUnsat = 1;
pWlcPars->RunId = pData->RunId;
pWlcPars->pFuncStop = Ufar_CallBackToStop;
_pWla = Wla_ManStart( pNtk, pWlcPars );
}
~PDRWLA() { Wla_ManStop(_pWla); }
virtual int Solve() {
return Wla_ManSolve( _pWla, &_Pars );
}
virtual void SetCex( Abc_Cex_t ** ppCex ) {
assert( _pWla->pCex );
*(ppCex) = _pWla->pCex;
_pWla->pCex = NULL;
}
private:
Wla_Man_t * _pWla;
Wlc_Par_t _Pars;
};
void KillOthers() {
pthread_cond_signal( &g_cond );
++g_nRunIds;
}
void * RunSolver( void * pArg ) {
Pth_Data_t * pData = (Pth_Data_t *)pArg;
Solver * pSolver = NULL;
int status;
if ( *(pData->engine) == "pdr" )
pSolver = new PDR( pArg );
else if ( *(pData->engine) == "pdra" )
pSolver = new PDRA( pArg );
else if ( *(pData->engine) == "bmc3" )
pSolver = new BMC3( pArg );
else if ( *(pData->engine) == "wla" )
pSolver = new PDRWLA( pArg );
else {
pthread_exit( NULL );
assert(0);
return 0;
}
pData->RetValue = pSolver->Solve();
int ret = pData->RetValue;
status = pthread_mutex_lock(&g_mutex); assert( status == 0 );
if ( ret == 0 ) {
pSolver->SetCex( pData->ppCex );
LOG(2) << *(pData->engine) << " found CEX. RunId = " << pData->RunId;
KillOthers();
} else if ( ret == 1 ) {
LOG(2) << *(pData->engine) << " proved the problem. RunId = " << pData->RunId;
KillOthers();
} else {
if ( pData->RunId < g_nRunIds ) {
LOG(2) << *(pData->engine) << " was cancelled. RunId = " << pData->RunId;
}
}
status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
delete pSolver;
pthread_exit( NULL );
assert(0);
return 0;
}
void * Timer ( void * pArg ) {
struct timespec * pTimeout = ( struct timespec * )pArg;
int retcode = 0;
int status;
status = pthread_mutex_lock(&g_mutex); assert( status == 0 );
retcode = pthread_cond_timedwait(&g_cond, &g_mutex, pTimeout);
if ( retcode == ETIMEDOUT ) {
LOG(2) << "Timer reached timeout.";
KillOthers();
} else {
LOG(2) << "Timer was cancelled.";
}
status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
pthread_exit( NULL );
assert(0);
return 0;
}
int RunConcurrentSolver( Wlc_Ntk_t * pNtk, const vector<string>& vSolvers, Abc_Cex_t ** ppCex, struct timespec * pTimeout ) {
assert( pTimeout );
int status;
vector<Pth_Data_t> vDatas ( vSolvers.size() );
vector<pthread_t> vThreads ( vSolvers.size() );
pthread_t timer;
Gia_Man_t * pGia = BitBlast( pNtk );
status = pthread_create( &timer, NULL, Timer, pTimeout );
assert( status == 0 );
for ( size_t i = 0; i < vSolvers.size(); ++i ) {
vDatas[i].set( &vSolvers[i], g_nRunIds, pNtk, pGia, ppCex );
status = pthread_create( &vThreads[i], NULL, RunSolver, &vDatas[i] );
assert( status == 0 );
}
status = pthread_join( timer, NULL );
assert( status == 0 );
for ( size_t i = 0; i < vSolvers.size(); ++i ) {
status = pthread_join( vThreads[i], NULL );
assert( status == 0 );
}
Gia_ManStop( pGia );
for( auto& x : vDatas ) {
if ( x.RetValue != -1 )
return x.RetValue;
}
return -1;
}
}

17
src/opt/ufar/UfarPth.h Executable file
View File

@ -0,0 +1,17 @@
//
// Created by Yen-Sheng Ho on 04/09/17.
//
#ifndef SRC_EXT2_UFAR_PTH_H
#define SRC_EXT2_UFAR_PTH_H
#include "base/wlc/wlc.h"
#include <vector>
#include <string>
namespace UFAR
{
int RunConcurrentSolver( Wlc_Ntk_t * pNtk, const std::vector<std::string>& vSolvers, Abc_Cex_t ** ppCex, struct timespec * timeout );
}
#endif //SRC_EXT2_UFAR_PTH_H

3
src/opt/ufar/module.make Executable file
View File

@ -0,0 +1,3 @@
SRC += src/opt/ufar/UfarCmd.cpp \
src/opt/ufar/UfarPth.cpp \
src/opt/ufar/UfarMgr.cpp

63
src/opt/untk/Netlist.cpp Executable file
View File

@ -0,0 +1,63 @@
//
// Created by Yen-Sheng Ho on 8/9/16.
//
#include "Netlist.h"
#include <base/wlc/wlc.h>
#include <iostream>
using namespace std;
namespace UFAR {
WNetlist::WNetlist() {
_pNtk = Wlc_NtkAlloc("main", 100);
}
WNetlist::WNetlist(Wlc_Ntk_t *pNtk) {
if (pNtk)
_pNtk = Wlc_NtkDupDfsSimple(pNtk);
else
_pNtk = NULL;
}
WNetlist::WNetlist(const WNetlist& that) {
_pNtk = Wlc_NtkDupDfsSimple(that._pNtk);
}
WNetlist::WNetlist(WNetlist && that) {
_pNtk = that._pNtk;
that._pNtk = NULL;
}
WNetlist& WNetlist::operator=(const WNetlist& that) {
Wlc_Ntk_t * pTemp = _pNtk;
_pNtk = Wlc_NtkDupDfsSimple(that._pNtk);
if (pTemp) Wlc_NtkFree(pTemp);
return *this;
}
WNetlist::~WNetlist() {
if (_pNtk) Wlc_NtkFree(_pNtk);
}
void WNetlist::Clear() {
if (_pNtk) Wlc_NtkFree(_pNtk);
_pNtk = Wlc_NtkAlloc("main", 100);
}
bool WNetlist::Empty() const {
if (_pNtk == NULL) return true;
return Wlc_NtkObjNum(_pNtk) == 0;
}
void WNetlist::Reset(Wlc_Ntk_t *pNtk) {
Wlc_Ntk_t * pTemp = _pNtk;
_pNtk = Wlc_NtkDupDfsSimple(pNtk);
if (pTemp) Wlc_NtkFree(pTemp);
}
}

33
src/opt/untk/Netlist.h Executable file
View File

@ -0,0 +1,33 @@
//
// Created by ysho on 8/9/16.
//
#ifndef ABC_WAR_NETLIST_H
#define ABC_WAR_NETLIST_H
#include <type_traits>
typedef struct Wlc_Ntk_t_ Wlc_Ntk_t;
namespace UFAR {
class WNetlist {
public:
WNetlist();
WNetlist(Wlc_Ntk_t * pNtk);
WNetlist(const WNetlist& that);
~WNetlist();
WNetlist(WNetlist && that);
WNetlist& operator=(const WNetlist& that);
Wlc_Ntk_t * GetNtk() const {return _pNtk;}
void Clear();
bool Empty() const;
void Reset(Wlc_Ntk_t * pNtk);
private:
Wlc_Ntk_t * _pNtk;
};
}
#endif //ABC_WAR_NETLIST_H

12
src/opt/untk/NtkCmd.cpp Executable file
View File

@ -0,0 +1,12 @@
/*
* NtkCmd.cpp
*
* Created on: Aug 25, 2015
* Author: Yen-Sheng Ho
*/
#include "opt/untk/NtkCmd.h"
void Ntk_Init (Abc_Frame_t *pAbc)
{
}

15
src/opt/untk/NtkCmd.h Executable file
View File

@ -0,0 +1,15 @@
/*
* NtkCmd.h
*
* Created on: Aug 25, 2015
* Author: Yen-Sheng Ho
*/
#ifndef SRC_EXT2_NTK_NTKCMD_H_
#define SRC_EXT2_NTK_NTKCMD_H_
#include "base/main/mainInt.h"
void Ntk_Init(Abc_Frame_t *pAbc);
#endif /* SRC_EXT2_NTK_NTKCMD_H_ */

1487
src/opt/untk/NtkNtk.cpp Executable file
View File

File diff suppressed because it is too large Load Diff

150
src/opt/untk/NtkNtk.h Executable file
View File

@ -0,0 +1,150 @@
/*
* NtkNtk.h
*
* Created on: Aug 25, 2015
* Author: Yen-Sheng Ho
*/
#ifndef SRC_EXT2_NTK_NTKNTK_H_
#define SRC_EXT2_NTK_NTKNTK_H_
#include <set>
#include <vector>
#include <string>
#include <array>
#include <sstream>
#include <algorithm>
#include <base/wlc/wlc.h>
#include "Netlist.h"
typedef struct Wlc_Ntk_t_ Wlc_Ntk_t;
typedef struct Abc_Cex_t_ Abc_Cex_t;
typedef struct Vec_Int_t_ Vec_Int_t;
typedef struct Gia_Man_t_ Gia_Man_t;
namespace UFAR {
using VecVecChar = std::vector<std::vector<char> >;
using VecVecInt = std::vector<std::vector<int> >;
using IntPair = std::pair<int, int>;
struct OperatorID {
OperatorID() : idx(-1), timediff(0) {}
OperatorID(int i) : idx(i), timediff(0) {}
OperatorID(int i, int t) : idx(i), timediff(t) {}
bool operator< (const OperatorID& rhs) const {
if (timediff != rhs.timediff) return (timediff < rhs.timediff);
return (idx < rhs.idx);
}
bool operator!= (const OperatorID& rhs) const {
return ((idx != rhs.idx) || (timediff != rhs.timediff));
}
int idx;
int timediff;
};
std::ostream& operator<<(std::ostream& os, const OperatorID& obj);
struct UifPair {
UifPair(const OperatorID& first_, const OperatorID& second_) : first(first_), second(second_), fMark(false) {}
UifPair(const OperatorID& first_, const OperatorID& second_, bool fMark_) : first(first_), second(second_), fMark(fMark_) {}
bool operator< (const UifPair& rhs) const {
if(first != rhs.first) return (first < rhs.first);
if(second != rhs.second) return (second < rhs.second);
return (!fMark && rhs.fMark);
}
OperatorID first;
OperatorID second;
bool fMark;
};
class Greyness {
public:
Greyness(Wlc_Ntk_t * pNtk, Wlc_Obj_t * pObj);
std::string to_string() const {
std::ostringstream oss;
for (size_t i = 0; i < _vec_black_bits.size(); ++i)
oss << ( _vec_black_bits[i] ? '0' : '1' );
return oss.str();
}
bool IsGrey() const {
return (!IsBlack() && !IsWhite());
}
bool IsWhite() const {
return (std::find(_vec_black_bits.begin(), _vec_black_bits.end(), true) == _vec_black_bits.end());
}
bool IsBlack() const {
return (std::find(_vec_black_bits.begin(), _vec_black_bits.end(), false) == _vec_black_bits.end());
}
unsigned TotalCost() const { return _total_cost; }
unsigned CurrentCost() const { return _current_cost; }
void UpdateCost();
size_t Size() const { return _vec_black_bits.size(); }
bool Get(size_t pos) const { return _vec_black_bits[pos]; }
void Set(size_t pos, bool val) { _vec_black_bits[pos] = val; }
void SetWhite() {
_vec_black_bits = std::vector<bool>(_vec_black_bits.size(), false);
_current_cost = _total_cost;
}
bool IsTooWhite(float threshold) const {
float ratio = float(_current_cost) / float(_total_cost);
if ((ratio > threshold) || (_current_cost == _total_cost))
return true;
if (ratio > 0.5 && _total_cost < 1000)
return true;
return false;
}
private:
std::vector<bool> _vec_black_bits;
unsigned _total_cost;
unsigned _current_cost;
unsigned _orig_size;
WNetlist _N_white;
int _iOpId;
};
Wlc_Ntk_t * AbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit );
Wlc_Ntk_t * AddConstFlops( Wlc_Ntk_t * p, const std::set<unsigned>& types );
Wlc_Ntk_t * IntroduceChoices( Wlc_Ntk_t * p, Vec_Int_t * vNodes );
Wlc_Ntk_t * IntroduceBitwiseChoices( Wlc_Ntk_t * pNtk, std::vector<int>& vec_ids, const std::vector<Greyness>& vec_greys, std::vector<IntPair>& vec_choice2idx );
Wlc_Ntk_t * CreateMiter(Wlc_Ntk_t *pNtk, bool fXor);
Wlc_Ntk_t * NormalizeDataTypes(Wlc_Ntk_t * p, const std::set<unsigned>& types, bool fUnify);
Wlc_Ntk_t * AddAuxPOsForOperators(Wlc_Ntk_t * p, std::vector<int>& vec_ids, int max_input_bw = -1, int max_output_bw = -1);
Wlc_Ntk_t * RemoveAuxPOs(Wlc_Ntk_t * p, int iStart);
Wlc_Ntk_t * DupNtkAndUpdateIDs(Wlc_Ntk_t * p, std::vector<int>& vec_ids);
Wlc_Ntk_t * ApplyGreynessConstraints(Wlc_Ntk_t * pNtk, const std::vector<Greyness>& vec_grey, std::vector<int>& vec_ids);
Wlc_Ntk_t * IntroducePrevOperators(Wlc_Ntk_t * pNtk, std::vector<int>& vec_ids, const std::set<OperatorID>& set_prev_ops, VecVecInt& vv_op_ffs);
Wlc_Ntk_t * ApplyGreyConstraints(Wlc_Ntk_t * pNtk, std::vector<int>& vec_ids, bool fSeq);
int AddOneFanoutFF(Wlc_Ntk_t * pNtk, int obj_id, unsigned& count_bits);
int AddOneUifImplication(Wlc_Ntk_t * pNtk, const std::array<int, 3>& wires1, const std::array<int, 3>& wires2);
void FoldCombConstraints(Wlc_Ntk_t *pNtk, Vec_Int_t *vConstrs);
void FoldSeqConstraints(Wlc_Ntk_t *pNtk, Vec_Int_t *vConstrs);
void CollectPoValuesInCex(Gia_Man_t * pGia, Abc_Cex_t * pCex, VecVecChar& po_values, bool fCexMin);
bool HasOperator(const Wlc_Ntk_t * p, const std::set<unsigned>& types);
void ComputeMaxBW(Wlc_Ntk_t * p, const std::vector<int>& vec_ids, int& max_input_bw, int& max_output_bw );
void PrintWordCEX(Wlc_Ntk_t * pNtk, Abc_Cex_t * pCex, const std::vector<std::string>* names = nullptr);
unsigned compute_bit_level_pi_num(Wlc_Ntk_t * pNtk);
int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const std::string* pFileName = NULL, const std::string* pParSetting = NULL, bool fSyn = false, struct timespec * timeout = NULL);
int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const std::string* pFileName = NULL, const std::string* pParSetting = NULL, bool fSyn = false);
Gia_Man_t * BitBlast(Wlc_Ntk_t * pNtk);
Gia_Man_t * GetInvMiter(Wlc_Ntk_t * pNtk, char * nameInv);
void TestInvariant(std::string& nameNtk, std::string& nameInv);
Wlc_Ntk_t * MakeUnderApprox(Wlc_Ntk_t * pNtk, int num_bits);
Wlc_Ntk_t * MakeUnderApprox2(Wlc_Ntk_t * pNtk, const std::set<unsigned>& types, int num_bits);
}
#endif /* SRC_EXT2_NTK_NTKNTK_H_ */

6
src/opt/untk/module.make Executable file
View File

@ -0,0 +1,6 @@
SRC += src/opt/untk/NtkCmd.cpp \
src/opt/untk/NtkCmd.h \
src/opt/untk/Netlist.cpp \
src/opt/untk/Netlist.h \
src/opt/untk/NtkNtk.cpp \
src/opt/untk/NtkNtk.h

2
src/opt/util/module.make Executable file
View File

@ -0,0 +1,2 @@
SRC += src/opt/util/util.cpp \
src/opt/util/util.h

119
src/opt/util/util.cpp Executable file
View File

@ -0,0 +1,119 @@
/*
* util.cpp
*
* Created on: Aug 31, 2015
* Author: Yen-Sheng Ho
*/
#include <iomanip>
#include <csignal>
#include <unistd.h>
#include "util.h"
using namespace std;
unsigned LogT::loglevel = 0;
string LogT::prefix = "LOG";
bool OptMgr::Parse(int argc, char * argv[]) {
if(argc <= 1) return true;
for(int i = 1; i < argc; i++) {
if(_map.count(argv[i]) == 0)
return false;
Option& opt = _map[argv[i]];
opt._val = "yes";
if(!opt.isBool()) {
if (i + 1 == argc)
return false;
opt._val = argv[++i];
}
}
return true;
}
void OptMgr::PrintUsage() {
cout << "usage: " << _cmd << endl;
cout << " Uninterpreted Function Abstraction and Refinement (UFAR)\n";
for (auto x : _map) {
ostringstream ss;
ss << x.first << " " << (x.second.isBool() ? "" : x.second._arg_type);
cout << " " << setw(10) << left << ss.str();
cout << " : " << x.second._help << " [default = " << x.second._default << "]" << endl;
}
}
#ifdef __linux__
#include <sys/prctl.h>
void kill_on_parent_death(int sig)
{
// kill process if parent dies
prctl(PR_SET_PDEATHSIG, sig);
// the parent might have died before calling prctl
// in that case, it would be adopted by init, whose pid is 1
if (getppid() == 1)
{
raise(sig);
}
}
#elif defined(__APPLE__)
#include <thread>
#include <cassert>
#include <sys/types.h>
#include <sys/event.h>
#include <sys/time.h>
void kill_on_parent_death(int sig)
{
const int ppid = getppid();
std::thread monitor_thread([ppid, sig](){
struct kevent change;
EV_SET(&change, ppid, EVFILT_PROC, EV_ADD, NOTE_EXIT, 0, nullptr);
int kq = kqueue();
assert( kq >= 0 );
struct kevent event;
struct timespec ts = {0, 0};
// start listening, we are guaranteed to receive a notification if ppid is dead
kevent(kq, &change, 1, &event, 1, &ts);
// however, if ppid died before the call to kevent, ppid might not be the pid of the parent
// in that case, the process it would be adopted by init, whose pid is 1
if( getppid() == 1 )
{
raise(sig);
}
// now block on kevent until the the parent process dies
retry_eintr([&](){
return kevent(kq, &change, 1, &event, 1, nullptr);
});
raise(sig);
});
monitor_thread.detach();
}
#else // neither linux or OS X
void kill_on_parent_death(int sig)
{
}
#endif

85
src/opt/util/util.h Executable file
View File

@ -0,0 +1,85 @@
/*
* util.h
*
* Created on: Aug 31, 2015
* Author: Yen-Sheng Ho
*/
#ifndef SRC_EXT2_UTIL_UTIL_H_
#define SRC_EXT2_UTIL_UTIL_H_
/* http://stackoverflow.com/questions/6168107/how-to-implement-a-good-debug-logging-feature-in-a-project */
#include <iostream>
#include <sstream>
#include <string>
#include <map>
#include <vector>
#include <sys/time.h>
class LogT {
public:
LogT(unsigned _loglevel = 0) {
// _buffer << "LOG" << _loglevel << " :" << std::string(_loglevel > 0 ? _loglevel * 4 : 1, ' ');
_buffer << prefix << " :" << std::string(_loglevel > 0 ? _loglevel * 4 : 1, ' ');
}
template<typename T>
LogT & operator<<(T const & value) {
_buffer << value;
return *this;
}
~LogT() {
std::cout << _buffer.str() << std::endl;
}
static unsigned loglevel;
static std::string prefix;
private:
std::ostringstream _buffer;
};
#define LOG(level) \
if (level > LogT::loglevel) ; \
else LogT(level)
class OptMgr {
public:
OptMgr(const std::string& cmd) : _cmd(cmd) {}
bool Parse(int argc, char * argv[]);
void AddOpt(const std::string& opt, const std::string& default_val, const std::string& arg_type, const std::string& help) {
_map[opt] = Option(default_val, arg_type, help);
}
std::string GetOptVal(const std::string& opt) {return _map[opt]._val;}
bool operator[](const std::string& opt) {return _has_opt(opt);}
void PrintUsage();
private:
struct Option {
Option(){}
Option(const std::string& val, const std::string& arg_type, const std::string& help) :
_default(val), _help(help), _arg_type(arg_type){}
bool isBool() {return _arg_type == "";}
std::string _default;
std::string _help;
std::string _arg_type;
std::string _val;
};
bool _has_opt(const std::string& opt) {return !_map[opt]._val.empty();}
std::map<std::string, Option> _map;
std::string _cmd;
};
static inline unsigned elapsed_time_usec(const timeval& tBefore, const timeval& tAfter) {
return (tAfter.tv_sec - tBefore.tv_sec)*1000000 + (tAfter.tv_usec - tBefore.tv_usec);
}
void kill_on_parent_death(int sig);
int call_python(const char* modulename, const char* funcname, const char* aig, std::vector<int>& cex);
#endif /* SRC_EXT2_UTIL_UTIL_H_ */