Merge branch 'master' of github.com:trailofbits/manticore into ss/hea…

…p_tracker

.github/workflows/ci.yml

@@ -77,7 +77,7 @@ jobs:
         ./run_tests.sh
     - name: Coveralls Parallel
       run: |
-        coveralls
+        coveralls --service=github
       env:
         COVERALLS_PARALLEL: true
         GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
@@ -87,7 +87,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Coveralls Finished
-      uses: coverallsapp/github-action@v1.1.1
+      uses: coverallsapp/github-action@v1.1.2
       with:
         github-token: ${{ secrets.GITHUB_TOKEN }}
         parallel-finished: true

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
 

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.
 

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.

examples/evm/minimal.py

@@ -24,8 +24,7 @@
     } 
 }
 """
-
-user_account = m.create_account(balance=1000, name="user_account")
+user_account = m.create_account(balance=m.make_symbolic_value(), name="user_account")
 print("[+] Creating a user account", user_account.name_)
 
 contract_account = m.solidity_create_contract(

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()
 

examples/script/concolic.py

@@ -109,7 +109,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
 

manticore/__main__.py

@@ -209,7 +209,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(