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

Re: [xsmith-bugs] Formal parameters created by lambdas not used for creating references

On Sun, Jan 31, 2021 at 01:43:03PM -0800, Danila Fedorin wrote:

First of all, thank you for all your work on Xsmith. It's an incredible

I've run into an issue while trying to create a fuzzer for a small,
Haskell-like language. It appears as though the version of xsmith available
via `raco` does not contain some of the canned components found in the
Xsmith repository

Yeah, the git version is always getting new features.  We will probably
do a new release reasonably soon.

, so I opted to define the components myself, drawing
heavily on LambdaSingleWithExpression. I also defined a VariableReference
equivalent, and basic arithmetic. However, running Xsmith, I was
consistently met with an error like the following:

   xsmith: internal error -- no destinations for lift from:
XsmithAstHoleExpression, type: #<number>, depth: 2

I run into a similar issue when using purely canned components such as
LambdaWithExpression and VariableReference. That is what makes me suspect
that this is a bug.

I've just pushed an improvement to the documentation here, because
looking at it again it's not very clear on this point.  If you have
reference expressions, Xsmith practically needs to assume that the top
level node has some `Definitions *` field where it can reliably lift
references if all else fails.

From what I understand, whenever a reference node is created, Xsmith
attempts to fill it with a visible variable of the same type, and if none
is found, it attempts to "lift" the new reference, adding it to an existing
definition. Lambda functions cannot be "lifted" to (since doing so would
change the function's type); this leaves no constructs in my small language
to serve as lift targets. However, I don't think this should be an error.
The debug log mentions concretizing various "arg"s (formal parameters of
the Lambda) to be of type #<number>:

   Concretizing binding def1.  Type: #<type-variable #f>, concretized to:
   Concretizing binding arg2.  Type: #<type-variable #f>, concretized to:

This leads me to believe that they are suitable to fill a reference of type
#<number> (as reported in the internal error). However, this never occurs,
and I get "no destinations to lift from" as soon as Xsmith picks a
reference. This seems to make it nearly impossible to define a language in
which lambda functions are the only source of binding. My suspicion that
this is a bug is further corroborated by the fact that the lambda functions
generated by the "Canned Components" example from the manual overwhelmingly
ignore their arguments. Out of 20 lambda functions generated from 4 runs of
the fuzzer, only 2 used their argument, while the others created and lifted
a new reference.

Xsmith has a very conservative effect analysis that makes references
more difficult in the face of higher order functions.  It could be the
problem.  Last week I've just been improving that analysis so that
Xsmith can always choose function parameters as references, but that
code is not actually in the master branch yet.  I'll merge it this
week, probably today.

With that change maybe this would work?  If I can see your code and
try running it I'll know for certain.  It could be an unrelated bug,
in which case I would also like to see your code if possible.

Also, saliently, the default `reference-choice-info` property always
allows lifts, and can always pick them with some probability.  It
could be that every program you generate unfortunately picks a lift
somewhere in the program each time instead of using a visible
reference.  You can write your own function to pick a binding that
never lifts.  Actually, there is another improvement in the same
not-yet-merged branch that improves the situation for when no binding
is possible, so your fuzzer will probably work a lot better with the
git version.

I hope I'm not missing something obvious.

Thank you in advance,

I hope this helps!

William Hatch