(simplify, reduce-invertible, default) Soundness bug on QF_BV formula (assert (= (bvnand a (bvnand b b)) a))

[muchang]

Hi,
For this case, Z3 gives an incorrect answer:

[527] % z3-4.8.5 small.smt2
unsat
sat
[528] % z3-4.8.6 small.smt2
unsat
sat
[529] % z3-4.8.7 small.smt2
unsat
sat
[530] % z3-4.8.8 small.smt2
unsat
sat
[531] % z3release small.smt2
unsat
sat
[532] % 
[532] % cat small.smt2
(declare-fun a () (_ BitVec 1))
(declare-fun b () (_ BitVec 1))
(assert (= (bvnand a (bvnand b b)) a))
(check-sat-using (then simplify reduce-invertible default))
(check-sat)
[533] %

OS: Ubuntu 18.04
Commit: d6ad371

[NikolajBjorner]

please stop filing fuzz bugs for the next few weeks until they can be addressed.

[aniemetz]

@muchang I'm seriously wondering why you don't make your tool publicly available. I would consider this a far more valuable contribution to the SMT community (since we SMT solver developers could then use the tool to continuously test our solvers for robustness) than filling up issue trackers on GitHub.

[zhendongsu]

please stop filing fuzz bugs for the next few weeks until they can be addressed.

Okay, Nikolaj, a few weeks is an awfully long time, but we'll do as instructed, and only try to find bugs in secret :)

[zhendongsu]

@muchang I'm seriously wondering why you don't make your tool publicly available. I would consider this a far more valuable contribution to the SMT community (since we SMT solver developers could then use the tool to continuously test our solvers for robustness) than filling up issue trackers on GitHub.

That is definitely our eventual plan, and we are working toward that to make the tools robust and usable by others before we do so. Please stay tuned! That being said, it is also a lot of fun in finding and reporting bugs :)

[aytey]

@zhendongsu are you aware of the arrogance that you and your team display in requesting that @NikolajBjorner /et al./ fix bugs in things for which you are not even the consumers?

For example:

• Soudness bug on QF_S with regex  #4376 (comment) -- I presume here you're not writing tools yourself that use strings?

• Invalid model for QF_FP formula  #3794 (comment) -- I presume you're also not writing tools yourself that use FPs?

My interpretation here is that you're requesting that Nikolaj fix stuff so that a) it makes it easier for you to find new bugs which aren't duplicates (because doing the de-duplication is too hard for you to automate) and b) so you can increase your "genuinely found" issue count (even though these issues are totally fabricated).

As someone who uses Z3/Boolector/STP/CVC4 1000s of times a day (in commercial usage, and where I personally contribute back to the development of all four of these tools!), I would much rather that issue trackers such as these are full-up with issues that real users find, than the ones you derive from the SMT-COMP instances.

¯\(ツ)/¯

[zhendongsu]

@andrewvaughanj We are sorry that you felt that way. Like for compilers such as GCC/LLVM, we believe that SMT solvers are foundational tools and thus hope to help make them more reliable, robust, and usable in ways with which we are more experienced. Also, like any other software systems, we feel that they could benefit from user applications and testing, and could also benefit significantly from automated testing, like the work by John Regehr's group and mine on testing compilers.

In any case, our goal is to try to contribute something meaningful to great tools like Z3 and CVC4 by finding/reporting bugs in them, and by developing automated testing tools (and other accompanying tools that we also hope to build) that could be used by solver developers in the future.

[aytey]

So, I think we need to be honest here: you are not testing what is ostensibly a commercially-backed tool like you were with clang; you are testing two (or more!), open-source and academic-led research tools -- and your approach to this testing is not "kind", but "brutal and unforgiving".

When you were raising bugs against clang, where you @ing Chris Lattner and demanding fixes to your issues, such that you can start discovering your next set? You only want these issues fixed so you can find your "next batch", not because you've building something awesome that needs this "broken" functionality. The view from the outside perspective here is that, because you are dealing with academics, they should "roll over" and just resolve whatever asinine bugs you find.

What you might be forgetting is that is Z3 is a tool, which, for the most part, exclusively used by experts. This means that it is highly unlikely that a user would ever intentionally say "my problem is finite domain (QF_FD) and then go and use unbounded integers in the instance". While these kind of cases might be "a lot of fun [to] find[] and report[]", it is highly unlikely that they reflect the real-world usage of Z3.

