Slottify expressions

CHANGELOG.md

@@ -409,7 +409,7 @@ Thanks to our external contributors!
 - Ethereum: Support for Solidity `bytesM` and `bytes` types
 - Ethereum: Beta API for preconstraining inputs (`ManticoreEVM.constrain`)
 - Improved performance for smtlib module
-- Ability to transparently operate on bytearray and symbolic buffer (ArrayProxy) types (e.g: concatenate, slice)
+- Ability to transparently operate on bytearray and symbolic buffer (MutableArray) types (e.g: concatenate, slice)
 
 ### Changed
 

examples/evm/asm_to_smtlib.py

@@ -42,7 +42,7 @@ def printi(instruction):
 )
 
 
-data = constraints.new_array(index_bits=256, name="array")
+data = constraints.new_array(index_size=256, name="array")
 
 
 class callbacks:
@@ -57,8 +57,8 @@ def will_execute_instruction(self, pc, instr):
 
 class DummyWorld:
     def __init__(self, constraints):
-        self.balances = constraints.new_array(index_bits=256, value_bits=256, name="balances")
-        self.storage = constraints.new_array(index_bits=256, value_bits=256, name="storage")
+        self.balances = constraints.new_array(index_size=256, value_size=256, name="balances")
+        self.storage = constraints.new_array(index_size=256, value_size=256, name="storage")
         self.origin = constraints.new_bitvec(256, name="origin")
         self.price = constraints.new_bitvec(256, name="price")
         self.timestamp = constraints.new_bitvec(256, name="timestamp")

examples/evm/minimal.py

@@ -25,13 +25,13 @@
 }
 """
 
-user_account = m.create_account(balance=1000, name="user_account")
+user_account = m.create_account(balance=10 ** 10, name="user_account")
 print("[+] Creating a user account", user_account.name_)
 
 contract_account = m.solidity_create_contract(
     source_code, owner=user_account, name="contract_account"
 )
-print("[+] Creating a contract account", contract_account.name_)
+print("[+] Creating a contract account", contract_account)
 contract_account.named_func(1)
 
 print("[+] Now the symbolic values")

examples/script/concolic.py

@@ -66,21 +66,21 @@ def flip(constraint):
     """
     flips a constraint (Equal)
 
-    (Equal (BitVecITE Cond IfC ElseC) IfC)
+    (Equal (BitvecITE Cond IfC ElseC) IfC)
         ->
-    (Equal (BitVecITE Cond IfC ElseC) ElseC)
+    (Equal (BitvecITE Cond IfC ElseC) ElseC)
     """
     equal = copy.copy(constraint)
 
     assert len(equal.operands) == 2
     # assume they are the equal -> ite form that we produce on standard branches
     ite, forcepc = equal.operands
-    if not (isinstance(ite, BitVecITE) and isinstance(forcepc, BitVecConstant)):
+    if not (isinstance(ite, BitvecITE) and isinstance(forcepc, BitvecConstant)):
         return constraint
-    assert isinstance(ite, BitVecITE) and isinstance(forcepc, BitVecConstant)
+    assert isinstance(ite, BitvecITE) and isinstance(forcepc, BitvecConstant)
     assert len(ite.operands) == 3
     cond, iifpc, eelsepc = ite.operands
-    assert isinstance(iifpc, BitVecConstant) and isinstance(eelsepc, BitVecConstant)
+    assert isinstance(iifpc, BitvecConstant) and isinstance(eelsepc, BitvecConstant)
 
     equal._operands = (equal.operands[0], eelsepc if forcepc.value == iifpc.value else iifpc)
 

manticore/core/smtlib/__init__.py

@@ -1,4 +1,4 @@
-from .expression import Expression, Bool, BitVec, Array, BitVecConstant, issymbolic  # noqa
+from .expression import Expression, Bool, Bitvec, Array, BitvecConstant, issymbolic  # noqa
 from .constraints import ConstraintSet  # noqa
 from .solver import *  # noqa
 from . import operators as Operators  # noqa

manticore/core/smtlib/constraints.py

@@ -6,26 +6,19 @@
 from ...exceptions import SmtlibError
 from .expression import (
     Expression,
-    BitVecVariable,
+    BitvecVariable,
     BoolVariable,
     ArrayVariable,
     Array,
     Bool,
-    BitVec,
+    Bitvec,
     BoolConstant,
-    ArrayProxy,
+    MutableArray,
     BoolEqual,
     Variable,
     Constant,
 )
-from .visitors import (
-    GetDeclarations,
-    TranslatorSmtlib,
-    get_variables,
-    simplify,
-    replace,
-    pretty_print,
-)
+from .visitors import GetDeclarations, TranslatorSmtlib, get_variables, simplify, replace
 from ...utils import config
 import logging
 
@@ -40,11 +33,15 @@ class ConstraintException(SmtlibError):
     pass
 
 
+class Model:
+    pass
+
+
 class ConstraintSet:
-    """ Constraint Sets
+    """Constraint Sets
 
-        An object containing a set of constraints. Serves also as a factory for
-        new variables.
+    An object containing a set of constraints. Serves also as a factory for
+    new variables.
     """
 
     def __init__(self):
