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)
trailofbits · May 30, 2019 · 06702d8 · 06702d8
2 parents 82e23e6 + ddb833d
commit 06702d8
Show file tree

Hide file tree

Showing 40 changed files with 606 additions and 71,638 deletions.
diff --git a/.codeclimate.yml b/.codeclimate.yml
@@ -48,6 +48,10 @@ plugins:
         enabled: false
       E701:
         enabled: false
+      E203:
+        enabled: false
+      W503:
+        enabled: false
   sonar-python:
     enabled: false
     config:

diff --git a/.travis.yml b/.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"

diff --git a/CONTRIBUTING.md b/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.

diff --git a/docs/conf.py b/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.

diff --git a/examples/script/aarch64/basic.py b/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.

diff --git a/examples/script/aarch64/hello42.py b/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")
diff --git a/manticore/__main__.py b/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()
diff --git a/manticore/core/smtlib/visitors.py b/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

diff --git a/manticore/ethereum/manticore.py b/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():

diff --git a/manticore/native/cli.py b/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)

diff --git a/manticore/native/cpu/x86.py b/manticore/native/cpu/x86.py
@@ -5709,6 +5709,27 @@ def MOVHPD(cpu, dest, src):
             value = Operators.EXTRACT(dest.read(), 0, 64)  # low part
             dest.write(Operators.CONCAT(128, src.read(), value))
 
+    @instruction
+    def MOVHPS(cpu, dest, src):
+        """
+        Moves high packed single-precision floating-point value.
+
+        Moves two packed single-precision floating-point values from the source operand
+        (second operand) to the destination operand (first operand). The source and destination
+        operands can be an XMM register or a 64-bit memory location. The instruction allows
+        single-precision floating-point values to be moved to and from the high quadword of
+        an XMM register and memory. It cannot be used for register to register or memory to
+        memory moves. When the destination operand is an XMM register, the low quadword
+        of the register remains unchanged.
+        """
+        if src.size == 128:
+            assert dest.size == 64
+            dest.write(Operators.EXTRACT(src.read(), 64, 64))
+        else:
+            assert src.size == 64 and dest.size == 128
+            value = Operators.EXTRACT(dest.read(), 0, 64)  # low part
+            dest.write(Operators.CONCAT(128, src.read(), value))
+
     @instruction
     def PSUBB(cpu, dest, src):
         """

diff --git a/manticore/native/manticore.py b/manticore/native/manticore.py
@@ -57,10 +57,10 @@ def __init__(self, path_or_state, argv=None, workspace_url=None, policy="random"
 
         # Move the following into a linux plugin
         self._assertions = {}
-        self._coverage_file = None
         self.trace = None
         # sugar for 'will_execute_instruction"
         self._hooks = {}
+        self._init_hooks = set()
 
         # self.subscribe('will_generate_testcase', self._generate_testcase_callback)
 
@@ -100,15 +100,6 @@ def _model_hook_callback(self, state, instruction):
         for cb in self._model_hooks[pc]:
             cb(state)
 
-    @property
-    def coverage_file(self):
-        return self._coverage_file
-
-    @coverage_file.setter
-    @ManticoreBase.at_not_running
-    def coverage_file(self, path):
-        self._coverage_file = path
-
     def _generate_testcase_callback(self, state, testcase, message):
         """
         Create a serialized description of a given state.
@@ -282,7 +273,9 @@ def init(self, f):
         A decorator used to register a hook function to run before analysis begins. Hook
         function takes one :class:`~manticore.core.state.State` argument.
         """
-        self.subscribe("will_run", f)
+        self._init_hooks.add(f)
+        if self._init_hooks:
+            self.subscribe("will_run", self._init_callback)
         return f
 
     def hook(self, pc):
@@ -335,6 +328,13 @@ def _hook_callback(self, state, pc, instruction):
         for cb in self._hooks.get(None, []):
             cb(state)
 
+    def _init_callback(self, ready_states):
+        for cb in self._init_hooks:
+            # We _should_ only ever have one starting state. Right now we're putting
+            # this in a loop for futureproofing.
+            for state in ready_states:
+                cb(state)
+
     ###############################
     # Symbol Resolution
     ###############################