To put this into the clang analogy, this is like saying "when I use clang and specify -march=mblaze and then try to use use -msse4.2, clang doesn't behave". I mean, yeah, no surprise, you're trying to do two things that are completely orthogonal and shouldn't be used together. It is very much a case of "play stupid games, win stupid prizes".

The academic teams working on these tools are funded by grants to "push forward" the state of the art in SMT reasoning -- they are not paid to engineer robust tools that work in 100% of circumstances. Your approach to finding these edge-cases which are unlikely to reflect real-world usage does not make your approach seem impressive, it just makes your team seem petty. Also, for any issues that might be a segmentation volition or use-after free---which, don't get me wrong, aren't ideal---really don't have much an impact -- no-one is using Z3 like a server where an exploit matters. Probably the only place where Z3 is web-accessible is rise4fun, and I bet that MSFT have a lot of engineering in place to ensure that trivial crashes aren't exploitable.

Reading your paper you state that the code to do this is only "1,032 lines of Python 3.7 code" -- so what's stopping you just releasing this? It is 1000 lines; just release it is as is, and then fix your "robustness" issues when people fuzz your tools and find bugs! Unless you're following a mantra of "do as I say, not do I do" ...

The benefit to "humanity" that you and your team would provide could be greatly increased if you released, and documented, your approach for finding these bugs rather than continually hammering GitHub with the outputs. Imagine if rather than realising clang, Chris had just kept it as a private tool that he ran against the Linux kernel and continually said "that code is wrong!" to Linus? That provides very little benefit to anyone.

Undoubtedly, Nikolaj has been under a lot of pressure to placate you and the issues you've found and, for that, I commend him. However, judiciously reading the Z3 issue tracker like I do, it certainly feels that your efforts have been for the worse. We have seen Nikolaj remove features from Z3 because you've found bug in low-usage code -- who knows what "real world" usages you've undone in finding weird edge-cases no-ones ever found before (again, because they're experts and don't do silly stuff).

Furthermore, it also feels like the number of genuine users (1, 2) who are experiencing issues has dramatically increased since your work started -- I personally wouldn't call it an accomplishment that I put Nikolaj and others under so much pressure to fix things that the project I was testing got worse.

Oh, but I hear you say, we test soundness too! Well, no, you use Z3's model_validate option to see what happens -- a technique that Nikolaj has already told you is not complete. If you really cared about soundness, why are you not "cross validating" the results from Z3 against other solvers? Take the model, assert it back, and then run it against CVC4, or STP, or Boolector -- then if the alternative solver said "this is incorrect", it would be a lot better than finding potential false positives in Z3's model validation.

For anyone else who has got here, I am not the only one who feels like this: see impassioned Twitter thread by @martin-cs (one of the CVC4 developers).

[NikolajBjorner]

There are many sound points above I haven't read them in detail.

The incredible work by the fuzzers is very much appreciated.
It has helped progress the new arithmetic solver and uncover many serious bugs.

All soundness bugs are taken seriously (including this one).
They could affect users even if filed by a fuzz tool.
The fuzz tools are very diligent at finding such bugs and appear to offer a much
better test coverage than running simple regressions or SMTLIB2.
As many fuzz bugs are in corner cases that are not exercised by users
(I have seen a bvnand or nand bug somewhere before).

It is/was never claimed that z3 is bug free, but best effort is made to fix issues.

User bugs have to take priority: when users rely on some functionality for their tools it is a blocker if it isn't working. I try to be responsive on these issues.

Usability bugs (crashes during proof mode, cancellation) would be nice to fix.
At some point the question of "business justification" comes up.
I am not sure some of these matters to anybody.
User tools cold have workarounds in cases I am aware of.
(it limits the test matrix for a tool that cancels z3 to start from scratch).

Right now, I am overhauling regexes. This requires my full attention and I cannot possibly spend 6 hours of each day going over fuzz bugs. The regex work will deal some previously reported soundness bugs as well. I simply have to turn off this mode of working with fuzz bugs on a daily basis for some weeks, otherwise I cannot finish this work in a reasonable way.

Some wishful thinking:

