Merge branch 'master' into capstone-5-dev

* master: (35 commits)
  Track last_pc in StateDescriptors (#2471)
  Expose Result Register for Native CPU (#2470)
  Install pinned version of truffle to fix CI (#2467)
  Use fixed owner and attacker accounts in multi_tx_analysis (#2464)
  Manticore 0.3.6 (#2456)
  Fix IntrospectionAPIPlugin Name (#2459)
  Portfolio of parallel solvers (#2420)
  Replace Quick mode with Thorough mode (#2457)
  Fix incorrect comparison for symbolic file wildcards (#2454)
  Reduce the number of calls to the SMT solver in EVM (#2411)
  Fixes to Unicorn emulation - start/stop/resume (#1796)
  Add support for multiple compilation units (#2444)
  Basic solver stats (#2415)
  Fix the generation of EVM tests (#2426)
  Disabled EVM events in testcases by default (#2417)
  added proper timeouts for cvc4 and boolector (#2418)
  Removed use of global solver from Native Memory (#2414)
  Support to use boolector as the SMT solver (#2410)
  Update CI and suggest to use pip3 instead of pip (#2409)
  Expressions use keyword-only arguments for init (#2395)
  ...

Author: ekilmer

.github/workflows/ci.yml

@@ -12,7 +12,7 @@ on:
 jobs:
   # needs to run only on pull_request
   lint:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-18.04
     steps:
     - uses: actions/checkout@v2
     - name: Set up Python 3.6
@@ -39,7 +39,7 @@ jobs:
         mypy --version
         mypy
   tests:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-18.04
     strategy:
       matrix:
         type: ["ethereum_truffle", "ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "wasm", "wasm_sym", "other"]
@@ -57,18 +57,34 @@ jobs:
       env:
         TEST_TYPE: ${{ matrix.type }}
       run: |
+        #install utils
+        pip install coveralls
+        pip install -e ".[dev-noks]"
         #install cvc4
         sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
         sudo chmod +x /usr/bin/cvc4
         #install yices
         sudo add-apt-repository ppa:sri-csl/formal-methods
         sudo apt-get update
         sudo apt-get install yices2
+        #install boolector
+        mkdir -p /tmp/build
+        cd /tmp/build
+        git clone https://github.com/boolector/boolector.git
+        cd boolector
+        # Version 3.2.1
+        git checkout "f61c0dcf4a76e2f7766a6358bfb9c16ca8217224"
+        git log -1 --oneline > ../boolector.commit
+        ./contrib/setup-lingeling.sh
+        ./contrib/setup-btor2tools.sh
+        ./configure.sh
+        cd build
+        make -j4
+        mkdir -p /tmp/boolector
+        sudo make DESTDIR=/usr install
         # Install solc unconditionally because it only takes a second or two
         sudo wget -O /usr/bin/solc https://github.com/ethereum/solidity/releases/download/v0.4.24/solc-static-linux
         sudo chmod +x /usr/bin/solc
-        pip install coveralls
-        pip install -e ".[dev-noks]"
     - name: Run Tests
       env:
         TEST_TYPE: ${{ matrix.type }}
@@ -77,22 +93,22 @@ jobs:
         ./run_tests.sh
     - name: Coveralls Parallel
       run: |
-        coveralls
+        coveralls --service=github
       env:
         COVERALLS_PARALLEL: true
         GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
   # Send notification when all tests have finished to combine coverage results
   coverage-finish:
     needs: tests
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-18.04
     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
   upload:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-18.04
     if: github.event_name == 'schedule'
     needs: tests
     steps:

.github/workflows/osx.yml

@@ -31,12 +31,13 @@ jobs:
     - name: Install Mac Dependencies
       run: |
         brew install bash
-        brew tap ethereum/ethereum
-        brew install solidity@4
         brew install wabt
         brew install SRI-CSL/sri-csl/yices2
         brew tap cvc4/cvc4
         brew install cvc4/cvc4/cvc4
+        pip install solc-select
+        solc-select install 0.4.26
+        solc-select use 0.4.26
     - name: Run Tests
       env:
         TEST_TYPE: ${{ matrix.type }}

.github/workflows/release.yml

@@ -0,0 +1,78 @@
+name: Upload to PyPI
+
+on:
+  release:
+    types: [published]
+
+jobs:
+  tests:
+    runs-on: ubuntu-18.04
+    strategy:
+      matrix:
+        type: ["ethereum_truffle", "ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "wasm", "wasm_sym", "other"]
+    steps:
+    - uses: actions/checkout@v1
+    - name: Set up Python 3.6
+      uses: actions/setup-python@v1
+      with:
+        python-version: 3.6
+    - name: Install NPM
+      uses: actions/setup-node@v1
+      with:
+        node-version: '13.x'
+    - name: Install dependencies
+      env:
+        TEST_TYPE: ${{ matrix.type }}
+      run: |
+        #install utils
+        pip install coveralls
+        pip install -e ".[dev-noks]"
+        #install cvc4
+        sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
+        sudo chmod +x /usr/bin/cvc4
+        #install yices
+        sudo add-apt-repository ppa:sri-csl/formal-methods
+        sudo apt-get update
+        sudo apt-get install yices2
+        #install boolector
+        mkdir -p /tmp/build
+        cd /tmp/build
+        git clone https://github.com/boolector/boolector.git
+        cd boolector
+        # Version 3.2.1
+        git checkout "f61c0dcf4a76e2f7766a6358bfb9c16ca8217224"
+        git log -1 --oneline > ../boolector.commit
+        ./contrib/setup-lingeling.sh
+        ./contrib/setup-btor2tools.sh
+        ./configure.sh
+        cd build
+        make -j4
+        mkdir -p /tmp/boolector
+        sudo make DESTDIR=/usr install
+        # Install solc unconditionally because it only takes a second or two
+        sudo wget -O /usr/bin/solc https://github.com/ethereum/solidity/releases/download/v0.4.24/solc-static-linux
+        sudo chmod +x /usr/bin/solc
+    - name: Run Tests
+      env:
+        TEST_TYPE: ${{ matrix.type }}
+      run: |
+        cp scripts/run_tests.sh .
+        ./run_tests.sh
+
+  upload:
+    runs-on: ubuntu-18.04
+    needs: tests
+    steps:
+    - uses: actions/checkout@v2
+    - name: Set up Python 3.6
+      uses: actions/setup-python@v1
+      with:
+        python-version: 3.6
+    - name: Build Dist
+      run: |
+        python3 -m pip install wheel
+        python3 setup.py sdist bdist_wheel
+    - name: Upload to PyPI
+      uses: pypa/gh-action-pypi-publish@v1.2.2
+      with:
+        password: ${{ secrets.PYPI_UPLOAD }}

CHANGELOG.md

@@ -1,6 +1,61 @@
 # Change Log
 
-## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.4...HEAD)
+## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.6...HEAD)
+
+## 0.3.6 - 2021-06-09
+
+Thanks to our external contributors!
+ - [timgates42](https://github.com/trailofbits/manticore/commits?author=timgates42)
+
+### Ethereum
+* **[Changed API]** Default to quick mode: disable detectors and gas [#2457](https://github.com/trailofbits/manticore/pull/2457)
+* Allow symbolic balances from the beginning of execution [#1818](https://github.com/trailofbits/manticore/pull/1818)
+* Disable EVM Events in Testcases [#2417](https://github.com/trailofbits/manticore/pull/2417)
+
+### Native
+* **[Added API]** Syscall-specific hooks [#2389](https://github.com/trailofbits/manticore/pull/2389)
+* Fix wildcard behavior in symbolic files [#2454](https://github.com/trailofbits/manticore/pull/2454)
+* Bugfixes for control transfer between Manticore & Unicorn [#1796](https://github.com/trailofbits/manticore/pull/1796)
+
+### Other
+* Run multiple SMT solvers in parallel, take the fastest response [#2420](https://github.com/trailofbits/manticore/pull/2420)
+* Add socket for TUI [#1620](https://github.com/trailofbits/manticore/pull/1620)
+* Memory usage improvements in expression system [#2394](https://github.com/trailofbits/manticore/pull/2394)
+* Support for Boolector [#2410](https://github.com/trailofbits/manticore/pull/2410)
+* Solver Statistics API [#2415](https://github.com/trailofbits/manticore/pull/2415)
+* Allow duplicated config options [#2397](https://github.com/trailofbits/manticore/pull/2397)
+
+
+## 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

@@ -46,10 +46,10 @@ Option 2: Installing from PyPI, with extra dependencies needed to execute native
 pip install "manticore[native]"
 ```
 
-Option 3: Installing a nightly development build (fill in the latest version from [the PyPI history](https://pypi.org/project/manticore/#history)):
+Option 3: Installing a nightly development build:
 
 ```bash
-pip install "manticore[native]==0.x.x.devYYMMDD"
+pip install --pre "manticore[native]"
 ```
 
 Option 4: Installing from the `master` branch:
@@ -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.6"
 # The full version, including alpha/beta/rc tags.
-release = "0.3.4"
+release = "0.3.6"
 
 # 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
 

examples/script/symbolic_file.py

@@ -0,0 +1,77 @@
+#!/usr/bin/env python
+
+"""
+Example to show usage of introducing a file with symbolic contents
+
+This script should be the equivalent of:
+    $ echo "+++++++++++++" > symbolic_file.txt
+    $ manticore -v --file symbolic_file.txt ../linux/fileio symbolic_file.txt
+"""
+import copy
+import glob
+import os
+import pathlib
+import sys
+import tempfile
+
+from manticore.__main__ import main
+
+
+def test_symbolic_file(tmp_path):
+    # Run this file with Manticore
+    filepath = pathlib.Path(__file__).resolve().parent.parent / pathlib.Path("linux/fileio")
+    assert filepath.exists(), f"Please run the Makefile in {filepath.parent} to build {filepath}"
+
+    # Temporary workspace for Manticore
+    workspace_dir = tmp_path / "mcore_workspace"
+    workspace_dir.mkdir(parents=True, exist_ok=True)
+    assert (
+        len(os.listdir(workspace_dir)) == 0
+    ), f"Manticore workspace {workspace_dir} should be empty before running"
+
+    # Manticore will search for and read this partially symbolic file
+    sym_file_name = "symbolic_file.txt"
+    sym_file = tmp_path / sym_file_name
+    sym_file.write_text("+++++++++++++")
+
+    # Program arguments that would be passed to Manticore via CLI
+    manticore_args = [
+        # Show some progress
+        "-v",
+        # Register our symbolic file with Manticore
+        "--file",
+        str(sym_file),
+        # Setup workspace, for this test, or omit to use current directory
+        "--workspace",
+        str(workspace_dir),
+        # Manticore will execute our file here with arguments
+        str(filepath),
+        str(sym_file),
+    ]
+
+    # Bad hack to workaround passing the above arguments like we do on command
+    # line and have them parsed with argparse
+    backup_argv = copy.deepcopy(sys.argv[1:])
+    del sys.argv[1:]
+    sys.argv.extend(manticore_args)
+
+    # Call Manticore's main with our new argv list for argparse
+    main()
+
+    del sys.argv[1:]
+    sys.argv.extend(backup_argv)
+
+    # Manticore will write out the concretized contents of our symbolic file for
+    # each path in the program
+    all_concretized_sym_files = glob.glob(str(workspace_dir / f"*{sym_file_name}"))
+    assert (
+        len(all_concretized_sym_files) > 1
+    ), "Should have found more than 1 path through the program"
+    assert any(
+        map(lambda f: b"open sesame" in pathlib.Path(f).read_bytes(), all_concretized_sym_files)
+    ), "Could not find 'open sesame' in our concretized symbolic file"
+
+
+if __name__ == "__main__":
+    with tempfile.TemporaryDirectory() as workspace:
+        test_symbolic_file(pathlib.Path(workspace))