Source code for claripy.backends.backend_z3_parallel

import os
import pickle
import threading

num_children = 0

import logging

l = logging.getLogger("claripy.backends.backend_z3_parallel")

from .backend_z3 import BackendZ3

[docs]class BackendZ3Parallel(BackendZ3):
[docs] def __init__(self): BackendZ3.__init__(self) self._child = False self._lock = threading.RLock() self._cache_objects = False
def _background(self, f_name, *args, **kwargs): global num_children f = getattr(BackendZ3, f_name) if self._child: return f(self, *args, **kwargs) p_r, p_w = os.pipe() p = os.fork() if p == 0: self._child = True self._lock = threading.RLock() try: r = f(self, *args, **kwargs) except UnsatError as e: r = e # print("WRITING (%d)" % os.getpid()) pickled = pickle.dumps(r, -1) written = 0 while written < len(pickled): written += os.write(p_w, pickled[written:]) os.close(p_w) os.close(p_r) # print("WROTE (%d)" % os.getpid()) os.kill(os.getpid(), 9) # os.abort() # sys.exit(1) else: os.close(p_w) num_children += 1 l.debug("in _background with function %s and child %d (among %d)", f, p, num_children) # print("READING (from %d)" % p) try: strs = [, 1024 * 1024)] while strs[-1] != "": strs.append(, 1024 * 1024)) except EOFError: raise ClaripyError("read error while receiving data from child") os.close(p_r) # print("READ (from %d)" % p) # thread.start_new_thread(os.wait, ()) r = pickle.loads("".join(strs)) os.waitpid(p, 0) num_children -= 1 l.debug("... child %d is done. %d left", p, num_children) if isinstance(r, Exception): raise r else: return r def _synchronize(self, f, *args, **kwargs): if self._child: return getattr(BackendZ3, f)(self, *args, **kwargs) self._lock.acquire() # while not self._lock.acquire(blocking=False): print("ACQUIRING...",__import__('time').sleep(1)) try: return getattr(BackendZ3, f)(self, *args, **kwargs) finally: self._lock.release() @staticmethod def _translate(*args): for a in args: if hasattr(a, "translate"): a.translate() # backgrounded def _results(self, *args, **kwargs): return self._background("_results", *args, **kwargs) def _eval(self, *args, **kwargs): return self._background("_eval", *args, **kwargs) def _batch_eval(self, *args, **kwargs): return self._background("_batch_eval", *args, **kwargs) def _min(self, *args, **kwargs): return self._background("_min", *args, **kwargs) def _max(self, *args, **kwargs): return self._background("_max", *args, **kwargs) def _convert(self, *args, **kwargs): return self._synchronize("_convert", *args, **kwargs)
[docs] def abstract(self, *args, **kwargs): return self._synchronize("abstract", *args, **kwargs)
[docs] def solver(self, *args, **kwargs): return self._synchronize("solver", *args, **kwargs)
def _add(self, *args, **kwargs): return self._synchronize("_add", *args, **kwargs) def _check(self, *args, **kwargs): return self._synchronize("_check", *args, **kwargs) def _simplify(self, *args, **kwargs): return self._synchronize("_simplify", *args, **kwargs)
[docs] def call(self, *args, **kwargs): return self._synchronize("call", *args, **kwargs)
[docs] def resolve(self, *args, **kwargs): return self._synchronize("resolve", *args, **kwargs)
[docs] def simplify(self, *args, **kwargs): return self._synchronize("simplify", *args, **kwargs)
from ..errors import ClaripyError, UnsatError