| """ |
| The MIT License |
| |
| Copyright (c) 2008 Vijay Ganesh |
| 2014 Jurriaan Bremer, jurriaanbremer@gmail.com |
| 2018-2021 Andrew V. Jones, andrewvaughanj@gmail.com |
| |
| Permission is hereby granted, free of charge, to any person obtaining |
| a copy of this software and associated documentation files (the |
| "Software"), to deal in the Software without restriction, including |
| without limitation the rights to use, copy, modify, merge, publish, |
| distribute, sublicense, and/or sell copies of the Software, and to |
| permit persons to whom the Software is furnished to do so, subject to |
| the following conditions: |
| |
| The above copyright notice and this permission notice shall be |
| included in all copies or substantial portions of the Software. |
| |
| THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, |
| EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF |
| MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND |
| NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE |
| LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION |
| OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION |
| WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. |
| """ |
| |
| import ast |
| from ctypes import cdll, POINTER, CFUNCTYPE |
| from ctypes import c_char_p, c_void_p, c_int32, c_uint32, c_uint64, c_ulong, c_bool |
| import inspect |
| import os.path |
| import sys |
| |
| __all__ = [ |
| 'Expr', 'Solver', 'stp', 'add', 'bitvec', 'bitvecs', 'check', 'model', |
| 'get_git_version_sha', 'get_git_version_tag', 'get_compilation_env', 'get_lib' |
| ] |
| |
| Py3 = sys.version_info >= (3, 0, 0) |
| |
| if Py3: |
| long = int |
| |
| from library_path import PATHS |
| |
| for path in PATHS: |
| if not os.path.exists(path): |
| continue |
| |
| _lib = cdll.LoadLibrary(path) |
| break |
| else: |
| raise Exception('Unable to locate the libstp shared object') |
| |
| |
| def _set_func(name, restype, *argtypes): |
| getattr(_lib, name).restype = restype |
| getattr(_lib, name).argtypes = argtypes |
| |
| _VC = c_void_p |
| _Expr = c_void_p |
| _Type = c_void_p |
| _WholeCounterExample = c_void_p |
| |
| _set_func('get_git_version_sha', c_char_p) |
| _set_func('get_git_version_tag', c_char_p) |
| _set_func('get_compilation_env', c_char_p) |
| _set_func('vc_createValidityChecker', _VC) |
| _set_func('vc_supportsMinisat', c_bool, _VC) |
| _set_func('vc_useMinisat', c_bool, _VC) |
| _set_func('vc_isUsingMinisat', c_bool, _VC) |
| _set_func('vc_supportsSimplifyingMinisat', c_bool, _VC) |
| _set_func('vc_useSimplifyingMinisat', c_bool, _VC) |
| _set_func('vc_isUsingSimplifyingMinisat', c_bool, _VC) |
| _set_func('vc_supportsCryptominisat', c_bool, _VC) |
| _set_func('vc_useCryptominisat', c_bool, _VC) |
| _set_func('vc_isUsingCryptominisat', c_bool, _VC) |
| _set_func('vc_supportsRiss', c_bool, _VC) |
| _set_func('vc_useRiss', c_bool, _VC) |
| _set_func('vc_isUsingRiss', c_bool, _VC) |
| _set_func('vc_boolType', _Type, _VC) |
| _set_func('vc_arrayType', _Type, _VC, _Type, _Type) |
| _set_func('vc_varExpr', _Expr, _VC, c_char_p, _Type) |
| _set_func('vc_varExpr1', _Expr, _VC, c_char_p, c_int32, c_int32) |
| _set_func('vc_getType', _Type, _VC, _Expr) |
| _set_func('vc_getBVLength', c_int32, _VC, _Expr) |
| _set_func('vc_eqExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_trueExpr', _Expr, _VC) |
| _set_func('vc_falseExpr', _Expr, _VC) |
| _set_func('vc_notExpr', _Expr, _VC, _Expr) |
| _set_func('vc_andExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_andExprN', _Expr, _VC, POINTER(_Expr), c_int32) |
| _set_func('vc_orExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_xorExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_orExprN', _Expr, _VC, POINTER(_Expr), c_int32) |
| _set_func('vc_impliesExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_iffExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_iteExpr', _Expr, _VC, _Expr, _Expr, _Expr) |
| _set_func('vc_boolToBVExpr', _Expr, _VC, _Expr) |
| _set_func('vc_paramBoolExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_readExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_writeExpr', _Expr, _VC, _Expr, _Expr, _Expr) |
| _set_func('vc_parseExpr', _Expr, _VC, c_char_p) |
| _set_func('vc_printExpr', None, _VC, _Expr) |
| _set_func('vc_printExprCCode', None, _VC, _Expr) |
| _set_func('vc_printSMTLIB', c_char_p, _VC, _Expr) |
| _set_func('vc_printExprFile', None, _VC, _Expr, c_int32) |
| _set_func('vc_printExprToBuffer', None, _VC, _Expr, POINTER(c_char_p), POINTER(c_ulong)) |
| _set_func('vc_printCounterExample', None, _VC) |
| _set_func('vc_printVarDecls', None, _VC) |
| _set_func('vc_clearDecls', None, _VC) |
| _set_func('vc_printAsserts', None, _VC, c_int32) |
| _set_func('vc_printQueryStateToBuffer', None, _VC, _Expr, POINTER(c_char_p), POINTER(c_ulong), c_int32) |
| _set_func('vc_printCounterExampleToBuffer', None, _VC, POINTER(c_char_p), POINTER(c_ulong)) |
| _set_func('vc_printQuery', None, _VC) |
| _set_func('vc_assertFormula', None, _VC, _Expr) |
| _set_func('vc_simplify', _Expr, _VC, _Expr) |
| _set_func('vc_query_with_timeout', c_int32, _VC, _Expr, c_int32, c_int32) |
| _set_func('vc_query', c_int32, _VC, _Expr) |
| _set_func('vc_getCounterExample', _Expr, _VC, _Expr) |
| _set_func('vc_getCounterExampleArray', None, _VC, _Expr, POINTER(POINTER(_Expr)), POINTER(POINTER(_Expr)), POINTER(c_int32)) |
| _set_func('vc_counterexample_size', c_int32, _VC) |
| _set_func('vc_push', None, _VC) |
| _set_func('vc_pop', None, _VC) |
| _set_func('getBVInt', c_int32, _Expr) |
| _set_func('getBVUnsigned', c_uint32, _Expr) |
| _set_func('getBVUnsignedLongLong', c_uint64, _Expr) |
| _set_func('vc_bvType', _Type, _VC, c_int32) |
| _set_func('vc_bv32Type', _Type, _VC) |
| _set_func('vc_getValueSize', c_int32, _VC, _Type) |
| _set_func('vc_getIndexSize', c_int32, _VC, _Type) |
| _set_func('vc_bvConstExprFromDecStr', _Expr, _VC, c_int32, c_char_p) |
| _set_func('vc_bvConstExprFromStr', _Expr, _VC, c_char_p) |
| _set_func('vc_bvConstExprFromInt', _Expr, _VC, c_int32, c_uint32) |
| _set_func('vc_bvConstExprFromLL', _Expr, _VC, c_int32, c_uint64) |
| _set_func('vc_bv32ConstExprFromInt', _Expr, _VC, c_uint32) |
| _set_func('vc_bvConcatExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvPlusExpr', _Expr, _VC, c_int32, _Expr, _Expr) |
| _set_func('vc_bvPlusExprN', _Expr, _VC, c_int32, POINTER(_Expr), c_int32) |
| _set_func('vc_bv32PlusExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvMinusExpr', _Expr, _VC, c_int32, _Expr, _Expr) |
| _set_func('vc_bv32MinusExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvMultExpr', _Expr, _VC, c_int32, _Expr, _Expr) |
| _set_func('vc_bv32MultExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvDivExpr', _Expr, _VC, c_int32, _Expr, _Expr) |
| _set_func('vc_bvModExpr', _Expr, _VC, c_int32, _Expr, _Expr) |
| _set_func('vc_bvRemExpr', _Expr, _VC, c_int32, _Expr, _Expr) |
| _set_func('vc_sbvDivExpr', _Expr, _VC, c_int32, _Expr, _Expr) |
| _set_func('vc_sbvModExpr', _Expr, _VC, c_int32, _Expr, _Expr) |
| _set_func('vc_sbvRemExpr', _Expr, _VC, c_int32, _Expr, _Expr) |
| _set_func('vc_bvLtExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvLeExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvGtExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvGeExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_sbvLtExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_sbvLeExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_sbvGtExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_sbvGeExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvUMinusExpr', _Expr, _VC, _Expr) |
| _set_func('vc_bvAndExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvOrExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvXorExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvNotExpr', _Expr, _VC, _Expr) |
| _set_func('vc_bvLeftShiftExprExpr', _Expr, _VC, c_int32, _Expr, _Expr) |
| _set_func('vc_bvRightShiftExprExpr', _Expr, _VC, c_int32, _Expr, _Expr) |
| _set_func('vc_bvSignedRightShiftExprExpr', _Expr, _VC, c_int32, _Expr, _Expr) |
| _set_func('vc_bvLeftShiftExpr', _Expr, _VC, c_int32, _Expr) |
| _set_func('vc_bvRightShiftExpr', _Expr, _VC, c_int32, _Expr) |
| _set_func('vc_bv32LeftShiftExpr', _Expr, _VC, c_int32, _Expr) |
| _set_func('vc_bv32RightShiftExpr', _Expr, _VC, c_int32, _Expr) |
| _set_func('vc_bvVar32LeftShiftExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvVar32RightShiftExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvVar32DivByPowOfTwoExpr', _Expr, _VC, _Expr, _Expr) |
| _set_func('vc_bvExtract', _Expr, _VC, _Expr, c_int32, c_int32) |
| _set_func('vc_bvBoolExtract', _Expr, _VC, _Expr, c_int32) |
| _set_func('vc_bvBoolExtract_Zero', _Expr, _VC, _Expr, c_int32) |
| _set_func('vc_bvBoolExtract_One', _Expr, _VC, _Expr, c_int32) |
| _set_func('vc_bvSignExtend', _Expr, _VC, _Expr, c_int32) |
| _set_func('vc_bvCreateMemoryArray', _Expr, _VC, c_char_p) |
| _set_func('vc_bvReadMemoryArray', _Expr, _VC, _Expr, _Expr, c_int32) |
| _set_func('vc_bvWriteToMemoryArray', _Expr, _VC, _Expr, _Expr, _Expr, c_int32) |
| _set_func('vc_bv32ConstExprFromInt', _Expr, _VC, c_uint32) |
| _set_func('exprString', c_char_p, _Expr) |
| _set_func('typeString', c_char_p, _Type) |
| _set_func('getChild', _Expr, _Expr, c_int32) |
| _set_func('vc_isBool', c_int32, _Expr) |
| _set_func('vc_registerErrorHandler', None, CFUNCTYPE(None, c_char_p)) |
| _set_func('vc_getHashQueryStateToBuffer', c_int32, _VC, _Expr) |
| _set_func('vc_Destroy', None, _VC) |
| _set_func('vc_DeleteExpr', None, _Expr) |
| _set_func('vc_getWholeCounterExample', _WholeCounterExample, _VC) |
| _set_func('vc_getTermFromCounterExample', _Expr, _VC, _Expr, _WholeCounterExample) |
| _set_func('vc_deleteWholeCounterExample', None, _WholeCounterExample) |
| _set_func('getDegree', c_int32, _Expr) |
| _set_func('getBVLength', c_int32, _Expr) |
| _set_func('getVWidth', c_int32, _Expr) |
| _set_func('getIWidth', c_int32, _Expr) |
| _set_func('vc_printCounterExampleFile', None, _VC, c_int32) |
| _set_func('exprName', c_char_p, _Expr) |
| _set_func('getExprID', c_int32, _Expr) |
| _set_func('vc_parseMemExpr', c_int32, _VC, c_char_p, POINTER(_Expr), POINTER(_Expr)) |
| |
| |
| class Solver(object): |
| current = None |
| |
| def __init__(self): |
| self.keys = {} |
| self.vc = _lib.vc_createValidityChecker() |
| assert self.vc is not None, 'Error creating validity checker' |
| |
| def __del__(self): |
| # TODO We're not quite there yet. |
| # _lib.vc_Destroy(self.vc) |
| pass |
| |
| def __enter__(self): |
| Solver.current = self |
| return self |
| |
| def __exit__(self, exc_type, exc_value, traceback): |
| Solver.current = None |
| |
| def supportsMinisat(self): |
| return _lib.vc_supportsMinisat(self.vc) |
| |
| def useMinisat(self): |
| return _lib.vc_useMinisat(self.vc) |
| |
| def isUsingMinisat(self): |
| return _lib.vc_isUsingMinisat(self.vc) |
| |
| def supportsSimplifyingMinisat(self): |
| return _lib.vc_supportsSimplifyingMinisat(self.vc) |
| |
| def useSimplifyingMinisat(self): |
| return _lib.vc_useSimplifyingMinisat(self.vc) |
| |
| def isUsingSimplifyingMinisat(self): |
| return _lib.vc_isUsingSimplifyingMinisat(self.vc) |
| |
| def supportsCryptominisat(self): |
| return _lib.vc_supportsCryptominisat(self.vc) |
| |
| def useCryptominisat(self): |
| return _lib.vc_useCryptominisat(self.vc) |
| |
| def isUsingCryptominisat(self): |
| return _lib.vc_isUsingCryptominisat(self.vc) |
| |
| def supportsRiss(self): |
| return _lib.vc_supportsRiss(self.vc) |
| |
| def useRiss(self): |
| return _lib.vc_useRiss(self.vc) |
| |
| def isUsingRiss(self): |
| return _lib.vc_isUsingRiss(self.vc) |
| |
| def bitvec(self, name, width=32): |
| """Creates a new BitVector variable.""" |
| # TODO Sanitize the name or stp will segfault. |
| # TODO Perhaps cache these calls per width? |
| # TODO Please, please, fix this terrible Py3 support. |
| name_conv = bytes(name, 'utf8') if Py3 else name |
| |
| bv_type = _lib.vc_bvType(self.vc, width) |
| self.keys[name] = _lib.vc_varExpr(self.vc, name_conv, bv_type) |
| return Expr(self, width, self.keys[name], name=name) |
| |
| def bitvecs(self, names, width=32): |
| """Creates one or more BitVectors variables.""" |
| return [self.bitvec(name, width) for name in names.split()] |
| |
| def bitvecval(self, width, value): |
| """Creates a new BitVector with a constant value.""" |
| expr = _lib.vc_bvConstExprFromLL(self.vc, width, value) |
| return Expr(self, width, expr) |
| |
| def bitvecvalD(self, width, value): |
| """Creates a new BitVector with a constant value.""" |
| value_conv = bytes(value, 'utf8') if Py3 else value |
| |
| expr = _lib.vc_bvConstExprFromDecStr(self.vc, width, value_conv) |
| return Expr(self, width, expr) |
| |
| def true(self): |
| """Creates a True boolean.""" |
| return Expr(self, None, _lib.vc_trueExpr(self.vc)) |
| |
| def false(self): |
| """Creates a False boolean.""" |
| return Expr(self, None, _lib.vc_falseExpr(self.vc)) |
| |
| def add(self, *exprs): |
| """Adds one or more constraint(s) to STP.""" |
| for expr in exprs: |
| assert isinstance(expr, Expr), 'Formula should be an Expression' |
| _lib.vc_assertFormula(self.vc, expr.expr) |
| |
| def push(self): |
| """Enter a new frame.""" |
| _lib.vc_push(self.vc) |
| |
| def pop(self): |
| """Leave the current frame.""" |
| _lib.vc_pop(self.vc) |
| |
| def _n_exprs(self, *exprs): |
| """Creates an array of Expressions to be used in the C API.""" |
| for expr in exprs: |
| assert isinstance(expr, Expr), 'Object should be an Expression' |
| |
| # This may not be very clean, but I'm not sure if there are |
| # better ways to achieve this goal. |
| exprs = [expr.expr for expr in exprs] |
| exprs = (_Expr * len(exprs))(*exprs) |
| return exprs, len(exprs) |
| |
| def check_with_timeout(self, *exprs, **kwargs): |
| """Check whether the various expressions are satisfiable.""" |
| |
| _, length = self._n_exprs(*exprs) |
| if (length > 0): |
| expr = self.and_(*exprs) |
| expr = _lib.vc_notExpr(self.vc, expr.expr) |
| else: |
| expr = self.false().expr |
| |
| max_conflicts = kwargs.get("max_conflicts", -1) |
| max_time = kwargs.get("max_time", -1) |
| |
| self.push() |
| ret = _lib.vc_query_with_timeout(self.vc, expr, max_conflicts, max_time) |
| self.pop() |
| return ret |
| |
| def check(self, *exprs): |
| ret = self.check_with_timeout(*exprs, max_conflicts=-1, max_time=-1) |
| assert ret == 0 or ret == 1, 'Error querying your input' |
| return not ret |
| |
| def model(self, key=None, expr=None): |
| """ |
| Returns the value for an expression (or a name), or a model for the |
| entire counterexample otherwise. |
| |
| Args: |
| key (str): to look up a value by name |
| expr (Expr): to look up a value by expression |
| |
| Returns: |
| long (if expr or key is specified): the counterexample for the |
| expression or key |
| |
| dict (if no expr or key): the counterexample model for all named |
| keys |
| """ |
| |
| if expr and isinstance(expr, Expr): |
| # |
| # If we have an expression, and it is a _wrapped_ expression, we |
| # need to unbox it |
| # |
| expr = expr.expr |
| elif not expr and key is not None: |
| # |
| # If have no expression, but we have a key, then look-up based on |
| # keys (values stored in `self.keys) is already unboxed |
| # |
| expr = self.keys[key] |
| |
| if expr: |
| value = _lib.vc_getCounterExample(self.vc, expr) |
| return _lib.getBVUnsignedLongLong(value) |
| |
| # |
| # If no expression, return a model giving values to simple bitvectors |
| # (but not, e.g., arrays) |
| # |
| return dict((k, self.model(k)) for k in self.keys) |
| |
| # Allows easy access to the Counter Example. |
| __getitem__ = model |
| |
| def and_(self, *exprs): |
| exprs, length = self._n_exprs(*exprs) |
| expr = _lib.vc_andExprN(self.vc, exprs, length) |
| return Expr(self, None, expr) |
| |
| def or_(self, *exprs): |
| exprs, length = self._n_exprs(*exprs) |
| expr = _lib.vc_orExprN(self.vc, exprs, length) |
| return Expr(self, None, expr) |
| |
| def xor(self, a, b): |
| assert isinstance(a, Expr), 'Object must be an Expression' |
| assert isinstance(b, Expr), 'Object must be an Expression' |
| expr = _lib.vc_xorExpr(self.vc, a.expr, b.expr) |
| return Expr(self, None, expr) |
| |
| def ite(self, a, b, c): |
| assert isinstance(a, Expr), 'Object must be an Expression' |
| assert isinstance(b, Expr), 'Object must be an Expression' |
| assert isinstance(c, Expr), 'Object must be an Expression' |
| assert b.width == c.width, 'Objects must have the same width' # compound expressions have width None or 0 |
| expr = _lib.vc_iteExpr(self.vc, a.expr, b.expr, c.expr) |
| return Expr(self, b.width, expr) |
| |
| def not_(self, obj): |
| assert isinstance(obj, Expr), 'Object should be an Expression' |
| expr = _lib.vc_notExpr(self.vc, obj.expr) |
| return Expr(self, obj.width, expr) |
| |
| |
| class Expr(object): |
| def __init__(self, s, width, expr, name=None): |
| self.s = s |
| self.width = width |
| self.expr = expr |
| self.name = name |
| |
| def __del__(self): |
| # TODO We're not quite there yet. |
| # _lib.vc_DeleteExpr(self.expr) |
| pass |
| |
| def _1(self, cb): |
| """Wrapper around single-expression STP functions.""" |
| expr = cb(self.s.vc, self.expr) |
| return Expr(self.s, self.width, expr) |
| |
| def _1w(self, cb): |
| """Wrapper around single-expression with width STP functions.""" |
| expr = cb(self.s.vc, self.width, self.expr) |
| return Expr(self.s, self.width, expr) |
| |
| def _toexpr(self, other): |
| if isinstance(other, (int, long)): |
| return self.s.bitvecval(self.width, other) |
| |
| if isinstance(other, bool): |
| return self.s.true() if other else self.s.false() |
| |
| return other |
| |
| def _2(self, cb, other): |
| """Wrapper around double-expression STP functions.""" |
| other = self._toexpr(other) |
| assert isinstance(other, Expr), 'Other object must be an Expr instance' |
| expr = cb(self.s.vc, self.expr, other.expr) |
| return Expr(self.s, self.width, expr) |
| |
| def _2w(self, cb, a, b): |
| """Wrapper around double-expression with width STP functions.""" |
| a, b = self._toexpr(a), self._toexpr(b) |
| assert isinstance(a, Expr), 'Left operand must be an Expr instance' |
| assert isinstance(b, Expr), 'Right operand must be an Expr instance' |
| assert self.width == a.width, 'Width must be equal' |
| assert self.width == b.width, 'Width must be equal' |
| expr = cb(self.s.vc, self.width, a.expr, b.expr) |
| return Expr(self.s, self.width, expr) |
| |
| def add(self, other): |
| return self._2w(_lib.vc_bvPlusExpr, self, other) |
| |
| __add__ = add |
| __radd__ = add |
| |
| def sub(self, other): |
| return self._2w(_lib.vc_bvMinusExpr, self, other) |
| |
| __sub__ = sub |
| |
| def rsub(self, other): |
| return self._2w(_lib.vc_bvMinusExpr, other, self) |
| |
| __rsub__ = rsub |
| |
| def mul(self, other): |
| return self._2w(_lib.vc_bvMultExpr, self, other) |
| |
| __mul__ = mul |
| __rmul__ = mul |
| |
| def div(self, other): |
| return self._2w(_lib.vc_bvDivExpr, self, other) |
| |
| __div__ = div |
| __floordiv__ = div |
| |
| def rdiv(self, other): |
| return self._2w(_lib.vc_bvDivExpr, other, self) |
| |
| __rdiv__ = rdiv |
| __rfloordiv__ = rdiv |
| |
| def mod(self, other): |
| return self._2w(_lib.vc_bvModExpr, self, other) |
| |
| __mod__ = mod |
| |
| def rmod(self, other): |
| return self._2w(_lib.vc_bvModExpr, other, self) |
| |
| __rmod__ = rmod |
| |
| def rem(self, other): |
| return self._2w(_lib.vc_bvRemExpr, self, other) |
| |
| def rrem(self, other): |
| return self._2w(_lib.vc_bvRemExpr, other, self) |
| |
| def sdiv(self, other): |
| return self._2w(_lib.vc_sbvDivExpr, self, other) |
| |
| def rsdiv(self, other): |
| return self._2w(_lib.vc_sbvDivExpr, other, self) |
| |
| def smod(self, other): |
| return self._2w(_lib.vc_sbvModExpr, self, other) |
| |
| def rsmod(self, other): |
| return self._2w(_lib.vc_sbvModExpr, other, self) |
| |
| def srem(self, other): |
| return self._2w(_lib.vc_sbvRemExpr, self, other) |
| |
| def rsrem(self, other): |
| return self._2w(_lib.vc_sbvRemExpr, other, self) |
| |
| def eq(self, other): |
| return self._2(_lib.vc_eqExpr, other) |
| |
| __eq__ = eq |
| |
| def ne(self, other): |
| return self.s.not_(self.eq(other)) |
| |
| __ne__ = ne |
| |
| def lt(self, other): |
| return self._2(_lib.vc_bvLtExpr, other) |
| |
| __lt__ = lt |
| |
| def le(self, other): |
| return self._2(_lib.vc_bvLeExpr, other) |
| |
| __le__ = le |
| |
| def gt(self, other): |
| return self._2(_lib.vc_bvGtExpr, other) |
| |
| __gt__ = gt |
| |
| def ge(self, other): |
| return self._2(_lib.vc_bvGeExpr, other) |
| |
| __ge__ = ge |
| |
| def slt(self, other): |
| return self._2(_lib.vc_sbvLtExpr, other) |
| |
| def sle(self, other): |
| return self._2(_lib.vc_sbvLeExpr, other) |
| |
| def sgt(self, other): |
| return self._2(_lib.vc_sbvGtExpr, other) |
| |
| def sge(self, other): |
| return self._2(_lib.vc_sbvGeExpr, other) |
| |
| def and_(self, other): |
| return self._2(_lib.vc_bvAndExpr, other) |
| |
| __and__ = and_ |
| __rand__ = and_ |
| |
| def or_(self, other): |
| return self._2(_lib.vc_bvOrExpr, other) |
| |
| __or__ = or_ |
| __ror__ = or_ |
| |
| def xor(self, other): |
| return self._2(_lib.vc_bvXorExpr, other) |
| |
| __xor__ = xor |
| __rxor__ = xor |
| |
| def neg(self): |
| return self._1(_lib.vc_bvUMinusExpr) |
| |
| __neg__ = neg |
| |
| def __pos__(self): |
| return self |
| |
| def not_(self): |
| return self._1(_lib.vc_bvNotExpr) |
| |
| __invert__ = not_ |
| |
| def shl(self, other): |
| return self._2w(_lib.vc_bvLeftShiftExprExpr, self, other) |
| |
| __lshift__ = shl |
| |
| def rshl(self, other): |
| return self._2w(_lib.vc_bvLeftShiftExprExpr, other, self) |
| |
| __rlshift__ = rshl |
| |
| def shr(self, other): |
| return self._2w(_lib.vc_bvRightShiftExprExpr, self, other) |
| |
| __rshift__ = shr |
| |
| def rshr(self, other): |
| return self._2w(_lib.vc_bvRightShiftExprExpr, other, self) |
| |
| __rrshift__ = rshr |
| |
| def sar(self, other): |
| return self._2w(_lib.vc_bvSignedRightShiftExprExpr, self, other) |
| |
| def rsar(self, other): |
| return self._2w(_lib.vc_bvSignedRightShiftExprExpr, other, self) |
| |
| def extract(self, high, low): |
| expr = _lib.vc_bvExtract(self.s.vc, self.expr, high, low) |
| return Expr(self.s, self.width, expr) |
| |
| def simplify(self): |
| """Simplify an expression.""" |
| expr = _lib.vc_simplify(self.s.vc, self.expr) |
| return Expr(self.s, self.width, expr) |
| |
| @property |
| def value(self): |
| """Returns the value of this BitVec in the current model.""" |
| return self.s.model(expr=self) |
| |
| |
| class ASTtoSTP(ast.NodeVisitor): |
| def __init__(self, s, count, *args, **kwargs): |
| ast.NodeVisitor.__init__(self) |
| self.s = s |
| self.count = count |
| self.inside = False |
| self.func_name = None |
| self.bitvecs = {} |
| self.exprs = [] |
| self.returned = None |
| self.args = args |
| self.kwargs = kwargs |
| |
| def _super(self, node): |
| return super(ASTtoSTP, self).generic_visit(node) |
| |
| visit_Module = _super |
| |
| def visit_FunctionDef(self, node): |
| assert node.args.vararg is None and node.args.kwarg is None, \ |
| 'Variable and Keyword arguments are not allowed' |
| |
| if self.inside: |
| raise Exception('Nested functions are not allowed') |
| |
| self.inside = True |
| self.func_name = node.name |
| |
| for idx, arg in enumerate(node.args.args): |
| arg = arg.arg if Py3 else arg.id |
| name = '%s_%d_%s' % (self.func_name, self.count, arg) |
| if idx < len(self.args): |
| self.bitvecs[name] = self.args[idx] |
| continue |
| |
| if arg in self.kwargs: |
| self.bitvecs[name] = self.kwargs[arg] |
| continue |
| |
| width = 32 |
| if idx < len(node.args.defaults): |
| width = node.args.defaults[idx] |
| |
| self.bitvecs[name] = self.s.bitvec(name, width=width) |
| |
| for row in node.body: |
| self.visit(row) |
| |
| def visit_Num(self, node): |
| return node.n |
| |
| def visit_BoolOp(self, node): |
| ops = { |
| ast.And: self.s.and_, |
| ast.Or: self.s.or_, |
| } |
| x = self.visit(node.values[0]) |
| y = self.visit(node.values[1]) |
| return ops[node.op.__class__](x, y) |
| |
| def visit_BinOp(self, node): |
| ops = { |
| ast.Add: lambda x, y: x + y, |
| ast.Sub: lambda x, y: x - y, |
| ast.Mult: lambda x, y: x * y, |
| ast.Div: lambda x, y: x / y, |
| ast.Mod: lambda x, y: x % y, |
| ast.LShift: lambda x, y: x << y, |
| ast.RShift: lambda x, y: x >> y, |
| ast.BitOr: lambda x, y: x | y, |
| ast.BitXor: lambda x, y: x ^ y, |
| ast.BitAnd: lambda x, y: x & y, |
| } |
| x = self.visit(node.left) |
| y = self.visit(node.right) |
| return ops[node.op.__class__](x, y) |
| |
| def visit_Compare(self, node): |
| assert len(node.ops) == 1, 'TODO Support multiple comparison ops' |
| |
| cmps = { |
| ast.Eq: lambda x, y: x == y, |
| ast.NotEq: lambda x, y: x != y, |
| ast.Lt: lambda x, y: x < y, |
| ast.LtE: lambda x, y: x <= y, |
| ast.Gt: lambda x, y: x > y, |
| ast.GtE: lambda x, y: x >= y, |
| ast.Is: lambda x, y: x == y, |
| ast.IsNot: lambda x, y: x != y, |
| } |
| |
| x = self.visit(node.left) |
| y = self.visit(node.comparators[0]) |
| return cmps[node.ops[0].__class__](x, y) |
| |
| def visit_Name(self, node): |
| if isinstance(node.ctx, ast.Load): |
| name = '%s_%d_%s' % (self.func_name, self.count, node.id) |
| return self.bitvecs[name] |
| |
| raise |
| |
| def visit_Assert(self, node): |
| self.exprs.append(self.visit(node.test)) |
| |
| def visit_Return(self, node): |
| self.returned = self.visit(node.value) |
| |
| def generic_visit(self, node): |
| raise Exception(node.__class__.__name__ + ' is not yet supported!') |
| |
| |
| def _eval_ast(root, *args, **kwargs): |
| s = Solver.current |
| node = ASTtoSTP(s, root.count-1, *args, **kwargs) |
| node.visit(root) |
| if node.exprs: |
| s.add(*node.exprs) |
| return node.returned |
| |
| |
| def stp(f): |
| try: |
| src = inspect.getsource(f) |
| except IOError: |
| raise Exception( |
| 'It is only possible to use the @stp decorator when the ' |
| 'function is stored in a source file. It does *not* work ' |
| 'directly from the Python interpreter.') |
| |
| node = ast.parse(src) |
| node.count = 0 |
| |
| def h(*args, **kwargs): |
| node.count += 1 |
| return _eval_ast(node, *args, **kwargs) |
| |
| return h |
| |
| |
| def add(*args, **kwargs): |
| return Solver.current.add(*args, **kwargs) |
| |
| |
| def bitvec(*args, **kwargs): |
| return Solver.current.bitvec(*args, **kwargs) |
| |
| |
| def bitvecs(*args, **kwargs): |
| return Solver.current.bitvecs(*args, **kwargs) |
| |
| |
| def check(*args, **kwargs): |
| return Solver.current.check(*args, **kwargs) |
| |
| |
| def model(*args, **kwargs): |
| return Solver.current.model(*args, **kwargs) |
| |
| def get_git_version_sha(): |
| return _lib.get_git_version_sha() |
| |
| def get_git_version_tag(): |
| return _lib.get_git_version_tag() |
| |
| def get_compilation_env(): |
| return _lib.get_compilation_env() |
| |
| def get_lib(): |
| # |
| # Helper function to expose STP's CDLL object -- this allows for API-based |
| # access to STP's API without going via the `Solver` class. |
| # |
| # There are some calls (e.g., vc_bvConcatExpr) that exist inside of the |
| # `_lib` object, but which do not exist inside of `Solver`. |
| # |
| # Directly exposing `_lib_ allows for access to these routines in the API. |
| # |
| return _lib |
| |
| # EOF |
