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

Re: [xsmith-dev] XSmith questions



Nope, no global variables.

I’m not sure if the ability to exclude types will help in this case. Consider the following pseudocode

function f(x : int): int {
  len(list(hole, hole))
}

method main() {
  declare a: array();
  declare b: array();
  print list(a, b);
}

The problem occurs when hole has type array, because there is no lifting target. But also consider:

method main() {
  declare a: array();
  declare b: array();
  function f(x : int): int {
    len(list(hole, hole))
  };
  print f(1);
}

In this case, hole can be a variable referencing a and b. And also:

function f(x : array): int {
  len(list(hole, hole))
}

method main() {
}

In this case, hole can be a variable referencing x.

It sounds like you are suggesting that I exclude array. But what does that mean? I definitely don’t want to exclude a list from having an array as an element, because that works just fine in method, and even in functions that do have an access to an array variable.

If we don’t care about completeness, I guess we can have two variants of _expression_, where one is to be used in method, and another is to be used in function. _expression_ that is to be used in function would not allow array anywhere at all. E.g., an element of a list cannot be array. But that sounds really not ideal.

I think I have a temporary solution, but it’s really hacky. I will disallow top-level functions in the grammar. Because the Main method has a list of declarations at the top, I can post-process them by randomly picking some lambdas and lifting them up to top-level functions, as long as they don’t transitively need an array declaration.




On Fri, Aug 27, 2021 at 5:29 PM William G Hatch <william@hatch.uno> wrote:
As hinted in my other reply, the best answer would be that Xsmith type
variables have a list of types that they can't be in addition to their
list of possible types.  Then you could test whether it is possibly,
definitely, or definitely not a given thing, and if you make a choice
that it isn't something you can specify just that without removing
other flexibility later.  But since that feature still doesn't exist,
I don't have a great answer.  Sometimes in situations like this I punt
to concretizing the type.  It removes flexibility for later choices,
but lets me make a clear decision about the type now (without forcing
all unconstrained variables into the same choice).

On Fri, Aug 27, 2021 at 02:25:38PM -0700, Sorawee Porncharoenwase wrote:
>So, this is actually another question that I meant to ask. I have this code
>as a choice method for choice-filters-to-apply:
>
>[VariableReference
>  (λ ()
>    (define t ($xsmith_type (current-hole)))
>    (define method? (can-unify? t (method-type (fresh-type-variable)
>(fresh-type-variable))))
>    (cond
>      [method?
>       (and (parent-node (current-hole))
>            (equal? (ast-node-type (parent-node (current-hole)))
>                    'ProcedureApplicationForMethod))]
>      ;; we are generating default return values.
>      ;; at this point, there's no lifting target, so we can't have
>      ;; variable reference
>      [(and (parent-node (current-hole))
>            (equal? (ast-node-type (parent-node (current-hole)))
>                    'TopLevelMethod))
>       #f]
>      [else #t]))]
>
>I raised a concern earlier that can-unify? is not ideal because
>
>($xsmith_type (current-hole))
>
>is sometimes unconstrained, meaning it rejects more than it should, and you
>agree with that. What’s the right way to do this properly?
>
>
>On Fri, Aug 27, 2021 at 2:10 PM William G Hatch <william@hatch.uno> wrote:
>
>> In Dafny do function expressions not generate closures?
>>
>> My first thought is that you can add a choice filter (with
>> choice-filters-to-apply, defined probably with add-choice-method) that
>> disallows expressions that need an array type unless there is a
>> variable already visible or its in a context where it can lift one.
>>
>> > function _expression_ (which can't have any statement)
>>
>> As an aside, I hate languages that do this...
>>
>> On Fri, Aug 27, 2021 at 02:33:59AM -0700, Sorawee Porncharoenwase wrote:
>> >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.,
>> >> >
>> >> >(fresh-type-variable
>> >> > (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
>> >> >this.
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >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
>> >> >>>
>> >> >>
>> >>
>>