[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [xsmith-dev] Early Dafny Results (Re: XSmith questions)

Two more bugs:

- https://github.com/dafny-lang/dafny/issues/1365
- https://github.com/dafny-lang/dafny/issues/1367

On Fri, Aug 20, 2021 at 2:07 PM Sorawee Porncharoenwase <sorawee.pwase@gmail.com> wrote:
Are these 4 bugs or 6?  Or is it uncertain whether the two comment
links are separate bugs?

I would count it as 6. For example, https://github.com/dafny-lang/dafny/issues/1359 and https://github.com/dafny-lang/dafny/issues/1359#issuecomment-902594485 are obviously very related to each other, but the operations are different (membership vs disjointness) and the bug occurs in different set of compilers (C# and JS vs only C#).

As an aside, I recently wrote a built-in minimizer.  I haven't really

Yes, I successfully hooked it up last week, though eventually I still need to read the code to understand the problem and minimize it further.
Also, I'm curious to hear about your testing setup.  Are you using any
of our harness repository tools, or did you set up your own

I didn't use the harness repo. One reason is that we are doing verification fuzzing, which requires it to run a generated program, then correlate the output with source location, then modify the AST, and run the modified program. This means the standard workflow doesn't quite work. We use AWS Batch as the environment to run the fuzzer, which is packaged in a Docker image.
How much have you been running your fuzzer (ballpark approximation)? 

350000 programs per day. This is the number that I computed for Zvonimir a while back, so it might have changed.
Have you spent much time doing things like adjusting weights? 

Nope, not at all.
How big is your fuzzer (eg. LOC)?

My actual fuzzer is about 1KLOC (this is not pure Xsmith -- I defined some macros to make adding some constructs more concise). But there are other files too. The oracle is about 200LOC. The pretty printer is about 300LOC (I implement pretty printer separately, since I want to be able to perform tree surgery from the output of Xsmith). The output-source location correlation is about 300LOC.