Skip to content

Conversation

gustavo-grieco
Copy link
Contributor

When manticore is used during audits, it's very common to take a piece of code and abstract the state variables as parameters, to allow our tool to explore any possible state (even at the cost of false positives). This increases the list of parameters in functions. Unfortunately with the current size of symbolic inputs, this can happen:

contract C {
  function f(uint256, uint256, uint256, uint256, uint256, uint256, uint256, uint256, uint256, uint256, uint256 x) public {
    require(x > 0);
  }
}

Manticore silently fails to produce live states:

$ manticore long.sol --txlimit 1
2021-06-23 14:48:15,905: [32264] m.main:INFO: Registered plugins: <class 'manticore.core.plugin.IntrospectionAPIPlugin'>, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2021-06-23 14:48:15,905: [32264] m.main:INFO: Beginning analysis
2021-06-23 14:48:15,907: [32264] m.e.manticore:INFO: Starting symbolic create contract
2021-06-23 14:48:16,091: [32264] m.e.manticore:INFO: Starting symbolic transaction: 0
2021-06-23 14:48:16,736: [32264] m.e.manticore:INFO: 0 alive states, 2 terminated states
2021-06-23 14:48:16,774: [32264] m.c.manticore:INFO: Results in /home/g/Code/manticore/mcore_mkqlwra1
2021-06-23 14:48:16,775: [32264] m.c.manticore:INFO: Total time: 0.6813325881958008

This PR doubles the amount of symbolic bytes to mitigate this issue.

@ehennenfent
Copy link
Contributor

Per the meeting, since this could increase the amount of symbolic data Manticore has to deal with in simple cases, we should look into using the information crytic-compile provides us to see if we can choose the exact number of symbolic bytes we need based on the ABI of the contract functions. This will only work for fixed-size arguments, but would be more efficient than always just guessing, as we currently do.

@dguido dguido requested a review from ekilmer as a code owner August 21, 2025 17:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants