Adding SMT2 queries from hevm symbolic execution framework running on the eth-sc-comp set

[msooseth]

Hi All,

This is a set of files generated by the hevm symbolic execution framework [1] running on eth-sc-comp benchmarks [2] set with --dumpsmt flag set on ./bench.py in [2]. The files have been massaged to fit the requirements by the SMT-LIB benchmark set: status, license info, etc. Unfortunately, the as const syntax such as:

(define-sort Word () (_ BitVec 256))
(define-sort Addr () (_ BitVec 160))
(define-sort Storage () (Array Word Word))
(declare-const symaddr_arg1 Addr)
(assert (= (ite (= (select ((as const Storage) #x0000000000000000000000000000000000000000000000000000000000000000) (concat (_ bv0 96) symaddr_arg1 )) (_ bv0 256)) (_ bv1 256) (_ bv0 256)) (_ bv0 256)))

is not standardized but needed by hevm. However, it is supported by all SMT solvers we use: Z3, CVC5, Bitwuzla, though Z3 strangely only supports it in ALL logic, not in QF_AUFBV. I have been told that I should just submit these as-is, as the LIB-SMT standardization committee may make progress on this feature.

Let me know if there is something amiss and looking forward to meeting in Montreal,

Mate

[1] https://github.com/ethereum/hevm
[2] https://github.com/eth-sc-comp/benchmarks

[hansjoergschurr]

The CI complains about some duplicated benchmarks right now, we will have to remove those.

I think the benchmarks can also be polish to make them a bit nicer to work with:

1. We try to keep the order of the commands in the benchmark headers consistent (see https://github.com/SMT-LIB/benchmark-submission/blob/main/README.md?plain=1#L54 ) So in your case the :status should move to the end.
2. The benchmarks start with very long comments containing some tree. I would tend towards deleting these comments. However, you know the benchmarks better. So if you believe this is useful information we keep it. Maybe it would then be better to move the comment after the header.
3. There should be a newline after (exit).
4. The :source header should contain a Generated by (can be an institution) and a Generated on line. I think in your case it might also make sense to include Application.
5. I think it would be great to include the first part of the description of the benchmarks from your pull request directly in the benchmark. See https://github.com/SMT-LIB/benchmark-submission/blob/main/README.md?plain=1#L109

The idea is that we polish benchmarks that use widely used, but non-standard, features, and then include them in a benchmark release as soon as those features become standard.

[msooseth]

Hi,

First of all, thanks for all the feedback! Sorry, I am currently on a bit of a break for industry (i.e. HEVM). Let me try to respond to your comments, here:

1. Fair point, sorry. It's a bit painful to change it now, though. This kind of large-scale text editing takes lots of time.
2. These are actually incredibly useful for us, and they map to the problem 1-to-1, I think they are relatively easy to read and should be helpful to understand the problem. I'd prefer leaving them in.
3. Sorry about the newline, that's an easy fix :)
4. Yeah, good point, I can add, though editing these text files automatically can be quite fragile.
5. It seems like we added both too much and too little :D If it's not a problem, I'll leave in the comments, and try to also add something about the github repository. It was just a bit confusing to me, sorry.

Do you know if someone could help us with this? There are too many deadlines, too many things that are on my plate and I'm afraid this will fall off. I'd really appreciate some help :)

[hansjoergschurr]

I am happy to do the changes, and should be able to push to this pull request.
We are currently in the process of finishing up this years release and then I will come back to it.

[hansjoergschurr]

I finally got around to do the edits. Since the benchmarks contain (as const I will not merge the the benchmarks, but mark them with a tag.

[msooseth]

That’s awesome! Thank you so much! I’ll be at CAV so I’ll try my best to repay the favour with dinner&drinks sometime :) Thank you so much! See you at CAV hopefully, Mate

…

On Thu 20. Jun 2024 at 11:12, Hans-Jörg ***@***.***> wrote: I finally got around to do the edits. Since the benchmarks contain (as const I will not merge the the benchmarks, but mark them with a tag. — Reply to this email directly, view it on GitHub <#7 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXYLY5C4MPY6U732ZMHQH2LZILWONAVCNFSM6AAAAABFJBVZ6OVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCOBQHE2DQOBUGQ> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[hansjoergschurr]

I will unfortunately not be at CAV, but I think Mathias will be. He does a ton of work on the benchmark that is a bit less submitter-visible. I am happy to forward my drink to him ^^.

[msooseth]

Haha, okay, Mathias it is!

[barrettcw]

@msooseth - sorry to hijack this thread, but I sent an email to your gmail that is kind of urgent - could you have a look? Thanks!

[msoos]

Oh, I'm so sorry. I had a look but couldn't find an email from you :( Can you please re-send it? My address is a bit confusing, it's [email protected] (and not mate.soos@)

Sorry again,

Mate

[barrettcw]

Just resent to your gmail. Maybe check spam? It's from [email protected]

[msooseth]

@hansjoergschurr was this merged in the end? Or is there something I can do to help merge it?

[msooseth]

Actually, sorry, I see it hasn't been merged, but "only" because of the as const. Is that support coming to SMTLib sometime?

[barrettcw]

Yes the support for const arrays should be coming soon - it's on my to-do list

[msooseth]

Nice! Thank you, that'd be awesome!