evm: aggressively check & migrate expressions into current ConstraintSet in case they are global/external

[feliam]

this pr introduces advanced functionality (state.migrate_expression, and friends) for migration of potentially external/global ("foreign") expression objects into a particular ConstraintSet. with recent developments in the Ethereum API specifically (global expressions via `ManticoreEVM.make_....1), we expect foreign expressions to be passed into these interfaces fairly frequently now, so that PR "aggressively" adds a call to this function in nearly every interface that accepts an expression object, in order to be as safe as possible

from manticore.ethereum import ManticoreEVM
from manticore.core.smtlib import Operators
from manticore.core.smtlib import solver

m = ManticoreEVM()

contract_src='''
contract Overflow {
  uint public sellerBalance=0;

  function add(uint value)public  returns (bool){
      sellerBalance += value;
  }
}
'''

owner_account=m.create_account(balance=1000)
attacker_account=m.create_account(balance=1000)
contract_account=m.solidity_create_contract(contract_src,
                                            owner=owner_account,
                                            balance=0)

#Some global expression `sym_add1` 
sym_add1 = m.make_symbolic_value(name='sym_add1')
#Let's constraint it on the global fake constraintset
m.constrain(sym_add1>0)
m.constrain(sym_add1<10)
#Symb tx 1
contract_account.add(sym_add1, caller=attacker_account)

# A new!? global expression 
sym_add2 = m.make_symbolic_value(name='sym_add2')
#constraints involve old expression.  Some states may get invalidated by this. Should this be accepted?
m.constrain(sym_add1 > sym_add2)
#Symb tx 2
contract_account.add(sym_add2, caller=attacker_account)

#random concrete tx
contract_account.sellerBalance(caller=attacker_account)

#anooother constraining on the global constraintset. Yet more running states could get unfeasible by this.
m.constrain(sym_add1 > 8)



for state_num, state in enumerate(m.all_states):

    if state.is_feasible():
        #todo merge with some expression got froms state
        print ('feasible state found')
        print ('sym_add1', state.solve_one(sym_add1))
        print ('sym_add2', state.solve_one(sym_add2))
        m.generate_testcase(state, 'test{}'.format(state_num))

---

This change is 

[offlinemark]

ConstraintSet.get_variable() 😍

[offlinemark]

If a user does something like cs.new_bitvec(name='myvar') then that variable will get a new name like myvar_1 via _get_new_name. that new name is what's used as the dict key. so if a user then goes to do cs.get_variable('myvar') it won't work, right?

[feliam]

I guess so. The name= is then a suggestion. User should do a cs.get_variable(var.name) -> var

[offlinemark]

I see. that's very non-obvious :)

why do we need to do the _get_new_name thing? could we throw an error if a name is passed that already exists? or have an optional flag to do the new name thing?

from a user perspective it would be very nice to just pick a name for the variable and be able to use that throughout.

[feliam]

If it does not exist the name the user picked would be the same as in the returned var.name.
Throwing when already exists will pull in a lot of try:except:
How would the new signature of new_bitvec? We can also change name for suggestedname :)
pyz3 returns the old variable with the same name on that 🤷‍♀️

[offlinemark]

If it does not exist the name the user picked would be the same as in the returned var.name

it looks to me like we unconditionally append digits and change the name

my mistake, didn't read the pr closely enough yet.

manticore/manticore/core/smtlib/constraints.py

Line 245 in 59a5ff0

name = self._get_new_name(name)

How would the new signature of new_bitvec?

very roughly, here's an idea

# ignoring self, size, taint
def new_bitvec(name, avoid_name_collision=False)
    if avoid_name_collision:
        if name exists:
            name = get_name_name(name)
    else:
        if name exists:
            raise Exception
    return BitVecVariable(name)

[feliam]

if we want to ref them as bytes should probably just store them as bytes rather than decoding every item on each access to signatures.

since its a hex string, should probably just be str no? this is where python static typing stuff would be handy

[feliam]

rename=True/False instead of avoid_name_collision=True/False ?
Also if "avoid_name_collision=False" should it raise or return the old known version of the variable (In which case we'll need to remove the "new_" from the name) ?

[offlinemark]

rename=True/False instead of avoid_name_collision=True/False ?

i do think avoid_name_collision is pretty clunky, i didn't put much thought into it :) . but i'm not sure if rename is expressive enough. maybe strict=? avoid_collision

alternatively what if we have

new_bitvec(name=None, prefix=None).

if you specify name, it must not exist, otherwise an error will be thrown.
if you specify prefix, you don't care, and things will be appended to it to make it unique.
it is an error to specify both.
if none are specified, and random name default name/prefix will be chosen.

Also if "avoid_name_collision=False" should it raise or return the old known version of the variable (In which case we'll need to remove the "new_" from the name) ?

I think it should raise there. trying to a create a "new" one with an existing name is an error condition imo. users should probably check to see if a name exists before trying to make a new one. i guess they would use get_variable() for this check?

[offlinemark]

my understanding is that there two main users of the new_bitvec etc class of functions.

1. external users
2. the manticore core

the name= interface is geared for the external users, who have a specific variable in mind they want to create, and want to attach a name to it so they can find it later. since they want to find it later, we should not change it, and raise an exception.

the prefix= interface is meant for the manticore core, for example places like here

manticore/manticore/core/smtlib/solver.py

Line 406 in 24cb4bd

aux = temp_cs.new_bitvec(X.size, name='optimized_')

where the name is somewhat auto generated, and doesn't particularly matter to anyone anyway, so it's fine to change it.

this could all be overcomplicating things though. i'm fine with the name=, bool_flag= interface, and i think either rename= or avoid_collisions= would be good. i'm happy with either, @feliam i'll let you choose :)

[offlinemark]

Reviewable status: 0 of 5 files reviewed, 2 unresolved discussions (waiting on @feliam)

---

manticore/core/state.py, line 211 at r4 (raw file):

        label = options.get('label', 'buffer')
        taint = options.get('taint', frozenset())
        expr = self._constraints.new_array(name=label, index_max=nbytes, value_bits=8, taint=taint, avoid_collisions=True)

since this is a user API, I think this should be avoid_collisions=False, if they gave a label/name, otherwise avoid_collissions=True. same below

[offlinemark]

this looks awesome, really great work! i don't have a lot of really substantial comments. a lot of it is naming/readability related. a few thoughts on use of avoid_collisions

Reviewable status: 0 of 5 files reviewed, 15 unresolved discussions (waiting on @feliam)

---

manticore/ethereum.py, line 1198 at r4 (raw file):

                                value=100000 )
        '''
        return self.constraints.new_array(index_bits=256, name=name, index_max=size, value_bits=8, taint=frozenset(), avoid_collisions=True)

i'm also thinking avoid_collisions here should depend on whether a name was given

---

manticore/ethereum.py, line 1239 at r4 (raw file):

                state_constraints = state.constraints

                migration_bindings = state.context.get('migration_bindings')

can be simplified to .get('migration_bindings', {})

---

manticore/ethereum.py, line 1242 at r4 (raw file):

                if migration_bindings is None:
                    migration_bindings = {}
                migrated_constraint = state_constraints.migrate(constraint, migration_bindings=migration_bindings)

we should use state.migrate_expression here? it looks copypastad

---

manticore/ethereum.py, line 1784 at r4 (raw file):

        return self.accounts[name]

    def __migrate_tx_expressions(self, state, caller, address, value, data):

nit, i think we should use 1 underscore here. 2 means something special i think

---

manticore/ethereum.py, line 1796 at r4 (raw file):

            if migration_bindings is None:
                migration_bindings = {}
            if issymbolic(caller):

imo we should add some comments here to explain why, it's not super obvious. I guess the reason is that commonly users will be making these symbolic by creating global symbolic variables via ManticoreEVM.make_.... and those global expressions need to be imported into each state when a tx actually happens

---

manticore/core/state.py, line 281 at r4 (raw file):

    def can_be_true(self, expr):
        expr = self.migrate_expression(expr)

i wonder if it's necessary to sprinkle this everywhere now. maybe the user should be aware when they are mixing expressions with unrelated states/constraintsets and call migrate_expression first?

---

manticore/core/smtlib/constraints.py, line 213 at r4 (raw file):

        return self.to_string()

    def _get_new_name(self, name='VAR'):

nit, while we're here maybe we can rename this to _make_unique_name

---

manticore/core/smtlib/constraints.py, line 219 at r4 (raw file):

        return name

    def migrate(self, expression, migration_bindings=None):

maybe migrate_expression would be a better name here. it took me a bit to understand that the only affect on the state here was adding variables, but didn't automatically apply the expression/constraint. not totally sure about this, maybe migrate is enough. might be enough to just add some more details to the docstring on how this function basically just creates the needed variables in the constraint set

---

manticore/core/smtlib/constraints.py, line 225 at r4 (raw file):

            :param migration_bindings: a name to name mapping of already migrated variables
        '''
        if migration_bindings is None:

i think this name is also a bit confusing, rather than call them bindings, maybe "map". i think a little more verbose description of what this variable is would be useful.

---

manticore/core/smtlib/constraints.py, line 231 at r4 (raw file):

        #  Based on the name mapping in migration_bindings build an object to
        #  object mapping to be used in the replacing of variables
        fat_bindings = {}

i think we should choose a better name for fat_bindings, it's not very clear what it is based on the name. it's the actual map from "alient" expression object, to the newly created native object. maybe something like foreign_to_native_expression_map? but that is pretty verbose. i think throughout this code could be made more readable by deciding on a convention like "foreign"/"native" or alien/local etc etc and using those in the variable names throughout. i can submit a PR with what i think could be more readable

---

manticore/core/smtlib/constraints.py, line 236 at r4 (raw file):

        for old_name in expression_variables:
            migrated_name = migration_bindings.get(old_name)
            if migrated_name in declared_names:

rather than have this declared_names variable, we could use self.get_variable for this check? e.g

native_var = self.get_variable(migrated_name)
if native_var is not None:
  fat_bindings[....] = native_var

it would make this a bit easier to read by reducing the number of local vars

---

manticore/core/smtlib/constraints.py, line 255 at r4 (raw file):

            if name in self._declarations:
                name = self._get_new_name(var.name + '_migrated')
            if name in self._declarations:

should we use a loop here? the point is to get a unique name right? loop bumping some int until we have a unique name?

---

manticore/core/smtlib/constraints.py, line 265 at r4 (raw file):

                new_var = self.new_array(index_max=var.index_max, index_bits=var.index_bits, value_bits=var.value_bits, name=name).array
            else:
                raise NotImplemented("Unknown type {}".format(type(var)))

this err msg could be a bit more verbose, "Unknown expression type encountered during expression migration"

[feliam]

---

manticore/core/smtlib/constraints.py, line 220 at r7 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

i understand the theoretical use of the name_migration_map, but im having trouble thinking of an actual use case. i don't think the code even really uses it right now. can you give an example of a use case?

The idea is that when you migrate the same variable twice it maps to the same local variable.

It maps alien names with local declared names.
If there are 2 alien variables (for example from 2 other different constraint sets) with the same name it will be a collision.
This name map get serialized with the state in the state context.

[feliam]

Reviewable status: 5 of 8 files reviewed, 6 unresolved discussions (waiting on @Mossberg and @feliam)

---

manticore/core/smtlib/constraints.py, line 215 at r5 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

we should just do if name in self._declarations

Done.

---

manticore/core/smtlib/constraints.py, line 269 at r5 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

I still don't see why we need to create that list of tuples. get_variables() returns a set. why can't we just iter through the set?

for expression_var in get_variables(expression):
  # blah blah expression_var.name

Done.

---

manticore/core/smtlib/constraints.py, line 271 at r5 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

ok, i reread this, and i'm still having trouble understanding it exactly.

--

is it correct to say that object_migration_map's keys should ALWAYS be external/foreign expressions, and its values should ALWAYS be internal/local expressions?

if this is the case, this invariant can be violated if

• expression_var is a local ConstraintSet variable
• expression_name is in migration_map and it's value corresponds to an expression that is also in this ConstraintSet

in which keys object_migration_map will record a mapping from a local expression to another local expression, which I don't understand, since there is no migration necessary in this case?

--

i'm also confused by this .get() call. is the intention for this loop body to do nothing if expression_name is not in the name_migration_map? right now i can see that it is implicitly doing nothing, because the .get() will return None, which will cause get_variable() to return None. however this is pretty convoluted. if this is the intention, I think we should have an explicit if migrated_name is None: continue line

is it correct to say that object_migration_map's keys should ALWAYS be external/foreign expressions, and its values should ALWAYS be internal/local expressions? that's correct.

Let see how the new arrangement holds up with that invariant in mind.. actually I'm adding it as a comment.

---

manticore/core/smtlib/constraints.py, line 284 at r5 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

i'm confused by this check in the first place. when would this if succeed?

shouldn't we instead be checking if var exists as a key in object_migration_map? the point here is to check if it already has a replacement assigned, right?

so right now we're checking if it's in the values. from what i see, all of the values in object_migration_map belong to the local ConstraintSet. therefore, they would appear in get_declared_variables, and above get_declared_variables check would succeed. so i don't quite see how we would get past this if.

Done.

---

manticore/core/smtlib/constraints.py, line 216 at r8 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

i'd like to add a comment here

"the while loop is necessary because appending the result of _get_sid() is not guaranteed to make a unique name on the first try; a colliding name could have been added previously"

Done.

[offlinemark]

great, algorithm looks sound to me now, and i love that it's not 2 loops :)

Reviewed 3 of 3 files at r9.
Reviewable status: all files reviewed, 9 unresolved discussions (waiting on @feliam)

---

manticore/core/smtlib/constraints.py, line 223 at r9 (raw file):

        return name

    def migrate(self, expression, name_migration_map=None):

ok, i finally understand name_migration_map. it took a while for it to click to me that this is persistently stored in the State and passed into this on each migration. I think to make this code more readable, I'd like to propose renaming name_migration_map to previously_migrated_map

---

manticore/core/smtlib/constraints.py, line 234 at r9 (raw file):

            ```
            from manticore.core.smtlib import *

now that there's a unit test can we rm this? it will just become bitrotted and outdated.

---

manticore/core/smtlib/constraints.py, line 261 at r9 (raw file):

            :param expression: the potentially foreign expression
            :param name_migration_map: a name to name mapping of already migrated variables

would like to expand on this:

:param previously_migrated_map: mapping of already migrated variables. maps from string name of foreign variable to its currently existing migrated string name

---

manticore/core/smtlib/constraints.py, line 278 at r9 (raw file):

            # do nothing if it is a known/declared variable object
            if any(expression_var is x for x in self.get_declared_variables()):

this strikes me as worth being a ConstraintSet method. will make this already complex function easier to read. if self.is_declared(expression_var) or if expression_var in self?

---

manticore/core/smtlib/constraints.py, line 285 at r9 (raw file):

                migrated_name = name_migration_map[expression_var.name]
                native_var = self.get_variable(migrated_name)
                if native_var is None:

this actually looks more appropriate for an assert to me. this is not an error condition that we expect to ever happen, assert native_var is not None is a strict invariant? it seems like a serious internal error if name_migration_map/previously_migrated_map contains a value which does not exist.

---

manticore/core/smtlib/constraints.py, line 286 at r9 (raw file):

                native_var = self.get_variable(migrated_name)
                if native_var is None:
                    raise Exception("name_migration_map contains an unknown variable")

i'd say "contains a variable that does not exist in this ConstraintSet" to be very clear

---

manticore/core/smtlib/constraints.py, line 289 at r9 (raw file):

                object_migration_map[expression_var] = native_var
                #continue if there is already a migrated variable for it
                continue

i think we would also improve the readability by removing the "continue" and using an explicit "else" block for the below block where a new_var is created. what do you think?

if expression_var in self: # or whatever
  continue

# what about this? just for readability I guess. at this point, we've confirmed it's foreign. this naming throughout helps the reader understand the key invariant commented above.
foreign_var = expression_var


if foreign_var.name in previously_migrated_map:
    #
    native_var = ....
else:
    # make new_var

    native_var = new_var
    previously_migrated[foreign_var.name] = new_var.name

object_migration_map[foreign_var] = native_var

---

manticore/core/smtlib/constraints.py, line 292 at r9 (raw file):

            # expression_var was not found in the local declared variables nor
            # any variable with the dsame name was previously migrated

dsame typo

---

tests/test_models.py, line 30 at r9 (raw file):

    def _clear_constraints(self):
        self.state.context['migration_map']=None

why is this necessary exactly? should the migration stuff be able to gracefully default if 'migration_map' is not in the context? migration stuff has no relevance to model tests, so i don't really think this should be here.

[feliam]

Reviewable status: all files reviewed, 9 unresolved discussions (waiting on @feliam and @Mossberg)

---

manticore/core/smtlib/constraints.py, line 234 at r9 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

now that there's a unit test can we rm this? it will just become bitrotted and outdated.

Done.

---

manticore/core/smtlib/constraints.py, line 278 at r9 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

this strikes me as worth being a ConstraintSet method. will make this already complex function easier to read. if self.is_declared(expression_var) or if expression_var in self?

Done.

---

manticore/core/smtlib/constraints.py, line 285 at r9 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

this actually looks more appropriate for an assert to me. this is not an error condition that we expect to ever happen, assert native_var is not None is a strict invariant? it seems like a serious internal error if name_migration_map/previously_migrated_map contains a value which does not exist.

Done.

---

manticore/core/smtlib/constraints.py, line 289 at r9 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

i think we would also improve the readability by removing the "continue" and using an explicit "else" block for the below block where a new_var is created. what do you think?

if expression_var in self: # or whatever
  continue

# what about this? just for readability I guess. at this point, we've confirmed it's foreign. this naming throughout helps the reader understand the key invariant commented above.
foreign_var = expression_var


if foreign_var.name in previously_migrated_map:
    #
    native_var = ....
else:
    # make new_var

    native_var = new_var
    previously_migrated[foreign_var.name] = new_var.name

object_migration_map[foreign_var] = native_var

I tried to pre-filter the list of variable so we do not need to "continue"

---

manticore/core/smtlib/constraints.py, line 292 at r9 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

dsame typo

Done.

---

tests/test_models.py, line 30 at r9 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

why is this necessary exactly? should the migration stuff be able to gracefully default if 'migration_map' is not in the context? migration stuff has no relevance to model tests, so i don't really think this should be here.

This is trying to clean the constraints of a constraintset in a state and re use it. If you keep old migration mappings there is trouble. I can skip the test that make problem if you prefer and you fix them later?

[offlinemark]

Reviewable status: 7 of 8 files reviewed, 5 unresolved discussions (waiting on @Mossberg and @feliam)

---

manticore/core/smtlib/constraints.py, line 227 at r10 (raw file):

        if not isinstance(expression_var, Variable):
            raise ValueError("Expression must be a Variable")
        return any(expression_var is x for x in self.get_declared_variables()):

watch out! stray colon!

[offlinemark]

Reviewed 1 of 1 files at r10.
Reviewable status: all files reviewed, 3 unresolved discussions (waiting on @feliam)

---

manticore/core/smtlib/constraints.py, line 242 at r10 (raw file):

            :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 expresion where all the variables are fresh BoolVariable. name_migration_map is updated

are all the variables in the returned expression BoolVariable? couldn't they just be regular variables? for example, if a BitVecAdd with 2 BitVec children was "migrated", wouldn't the returned expression look the same? There would be no BoolVariables?

---

manticore/core/smtlib/constraints.py, line 265 at r10 (raw file):

                assert native_var is not None, "name_migration_map contains a variable that does not exist in this ConstraintSet"
                object_migration_map[foreign_var] = native_var
                #continue if there is already a migrated variable for it

don't need this comment anymore

[yan]

Reviewable status: all files reviewed, 5 unresolved discussions (waiting on @feliam)

---

manticore/core/smtlib/constraints.py, line 173 at r10 (raw file):

    def get_variable(self, name):
        ''' Returns the variable declared under name or None if it does not exists '''
        if name not in self._declarations:

return self._declarations.get(name, None)?

---

manticore/core/smtlib/constraints.py, line 275 at r10 (raw file):

                    migrated_name = self._make_unique_name(foreign_var.name + '_migrated')
                # Create and declare a new variable of given type
                if isinstance(foreign_var, Bool):

This pattern comes up pretty regularly (in Solver.get_all_values, Solver.get_value, here), should we make a Expression.clone() method that a few relevant classes can override?

[offlinemark]

Reviewable status: all files reviewed, 5 unresolved discussions (waiting on @feliam)

---

manticore/core/smtlib/constraints.py, line 275 at r10 (raw file):

Previously, yan (Yan Ivnitskiy) wrote…

This pattern comes up pretty regularly (in Solver.get_all_values, Solver.get_value, here), should we make a Expression.clone() method that a few relevant classes can override?

i generally agree, but i think we should save that for a different PR. this one already has a lot of complexity

[feliam]

Reviewable status: all files reviewed, 5 unresolved discussions (waiting on @feliam, @Mossberg, and @yan)

---

manticore/core/smtlib/constraints.py, line 242 at r10 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

are all the variables in the returned expression BoolVariable? couldn't they just be regular variables? for example, if a BitVecAdd with 2 BitVec children was "migrated", wouldn't the returned expression look the same? There would be no BoolVariables?

Done.

---

manticore/core/smtlib/constraints.py, line 265 at r10 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

don't need this comment anymore

Done.

---

manticore/core/smtlib/constraints.py, line 275 at r10 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

i generally agree, but i think we should save that for a different PR. this one already has a lot of complexity

diff pr

[offlinemark]

Reviewed 1 of 1 files at r11.
Reviewable status: all files reviewed, 2 unresolved discussions (waiting on @feliam and @yan)

---

manticore/core/smtlib/constraints.py, line 173 at r10 (raw file):

Previously, yan (Yan Ivnitskiy) wrote…

return self._declarations.get(name, None)?

+1

[feliam]

Reviewable status: all files reviewed, 2 unresolved discussions (waiting on @yan)

---

manticore/core/smtlib/constraints.py, line 173 at r10 (raw file):

Previously, mossberg (Mark Mossberg) wrote…

+1

Done.

---

manticore/core/smtlib/constraints.py, line 275 at r10 (raw file):

Previously, feliam (feliam) wrote…

diff pr

Let's make an issue maybe?

[feliam]

---

manticore/core/smtlib/constraints.py, line 275 at r10 (raw file):

Previously, feliam (feliam) wrote…

Let's make an issue maybe?

#1059
done!

[feliam]

Reviewable status: 7 of 8 files reviewed, 2 unresolved discussions (waiting on @Mossberg and @yan)

---

manticore/core/smtlib/constraints.py, line 275 at r10 (raw file):

Previously, feliam (feliam) wrote…

#1059
done!

Done.

[offlinemark]

Reviewed 1 of 1 files at r12, 1 of 1 files at r13.
Reviewable status: all files reviewed, 2 unresolved discussions (waiting on @yan)