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

[Sorawee Porncharoenwase]

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/20210821/7bdc0f8f/attachment.html>