Merge branch 'master' into improve-solidity-create-contract-ux

* master:
  Ensure native deps (better error message) (#1367)
  Make sys_lseek return offset location (#1355)
  Fix a typo in the documentation (#1360)
  Refactor tests structure (#1352)
  Dev single gas calc (#1353)
  Symbolic memory model bugfixes (#1350)
  Refactor not-existing SValue into BitVecVariable
  Config with context (#1345)
  Update Capstone to 4.0.1 (#1312)
  evm: fix _check_jumpdest when run with detectors (#1347)
  Move tx default gas value to config (#1346)

.travis.yml

@@ -18,8 +18,9 @@ env:
     - PYTHONWARNINGS="default::ResourceWarning" # Enable ResourceWarnings
   matrix:
     - TEST_TYPE=examples
-    - TEST_TYPE=tests
-    - TEST_TYPE=eth
+    - TEST_TYPE=ethereum
+    - TEST_TYPE=native
+    - TEST_TYPE=other
 
 branches:
   only:

docs/gotchas.rst

@@ -22,7 +22,7 @@ An example of a global context race condition, when modifying two context entrie
 
     m.context['flag1'] += ['a']
     --- interrupted by other worker
-    m.context['flag2] += ['b']
+    m.context['flag2'] += ['b']
 
 Client code should use the :meth:`~manticore.core.ManticoreBase.locked_context` API::
 

manticore/__main__.py

@@ -40,6 +40,7 @@ def main():
     if args.argv[0].endswith('.sol'):
         ethereum_main(args, logger)
     else:
+        install_helper.ensure_native_deps()
         native_main(args, logger)
 
 

manticore/ethereum/manticore.py

@@ -29,6 +29,9 @@
 
 logger = logging.getLogger(__name__)
 
+cfg = config.get_group('evm')
+cfg.add('defaultgas', 3000000, 'Default gas value for ethereum transactions.')
+
 
 def flagged(flag):
     """
@@ -571,7 +574,7 @@ def make_symbolic_arguments(self, types):
 
     def solidity_create_contract(self, source_code, owner, name=None, contract_name=None, libraries=None,
                                  balance=0, address=None, args=(), solc_bin=None, solc_remaps=[],
-                                 working_dir=None, gas=3000000):
+                                 working_dir=None, gas=None):
         """ Creates a solidity contract and library dependencies
 
             :param str source_code: solidity source code
@@ -580,7 +583,7 @@ def solidity_create_contract(self, source_code, owner, name=None, contract_name=
             :param contract_name: Name of the contract to analyze (optional if there is a single one in the source code)
             :type contract_name: str
             :param balance: balance to be transferred on creation
-            :type balance: int or SValue
+            :type balance: int or BitVecVariable
             :param address: the address for the new contract (optional)
             :type address: int or EVMAccount
             :param tuple args: constructor arguments
@@ -664,13 +667,13 @@ def get_nonce(self, address):
         else:
             return next(iter(nonces))
 
-    def create_contract(self, owner, balance=0, address=None, init=None, name=None, gas=3000000):
+    def create_contract(self, owner, balance=0, address=None, init=None, name=None, gas=None):
         """ Creates a contract
 
             :param owner: owner account (will be default caller in any transactions)
             :type owner: int or EVMAccount
             :param balance: balance to be transferred on creation
-            :type balance: int or SValue
+            :type balance: int or BitVecVariable
             :param int address: the address for the new contract (optional)
             :param str init: initializing evm bytecode and arguments
             :param str name: a unique name for reference
@@ -728,15 +731,15 @@ def new_address(self):
             if new_address not in all_addresses:
                 return new_address
 
-    def transaction(self, caller, address, value, data, gas=21000):
+    def transaction(self, caller, address, value, data, gas=None):
         """ Issue a symbolic transaction in all running states
 
             :param caller: the address of the account sending the transaction
             :type caller: int or EVMAccount
             :param address: the address of the contract to call
             :type address: int or EVMAccount
             :param value: balance to be transfered on creation
-            :type value: int or SValue
+            :type value: int or BitVecVariable
             :param data: initial data
             :param gas: gas budget
             :raises NoAliveStates: if there are no alive states to execute
@@ -747,7 +750,7 @@ def create_account(self, balance=0, address=None, code=None, name=None):
         """ Low level creates an account. This won't generate a transaction.
 
             :param balance: balance to be set on creation (optional)
-            :type balance: int or SValue
+            :type balance: int or BitVecVariable
             :param address: the address for the new account (optional)
             :type address: int
             :param code: the runtime code for the new account (None means normal account) (optional)
@@ -839,25 +842,27 @@ def _migrate_tx_expressions(self, state, caller, address, value, data):
 
             return caller, address, value, data
 
-    def _transaction(self, sort, caller, value=0, address=None, data=None, gaslimit=0, price=1):
+    def _transaction(self, sort, caller, value=0, address=None, data=None, gaslimit=None, price=1):
         """ Initiates a transaction
 
             :param caller: caller account
             :type caller: int or EVMAccount
             :param int address: the address for the transaction (optional)
             :param value: value to be transferred
             :param price: the price of gas for this transaction. Mostly unused.
-            :type value: int or SValue
+            :type value: int or BitVecVariable
             :param str data: initializing evm bytecode and arguments or transaction call data
             :param gaslimit: gas budget
             :rtype: EVMAccount
         """
-        #Type Forgiveness
+        if gaslimit is None:
+            gaslimit = cfg.defaultgas
+        # Type Forgiveness
         if isinstance(address, EVMAccount):
             address = int(address)
         if isinstance(caller, EVMAccount):
             caller = int(caller)
-        #Defaults, call data is empty
+        # Defaults, call data is empty
         if data is None:
             data = bytearray(b"")
         if isinstance(data, (str, bytes)):
@@ -1021,8 +1026,7 @@ def multi_tx_analysis(self, solidity_filename, working_dir=None, contract_name=N
                 self.transaction(caller=tx_account[min(tx_no, len(tx_account) - 1)],
                                  address=contract_account,
                                  data=symbolic_data,
-                                 value=value,
-                                 gas=2100000)
+                                 value=value)
                 logger.info("%d alive states, %d terminated states", self.count_running_states(), self.count_terminated_states())
             except NoAliveStates:
                 break

manticore/native/cpu/x86.py

@@ -583,7 +583,7 @@ def _update_cache(self, name, value):
             self._cache.pop(affected, None)
 
     def read(self, name):
-        name = self._alias(name)
+        name = str(self._alias(name))
         if name in ('ST0', 'ST1', 'ST2', 'ST3', 'ST4', 'ST5', 'ST6', 'ST7'):
             name = f'FP{((self.read("TOP") + int(name[2])) & 7)}'
         if name in self._cache:

manticore/platforms/evm.py

@@ -902,12 +902,12 @@ def _push_results(self, instruction, result):
             assert instruction.pushes == 0
             assert result is None
 
-    def _calculate_extra_gas(self, *arguments):
+    def _calculate_gas(self, *arguments):
         current = self.instruction
         implementation = getattr(self, f"{current.semantics}_gas", None)
         if implementation is None:
-            return 0
-        return implementation(*arguments)
+            return current.fee
+        return current.fee + implementation(*arguments)
 
     def _handler(self, *arguments):
         current = self.instruction
@@ -933,7 +933,7 @@ def _checkpoint(self):
             #FIXME Not clear which exception should trigger first. OOG or insuficient stack
             # this could raise an insuficient stack exception
             arguments = self._pop_arguments()
-            fee = instruction.fee + self._calculate_extra_gas(*arguments)
+            fee = self._calculate_gas(*arguments)
             self._checkpoint_data = (pc, old_gas, instruction, arguments, fee, allocated)
         return self._checkpoint_data
 
@@ -972,7 +972,10 @@ def _check_jmpdest(self):
 
         if should_check_jumpdest:
             self._check_jumpdest = False
-            if self.pc not in self._valid_jumpdests:
+
+            pc = self.pc.value if isinstance(self.pc, Constant) else self.pc
+
+            if pc not in self._valid_jumpdests:
                 raise InvalidOpcode()
 
     def _advance(self, result=None, exception=False):
@@ -2023,6 +2026,7 @@ def _close_transaction(self, result, data=None, rollback=False):
         else:
             self._deleted_accounts = deleted_accounts
 
+            #FIXME: BUG: a CREATE can be succesfull and still return an empty contract :shrug:
             if not issymbolic(tx.caller) and (tx.sort == 'CREATE' or not self._world_state[tx.caller]['code']):
                 # Increment the nonce if this transaction created a contract, or if it was called by a non-contract account
                 self.increase_nonce(tx.caller)
@@ -2426,7 +2430,7 @@ def create_account(self, address=None, balance=0, code=None, storage=None, nonce
 
         return address
 
-    def create_contract(self, price=0, address=None, caller=None, balance=0, init=None, gas=2300):
+    def create_contract(self, price=0, address=None, caller=None, balance=0, init=None, gas=None):
         """
         Create a contract account. Sends a transaction to initialize the contract
 

manticore/platforms/linux.py

@@ -1248,19 +1248,17 @@ def sys_lseek(self, fd, offset, whence):
                        SEEK_CUR: The file offset is set to its current location plus offset bytes.
                        SEEK_END: The file offset is set to the size of the file plus offset bytes.
 
-        :return: 0 (Success), or EBADF (fd is not a valid file descriptor or is not open)
+        :return: offset from file beginning, or EBADF (fd is not a valid file descriptor or is not open)
 
         '''
         signed_offset = self._to_signed_dword(offset)
         try:
-            self._get_fd(fd).seek(signed_offset, whence)
+            return self._get_fd(fd).seek(signed_offset, whence)
         except FdError as e:
             logger.info(("LSEEK: Not valid file descriptor on lseek."
                          "Fd not seekable. Returning EBADF"))
             return -e.err
 
-        return 0
-
     def sys_read(self, fd, buf, count):
         data: bytes = bytes()
         if count != 0:

manticore/utils/config.py

@@ -47,6 +47,13 @@ class _Group:
     And then use their value in the code as:
         group.some_var
 
+    Can also be used with a `with-statement context` so it would revert the value, e.g.:
+    group.var = 100
+    with group.temp_vals():
+        group.var = 123
+        # group.var is 123 for the time of with statement
+    # group.var is back to 100
+
     Note that it is not recommended to use it as a default argument value for a function as it will be evaluated once.
     Also don't forget that a given variable can be set through CLI or .yaml file!
     (see config.py)
@@ -114,9 +121,10 @@ def _var_object(self, name: str) -> _Var:
         return self._vars[name]
 
     def __getattr__(self, name):
-        if name not in self._vars:
+        try:
+            return self._vars[name].value
+        except KeyError:
             raise AttributeError(f"Group '{self.name}' has no variable '{name}'")
-        return self._vars[name].value
 
     def __setattr__(self, name, new_value):
         self._vars[name].value = new_value
@@ -127,6 +135,46 @@ def __iter__(self):
     def __contains__(self, key):
         return key in self._vars
 
+    def temp_vals(self) -> "_TemporaryGroup":
+        """
+        Returns a contextmanager that can be used to set temporary config variables.
+        E.g.:
+        group.var = 123
+
+        with group.temp_vals():
+            group.var = 456
+            # var is 456
+
+        # group.var is back to 123
+        """
+        return _TemporaryGroup(self)
+
+
+class _TemporaryGroup:
+    def __init__(self, group: _Group):
+        object.__setattr__(self, '_group', group)
+        object.__setattr__(self, '_entered', False)
+        object.__setattr__(self, '_saved', {k: v.value for k, v in group._vars.items()})
+
+    def __getattr__(self, item):
+        return getattr(self._grp, item)
+
+    def __setattr__(self, key, value):
+        if self._entered and key not in self._saved:
+            self._saved[key] = getattr(self._group, key).value
+
+    def __enter__(self):
+        if self._entered is True:
+            raise ConfigError("Can't use temporary group recursively!")
+
+        object.__setattr__(self, '_entered', True)
+
+    def __exit__(self, *_):
+        for k in self._saved:
+            setattr(self._group, k, self._saved[k])
+
+        object.__setattr__(self, '_entered', False)
+
 
 def get_group(name: str) -> _Group:
     """

scripts/travis_install.sh

@@ -10,9 +10,9 @@ function install_mcore {
     pip uninstall -y Manticore || echo "Manticore not cached"  # uninstall any old, cached Manticore
 
 
-    # We only need to install keystone if we're just running regular tests
+    # We only need to install keystone if we're running tests other than ethereum
     EXTRAS="dev-noks"
-    if [ "$1" = "tests" ]; then
+    if [ "$1" != "ethereum" ]; then
         EXTRAS="dev"
     fi