[xsmith-dev] XSmith questions

[Sorawee Porncharoenwase]

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 at 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 at 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 at 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 at gmail.com> wrote:
> >> >> >
> >> >> >> As always, thanks! :)
> >> >> >>
> >> >> >> On Fri, Jul 30, 2021 at 5:29 PM William G Hatch <william at 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
> >> >> >>>
> >> >> >>
> >> >>
> >>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </listarchives/xsmith-dev/attachments/20210829/cd9518d9/attachment.html>