runtimeverification / runtimeverification/evm-semantics

Segmentation Fault Encountered While Generating a Proof

Open
#2,070 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
KCL
Stars
591
Forks
156
Avg merge
2h 19m
Merged PRs (30d)
1

Description

NOTICE: I moved this issue here from the https://github.com/runtimeverification/hs-backend-booster repository.

I'm facing a segmentation fault issue when attempting to generate a proof using the kevm foundry-prove command in our Symbolic Solidity Debugger project. Although this is not directly related to the ongoing Blockswap project, it's crucial for the Symbolic Solidity Debugger. However, I want to emphasize that this issue is not of high priority.

Reproduction Steps:

The following command triggers the issue. This issue occurs irrespective of the flags --no-simplify-init and --use-booster.

> git clone https://github.com/runtimeverification/_audits_bswap-eng_gateway-kernel
> cd _audits_bswap-eng_gateway-kernel
> export FOUNDRY_PROFILE=k
> kevm foundry-kompile --with-llvm-library
> kevm foundry-prove --max-depth 10000 --max-iterations 10000 --bmc-depth 3 --workers 1 --verbose --break-every-step --test DepositTest.testDepositRevertsIffNotInDomain
...
...
INFO 2023-09-13 13:21:08,236 pyk.ktool.kprint - Invoking kast_to_kore
INFO 2023-09-13 13:21:08,305 pyk.kore.rpc - Sending request to localhost:34175: 2 - simplify
INFO 2023-09-13 13:24:12,544 pyk.kore.rpc - Received response from localhost:34175: 2 - simplify
/nix/store/bylyxgwa7g05919jc01wk9riidv0pgg4-kevm-dirty/bin/.kevm-wrapped: line 9: 23241 Segmentation fault      /nix/store/1wzsgx4ir4z2iyn58gwghzf48gdjrjrp-python3.10-kevm-pyk-1.0.289/bin/kontrol "$@"
  • I'm not entirely sure whether this issue resides in the backend or elsewhere, but I'm running out of troubleshooting ideas.
  • Could someone from your team please look into this when convenient?

The full bug report can be found here: https://github.com/runtimeverification/_audits_bswap-eng_gateway-kernel/issues/1

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Reproduce the failure using the listed git clone, foundry-kompile, and kevm foundry-prove commands, including the named DepositTest.testDepositRevertsIffNotInDomain test. Compare the output with the full report in _audits_bswap-eng_gateway-kernel/issues/1 and trace whether the fault is in the proof command or backend; done means the cause is isolated and the proof no longer segfaults.

Written by the indexing model from the issue text.

Assessment

Tech stack
solidity
Domain
backend
Issue type
Bug
Difficulty
5/5
Estimated time
Over a week
Activity status
Stale
Clarity
Needs clarification
Newbie friendliness
25/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.