Manticore verifier (#1717)

* Add ONE failing test

* Fix test

* Try fix get-related

* Snapshots

* CC

* Allow snapshooting just from main()

* A test

* Test and fix is_main

* CC

* review

* ismain vs is_running

* is main to is main script

* Remove unused member variable

* initial import manticore verifier

* Fix verifier installation

* clear ready states

* CC and smoke test

* CC

* Increase cov

* Move regression to other

* blkn

* blkn

* Move get related

* CC

* fix concolic

* lint

* DivByZero default to zero

* blkn

* Update manticore/core/smtlib/solver.py

Co-authored-by: Eric Kilmer <[email protected]>

* Update manticore/core/smtlib/constraints.py

Co-authored-by: Eric Kilmer <[email protected]>

* Update manticore/core/smtlib/constraints.py

Co-authored-by: Eric Kilmer <[email protected]>

* remove odd string

* lint

* mypy lint

* Update manticore/core/smtlib/visitors.py

Co-authored-by: Eric Kilmer <[email protected]>

* lint

* Add Docs

* blkn

* blkn

* Replace modulo with masks

* Blacken

* blkn

* fix mypy

* fix mypy

* Add tests for signed LT behavior

* New test

* Fix constant folding

* lint

* blkn

* lint

* Fixes...

* lint

* Unittesting power

* Permisive read_buffer

* Fix optimize

* Preserve precision in constant folding

* Strip left-in print debugging

* blkn

* remove wasm_sym temporarily

* Better simplification for constants

* Add json

* blkn

* Better commmandline args

* blkn

* fix wasm

* Fix

* better commanlining

* REmove get_related from the default path and fix arm test

* blkn

* fix related to tests

* blkn

* Fix bug in test and disable debug messages in Solver

* smtlib config to disable multiple check-sat in newer z3

* Disable log test and fix merging poc vs variable migration

* blkn

* Avoid exception in some callbacks

* can_rais at did_will

* yikes!

* blkn

* Yices found one more states in truffle

* Add a config constant to ignore symbolic balances

* Add a config constant to ignore symbolic balances 2

* Relax truffle state count

* Relax truffle state count 2

* Change cli name and test

* Clear redy states in verifier workspace

* Clear ready states in verifier workspace

* Relative ws path on verifier output. Clean CREATE testcase example

* Blkn

* Improve coverage and funcid solving

* lint

* Better testcase generation at verifier

* Better testcase generation at verifier and typos

* Better output and default re

* Test must revert

* Better output and default re

* move generate_testcase_ex to private method

Co-authored-by: Eric Kilmer <[email protected]>
Co-authored-by: Eric Hennenfent <[email protected]>

Author: 3 people

manticore/__main__.py

@@ -212,9 +212,7 @@ def positive(value):
     )
 
     eth_flags.add_argument(
-        "--limit-loops",
-        action="store_true",
-        help="Avoid exploring constant functions for human transactions",
+        "--limit-loops", action="store_true", help="Limit loops depth",
     )
 
     eth_flags.add_argument(

manticore/core/manticore.py

@@ -23,7 +23,7 @@
 from ..utils.helpers import PickleSerializer
 from ..utils.log import set_verbosity
 from ..utils.nointerrupt import WithKeyboardInterruptAs
-from .workspace import Workspace
+from .workspace import Workspace, Testcase
 from .worker import WorkerSingle, WorkerThread, WorkerProcess
 
 from multiprocessing.managers import SyncManager
@@ -403,8 +403,7 @@ def goto_snapshot(self):
         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)
+        self.clear_ready_states()
         for state_id in self._snapshot:
             self._ready_states.append(state_id)
         self._snapshot = None
@@ -421,13 +420,23 @@ def clear_snapshot(self):
     @sync
     @at_not_running
     def clear_terminated_states(self):
-        """ Simply remove all states from terminated list """
+        """ Remove all states from the 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
 
+    @sync
+    @at_not_running
+    def clear_ready_states(self):
+        """ Remove all states from the ready list """
+        ready_states_ids = tuple(self._ready_states)
+        for state_id in ready_states_ids:
+            self._ready_states.remove(state_id)
+            self._remove(state_id)
+        assert self.count_ready_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}>"
 
@@ -833,7 +842,7 @@ def count_terminated_states(self):
         """ Terminated states count """
         return len(self._terminated_states)
 
-    def generate_testcase(self, state, message: str = "test", name: str = "test"):
+    def generate_testcase(self, state, message: str = "test", name: str = "test") -> Testcase:
         if message == "test" and hasattr(state, "_terminated_by") and state._terminated_by:
             message = str(state._terminated_by)
         testcase = self._output.testcase(prefix=name)

manticore/core/smtlib/solver.py

@@ -593,7 +593,7 @@ def get_value(self, constraints: ConstraintSet, *expressions):
         """
         values = []
         start = time.time()
-        with constraints as temp_cs:
+        with constraints.related_to(*expressions) as temp_cs:
             for expression in expressions:
                 if not issymbolic(expression):
                     values.append(expression)

manticore/core/workspace.py

