Manticore seems to terminate without proper ending message

[sunbeomso]

OS / Environment

host: Ubuntu 18.04.2 , used provided Manticore docker image

Manticore version

0.2.5 (from docker image)

Python version

3.6.7 (from docker image)

Summary of the problem

While running Manticore on the four contracts below, I observed that Manticore did not print proper termination message. For the four contract and corresponding entire logs, please see Any relevant logs below. I wonder whether all these are Manticore's internal bugs or Manticore's analyses are properly terminated.

But based on my experience with Manticore, in usual termination cases, Manticore seems to produce command log that ends with information on analysis result file and total elapsed time, e.g.,:

[8413] m.c.manticore: [[34mINFO: [[0m Results in /mcore_ew51iy6r
[8413] m.c.manticore: [[34mINFO: [[0m Total time: 2062.4852361679077

which are absent for the four contracts that I attached below.

Step to reproduce the behavior

As did in #1435 , I typed the following command to detect integer overflow bugs for each contract:

docker exec -it CONTAINERID manticore --core.timeout 1800 //contract.sol --contract MyAdvancedToken --exclude delegatecall,reentrancy,reentrancy-adv,env-instr,ext-call-leak,suicidal,uninitialized-memory,uninitialized-storage,invalid,unused-return

where CONTAINERID is a docker container's ID, and contract.sol is each of the four contracts below (see "Any relevant logs").

Any relevant logs

Contract1: https://etherscan.io/address/0x3ac96bbe8b60d715fd818b3fe242edf9def20571#code
Entire log on Contract1:

[5969] m.c.manticore: [34mINFO: [0m Verbosity set to 1.
[5969] m.main: [34mINFO: [0m Registered plugins: DetectIntegerOverflow
[5969] m.main: [34mINFO: [0m Beginning analysis
[5969] m.e.manticore: [34mINFO: [0m Starting symbolic create contract

Contract2: https://etherscan.io/address/0x81a9ebfdcd87cd291eb5e5260901a898df3bdafd#code
Entire log on Contract2:

[5808] m.c.manticore: [34mINFO: [0m Verbosity set to 1.
[5808] m.main: [34mINFO: [0m Registered plugins: DetectIntegerOverflow
[5808] m.main: [34mINFO: [0m Beginning analysis
[5808] m.e.manticore: [34mINFO: [0m Starting symbolic create contract
[5808] m.e.detectors: [33mWARNING: [0m Unsigned integer overflow at MUL instruction
[5808] m.e.detectors: [33mWARNING: [0m Unsigned integer overflow at MUL instruction

Contract3: https://etherscan.io/address/0x10e886bacd4a12c21bb39646751374eae495b776#code
Entire log on Contract3:

[9739] m.c.manticore: [34mINFO: [0m Verbosity set to 1.
[9739] m.main: [34mINFO: [0m Registered plugins: DetectIntegerOverflow
[9739] m.main: [34mINFO: [0m Beginning analysis
[9739] m.e.manticore: [34mINFO: [0m Starting symbolic create contract

Contract4: https://etherscan.io/address/0x2d6669c810bf1444d2e5e7f4cfc56a4c10cf7a2a#code
Entire log on Contract4:

[15908] m.c.manticore: [34mINFO: [0m Verbosity set to 1.
[15908] m.main: [34mINFO: [0m Registered plugins: DetectIntegerOverflow
[15908] m.main: [34mINFO: [0m Beginning analysis
[15908] m.e.manticore: [34mINFO: [0m Starting symbolic create contract^M

Further I note that, for all 4 cases, Manticore produce a directory that only contains one or two files named "state_ 00000001.pkl" (though this directory was not specified in the command log, I was able to track this by just running Manticore only on these 4 contracts).

[ehennenfent]

Regarding the termination message: When #1385 was merged, it included some changes to both the API and the output. #1384 will restore the old output behavior, and we'll have a list of all the changes when we next issue a release. Of course, since you're on the latest master, that doesn't really help you, and I'm afraid I don't have a workaround right now. We're working on merging #1384 ASAP, so hopefully the ending messages should be back to normal before too long.

[sunbeomso]

@ehennenfent Thanks for the reply. So do you mean that it is currently not sure whether Manticore successfully terminated or not? ( or just the problem of a module for logging message?) As I described, Manticore produced a directory that only contains a X.pkl file such as state_ 00000001.pkl .

[ehennenfent]

Hey, sorry we've been letting this languish. We're prepping to release a new version of Manticore that should have these changes documented in the changelog. In #1384 we moved the total time printing to manticore/native. That means that if you're running on an ELF binary, it'll print the total time, but it won't do so for EVM smart contracts. We made this change because the start time is recorded in the will_run callback, which should only ever be run once for native binaries. However, in smart contracts, it's called once for every transaction, which means that "total time" in the sense we've measured it before isn't valid. In this case, its absence is expected.

We were missing the save_run_data call in ethereum/manticore that saves the Manticore command and config data and prints the "Results in " message, so we've added that back in.

The directory full of .pkl files is also expected. Those are serialized states that Manticore has moved to the disk. Since #1385, one needs to call the finalize method (or the underlying generate_testcases method in order to dump the states to the disk. That's for performance reasons, so that users can make the decision themselves whether to spend the time waiting for the solver.