Merge branch 'master' into ekilmer-dev

* master: Symbolic model for strcpy (#1681) Rollback to support yices again (#1714) Fix default output space when workspace is in mem: (#1724) VMTests tests for istanbul (#1676) Snapshots & is_main (#1710) Fix Black (#1718) Use CoverageRC, Make CodeCov Less Aggressive (#1705) Fix plugin enable/disable magic (#1708) Add a warning when selected no methods for inclusion (#1707) Remove duplicated entries (#1709) Blacken (#1711)
trailofbits · Jun 15, 2020 · ae2eec3 · ae2eec3
2 parents 178e28f + bdbd039
commit ae2eec3
Show file tree

Hide file tree

Showing 99 changed files with 2,372 additions and 84,703 deletions.
diff --git a/.github/ISSUE_TEMPLATE/config.yml b/.github/ISSUE_TEMPLATE/config.yml
@@ -1,11 +1,5 @@
 blank_issues_enabled: false
 contact_links:
-  - name: Bug Report
-    url: https://github.com/trailofbits/manticore/issues/new?labels=bug&template=bug_report.md
-    about: Report a bug in Manticore
-  - name: Feature Request
-    url: https://github.com/trailofbits/manticore/issues/new?labels=idea&template=feature_request.md
-    about: Request a new feature in Manticore
   - name: Ask a Question
     url: https://github.com/trailofbits/manticore/discussions/new
     about: Ask for help or clarification from the developers

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -20,11 +20,13 @@ jobs:
     - name: Lint
       env:
         BASE_SHA: ${{ github.event.pull_request.base.sha }}
-        HEAD_SHA: ${{ github.event.pull_request.head.sha }}
       run: |
         pip install -e .[lint]
         black --version
-        git diff --name-only $BASE_SHA..$HEAD_SHA | python scripts/pyfile_exists.py | xargs black --diff --check
+        git fetch --depth=1 origin $BASE_SHA
+        echo "Files Changed:"
+        git diff --name-only $BASE_SHA... | tee .diff_names.txt
+        cat .diff_names.txt | python scripts/pyfile_exists.py | xargs black --diff --check
         mypy --version
         mypy
   tests:
@@ -46,6 +48,13 @@ jobs:
       env:
         TEST_TYPE: ${{ matrix.type }}
       run: |
+        #install cvc4
+        sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
+        sudo chmod +x /usr/bin/cvc4
+        #install yices
+        sudo add-apt-repository ppa:sri-csl/formal-methods
+        sudo apt-get update
+        sudo apt-get install yices2
         # Install solc unconditionally because it only takes a second or two
         sudo wget -O /usr/bin/solc https://github.com/ethereum/solidity/releases/download/v0.4.24/solc-static-linux
         sudo chmod +x /usr/bin/solc
@@ -56,6 +65,7 @@ jobs:
       run: |
         # Launches all examples; this assumes PWD is examples/script
         launch_examples() {
+            COVERAGE_RCFILE=$GITHUB_WORKSPACE/.coveragerc
             # concolic assumes presence of ../linux/simpleassert
             echo "Running concolic.py..."
             HW=../linux/helloworld
@@ -112,8 +122,8 @@ jobs:
                 echo "Automaking VMTests" `pwd`
                 cd ./tests/ && mkdir -p  ethereum_vm/VMTests_concrete && mkdir -p ethereum_vm/VMTests_symbolic
                 rm -Rf vmtests; git clone https://github.com/ethereum/tests --depth=1 vmtests
-                for i in ./vmtests/VMTests/*; do python ./auto_generators/make_VMTests.py $i; done
-                for i in ./vmtests/VMTests/*; do python ./auto_generators/make_VMTests.py $i --symbolic; done
+                for i in ./vmtests/BlockchainTests/ValidBlocks/VMTests/*/*json; do python ./auto_generators/make_VMTests.py -f istanbul -i $i -o ethereum_vm/VMTests_concrete; done
+                rm ethereum_vm/VMTests_concrete/test_loop*.py #too slow
                 rm -rf ./vmtests
                 touch ethereum_vm/.done
             fi
@@ -147,14 +157,15 @@ jobs:
         }
 
         run_truffle_tests(){
+            COVERAGE_RCFILE=$GITHUB_WORKSPACE/.coveragerc
             mkdir truffle_tests
             cd truffle_tests
             truffle unbox metacoin
-            coverage run -m manticore . --contract MetaCoin --workspace output
+            coverage run -m manticore . --contract MetaCoin --workspace output --exclude-all --evm.oog ignore --evm.txfail optimistic
             # Truffle smoke test. We test if manticore is able to generate states
             # from a truffle project. 
-            if [ "$(ls output/*tx -l | wc -l)" != "34" ]; then
-                echo "Truffle test failed" `ls output/*tx -l | wc -l` "!= 34"
+            if [ "$(ls output/*tx -l | wc -l)" != "26" ]; then
+                echo "Truffle test failed" `ls output/*tx -l | wc -l` "!= 26"
                 return 1
             fi
             echo "Truffle test succeded"
@@ -166,8 +177,9 @@ jobs:
 
         run_tests_from_dir() {
             DIR=$1
+            COVERAGE_RCFILE=$GITHUB_WORKSPACE/.coveragerc
             echo "Running only the tests from 'tests/$DIR' directory"
-            pytest --durations=100 --cov=manticore -n auto "tests/$DIR"
+            pytest --durations=100 --cov=manticore --cov-config=$GITHUB_WORKSPACE/.coveragerc -n auto "tests/$DIR"
             coverage xml
         }
 

diff --git a/README.md b/README.md
@@ -216,6 +216,23 @@ for idx, val_list in enumerate(m.collect_returns()):
 * We're still in the process of implementing full support for the EVM Istanbul instruction semantics, so certain opcodes may not be supported.
 In a pinch, you can try compiling with Solidity 0.4.x to avoid generating those instructions. 
 
+## Using a different solverr (Z3, Yices, CVC4)
+Manticore relies on an external solver supporting smtlib2. Curently Z3, Yices and CVC4 are supported and can be selected via commandline or configuration settings.
+By default Manticore will use Z3. Once you installed a different solver you can choose a different solver like this:
+```manticore --smt.solver yices```
+### Installing CVC4
+For more details go to https://cvc4.github.io/. Otherwise just get the binary and use it.
+
+        sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
+        sudo chmod +x /usr/bin/cvc4
+
+### Installing Yices
+Yices is incredibly fast. More details here https://yices.csl.sri.com/
+
+        sudo add-apt-repository ppa:sri-csl/formal-methods
+        sudo apt-get update
+        sudo apt-get install yices2
+
 ## Getting Help
 
 Feel free to stop by our #manticore slack channel in [Empire Hacking](https://empireslacking.herokuapp.com/) for help using or extending Manticore.

diff --git a/codecov.yml b/codecov.yml
@@ -6,3 +6,7 @@ codecov:
     # If we add or remove any, we need to change this number.
     after_n_builds: 9
     wait_for_ci: yes
+  status:
+    project:
+      default:
+        threshold: 0.2%
diff --git a/manticore/__init__.py b/manticore/__init__.py
@@ -8,5 +8,13 @@
 from .utils.log import set_verbosity
 from .core.smtlib import issymbolic, istainted
 from .ethereum.manticore import ManticoreEVM
+from .core.plugin import Plugin
+from .exceptions import ManticoreError
 
-__all__ = [issymbolic.__name__, istainted.__name__, ManticoreEVM.__name__, set_verbosity.__name__]
+__all__ = [
+    issymbolic.__name__,
+    istainted.__name__,
+    ManticoreEVM.__name__,
+    set_verbosity.__name__,
+    ManticoreError.__name__,
+]
diff --git a/manticore/core/manticore.py b/manticore/core/manticore.py
@@ -1,3 +1,4 @@
+import os
 import itertools
 import logging
 import sys
@@ -177,6 +178,19 @@ def newFunction(self, *args, **kw):
 
         return newFunction
 
+    def only_from_main_script(func: Callable) -> Callable:  # type: ignore
+        """Allows the decorated method to run only from the main manticore script
+        """
+
+        @functools.wraps(func)
+        def newFunction(self, *args, **kw):
+            if not self.is_main() or self.is_running():
+                logger.error("Calling from worker or forked process not allowed")
+                raise ManticoreError(f"{func.__name__} only allowed from main")
+            return func(self, *args, **kw)
+
+        return newFunction
+
     _published_events = {
         "run",
         "start_worker",
@@ -304,10 +318,11 @@ def __init__(self, initial_state, workspace_url=None, outputspace_url=None, **kw
         """
         super().__init__()
         random.seed(consts.seed)
-        {consts.mprocessing.single: self._manticore_single,
-         consts.mprocessing.threading: self._manticore_threading,
-         consts.mprocessing.multiprocessing: self._manticore_multiprocessing
-         }[consts.mprocessing]()
+        {
+            consts.mprocessing.single: self._manticore_single,
+            consts.mprocessing.threading: self._manticore_threading,
+            consts.mprocessing.multiprocessing: self._manticore_multiprocessing,
+        }[consts.mprocessing]()
 
         if any(
             not hasattr(self, x)
@@ -338,6 +353,8 @@ def __init__(self, initial_state, workspace_url=None, outputspace_url=None, **kw
                 raise TypeError(f"Invalid workspace type: {type(workspace_url).__name__}")
         self._workspace = Workspace(workspace_url)
         # reuse the same workspace if not specified
+        if outputspace_url is None:
+            outputspace_url = workspace_url
         if outputspace_url is None:
             outputspace_url = f"fs:{self._workspace.uri}"
         self._output = ManticoreOutput(outputspace_url)
@@ -356,7 +373,60 @@ def __init__(self, initial_state, workspace_url=None, outputspace_url=None, **kw
 
         # Workers will use manticore __dict__ So lets spawn them last
         self._workers = [self._worker_type(id=i, manticore=self) for i in range(consts.procs)]
-        self._is_main = True
+        self._snapshot = None
+        self._main_id = os.getpid(), threading.current_thread().ident
+
+    def is_main(self):
+        """ True if called from the main process/script
+        Note: in "single" mode this is _most likely_ True """
+        return self._main_id == (os.getpid(), threading.current_thread().ident)
+
+    @sync
+    @only_from_main_script
+    def take_snapshot(self):
+        """ Copy/Duplicate/backup all ready states and save it in a snapshot.
+        If there is a snapshot already saved it will be overrwritten
+        """
+        if self._snapshot is not None:
+            logger.info("Overwriting a snapshot of the ready states")
+        snapshot = []
+        for state_id in self._ready_states:
+            state = self._load(state_id)
+            # Re-save the state in case the user changed its data
+            snapshot.append(self._save(state))
+        self._snapshot = snapshot
+
+    @sync
+    @only_from_main_script
+    def goto_snapshot(self):
+        """ REMOVE current ready states and replace them with the saved states
+        in a snapshot """
+        if not self._snapshot:
+            raise ManticoreError("No snapshot to go to")
+        for state_id in tuple(self._ready_states):
+            self._ready_states.remove(state_id)
+        for state_id in self._snapshot:
+            self._ready_states.append(state_id)
+        self._snapshot = None
+
+    @sync
+    @only_from_main_script
+    def clear_snapshot(self):
+        """ Remove any saved states """
+        if self._snapshot:
+            for state_id in self._snapshot:
+                self._remove(state_id)
+        self._snapshot = None
+
+    @sync
+    @at_not_running
+    def clear_terminated_states(self):
+        """ Simply remove all states from terminated list """
+        terminated_states_ids = tuple(self._terminated_states)
+        for state_id in terminated_states_ids:
+            self._terminated_states.remove(state_id)
+            self._remove(state_id)
+        assert self.count_terminated_states() == 0
 
     def __str__(self):
         return f"<{str(type(self))[8:-2]}| Alive States: {self.count_ready_states()}; Running States: {self.count_busy_states()} Terminated States: {self.count_terminated_states()} Killed States: {self.count_killed_states()} Started: {self._running.value} Killed: {self._killed.value}>"
@@ -865,7 +935,6 @@ def context(self):
         return self._shared_context
 
     @contextmanager
-    @sync
     def locked_context(self, key=None, value_type=list):
         """
         A context manager that provides safe parallel access to the global
@@ -895,20 +964,20 @@ def locked_context(self, key=None, value_type=list):
         :param value_type: type of value associated with key
         :type value_type: list or dict or set
         """
-
-        if key is None:
-            # If no key is provided we yield the raw shared context under a lock
-            yield self._shared_context
-        else:
-            # if a key is provided we yield the specific value or a fresh one
-            if value_type not in (list, dict):
-                raise TypeError("Type must be list or dict")
-            if hasattr(self, "_context_value_types"):
-                value_type = self._context_value_types[value_type]
-            context = self._shared_context
-            if key not in context:
-                context[key] = value_type()
-            yield context[key]
+        with self._lock:
+            if key is None:
+                # If no key is provided we yield the raw shared context under a lock
+                yield self._shared_context
+            else:
+                # if a key is provided we yield the specific value or a fresh one
+                if value_type not in (list, dict):
+                    raise TypeError("Type must be list or dict")
+                if hasattr(self, "_context_value_types"):
+                    value_type = self._context_value_types[value_type]
+                context = self._shared_context
+                if key not in context:
+                    context[key] = value_type()
+                yield context[key]
 
     ############################################################################
     # Public API

diff --git a/manticore/core/plugin.py b/manticore/core/plugin.py
@@ -10,20 +10,34 @@
 logger = logging.getLogger(__name__)
 
 
-class Plugin:
+class DecorateAllMeta(type):
+    @staticmethod
+    def _if_enabled(f):
+        """ decorator used to guard callbacks """
+
+        @wraps(f)
+        def g(self, *args, **kwargs):
+            if self.is_enabled():
+                return f(self, *args, **kwargs)
+
+        return g
+
+    def __new__(cls, name, bases, local):
+        for attr in local:
+            value = local[attr]
+            if attr.endswith("_callback") and callable(value):
+                local[attr] = cls._if_enabled(value)
+        return type.__new__(cls, name, bases, local)
+
+
+class Plugin(metaclass=DecorateAllMeta):
+    __slots__ = ("manticore", "_enabled_key", "_plugin_context_name")
 
     def __init__(self):
         self.manticore = None
-        self._enabled_key = f"{str(type(self))}_enabled_{hash(self)}"
-        self._plugin_context_name = f"{str(type(self))}_context_{hash(self)}"
-        self.__decorate_callbacks()
-
-    def __decorate_callbacks(self):
-        for attr in self.__dict__:
-            if attr.endswith('_callback'):
-                method = getattr(self, attr)
-                if callable(method):
-                    setattr(self, attr, self._if_enabled(method))
+        classname = str(type(self)).split("'")[1]
+        self._enabled_key = f"{classname}_enabled_{hex(hash(self))}"
+        self._plugin_context_name = f"{classname}_context_{hex(hash(self))}"
 
     def enable(self):
         """ Enable all callbacks """
@@ -40,15 +54,6 @@ def is_enabled(self):
         with self.manticore.locked_context() as context:
             return context.get(self._enabled_key, True)
 
-    @staticmethod
-    def _if_enabled(f):
-        """ decorator used to guard callbacks """
-        @wraps(f)
-        def g(self, *args, **kwargs):
-            if self.is_enabled():
-                return f(self, *args, **kwargs)
-        return g
-
     @property
     def name(self):
         return str(self.__class__)
@@ -148,20 +153,14 @@ def will_read_memory_callback(self, state, where, size):
         if self.current_pc == where:
             return
 
-        # print(f'will_read_memory {where:x} {size!r}, current_pc {self.current_pc:x}')
-
     def did_read_memory_callback(self, state, where, value, size):
         if self.current_pc == where:
             return
 
-        # print(f'did_read_memory {where:x} {value!r} {size!r}, current_pc {self.current_pc:x}')
-
     def will_write_memory_callback(self, state, where, value, size):
         if self.current_pc == where:
             return
 
-        # print(f'will_write_memory {where:x} {value!r} {size!r}, current_pc {self.current_pc:x}')
-
     def did_write_memory_callback(self, state, where, value, size):
         if self.current_pc == where:
             raise Exception

diff --git a/manticore/core/smtlib/constraints.py b/manticore/core/smtlib/constraints.py
@@ -24,7 +24,9 @@
 
 consts = config.get_group("smt")
 consts.add(
-    "related_constraints", default=False, description="Try slicing the current path constraint to contain only related items"
+    "related_constraints",
+    default=False,
+    description="Try slicing the current path constraint to contain only related items",
 )
 
 
@@ -146,7 +148,7 @@ def __get_related(self, related_to=None):
                             break
 
                     variables = get_variables(constraint)
-                    if related_variables & variables:
+                    if related_variables & variables or not (variables):
                         remaining_constraints.remove(constraint)
                         related_constraints.add(constraint)
                         related_variables |= variables