merge master in

feliam · feliam · commit d46eea1b0e86 · 2021-01-15T16:42:09.000-03:00
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,6 +1,37 @@
 # Change Log
 
-## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.4...HEAD)
+## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.5...HEAD)
+
+## 0.3.5 - 2020-11-06
+
+Thanks to our external contributors!
+ - [wolfo](https://github.com/trailofbits/manticore/commits?author=wolfo)
+ - [geohot](https://github.com/trailofbits/manticore/commits?author=geohot)
+ - [romits800](https://github.com/trailofbits/manticore/commits?author=romits800)
+
+### Ethereum
+* Made EVM module ignore runtime gas calculations by default [#1816](https://github.com/trailofbits/manticore/pull/1816)
+* Updated gas calculations for calls to empty accounts [#1774](https://github.com/trailofbits/manticore/pull/1774)
+* Fixed account existence checks for `selfdestruct` and `call` [#1801](https://github.com/trailofbits/manticore/pull/1801)
+
+### Native
+* **[Added API]** new `strlen` models [#1725](https://github.com/trailofbits/manticore/pull/1725)
+* **[Added API]** State-specific hooks [#1777](https://github.com/trailofbits/manticore/pull/1777)
+* Improved system call argument handling [#1785](https://github.com/trailofbits/manticore/pull/1785)
+* Improved `stat` support for file descriptors [#1780](https://github.com/trailofbits/manticore/pull/1780)
+* Support symbolic-length reads from sockets [#1786](https://github.com/trailofbits/manticore/pull/1786)
+* Add stubs for `sendto` [#1791](https://github.com/trailofbits/manticore/pull/1791)
+
+### WASM
+* Fix type confusion when importing external functions [#1803](https://github.com/trailofbits/manticore/pull/1803)
+
+### Other
+* Made [Yices2](https://yices.csl.sri.com/) the default SMT Solver [#1820](https://github.com/trailofbits/manticore/pull/1820)
+* **[Added API]** Added an API for introspecting live states [#1775](https://github.com/trailofbits/manticore/pull/1775)
+* Changed default multiprocessing type to threading [#1779](https://github.com/trailofbits/manticore/pull/1779)
+* Improved array serialization performance [#1756](https://github.com/trailofbits/manticore/pull/1756)
+* Fix name collisions in SMT variables [#1792](https://github.com/trailofbits/manticore/pull/1792)
+
 
 ## 0.3.4 - 2020-06-26
 
diff --git a/README.md b/README.md
@@ -229,10 +229,10 @@ for idx, val_list in enumerate(m.collect_returns()):
 * We're still in the process of implementing full support for the EVM Istanbul instruction semantics, so certain opcodes may not be supported.
 In a pinch, you can try compiling with Solidity 0.4.x to avoid generating those instructions. 
 
-## Using a different solver (Z3, Yices, CVC4)
+## Using a different solver (Yices, Z3, CVC4)
 Manticore relies on an external solver supporting smtlib2. Currently Z3, Yices and CVC4 are supported and can be selected via commandline or configuration settings.
-By default Manticore will use Z3. Once you've installed a different solver, you can choose which one to use like this:
-```manticore --smt.solver yices```
+If Yices is available, Manticore will use it by default. If not, it will fall back to Z3 or CVC4. If you want to manually choose which solver to use, you can do so like this:
+```manticore --smt.solver Z3```
 ### Installing CVC4
 For more details go to https://cvc4.github.io/. Otherwise just get the binary and use it.
 
diff --git a/docs/conf.py b/docs/conf.py
@@ -54,9 +54,9 @@
 # built documents.
 #
 # The short X.Y version.
-version = "0.3.4"
+version = "0.3.5"
 # The full version, including alpha/beta/rc tags.
-release = "0.3.4"
+release = "0.3.5"
 
 # The language for content autogenerated by Sphinx. Refer to documentation
 # for a list of supported languages.
diff --git a/examples/linux/introspect_state.py b/examples/linux/introspect_state.py
@@ -9,7 +9,11 @@
     description="Explore a binary with Manticore and print the tree of states"
 )
 parser.add_argument(
-    "binary", type=str, nargs="?", default="binaries/multiple-styles", help="The program to run",
+    "binary",
+    type=str,
+    nargs="?",
+    default="binaries/multiple-styles",
+    help="The program to run",
 )
 args = parser.parse_args()
 
diff --git a/examples/script/concolic.py b/examples/script/concolic.py
@@ -110,7 +110,7 @@ def eq(a, b):
 
 
 def perm(lst, func):
-    """ Produce permutations of `lst`, where permutations are mutated by `func`. Used for flipping constraints. highly
+    """Produce permutations of `lst`, where permutations are mutated by `func`. Used for flipping constraints. highly
     possible that returned constraints can be unsat this does it blindly, without any attention to the constraints
     themselves
 
diff --git a/manticore/__main__.py b/manticore/__main__.py
@@ -211,7 +211,9 @@ def positive(value):
     )
 
     eth_flags.add_argument(
-        "--limit-loops", action="store_true", help="Limit loops depth",
+        "--limit-loops",
+        action="store_true",
+        help="Limit loops depth",
     )
 
     eth_flags.add_argument(
diff --git a/manticore/core/plugin.py b/manticore/core/plugin.py
@@ -638,7 +638,9 @@ def on_execution_intermittent_callback(
                     state.id,
                 )
             update_cb(
-                context.setdefault(state.id, StateDescriptor(state_id=state.id)), *args, **kwargs,
+                context.setdefault(state.id, StateDescriptor(state_id=state.id)),
+                *args,
+                **kwargs,
             )
             context[state.id].last_intermittent_update = datetime.now()
 
diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py
@@ -63,7 +63,7 @@ class SolverType(config.ConfigEnum):
 
 consts.add(
     "solver",
-    default=SolverType.yices,
+    default=SolverType.auto,
     description="Choose default smtlib2 solver (z3, yices, cvc4, auto)",
 )
 
@@ -794,7 +794,7 @@ def _solver_version(self) -> Version:
 class YicesSolver(SMTLIBSolver):
     def __init__(self):
         init = ["(set-logic QF_AUFBV)"]
-        command = f"{consts.yices_bin} --timeout={consts.timeout * 1000}  --incremental"
+        command = f"{consts.yices_bin} --timeout={consts.timeout}  --incremental"
         super().__init__(
             command=command,
             init=init,
diff --git a/manticore/core/worker.py b/manticore/core/worker.py
@@ -246,7 +246,10 @@ def start(self, target: typing.Optional[typing.Callable] = None):
         thread as an argument.
         """
         logger.debug(
-            "Starting Daemon %d. (Pid %d Tid %d).", self.id, os.getpid(), threading.get_ident(),
+            "Starting Daemon %d. (Pid %d Tid %d).",
+            self.id,
+            os.getpid(),
+            threading.get_ident(),
         )
 
         self._t = threading.Thread(target=self.run if target is None else target, args=(self,))
diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
@@ -797,7 +797,7 @@ def create_account(self, balance=0, address=None, code=None, name=None, nonce=No
             raise EthereumError("Name already used")
 
         # Balance check
-        if not isinstance(balance, int):
+        if not isinstance(balance, (int, BitVec)):
             raise EthereumError("Balance invalid type")
 
         if isinstance(code, str):
diff --git a/manticore/ethereum/verifier.py b/manticore/ethereum/verifier.py
@@ -366,7 +366,11 @@ def main():
     cryticparser.init(parser)
 
     parser.add_argument(
-        "source_code", type=str, nargs="*", default=[], help="Contract source code",
+        "source_code",
+        type=str,
+        nargs="*",
+        default=[],
+        help="Contract source code",
     )
     parser.add_argument(
         "-v", action="count", default=0, help="Specify verbosity level from -v to -vvvv"
@@ -387,7 +391,9 @@ def main():
         help="Show program version information",
     )
     parser.add_argument(
-        "--propconfig", type=str, help="Solidity property accounts config file (.yml)",
+        "--propconfig",
+        type=str,
+        help="Solidity property accounts config file (.yml)",
     )
     eth_flags = parser.add_argument_group("Ethereum flags")
 
diff --git a/manticore/native/cpu/abstractcpu.py b/manticore/native/cpu/abstractcpu.py
@@ -90,7 +90,11 @@ class ConcretizeRegister(CpuException):
     """
 
     def __init__(
-        self, cpu: "Cpu", reg_name: str, message: Optional[str] = None, policy: str = "MINMAX",
+        self,
+        cpu: "Cpu",
+        reg_name: str,
+        message: Optional[str] = None,
+        policy: str = "MINMAX",
     ):
         self.message = message if message else f"Concretizing {reg_name}"
 
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
@@ -42,7 +42,7 @@
 logger = logging.getLogger(__name__)
 
 # Gas behaviour configuration
-# When gas is concrete the gas checks and calculation are pretty straigth forward
+# When gas is concrete the gas checks and calculation are pretty straight forward
 # Though Gas can became symbolic in normal bytecode execution for example at instructions
 # MSTORE, MSTORE8, EXP, ... and every instruction with internal operation restricted by gas
 # This configuration variable allows the user to control and perhaps relax the gas calculation
@@ -69,7 +69,7 @@ def globalfakesha3(data):
 
 consts.add(
     "oog",
-    default="complete",
+    default="ignore",
     description=(
         "Default behavior for symbolic out of gas exception."
         "pedantic: Fully faithful. Test at every instruction. Forks."
@@ -103,7 +103,9 @@ def globalfakesha3(data):
     description="Max calldata size to explore in each CALLDATACOPY. Iff size in a calldata related instruction are symbolic it will be constrained to be less than this constant. -1 means free(only use when gas is being tracked)",
 )
 consts.add(
-    "ignore_balance", default=False, description="Do not try to solve symbolic balances",
+    "ignore_balance",
+    default=False,
+    description="Do not try to solve symbolic balances",
 )
 
 
@@ -3175,6 +3177,9 @@ def create_account(self, address=None, balance=0, code=None, storage=None, nonce
             # As per EIP 161, contract accounts are initialized with a nonce of 1
             nonce = 1 if len(code) > 0 else 0
 
+        if isinstance(balance, BitVec):
+            balance = Operators.ZEXTEND(balance, 512)
+
         if address is None:
             address = self.new_address()
 
diff --git a/setup.py b/setup.py
@@ -18,7 +18,7 @@ def rtd_dependent_deps():
 # (we need to know how to import a given native dependency so we can check if native dependencies are installed)
 native_deps = ["capstone==4.0.1", "pyelftools", "unicorn==1.0.2rc2"]
 
-lint_deps = ["black==19.10b0", "mypy==0.790"]
+lint_deps = ["black==20.8b1", "mypy==0.790"]
 
 auto_test_deps = ["py-evm"]
 
@@ -57,7 +57,7 @@ def rtd_dependent_deps():
     long_description=long_description,
     url="https://github.com/trailofbits/manticore",
     author="Trail of Bits",
-    version="0.3.4" + dev_extension,
+    version="0.3.5" + dev_extension,
     packages=find_packages(exclude=["tests", "tests.*"]),
     python_requires=">=3.6",
     install_requires=[
diff --git a/tests/native/test_aarch64cpu.py b/tests/native/test_aarch64cpu.py
@@ -40,7 +40,7 @@ def _ks_assemble(asm: str) -> bytes:
 def assemble(asm: str) -> bytes:
     """
     Assemble the given string.
-    
+
     An assembly cache is first checked, and if there is no entry there, then Keystone is used.
     """
     if asm in assembly_cache:
diff --git a/tests/native/test_armv7cpu.py b/tests/native/test_armv7cpu.py
@@ -280,7 +280,7 @@ def _ks_assemble(asm: str, mode=CS_MODE_ARM) -> bytes:
 def assemble(asm: str, mode=CS_MODE_ARM) -> bytes:
     """
     Assemble the given string.
-    
+
     An assembly cache is first checked, and if there is no entry there, then Keystone is used.
     """
     if asm in assembly_cache[mode]:
diff --git a/tests/native/test_armv7unicorn.py b/tests/native/test_armv7unicorn.py
@@ -184,7 +184,7 @@ def _ks_assemble(asm: str, mode=CS_MODE_ARM) -> bytes:
 def assemble(asm: str, mode=CS_MODE_ARM) -> bytes:
     """
     Assemble the given string.
-    
+
     An assembly cache is first checked, and if there is no entry there, then Keystone is used.
     """
     if asm in assembly_cache[mode]:
diff --git a/tests/native/test_cpu_automatic.py b/tests/native/test_cpu_automatic.py
diff --git a/tests/native/test_cpu_manual.py b/tests/native/test_cpu_manual.py
diff --git a/tests/native/test_dyn.py b/tests/native/test_dyn.py
diff --git a/tests/native/test_slam_regre.py b/tests/native/test_slam_regre.py
diff --git a/tests/native/test_x86.py b/tests/native/test_x86.py
diff --git a/tests/native/test_x86_pcmpxstrx.py b/tests/native/test_x86_pcmpxstrx.py

Original file line number	Diff line number	Diff line change
`@@ -9,7 +9,11 @@`
`9`	`9`	`description="Explore a binary with Manticore and print the tree of states"`
`10`	`10`	`)`
`11`	`11`	`parser.add_argument(`
`12`		`- "binary", type=str, nargs="?", default="binaries/multiple-styles", help="The program to run",`
	`12`	`+ "binary",`
	`13`	`+ type=str,`
	`14`	`+ nargs="?",`
	`15`	`+ default="binaries/multiple-styles",`
	`16`	`+ help="The program to run",`
`13`	`17`	`)`
`14`	`18`	`args = parser.parse_args()`
`15`	`19`
Original file line number	Diff line number	Diff line change
`@@ -211,7 +211,9 @@ def positive(value):`
`211`	`211`	`)`
`212`	`212`
`213`	`213`	`eth_flags.add_argument(`
`214`		`- "--limit-loops", action="store_true", help="Limit loops depth",`
	`214`	`+ "--limit-loops",`
	`215`	`+ action="store_true",`
	`216`	`+ help="Limit loops depth",`
`215`	`217`	`)`
`216`	`218`
`217`	`219`	`eth_flags.add_argument(`
Original file line number	Diff line number	Diff line change
`@@ -638,7 +638,9 @@ def on_execution_intermittent_callback(`
`638`	`638`	`state.id,`
`639`	`639`	`)`
`640`	`640`	`update_cb(`
`641`		`- context.setdefault(state.id, StateDescriptor(state_id=state.id)), args, *kwargs,`
	`641`	`+ context.setdefault(state.id, StateDescriptor(state_id=state.id)),`
	`642`	`+ *args,`
	`643`	`+ **kwargs,`
`642`	`644`	`)`
`643`	`645`	`context[state.id].last_intermittent_update = datetime.now()`
`644`	`646`