Very high memory usage

[iowaguy]

I am running greed on contract Ethereum 0x3DCb577A5d3bFAedb848F59ae5939e4d2D22d182, and the memory usage is extremely high. The machine has 188 GB RAM, and it is being killed by the OOM killer. In fact, this is just one of thousands of contracts that are seeing the same issue.

I am surprised by this as symbolic execution, in my experience, doesn't usually use so much memory, especially for small programs like solidity contracts. In our case, we are only checking the transfer() function, which is quite short.

Below is the output from the Memray python memory profiler.

memray-flamegraph-mev_tk_checker.py.21272.html

In particular, it seems that self.root_lambda_constraint.initiate(index) is doing most of the allocations.

Any idea how we can decrease the memory footprint so we can complete a run of greed on these contracts?

[robmcl4]

What exploration strategy are you using? I've seen path explosion in the transfer() function before due to several different possible symbolic variable settings.

My best guess is that you're exploring many, many possible paths, and along the way, you're generating a LOT of symbolic variables, which we never remove from the symbolic state.

(When we run Greed we typically set a memory limit in the OS and just let it fail on some cases... I recommend you consider this as well as 100% success is unrealistic)

[iowaguy]

We are exploring as many states as possible. I thought that we might not see a path explosion though, because the functions we're looking at are relatively short.

Is there any way to prune symbolic variables that aren't used anymore?

[degrigis]

Hey @iowaguy, the actual code of the transfer for that contract (see the decompiled
at https://app.dedaub.com/ethereum/address/0x3dcb577a5d3bfaedb848f59ae5939e4d2d22d182/decompiled) is not very small. So, if you keep everything symbolic in the initial setup (e.g., CALLER, BLOCK, etc...), this is gonna likely state explode and OOM your box.

I can see, for instance, the transfer calling swapAndLiquify under certain conditions (https://app.dedaub.com/ethereum/address/0x3dcb577a5d3bfaedb848f59ae5939e4d2d22d182/decompiled?line=508), which contains a while loop. If the condition of such a loop is symbolic you will state explode without a pruning strat.

I would suggest starting with a few concrete variables and writing a simple pruning technique. This will move the SimState in the "pruned" stash, and the solver's context will get disposed (https://github.com/ucsb-seclab/greed/blob/main/greed/sim_manager.py#L195) .
I believe this obtains what you were looking for: "prune symbolic variables that aren't used anymore".

If you want to share your greed's setup here, we can give you some hints.