Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve crytic-compile support #1795

Merged
merged 1 commit into from
Aug 25, 2020

Conversation

montyly
Copy link
Member

@montyly montyly commented Aug 18, 2020

  • crytic-compile: use latest release
  • manticore-verifier: enable crytic-compile cli flags

The crytic-compile version currently used by Manticore is out of date.

Additionally, manticore-verifier did not use the crytic-compile cli flags

To test this:

$ npx truffle unbox metacoin

Update contracts/MetaCoin.sol and add

    function crytic_test() public returns(bool){
        return balances[msg.sender] > 1;
    }

Then

$ manticore-verifier . --contract MetaCoin
$ rm truffle-config.js 
$ manticore-verifier . --contract MetaCoin --compile-force-framework Truffle --ignore-compile

The last command re-run Manticore, but fails without this PR

manticore-verifier: enable crytic-comoile cli flags
@ggrieco-tob
Copy link
Contributor

I tested this PR and seems to be working fine! 🎉 However, the flag names and cli help could be improved:

                          ...
                          [--propconfig PROPCONFIG] [--quick-mode]
                          [--contract_name CONTRACT_NAME] [--maxfail MAXFAIL]
                          ...

Can we use --contract instead of --contract_name and --config instead of --propconfig?

@montyly
Copy link
Member Author

montyly commented Aug 18, 2020

It's a good idea, but these flags are not related to crytic-compile; so we should probably move this recommendation to a separate issue/PR

@ehennenfent ehennenfent added this to Reviewer approved in Manticore Aug 25, 2020
@ehennenfent
Copy link
Contributor

This has been approved w/o changes for 7 days, so I'm going to merge it. Thanks for the fix!

@ehennenfent ehennenfent merged commit 2eaf7c0 into master Aug 25, 2020
Manticore automation moved this from Reviewer approved to Done Aug 25, 2020
@ehennenfent ehennenfent deleted the dev-manticore-verifier-crytic-compile branch August 25, 2020 23:27
@ehennenfent ehennenfent added this to the Manticore 0.3.5 milestone Sep 3, 2020
ekilmer added a commit that referenced this pull request Sep 28, 2020
* master:
  Change types.FunctionType=<class 'function'> (#1803)
  Fix test regressions (#1804)
  State Introspection API (#1775)
  Fix EVM account existence checks for selfdestruct and call (#1801)
  Add partial implementation of sendto syscall (#1791)
  crytic-compile: use latest release (#1795)
  Update gas metering for calls to empty accounts (#1774)
  Fix BitVec with symbolic offset and fix TranslatorSmtlib.unique thread safety (#1792)
  Fix Coveralls for external PRs (#1794)
  Convert plugin list to dict (#1781)
  Symbolic-length reads from symbolic sockets (#1786)
  Removing Thread unsafe global caching (#1788)
  Add Manticore native State-specific hooks (#1777)
ekilmer added a commit that referenced this pull request Feb 27, 2021
* master: (43 commits)
  Syscall specific hooks (#2389)
  TUI Support Infrastructure (#1620)
  Fix coveralls upload (#2387)
  docs: fix simple typo, straigth -> straight (#2381)
  Attempt to allow symbolic balances from the start (#1818)
  Fix state.cpu.PC member (#1825)
  Bump black and mypy (#1824)
  Manticore 0.3.5 (#1808)
  Fix yices timeout argument (#1817)
  Detect default solver (#1820)
  Ignore Gas Calculations by Default (#1816)
  native/cpu/x86: Add support for CPUID EAX=80000000h (#1811)
  Change types.FunctionType=<class 'function'> (#1803)
  Fix test regressions (#1804)
  State Introspection API (#1775)
  Fix EVM account existence checks for selfdestruct and call (#1801)
  Add partial implementation of sendto syscall (#1791)
  crytic-compile: use latest release (#1795)
  Update gas metering for calls to empty accounts (#1774)
  Fix BitVec with symbolic offset and fix TranslatorSmtlib.unique thread safety (#1792)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
Manticore
  
Done
Development

Successfully merging this pull request may close these issues.

None yet

4 participants