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

Re: [xsmith-dev] XSmith questions

I feel like this should be easy, but somehow the solution eludes me...

An array in Dafny must be allocated and then stored in a variable as a part of the array declaration statement (essentially, there's no array literal). The variable can then be used freely in any _expression_ position. However, the fact that the allocation is a statement means that in function _expression_ (which can't have any statement), the only way to get an array value in is through parameters. In particular, there is no lifting target of array type inside function expressions.

How should I deal with this situation? Is it possible to create a new kind of variable reference that "tries" the array type, and use stuff like xsmith_get-reference-for-child! to see if there is a lifting target, and if there's none, then try other types (say, integer) that are guaranteed to have a lifting target instead? That doesn't seem possible since the type of the node seems already predetermined by the time fresh is invoked.

On Mon, Aug 23, 2021 at 10:06 AM William G Hatch <william@hatch.uno> wrote:
I agree this is too bad.  But I'm sorry to say that I'm not going to
improve this right now.  It would require fairly major work in the
type unification machinery.  The workaround is maybe not the best, but
it's at least pretty easy to do.

On Mon, Aug 23, 2021 at 12:12:38AM -0700, Sorawee Porncharoenwase wrote:
>I want to express a type constraint that it’s either a product type of
>length 0, 2, or 3. Is there a way to do that? fresh-type-variable with
>arguments seems like a solution, except that the composite type isn’t
>allowed to be repeated. Usually, if I have a generic type of the same
>arity, I can simply push fresh-type-variable in. E.g.,
> (immutable (array-type ...))
> (immutable (set-type ...)))
>(immutable (fresh-type-variable (array-type ...) (set-type ...)))
>The problem is that product-type‘s argument is a list of types of false, so
>fresh-type-variable doesn’t work there.
>I guess I can create generic types product0, product2, and product3, and
>put them in fresh-type-variable, but well, I really want to avoid doing
>On Fri, Jul 30, 2021 at 5:35 PM Sorawee Porncharoenwase <
>sorawee.pwase@gmail.com> wrote:
>> As always, thanks! :)
>> On Fri, Jul 30, 2021 at 5:29 PM William G Hatch <william@hatch.uno> wrote:
>>> On Fri, Jul 30, 2021 at 03:32:54PM -0700, Sorawee Porncharoenwase wrote:
>>> >> When I've had this situation, as a workaround, I've just made a
>>> >> function that returns a fresh-type-variable with all of the supported
>>> >> base types and maybe some constructed types.  It's... not great.
>>> >>
>>> >
>>> >My question is, say, I want to disallow a function, a list of functions,
>>> a
>>> >list of list of functions, a list of list of list of functions, and so
>>> on.
>>> >Of course, I can express things positively: it's an int or bool or
>>> >listof... what? A list of fresh-type-variable runs a risk of choosing
>>> >function type. So I could do a listof (int or bool or listof ...) for
>>> >another level, and keep increasing levels. Is this what you have in mind?
>>> Yeah, that's the problem with it.  You can realistically only specify
>>> a small set of the infinite set of constructible types (granted in
>>> practice the set of types usable by xsmith is bounded as well since it
>>> bounds the tree depth of constructed types).  But specifying that list
>>> is a chore and you probably get poor performance if you actually try
>>> to generate many combinations with constructed types.  So in practice
>>> when I have this situation so far I just... don't generate as many
>>> things as I otherwise could.
>>> >> However, that feature just hasn't made it to the top of my priorities
>>> >> yet...  Sorry :(
>>> >>
>>> >
>>> >No worries at all! If there's anything that I can help regarding this
>>> >feature, let me know. It looks like the representation of a type right
>>> now
>>> >consists of a lower bound and an upper bound, and probably this feature
>>> >will require changing the representation, correct?
>>> The upper and lower bounds are about subtyping.  If a type changes
>>> through unification it can affect the types connected as upper/lower
>>> bounds.  This feature shouldn't change that, other than being more
>>> information that will be conveyed to the related type variables.  When
>>> a variable is constrained by unification to remove a type from its
>>> allowed list, all related types in its upper/lower bounds lists also
>>> remove that type.  Eg. if variable A is (or string int (-> int int))
>>> and variable B is (or (subtype-of string) (subtype-of int) (subtype-of
>>> (-> int int))) and variable A is constrained to definitely not be a
>>> function, variable B could no longer be a function and still be a
>>> subtype of A.  If two variables are unified with `unify!` instead of
>>> `subtype-unify!` (or equivalently by being `subtype-unify!`ed in both
>>> directions) they are more or less merged into a single variable.  (IE
>>> the object that you get from `fresh-type-variable` can be merged with
>>> others and they are always canonicalized before doing anything to
>>> them.)
>>> Right now a type variable has a list of possible types (or #f for
>>> unconstrained).  The list can have any number of base types and every
>>> compound type, but it's limited in that it can only have one of each
>>> compound type (though each compound type may have type variables
>>> inside and thus represent potentially many types).
>>> I think the needed change would be to add a list of disallowed types.
>>> I think this list should probably be applied recursively -- IE it
>>> should be pushed to child types.  So eg. if you disallow function
>>> types in a type variable it also disallows lists of functions, etc.
>>> I'm not certain if there are exceptions, though.  Would it make sense
>>> to have a recursive and non-recursive version of this?
>>> At any rate, when checking if things `can-unify?`, you would use the
>>> disallowed list as well as the allowed list of both variables to
>>> determine the outcome.  When variables are unified, they need to
>>> propagate their disallowed list to related type variables (IE the ones
>>> in the upper/lower bounds lists).
>>> Another thing that would need to be worked out is what exactly to
>>> store in the disallowed list.  Constructors for compound types?  Or
>>> maybe predicates?  Probably base types and predicates is my guess.
>>> At any rate, since we keep emailing about the issue I've thought
>>> through more of it than before, so now I'm much more likely to
>>> actually sit down and do it soon. :P