-
Notifications
You must be signed in to change notification settings - Fork 474
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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) ...
- Loading branch information
Showing
79 changed files
with
18,508 additions
and
15,966 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -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/[email protected].1 | ||
| uses: coverallsapp/[email protected].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: | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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/[email protected] | ||
| with: | ||
| password: ${{ secrets.PYPI_UPLOAD }} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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)) |
Oops, something went wrong.