Replace Quick mode with Thorough mode (#2457)

* Replace Quick mode with Thorough mode

Replaces the `quick_mode` flag with `thorough_mode` and inverts the logic. Closes #2424.

* Run truffle tests in thorough mode

* Use thorough mode for failing test

manticore/__main__.py

@@ -227,10 +227,10 @@ def positive(value):
     )
 
     eth_flags.add_argument(
-        "--quick-mode",
+        "--thorough-mode",
         action="store_true",
-        help="Configure Manticore for quick exploration. Disable gas, generate testcase only for alive states, "
-        "do not explore constant functions. Disable all detectors.",
+        help="Configure Manticore for more exhaustive exploration. Evaluate gas, generate testcases for dead states, "
+        "explore constant functions, and run a small suite of detectors.",
     )
 
     config_flags = parser.add_argument_group("Constants")

manticore/ethereum/cli.py

@@ -89,7 +89,7 @@ def choose_detectors(args):
 def ethereum_main(args, logger):
     m = ManticoreEVM(workspace_url=args.workspace)
 
-    if args.quick_mode:
+    if not args.thorough_mode:
         args.avoid_constant = True
         args.exclude_all = True
         args.only_alive_testcases = True

manticore/ethereum/verifier.py

@@ -398,10 +398,10 @@ def main():
     eth_flags = parser.add_argument_group("Ethereum flags")
 
     eth_flags.add_argument(
-        "--quick-mode",
+        "--thorough-mode",
         action="store_true",
-        help="Configure Manticore for quick exploration. Disable gas, generate testcase only for alive states, "
-        "do not explore constant functions. Disable all detectors.",
+        help="Configure Manticore for more exhaustive exploration. Evaluate gas, generate testcases for dead states, "
+        "explore constant functions, and run a small suite of detectors.",
     )
     eth_flags.add_argument(
         "--contract_name", type=str, help="The target contract name defined in the source code"

scripts/run_tests.sh

@@ -103,7 +103,7 @@ run_truffle_tests(){
     mkdir truffle_tests
     cd truffle_tests
     truffle unbox metacoin
-    coverage run -m manticore . --contract MetaCoin --workspace output --exclude-all --evm.oog ignore --evm.txfail optimistic
+    coverage run -m manticore . --contract MetaCoin --workspace output --exclude-all --thorough-mode --evm.oog ignore --evm.txfail optimistic
     # Truffle smoke test. We test if manticore is able to generate states
     # from a truffle project.
     count=$(find output/ -name '*tx' -type f | wc -l)

tests/ethereum/test_regressions.py

@@ -235,7 +235,9 @@ def test_regressions_imports(self):
 
     def test_1102(self):
         with tempfile.TemporaryDirectory() as workspace:
-            self._simple_cli_run("1102.sol", workspace=workspace, testcases=True)
+            self._simple_cli_run(
+                "1102.sol", workspace=workspace, testcases=True, args=["--thorough-mode"]
+            )
 
             with open(os.path.join(workspace, "global.findings")) as gf:
                 global_findings = gf.read().splitlines()