Manticore tutorial simple example incorrect #2583

bzhang42 · 2022-08-25T19:35:12Z

Summary of the problem

Running the simple example on the Tutorial does not result in the correct output. https://github.com/trailofbits/manticore/wiki/Tutorial:-Running-under-Manticore

Manticore version

0.3.7

Python version

3.7

OS / Environment

Ubuntu (WSL)

Dependencies

I am using solc version 0.8.16.

Step to reproduce the behavior

Create a file called simple_example.sol:

pragma solidity >=0.4.24;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

Then run manticore simple_example.sol.

Expected behavior

An output like the tutorial mentions, with multiple test cases:

...
... m.c.manticore:INFO: Generated testcase No. 0 - STOP
... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
... m.c.manticore:INFO: Generated testcase No. 4 - STOP
... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
...

Actual behavior

2022-08-25 15:31:37,907: [30234] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2022-08-25 15:31:37,907: [30234] m.main:INFO: Beginning analysis
2022-08-25 15:31:37,938: [30234] m.e.manticore:INFO: Starting symbolic create contract
2022-08-25 15:31:39,131: [30234] m.e.manticore:INFO: Starting symbolic transaction: 0
2022-08-25 15:31:39,674: [30234] m.e.manticore:INFO: 1 alive states, 1 terminated states
2022-08-25 15:31:39,731: [30234] m.e.manticore:INFO: Starting symbolic transaction: 1
2022-08-25 15:31:40,559: [30234] m.e.manticore:INFO: 1 alive states, 1 terminated states
2022-08-25 15:31:40,770: [30297] m.c.manticore:INFO: Generated testcase No. 0 - STOP(3 txs)
2022-08-25 15:31:40,775: [30297] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-25 15:31:42,111: [30234] m.c.manticore:INFO: Results in [redacted]
2022-08-25 15:31:42,112: [30234] m.c.manticore:INFO: Total time: 2.362511396408081

Any relevant logs

The user_00000000.tx file shows:

Transactions No. 0
Type: CREATE (0)
From: owner(0x10000) 
To: contract0(0xcb37f4304de8d1ca2df2474c6e3a00ab3e720462) 
Value: 0 (*)
Gas used: 230000 
Data: 0x6080604052348015600f57600080fd5b50609e8061001e6000396000f300608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff168063b3de648b146044575b600080fd5b6060600480360381019080803590602001909291905050506062565b005b6041811415606f57600080fd5b505600a165627a7a72305820daaf2e537785ac684496ebcb086d2401e4b1dac4f633868ca73d99560e0a953c0029 
Return_data: 0x608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff168063b3de648b146044575b600080fd5b6060600480360381019080803590602001909291905050506062565b005b6041811415606f57600080fd5b505600a165627a7a72305820daaf2e537785ac684496ebcb086d2401e4b1dac4f633868ca73d99560e0a953c0029  (*)
Function call:
Constructor() -> RETURN 


Transactions No. 1
Type: CALL (0)
From: attacker(0x20000) 
To: contract0(0xcb37f4304de8d1ca2df2474c6e3a00ab3e720462) 
Value: 1836912146 (*)
Gas used: 230000 
Data: 0xb3de648b00000000000000000000000000000000000000000000000000000000ff000041 (*)
Return_data: 0x () 

Function call:
f(4278190145) -> STOP (*)


Transactions No. 2
Type: CALL (0)
From: attacker(0x20000) 
To: contract0(0xcb37f4304de8d1ca2df2474c6e3a00ab3e720462) 
Value: 0 (*)
Gas used: 230000 
Data: 0xb3de648b00000000000000000000000000000000ff000000000000000000000000000041 (*)
Return_data: 0x () 

Function call:
f(338953138925153547590470800371487866945) -> STOP (*)




(*) Example solution given. Value is symbolic and may take other values

The text was updated successfully, but these errors were encountered:

Kaylee-Hsu · 2022-08-31T09:21:37Z

I think I am having similar problem.

manticore version : 0.3.7
python version : 3.7
OS : Ubuntu 16.04

Expected behavior
From source : https://asciinema.org/a/154012

