Slow symbolic execution of the first example for PrimalityCheck

[enzeve]

First of all. So far, with my relative little amount of experience with hevm, I really like it. It is intuitive, easy to use, and has a lot of features. However, it is slower than expected.

I'm testing hevm in the GitHub actions.

I wanted to learn more about hevm so I followed the steps on this page.

The first example (PrimalityCheck.sol) took 40 minutes to finish in a GitHub action. On the linked page it looked like it should be way faster.

The relevant part in main.yml for the GitHub action looks like this:

HEVM:
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v3
        with:
          submodules: recursive

      - name: Setup dapptools environment
        uses: risedle/setup-dapptools@v4
        with:
          solc: "solc_0_8_13"

      - name: hevm version
        run: hevm version

      - name: PrimalityCheck bin-runtime
        run: docker run -v ${{ github.workspace }}:/project ethereum/solc:0.8.13 -o /project --bin-runtime --overwrite /project/apps/smart-contracts/src/PrimalityCheck.sol

      - name: PrimalityCheck symbolic
        run: hevm symbolic --smttimeout 3600000 --code $(<PrimalityCheck.bin-runtime) --sig "factor(uint x, uint y)"

The output of hevm version was 0.49.1.

The output of PrimalityCheck symbolic was as expected but it took 40 minutes.

checking postcondition...
Assertion violation found.
Calldata:
0xd5a2424900000000000000000000000000000000000000000000000000000000000003b900000000000000000000000000000000000000000000000000000000000003fd
factor(953, 1021)
Caller:
0x0000000000000000000000000000000000000000
Callvalue:
0
Error: Process completed with exit code 1.

Does anyone know why this takes so long?

[d-xo]

In general symbolic execution is slow because it's a hard problem, and non linear arithmetic (multiplication and division) is very difficult for smt solvers to handle.

We're working on an upgraded symbolic execution engine at https://github.com/ethereum/hevm/ that we expect to improve matters, but it's not yet in a usable state.