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

[Sorawee Porncharoenwase]

>
> 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/20210820/ad1a9bc7/attachment.html>