Merge branch 'master' into chess

* master:
  Fix the generation of EVM tests (#2426)
  Disabled EVM events in testcases by default (#2417)
  added proper timeouts for cvc4 and boolector (#2418)

manticore/core/smtlib/solver.py

@@ -736,14 +736,14 @@ def __init__(self):
 class CVC4Solver(SMTLIBSolver):
     def __init__(self):
         init = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"]
-        command = f"{consts.cvc4_bin} --lang=smt2 --incremental"
+        command = f"{consts.cvc4_bin} --tlimit={consts.timeout * 1000} --lang=smt2 --incremental"
         super().__init__(command=command, init=init)
 
 
 class BoolectorSolver(SMTLIBSolver):
     def __init__(self):
         init = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"]
-        command = f"{consts.boolector_bin} -i"
+        command = f"{consts.boolector_bin} --time={consts.timeout} -i"
         super().__init__(command=command, init=init)
 
 

manticore/ethereum/manticore.py

@@ -52,6 +52,11 @@
     60 * 60,
     "Default timeout for matching sha3 for unsound states (see unsound symbolication).",
 )
+consts.add(
+    "events",
+    False,
+    "Show EVM events in the testcases.",
+)
 
 
 def flagged(flag):
@@ -1666,27 +1671,28 @@ def _generate_testcase_ex(self, state, message="", name="user"):
                 json.dump(txlist, txjson)
 
         # logs
-        with testcase.open_stream("logs") as logs_summary:
-            is_something_symbolic = False
-            for log_item in blockchain.logs:
-                is_log_symbolic = issymbolic(log_item.memlog)
-                is_something_symbolic = is_log_symbolic or is_something_symbolic
-                solved_memlog = state.solve_one(log_item.memlog)
-
-                logs_summary.write("Address: %x\n" % log_item.address)
-                logs_summary.write(
-                    "Memlog: %s (%s) %s\n"
-                    % (
-                        binascii.hexlify(solved_memlog).decode(),
-                        printable_bytes(solved_memlog),
-                        flagged(is_log_symbolic),
-                    )
-                )
-                logs_summary.write("Topics:\n")
-                for i, topic in enumerate(log_item.topics):
+        if consts.events:
+            with testcase.open_stream("logs") as logs_summary:
+                is_something_symbolic = False
+                for log_item in blockchain.logs:
+                    is_log_symbolic = issymbolic(log_item.memlog)
+                    is_something_symbolic = is_log_symbolic or is_something_symbolic
+                    solved_memlog = state.solve_one(log_item.memlog)
+
+                    logs_summary.write("Address: %x\n" % log_item.address)
                     logs_summary.write(
-                        "\t%d) %x %s" % (i, state.solve_one(topic), flagged(issymbolic(topic)))
+                        "Memlog: %s (%s) %s\n"
+                        % (
+                            binascii.hexlify(solved_memlog).decode(),
+                            printable_bytes(solved_memlog),
+                            flagged(is_log_symbolic),
+                        )
                     )
+                    logs_summary.write("Topics:\n")
+                    for i, topic in enumerate(log_item.topics):
+                        logs_summary.write(
+                            "\t%d) %x %s" % (i, state.solve_one(topic), flagged(issymbolic(topic)))
+                        )
 
         with testcase.open_stream("constraints") as smt_summary:
             smt_summary.write(str(state.constraints))

scripts/run_tests.sh

@@ -56,7 +56,8 @@ make_vmtests(){
     if  [ ! -f ethereum_vm/.done ]; then
         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
+        # March 27, 2021. Newer commits move files around
+        rm -Rf vmtests; git clone https://github.com/ethereum/tests vmtests ; cd vmtests ; git checkout ff68495eb56c382b2ddcea4020259e106353b874 ; cd ..
         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

tests/ethereum/test_general.py

@@ -752,6 +752,8 @@ def test_gen_testcase_only_if(self):
             }
         }
         """
+        consts = config.get_group("evm")
+        consts.events = True
         user_account = self.mevm.create_account(balance=10 ** 10)
         contract_account = self.mevm.solidity_create_contract(source_code, owner=user_account)
         input_sym = self.mevm.make_symbolic_value()