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

[Sorawee Porncharoenwase]

Two more bugs:

- https://github.com/dafny-lang/dafny/issues/1372
- https://github.com/dafny-lang/dafny/issues/1373

The latter one is not discovered by fuzzing itself. I was writing a type
constraint to be put in the fuzzer, and thinking what will happen if we
violate the constraint, so I tried it out manually and discovered the issue.

On Sat, Aug 21, 2021 at 7:53 PM Sorawee Porncharoenwase <
sorawee.pwase at gmail.com> wrote:

> 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 at 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
>>> infrastructure?
>>
>>
>> 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.
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </listarchives/xsmith-dev/attachments/20210822/ebec2424/attachment.html>