WIP load truffle json artifacts

examples/evm/minimal-json.py

@@ -0,0 +1,298 @@
+from manticore.ethereum import ManticoreEVM
+
+################ Script #######################
+
+m = ManticoreEVM()
+
+#And now make the contract account to analyze
+truffle_json = '''
+{
+  "abi": [
+    {
+      "constant": false,
+      "inputs": [],
+      "name": "renounceOwnership",
+      "outputs": [],
+      "payable": false,
+      "stateMutability": "nonpayable",
+      "type": "function",
+      "signature": "0x715018a6"
+    },
+    {
+      "constant": true,
+      "inputs": [],
+      "name": "owner",
+      "outputs": [
+        {
+          "name": "",
+          "type": "address"
+        }
+      ],
+      "payable": false,
+      "stateMutability": "view",
+      "type": "function",
+      "signature": "0x8da5cb5b"
+    },
+    {
+      "constant": true,
+      "inputs": [],
+      "name": "isOwner",
+      "outputs": [
+        {
+          "name": "",
+          "type": "bool"
+        }
+      ],
+      "payable": false,
+      "stateMutability": "view",
+      "type": "function",
+      "signature": "0x8f32d59b"
+    },
+    {
+      "constant": false,
+      "inputs": [
+        {
+          "name": "newOwner",
+          "type": "address"
+        }
+      ],
+      "name": "transferOwnership",
+      "outputs": [],
+      "payable": false,
+      "stateMutability": "nonpayable",
+      "type": "function",
+      "signature": "0xf2fde38b"
+    },
+    {
+      "anonymous": false,
+      "inputs": [
+        {
+          "indexed": true,
+          "name": "_agreementId",
+          "type": "bytes32"
+        },
+        {
+          "indexed": true,
+          "name": "_did",
+          "type": "bytes32"
+        },
+        {
+          "indexed": true,
+          "name": "_sender",
+          "type": "address"
+        },
+        {
+          "indexed": false,
+          "name": "_didOwner",
+          "type": "address"
+        },
+        {
+          "indexed": false,
+          "name": "_templateId",
+          "type": "address"
+        }
+      ],
+      "name": "AgreementCreated",
+      "type": "event"
+    },
+    {
+      "anonymous": false,
+      "inputs": [
+        {
+          "indexed": true,
+          "name": "previousOwner",
+          "type": "address"
+        },
+        {
+          "indexed": true,
+          "name": "newOwner",
+          "type": "address"
+        }
+      ],
+      "name": "OwnershipTransferred",
+      "type": "event"
+    },
+    {
+      "constant": false,
+      "inputs": [
+        {
+          "name": "_owner",
+          "type": "address"
+        },
+        {
+          "name": "_conditionStoreManagerAddress",
+          "type": "address"
+        },
+        {
+          "name": "_templateStoreManagerAddress",
+          "type": "address"
+        }
+      ],
+      "name": "initialize",
+      "outputs": [],
+      "payable": false,
+      "stateMutability": "nonpayable",
+      "type": "function",
+      "signature": "0xc0c53b8b"
+    },
+    {
+      "constant": false,
+      "inputs": [
+        {
+          "name": "sender",
+          "type": "address"
+        }
+      ],
+      "name": "initialize",
+      "outputs": [],
+      "payable": false,
+      "stateMutability": "nonpayable",
+      "type": "function",
+      "signature": "0xc4d66de8"
+    },
+    {
+      "constant": false,
+      "inputs": [
+        {
+          "name": "_id",
+          "type": "bytes32"
+        },
+        {
+          "name": "_did",
+          "type": "bytes32"
+        },
+        {
+          "name": "_didOwner",
+          "type": "address"
+        },
+        {
+          "name": "_conditionTypes",
+          "type": "address[]"
+        },
+        {
+          "name": "_conditionIds",
+          "type": "bytes32[]"
+        },
+        {
+          "name": "_timeLocks",
+          "type": "uint256[]"
+        },
+        {
+          "name": "_timeOuts",
+          "type": "uint256[]"
+        }
+      ],
+      "name": "createAgreement",
+      "outputs": [
+        {
+          "name": "size",
+          "type": "uint256"
+        }
+      ],
+      "payable": false,
+      "stateMutability": "nonpayable",
+      "type": "function",
+      "signature": "0x26903704"
+    },
+    {
+      "constant": true,
+      "inputs": [
+        {
+          "name": "_id",
+          "type": "bytes32"
+        }
+      ],
+      "name": "getAgreement",
+      "outputs": [
+        {
+          "name": "did",
+          "type": "bytes32"
+        },
+        {
+          "name": "didOwner",
+          "type": "address"
+        },
+        {
+          "name": "templateId",
+          "type": "address"
+        },
+        {
+          "name": "conditionIds",
+          "type": "bytes32[]"
+        },
+        {
+          "name": "lastUpdatedBy",
+          "type": "address"
+        },
+        {
+          "name": "blockNumberUpdated",
+          "type": "uint256"
+        }
+      ],
+      "payable": false,
+      "stateMutability": "view",
+      "type": "function",
+      "signature": "0xf42eb765"
+    },
+    {
+      "constant": true,
+      "inputs": [
+        {
+          "name": "_id",
+          "type": "bytes32"
+        }
+      ],
+      "name": "getAgreementDidOwner",
+      "outputs": [
+        {
+          "name": "didOwner",
+          "type": "address"
+        }
+      ],
+      "payable": false,
+      "stateMutability": "view",
+      "type": "function",
+      "signature": "0xe609131c"
+    },
+    {
+      "constant": true,
+      "inputs": [],
+      "name": "getAgreementListSize",
+      "outputs": [
+        {
+          "name": "size",
+          "type": "uint256"
+        }
+      ],
+      "payable": false,
+      "stateMutability": "view",
+      "type": "function",
+      "signature": "0x8a9013cb"
+    }
+  ],
+  "bytecode": "0x608060405234801561001057600080fd5b50610e7e806100206000396000f3fe608060405234801561001057600080fd5b50600436106100bb576000357c010000000000000000000000000000000000000000000000000000000090048063c0c53b8b11610083578063c0c53b8b1461036f578063c4d66de8146103a7578063e609131c146103cd578063f2fde38b146103ea578063f42eb76514610410576100bb565b806326903704146100c0578063715018a61461031d5780638a9013cb146103275780638da5cb5b1461032f5780638f32d59b14610353575b600080fd5b61030b600480360360e08110156100d657600080fd5b813591602081013591600160a060020a03604083013516919081019060808101606082013564010000000081111561010d57600080fd5b82018360208201111561011f57600080fd5b8035906020019184602083028401116401000000008311171561014157600080fd5b919080806020026020016040519081016040528093929190818152602001838360200280828437600092019190915250929594936020810193503591505064010000000081111561019157600080fd5b8201836020820111156101a357600080fd5b803590602001918460208302840111640100000000831117156101c557600080fd5b919080806020026020016040519081016040528093929190818152602001838360200280828437600092019190915250929594936020810193503591505064010000000081111561021557600080fd5b82018360208201111561022757600080fd5b8035906020019184602083028401116401000000008311171561024957600080fd5b919080806020026020016040519081016040528093929190818152602001838360200280828437600092019190915250929594936020810193503591505064010000000081111561029957600080fd5b8201836020820111156102ab57600080fd5b803590602001918460208302840111640100000000831117156102cd57600080fd5b9190808060200260200160405190810160405280939291908181526020018383602002808284376000920191909152509295506104da945050505050565b60408051918252519081900360200190f35b6103256107dc565b005b61030b610846565b61033761084d565b60408051600160a060020a039092168252519081900360200190f35b61035b61085c565b604080519115158252519081900360200190f35b6103256004803603606081101561038557600080fd5b50600160a060020a03813581169160208101358216916040909101351661086d565b610325600480360360208110156103bd57600080fd5b5035600160a060020a03166109df565b610337600480360360208110156103e357600080fd5b5035610ade565b6103256004803603602081101561040057600080fd5b5035600160a060020a0316610afc565b61042d6004803603602081101561042657600080fd5b5035610b1b565b6040518087815260200186600160a060020a0316600160a060020a0316815260200185600160a060020a0316600160a060020a031681526020018060200184600160a060020a0316600160a060020a03168152602001838152602001828103825285818151815260200191508051906020019060200280838360005b838110156104c15781810151838201526020016104a9565b5050505090500197505050505050505060405180910390f35b606754604080517fb727a2550000000000000000000000000000000000000000000000000000000081523360048201529051600092600160a060020a03169163b727a255916024808301926020929190829003018186803b15801561053e57600080fd5b505afa158015610552573d6000803e3d6000fd5b505050506040513d602081101561056857600080fd5b505115156001146105c3576040805160e560020a62461bcd02815260206004820152601560248201527f54656d706c617465206e6f7420417070726f7665640000000000000000000000604482015290519081900360640190fd5b845184511480156105d5575084518351145b80156105e2575084518251145b1515610638576040805160e560020a62461bcd02815260206004820152601b60248201527f417267756d656e747320686176652077726f6e67206c656e6774680000000000604482015290519081900360640190fd5b60005b8551811015610766576066548551600160a060020a039091169063fe3ae90f9087908490811061066757fe5b90602001906020020151888481518110151561067f57fe5b90602001906020020151878581518110151561069757fe5b9060200190602002015187868151811015156106af57fe5b906020019060200201516040518563ffffffff167c01000000000000000000000000000000000000000000000000000000000281526004018085815260200184600160a060020a0316600160a060020a03168152602001838152602001828152602001945050505050602060405180830381600087803b15801561073257600080fd5b505af1158015610746573d6000803e3d6000fd5b505050506040513d602081101561075c57600080fd5b505060010161063b565b5061077c6068898989338963ffffffff610bd316565b5060408051600160a060020a03881681523360208201819052825190928a928c927fad72a6a56b990b1fe61d5058e5af5169720a65e05fdcf8119a803d010d08c6a8929181900390910190a46107d0610846565b98975050505050505050565b6107e461085c565b15156107ef57600080fd5b603354604051600091600160a060020a0316907f8be0079c531659141344cd1fd0a4f28419497f9722a3daafe3b4186f6b6457e0908390a36033805473ffffffffffffffffffffffffffffffffffffffff19169055565b6069545b90565b603354600160a060020a031690565b603354600160a060020a0316331490565b600054610100900460ff16806108865750610886610d3b565b80610894575060005460ff16155b15156108d45760405160e560020a62461bcd02815260040180806020018281038252602e815260200180610e25602e913960400191505060405180910390fd5b60008054600161010061ff00198316811760ff1916919091179092550460ff16600160a060020a038316158015906109145750600160a060020a03821615155b80156109285750600160a060020a03841615155b151561097e576040805160e560020a62461bcd02815260206004820152600f60248201527f496e76616c696420616464726573730000000000000000000000000000000000604482015290519081900360640190fd5b610987846109df565b60668054600160a060020a0394851673ffffffffffffffffffffffffffffffffffffffff19918216179091556067805493909416921691909117909155600080549115156101000261ff001990921691909117905550565b600054610100900460ff16806109f857506109f8610d3b565b80610a06575060005460ff16155b1515610a465760405160e560020a62461bcd02815260040180806020018281038252602e815260200180610e25602e913960400191505060405180910390fd5b60008054600161010061ff00198316811760ff19169190911783556033805473ffffffffffffffffffffffffffffffffffffffff1916600160a060020a0386811691909117918290556040519290930460ff1693921691907f8be0079c531659141344cd1fd0a4f28419497f9722a3daafe3b4186f6b6457e0908290a3600080549115156101000261ff001990921691909117905550565b600090815260686020526040902060010154600160a060020a031690565b610b0461085c565b1515610b0f57600080fd5b610b1881610d41565b50565b6000818152606860209081526040808320805460018201546002830154600390930180548551818802810188019096528086529296600160a060020a03928316969290941694606094938493919291830182828015610b9957602002820191906000526020600020905b815481526020019060010190808311610b85575b5050506000998a5250506068602052604090972060048101546005909101549698959794969495600160a060020a03909116949350915050565b60008581526020879052604081206005015415610c3a576040805160e560020a62461bcd02815260206004820152601160248201527f496420616c726561647920657869737473000000000000000000000000000000604482015290519081900360640190fd5b6040805160c081018252868152600160a060020a038087166020808401918252878316848601908152606085018881523360808701524360a087015260008d81528e84529690962085518155925160018401805491861673ffffffffffffffffffffffffffffffffffffffff1992831617905590516002840180549190951691161790925592518051929392610cd69260038501920190610dbf565b50608082015160048201805473ffffffffffffffffffffffffffffffffffffffff1916600160a060020a0390921691909117905560a0909101516005909101555050505060019283018054938401815560008181526020902090930191909155505490565b303b1590565b600160a060020a0381161515610d5657600080fd5b603354604051600160a060020a038084169216907f8be0079c531659141344cd1fd0a4f28419497f9722a3daafe3b4186f6b6457e090600090a36033805473ffffffffffffffffffffffffffffffffffffffff1916600160a060020a0392909216919091179055565b828054828255906000526020600020908101928215610dfa579160200282015b82811115610dfa578251825591602001919060010190610ddf565b50610e06929150610e0a565b5090565b61084a91905b80821115610e065760008155600101610e1056fe436f6e747261637420696e7374616e63652068617320616c7265616479206265656e20696e697469616c697a6564a165627a7a7230582065d10ffdbe26793f1178782e23b374f76276d44bb94d2bdb01963dcb73c964d30029",
+  "address": "0xd462a1b14cbd7a6c2cbea0958d2f755a6f0901a6",
+  "version": "v0.7.0"
+}
+'''
+
+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')
+print("[+] Creating a contract account", contract_account.name_)
+contract_account.named_func(1)
+
+print("[+] Now the symbolic values")
+symbolic_data = m.make_symbolic_buffer(320) 
+symbolic_value = m.make_symbolic_value(name="VALUE")
+symbolic_address = m.make_symbolic_value(name="ADDRESS")
+symbolic_caller = m.make_symbolic_value(name="CALLER")
+m.transaction(caller=symbolic_caller,
+                address=symbolic_address,
+                data=symbolic_data,
+                value=symbolic_value )
+
+#Let seth know we are not sending more transactions 
+m.finalize()
+print(f"[+] Look for results in {m.workspace}")