• It is great when bug reports are grouped according to what feature they are finding bugs in. These are almost for sure duplicates.
• Submit regression unit test for https://github.com/z3prover/z3test
• Localize and even submit fixes for simple bugs that can be addressed (some of these bugs are pretty basic and require no deep understanding of internals).

[kuldeepmeel]

Z3, along with the other state of the art SMT solvers (CVC4, STP, Boolector, Yices, Beaver to name a few), has allowed rest of us to pursue research at the frontiers that would have been unthinkable about a decade ago. In this context, the time of the researchers behind Z3 is of prime importance for the rest of us. The cost of these fuzzing bugs on the research community is real, and I have personally experienced the valuable research time slipping away from Nikolaj’ hands while fixing these issues, and I kind of decided to hold off sending emails to Nikolaj about some potentially mutually interesting research ideas until he finds time to breathe from fixing these bugs. And I am sure I am not the only one here who is ruing the time of the developers of Z3 and CVC4 developers that is being robbed away from the rest of SAT/SMT community.

Some of these bugs remind me of my experience of maintaining ApproxMC (a tool for model counting) where there was a corner case that I hadn’t bothered to handle — outputting zero if the underlying formula is UNSAT. And someone kept pestering me if I could output zero rather than just exiting with some error. And I had to flat out refuse by saying that I am not interested in counting the number of solutions of UNSAT formulas and if that’s what fancies you, go and do it!

While acknowledging that fuzzing is a wonderful tool, there is always a need for cost-benefit analysis. Not every bug is worth fixing.

[zhendongsu]

@NikolajBjorner
Thank you for the incredibly kind, appreciative words on our work, Nikolaj; these meant very much to us! Developing and maintaining an important tool like Z3 demand a lot of time and devotion; thank you, as well as the other contributors!

@andrewvaughanj
We just wish to comment very briefly. First, you must have confused us, in particular, @wintered (Dominik Winterer) and @muchang (Chengyu Zhang), with @rainoftime, as the two issues that you referred to in your comments were from @rainoftime, not us. There are several concurrent fuzzing efforts; we do not want to take unnecessary blames (nor credits) for other people's work.

Second, we value and appreciate developers' time and effort. In fact, we spent an enormous amount of time reducing our tests, and separated them into soundness issues, genuine invalid model issues, model validation errors, crashes, performance issues, etc. We still, inevitably, made some unintended mistakes, and reported duplicates, some minor issues, etc.

Third, as I mentioned in an earlier comment, we do plan to release our tools to be used by solver developers when they are cleaned up and ready. Building a strong testing tool is also an iterative process that takes time and effort, and we learn how to refine/extend it by finding and reporting bugs. We believe that a tool that cannot continuously find interesting bugs would not be very useful.

Thank you for this discussion. I hope everyone works together to make fantastic tools like Z3 as widely-used as possible.

[kuldeepmeel]

@zhendongsu

I apologise for pressing you further on the issue of public release of your tool but I feel your response above and on twitter has been less than satisfactory. I have anyway built a negative reputation of pressing people too much for source code release, so I guess I will take the liberty once again.

AFAIK, the paper is accepted and slated to be published at PLDI in 3 weeks, therefore it is reasonable for us to expect that you will release the artifact by the publication date. There are two benefits to release of artifact: it allows developers immediate access so that they don’t have to context switch. Right now, you are letting SMT developers access your fuzzing tool 5 times a day and that also via an incredibly inefficient asynchronous mode of communication (Github Issues). Secondly, if we find that the fuzzing tool mostly finds useless things — SAT/SMT community can use its expertise to develop better fuzzing tool.

As a lot of us have indicated above, all these fuzz reports have a real significant cost, and given that Nikolaj has explicitly mentioned that he is working on incredibly challenging task of handling regexp, it is perhaps better for your team to focus on making sure the tools “are cleaned up and ready.” Surely, one can’t expect Z3 and CVC4 developers to spend tens or hundreds of hours to even get fuzzing tools to be publicly released — release of open source version of tools is expected in SAT/SMT community if one wants to merely participate in competitions.

Given that your response above and on twitter seems to highlight that you are focused on doing things better than other competing efforts, I think if you take the lead in releasing the tool, others may be forced to do the same. Well, you can expect me to lurk on these forums and point to the release of your code.

[fuzzilla]

