Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix 1427 - limit sanity check in SMTlib #1543

Merged
merged 6 commits into from
Nov 8, 2019
Merged

fix 1427 - limit sanity check in SMTlib #1543

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
ae16521
add type hints replacing assert isinstances and reformat with black
Srinivas11789 Oct 27, 2019
5881aba
change annotations to support python 3.6
Srinivas11789 Oct 28, 2019
bae36c0
address mypy test issues and prefer forward references
Srinivas11789 Oct 28, 2019
9d46c2d
address feedback --> remove any and obvious None returns, explicit types
Srinivas11789 Nov 3, 2019
6920d24
decide to remove Any altogether and test with mypy
Srinivas11789 Nov 6, 2019
7e0fa0f
correct type hints for some functions
Srinivas11789 Nov 6, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
116 changes: 54 additions & 62 deletions manticore/core/smtlib/expression.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

import re
import copy
from typing import Union, Type, Optional, Dict, Any


class ExpressionException(SmtlibError):
Expand All @@ -17,10 +18,9 @@ class ExpressionException(SmtlibError):
class Expression:
""" Abstract taintable Expression. """

def __init__(self, taint=()):
def __init__(self, taint: Union[tuple, frozenset] = ()):
if self.__class__ is Expression:
raise TypeError
assert isinstance(taint, (tuple, frozenset))
super().__init__()
self._taint = frozenset(taint)

Expand Down Expand Up @@ -111,10 +111,10 @@ def taint_with(arg, *taints, value_bits=256, index_bits=256):


class Variable(Expression):
def __init__(self, name, *args, **kwargs):
def __init__(self, name: str, *args, **kwargs):
if self.__class__ is Variable:
raise TypeError
assert isinstance(name, str) and " " not in name
assert " " not in name
super().__init__(*args, **kwargs)
self._name = name

Expand All @@ -137,10 +137,9 @@ def __repr__(self):


class Constant(Expression):
def __init__(self, value, *args, **kwargs):
def __init__(self, value: Union[bool, int], *args, **kwargs):
if self.__class__ is Constant:
raise TypeError
assert isinstance(value, (bool, int))
super().__init__(*args, **kwargs)
self._value = value

Expand Down Expand Up @@ -174,10 +173,9 @@ class Bool(Expression):
def __init__(self, *operands, **kwargs):
super().__init__(*operands, **kwargs)

def cast(self, value, **kwargs):
def cast(self, value: Union[int, bool], **kwargs) -> Union["BoolConstant", "Bool"]:
if isinstance(value, Bool):
return value
assert isinstance(value, (int, bool))
return BoolConstant(bool(value), **kwargs)

def __cmp__(self, *args):
Expand Down Expand Up @@ -227,8 +225,7 @@ def declaration(self):


class BoolConstant(Bool, Constant):
def __init__(self, value, *args, **kwargs):
assert isinstance(value, bool)
def __init__(self, value: bool, *args, **kwargs):
super().__init__(value, *args, **kwargs)

def __bool__(self):
Expand All @@ -251,9 +248,7 @@ def __init__(self, a, b, **kwargs):


class BoolOr(BoolOperation):
def __init__(self, a, b, **kwargs):
assert isinstance(a, Bool)
assert isinstance(b, Bool)
def __init__(self, a: "Bool", b: "Bool", **kwargs):
super().__init__(a, b, **kwargs)


Expand All @@ -263,10 +258,7 @@ def __init__(self, a, b, **kwargs):


class BoolITE(BoolOperation):
def __init__(self, cond, true, false, **kwargs):
assert isinstance(true, Bool)
assert isinstance(false, Bool)
assert isinstance(cond, Bool)
def __init__(self, cond: "Bool", true: "Bool", false: "Bool", **kwargs):
super().__init__(cond, true, false, **kwargs)


Expand All @@ -285,7 +277,9 @@ def mask(self):
def signmask(self):
return 1 << (self.size - 1)

def cast(self, value, **kwargs):
def cast(
self, value: Union["BitVec", str, int, bytes], **kwargs
) -> Union["BitVecConstant", "BitVec"]:
if isinstance(value, BitVec):
assert value.size == self.size
return value
Expand Down Expand Up @@ -481,8 +475,7 @@ def declaration(self):


class BitVecConstant(BitVec, Constant):
def __init__(self, size, value, *args, **kwargs):
assert isinstance(value, int)
def __init__(self, size: int, value: int, *args, **kwargs):
super().__init__(size, value, *args, **kwargs)

def __bool__(self):
Expand Down Expand Up @@ -568,9 +561,7 @@ def __init__(self, a, b, *args, **kwargs):


class BitVecOr(BitVecOperation):
def __init__(self, a, b, *args, **kwargs):
assert isinstance(a, BitVec)
assert isinstance(b, BitVec)
def __init__(self, a: BitVec, b: BitVec, *args, **kwargs):
assert a.size == b.size
super().__init__(a.size, a, b, *args, **kwargs)

