Slottify expressions

.github/workflows/ci.yml

@@ -16,9 +16,9 @@ jobs:
     steps:
     - uses: actions/checkout@v2
     - name: Set up Python 3.6
-      uses: actions/setup-python@v1
+      uses: actions/setup-python@v2
       with:
-        python-version: 3.6
+        python-version: '3.6'
     - name: Lint
       if: github.event_name == 'pull_request'
       env:
@@ -41,14 +41,15 @@ jobs:
   tests:
     runs-on: ubuntu-latest
     strategy:
+      fail-fast: false
       matrix:
-        type: ["ethereum_truffle", "ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "wasm", "wasm_sym", "other"]
+        type: ["ethereum_truffle", "ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "other", "wasm", "wasm_sym"]
     steps:
     - uses: actions/checkout@v1
     - name: Set up Python 3.6
-      uses: actions/setup-python@v1
+      uses: actions/setup-python@v2
       with:
-        python-version: 3.6
+        python-version: '3.6'
     - name: Install NPM
       uses: actions/setup-node@v1
       with:
@@ -98,9 +99,9 @@ jobs:
     steps:
     - uses: actions/checkout@v2
     - name: Set up Python 3.6
-      uses: actions/setup-python@v1
+      uses: actions/setup-python@v2
       with:
-        python-version: 3.6
+        python-version: '3.6'
     - name: Build Dist
       run: |
         python3 -m pip install wheel

.gitignore

@@ -45,6 +45,7 @@ nosetests.xml
 coverage.xml
 *,cover
 .hypothesis/
+mcore_*
 
 # Translations
 *.mo

CHANGELOG.md

@@ -440,7 +440,7 @@ Thanks to our external contributors!
 - Ethereum: Support for Solidity `bytesM` and `bytes` types
 - Ethereum: Beta API for preconstraining inputs (`ManticoreEVM.constrain`)
 - Improved performance for smtlib module
-- Ability to transparently operate on bytearray and symbolic buffer (ArrayProxy) types (e.g: concatenate, slice)
+- Ability to transparently operate on bytearray and symbolic buffer (MutableArray) types (e.g: concatenate, slice)
 
 ### Changed
 

examples/evm/asm_to_smtlib.py

@@ -7,7 +7,9 @@
 from manticore.utils import log
 
 # log.set_verbosity(9)
-config.out_of_gas = 1
+# FIXME: What's the equivalent?
+consts = config.get_group("evm")
+consts["oog"] = "complete"
 
 
 def printi(instruction):
@@ -42,11 +44,11 @@ def printi(instruction):
 )
 
 
-data = constraints.new_array(index_bits=256, name="array")
+data = constraints.new_array(index_size=256, name="array")
 
 
-class callbacks:
-    initial_stack = []
+class Callbacks:
+    initial_stack: List[BitVec] = []
 
     def will_execute_instruction(self, pc, instr):
         for i in range(len(evm.stack), instr.pops):
@@ -57,8 +59,8 @@ def will_execute_instruction(self, pc, instr):
 
 class DummyWorld:
     def __init__(self, constraints):
-        self.balances = constraints.new_array(index_bits=256, value_bits=256, name="balances")
-        self.storage = constraints.new_array(index_bits=256, value_bits=256, name="storage")
+        self.balances = constraints.new_array(index_size=256, value_size=256, name="balances")
+        self.storage = constraints.new_array(index_size=256, value_size=256, name="storage")
         self.origin = constraints.new_bitvec(256, name="origin")
         self.price = constraints.new_bitvec(256, name="price")
         self.timestamp = constraints.new_bitvec(256, name="timestamp")
@@ -112,10 +114,10 @@ def send_funds(self, address, recipient, value):
 value = constraints.new_bitvec(256, name="value")
 
 world = DummyWorld(constraints)
-callbacks = callbacks()
+callbacks = Callbacks()
 
 # evm = world.current_vm
-evm = EVM(constraints, 0x41424344454647484950, data, caller, value, code, world=world, gas=1000000)
+evm = EVM(0x41424344454647484950, data, caller, value, code, world=world, gas=1000000)
 evm.subscribe("will_execute_instruction", callbacks.will_execute_instruction)
 
 print("CODE:")
@@ -138,5 +140,5 @@ def send_funds(self, address, recipient, value):
 print(constraints)
 
 print(
-    f"PC: {translate_to_smtlib(evm.pc)} {solver.get_all_values(constraints, evm.pc, maxcnt=3, silent=True)}"
+    f"PC: {translate_to_smtlib(evm.pc)} {SMTLIBSolver.get_all_values(constraints, evm.pc, maxcnt=3, silent=True)}"
 )

examples/evm/coverage.py

@@ -8,9 +8,8 @@
 
 user_account = m.create_account(balance=1000)
 
-bytecode = m.compile(source_code)
 # Initialize contract
-contract_account = m.create_contract(owner=user_account, balance=0, init=bytecode)
+contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0)
 
 m.transaction(
     caller=user_account,

examples/evm/mappingchallenge.py

@@ -30,22 +30,24 @@ class StopAtDepth(Detector):
     """ This just aborts explorations that are too deep """
 
     def will_run_callback(self, *args):
-        with self.manticore.locked_context("seen_rep", dict) as reps:
-            reps.clear()
+        if self.manticore:
+            with self.manticore.locked_context("seen_rep", dict) as reps:
+                reps.clear()
 
     def will_decode_instruction_callback(self, state, pc):
         world = state.platform
-        with self.manticore.locked_context("seen_rep", dict) as reps:
-            item = (
-                world.current_transaction.sort == "CREATE",
-                world.current_transaction.address,
-                pc,
-            )
-            if not item in reps:
-                reps[item] = 0
-            reps[item] += 1
-            if reps[item] > 2:
-                state.abandon()
+        if self.manticore:
+            with self.manticore.locked_context("seen_rep", dict) as reps:
+                item = (
+                    world.current_transaction.sort == "CREATE",
+                    world.current_transaction.address,
+                    pc,
+                )
+                if not item in reps:
+                    reps[item] = 0
+                reps[item] += 1
+                if reps[item] > 2:
+                    state.abandon()
 
 
 m.register_plugin(StopAtDepth())

examples/evm/minimal-json.py

@@ -1047,7 +1047,9 @@
 user_account = m.create_account(balance=1000, name="user_account")
 print("[+] Creating a user account", user_account.name_)
 
-contract_account = m.json_create_contract(truffle_json, owner=user_account, name="contract_account")
+contract_account = m.solidity_create_contract(
+    truffle_json, owner=user_account, name="contract_account"
+)
 print("[+] Creating a contract account", contract_account.name_)
 contract_account.sendCoin(1, 1)
 

examples/evm/minimal.py

@@ -24,13 +24,14 @@
     } 
 }
 """
-user_account = m.create_account(balance=m.make_symbolic_value(), name="user_account")
+
+user_account = m.create_account(balance=10 ** 10, name="user_account")
 print("[+] Creating a user account", user_account.name_)
 
 contract_account = m.solidity_create_contract(
     source_code, owner=user_account, name="contract_account"
 )
-print("[+] Creating a contract account", contract_account.name_)
+print(f"[+] Creating a contract account {contract_account}")
 contract_account.named_func(1)
 
 print("[+] Now the symbolic values")

examples/evm/use_def.py

@@ -41,6 +41,8 @@
 class EVMUseDef(Plugin):
     def did_evm_write_storage_callback(self, state, address, offset, value):
         m = self.manticore
+        if not m:
+            return
         world = state.platform
         tx = world.all_transactions[-1]
         md = m.get_metadata(tx.address)
@@ -55,6 +57,8 @@ def did_evm_write_storage_callback(self, state, address, offset, value):
 
     def did_evm_read_storage_callback(self, state, address, offset, value):
         m = self.manticore
+        if not m:
+            return
         world = state.platform
         tx = world.all_transactions[-1]
         md = m.get_metadata(tx.address)

examples/linux/binaries/concrete_solve.py

@@ -1,16 +1,14 @@
-from manticore import Manticore
+from manticore.native import Manticore
 
 
 def fixme():
     raise Exception("Fill in the blanks!")
 
 
 # Let's initialize the manticore control object
-m = Manticore("multiple-styles")
-
 # First, let's give it some fake data for the input. Anything the same size as
 # the real flag should work fine!
-m.concrete_data = "infiltrate miami!"
+m = Manticore("multiple-styles", concrete_start="infiltrate miami!")
 
 # Now we're going to want to execute a few different hooks and share data, so
 # let's use the m.context dict to keep our solution in

examples/linux/binaries/symbolic_solve.py

@@ -1,4 +1,4 @@
-from manticore import Manticore
+from manticore.native import Manticore
 
 
 def fixme():

examples/script/concolic.py

@@ -16,6 +16,7 @@
 import queue
 import struct
 import itertools
+from typing import Any
 
 from manticore import set_verbosity
 from manticore.native import Manticore
@@ -234,7 +235,7 @@ def constraints_are_sat(cons):
 
 
 def get_new_constrs_for_queue(oldcons, newcons):
-    ret = []
+    ret: List[Any] = []
 
     # i'm pretty sure its correct to assume newcons is a superset of oldcons
 
@@ -299,7 +300,7 @@ def concrete_input_to_constraints(ci, prev=None):
 
 def main():
 
-    q = queue.Queue()
+    q: queue.Queue = queue.Queue()
 
     # todo randomly generated concrete start
     stdin = ints2inp(0, 5, 0)

examples/script/introduce_symbolic_bytes.py

@@ -1,6 +1,7 @@
 #!/usr/bin/env python
 
 import sys
+import capstone
 
 from manticore import issymbolic
 from manticore.native import Manticore
@@ -64,7 +65,6 @@ def introduce_sym(state):
         state.cpu.write_int(state.cpu.RBP - 0xC, val, 32)
 
     def has_tainted_operands(operands, taint_id):
-        # type: (list[manticore.core.cpu.abstractcpu.Operand], object) -> bool
         for operand in operands:
             op = operand.read()
             if issymbolic(op) and taint_id in op.taint:

manticore/__main__.py

@@ -26,6 +26,8 @@
 
 
 def main() -> None:
+    import pdb
+
     """
     Dispatches execution into one of Manticore's engines: evm or native.
     """