@muchang I'm seriously wondering why you don't make your tool publicly available. I would consider this a far more valuable contribution to the SMT community (since we SMT solver developers could then use the tool to continuously test our solvers for robustness) than filling up issue trackers on GitHub.

That is definitely our eventual plan, and we are working toward that to make the tools robust and usable by others before we do so. Please stay tuned! That being said, it is also a lot of fun in finding and reporting bugs :)

It would be good to publicly release this and other bug finding tools you've developed.

[meng-xu-gatech]

I think beyond finding more bugs with fuzzing, maybe we can use it for parameter tuning?

For example, I am looking at the script from CVC4 for the SMT-COMP 2020. The developers have manually coded many rules to try on per each logic and I can see a lot of craftsmanship in this script.

At the same time, I also noticed that each rule is basically turning certain knobs on and off, which is sth fuzzers are extremely good at. This makes me wonder whether we can use fuzzing to find and tune the parameters? Essentially, with fuzzers, we still generate SMT inputs as well as knob configurations. And now what we need is some feedback mechanism to drive the evolution on performance instead of bugs: i.e., what makes turning on a knob beneficial and what does not. The end result can be a script like the one mentioned before but automatically generated instead of manually crafted.

[yannickmoy]

you are testing two (or more!), open-source and academic-led research tools

@andrewvaughanj I'd like to disagree with the above presentation. Tools like Z3 and CVC4 are also heavily used industrially. For example, like we do in SPARK, but we're not the only ones, see this keynote at FLoC in 2018 by Byron Cook from AWS. He talks of 10s of millions of calls to Z3 and CVC4 per day, for a given customer-facing service.

they are not paid to engineer robust tools that work in 100% of circumstances

In fact, even engineers developing critical robust tools (like our compilers and verifiers) can't afford to fix bugs that don't matter. Obscure crashes on illogical source code using combinations of features that are unheard of in real life (this can be combination of tool switches or code features). The key here is to separate critical issues (miscompilation for a compiler, soundness for a verifier) from less critical ones. Sure, if we had infinite time and money, it would be great to fix all obscure crashes, but we don't.

In the Twitter thread you pointed at, Clark Barrett also points out a very important distinction regarding soundness issues in provers: wrongly saying "unsat" is far-far-far more critical than wrongly saying "sat".

As a heavy user of SMT solvers in our tools, which in turns are used by all our industrial/community users, I really value the increase in quality and confidence that we get from bugs being reported by researchers and fixed by developers of SMT solvers, but I strongly encourage the researchers to engage more with the developers to find bugs that matter.

[aytey]

@yannickmoy I think you missed the bit where I already said I'm an industrial user ... at Vector, I lead a team that develops a product on top of SMT for symbolic execution. What we build supports, builds and ships Z3/Boolector/STP/CVC4 on Win32/Win64/Linux32/Linux64, and I have personally contributed back to all four of these tools as part of my employment (and also, in some instances, for pleasure).

I originally said "1000s" of queries a day, but if I consider our incremental usage, it more likely to be in excess of 500,000s of SMT queries a day (we have a test-bed of around 10,000 files, each with, I'm guessing, 10 subprograms each, and if each subprogram generates 5 separate asserts -- now I've written this, I bet this is a low number).

This is also a tool that we ship and sell licenses for, so I cannot gauge the additional queries that users are generating when using our symbolic execution engine "in the field". So, indeed, correctness is also important to me!

Anyway, I think this bit:

I strongly encourage the researchers to engage more with the developers to find bugs that matter.

was the crux of what I was trying to suggest.

From reading the issues here, there seemed to be a lot of "throw it at the Z3 GitHub issue tracker and see what sticks", rather than trying to: a) triage these bugs internally, b) do some manual de-duplication, c) make suggestions towards the fixes, d) not "demand" fixes for features for which they are not the end users.

Point d) is the most important bit here; there were requests from "the fuzzers" to fix issues found, purely so they could start raising new bugs without the fear of them getting closed as duplicates -- and even just closing those as duplicates takes time from Nikolaj.

I am certain that real, genuine bugs have been found via the fuzzing efforts here, and that is genuinely great. I just think that there becomes a point where we, as a community of SMT developers and users, need take a step back and decide on the cost-to-benefit ratio -- what are we missing out on (e.g., Nikolaj's improved regex work) because he is "spend[ing] 6 hours of each day going over fuzz bugs"?