diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/base/cmd/cmdUtils.c | 2 | ||||
-rw-r--r-- | src/python/abcpy_test.py | 2 | ||||
-rw-r--r-- | src/python/module.make | 4 | ||||
-rw-r--r-- | src/python/package.py | 5 | ||||
-rw-r--r-- | src/python/pyabc.i | 64 | ||||
-rw-r--r-- | src/python/reachx_cmd.py | 108 | ||||
-rw-r--r-- | src/python/setup.py | 2 |
7 files changed, 151 insertions, 36 deletions
diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c index f97a2c6a..683d336e 100644 --- a/src/base/cmd/cmdUtils.c +++ b/src/base/cmd/cmdUtils.c @@ -454,7 +454,7 @@ FILE * CmdFileOpen( Abc_Frame_t * pAbc, char *sFileName, char *sMode, char **pFi else { // print the path/name of the resource file 'abc.rc' that is being loaded - if ( strlen(sRealName) >= 6 && strcmp( sRealName + strlen(sRealName) - 6, "abc.rc" ) == 0 ) + if ( !silent && strlen(sRealName) >= 6 && strcmp( sRealName + strlen(sRealName) - 6, "abc.rc" ) == 0 ) printf( "Loading resource file \"%s\".\n", sRealName ); } } diff --git a/src/python/abcpy_test.py b/src/python/abcpy_test.py index 912cae9f..28c3505b 100644 --- a/src/python/abcpy_test.py +++ b/src/python/abcpy_test.py @@ -34,7 +34,7 @@ import optparse def pytest3_cmd(args): usage = "usage: %prog [options]" - parser = optparse.OptionParser(usage) + parser = optparse.OptionParser(usage, prog="pytest3") parser.add_option("-c", "--cmd", dest="cmd", help="command to ask help for") parser.add_option("-v", "--version", action="store_true", dest="version", help="display Python Version") diff --git a/src/python/module.make b/src/python/module.make index 3f48bbaf..09e2de3f 100644 --- a/src/python/module.make +++ b/src/python/module.make @@ -57,7 +57,7 @@ pyabc.tgz : $(PROG) $(ABC_PYTHON_SRC:_wrap.c=.py) $(ABC_PYTHON_FILES_PREFIX)/abc $(ABC_PYTHON) $(ABC_PYTHON_FILES_PREFIX)/package.py \ --abc=$(PROG) \ --abc_sh=$(ABC_PYTHON_FILES_PREFIX)/abc.sh \ - --pyabc=$(ABC_PYTHON_SRC:_wrap.c=.py) \ + --pyabc=$(ABC_PYTHON_FILES_PREFIX) \ --out=$@ \ $(ABC_PYTHON_OPTIONS) @@ -66,8 +66,6 @@ PYABC_INSTALL_TARGET := $(PYABC_INSTALL_TARGET) PYABC_INSTALL_DIR ?= /hd/common/pyabc/builds/pyabc_builds/ -.PHONY: zzz - pyabc_install_target: pyabc_extension_bdist mkdir -p "$(PYABC_INSTALL_DIR)/$(PYABC_INSTALL_TARGET)" tar \ diff --git a/src/python/package.py b/src/python/package.py index 9c79a944..1764ab6f 100644 --- a/src/python/package.py +++ b/src/python/package.py @@ -70,7 +70,10 @@ def package(abc_exe, abc_sh, pyabc, ofname, scripts_dir, use_sys): add_file( tf, fullname, os.path.join("pyabc/scripts", fn), 0666, mtime) add_dir(tf, "pyabc/lib", mtime) - add_file( tf, pyabc, "pyabc/lib/pyabc.py", 0666, mtime) + + for entry in os.listdir(pyabc): + if entry.endswith('.py'): + add_file( tf, os.path.join(pyabc, entry), os.path.join("pyabc/lib", entry), 0666, mtime) if not use_sys: # ZIP standard library diff --git a/src/python/pyabc.i b/src/python/pyabc.i index 44a880a7..1da81016 100644 --- a/src/python/pyabc.i +++ b/src/python/pyabc.i @@ -262,8 +262,6 @@ void pyabc_internal_set_command_callback( PyObject* callback ) pyabc_internal_python_command_callback = callback; } -PyThreadState *_save; - static int pyabc_internal_abc_command_callback(Abc_Frame_t * pAbc, int argc, char ** argv) { int i; @@ -271,13 +269,15 @@ static int pyabc_internal_abc_command_callback(Abc_Frame_t * pAbc, int argc, cha PyObject* args; PyObject* arglist; PyObject* res; - + + PyGILState_STATE gstate; + long lres; if ( !pyabc_internal_python_command_callback ) return 0; - Py_BLOCK_THREADS + gstate = PyGILState_Ensure(); args = PyList_New(argc); @@ -292,14 +292,14 @@ static int pyabc_internal_abc_command_callback(Abc_Frame_t * pAbc, int argc, cha if ( !res ) { - Py_UNBLOCK_THREADS + PyGILState_Release(gstate); return -1; } lres = PyInt_AsLong(res); Py_DECREF(res); - Py_UNBLOCK_THREADS + PyGILState_Release(gstate); return lres; } @@ -309,11 +309,11 @@ int run_command(char* cmd) Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame(); int rc; - Py_UNBLOCK_THREADS + Py_BEGIN_ALLOW_THREADS rc = Cmd_CommandExecute(pAbc, cmd); - Py_BLOCK_THREADS + Py_END_ALLOW_THREADS return rc; } @@ -401,13 +401,15 @@ int Util_SignalSystem(const char* cmd) { PyObject* arglist; PyObject* res; + + PyGILState_STATE gstate; long lres; if ( !pyabc_internal_system_callback ) return -1; - Py_BLOCK_THREADS + gstate = PyGILState_Ensure(); arglist = Py_BuildValue("(O)", PyString_FromString(cmd)); Py_INCREF(arglist); @@ -417,14 +419,14 @@ int Util_SignalSystem(const char* cmd) if ( !res ) { - Py_UNBLOCK_THREADS + PyGILState_Release(gstate); return -1; } lres = PyInt_AsLong(res); Py_DECREF(res); - Py_UNBLOCK_THREADS + PyGILState_Release(gstate); return lres; } @@ -437,12 +439,14 @@ int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name) PyObject* arglist; PyObject* res; + PyGILState_STATE gstate; + *out_name = NULL; if ( !pyabc_internal_tmpfile_callback ) return 0; - Py_BLOCK_THREADS + gstate = PyGILState_Ensure(); arglist = Py_BuildValue("(ss)", prefix, suffix); Py_INCREF(arglist); @@ -452,7 +456,7 @@ int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name) if ( !res ) { - Py_UNBLOCK_THREADS + PyGILState_Release(gstate); return -1; } @@ -463,7 +467,7 @@ int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name) Py_DECREF(res); - Py_UNBLOCK_THREADS + PyGILState_Release(gstate); return open(*out_name, O_WRONLY); } @@ -472,11 +476,13 @@ void Util_SignalTmpFileRemove(const char* fname, int fLeave) { PyObject* arglist; PyObject* res; + + PyGILState_STATE gstate; if ( !pyabc_internal_tmpfile_remove_callback ) return; - Py_BLOCK_THREADS + gstate = PyGILState_Ensure(); arglist = Py_BuildValue("(si)", fname, fLeave); Py_INCREF(arglist); @@ -485,7 +491,7 @@ void Util_SignalTmpFileRemove(const char* fname, int fLeave) Py_DECREF(arglist); Py_XDECREF(res); - Py_UNBLOCK_THREADS + PyGILState_Release(gstate); } void pyabc_internal_set_util_callbacks( PyObject* system_callback, PyObject* tmpfile_callback, PyObject* tmpfile_remove_callback ) @@ -607,18 +613,18 @@ class _Cex(object): return _cex_get_frame(self.pCex) def cex_get_vector(): - - res = [] - - for i in xrange(_cex_get_vec_len()): - cex = _cex_get_vec(i) - - if cex is None: - res.append(None) - else: - res.append(_Cex(cex)) - - return res + + res = [] + + for i in xrange(_cex_get_vec_len()): + cex = _cex_get_vec(i) + + if cex is None: + res.append(None) + else: + res.append(_Cex(cex)) + + return res def cex_get(): @@ -1045,7 +1051,7 @@ def cmd_python(cmd_args): usage = "usage: %prog [options] <Python files>" - parser = optparse.OptionParser(usage) + parser = optparse.OptionParser(usage, prog="python") parser.add_option("-c", "--cmd", dest="cmd", help="Execute Python command directly") parser.add_option("-v", "--version", action="store_true", dest="version", help="Display Python Version") diff --git a/src/python/reachx_cmd.py b/src/python/reachx_cmd.py new file mode 100644 index 00000000..8461cb1d --- /dev/null +++ b/src/python/reachx_cmd.py @@ -0,0 +1,108 @@ +# You can use 'from pyabc import *' and then not need the pyabc. prefix everywhere + +import sys +import optparse +import subprocess +import tempfile +import threading +import os +import os.path +from contextlib import contextmanager, nested + +import pyabc + + +def popen_and_wait_with_timeout(timeout,cmd, *args, **kwargs): + """ Wait for a subprocess.Popen object to terminate, or until timeout (in seconds) expires. """ + + p = None + t = None + + try: + p = subprocess.Popen(cmd, *args, **kwargs) + + if timeout <= 0: + timeout = None + + t = threading.Thread(target=lambda: p.communicate()) + t.start() + + t.join(timeout) + + finally: + + if p is not None and p.poll() is None: + p.kill() + + if t is not None and t.is_alive(): + t.join() + + if p is not None: + return p.returncode + + return -1 + +@contextmanager +def temp_file_name(suffix=""): + file = tempfile.NamedTemporaryFile(delete=False, suffix=suffix) + name = file.name + file.close() + + try: + yield name + finally: + os.unlink(name) + +def cygpath(path): + if sys.platform == "win32": + if os.path.isabs(path): + drive, tail = os.path.splitdrive(path) + drive = drive.lower() + tail = tail.split(os.path.sep) + return '/cygdrive/%s'%drive[0] + '/'.join(tail) + else: + path = path.split(os.path.sep) + return "/".join(path) + return path + +def run_reachx_cmd(effort, timeout): + with nested(temp_file_name(suffix=".aig"), temp_file_name()) as (tmpaig_name, tmplog_name): + pyabc.run_command("write %s"%tmpaig_name) + + cmdline = [ + 'read %s'%cygpath(tmpaig_name), + 'qua_ffix -effort %d -L %s'%(effort, cygpath(tmplog_name)), + 'quit' + ] + + cmd = ["jabc", "-c", " ; ".join(cmdline)] + + rc = popen_and_wait_with_timeout(timeout, cmd, shell=False, stdout=sys.stdout, stderr=sys.stderr) + + if rc != 0: + # jabc failed or stopped. Write a status file to update the status to unknown + with open(tmplog_name, "w") as f: + f.write('snl_UNK -1 unknown\n') + f.write('NULL\n') + f.write('NULL\n') + + pyabc.run_command("read_status %s"%tmplog_name) + + return rc + +def reachx_cmd(argv): + usage = "usage: %prog [options]" + + parser = optparse.OptionParser(usage, prog="reachx") + + parser.add_option("-e", "--effort", dest="effort", type=int, default=0, help="effort level. [default=0, means unlimited]") + parser.add_option("-t", "--timeout", dest="timeout", type=int, default=0, help="timeout in seconds [default=0, unlimited]") + + options, args = parser.parse_args(argv) + + rc = run_reachx_cmd(options.effort, options.timeout) + print "%s command: jabc returned: %d"%(argv[0], rc) + + return 0 + +pyabc.add_abc_command(reachx_cmd, "Verification", "reachx", 0) diff --git a/src/python/setup.py b/src/python/setup.py index 3ef006af..68a4adae 100644 --- a/src/python/setup.py +++ b/src/python/setup.py @@ -63,5 +63,5 @@ setup( name='pyabc', version='1.0', ext_modules=[ext], - py_modules=['pyabc','getch','pyabc_split','redirect'] + py_modules=['pyabc','getch','pyabc_split','redirect', 'reachx_cmd'] ) |