Merge branch 'master' into chess

* master:
  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)

.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/[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:

.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 }}

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(