[I] mark ubuntu /m/h/c/m/e/evm (master) ❯ manticore umd_example.sol                                                                                                      ❮ 07:26
2017-12-22 19:26:36,308: [108889] m.main:INFO: Beginning analysis                                                                                                               
2017-12-22 19:26:36,372: [108889] m.ethereum:INFO: Starting symbolic transaction: 1                                                                                             
2017-12-22 19:26:37,076: [108889] m.ethereum:INFO: Generated testcase No. 0 - REVERT                                                                                            
2017-12-22 19:26:38,781: [108889] m.ethereum:INFO: Generated testcase No. 1 - REVERT                                                                                            
2017-12-22 19:26:40,927: [108889] m.ethereum:INFO: Generated testcase No. 2 - REVERT                                                                                            
2017-12-22 19:26:43,761: [108889] m.ethereum:INFO: Generated testcase No. 3 - REVERT                                                                                            
2017-12-22 19:26:46,297: [108889] m.ethereum:INFO: Generated testcase No. 4 - THROW                                                                                             
2017-12-22 19:26:48,629: [108889] m.ethereum:INFO: Finished symbolic transaction: 1 | Code Coverage: 100% | Terminated States: 5 | Alive States: 4                              
2017-12-22 19:26:48,640: [108889] m.ethereum:INFO: Generated testcase No. 5 - STOP                                                                                              
2017-12-22 19:26:51,005: [108889] m.ethereum:INFO: Generated testcase No. 6 - STOP                                                                                              
2017-12-22 19:26:53,372: [108889] m.ethereum:INFO: Generated testcase No. 7 - STOP                                                                                              
2017-12-22 19:26:55,730: [108889] m.ethereum:INFO: Generated testcase No. 8 - STOP                                                                                              
2017-12-22 19:26:58,145: [108889] m.ethereum:INFO: Results in /mnt/hgfs/code/manticore/examples/evm/mcore_nOeEvF

Actual behavior

$ manticore umd_example.sol 
2022-08-31 17:05:45,984: [27903] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2022-08-31 17:05:45,985: [27903] m.main:INFO: Beginning analysis
2022-08-31 17:05:45,986: [27903] m.e.manticore:INFO: Starting symbolic create contract
2022-08-31 17:05:46,828: [27903] m.e.manticore:INFO: Starting symbolic transaction: 0
2022-08-31 17:06:16,999: [27903] m.e.manticore:INFO: 4 alive states, 2 terminated states
2022-08-31 17:06:17,353: [27903] m.e.manticore:INFO: Starting symbolic transaction: 1

2022-08-31 17:08:27,332: [27903] m.e.manticore:INFO: 16 alive states, 6 terminated states
2022-08-31 17:08:27,836: [28631] m.c.manticore:INFO: Generated testcase No. 1 - STOP(3 txs)
2022-08-31 17:08:27,837: [28631] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,841: [28629] m.c.manticore:INFO: Generated testcase No. 0 - STOP(3 txs)
2022-08-31 17:08:27,842: [28629] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,845: [28634] m.c.manticore:INFO: Generated testcase No. 2 - STOP(3 txs)
2022-08-31 17:08:27,846: [28634] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,881: [28632] m.c.manticore:INFO: Generated testcase No. 4 - STOP(3 txs)
2022-08-31 17:08:27,882: [28632] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,895: [28635] m.c.manticore:INFO: Generated testcase No. 5 - STOP(3 txs)
2022-08-31 17:08:27,909: [28630] m.c.manticore:INFO: Generated testcase No. 7 - STOP(3 txs)
2022-08-31 17:08:27,909: [28635] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,909: [28630] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,895: [28628] m.c.manticore:INFO: Generated testcase No. 3 - STOP(3 txs)
2022-08-31 17:08:27,910: [28628] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,916: [28633] m.c.manticore:INFO: Generated testcase No. 6 - STOP(3 txs)
2022-08-31 17:08:27,924: [28633] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,933: [28637] m.c.manticore:INFO: Generated testcase No. 8 - STOP(3 txs)
2022-08-31 17:08:27,934: [28637] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,947: [28641] m.c.manticore:INFO: Generated testcase No. 9 - STOP(3 txs)
2022-08-31 17:08:27,948: [28641] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,996: [28640] m.c.manticore:INFO: Generated testcase No. 10 - STOP(3 txs)
2022-08-31 17:08:27,996: [28640] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:31,044: [28629] m.c.manticore:INFO: Generated testcase No. 11 - STOP(3 txs)
2022-08-31 17:08:31,228: [28634] m.c.manticore:INFO: Generated testcase No. 12 - STOP(3 txs)
2022-08-31 17:08:31,265: [28630] m.c.manticore:INFO: Generated testcase No. 13 - STOP(3 txs)
2022-08-31 17:08:31,311: [28641] m.c.manticore:INFO: Generated testcase No. 14 - STOP(3 txs)
2022-08-31 17:08:31,445: [28631] m.c.manticore:INFO: Generated testcase No. 15 - STOP(3 txs)
2022-08-31 17:08:34,219: [27903] m.c.manticore:INFO: Results in /***/example/umd_example/mcore_cuh9jykm
2022-08-31 17:08:34,219: [27903] m.c.manticore:INFO: Total time: 136.78626823425293