examples/evm/minimal.py

@@ -7,20 +7,19 @@
 #And now make the contract account to analyze
 # cat  | solc --bin 
 source_code = '''
-pragma solidity ^0.4.13;
 contract NoDistpatcher {
     event Log(string);
 
-    function  named_func(uint x) returns (uint) {
+    function  named_func(uint x) public returns (uint) {
     return 5 + x;
     }
 
-    function() payable {
+    function() external payable {
         if (msg.data[0] == 'A') {
-            Log("Got an A");
+            emit Log("Got an A");
         }
         else{
-            Log("Got something else");
+            emit Log("Got something else");
         }
     } 
 }

manticore/ethereum/manticore.py

@@ -572,6 +572,57 @@ def make_symbolic_arguments(self, types):
         # FIXME this is more naive than reasonable.
         return ABI.deserialize(types, self.make_symbolic_buffer(32, name='INITARGS', avoid_collisions=True))
 
+
+    def json_create_contract(self, jfile, owner=None, name=None, contract_name=None, balance=0,
+                                 address=None, args=(), gas=None): 
+        """ Creates a solidity contract based on a truffle json artifact.
+
+            :param str jfile: truffle json artifact
+            :param owner: owner account (will be default caller in any transactions)
+            :type owner: int or EVMAccount
+            :param contract_name: Name of the contract to analyze (optional if there is a single one in the source code)
+            :type contract_name: str
+            :param balance: balance to be transferred on creation
+            :type balance: int or BitVecVariable
+            :param address: the address for the new contract (optional)
+            :type address: int or EVMAccount
+            :param tuple args: constructor arguments
+            :param solc_bin: path to solc binary
+            :type solc_bin: str
+            :param solc_remaps: solc import remaps
+            :type solc_remaps: list of str
+            :param working_dir: working directory for solc compilation (defaults to current)
+            :type working_dir: str
+            :param gas: gas budget for each contract creation needed (may be more than one if several related contracts defined in the solidity source)
+            :type gas: int
+            :rtype: EVMAccount
+        """
+        truffle = json.loads(jfile)
+        #(name, source_code, init_bytecode, runtime_bytecode, srcmap, srcmap_runtime, hashes, abi, warnings)
+        hashes = {}
+        for item in truffle['abi']:
+            type = item['type']
+            if type in ('function'):
+                signature = SolidityMetadata.function_signature_for_name_and_inputs(item['name'], item['inputs'])
+                hashes[signature] = sha3.keccak_256(signature.encode()).hexdigest()[:8]
+                assert item['signature'] ==  '0x'+hashes[signature]
+
+        md = SolidityMetadata('', '' , binascii.unhexlify(truffle['bytecode'][2:]), '', {}, {}, hashes, truffle['abi'], '')
+        contract_account = self.create_contract(owner=owner, init=md._init_bytecode)
+
+        if contract_account is None:
+            raise EthereumError("Failed to build contract %s" % contract_name_i)
+        self.metadata[int(contract_account)] = md
+
+        contract_account = self.create_contract(owner=owner, init=md._init_bytecode)
+
+        if contract_account is None:
+            raise EthereumError("Failed to build contract %s" % contract_name_i)
+        self.metadata[int(contract_account)] = md
+        if not self.count_running_states() or len(self.get_code(contract_account)) == 0:
+            return None
+        return contract_account
+
     def solidity_create_contract(self, source_code, owner, name=None, contract_name=None, libraries=None,
                                  balance=0, address=None, args=(), solc_bin=None, solc_remaps=[],
                                  working_dir=None, gas=None):

manticore/ethereum/solidity.py

@@ -88,31 +88,32 @@ def __build_source_map(self, bytecode, srcmap):
         # https://solidity.readthedocs.io/en/develop/miscellaneous.html#source-mappings
         new_srcmap = {}
         bytecode = self._without_metadata(bytecode)
-
-        asm_offset = 0
-        asm_pos = 0
-        md = dict(enumerate(srcmap[asm_pos].split(':')))
-        byte_offset = int(md.get(0, 0))  # is the byte-offset to the start of the range in the source file
-        source_len = int(md.get(1, 0))  # is the length of the source range in bytes
-        file_index = int(md.get(2, 0))  # is the source index over sourceList
-        jump_type = md.get(3, None)  # this can be either i, o or - signifying whether a jump instruction goes into a function, returns from a function or is a regular jump as part of e.g. a loop
-
-        pos_to_offset = {}
-        for i in EVMAsm.disassemble_all(bytecode):
-            pos_to_offset[asm_pos] = asm_offset
-            asm_pos += 1
-            asm_offset += i.size
-
-        for asm_pos, md in enumerate(srcmap):
-            if len(md):
-                d = {p: k for p, k in enumerate(md.split(':')) if k}
-
-                byte_offset = int(d.get(0, byte_offset))
-                source_len = int(d.get(1, source_len))
-                file_index = int(d.get(2, file_index))
-                jump_type = d.get(3, jump_type)
-
-            new_srcmap[pos_to_offset[asm_pos]] = (byte_offset, source_len, file_index, jump_type)
+        if self.source_code:
+
+            asm_offset = 0
+            asm_pos = 0
+            md = dict(enumerate(srcmap[asm_pos].split(':')))
+            byte_offset = int(md.get(0, 0))  # is the byte-offset to the start of the range in the source file
+            source_len = int(md.get(1, 0))  # is the length of the source range in bytes
+            file_index = int(md.get(2, 0))  # is the source index over sourceList
+            jump_type = md.get(3, None)  # this can be either i, o or - signifying whether a jump instruction goes into a function, returns from a function or is a regular jump as part of e.g. a loop
+
+            pos_to_offset = {}
+            for i in EVMAsm.disassemble_all(bytecode):
+                pos_to_offset[asm_pos] = asm_offset
+                asm_pos += 1
+                asm_offset += i.size
+
+            for asm_pos, md in enumerate(srcmap):
+                if len(md):
+                    d = {p: k for p, k in enumerate(md.split(':')) if k}
+
+                    byte_offset = int(d.get(0, byte_offset))
+                    source_len = int(d.get(1, source_len))
+                    file_index = int(d.get(2, file_index))
+                    jump_type = d.get(3, jump_type)
+
+                new_srcmap[pos_to_offset[asm_pos]] = (byte_offset, source_len, file_index, jump_type)
 
         return new_srcmap