@@ -44,7 +44,7 @@ def __exit__(self, *excinfo):
 consts.add("dir", default=".", description="Location of where to create workspace directories")
 
 
-class WorkspaceTestcase:
+class Testcase:
     """
     A `WorkspaceTestCase` represents a test case input generated by Manticore.
     """
@@ -519,8 +519,8 @@ def __init__(self, desc=None):
         self._descriptor = desc
         self._store = Store.fromdescriptor(desc)
 
-    def testcase(self, prefix: str = "test") -> WorkspaceTestcase:
-        return WorkspaceTestcase(self, prefix)
+    def testcase(self, prefix: str = "test") -> Testcase:
+        return Testcase(self, prefix)
 
     @property
     def store(self):
@@ -587,7 +587,7 @@ def _named_stream(self, name, binary=False, lock=False):
             yield s
 
     # Remove/move ...
-    def save_testcase(self, state: StateBase, testcase: WorkspaceTestcase, message: str = ""):
+    def save_testcase(self, state: StateBase, testcase: Testcase, message: str = ""):
         """
         Save the environment from `state` to storage. Return a state id
         describing it, which should be an int or a string.

manticore/ethereum/manticore.py

@@ -13,7 +13,8 @@
 
 from crytic_compile import CryticCompile, InvalidCompilation, is_supported
 
-from ..core.manticore import ManticoreBase
+from ..core.manticore import ManticoreBase, Testcase, ManticoreError
+
 from ..core.smtlib import (
     ConstraintSet,
     Array,
@@ -1536,10 +1537,6 @@ def current_location(self, state):
 
     def generate_testcase(self, state, message="", only_if=None, name="user"):
         """
-        Generate a testcase to the workspace for the given program state. The details of what
-        a testcase is depends on the type of Platform the state is, but involves serializing the state,
-        and generating an input (concretizing symbolic variables) to trigger this state.
-
         The only_if parameter should be a symbolic expression. If this argument is provided, and the expression
         *can be true* in this state, a testcase is generated such that the expression will be true in the state.
         If it *is impossible* for the expression to be true in the state, a testcase is not generated.
@@ -1552,29 +1549,38 @@ def generate_testcase(self, state, message="", only_if=None, name="user"):
 
             m.generate_testcase(state, 'balance CAN be 0', only_if=balance == 0)
             # testcase generated with an input that will violate invariant (make balance == 0)
+        """
+        try:
+            with state as temp_state:
+                if only_if is not None:
+                    temp_state.constrain(only_if)
+                return self._generate_testcase_ex(temp_state, message, name=name)
+        except ManticoreError:
+            return None
+
+    def _generate_testcase_ex(self, state, message="", name="user"):
+        """
+        Generate a testcase in the outputspace for the given program state.
+        An exception is raised if the state is unsound or unfeasible
+
+        On return you get a Testcase containing all the informations about the state.
+        A Testcase is a collection of files living at the OutputSpace.
+        Registered plugins and other parts of Manticore add files to the Testcase.
+        User can add more streams to is like this:
+
+        testcase = m.generate_testcase_ex(state)
+        with testcase.open_stream("txt") as descf:
+            descf.write("This testcase is interesting!")
 
         :param manticore.core.state.State state:
         :param str message: longer description of the testcase condition
-        :param manticore.core.smtlib.Bool only_if: only if this expr can be true, generate testcase. if is None, generate testcase unconditionally.
-        :param str name: short string used as the prefix for the workspace key (e.g. filename prefix for testcase files)
-        :return: If a testcase was generated
+        :param str name: short string used as the prefix for the outputspace key (e.g. filename prefix for testcase files)
+        :return: a Testcase
         :rtype: bool
         """
-        """
-        Create a serialized description of a given state.
-        :param state: The state to generate information about
-        :param message: Accompanying message
-        """
+        # Refuse to generate a testcase from an unsound state
         if not self.fix_unsound_symbolication(state):
-            return False
-
-        if only_if is not None:
-            with state as temp_state:
-                temp_state.constrain(only_if)
-                if temp_state.is_feasible():
-                    return self.generate_testcase(temp_state, message, only_if=None, name=name)
-                else:
-                    return False
+            raise ManticoreError("Trying to generate a testcase out of an unsound state path")
 
         blockchain = state.platform
 
@@ -1584,8 +1590,6 @@ def generate_testcase(self, state, message="", only_if=None, name="user"):
         testcase = super().generate_testcase(
             state, message + f"({len(blockchain.human_transactions)} txs)", name=name
         )
-        # TODO(mark): Refactor ManticoreOutput to let the platform be more in control
-        #  so this function can be fully ported to EVMWorld.generate_workspace_files.
 
         local_findings = set()
         for detector in self.detectors.values():
@@ -1865,8 +1869,8 @@ def ready_sound_states(self):
         This tries to solve any symbolic imprecision added by unsound_symbolication
         and then iterates over the resultant set.
 
-        This is the recommended to iterate over resultant steas after an exploration
-        that included unsound symbolication
+        This is the recommended way to iterate over the resultant states after
+        an exploration that included unsound symbolication
 
         """
         self.fix_unsound_all()