DaniWppner · 2022-09-20T16:25:29Z

From manticore version 3.6 onwards the cli defaults to quick-mode instead of thorough-mode.
Try running manticore simple_example.sol --thorough instead.

0xharold · 2022-10-03T12:52:28Z

Hi,
I am having similar issues:

manticore version : 0.3.7
python version : 3.8.10
OS : WSL2 -> Ubuntu

1. Using eth-security-toolbox in Docker

Once I run the following commands:

sudo docker run -it --rm -v $PWD:/src trailofbits/eth-security-toolbox

ethsec@fce73100d55f:~$ cd /src/contracts/manticore/exercise1/
ethsec@fce73100d55f:/src/contracts/manticore/exercise1$ manticore Example1.sol

then I get:

2022-10-03 12:41:04,609: [21] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2022-10-03 12:41:04,609: [21] m.main:INFO: Beginning analysis
2022-10-03 12:41:04,614: [21] m.e.manticore:INFO: Starting symbolic create contract
Process Process-1:
Traceback (most recent call last):
  File "/usr/lib/python3.6/multiprocessing/process.py", line 258, in _bootstrap
    self.run()
  File "/usr/lib/python3.6/multiprocessing/process.py", line 93, in run
    self._target(*self._args, **self._kwargs)
  File "/home/ethsec/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 1756, in worker_finalize
    finalizer(q.get_nowait())
  File "/home/ethsec/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 1747, in finalizer
    if only_alive_states and last_tx.result in {"REVERT", "THROW", "TXERROR"}:
AttributeError: 'NoneType' object has no attribute 'result'
2022-10-03 12:41:04,848: [21] m.c.manticore:INFO: Results in /src/contracts/manticore/exercise1/mcore_g5qqqyb9
2022-10-03 12:41:04,849: [21] m.c.manticore:WARNING: Manticore failed to run

or:

ethsec@fce73100d55f:/src/contracts/manticore/exercise1$ manticore Example1.sol --thorough

2022-10-03 12:42:30,387: [44] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, DetectReentrancySimple, DetectReentrancyAdvanced, DetectUnusedRetVal, DetectSuicidal, DetectDelegatecall, DetectExternalCallAndLeak, DetectEnvInstruction, DetectManipulableBalance
2022-10-03 12:42:30,388: [44] m.main:INFO: Beginning analysis
2022-10-03 12:42:30,392: [44] m.e.manticore:INFO: Starting symbolic create contract
2022-10-03 12:42:30,660: [53] m.c.manticore:INFO: Generated testcase No. 0 - NO STATE RESULT (?)(0 txs)
2022-10-03 12:42:30,661: [53] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 12:42:30,734: [44] m.c.manticore:INFO: Results in /src/contracts/manticore/exercise1/mcore_z0ba6a_k
2022-10-03 12:42:30,735: [44] m.c.manticore:WARNING: Manticore failed to run

