diff --git a/manticore/core/smtlib/constraints.py b/manticore/core/smtlib/constraints.py index 533ad4ed7..ba7aae9e1 100644 --- a/manticore/core/smtlib/constraints.py +++ b/manticore/core/smtlib/constraints.py @@ -93,7 +93,7 @@ def add(self, constraint) -> None: :param constraint: The constraint to add to the set. """ if isinstance(constraint, bool): - constraint = BoolConstant(constraint) + constraint = BoolConstant(value=constraint) assert isinstance(constraint, Bool) constraint = simplify(constraint) # If self._child is not None this constraint set has been forked and a @@ -380,8 +380,7 @@ def new_bool(self, name=None, taint=frozenset(), avoid_collisions=False): name = self._make_unique_name(name) if not avoid_collisions and name in self._declarations: raise ValueError(f"Name {name} already used") - var = BoolVariable(name, taint=taint) - return self._declare(var) + return self._declare(BoolVariable(name=name, taint=taint)) def new_bitvec(self, size, name=None, taint=frozenset(), avoid_collisions=False): """Declares a free symbolic bitvector in the constraint store @@ -400,8 +399,7 @@ def new_bitvec(self, size, name=None, taint=frozenset(), avoid_collisions=False) name = self._make_unique_name(name) if not avoid_collisions and name in self._declarations: raise ValueError(f"Name {name} already used") - var = BitVecVariable(size, name, taint=taint) - return self._declare(var) + return self._declare(BitVecVariable(size=size, name=name, taint=taint)) def new_array( self, @@ -430,5 +428,15 @@ def new_array( name = self._make_unique_name(name) if not avoid_collisions and name in self._declarations: raise ValueError(f"Name {name} already used") - var = self._declare(ArrayVariable(index_bits, index_max, value_bits, name, taint=taint)) - return ArrayProxy(var, default=default) + return ArrayProxy( + array=self._declare( + ArrayVariable( + index_bits=index_bits, + index_max=index_max, + value_bits=value_bits, + name=name, + taint=taint, + ) + ), + default=default, + ) diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py index 009910b9d..df607e567 100644 --- a/manticore/core/smtlib/expression.py +++ b/manticore/core/smtlib/expression.py @@ -69,7 +69,7 @@ class Expression(object, metaclass=XSlotted, abstract=True): __xslots__: Tuple[str, ...] = ("_taint",) - def __init__(self, taint: Union[tuple, frozenset] = ()): + def __init__(self, *, taint: Union[tuple, frozenset] = (), **kwargs): if self.__class__ is Expression: raise TypeError super().__init__() @@ -146,14 +146,14 @@ def taint_with(arg, *taints, value_bits=256, index_bits=256): tainted_fset = frozenset(tuple(taints)) if not issymbolic(arg): if isinstance(arg, int): - arg = BitVecConstant(value_bits, arg) + arg = BitVecConstant(size=value_bits, value=arg) arg._taint = tainted_fset else: raise ValueError("type not supported") else: if isinstance(arg, BitVecVariable): - arg = arg + BitVecConstant(value_bits, 0, taint=tainted_fset) + arg = arg + BitVecConstant(size=value_bits, value=0, taint=tainted_fset) else: arg = copy.copy(arg) arg._taint |= tainted_fset @@ -166,46 +166,46 @@ def taint_with(arg, *taints, value_bits=256, index_bits=256): class Bool(Expression, abstract=True): """Bool expressions represent symbolic value of truth""" - def __init__(self, *operands, **kwargs): - super().__init__(*operands, **kwargs) + def __init__(self, *args, **kwargs): + super().__init__(**kwargs) def cast(self, value: Union["Bool", int, bool], **kwargs) -> Union["BoolConstant", "Bool"]: if isinstance(value, Bool): return value - return BoolConstant(bool(value), **kwargs) + return BoolConstant(value=bool(value), **kwargs) def __cmp__(self, *args): raise NotImplementedError("CMP for Bool") def __invert__(self): - return BoolNot(self) + return BoolNot(value=self) def __eq__(self, other): - return BoolEqual(self, self.cast(other)) + return BoolEqual(a=self, b=self.cast(other)) def __hash__(self): return object.__hash__(self) def __ne__(self, other): - return BoolNot(self == self.cast(other)) + return BoolNot(value=self == self.cast(other)) def __and__(self, other): - return BoolAnd(self, self.cast(other)) + return BoolAnd(a=self, b=self.cast(other)) def __or__(self, other): - return BoolOr(self, self.cast(other)) + return BoolOr(a=self, b=self.cast(other)) def __xor__(self, other): - return BoolXor(self, self.cast(other)) + return BoolXor(a=self, b=self.cast(other)) def __rand__(self, other): - return BoolAnd(self.cast(other), self) + return BoolAnd(a=self.cast(other), b=self) def __ror__(self, other): - return BoolOr(self.cast(other), self) + return BoolOr(a=self.cast(other), b=self) def __rxor__(self, other): - return BoolXor(self.cast(other), self) + return BoolXor(a=self.cast(other), b=self) def __bool__(self): # try to be forgiving. Allow user to use Bool in an IF sometimes @@ -220,9 +220,9 @@ def __bool__(self): class BoolVariable(Bool): __xslots__: Tuple[str, ...] = ("_name",) - def __init__(self, name: str, *args, **kwargs): + def __init__(self, *, name: str, **kwargs): assert " " not in name - super().__init__(*args, **kwargs) + super().__init__(**kwargs) self._name = name @property @@ -246,8 +246,8 @@ def declaration(self): class BoolConstant(Bool): __xslots__: Tuple[str, ...] = ("_value",) - def __init__(self, value: bool, *args, **kwargs): - super().__init__(*args, **kwargs) + def __init__(self, *, value: bool, **kwargs): + super().__init__(**kwargs) self._value = value def __bool__(self): @@ -263,7 +263,7 @@ class BoolOperation(Bool, abstract=True): __xslots__: Tuple[str, ...] = ("_operands",) - def __init__(self, *operands, **kwargs): + def __init__(self, *, operands: Tuple, **kwargs): self._operands = operands # If taint was not forced by a keyword argument, calculate default @@ -277,28 +277,28 @@ def operands(self): class BoolNot(BoolOperation): - def __init__(self, value, **kwargs): - super().__init__(value, **kwargs) + def __init__(self, *, value, **kwargs): + super().__init__(operands=(value,), **kwargs) class BoolAnd(BoolOperation): - def __init__(self, a, b, **kwargs): - super().__init__(a, b, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(operands=(a, b), **kwargs) class BoolOr(BoolOperation): - def __init__(self, a: "Bool", b: "Bool", **kwargs): - super().__init__(a, b, **kwargs) + def __init__(self, *, a: "Bool", b: "Bool", **kwargs): + super().__init__(operands=(a, b), **kwargs) class BoolXor(BoolOperation): - def __init__(self, a, b, **kwargs): - super().__init__(a, b, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(operands=(a, b), **kwargs) class BoolITE(BoolOperation): - def __init__(self, cond: "Bool", true: "Bool", false: "Bool", **kwargs): - super().__init__(cond, true, false, **kwargs) + def __init__(self, *, cond: "Bool", true: "Bool", false: "Bool", **kwargs): + super().__init__(operands=(cond, true, false), **kwargs) class BitVec(Expression, abstract=True): @@ -306,8 +306,8 @@ class BitVec(Expression, abstract=True): __xslots__: Tuple[str, ...] = ("size",) - def __init__(self, size, *operands, **kwargs): - super().__init__(*operands, **kwargs) + def __init__(self, *, size, **kwargs): + super().__init__(**kwargs) self.size = size @property @@ -330,37 +330,37 @@ def cast( if not isinstance(value, int): value = int(value) # FIXME? Assert it fits in the representation - return BitVecConstant(self.size, value, **kwargs) + return BitVecConstant(size=self.size, value=value, **kwargs) def __add__(self, other): - return BitVecAdd(self, self.cast(other)) + return BitVecAdd(a=self, b=self.cast(other)) def __sub__(self, other): - return BitVecSub(self, self.cast(other)) + return BitVecSub(a=self, b=self.cast(other)) def __mul__(self, other): - return BitVecMul(self, self.cast(other)) + return BitVecMul(a=self, b=self.cast(other)) def __mod__(self, other): - return BitVecMod(self, self.cast(other)) + return BitVecMod(a=self, b=self.cast(other)) # object.__divmod__(self, other) # object.__pow__(self, other[, modulo]) def __lshift__(self, other): - return BitVecShiftLeft(self, self.cast(other)) + return BitVecShiftLeft(a=self, b=self.cast(other)) def __rshift__(self, other): - return BitVecShiftRight(self, self.cast(other)) + return BitVecShiftRight(a=self, b=self.cast(other)) def __and__(self, other): - return BitVecAnd(self, self.cast(other)) + return BitVecAnd(a=self, b=self.cast(other)) def __xor__(self, other): - return BitVecXor(self, self.cast(other)) + return BitVecXor(a=self, b=self.cast(other)) def __or__(self, other): - return BitVecOr(self, self.cast(other)) + return BitVecOr(a=self, b=self.cast(other)) # The division operator (/) is implemented by these methods. The # __truediv__() method is used when __future__.division is in effect, @@ -369,10 +369,10 @@ def __or__(self, other): # TypeError will be raised instead. def __div__(self, other): - return BitVecDiv(self, self.cast(other)) + return BitVecDiv(a=self, b=self.cast(other)) def __truediv__(self, other): - return BitVecDiv(self, self.cast(other)) + return BitVecDiv(a=self, b=self.cast(other)) def __floordiv__(self, other): return self / other @@ -386,43 +386,43 @@ def __floordiv__(self, other): # y.__rsub__(x) is called if x.__sub__(y) returns NotImplemented. def __radd__(self, other): - return BitVecAdd(self.cast(other), self) + return BitVecAdd(a=self.cast(other), b=self) def __rsub__(self, other): - return BitVecSub(self.cast(other), self) + return BitVecSub(a=self.cast(other), b=self) def __rmul__(self, other): - return BitVecMul(self.cast(other), self) + return BitVecMul(a=self.cast(other), b=self) def __rmod__(self, other): - return BitVecMod(self.cast(other), self) + return BitVecMod(a=self.cast(other), b=self) def __rtruediv__(self, other): - return BitVecDiv(self.cast(other), self) + return BitVecDiv(a=self.cast(other), b=self) def __rdiv__(self, other): - return BitVecDiv(self.cast(other), self) + return BitVecDiv(a=self.cast(other), b=self) # object.__rdivmod__(self, other) # object.__rpow__(self, other) def __rlshift__(self, other): - return BitVecShiftLeft(self.cast(other), self) + return BitVecShiftLeft(a=self.cast(other), b=self) def __rrshift__(self, other): - return BitVecShiftRight(self.cast(other), self) + return BitVecShiftRight(a=self.cast(other), b=self) def __rand__(self, other): - return BitVecAnd(self.cast(other), self) + return BitVecAnd(a=self.cast(other), b=self) def __rxor__(self, other): - return BitVecXor(self.cast(other), self) + return BitVecXor(a=self.cast(other), b=self) def __ror__(self, other): - return BitVecOr(self.cast(other), self) + return BitVecOr(a=self.cast(other), b=self) def __invert__(self): - return BitVecXor(self, self.cast(self.mask)) + return BitVecXor(a=self, b=self.cast(self.mask)) # These are the so-called "rich comparison" methods, and are called # for comparison operators in preference to __cmp__() below. The @@ -436,71 +436,71 @@ def __invert__(self): # x>=y calls x.__ge__(y). def __lt__(self, other): - return LessThan(self, self.cast(other)) + return LessThan(a=self, b=self.cast(other)) def __le__(self, other): - return LessOrEqual(self, self.cast(other)) + return LessOrEqual(a=self, b=self.cast(other)) def __eq__(self, other): - return BoolEqual(self, self.cast(other)) + return BoolEqual(a=self, b=self.cast(other)) def __hash__(self): return object.__hash__(self) def __ne__(self, other): - return BoolNot(BoolEqual(self, self.cast(other))) + return BoolNot(value=BoolEqual(a=self, b=self.cast(other))) def __gt__(self, other): - return GreaterThan(self, self.cast(other)) + return GreaterThan(a=self, b=self.cast(other)) def __ge__(self, other): - return GreaterOrEqual(self, self.cast(other)) + return GreaterOrEqual(a=self, b=self.cast(other)) def __neg__(self): - return BitVecNeg(self) + return BitVecNeg(a=self) # Unsigned comparisons def ugt(self, other): - return UnsignedGreaterThan(self, self.cast(other)) + return UnsignedGreaterThan(a=self, b=self.cast(other)) def uge(self, other): - return UnsignedGreaterOrEqual(self, self.cast(other)) + return UnsignedGreaterOrEqual(a=self, b=self.cast(other)) def ult(self, other): - return UnsignedLessThan(self, self.cast(other)) + return UnsignedLessThan(a=self, b=self.cast(other)) def ule(self, other): - return UnsignedLessOrEqual(self, self.cast(other)) + return UnsignedLessOrEqual(a=self, b=self.cast(other)) def udiv(self, other): - return BitVecUnsignedDiv(self, self.cast(other)) + return BitVecUnsignedDiv(a=self, b=self.cast(other)) def rudiv(self, other): - return BitVecUnsignedDiv(self.cast(other), self) + return BitVecUnsignedDiv(a=self.cast(other), b=self) def sdiv(self, other): - return BitVecDiv(self, self.cast(other)) + return BitVecDiv(a=self, b=self.cast(other)) def rsdiv(self, other): - return BitVecDiv(self.cast(other), self) + return BitVecDiv(a=self.cast(other), b=self) def srem(self, other): - return BitVecRem(self, self.cast(other)) + return BitVecRem(a=self, b=self.cast(other)) def rsrem(self, other): - return BitVecRem(self.cast(other), self) + return BitVecRem(a=self.cast(other), b=self) def urem(self, other): - return BitVecUnsignedRem(self, self.cast(other)) + return BitVecUnsignedRem(a=self, b=self.cast(other)) def rurem(self, other): - return BitVecUnsignedRem(self.cast(other), self) + return BitVecUnsignedRem(a=self.cast(other), b=self) def sar(self, other): - return BitVecArithmeticShiftRight(self, self.cast(other)) + return BitVecArithmeticShiftRight(a=self, b=self.cast(other)) def sal(self, other): - return BitVecArithmeticShiftLeft(self, self.cast(other)) + return BitVecArithmeticShiftLeft(a=self, b=self.cast(other)) def Bool(self): return self != 0 @@ -509,9 +509,9 @@ def Bool(self): class BitVecVariable(BitVec): __xslots__: Tuple[str, ...] = ("_name",) - def __init__(self, size: int, name: str, *args, **kwargs): + def __init__(self, *, size: int, name: str, **kwargs): assert " " not in name - super().__init__(size, *args, **kwargs) + super().__init__(size=size, **kwargs) self._name = name @property @@ -535,10 +535,10 @@ def declaration(self): class BitVecConstant(BitVec): __xslots__: Tuple[str, ...] = ("_value",) - def __init__(self, size: int, value: int, *args, **kwargs): + def __init__(self, *, size: int, value: int, **kwargs): MASK = (1 << size) - 1 self._value = value & MASK - super().__init__(size, *args, **kwargs) + super().__init__(size=size, **kwargs) def __bool__(self): return self.value != 0 @@ -568,13 +568,13 @@ class BitVecOperation(BitVec, abstract=True): __xslots__: Tuple[str, ...] = ("_operands",) - def __init__(self, size, *operands, **kwargs): + def __init__(self, *, size, operands: Tuple, **kwargs): self._operands = operands # If taint was not forced by a keyword argument, calculate default kwargs.setdefault("taint", reduce(lambda x, y: x.union(y.taint), operands, frozenset())) - super().__init__(size, **kwargs) + super().__init__(size=size, **kwargs) @property def operands(self): @@ -582,143 +582,143 @@ def operands(self): class BitVecAdd(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecSub(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecMul(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecDiv(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecUnsignedDiv(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecMod(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecRem(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecUnsignedRem(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecShiftLeft(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecShiftRight(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecArithmeticShiftLeft(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecArithmeticShiftRight(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecAnd(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecOr(BitVecOperation): - def __init__(self, a: BitVec, b: BitVec, *args, **kwargs): + def __init__(self, *, a: BitVec, b: BitVec, **kwargs): assert a.size == b.size - super().__init__(a.size, a, b, *args, **kwargs) + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecXor(BitVecOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a.size, a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(size=a.size, operands=(a, b), **kwargs) class BitVecNot(BitVecOperation): - def __init__(self, a, **kwargs): - super().__init__(a.size, a, **kwargs) + def __init__(self, *, a, **kwargs): + super().__init__(size=a.size, operands=(a,), **kwargs) class BitVecNeg(BitVecOperation): - def __init__(self, a, *args, **kwargs): - super().__init__(a.size, a, *args, **kwargs) + def __init__(self, *, a, **kwargs): + super().__init__(size=a.size, operands=(a,), **kwargs) # Comparing two bitvectors results in a Bool class LessThan(BoolOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(operands=(a, b), **kwargs) class LessOrEqual(BoolOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): + super().__init__(operands=(a, b), **kwargs) class BoolEqual(BoolOperation): - def __init__(self, a, b, *args, **kwargs): + def __init__(self, *, a, b, **kwargs): if isinstance(a, BitVec) or isinstance(b, BitVec): assert a.size == b.size - super().__init__(a, b, *args, **kwargs) + super().__init__(operands=(a, b), **kwargs) class GreaterThan(BoolOperation): - def __init__(self, a, b, *args, **kwargs): + def __init__(self, *, a, b, **kwargs): assert a.size == b.size - super().__init__(a, b, *args, **kwargs) + super().__init__(operands=(a, b), **kwargs) class GreaterOrEqual(BoolOperation): - def __init__(self, a, b, *args, **kwargs): + def __init__(self, *, a, b, **kwargs): assert a.size == b.size - super().__init__(a, b, *args, **kwargs) + super().__init__(operands=(a, b), **kwargs) class UnsignedLessThan(BoolOperation): - def __init__(self, a, b, *args, **kwargs): - super().__init__(a, b, *args, **kwargs) + def __init__(self, *, a, b, **kwargs): assert a.size == b.size + super().__init__(operands=(a, b), **kwargs) class UnsignedLessOrEqual(BoolOperation): - def __init__(self, a, b, *args, **kwargs): + def __init__(self, *, a, b, **kwargs): assert a.size == b.size - super().__init__(a, b, *args, **kwargs) + super().__init__(operands=(a, b), **kwargs) class UnsignedGreaterThan(BoolOperation): - def __init__(self, a, b, *args, **kwargs): + def __init__(self, *, a, b, **kwargs): assert a.size == b.size - super().__init__(a, b, *args, **kwargs) + super().__init__(operands=(a, b), **kwargs) class UnsignedGreaterOrEqual(BoolOperation): - def __init__(self, a, b, *args, **kwargs): + def __init__(self, *, a, b, **kwargs): assert a.size == b.size - super(UnsignedGreaterOrEqual, self).__init__(a, b, *args, **kwargs) + super(UnsignedGreaterOrEqual, self).__init__(operands=(a, b), **kwargs) ############################################################################### @@ -733,16 +733,14 @@ class Array(Expression, abstract=True): __xslots__: Tuple[str, ...] = ("_index_bits", "_index_max", "_value_bits") - def __init__( - self, index_bits: int, index_max: Optional[int], value_bits: int, *operands, **kwargs - ): + def __init__(self, *, index_bits: int, index_max: Optional[int], value_bits: int, **kwargs): assert index_bits in (32, 64, 256) assert value_bits in (8, 16, 32, 64, 256) assert index_max is None or index_max >= 0 and index_max < 2 ** index_bits self._index_bits = index_bits self._index_max = index_max self._value_bits = value_bits - super().__init__(*operands, **kwargs) + super().__init__(**kwargs) assert type(self) is not Array, "Abstract class" def _get_size(self, index): @@ -753,7 +751,7 @@ def _get_size(self, index): size = simplify(size) else: - size = BitVecConstant(self.index_bits, size) + size = BitVecConstant(size=self.index_bits, value=size) assert isinstance(size, BitVecConstant) return size.value @@ -772,7 +770,10 @@ def cast(self, possible_array): if isinstance(possible_array, bytearray): # FIXME This should be related to a constrainSet arr = ArrayVariable( - self.index_bits, len(possible_array), 8, "cast{}".format(uuid.uuid1()) + index_bits=self.index_bits, + index_max=len(possible_array), + value_bits=8, + name="cast{}".format(uuid.uuid1()), ) for pos, byte in enumerate(possible_array): arr = arr.store(pos, byte) @@ -782,7 +783,7 @@ def cast(self, possible_array): def cast_index(self, index: Union[int, "BitVec"]) -> Union["BitVecConstant", "BitVec"]: if isinstance(index, int): # assert self.index_max is None or index >= 0 and index < self.index_max - return BitVecConstant(self.index_bits, index) + return BitVecConstant(size=self.index_bits, value=index) assert index.size == self.index_bits return index @@ -796,7 +797,7 @@ def cast_value( value = ord(value) if not isinstance(value, int): value = int(value) - return BitVecConstant(self.value_bits, value) + return BitVecConstant(size=self.value_bits, value=value) def __len__(self): if self.index_max is None: @@ -817,10 +818,10 @@ def index_max(self): def select(self, index): index = self.cast_index(index) - return ArraySelect(self, index) + return ArraySelect(array=self, index=index) def store(self, index, value): - return ArrayStore(self, self.cast_index(index), self.cast_value(value)) + return ArrayStore(array=self, index=self.cast_index(index), value=self.cast_value(value)) def write(self, offset, buf): if not isinstance(buf, (Array, bytearray)): @@ -831,13 +832,13 @@ def write(self, offset, buf): return arr def read(self, offset, size): - return ArraySlice(self, offset, size) + return ArraySlice(array=self, offset=offset, size=size) def __getitem__(self, index): if isinstance(index, slice): start, stop = self._fix_index(index) size = self._get_size(index) - return ArraySlice(self, start, size) + return ArraySlice(array=self, offset=start, size=size) else: if self.index_max is not None: if not isinstance(index, Expression) and index >= self.index_max: @@ -852,18 +853,18 @@ def __eq__(self, other): # FIXME taint def compare_buffers(a, b): if len(a) != len(b): - return BoolConstant(False) - cond = BoolConstant(True) + return BoolConstant(value=False) + cond = BoolConstant(value=True) for i in range(len(a)): - cond = BoolAnd(cond.cast(a[i] == b[i]), cond) - if cond is BoolConstant(False): - return BoolConstant(False) + cond = BoolAnd(a=cond.cast(a[i] == b[i]), b=cond) + if cond is BoolConstant(value=False): + return BoolConstant(value=False) return cond return compare_buffers(self, other) def __ne__(self, other): - return BoolNot(self == other) + return BoolNot(value=self == other) def __hash__(self): return super().__hash__() @@ -880,34 +881,42 @@ def read_BE(self, address, size): bytes = [] for offset in range(size): bytes.append(self.get(address + offset, 0)) - return BitVecConcat(size * self.value_bits, tuple(bytes)) + return BitVecConcat(size_dest=size * self.value_bits, operands=tuple(bytes)) def read_LE(self, address, size): address = self.cast_index(address) bytes = [] for offset in range(size): bytes.append(self.get(address + offset, 0)) - return BitVecConcat(size * self.value_bits, tuple(reversed(bytes))) + return BitVecConcat(size_dest=size * self.value_bits, operands=tuple(reversed(bytes))) def write_BE(self, address, value, size): address = self.cast_index(address) - value = BitVecConstant(size * self.value_bits, value=0).cast(value) + value = BitVecConstant(size=size * self.value_bits, value=0).cast(value) array = self for offset in range(size): array = array.store( address + offset, - BitVecExtract(value, (size - 1 - offset) * self.value_bits, self.value_bits), + BitVecExtract( + operand=value, + offset=(size - 1 - offset) * self.value_bits, + size=self.value_bits, + ), ) return array def write_LE(self, address, value, size): address = self.cast_index(address) - value = BitVecConstant(size * self.value_bits, value=0).cast(value) + value = BitVecConstant(size=size * self.value_bits, value=0).cast(value) array = self for offset in reversed(range(size)): array = array.store( address + offset, - BitVecExtract(value, (size - 1 - offset) * self.value_bits, self.value_bits), + BitVecExtract( + operand=value, + offset=(size - 1 - offset) * self.value_bits, + size=self.value_bits, + ), ) return array @@ -922,11 +931,11 @@ def __add__(self, other): # FIXME This should be related to a constrainSet new_arr = ArrayProxy( - ArrayVariable( - self.index_bits, - self.index_max + len(other), - self.value_bits, - "concatenation{}".format(uuid.uuid1()), + array=ArrayVariable( + index_bits=self.index_bits, + index_max=self.index_max + len(other), + value_bits=self.value_bits, + name="concatenation{}".format(uuid.uuid1()), ) ) for index in range(self.index_max): @@ -946,11 +955,11 @@ def __radd__(self, other): # FIXME This should be related to a constrainSet new_arr = ArrayProxy( - ArrayVariable( - self.index_bits, - self.index_max + len(other), - self.value_bits, - "concatenation{}".format(uuid.uuid1()), + array=ArrayVariable( + index_bits=self.index_bits, + index_max=self.index_max + len(other), + value_bits=self.value_bits, + name="concatenation{}".format(uuid.uuid1()), ) ) for index in range(len(other)): @@ -965,9 +974,11 @@ def __radd__(self, other): class ArrayVariable(Array): __xslots__: Tuple[str, ...] = ("_name",) - def __init__(self, index_bits, index_max, value_bits, name, *args, **kwargs): + def __init__(self, *, index_bits, index_max, value_bits, name, **kwargs): assert " " not in name - super().__init__(index_bits, index_max, value_bits, *args, **kwargs) + super().__init__( + index_bits=index_bits, index_max=index_max, value_bits=value_bits, **kwargs + ) self._name = name @property @@ -993,13 +1004,18 @@ class ArrayOperation(Array): __xslots__: Tuple[str, ...] = ("_operands",) - def __init__(self, array: Array, *operands, **kwargs): + def __init__(self, *, array: Array, operands: Tuple, **kwargs): self._operands = (array, *operands) # If taint was not forced by a keyword argument, calculate default kwargs.setdefault("taint", reduce(lambda x, y: x.union(y.taint), operands, frozenset())) - super().__init__(array.index_bits, array.index_max, array.value_bits, **kwargs) + super().__init__( + index_bits=array.index_bits, + index_max=array.index_max, + value_bits=array.value_bits, + **kwargs, + ) @property def operands(self): @@ -1007,10 +1023,10 @@ def operands(self): class ArrayStore(ArrayOperation): - def __init__(self, array: "Array", index: "BitVec", value: "BitVec", *args, **kwargs): + def __init__(self, *, array: "Array", index: "BitVec", value: "BitVec", **kwargs): assert index.size == array.index_bits assert value.size == array.value_bits - super().__init__(array, index, value, *args, **kwargs) + super().__init__(array=array, operands=(index, value), **kwargs) @property def array(self): @@ -1037,6 +1053,7 @@ def __getstate__(self): array = array.array state["_array"] = array state["_items"] = items + state["_taint"] = self.taint return state def __setstate__(self, state): @@ -1046,6 +1063,7 @@ def __setstate__(self, state): self._index_bits = array.index_bits self._index_max = array.index_max self._value_bits = array.value_bits + self._taint = state["_taint"] index, value = state["_items"][0] self._operands = (array, index, value) @@ -1053,21 +1071,22 @@ def __setstate__(self, state): class ArraySlice(ArrayOperation): __xslots__: Tuple[str, ...] = ("_slice_offset", "_slice_size") - def __init__( - self, array: Union["Array", "ArrayProxy"], offset: int, size: int, *args, **kwargs - ): + def __init__(self, *, array: Union["Array", "ArrayProxy"], offset: int, size: int, **kwargs): if not isinstance(array, Array): raise ValueError("Array expected") if isinstance(array, ArrayProxy): array = array._array - super().__init__(array, **kwargs) + self._operands = (array,) + super().__init__( + array=array, operands=(self.cast_index(offset), self.cast_index(size)), **kwargs + ) self._slice_offset = offset self._slice_size = size @property def array(self): - return self.operands[0] + return self._operands[0] @property def underlying_variable(self): @@ -1090,9 +1109,9 @@ def select(self, index): def store(self, index, value): return ArraySlice( - self.array.store(index + self._slice_offset, value), - self._slice_offset, - self._slice_size, + array=self.array.store(index + self._slice_offset, value), + offset=self._slice_offset, + size=self._slice_size, ) @@ -1106,13 +1125,18 @@ class ArrayProxy(Array): "_name", ) - def __init__(self, array: Array, default: Optional[int] = None): + def __init__(self, *, array: Array, default: Optional[int] = None, **kwargs): self._default = default self._concrete_cache: Dict[int, int] = {} self._written = None if isinstance(array, ArrayProxy): # copy constructor - super().__init__(array.index_bits, array.index_max, array.value_bits) + super().__init__( + index_bits=array.index_bits, + index_max=array.index_max, + value_bits=array.value_bits, + **kwargs, + ) self._array: Array = array._array self._name: str = array._name if default is None: @@ -1121,12 +1145,22 @@ def __init__(self, array: Array, default: Optional[int] = None): self._written = set(array.written) elif isinstance(array, ArrayVariable): # fresh array proxy - super().__init__(array.index_bits, array.index_max, array.value_bits) + super().__init__( + index_bits=array.index_bits, + index_max=array.index_max, + value_bits=array.value_bits, + **kwargs, + ) self._array = array self._name = array.name else: # arrayproxy for a prepopulated array - super().__init__(array.index_bits, array.index_max, array.value_bits) + super().__init__( + index_bits=array.index_bits, + index_max=array.index_max, + value_bits=array.value_bits, + **kwargs, + ) self._name = array.underlying_variable.name self._array = array @@ -1189,7 +1223,9 @@ def __getitem__(self, index): if isinstance(index, slice): start, stop = self._fix_index(index) size = self._get_size(index) - array_proxy_slice = ArrayProxy(ArraySlice(self, start, size), default=self._default) + array_proxy_slice = ArrayProxy( + array=ArraySlice(array=self, offset=start, size=size), default=self._default + ) array_proxy_slice._concrete_cache = {} for k, v in self._concrete_cache.items(): if k >= start and k < start + size: @@ -1230,7 +1266,7 @@ def __setstate__(self, state): self._written = None def __copy__(self): - return ArrayProxy(self) + return ArrayProxy(array=self) @property def written(self): @@ -1254,24 +1290,24 @@ def written(self): def is_known(self, index): if isinstance(index, Constant) and index.value in self._concrete_cache: - return BoolConstant(True) + return BoolConstant(value=True) - is_known_index = BoolConstant(False) + is_known_index = BoolConstant(value=False) written = self.written if isinstance(index, Constant): for i in written: # check if the concrete index is explicitly in written if isinstance(i, Constant) and index.value == i.value: - return BoolConstant(True) + return BoolConstant(value=True) # Build an expression to check if our concrete index could be the # solution for anyof the used symbolic indexes - is_known_index = BoolOr(is_known_index.cast(index == i), is_known_index) + is_known_index = BoolOr(a=is_known_index.cast(index == i), b=is_known_index) return is_known_index # The index is symbolic we need to compare it agains it all for known_index in written: - is_known_index = BoolOr(is_known_index.cast(index == known_index), is_known_index) + is_known_index = BoolOr(a=is_known_index.cast(index == known_index), b=is_known_index) return is_known_index @@ -1284,7 +1320,12 @@ def get(self, index, default=None): from .visitors import simplify index = simplify( - BitVecITE(self.index_bits, index < 0, self.index_max + index + 1, index) + BitVecITE( + size=self.index_bits, + condition=index < 0, + true_value=self.index_max + index + 1, + false_value=index, + ) ) if isinstance(index, Constant) and index.value in self._concrete_cache: return self._concrete_cache[index.value] @@ -1298,28 +1339,31 @@ def get(self, index, default=None): return self._array.select(index) value = self._array.select(index) - return BitVecITE(self._array.value_bits, is_known, value, default) + return BitVecITE( + size=self._array.value_bits, condition=is_known, true_value=value, false_value=default + ) class ArraySelect(BitVec): __xslots__: Tuple[str, ...] = ("_operands",) - def __init__(self, array: "Array", index: "BitVec", *operands, **kwargs): + def __init__(self, *, array: "Array", index: "BitVec", **kwargs): + assert isinstance(array, Array) assert index.size == array.index_bits - self._operands = (array, index, *operands) + self._operands = (array, index) # If taint was not forced by a keyword argument, calculate default - kwargs.setdefault("taint", reduce(lambda x, y: x.union(y.taint), operands, frozenset())) + kwargs.setdefault("taint", frozenset({y for x in self._operands for y in x.taint})) - super().__init__(array.value_bits, **kwargs) + super().__init__(size=array.value_bits, **kwargs) @property def array(self): - return self.operands[0] + return self._operands[0] @property def index(self): - return self.operands[1] + return self._operands[1] @property def operands(self): @@ -1332,27 +1376,27 @@ def __repr__(self): class BitVecSignExtend(BitVecOperation): __xslots__: Tuple[str, ...] = ("extend",) - def __init__(self, operand: "BitVec", size_dest: int, *args, **kwargs): + def __init__(self, *, operand: "BitVec", size_dest: int, **kwargs): assert size_dest >= operand.size - super().__init__(size_dest, operand, *args, **kwargs) + super().__init__(size=size_dest, operands=(operand,), **kwargs) self.extend = size_dest - operand.size class BitVecZeroExtend(BitVecOperation): __xslots__: Tuple[str, ...] = ("extend",) - def __init__(self, size_dest: int, operand: "BitVec", *args, **kwargs): + def __init__(self, *, size_dest: int, operand: "BitVec", **kwargs): assert size_dest >= operand.size - super().__init__(size_dest, operand, *args, **kwargs) + super().__init__(size=size_dest, operands=(operand,), **kwargs) self.extend = size_dest - operand.size class BitVecExtract(BitVecOperation): __xslots__: Tuple[str, ...] = ("_begining", "_end") - def __init__(self, operand: "BitVec", offset: int, size: int, *args, **kwargs): + def __init__(self, *, operand: "BitVec", offset: int, size: int, **kwargs): assert offset >= 0 and offset + size <= operand.size - super().__init__(size, operand, *args, **kwargs) + super().__init__(size=size, operands=(operand,), **kwargs) self._begining = offset self._end = offset + size - 1 @@ -1370,25 +1414,25 @@ def end(self): class BitVecConcat(BitVecOperation): - def __init__(self, size_dest: int, operands: Tuple, **kwargs): + def __init__(self, *, size_dest: int, operands: Tuple, **kwargs): assert all(isinstance(x, BitVec) for x in operands) assert size_dest == sum(x.size for x in operands) - super().__init__(size_dest, *operands, **kwargs) + super().__init__(size=size_dest, operands=operands, **kwargs) class BitVecITE(BitVecOperation): def __init__( self, + *, size: int, condition: Union["Bool", bool], true_value: "BitVec", false_value: "BitVec", - *args, **kwargs, ): assert true_value.size == size assert false_value.size == size - super().__init__(size, condition, true_value, false_value, *args, **kwargs) + super().__init__(size=size, operands=(condition, true_value, false_value), **kwargs) @property def condition(self): diff --git a/manticore/core/smtlib/operators.py b/manticore/core/smtlib/operators.py index 79e2f0c61..5eb0f0e1e 100644 --- a/manticore/core/smtlib/operators.py +++ b/manticore/core/smtlib/operators.py @@ -19,7 +19,7 @@ def ORD(s): if s.size == 8: return s else: - return BitVecExtract(s, 0, 8) + return BitVecExtract(operand=s, offset=0, size=8) elif isinstance(s, int): return s & 0xFF else: @@ -31,7 +31,7 @@ def CHR(s): if s.size == 8: return s else: - return BitVecExtract(s, 0, 8) + return BitVecExtract(operand=s, offset=0, size=8) elif isinstance(s, int): return bytes([s & 0xFF]) else: @@ -125,11 +125,11 @@ def ULE(a, b): def EXTRACT(x, offset, size): if isinstance(x, BitVec) and isinstance(offset, BitVec): - return BitVecExtract(x >> offset, 0, size) + return BitVecExtract(operand=x >> offset, offset=0, size=size) elif isinstance(x, BitVec): if offset == 0 and size == x.size: return x - return BitVecExtract(x, offset, size) + return BitVecExtract(operand=x, offset=offset, size=size) else: return (x >> offset) & ((1 << size) - 1) @@ -140,7 +140,7 @@ def SEXTEND(x, size_src, size_dest): x -= 1 << size_src return x & ((1 << size_dest) - 1) assert x.size == size_src - return BitVecSignExtend(x, size_dest) + return BitVecSignExtend(operand=x, size_dest=size_dest) def ZEXTEND(x, size): @@ -148,7 +148,7 @@ def ZEXTEND(x, size): return x & ((1 << size) - 1) assert isinstance(x, BitVec) and size - x.size >= 0 if size - x.size > 0: - return BitVecZeroExtend(size, x) + return BitVecZeroExtend(size_dest=size, operand=x) else: return x @@ -160,10 +160,10 @@ def CONCAT(total_size, *args): def cast(x): if isinstance(x, int): - return BitVecConstant(arg_size, x) + return BitVecConstant(size=arg_size, value=x) return x - return BitVecConcat(total_size, tuple(map(cast, args))) + return BitVecConcat(size_dest=total_size, operands=tuple(map(cast, args))) else: return args[0] else: @@ -184,12 +184,12 @@ def ITE(cond, true_value, false_value): return false_value if isinstance(true_value, bool): - true_value = BoolConstant(true_value) + true_value = BoolConstant(value=true_value) if isinstance(false_value, bool): - false_value = BoolConstant(false_value) + false_value = BoolConstant(value=false_value) - return BoolITE(cond, true_value, false_value) + return BoolITE(cond=cond, true=true_value, false=false_value) def ITEBV(size, cond, true_value, false_value): @@ -213,11 +213,11 @@ def ITEBV(size, cond, true_value, false_value): return false_value if isinstance(true_value, int): - true_value = BitVecConstant(size, true_value) + true_value = BitVecConstant(size=size, value=true_value) if isinstance(false_value, int): - false_value = BitVecConstant(size, false_value) - return BitVecITE(size, cond, true_value, false_value) + false_value = BitVecConstant(size=size, value=false_value) + return BitVecITE(size=size, condition=cond, true_value=true_value, false_value=false_value) def UDIV(dividend, divisor): @@ -271,7 +271,7 @@ def SAR(size, a, b): assert size == a.size return a.sar(b) elif isinstance(b, BitVec): - return BitVecConstant(size, a).sar(b) + return BitVecConstant(size=size, value=a).sar(b) else: tempDest = a tempCount = b diff --git a/manticore/core/smtlib/visitors.py b/manticore/core/smtlib/visitors.py index f18b66b9f..f64dfd621 100644 --- a/manticore/core/smtlib/visitors.py +++ b/manticore/core/smtlib/visitors.py @@ -312,35 +312,35 @@ def visit_BitVecUnsignedDiv(self, expression, *operands) -> Optional[BitVecConst ret = 0 else: ret = math.trunc(Decimal(a) / Decimal(b)) - return BitVecConstant(expression.size, ret, taint=expression.taint) + return BitVecConstant(size=expression.size, value=ret, taint=expression.taint) return None def visit_LessThan(self, expression, *operands) -> Optional[BoolConstant]: if all(isinstance(o, Constant) for o in operands): a = operands[0].signed_value b = operands[1].signed_value - return BoolConstant(a < b, taint=expression.taint) + return BoolConstant(value=a < b, taint=expression.taint) return None def visit_LessOrEqual(self, expression, *operands) -> Optional[BoolConstant]: if all(isinstance(o, Constant) for o in operands): a = operands[0].signed_value b = operands[1].signed_value - return BoolConstant(a <= b, taint=expression.taint) + return BoolConstant(value=a <= b, taint=expression.taint) return None def visit_GreaterThan(self, expression, *operands) -> Optional[BoolConstant]: if all(isinstance(o, Constant) for o in operands): a = operands[0].signed_value b = operands[1].signed_value - return BoolConstant(a > b, taint=expression.taint) + return BoolConstant(value=a > b, taint=expression.taint) return None def visit_GreaterOrEqual(self, expression, *operands) -> Optional[BoolConstant]: if all(isinstance(o, Constant) for o in operands): a = operands[0].signed_value b = operands[1].signed_value - return BoolConstant(a >= b, taint=expression.taint) + return BoolConstant(value=a >= b, taint=expression.taint) return None def visit_BitVecDiv(self, expression, *operands) -> Optional[BitVecConstant]: @@ -357,7 +357,7 @@ def visit_BitVecDiv(self, expression, *operands) -> Optional[BitVecConstant]: result = 0 else: result = math.trunc(Decimal(numeral) / Decimal(dividend)) - return BitVecConstant(expression.size, result, taint=expression.taint) + return BitVecConstant(size=expression.size, value=result, taint=expression.taint) return None def visit_BitVecConcat(self, expression, *operands): @@ -366,11 +366,13 @@ def visit_BitVecConcat(self, expression, *operands): for o in operands: result <<= o.size result |= o.value - return BitVecConstant(expression.size, result, taint=expression.taint) + return BitVecConstant(size=expression.size, value=result, taint=expression.taint) def visit_BitVecZeroExtend(self, expression, *operands): if all(isinstance(o, Constant) for o in operands): - return BitVecConstant(expression.size, operands[0].value, taint=expression.taint) + return BitVecConstant( + size=expression.size, value=operands[0].value, taint=expression.taint + ) def visit_BitVecSignExtend(self, expression, *operands): if expression.extend == 0: @@ -384,7 +386,7 @@ def visit_BitVecExtract(self, expression, *operands): value = value >> begining mask = (1 << (end - begining)) - 1 value = value & mask - return BitVecConstant(expression.size, value, taint=expression.taint) + return BitVecConstant(size=expression.size, value=value, taint=expression.taint) def visit_BoolAnd(self, expression, a, b): if isinstance(a, Constant) and a.value == True: @@ -398,10 +400,10 @@ def _visit_operation(self, expression, *operands): if operation is not None and all(isinstance(o, Constant) for o in operands): value = operation(*(x.value for x in operands)) if isinstance(expression, BitVec): - return BitVecConstant(expression.size, value, taint=expression.taint) + return BitVecConstant(size=expression.size, value=value, taint=expression.taint) else: isinstance(expression, Bool) - return BoolConstant(value, taint=expression.taint) + return BoolConstant(value=value, taint=expression.taint) else: if any(operands[i] is not expression.operands[i] for i in range(len(operands))): expression = self._rebuild(expression, operands) @@ -449,7 +451,9 @@ def _visit_operation(self, expression, *operands): def visit_BitVecZeroExtend(self, expression, *operands): if self._changed(expression, operands): - return BitVecZeroExtend(expression.size, *operands, taint=expression.taint) + return BitVecZeroExtend( + size_dest=expression.size, operand=operands[0], taint=expression.taint + ) else: return expression @@ -494,9 +498,9 @@ def visit_BoolAnd(self, expression, *operands): value1 = operand_0_1.value beg = min(operand_0_0.begining, operand_1_0.begining) end = max(operand_0_0.end, operand_1_0.end) - return BitVecExtract(value0, beg, end - beg + 1) == BitVecExtract( - value1, beg, end - beg + 1 - ) + return BitVecExtract( + operand=value0, offset=beg, size=end - beg + 1 + ) == BitVecExtract(operand=value1, offset=beg, size=end - beg + 1) def visit_BoolNot(self, expression, *operands): if isinstance(operands[0], BoolNot): @@ -519,10 +523,10 @@ def visit_BoolEqual(self, expression, *operands): if value1 == value2 and value1 != value3: return operands[0].operands[0] # FIXME: this may break taint propagation elif value1 == value3 and value1 != value2: - return BoolNot(operands[0].operands[0], taint=expression.taint) + return BoolNot(value=operands[0].operands[0], taint=expression.taint) if operands[0] is operands[1]: - return BoolConstant(True, taint=expression.taint) + return BoolConstant(value=True, taint=expression.taint) if isinstance(operands[0], BitVecExtract) and isinstance(operands[1], BitVecExtract): if ( @@ -531,7 +535,7 @@ def visit_BoolEqual(self, expression, *operands): and operands[0].begining == operands[1].begining ): - return BoolConstant(True, taint=expression.taint) + return BoolConstant(value=True, taint=expression.taint) def visit_BoolOr(self, expression, a, b): if isinstance(a, Constant): @@ -560,7 +564,13 @@ def visit_BitVecITE(self, expression, *operands): return result if self._changed(expression, operands): - return BitVecITE(expression.size, *operands, taint=expression.taint) + return BitVecITE( + size=expression.size, + condition=operands[0], + true_value=operands[1], + false_value=operands[2], + taint=expression.taint, + ) def visit_BitVecConcat(self, expression, *operands): """concat( extract(k1, 0, a), extract(sizeof(a)-k1, k1, a)) ==> a @@ -580,7 +590,10 @@ def visit_BitVecConcat(self, expression, *operands): else: if last_o.value is o.value and last_o.begining == o.end + 1: last_o = BitVecExtract( - o.value, o.begining, last_o.end - o.begining + 1, taint=expression.taint + operand=o.value, + offset=o.begining, + size=last_o.end - o.begining + 1, + taint=expression.taint, ) changed = True else: @@ -594,7 +607,7 @@ def visit_BitVecConcat(self, expression, *operands): if last_o is not None: new_operands.append(last_o) if changed: - return BitVecConcat(expression.size, tuple(new_operands)) + return BitVecConcat(size_dest=expression.size, operands=tuple(new_operands)) op = operands[0] value = None @@ -624,7 +637,9 @@ def visit_BitVecConcat(self, expression, *operands): if value is not None: if end + 1 != value.size or begining != 0: - return BitVecExtract(value, begining, end - begining + 1, taint=expression.taint) + return BitVecExtract( + operand=value, offset=begining, size=end - begining + 1, taint=expression.taint + ) return value @@ -641,14 +656,18 @@ def visit_BitVecExtract(self, expression, *operands): if begining == 0 and end + 1 == op.size: return op elif isinstance(op, BitVecExtract): - return BitVecExtract(op.value, op.begining + begining, size, taint=expression.taint) + return BitVecExtract( + operand=op.value, offset=op.begining + begining, size=size, taint=expression.taint + ) elif isinstance(op, BitVecConcat): new_operands = [] for item in reversed(op.operands): if size == 0: assert expression.size == sum([x.size for x in new_operands]) return BitVecConcat( - expression.size, tuple(reversed(new_operands)), taint=expression.taint + size_dest=expression.size, + operands=tuple(reversed(new_operands)), + taint=expression.taint, ) if begining >= item.size: @@ -660,20 +679,26 @@ def visit_BitVecExtract(self, expression, *operands): size = 0 else: if size <= item.size - begining: - new_operands.append(BitVecExtract(item, begining, size)) + new_operands.append( + BitVecExtract(operand=item, offset=begining, size=size) + ) size = 0 else: - new_operands.append(BitVecExtract(item, begining, item.size - begining)) + new_operands.append( + BitVecExtract( + operand=item, offset=begining, size=item.size - begining + ) + ) size -= item.size - begining begining = 0 elif isinstance(op, BitVecConstant): - return BitVecConstant(size, (op.value >> begining) & ~(1 << size)) + return BitVecConstant(size=size, value=(op.value >> begining) & ~(1 << size)) if isinstance(op, (BitVecAnd, BitVecOr, BitVecXor)): bitoperand_a, bitoperand_b = op.operands return op.__class__( - BitVecExtract(bitoperand_a, begining, expression.size), - BitVecExtract(bitoperand_b, begining, expression.size), + a=BitVecExtract(operand=bitoperand_a, offset=begining, size=expression.size), + b=BitVecExtract(operand=bitoperand_b, offset=begining, size=expression.size), taint=expression.taint, ) @@ -707,10 +732,10 @@ def visit_BitVecSub(self, expression, *operands): subright = left.operands[1] if isinstance(subright, Constant): return BitVecSub( - subleft, - BitVecConstant( - subleft.size, - subright.value + right.value, + a=subleft, + b=BitVecConstant( + size=subleft.size, + value=subright.value + right.value, taint=subright.taint | right.taint, ), ) @@ -733,9 +758,9 @@ def visit_BitVecOr(self, expression, *operands): left_left = left.operands[0] left_right = left.operands[1] if isinstance(right, Constant): - return BitVecOr(left_left, (left_right | right), taint=expression.taint) + return BitVecOr(a=left_left, b=(left_right | right), taint=expression.taint) elif isinstance(left, BitVecConstant): - return BitVecOr(right, left, taint=expression.taint) + return BitVecOr(a=right, b=left, taint=expression.taint) def visit_BitVecAnd(self, expression, *operands): """ct & x => x & ct move constants to the right @@ -755,14 +780,14 @@ def visit_BitVecAnd(self, expression, *operands): left_left = left.operands[0] left_right = left.operands[1] if isinstance(right, Constant): - return BitVecAnd(left_left, left_right & right, taint=expression.taint) + return BitVecAnd(a=left_left, b=left_right & right, taint=expression.taint) elif isinstance(left, BitVecOr): left_left = left.operands[0] left_right = left.operands[1] - return BitVecOr(right & left_left, right & left_right, taint=expression.taint) + return BitVecOr(a=right & left_left, b=right & left_right, taint=expression.taint) elif isinstance(left, BitVecConstant): - return BitVecAnd(right, left, taint=expression.taint) + return BitVecAnd(a=right, b=left, taint=expression.taint) def visit_BitVecShiftLeft(self, expression, *operands): """a << 0 => a remove zero diff --git a/manticore/core/state.py b/manticore/core/state.py index f5536cef6..d6ae24608 100644 --- a/manticore/core/state.py +++ b/manticore/core/state.py @@ -76,7 +76,7 @@ def _setstate(self, state, _value): def __init__(self, filename, **kwargs): super().__init__( f"Saving state to {filename}", - BitVecConstant(32, 0), + BitVecConstant(size=32, value=0), setstate=self._setstate, policy="ONE", **kwargs, diff --git a/manticore/ethereum/abi.py b/manticore/ethereum/abi.py index e3a1bc310..9655e29f2 100644 --- a/manticore/ethereum/abi.py +++ b/manticore/ethereum/abi.py @@ -320,7 +320,7 @@ def _serialize_int(value: typing.Union[int, BitVec], size=32, padding=0): index_bits=256, index_max=32, value_bits=8, name="temp{}".format(uuid.uuid1()) ) value = Operators.SEXTEND(value, value.size, size * 8) - return ArrayProxy(buf.write_BE(padding, value, size)) + return ArrayProxy(array=buf.write_BE(padding, value, size)) else: buf_arr = bytearray() for _ in range(padding): diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index ea0de52c9..8e4c733d1 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -869,7 +869,7 @@ def _migrate_tx_expressions(self, state, caller, address, value, data, gas, pric data = data.array data = state.migrate_expression(data) if isinstance(data, Array): - data = ArrayProxy(data) + data = ArrayProxy(array=data) if issymbolic(gas): gas = state.migrate_expression(gas) @@ -1023,7 +1023,7 @@ def preconstraint_for_call_transaction( selectors = contract_metadata.function_selectors if not selectors or len(data) <= 4: - return BoolConstant(True) + return BoolConstant(value=True) symbolic_selector = data[:4] diff --git a/manticore/native/cpu/x86.py b/manticore/native/cpu/x86.py index c43b95f7b..e915eaef1 100644 --- a/manticore/native/cpu/x86.py +++ b/manticore/native/cpu/x86.py @@ -645,8 +645,8 @@ def make_symbolic(flag_expr): return Operators.ITEBV( register_size, value, - BitVecConstant(register_size, 1 << offset), - BitVecConstant(register_size, 0), + BitVecConstant(size=register_size, value=1 << offset), + BitVecConstant(size=register_size, value=0), ) flags = [] @@ -2529,7 +2529,12 @@ def LAHF(cpu): def make_flag(val, offset): if is_expression: - return Operators.ITEBV(8, val, BitVecConstant(8, 1 << offset), BitVecConstant(8, 0)) + return Operators.ITEBV( + size=8, + cond=val, + true_value=BitVecConstant(size=8, value=1 << offset), + false_value=BitVecConstant(size=8, value=0), + ) else: return val << offset diff --git a/manticore/native/memory.py b/manticore/native/memory.py index 5f8ca25c4..5a8850088 100644 --- a/manticore/native/memory.py +++ b/manticore/native/memory.py @@ -347,7 +347,9 @@ def __init__( self._array = backing_array else: self._array = expression.ArrayProxy( - expression.ArrayVariable(index_bits, index_max=size, value_bits=8, name=name) + array=expression.ArrayVariable( + index_bits=index_bits, index_max=size, value_bits=8, name=name + ) ) def __reduce__(self): @@ -382,10 +384,14 @@ def split(self, address: int): left_name, right_name = ["{}_{:d}".format(self._array.name, i) for i in range(2)] head_arr = expression.ArrayProxy( - expression.ArrayVariable(index_bits, left_size, value_bits, name=left_name) + array=expression.ArrayVariable( + index_bits=index_bits, index_max=left_size, value_bits=value_bits, name=left_name + ) ) tail_arr = expression.ArrayProxy( - expression.ArrayVariable(index_bits, right_size, value_bits, name=right_name) + array=expression.ArrayVariable( + index_bits=index_bits, index_max=right_size, value_bits=value_bits, name=right_name + ) ) head = ArrayMap(self.start, left_size, self.perms, index_bits, head_arr, left_name) @@ -1157,7 +1163,7 @@ def _get_size(self, size): if isinstance(size, BitVec): size = arithmetic_simplify(size) else: - size = BitVecConstant(self.memory_bit_size, size) + size = BitVecConstant(size=self.memory_bit_size, value=size) assert isinstance(size, BitVecConstant) return size.value diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 1630ba9e5..631166c8e 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -1304,7 +1304,9 @@ def execute(self): def setstate(state, value): if taints: - state.platform.current_vm.pc = BitVecConstant(256, value, taint=taints) + state.platform.current_vm.pc = BitVecConstant( + size=256, value=value, taint=taints + ) else: state.platform.current_vm.pc = value @@ -1404,7 +1406,7 @@ def read_buffer(self, offset, size): return b"" self._allocate(offset, size) data = self.memory[offset : offset + size] - return ArrayProxy(data) + return ArrayProxy(array=data) def write_buffer(self, offset, data): self._allocate(offset, len(data)) diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index abcaf1b91..0dea8cf85 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -1382,7 +1382,7 @@ def will_evm_execute_instruction_callback(self, state, i, *args, **kwargs): class EthHelpersTest(unittest.TestCase): def setUp(self): - self.bv = BitVecVariable(256, name="BVV") + self.bv = BitVecVariable(size=256, name="BVV") def test_concretizer(self): policy = "SOME_NONSTANDARD_POLICY" diff --git a/tests/native/test_cpu_manual.py b/tests/native/test_cpu_manual.py index 15daf9ee9..2e8296af8 100644 --- a/tests/native/test_cpu_manual.py +++ b/tests/native/test_cpu_manual.py @@ -309,7 +309,7 @@ def _construct_flag_bitfield(self, flags): return reduce(operator.or_, (self._flags[f] for f in flags)) def _construct_sym_flag_bitfield(self, flags): - return reduce(operator.or_, (BitVecConstant(32, self._flags[f]) for f in flags)) + return reduce(operator.or_, (BitVecConstant(size=32, value=self._flags[f]) for f in flags)) def test_set_eflags(self) -> None: cpu = I386Cpu(Memory32()) @@ -371,8 +371,8 @@ def flatten_ors(x: BitVecOr) -> List: cpu.CF = 1 cpu.AF = 1 - a = BitVecConstant(32, 1) != 0 - b = BitVecConstant(32, 0) != 0 + a = BitVecConstant(size=32, value=1) != 0 + b = BitVecConstant(size=32, value=0) != 0 cpu.ZF = a cpu.SF = b @@ -1290,7 +1290,7 @@ def test_symbolic_instruction(self): code = mem.mmap(0x1000, 0x1000, "rwx") stack = mem.mmap(0xF000, 0x1000, "rw") - mem[code] = BitVecConstant(8, 0x90) + mem[code] = BitVecConstant(size=8, value=0x90) cpu.EIP = code cpu.EAX = 116 cpu.EBP = stack + 0x700 diff --git a/tests/native/test_driver.py b/tests/native/test_driver.py index e516fc012..a22eb2f44 100644 --- a/tests/native/test_driver.py +++ b/tests/native/test_driver.py @@ -26,7 +26,7 @@ def testCreating(self): m.log_file = "/dev/null" def test_issymbolic(self): - v = BitVecVariable(32, "sym") + v = BitVecVariable(size=32, name="sym") self.assertTrue(issymbolic(v)) def test_issymbolic_neg(self): diff --git a/tests/native/test_register.py b/tests/native/test_register.py index 0663e811b..0c4834a2c 100644 --- a/tests/native/test_register.py +++ b/tests/native/test_register.py @@ -53,14 +53,14 @@ def test_Bool(self): def test_bitvec_flag(self): r = Register(1) - b = BitVecConstant(32, 0) + b = BitVecConstant(size=32, value=0) r.write(b) # __nonzero__ (==) currently unimplemented for Bool self.assertTrue(isinstance(r.read(), Bool)) def test_bitvec(self): r = Register(32) - b = BitVecConstant(32, 0) + b = BitVecConstant(size=32, value=0) r.write(b) self.assertIs(r.read(), b) diff --git a/tests/native/test_state.py b/tests/native/test_state.py index d330760df..1a9240cd6 100644 --- a/tests/native/test_state.py +++ b/tests/native/test_state.py @@ -79,27 +79,27 @@ def setUp(self): def test_solve_one(self): val = 42 - expr = BitVecVariable(32, "tmp") + expr = BitVecVariable(size=32, name="tmp") self.state.constrain(expr == val) solved = self.state.solve_one(expr) self.assertEqual(solved, val) def test_solve_n(self): - expr = BitVecVariable(32, "tmp") + expr = BitVecVariable(size=32, name="tmp") self.state.constrain(expr > 4) self.state.constrain(expr < 7) solved = sorted(self.state.solve_n(expr, 2)) self.assertEqual(solved, [5, 6]) def test_solve_n2(self): - expr = BitVecVariable(32, "tmp") + expr = BitVecVariable(size=32, name="tmp") self.state.constrain(expr > 4) self.state.constrain(expr < 100) solved = self.state.solve_n(expr, 5) self.assertEqual(len(solved), 5) def test_solve_min_max(self): - expr = BitVecVariable(32, "tmp") + expr = BitVecVariable(size=32, name="tmp") self.state.constrain(expr > 4) self.state.constrain(expr < 7) self.assertEqual(self.state.solve_min(expr), 5) @@ -107,7 +107,7 @@ def test_solve_min_max(self): self.assertEqual(self.state.solve_minmax(expr), (5, 6)) def test_policy_one(self): - expr = BitVecVariable(32, "tmp") + expr = BitVecVariable(size=32, name="tmp") self.state.constrain(expr > 0) self.state.constrain(expr < 100) solved = self.state.concretize(expr, "ONE") diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py index 11d4236cf..50d1d21ed 100644 --- a/tests/other/test_smtlibv2.py +++ b/tests/other/test_smtlibv2.py @@ -228,9 +228,9 @@ def check(ty: Type, pickle_size=None, sizeof=None, **kwargs): ) a = ArrayVariable(index_bits=32, value_bits=32, index_max=324, name="name") - check(ArraySlice, array=a, offset=0, size=10, pickle_size=244, sizeof=136) + check(ArraySlice, array=a, offset=0, size=10, pickle_size=326, sizeof=136) check(ArraySelect, array=a, index=bvx, pickle_size=255, sizeof=64) - check(ArrayStore, array=a, index=bvx, value=bvy, pickle_size=281, sizeof=120) + check(ArrayStore, array=a, index=bvx, value=bvy, pickle_size=286, sizeof=120) check(ArrayProxy, array=a, default=0, pickle_size=222, sizeof=120) def all_subclasses(cls) -> Set[Type]: @@ -262,7 +262,7 @@ def test_no_variable_expression_can_be_true(self): Tests if solver.can_be_true is correct when the expression has no nodes that subclass from Variable (e.g. BitVecConstant) """ - x = BitVecConstant(32, 10) + x = BitVecConstant(size=32, value=10) cs = ConstraintSet() self.assertFalse(self.solver.can_be_true(cs, x == False)) @@ -270,12 +270,12 @@ def test_constant_bitvec(self): """ Tests if higher bits are masked out """ - x = BitVecConstant(32, 0xFF00000000) + x = BitVecConstant(size=32, value=0xFF00000000) self.assertTrue(x.value == 0) def testBasicAST_001(self): """ Can't build abstract classes """ - a = BitVecConstant(32, 100) + a = BitVecConstant(size=32, value=100) self.assertRaises(TypeError, Expression, ()) self.assertRaises(TypeError, Constant, 123) @@ -284,16 +284,16 @@ def testBasicAST_001(self): def testBasicOperation(self): """ Add """ - a = BitVecConstant(32, 100) - b = BitVecVariable(32, "VAR") + a = BitVecConstant(size=32, value=100) + b = BitVecVariable(size=32, name="VAR") c = a + b self.assertIsInstance(c, BitVecAdd) self.assertIsInstance(c, Operation) self.assertIsInstance(c, Expression) def testBasicTaint(self): - a = BitVecConstant(32, 100, taint=("SOURCE1",)) - b = BitVecConstant(32, 200, taint=("SOURCE2",)) + a = BitVecConstant(size=32, value=100, taint=("SOURCE1",)) + b = BitVecConstant(size=32, value=200, taint=("SOURCE2",)) c = a + b self.assertIsInstance(c, BitVecAdd) self.assertIsInstance(c, Operation) @@ -302,10 +302,10 @@ def testBasicTaint(self): self.assertTrue("SOURCE2" in c.taint) def testBasicITETaint(self): - a = BitVecConstant(32, 100, taint=("SOURCE1",)) - b = BitVecConstant(32, 200, taint=("SOURCE2",)) - c = BitVecConstant(32, 300, taint=("SOURCE3",)) - d = BitVecConstant(32, 400, taint=("SOURCE4",)) + a = BitVecConstant(size=32, value=100, taint=("SOURCE1",)) + b = BitVecConstant(size=32, value=200, taint=("SOURCE2",)) + c = BitVecConstant(size=32, value=300, taint=("SOURCE3",)) + d = BitVecConstant(size=32, value=400, taint=("SOURCE4",)) x = Operators.ITEBV(32, a > b, c, d) self.assertTrue("SOURCE1" in x.taint) self.assertTrue("SOURCE2" in x.taint) @@ -339,29 +339,29 @@ def testSolver(self): def testBool1(self): cs = ConstraintSet() - bf = BoolConstant(False) - bt = BoolConstant(True) + bf = BoolConstant(value=False) + bt = BoolConstant(value=True) cs.add(Operators.AND(bf, bt)) self.assertFalse(self.solver.check(cs)) def testBool2(self): cs = ConstraintSet() - bf = BoolConstant(False) - bt = BoolConstant(True) + bf = BoolConstant(value=False) + bt = BoolConstant(value=True) cs.add(Operators.AND(bf, bt, bt, bt)) self.assertFalse(self.solver.check(cs)) def testBool3(self): cs = ConstraintSet() - bf = BoolConstant(False) - bt = BoolConstant(True) + bf = BoolConstant(value=False) + bt = BoolConstant(value=True) cs.add(Operators.AND(bt, bt, bf, bt)) self.assertFalse(self.solver.check(cs)) def testBool4(self): cs = ConstraintSet() - bf = BoolConstant(False) - bt = BoolConstant(True) + bf = BoolConstant(value=False) + bt = BoolConstant(value=True) cs.add(Operators.OR(True, bf)) cs.add(Operators.OR(bt, bt, False)) self.assertTrue(self.solver.check(cs)) @@ -566,7 +566,7 @@ def testBasicArraySlice(self): def testBasicArrayProxySymbIdx(self): cs = ConstraintSet() - array = ArrayProxy(cs.new_array(index_bits=32, value_bits=32, name="array"), default=0) + array = cs.new_array(index_bits=32, value_bits=32, name="array", default=0) key = cs.new_bitvec(32, name="key") index = cs.new_bitvec(32, name="index") @@ -581,7 +581,7 @@ def testBasicArrayProxySymbIdx(self): def testBasicArrayProxySymbIdx2(self): cs = ConstraintSet() - array = ArrayProxy(cs.new_array(index_bits=32, value_bits=32, name="array")) + array = cs.new_array(index_bits=32, value_bits=32, name="array") key = cs.new_bitvec(32, name="key") index = cs.new_bitvec(32, name="index") @@ -696,8 +696,8 @@ def testBitvector_max1_noop(self): consts.optimize = True def testBool_nonzero(self): - self.assertTrue(BoolConstant(True).__bool__()) - self.assertFalse(BoolConstant(False).__bool__()) + self.assertTrue(BoolConstant(value=True).__bool__()) + self.assertFalse(BoolConstant(value=False).__bool__()) def test_visitors(self): solver = Z3Solver.instance() @@ -745,8 +745,8 @@ def test_visitors(self): ) self.assertEqual(pretty_print(a, depth=2), "VAR\n") - x = BitVecConstant(32, 100, taint=("important",)) - y = BitVecConstant(32, 200, taint=("stuff",)) + x = BitVecConstant(size=32, value=100, taint=("important",)) + y = BitVecConstant(size=32, value=200, taint=("stuff",)) z = constant_folder(x + y) self.assertItemsEqual(z.taint, ("important", "stuff")) self.assertEqual(z.value, 300) @@ -816,26 +816,26 @@ def test_arithmetic_simplify_extract(self): def test_arithmetic_simplify_udiv(self): cs = ConstraintSet() a = cs.new_bitvec(32, name="VARA") - b = a + Operators.UDIV(BitVecConstant(32, 0), BitVecConstant(32, 2)) + b = a + Operators.UDIV(BitVecConstant(size=32, value=0), BitVecConstant(size=32, value=2)) self.assertEqual(translate_to_smtlib(b), "(bvadd VARA (bvudiv #x00000000 #x00000002))") self.assertEqual(translate_to_smtlib(simplify(b)), "VARA") - c = a + Operators.UDIV(BitVecConstant(32, 2), BitVecConstant(32, 2)) + c = a + Operators.UDIV(BitVecConstant(size=32, value=2), BitVecConstant(size=32, value=2)) self.assertEqual(translate_to_smtlib(c), "(bvadd VARA (bvudiv #x00000002 #x00000002))") self.assertEqual(translate_to_smtlib(simplify(c)), "(bvadd VARA #x00000001)") def test_constant_folding_udiv(self): cs = ConstraintSet() - x = BitVecConstant(32, 0xFFFFFFFF, taint=("important",)) - y = BitVecConstant(32, 2, taint=("stuff",)) + x = BitVecConstant(size=32, value=0xFFFFFFFF, taint=("important",)) + y = BitVecConstant(size=32, value=2, taint=("stuff",)) z = constant_folder(x.udiv(y)) self.assertItemsEqual(z.taint, ("important", "stuff")) self.assertEqual(z.value, 0x7FFFFFFF) def test_simplify_OR(self): cs = ConstraintSet() - bf = BoolConstant(False) - bt = BoolConstant(True) + bf = BoolConstant(value=False) + bt = BoolConstant(value=True) var = cs.new_bool() cs.add(simplify(Operators.OR(var, var)) == var) cs.add(simplify(Operators.OR(var, bt)) == bt) @@ -843,9 +843,9 @@ def test_simplify_OR(self): def testBasicReplace(self): """ Add """ - a = BitVecConstant(32, 100) - b1 = BitVecVariable(32, "VAR1") - b2 = BitVecVariable(32, "VAR2") + a = BitVecConstant(size=32, value=100) + b1 = BitVecVariable(size=32, name="VAR1") + b2 = BitVecVariable(size=32, name="VAR2") c = a + b1