Merge pull request #7 from trailofbits/master

Add Manticore native State-specific hooks (trailofbits#1777)

.coveragerc

@@ -2,3 +2,11 @@
 source = manticore
 omit =
 	*__init__.py
+
+[report]
+exclude_lines =
+    # Have to re-enable the standard pragma
+    pragma: no cover
+
+    # Don't try to cover special syntax "..." in abstract class
+    @abstractmethod

.github/ISSUE_TEMPLATE/config.yml

@@ -1,11 +1,5 @@
 blank_issues_enabled: false
 contact_links:
-  - name: Bug Report
-    url: https://github.com/trailofbits/manticore/issues/new?labels=bug&template=bug_report.md
-    about: Report a bug in Manticore
-  - name: Feature Request
-    url: https://github.com/trailofbits/manticore/issues/new?labels=idea&template=feature_request.md
-    about: Request a new feature in Manticore
   - name: Ask a Question
     url: https://github.com/trailofbits/manticore/discussions/new
     about: Ask for help or clarification from the developers

.github/workflows/ci.yml

@@ -23,11 +23,13 @@ jobs:
       if: github.event_name == 'pull_request'
       env:
         BASE_SHA: ${{ github.event.pull_request.base.sha }}
-        HEAD_SHA: ${{ github.event.pull_request.head.sha }}
       run: |
         pip install -e .[lint]
         black --version
-        git diff --name-only $BASE_SHA..$HEAD_SHA | python scripts/pyfile_exists.py | xargs black --diff --check
+        git fetch --depth=1 origin $BASE_SHA
+        echo "Files Changed:"
+        git diff --name-only $BASE_SHA... | tee .diff_names.txt
+        cat .diff_names.txt | python scripts/pyfile_exists.py | xargs black --diff --check
         mypy --version
         mypy
   tests:
@@ -49,187 +51,57 @@ jobs:
       env:
         TEST_TYPE: ${{ matrix.type }}
       run: |
+        #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 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 }}
       run: |
-        # Launches all examples; this assumes PWD is examples/script
-        launch_examples() {
-            # concolic assumes presence of ../linux/simpleassert
-            echo "Running concolic.py..."
-            HW=../linux/helloworld
-            coverage run ./concolic.py
-            if [ $? -ne 0 ]; then
-                return 1
-            fi
-
-            echo "Running count_instructions.py..."
-            coverage run ./count_instructions.py $HW |grep -q Executed
-            if [ $? -ne 0 ]; then
-                return 1
-            fi
-
-            echo "Running introduce_symbolic_bytes.py..."
-            gcc -static -g src/state_explore.c -o state_explore
-            ADDRESS=0x$(objdump -S state_explore | grep -A 1 '((value & 0xff) != 0)' |
-                    tail -n 1 | sed 's|^\s*||g' | cut -f1 -d:)
-            coverage run ./introduce_symbolic_bytes.py state_explore $ADDRESS
-            if [ $? -ne 0 ]; then
-                return 1
-            fi
-
-            echo "Running run_simple.py..."
-            gcc -x c -static -o hello test_run_simple.c
-            coverage run ./run_simple.py hello
-            if [ $? -ne 0 ]; then
-                return 1
-            fi
-
-            echo "Running run_hook.py..."
-            MAIN_ADDR=$(nm $HW|grep 'T main' | awk '{print "0x"$1}')
-            coverage run ./run_hook.py $HW $MAIN_ADDR
-            if [ $? -ne 0 ]; then
-                return 1
-            fi
-
-            echo "Running state_control.py..."
-            # Straight from the header of state_control.py
-            gcc -static -g src/state_explore.c -o state_explore
-            SE_ADDR=0x$(objdump -S state_explore | grep -A 1 'value == 0x41' |
-                       tail -n 1 | sed 's|^\s*||g' | cut -f1 -d:)
-            coverage run ./state_control.py state_explore $SE_ADDR
-            if [ $? -ne 0 ]; then
-                return 1
-            fi
-
-            return 0
-        }
-
-        make_vmtests(){
-            DIR=`pwd`
-            if  [ ! -f ethereum_vm/.done ]; then
-                echo "Automaking VMTests" `pwd`
-                cd ./tests/ && mkdir -p  ethereum_vm/VMTests_concrete && mkdir -p ethereum_vm/VMTests_symbolic
-                rm -Rf vmtests; git clone https://github.com/ethereum/tests --depth=1 vmtests
-                for i in ./vmtests/VMTests/*; do python ./auto_generators/make_VMTests.py $i; done
-                for i in ./vmtests/VMTests/*; do python ./auto_generators/make_VMTests.py $i --symbolic; done
-                rm -rf ./vmtests
-                touch ethereum_vm/.done
-            fi
-            cd $DIR
-        }
-
-        make_wasm_tests(){
-            DIR=`pwd`
-            if  [ ! -f .wasm_done ]; then
-                echo "Automaking WASM Tests" `pwd`
-                cd ./tests/wasm
-                ./generate_tests.sh
-                touch .wasm_done
-            fi
-            cd $DIR
-        }
-
-        make_wasm_sym_tests(){
-            DIR=`pwd`
-            if  [ ! -f .wasm_sym_done ]; then
-                echo "Automaking Symbolic WASM Tests" `pwd`
-                cd ./tests/wasm_sym
-                ./generate_symbolic_tests.sh
-                touch .wasm_sym_done
-            fi
-            cd $DIR
-        }
-
-        install_truffle(){
-            npm install -g truffle
-        }
-
-        run_truffle_tests(){
-            mkdir truffle_tests
-            cd truffle_tests
-            truffle unbox metacoin
-            coverage run -m manticore . --contract MetaCoin --workspace output
-            # Truffle smoke test. We test if manticore is able to generate states
-            # from a truffle project. 
-            if [ "$(ls output/*tx -l | wc -l)" != "34" ]; then
-                echo "Truffle test failed" `ls output/*tx -l | wc -l` "!= 34"
-                return 1
-            fi
-            echo "Truffle test succeded"
-            coverage xml
-            cd ..
-            cp truffle_tests/coverage.xml .
-            return 0
-        }
-
-        run_tests_from_dir() {
-            DIR=$1
-            echo "Running only the tests from 'tests/$DIR' directory"
-            pytest --durations=100 --cov=manticore -n auto "tests/$DIR"
-            coverage xml
-        }
-
-        run_examples() {
-            pushd examples/linux
-            make
-            for example in $(make list); do
-                ./$example < /dev/zero > /dev/null
-            done
-            echo Built and ran Linux examples
-            popd
+        cp scripts/run_tests.sh .
+        ./run_tests.sh
+    - name: Coveralls Parallel
+      run: |
+        coveralls
+      env:
+        COVERALLS_PARALLEL: true
+        COVERALLS_REPO_TOKEN: ${{ secrets.COVERALLS_REPO_TOKEN }}
+  # Send notification when all tests have finished to combine coverage results
+  coverage-finish:
+    needs: tests
+    runs-on: ubuntu-latest
+    steps:
+    - name: Coveralls Finished
+      uses: coverallsapp/github-action@v1.1.1
+      with:
+        github-token: ${{ secrets.GITHUB_TOKEN }}
+        parallel-finished: true
+  upload:
+    runs-on: ubuntu-latest
+    if: github.event_name == 'schedule'
+    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 --dev_release sdist bdist_wheel
+    - name: Upload to PyPI
+      uses: pypa/gh-action-pypi-publish@v1.2.2
+      with:
+        password: ${{ secrets.PYPI_UPLOAD }}
 
-            pushd examples/script
-            launch_examples
-            RESULT=$?
-            echo Ran example scripts
-            coverage xml
-            popd
-            cp examples/script/coverage.xml .
-            return $RESULT
-        }
 
-        # Test type
-        case $TEST_TYPE in
-            ethereum_vm)
-                make_vmtests
-                run_tests_from_dir $TEST_TYPE
-                ;;
-            ethereum_truffle)
-                echo "Running truffle test"
-                install_truffle
-                run_truffle_tests
-                ;;
-            wasm)
-                make_wasm_tests
-                run_tests_from_dir $TEST_TYPE
-                ;;
-            wasm_sym)
-                make_wasm_sym_tests ;&  # Fallthrough
-            native)                 ;&  # Fallthrough
-            ethereum)               ;&  # Fallthrough
-            ethereum_bench)         ;&  # Fallthrough
-            other)
-                run_tests_from_dir $TEST_TYPE
-                ;;
-            examples)
-                run_examples
-                ;;
-            *)
-                echo "Unknown TEST_TYPE: '$TEST_TYPE'"
-                exit 3;
-                ;;
-        esac
-    - name: Coverage Upload
-      uses: codecov/codecov-action@v1
-      with:
-        token: ${{ secrets.CODECOV_TOKEN }}
-        file: ./coverage.xml
-        yml: ./codecov.yml
-# Disabled this line because Codecov has been extra flaky lately, and having to re-run the entire
-# test suite until every coverage upload step succeeds is more of a hassle than it's worth. 
-#        fail_ci_if_error: true

.github/workflows/osx.yml

@@ -0,0 +1,45 @@
+name: MacOS Tests
+
+on:
+  schedule:
+    # Run every day at 11 PM.
+    - cron:  '0 23 * * *'
+
+jobs:
+  tests:
+    runs-on: macos-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        type: ["ethereum_truffle", "ethereum_bench", "ethereum", "ethereum_vm", "wasm", "wasm_sym", "other"]
+    steps:
+    - uses: actions/checkout@v2
+    - 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: |
+        EXTRAS="dev-noks"
+        pip install -e .[$EXTRAS]
+    - 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
+    - name: Run Tests
+      env:
+        TEST_TYPE: ${{ matrix.type }}
+      run: |
+        cp scripts/run_tests.sh .
+        ./run_tests.sh

CHANGELOG.md

@@ -1,8 +1,59 @@
 # Change Log
 
-## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.3...HEAD)
+## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.4...HEAD)
 
-## 0.3.3 - 2020-01
+## 0.3.4 - 2020-06-26
+
+Thanks to our external contributors!
+ - [jimpo](https://github.com/trailofbits/manticore/commits?author=jimpo)
+ - [langston-barrett](https://github.com/trailofbits/manticore/commits?author=langston-barrett)
+
+### Ethereum
+* Support and test against EVM Istanbul [#1676](https://github.com/trailofbits/manticore/pull/1676)
+* **[Added API]** Added a `manticore-verifier` script for checking properties of smart contracts [#1717](https://github.com/trailofbits/manticore/pull/1717)
+* Fixed RETURNDATASIZE [#1612](https://github.com/trailofbits/manticore/pull/1612)
+* Added strategies for symbolic SHA3 replacement [#1609](https://github.com/trailofbits/manticore/pull/1609)
+* Fixed GAS instruction [#1633](https://github.com/trailofbits/manticore/pull/1633)
+* Improved balance-related exploration [#1615](https://github.com/trailofbits/manticore/pull/1615)
+* Add `__format__` to EVM accounts [#1613](https://github.com/trailofbits/manticore/pull/1613)
+* Discard basic blocks that unavoidably REVERT [#1630](https://github.com/trailofbits/manticore/pull/1630)
+* Extract printable bytes from return data [#1671](https://github.com/trailofbits/manticore/pull/1671)
+* Support CHAINID, EXTCODEHASH, and SELFBALANCE instructions [#1644](https://github.com/trailofbits/manticore/pull/1644)
+* **[Changed API]** Renamed several arguments in EVM API, including `gaslimit` --> `gas` [#1652](https://github.com/trailofbits/manticore/pull/1652)
+* Explore states that self-destruct [#1699](https://github.com/trailofbits/manticore/pull/1699)
+* Lazy solving for the Ethereum leak detector [#1727](https://github.com/trailofbits/manticore/pull/1727)
+
+### Native
+* Support for ARM modified-immediate encodings [#1638](https://github.com/trailofbits/manticore/pull/1638)
+* Support for `/proc/self/maps` [#1639](https://github.com/trailofbits/manticore/pull/1639)
+* Support for `llseek` [#1640](https://github.com/trailofbits/manticore/pull/1640)
+* Support for `arm_fadvise64_64` [#1648](https://github.com/trailofbits/manticore/pull/1648)
+* Allow symbolic sockets in `accept` [#1618](https://github.com/trailofbits/manticore/pull/1618)
+* Fixes to `open` [#1657](https://github.com/trailofbits/manticore/pull/1657)
+* Overhauled filesystem emulation [#1673](https://github.com/trailofbits/manticore/pull/1673)
+* Fixed system call argument concretization [#1697](https://github.com/trailofbits/manticore/pull/1697)
+* **[Added API]** Add a symbolic model for `strcpy` [#1681](https://github.com/trailofbits/manticore/pull/1681)
+
+### WASM
+* Delay branch condition concretization for better coverage [#1641](https://github.com/trailofbits/manticore/pull/1641)
+
+### Other
+* **[Added API]** Added a snapshot system [#1710](https://github.com/trailofbits/manticore/pull/1710)
+* Transparent compression for state files [#1624](https://github.com/trailofbits/manticore/pull/1624)
+* Unify around singleton interface for solver [#1649](https://github.com/trailofbits/manticore/pull/1649)
+* Use `__slots__` to reduce memory usage in expression system [#1635](https://github.com/trailofbits/manticore/pull/1635)
+* **[Removed API]** Removed `policy` argument from ManticoreBase, added `outputspace_url` to optionally separate working files from output files [#1651](https://github.com/trailofbits/manticore/pull/1651)
+* Disable broken `get_related` logic [#1674](https://github.com/trailofbits/manticore/pull/1674)
+* Disable flaky Z3 tactics [#1691](https://github.com/trailofbits/manticore/pull/1691)
+* Remove Keystone engine from dependencies [#1684](https://github.com/trailofbits/manticore/pull/1684)
+* Improved error messages [#1632](https://github.com/trailofbits/manticore/pull/1632), [#1704](https://github.com/trailofbits/manticore/pull/1704)
+* Made ConstraintSets hashable [#1703](https://github.com/trailofbits/manticore/pull/1703)
+* Added system to dynamically enable/disable plugins [#1696](https://github.com/trailofbits/manticore/pull/1696) [#1708](https://github.com/trailofbits/manticore/pull/1708)
+* Re-establish support for Yices and CVC4 [#1714](https://github.com/trailofbits/manticore/pull/1714)
+* Improved constant folding and constraint set slicing [#1706](https://github.com/trailofbits/manticore/pull/1706)
+
+
+## 0.3.3 - 2020-01-30
 
 Thanks to our external contributors!