Merge remote-tracking branch 'origin/master' into dev-detect-transact…

…ion-reordering

.github/workflows/ci.yml

@@ -34,7 +34,7 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        type: ["ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "wasm", "wasm_sym", "other"]
+        type: ["ethereum_truffle", "ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "wasm", "wasm_sym", "other"]
     steps:
     - uses: actions/checkout@v1
     - name: Set up Python 3.6
@@ -157,25 +157,23 @@ jobs:
             mkdir truffle_tests
             cd truffle_tests
             truffle unbox metacoin
-            manticore . --exclude-all --contract MetaCoin --workspace output
-            ### The original comment says we should get 41 states, but after implementing the shift
-            ### insructions, we get 31. Was the original comment a typo?
-
-            # The correct answer should be 41
-            # but Manticore fails to explore the paths due to the lack of the 0x1f opcode support
-            # see https://github.com/trailofbits/manticore/issues/1166
-            # if [ "$(ls output/*tx -l | wc -l)" != "41" ]; then
+            coverage run -m manticore . --exclude-all --contract MetaCoin --workspace output
+            # 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"
                 return 1
             fi
             echo "Truffle test succeded"
+            coverage xml
             cd ..
+            cp truffle_tests/coverage.xml .
             return 0
         }
 
         run_tests_from_dir() {
             DIR=$1
+            echo "Running only the tests from 'tests/$DIR' directory"
             pytest --durations=100 --cov=manticore -n auto "tests/$DIR"
             coverage xml
         }
@@ -203,30 +201,24 @@ jobs:
         case $TEST_TYPE in
             ethereum_vm)
                 make_vmtests
-                echo "Running only the tests from 'tests/$TEST_TYPE' directory"
                 run_tests_from_dir $TEST_TYPE
-                RV=$?
-
+                ;;
+            ethereum_truffle)
                 echo "Running truffle test"
                 install_truffle
                 run_truffle_tests
-                RV=$(($RV + $?))
                 ;;
             wasm)
                 make_wasm_tests
-                echo "Running only the tests from 'tests/$TEST_TYPE' directory"
                 run_tests_from_dir $TEST_TYPE
-                RV=$?
                 ;;
             wasm_sym)
-                make_wasm_sym_tests ;&
+                make_wasm_sym_tests ;&  # Fallthrough
             native)                 ;&  # Fallthrough
             ethereum)               ;&  # Fallthrough
             ethereum_bench)         ;&  # Fallthrough
             other)
-                echo "Running only the tests from 'tests/$TEST_TYPE' directory"
                 run_tests_from_dir $TEST_TYPE
-                RV=$?
                 ;;
             examples)
                 run_examples

codecov.yml

@@ -2,7 +2,7 @@ comment: false
 
 codecov:
   notify:
-    # We have 8 test steps that produce coverage data.
+    # We have 9 test steps that produce coverage data.
     # If we add or remove any, we need to change this number.
-    after_n_builds: 8
+    after_n_builds: 9
     wait_for_ci: yes

docs/index.rst

@@ -17,6 +17,7 @@ Manticore is a symbolic execution tool for analysis of binaries and smart contra
    wasm
    plugins
    gotchas
+   utilities
 
 
 Indices and tables

docs/utilities.rst

@@ -0,0 +1,7 @@
+Utilities
+---------
+
+Logging
+^^^^^^^
+
+.. autofunction:: manticore.utils.log.set_verbosity

manticore/core/manticore.py

@@ -243,9 +243,9 @@ def __init__(self, initial_state, workspace_url=None, outputspace_url=None, **kw
         *State list: KILLED*
 
         KILLED contains all the READY and BUSY states found at a cancel event.
-        Manticore supports interactive analysis and has a prominetnt event system
-        A useror ui can stop or cancel the exploration at any time. The unfinnished
-        states cought at this situation are simply moved to its own list for
+        Manticore supports interactive analysis and has a prominent event system.
+        A user can stop or cancel the exploration at any time. The unfinished
+        states caught in this situation are simply moved to their own list for
         further user action. This is a final list.
 
 
@@ -395,7 +395,7 @@ def setstate(x, y):
     @staticmethod
     @deprecated("Use utils.log.set_verbosity instead.")
     def verbosity(level):
-        """ Sets global vervosity level.
+        """ Sets global verbosity level.
             This will activate different logging profiles globally depending
             on the provided numeric value
         """

manticore/core/smtlib/solver.py

@@ -164,6 +164,11 @@ def __init__(self):
             "(set-logic QF_AUFBV)",
             # The declarations and definitions will be scoped
             "(set-option :global-decls false)",
+            # sam.moelius: Option "tactic.solve_eqs.context_solve" was turned on by this commit in z3:
+            #   https://github.com/Z3Prover/z3/commit/3e53b6f2dbbd09380cd11706cabbc7e14b0cc6a2
+            # Turning it off greatly improves Manticore's performance on test_integer_overflow_storageinvariant
+            # in test_consensys_benchmark.py.
+            "(set-option :tactic.solve_eqs.context_solve false)",
         ]
 
         self._get_value_fmt = (RE_GET_EXPR_VALUE_FMT, 16)

manticore/core/worker.py

@@ -132,7 +132,7 @@ def run(self, *args):
                         assert current_state is None
                     # Handling Forking and terminating exceptions
                     except Concretize as exc:
-                        logger.info("[%r] Debug %r", self.id, exc)
+                        logger.info("[%r] Performing %r", self.id, exc.message)
                         # The fork() method can decides which state to keep
                         # exploring. For example when the fork results in a
                         # single state it is better to just keep going.

manticore/ethereum/manticore.py

@@ -592,14 +592,18 @@ def solidity_create_contract(
                                 f"Can't create solidity contract with balance ({balance}) "
                                 f"different than 0 because the contract's constructor is not payable."
                             )
-                    if not Z3Solver.instance().can_be_true(
-                        self.constraints,
-                        Operators.UGE(self.world.get_balance(owner.address), balance),
-                    ):
-                        raise EthereumError(
-                            f"Can't create solidity contract with balance ({balance}) "
-                            f"because the owner account ({owner}) has insufficient balance."
-                        )
+
+                    for state in self.ready_states:
+                        world = state.platform
+
+                        if not Z3Solver.instance().can_be_true(
+                            self.constraints,
+                            Operators.UGE(world.get_balance(owner.address), balance),
+                        ):
+                            raise EthereumError(
+                                f"Can't create solidity contract with balance ({balance}) "
+                                f"because the owner account ({owner}) has insufficient balance."
+                            )
 
                     contract_account = self.create_contract(
                         owner=owner,

manticore/utils/log.py

@@ -149,6 +149,7 @@ def match(name: str, pattern: str):
 
 
 def set_verbosity(setting: int) -> None:
+    """Set the global verbosity (0-5)."""
     global manticore_verbosity
     manticore_verbosity = min(max(setting, 0), len(get_levels()) - 1)
     for logger_name in all_loggers: