crytic / echidna

Ethereum smart contract fuzzer
https://secure-contracts.com/program-analysis/echidna/index.html
GNU Affero General Public License v3.0
2.75k stars 368 forks source link

Problem building with profile enable using NIX - the flag -p requires the program to be built with -prof #844

Open Robsonsjre opened 1 year ago

Robsonsjre commented 1 year ago

Hello,

I'm trying to fuzzy a contract using assert mode with testLimit 50000 . It is taking a long time and after they reach 6000 trials, echidna suddenly stops.

So in order to debug the problem, I've tried to build using Nix as recommended.

The documentation says: nix-build --arg profiling true After that, I've unpacked the created build (tar.gz file) inside the /result folder.

When I try to run the echidna command using +RTS -p, I receive the error the flag -p requires the program to be built with -prof

What I am doing wrong?

My machine:

MacOS M1 Max - Monterey

My echidna config.yaml:

#format can be "text" or "json" for different output (human or machine readable)
# format: 'text'
#coverage controls coverage guided testing
coverage: true
testMode: "assertion"
# #psender is the sender for property transactions; by default intentionally
# #the same as contract deployer
# psender: "0x00a329c0648769a73afac7f9381e08fb43dbea70"
# #prefix is the prefix for Boolean functions that are properties to be checked
prefix: "echidna_"
# #propMaxGas defines gas cost at which a property fails
# propMaxGas: 8000030
# #testMaxGas is a gas limit; does not cause failure, but terminates sequence
# testMaxGas: 8000030
# #maxGasprice is the maximum gas price
# maxGasprice: 100000000000
# #testLimit is the number of test sequences to run
testLimit: 50000
# #stopOnFail makes echidna terminate as soon as any property fails and has been shrunk
# stopOnFail: false
# #estimateGas makes echidna perform analysis of maximum gas costs for functions (experimental)
# estimateGas: false
# #seqLen defines how many transactions are in a test sequence
seqLen: 1000
# #shrinkLimit determines how much effort is spent shrinking failing sequences
# shrinkLimit: 5000
# #contractAddr is the address of the contract itself
# contractAddr: "0x00a329c0648769a73afac7f9381e08fb43dbea72"
# #deployer is address of the contract deployer (who often is privileged owner, etc.)
deployer: "0x30000"
# #sender is set of addresses transactions may originate from
sender: ["0x10000", "0x20000", "0x30000"]
# #balanceAddr is default balance for addresses
# balanceAddr: 0xffffffff
# #balanceContract overrides balanceAddr for the contract address
# balanceContract: 0
# #solcArgs allows special args to solc
# solcArgs: ""
# #solcLibs is solc libraries
# solcLibs: []
# #cryticArgs allows special args to crytic
cryticArgs:
  [
    "--solc-remaps", "@openzeppelin/contracts/=node_modules/@openzeppelin/contracts/ hardhat=node_modules/hardhat/"
#    "--solc-libraries", "DepositQueueLib=0xf378794d7e6062ee64e53c8be33e9b16d5a034dc"
  ]
# #quiet produces (much) less verbose output
quiet: false
# #initialize the blockchain with some data
# initialize: null
# #whether ot not to use the multi-abi mode of testing
# multi-abi: false
# #benchmarkMode enables benchmark mode
# benchmarkMode: false
# #timeout controls test timeout settings
# timeout: null
# #seed not defined by default, is the random seed
# #seed: 0
# #dictFreq controls how often to use echidna's internal dictionary vs random
# #values
# dictFreq: 0.40
# maxTimeDelay: 604800
# #maximum time between generated txs; default is one week
# maxBlockDelay: 60480
# #maximum number of blocks elapsed between generated txs; default is expected increment in one week
# # timeout:
# #campaign timeout (in seconds)
# # list of methods to filter
# filterFunctions: []
# # by default, blacklist methods in filterFunctions
# filterBlacklist: true
# #directory to save the corpus; by default is disabled
corpusDir: "echidna/corpus"
# # constants for corpus mutations (for experimentation only)
# mutConsts: [100, 1, 1]
# # maximum value to send to payable functions
# maxValue: 100000000000000000000 # 100 eth
ggrieco-tob commented 1 year ago

Hi Rob, thanks for creating this issue. @arcz is our Nix expert so let's wait for his response.

arcz commented 1 year ago

I've checked and this works for me fine. Are you sure you are running the correct binary? The binary is in result/bin/echidna-test but you are unpacking a tar.gz file. It seems that you ran macos-release.nix but you should run default.nix.

arcz commented 1 year ago

@Robsonsjre are you still experiencing this issue?

Robsonsjre commented 1 year ago

I went to vacations this week, I come back Monday and I will check if I managed to make it work!

Robsonsjre commented 1 year ago

Hi @arcz , Ive tried to run nix-build default.nix --arg profiling true. Now Im receiving some errors regarding the lack of libraries. How do I install those libraries?

lib/Echidna/Events.hs:3:8: error:
    Could not find module ‘Prelude’
    Perhaps you haven't installed the profiling libraries for package ‘base-4.14.3.0’?
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
  |
3 | module Echidna.Events where
  |        ^^^^^^^^^^^^^^

lib/Echidna/Events.hs:5:1: error:
    Could not find module ‘Data.ByteString’
    Perhaps you haven't installed the profiling libraries for package ‘bytestring-0.10.12.0’?
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
  |
5 | import Data.ByteString qualified as BS
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

lib/Echidna/Events.hs:6:1: error:
    Could not find module ‘Data.ByteString.Lazy’
    Perhaps you haven't installed the profiling libraries for package ‘bytestring-0.10.12.0’?
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
  |
6 | import Data.ByteString.Lazy (fromStrict)
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
arcz commented 1 year ago

I confirm I have the same error on M1, it doesn't happen on x86. I suspect there is some nixpkgs configuration issue on M1. I would need to dig into it. At the moment, what I can recommend is to get an x86 machine and build with profiling there.

siraben commented 1 year ago

As a workaround, nix develop --system x86_64-darwin works on M1 via Rosetta. Then you can run the profiler with cabal run --enable-profiling echidna -- +RTS -p -RTS tests/solidity/basic/flags.sol --seed 0 --test-limit 1000 --format text