@@ -178,58 +175,33 @@ def related_to(self, *related_to) -> "ConstraintSet":
 
     def to_string(self, replace_constants: bool = False) -> str:
         variables, constraints = self.get_declared_variables(), self.constraints
-
         if replace_constants:
             constant_bindings = {}
             for expression in constraints:
                 if (
                     isinstance(expression, BoolEqual)
                     and isinstance(expression.operands[0], Variable)
-                    and isinstance(expression.operands[1], (*Variable, *Constant))
+                    and not isinstance(expression.operands[1], (Variable, Constant))
                 ):
                     constant_bindings[expression.operands[0]] = expression.operands[1]
 
-        tmp = set()
         result = ""
-        for var in variables:
-            # FIXME
-            # band aid hack around the fact that we are double declaring stuff :( :(
-            if var.declaration in tmp:
-                logger.warning("Variable '%s' was copied twice somewhere", var.name)
-                continue
-            tmp.add(var.declaration)
-            result += var.declaration + "\n"
-
-        translator = TranslatorSmtlib(use_bindings=True)
+        translator = TranslatorSmtlib(use_bindings=False)
+        tuple(translator.visit_Variable(v) for v in variables)
         for constraint in constraints:
             if replace_constants:
                 constraint = simplify(replace(constraint, constant_bindings))
                 # if no variables then it is a constant
                 if isinstance(constraint, Constant) and constraint.value == True:
                     continue
-
+            # Translate one constraint
             translator.visit(constraint)
+
         if replace_constants:
             for k, v in constant_bindings.items():
                 translator.visit(k == v)
 
-        for name, exp, smtlib in translator.bindings:
-            if isinstance(exp, BitVec):
-                result += f"(declare-fun {name} () (_ BitVec {exp.size}))"
-            elif isinstance(exp, Bool):
-                result += f"(declare-fun {name} () Bool)"
-            elif isinstance(exp, Array):
-                result += f"(declare-fun {name} () (Array (_ BitVec {exp.index_bits}) (_ BitVec {exp.value_bits})))"
-            else:
-                raise ConstraintException(f"Type not supported {exp!r}")
-            result += f"(assert (= {name} {smtlib}))\n"
-
-        constraint_str = translator.pop()
-        while constraint_str is not None:
-            if constraint_str != "true":
-                result += f"(assert {constraint_str})\n"
-            constraint_str = translator.pop()
-        return result
+        return translator.smtlib()
 
     def _declare(self, var):
         """ Declare the variable `var` """
@@ -238,6 +210,10 @@ def _declare(self, var):
         self._declarations[var.name] = var
         return var
 
+    @property
+    def variables(self):
+        return self._declarations.values()
+
     def get_declared_variables(self):
         """ Returns the variable expressions of this constraint set """
         return self._declarations.values()
@@ -298,18 +274,18 @@ def is_declared(self, expression_var) -> bool:
         return any(expression_var is x for x in self.get_declared_variables())
 
     def migrate(self, expression, name_migration_map=None):
-        """ Migrate an expression created for a different constraint set to self.
-            Returns an expression that can be used with this constraintSet
+        """Migrate an expression created for a different constraint set to self.
+        Returns an expression that can be used with this constraintSet
 
-            All the foreign variables used in the expression are replaced by
-            variables of this constraint set. If the variable was replaced before
-            the replacement is taken from the provided migration map.
+        All the foreign variables used in the expression are replaced by
+        variables of this constraint set. If the variable was replaced before
+        the replacement is taken from the provided migration map.
 
-            The migration mapping is updated with new replacements.
+        The migration mapping is updated with new replacements.
 
-            :param expression: the potentially foreign expression
-            :param name_migration_map: mapping of already migrated variables. maps from string name of foreign variable to its currently existing migrated string name. this is updated during this migration.
-            :return: a migrated expression where all the variables are local. name_migration_map is updated
+        :param expression: the potentially foreign expression
+        :param name_migration_map: mapping of already migrated variables. maps from string name of foreign variable to its currently existing migrated string name. this is updated during this migration.
+        :return: a migrated expression where all the variables are local. name_migration_map is updated
 
         """
         if name_migration_map is None:
@@ -343,16 +319,16 @@ def migrate(self, expression, name_migration_map=None):
                 # Create and declare a new variable of given type
                 if isinstance(foreign_var, Bool):
                     new_var = self.new_bool(name=migrated_name)
-                elif isinstance(foreign_var, BitVec):
+                elif isinstance(foreign_var, Bitvec):
                     new_var = self.new_bitvec(foreign_var.size, name=migrated_name)
                 elif isinstance(foreign_var, Array):
                     # Note that we are discarding the ArrayProxy encapsulation
                     new_var = self.new_array(
-                        index_max=foreign_var.index_max,
-                        index_bits=foreign_var.index_bits,
-                        value_bits=foreign_var.value_bits,
+                        length=foreign_var.length,
+                        index_size=foreign_var.index_size,
+                        value_size=foreign_var.value_size,
                         name=migrated_name,
-                    ).array
+                    )
                 else:
                     raise NotImplementedError(
                         f"Unknown expression type {type(foreign_var)} encountered during expression migration"
@@ -367,11 +343,11 @@ def migrate(self, expression, name_migration_map=None):
         return migrated_expression
 
     def new_bool(self, name=None, taint=frozenset(), avoid_collisions=False):
-        """ Declares a free symbolic boolean in the constraint store
-            :param name: try to assign name to internal variable representation,
-                         if not unique, a numeric nonce will be appended
-            :param avoid_collisions: potentially avoid_collisions the variable to avoid name collisions if True
-            :return: a fresh BoolVariable
+        """Declares a free symbolic boolean in the constraint store
+        :param name: try to assign name to internal variable representation,
+                     if not unique, a numeric nonce will be appended
+        :param avoid_collisions: potentially avoid_collisions the variable to avoid name collisions if True
+        :return: a fresh BoolVariable
         """
         if name is None:
             name = "B"
@@ -380,16 +356,16 @@ 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)
+        var = BoolVariable(name=name, taint=taint)
         return self._declare(var)
 
     def new_bitvec(self, size, name=None, taint=frozenset(), avoid_collisions=False):
-        """ Declares a free symbolic bitvector in the constraint store
-            :param size: size in bits for the bitvector
-            :param name: try to assign name to internal variable representation,
-                         if not unique, a numeric nonce will be appended
-            :param avoid_collisions: potentially avoid_collisions the variable to avoid name collisions if True
-            :return: a fresh BitVecVariable
+        """Declares a free symbolic bitvector in the constraint store
+        :param size: size in bits for the bitvector
+        :param name: try to assign name to internal variable representation,
+                     if not unique, a numeric nonce will be appended
+        :param avoid_collisions: potentially avoid_collisions the variable to avoid name collisions if True
+        :return: a fresh BitvecVariable
         """
         if size <= 0:
             raise ValueError(f"Bitvec size ({size}) can't be equal to or less than 0")
@@ -400,28 +376,28 @@ 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)
+        var = BitvecVariable(size=size, name=name, taint=taint)
         return self._declare(var)
 
     def new_array(
         self,
-        index_bits=32,
+        index_size=32,
         name=None,
-        index_max=None,
-        value_bits=8,
+        length=None,
+        value_size=8,
         taint=frozenset(),
         avoid_collisions=False,
         default=None,
     ):
-        """ Declares a free symbolic array of value_bits long bitvectors in the constraint store.
-            :param index_bits: size in bits for the array indexes one of [32, 64]
-            :param value_bits: size in bits for the array values
-            :param name: try to assign name to internal variable representation,
-                         if not unique, a numeric nonce will be appended
-            :param index_max: upper limit for indexes on this array (#FIXME)
-            :param avoid_collisions: potentially avoid_collisions the variable to avoid name collisions if True
-            :param default: default for not initialized values
-            :return: a fresh ArrayProxy
+        """Declares a free symbolic array of value_size long bitvectors in the constraint store.
+        :param index_size: size in bits for the array indexes one of [32, 64]
+        :param value_size: size in bits for the array values
+        :param name: try to assign name to internal variable representation,
+                     if not unique, a numeric nonce will be appended
+        :param length: upper limit for indexes on this array (#FIXME)
+        :param avoid_collisions: potentially avoid_collisions the variable to avoid name collisions if True
+        :param default: default for not initialized values
+        :return: a fresh ArrayProxy
         """
         if name is None:
             name = "A"
@@ -430,5 +406,14 @@ 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)
+        var = self._declare(
+            ArrayVariable(
+                index_size=index_size,
+                length=length,
+                value_size=value_size,
+                name=name,
+                taint=taint,
+                default=default,
+            )
+        )
+        return var