Expand Down Expand Up @@ -647,10 +638,11 @@ def __init__(self, a, b, *args, **kwargs):
###############################################################################
# Array BV32 -> BV8 or BV64 -> BV8
class Array(Expression):
def __init__(self, index_bits, index_max, value_bits, *operands, **kwargs):
def __init__(
self, index_bits: int, index_max: Optional[int], value_bits: int, *operands, **kwargs
):
assert index_bits in (32, 64, 256)
assert value_bits in (8, 16, 32, 64, 256)
assert index_max is None or isinstance(index_max, int)
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
Expand Down Expand Up @@ -690,21 +682,24 @@ def cast(self, possible_array):
return arr
raise ValueError # cast not implemented

def cast_index(self, index):
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)
assert isinstance(index, BitVec) and index.size == self.index_bits
assert index.size == self.index_bits
return index

def cast_value(self, value):
def cast_value(
ehennenfent marked this conversation as resolved.
Show resolved Hide resolved
self, value: Union["BitVec", str, bytes, int]
) -> Union["BitVecConstant", "BitVec"]:
if isinstance(value, BitVec):
assert value.size == self.value_bits
return value
if isinstance(value, (str, bytes)) and len(value) == 1:
value = ord(value)
if isinstance(value, int):
return BitVecConstant(self.value_bits, value)
assert isinstance(value, BitVec)
assert value.size == self.value_bits
return value
if not isinstance(value, int):
value = int(value)
return BitVecConstant(self.value_bits, value)

def __len__(self):
if self.index_max is None:
Expand Down Expand Up @@ -875,18 +870,16 @@ def declaration(self):


class ArrayOperation(Array, Operation):
def __init__(self, array, *operands, **kwargs):
assert isinstance(array, Array)
def __init__(self, array: Array, *operands, **kwargs):
super().__init__(
array.index_bits, array.index_max, array.value_bits, array, *operands, **kwargs
)


class ArrayStore(ArrayOperation):
def __init__(self, array, index, value, *args, **kwargs):
assert isinstance(array, Array)
assert isinstance(index, BitVec) and index.size == array.index_bits
assert isinstance(value, BitVec) and value.size == array.value_bits
def __init__(self, array: "Array", index: "BitVec", value: "BitVec", *args, **kwargs):
assert index.size == array.index_bits
assert value.size == array.value_bits
super().__init__(array, index, value, *args, **kwargs)

@property
Expand All @@ -907,7 +900,9 @@ def value(self):


class ArraySlice(Array):
def __init__(self, array, offset, size, *args, **kwargs):
def __init__(
self, array: Union["Array", "ArrayProxy"], offset: int, size: int, *args, **kwargs
):
if not isinstance(array, Array):
raise ValueError("Array expected")
if isinstance(array, ArrayProxy):
Expand Down Expand Up @@ -954,16 +949,15 @@ def store(self, index, value):


class ArrayProxy(Array):
def __init__(self, array, default=None):
assert isinstance(array, Array)
def __init__(self, array: Array, default: Optional[int] = None):
self._default = default
self._concrete_cache = {}
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)
self._array = array._array
self._name = array._name
self._array: Array = array._array
self._name: str = array._name
if default is None:
self._default = array._default
self._concrete_cache = dict(array._concrete_cache)
Expand Down Expand Up @@ -1138,9 +1132,8 @@ def get(self, index, default=None):


class ArraySelect(BitVec, Operation):
def __init__(self, array, index, *args, **kwargs):
assert isinstance(array, Array)
assert isinstance(index, BitVec) and index.size == array.index_bits
def __init__(self, array: "Array", index: "BitVec", *args, **kwargs):
assert index.size == array.index_bits
super().__init__(array.value_bits, array, index, *args, **kwargs)

@property
Expand All @@ -1156,27 +1149,21 @@ def __repr__(self):


class BitVecSignExtend(BitVecOperation):
def __init__(self, operand, size_dest, *args, **kwargs):
assert isinstance(operand, BitVec)
assert isinstance(size_dest, int)
def __init__(self, operand: "BitVec", size_dest: int, *args, **kwargs):
assert size_dest >= operand.size
super().__init__(size_dest, operand, *args, **kwargs)
self.extend = size_dest - operand.size


class BitVecZeroExtend(BitVecOperation):
def __init__(self, size_dest, operand, *args, **kwargs):
assert isinstance(operand, BitVec)
assert isinstance(size_dest, int)
def __init__(self, size_dest: int, operand: "BitVec", *args, **kwargs):
assert size_dest >= operand.size
super().__init__(size_dest, operand, *args, **kwargs)
self.extend = size_dest - operand.size


class BitVecExtract(BitVecOperation):
def __init__(self, operand, offset, size, *args, **kwargs):
assert isinstance(offset, int)
assert isinstance(size, int)
def __init__(self, operand: "BitVec", offset: int, size: int, *args, **kwargs):
assert offset >= 0 and offset + size <= operand.size
super().__init__(size, operand, *args, **kwargs)
self._begining = offset
Expand All @@ -1196,17 +1183,22 @@ def end(self):


class BitVecConcat(BitVecOperation):
def __init__(self, size_dest, *operands, **kwargs):
assert isinstance(size_dest, int)
def __init__(self, size_dest: int, *operands, **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)


class BitVecITE(BitVecOperation):
def __init__(self, size, condition, true_value, false_value, *args, **kwargs):
assert isinstance(true_value, BitVec)
assert isinstance(false_value, BitVec)
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)