Merge branch 'master' into fix-emulate-step

* master: (22 commits) 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) Use Slots on all Expression objects (#2394) Allow double-adding exact same config option (#2397) Don't run OSX tests on PR Attempt to Fix solc Installation MacOS (#2392) Syscall specific hooks (#2389) TUI Support Infrastructure (#1620) Fix coveralls upload (#2387) docs: fix simple typo, straigth -> straight (#2381) Attempt to allow symbolic balances from the start (#1818) Fix state.cpu.PC member (#1825) Bump black and mypy (#1824) Manticore 0.3.5 (#1808) Fix yices timeout argument (#1817) ...
trailofbits · Apr 10, 2021 · c3d7885 · c3d7885
2 parents 565b35c + b4d129f
commit c3d7885
Show file tree

Hide file tree

Showing 66 changed files with 17,386 additions and 15,610 deletions.
diff --git a/.github/workflows/ci.yml b/.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:

diff --git a/.github/workflows/osx.yml b/.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 }}

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/evm/minimal.py b/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(

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
@@ -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
 

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