Merge branch 'master' into native-arb-cf-redirect-detector

* master:
  Restore old init hook behavior (#1447)
  Fix invalid pip argument (#1445)
  Blacken Manticore (#1438)
  Relegate coverage file to plugin (#1442)
  x86: movhps support (#1444)
  Delete statically generated tests (#1443)
  Hardcode expected matching concrete registers (#1437)
  Symbolic tests rf otf (#1441)
  Unicorn dependency update (#1440)
  aarch64: do not use the 'procs' argument (#1439)
  Symbolic tests rf (#1431)

Author: ekilmer

.codeclimate.yml

@@ -48,6 +48,10 @@ plugins:
         enabled: false
       E701:
         enabled: false
+      E203:
+        enabled: false
+      W503:
+        enabled: false
   sonar-python:
     enabled: false
     config:

.travis.yml

@@ -7,18 +7,20 @@ python:
   - 3.6.6
 
 stages:
+  - format
   - prepare
   - test
   - submit
 
 env:
   global:
     - CC_TEST_REPORTER_ID=db72f1ed59628c16eb0c00cbcd629c4c71f68aa1892ef42d18c7c2b8326f460a
-    - JOB_COUNT=3 # Three jobs generate test coverage: ethereum, native, and other
+    - JOB_COUNT=4 # Four jobs generate test coverage: ethereum, ethereum_vm, native, and other
     - PYTHONWARNINGS="default::ResourceWarning" # Enable ResourceWarnings
   matrix:
     - TEST_TYPE=examples
     - TEST_TYPE=ethereum
+    - TEST_TYPE=ethereum_vm
     - TEST_TYPE=native
     - TEST_TYPE=other
 
@@ -35,6 +37,10 @@ cache:
 
 jobs:
   include:
+    - stage: format
+      env: TEST_TYPE=format
+      script:
+        - git diff --name-only $TRAVIS_COMMIT_RANGE | python3 scripts/pyfile_exists.py | xargs black -t py36 -l 100 --check
     - stage: prepare
       env: TEST_TYPE=env
       script:
@@ -52,7 +58,7 @@ install:
   - scripts/travis_install.sh $TEST_TYPE
 
 script:
-  - scripts/travis_test.sh $TEST_TYPE
+  - travis_wait 60 scripts/travis_test.sh $TEST_TYPE
 
 after_success:
   - ./cc-test-reporter format-coverage -t coverage.py -o "coverage/codeclimate.$TEST_TYPE.json"

CONTRIBUTING.md

@@ -30,6 +30,10 @@ more documentation, look [here](https://guides.github.com/activities/forking/).
 
 Some pull request guidelines:
 
+- We use the [`black`](https://black.readthedocs.io/en/stable/index.html) auto-formatter
+  to enforce style conventions in Manticore. To ensure your code is properly 
+  formatted, run `black -t py36 -l 100 .` in the manticore directory before
+  committing.
 - Minimize irrelevant changes (formatting, whitespace, etc) to code that would
   otherwise not be touched by this patch. Save formatting or style corrections
   for a separate pull request that does not make any semantic changes.

docs/conf.py

@@ -46,17 +46,17 @@
 
 # General information about the project.
 project = "Manticore"
-copyright = "2017, Trail of Bits"
+copyright = "2019, Trail of Bits"
 author = "Trail of Bits"
 
 # The version info for the project you're documenting, acts as replacement for
 # |version| and |release|, also used in various other places throughout the
 # built documents.
 #
 # The short X.Y version.
-version = "0.1.0"
+version = "0.2.5"
 # The full version, including alpha/beta/rc tags.
-release = "0.1.0"
+release = "0.2.5"
 
 # The language for content autogenerated by Sphinx. Refer to documentation
 # for a list of supported languages.

examples/script/aarch64/basic.py

@@ -22,9 +22,8 @@
 
 
 @m.init
-def init(m, ready_states):
-    for state in ready_states:
-        state.platform.input.write(state.symbolicate_buffer(STDIN, label="STDIN"))
+def init(state):
+    state.platform.input.write(state.symbolicate_buffer(STDIN, label="STDIN"))
 
 
 # Hook the 'if' case.

examples/script/aarch64/hello42.py

@@ -49,6 +49,6 @@ def execute_instruction(self, insn, msg):
         lambda self, state, last_pc, pc, insn: execute_instruction(self, insn, "done"),
     )
 
-    m.run(procs=1)
+    m.run()
 
     print(f"Executed {m.context['count']} instructions")

manticore/__main__.py

@@ -57,7 +57,7 @@ def positive(value):
     )
     parser.add_argument("--context", type=str, default=None, help=argparse.SUPPRESS)
     parser.add_argument(
-        "--coverage", type=str, default=None, help="Where to write the coverage data"
+        "--coverage", type=str, default="visited.txt", help="Where to write the coverage data"
     )
     parser.add_argument("--names", type=str, default=None, help=argparse.SUPPRESS)
     parser.add_argument(
@@ -105,36 +105,6 @@ def positive(value):
         help="Manticore config file (.yml) to use. (default config file pattern is: ./[.]m[anti]core.yml)",
     )
 
-    detectors = parser.add_argument_group("Detectors")
-
-    detectors.add_argument(
-        "--list-ethereum-detectors",
-        help="List available ethereum detectors",
-        action=ListEthereumDetectors,
-        nargs=0,
-        default=False,
-    )
-
-    detectors.add_argument(
-        "--list-native-detectors",
-        help="List available native detectors",
-        action=ListNativeDetectors,
-        nargs=0,
-        default=False,
-    )
-
-    detectors.add_argument(
-        "--exclude",
-        help="Comma-separated list of detectors that should be excluded",
-        action="store",
-        dest="detectors_to_exclude",
-        default="",
-    )
-
-    detectors.add_argument(
-        "--exclude-all", help="Excludes all detectors", action="store_true", default=False
-    )
-
     bin_flags = parser.add_argument_group("Binary flags")
     bin_flags.add_argument("--entrysymbol", type=str, default=None, help="Symbol as entry point")
     bin_flags.add_argument("--assertions", type=str, default=None, help=argparse.SUPPRESS)
@@ -201,6 +171,28 @@ def positive(value):
         "--contract", type=str, help="Contract name to analyze in case of multiple contracts"
     )
 
+    eth_detectors = parser.add_argument_group("Ethereum detectors")
+
+    eth_detectors.add_argument(
+        "--list-detectors",
+        help="List available detectors",
+        action=ListEthereumDetectors,
+        nargs=0,
+        default=False,
+    )
+
+    eth_detectors.add_argument(
+        "--exclude",
+        help="Comma-separated list of detectors that should be excluded",
+        action="store",
+        dest="detectors_to_exclude",
+        default="",
+    )
+
+    eth_detectors.add_argument(
+        "--exclude-all", help="Excludes all detectors", action="store_true", default=False
+    )
+
     eth_flags.add_argument(
         "--avoid-constant",
         action="store_true",
@@ -246,13 +238,5 @@ def __call__(self, parser, *args, **kwargs):
         parser.exit()
 
 
-class ListNativeDetectors(argparse.Action):
-    def __call__(self, parser, *args, **kwargs):
-        from .native.detectors import get_detectors_classes, output_detectors
-
-        output_detectors(get_detectors_classes())
-        parser.exit()
-
-
 if __name__ == "__main__":
     main()

manticore/core/smtlib/visitors.py

@@ -488,6 +488,18 @@ def visit_BitVecSub(self, expression, *operands):
                 return left.operands[1]
             elif self._same_constant(left.operands[1], right):
                 return left.operands[0]
+        elif isinstance(left, BitVecSub) and isinstance(right, Constant):
+            subleft = left.operands[0]
+            subright = left.operands[1]
+            if isinstance(subright, Constant):
+                return BitVecSub(
+                    subleft,
+                    BitVecConstant(
+                        subleft.size,
+                        subright.value + right.value,
+                        taint=subright.taint | right.taint,
+                    ),
+                )
 
     def visit_BitVecOr(self, expression, *operands):
         """ a | 0 => a

manticore/ethereum/manticore.py

@@ -1165,7 +1165,6 @@ def multi_tx_analysis(
         if contract_account is None:
             logger.info("Failed to create contract: exception in constructor")
             return
-
         prev_coverage = 0
         current_coverage = 0
         tx_no = 0
@@ -1478,13 +1477,16 @@ def generate_testcase(self, state, message="", only_if=None, name="user"):
                 else:
                     return False
 
+        blockchain = state.platform
+
         # FIXME. workspace should not be responsible for formating the output
         # each object knows its secrets, and each class should be able to report
         # its final state
-        testcase = super().generate_testcase(state, message, name=name)
+        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.
-        blockchain = state.platform
 
         local_findings = set()
         for detector in self.detectors.values():

manticore/native/cli.py

@@ -47,7 +47,7 @@ def native_main(args, _logger):
 
     # Default plugins for now.. FIXME REMOVE!
     m.register_plugin(InstructionCounter())
-    m.register_plugin(Visited())
+    m.register_plugin(Visited(args.coverage))
     m.register_plugin(Tracer())
     m.register_plugin(RecordSymbolicBranches())
 
@@ -65,10 +65,9 @@ def native_main(args, _logger):
         m.load_assertions(args.assertions)
 
     @m.init
-    def init(m, ready_states):
+    def init(state):
         for file in args.files:
-            for state in ready_states:
-                state.platform.add_symbolic_file(file)
+            state.platform.add_symbolic_file(file)
 
     for detector in list(m.detectors):
         m.unregister_detector(detector)