2. Using manticore in Docker

This one produce at least some results, but it still seems not to work as indented:

sudo docker run -it --rm -v $PWD:/src trailofbits/manticore

root@445568859aaa:/# cd /src/contracts/manticore/exercise1/
root@445568859aaa:/src/contracts/manticore/exercise1# manticore Example1.sol --thorough

I get:

2022-10-03 12:46:49,974: [34] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, DetectReentrancySimple, DetectReentrancyAdvanced, DetectUnusedRetVal, DetectSuicidal, DetectDelegatecall, DetectExternalCallAndLeak, DetectEnvInstruction, DetectManipulableBalance
2022-10-03 12:46:49,974: [34] m.main:INFO: Beginning analysis
2022-10-03 12:46:49,976: [34] m.e.manticore:INFO: Starting symbolic create contract
2022-10-03 12:46:50,330: [34] m.e.manticore:INFO: Starting symbolic transaction: 0
2022-10-03 12:46:50,719: [34] m.e.manticore:INFO: 1 alive states, 3 terminated states
2022-10-03 12:46:50,794: [34] m.e.manticore:INFO: Starting symbolic transaction: 1
2022-10-03 12:46:51,654: [34] m.e.manticore:INFO: 1 alive states, 5 terminated states
2022-10-03 12:46:51,852: [116] m.c.manticore:INFO: Generated testcase No. 0 - REVERT(1 txs)
2022-10-03 12:46:51,856: [116] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 12:46:51,901: [117] m.c.manticore:INFO: Generated testcase No. 1 - REVERT(2 txs)
2022-10-03 12:46:51,903: [117] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 12:46:51,909: [119] m.c.manticore:INFO: Generated testcase No. 2 - REVERT(2 txs)
2022-10-03 12:46:51,921: [119] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 12:46:52,110: [115] m.c.manticore:INFO: Generated testcase No. 3 - STOP(3 txs)
2022-10-03 12:46:52,112: [115] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 12:46:52,171: [121] m.c.manticore:INFO: Generated testcase No. 4 - REVERT(3 txs)
2022-10-03 12:46:52,174: [121] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 12:46:52,430: [116] m.c.manticore:INFO: Generated testcase No. 5 - REVERT(3 txs)
2022-10-03 12:46:54,104: [34] m.c.manticore:INFO: Results in /src/contracts/manticore/exercise1/mcore_xh1ep81t
2022-10-03 12:46:54,105: [34] m.c.manticore:INFO: Total time: 3.3057878017425537

3. Using manticore standalone

This produces the same result as manticore in docker

pip install manticore

cd ./contracts/manticore/exercise1
manticore Example1.sol --thorough

I get the same results:

2022-10-03 14:48:28,750: [20899] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, DetectReentrancySimple, DetectReentrancyAdvanced, DetectUnusedRetVal, DetectSuicidal, DetectDelegatecall, DetectExternalCallAndLeak, DetectEnvInstruction, DetectManipulableBalance
2022-10-03 14:48:28,750: [20899] m.main:INFO: Beginning analysis
2022-10-03 14:48:28,752: [20899] m.e.manticore:INFO: Starting symbolic create contract
2022-10-03 14:48:29,115: [20899] m.e.manticore:INFO: Starting symbolic transaction: 0
2022-10-03 14:48:29,592: [20899] m.e.manticore:INFO: 1 alive states, 3 terminated states
2022-10-03 14:48:29,682: [20899] m.e.manticore:INFO: Starting symbolic transaction: 1
2022-10-03 14:48:30,683: [20899] m.e.manticore:INFO: 1 alive states, 5 terminated states
2022-10-03 14:48:30,949: [20996] m.c.manticore:INFO: Generated testcase No. 0 - REVERT(1 txs)
2022-10-03 14:48:30,956: [20996] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 14:48:30,972: [20997] m.c.manticore:INFO: Generated testcase No. 1 - REVERT(2 txs)
2022-10-03 14:48:30,974: [20997] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 14:48:30,993: [20998] m.c.manticore:INFO: Generated testcase No. 2 - REVERT(2 txs)
2022-10-03 14:48:30,995: [20998] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 14:48:31,297: [21000] m.c.manticore:INFO: Generated testcase No. 3 - REVERT(3 txs)
2022-10-03 14:48:31,298: [21000] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 14:48:31,315: [20995] m.c.manticore:INFO: Generated testcase No. 4 - STOP(3 txs)
2022-10-03 14:48:31,319: [20995] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 14:48:31,402: [21002] m.c.manticore:INFO: Generated testcase No. 5 - REVERT(3 txs)
2022-10-03 14:48:31,414: [21002] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 14:48:33,507: [20899] m.c.manticore:INFO: Results in /home/haraslub/echidna-tutorial/contracts/manticore/exercise1/mcore_8cmmnfn8
2022-10-03 14:48:33,507: [20899] m.c.manticore:INFO: Total time: 3.821932315826416

zeroonechange · 2022-11-15T10:04:44Z

Using eth-security-toolbox in Docker

WSL Ubuntu 18.04.6 LTS
Docker version 20.10.20, build 9fdeb9c

ethsec@c805cd48e755:/code$ manticore manticore/examples/evm/umd_example.sol
2022-11-15 09:57:17,372: [51] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2022-11-15 09:57:17,373: [51] m.main:INFO: Beginning analysis
2022-11-15 09:57:17,375: [51] m.e.manticore:INFO: Starting symbolic create contract
Process Process-12:
Traceback (most recent call last):
File "/usr/lib/python3.6/multiprocessing/process.py", line 258, in _bootstrap
self.run()
File "/usr/lib/python3.6/multiprocessing/process.py", line 93, in run
self._target(*self._args, **self._kwargs)
File "/home/ethsec/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 1756, in worker_finalize
finalizer(q.get_nowait())
File "/home/ethsec/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 1747, in finalizer
if only_alive_states and last_tx.result in {"REVERT", "THROW", "TXERROR"}:
AttributeError: 'NoneType' object has no attribute 'result'
2022-11-15 09:57:17,527: [51] m.c.manticore:INFO: Results in /code/mcore_t13shgmc
2022-11-15 09:57:17,527: [51] m.c.manticore:WARNING: Manticore failed to run

sachinbal · 2023-04-12T11:43:31Z

@bzhang42 did you get a solution to the bug which you have raised? I too am facing a similar problem. Please share in case you have found out a solution or workaround for this issue.

bzhang42 · 2023-04-16T14:54:26Z

No solution so far. I decided to use hevm symbolic execution instead.

spaceh3ad · 2023-12-13T15:40:20Z

Using python3.8 for manticore solves this

bzhang42 added the bug label Aug 25, 2022

ekilmer added this to the Manticore 0.4.0 milestone Nov 30, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Manticore tutorial simple example incorrect #2583

Manticore tutorial simple example incorrect #2583

bzhang42 commented Aug 25, 2022

Kaylee-Hsu commented Aug 31, 2022 •

edited

DaniWppner commented Sep 20, 2022 •

edited

0xharold commented Oct 3, 2022

zeroonechange commented Nov 15, 2022

sachinbal commented Apr 12, 2023

bzhang42 commented Apr 16, 2023

spaceh3ad commented Dec 13, 2023

Manticore tutorial simple example incorrect #2583

Manticore tutorial simple example incorrect #2583

Comments

bzhang42 commented Aug 25, 2022

Summary of the problem

Manticore version

Python version

OS / Environment

Dependencies

Step to reproduce the behavior

Expected behavior

Actual behavior

Any relevant logs

Kaylee-Hsu commented Aug 31, 2022 • edited

DaniWppner commented Sep 20, 2022 • edited

0xharold commented Oct 3, 2022

1. Using eth-security-toolbox in Docker

2. Using manticore in Docker

3. Using manticore standalone

zeroonechange commented Nov 15, 2022

sachinbal commented Apr 12, 2023

bzhang42 commented Apr 16, 2023

spaceh3ad commented Dec 13, 2023

Kaylee-Hsu commented Aug 31, 2022 •

edited

DaniWppner commented Sep 20, 2022 •

edited