[xsmith-dev] XSmith questions
Sorawee Porncharoenwase
sorawee.pwase at gmail.com
Thu Jul 15 21:09:13 MDT 2021
Yes, this is very helpful. I will let you know if I encounter any further
issues after updating XSmith.
By the way, do you want any help with Scribble? I notice a lot of typos and
link errors and can submit PRs to fix them.
On Thu, Jul 15, 2021 at 8:00 PM William G Hatch <william at hatch.uno> wrote:
> Sorry for the delay. I wanted to do the debugging before responding,
> but then I didn't get to it for a while.
>
> Anyway, I now see what's going wrong, and I've fixed some bugs.
>
> First, that issue with the bud-node was a bug in the `edit` property
> which the canned-components `ProcedureApplication` uses. It's fixed
> now.
>
> >> Hmm, it seems like first-order functions would be encoded as a
> >> function application node that only allows a reference as its RHS
> >> rather than allowing arbitrary expressions. But that said, I'm not
> >> sure I fully understand what you're trying to do.
> >>
> >I’m not sure what you mean by that. But:
>
> Erm, I misspoke (mistyped) a bit. I meant that it would be function
> application that only allows a reference in the procedure position. I
> don't know why I wrote RHS.
>
> Anyway, the strategy of having separate definition nodes for functions
> and everything else is used in Cish. I don't recommend following
> anything Cish does. However, it accomplishes this by having the
> program node have non-function definitions first, and disallowing use
> of functions on the RHS of those functions.
>
> The problem where it can't find a reference is a bug (that I haven't
> fixed yet) caused by the lifting mechanics not really being completely
> in sync with the reference mechanics with respect to nodes that have
> multiple definition fields. When there are multiple definition
> fields, definitions in the lower field can reference the definitions
> in the higher field, but not vice versa. The lifting machinery
> doesn't know about that ordering, it just stuffs the lifted definition
> into the front of the definitions in whatever field it is targetting.
> Thus it places a definition in a place that the reference machinery
> thinks is out of scope.
>
> So... if you want to have different binders that get different fields
> in the program node you can only make it work if you disallow stuff to
> be sure you never need to reference something that will be lifted into
> the lower field.
>
> That said, I've just fixed some issues to allow definition nodes to be
> subtypable, so now you can have a definition node that is a subtype of
> Definition, but has some different rules. Importantly, though, it can
> be lifted to the same field.
>
> Eg. if I change the MyDefinition declaration in your example to look
> like this:
>
> ```
> [MyDefinition Definition ()
> #:prop fresh (hash 'Expression (make-hole
> 'ProcedureApplication))]
> ```
>
> It can now be lifted among normal definitions, but always have
> ProcedureApplication as its RHS.
>
> However, I'm still not convinced that you actually want
> ProcedureApplication as the RHS. Maybe you want to restrict lambda
> nodes to only be generated on the RHS of a FunctionDefinition node
> (that's a subtype of Definition), and make FunctionDefinition always
> have a Lambda node as its RHS.
>
> There is an example in the documentation that is like this, in the
> explanation of the `choice-filters-to-apply` property. But I'll paste
> it here:
>
> ```
> (add-choice-method
> my-component
> no-lambda-except-global-def
> [#f (λ () #t)]
> [Lambda (λ ()
> (and (parent-node current-hole)
> (equal? (ast-node-type (parent-node current-hole))
> 'Definition)
> (parent-node (parent-node current-hole))
> (equal? (ast-node-type (parent-node (parent-node
> current-hole)))
> 'Program)))])
> (add-property my-component
> choice-filters-to-apply
> [#f (no-lambda-except-global-def)])
> ```
>
> You can use something like that to allow Lambda nodes to only be
> generated on the RHS of FunctionDefinition nodes, and define
> FunctionDefinition like MyDefinition above to always generate Lambda
> as its RHS, and I think it should work for a first-order language.
>
>
> >(Also note that I tried unify! these unrestricted type variables
> >with some concrete non-function type variables, but down the road, I get
> an
> >internal error about unification failure.). Perhaps I'm not supposed to
> >unify! inside add-choice-method?
>
> Well, probably not. Generally the only place you want to `unify!` is
> inside the type property in the function that determines child types
> based on the parent type. Inside that function you can `unify!`, but
> the unification needs to be consistent (IE not unified based on the
> result of `random`) OR the choice needs to be saved in a way that it
> can be looked up when that function is run again.
>
> The problem is that the choice method gets its type information based
> on a hole node that is later replaced, so the type is recomputed
> without necessarily consulting the type that the hole said it was.
> You should be able to constrain the type using unification if you save
> that type to re-unify it consistently later. But without seeing the
> exact error and code that generated it, I'm not 100% certain.
>
>
> > In the last email, I asked if lift-type->ast-binder-type could be used
> > nondeterministically in this manner, and my experience with it so far
> seems
> > to indicate no.
>
> I think this should work, barring the issues mentioned above about the
> lifting vs referencing bug when you have the different definition
> types in different fields. Adjusting your example to have
> MyDefinition as a subtype, and then only having a Definition field in
> MyProgram, random choice seems to work fine. But sometimes it
> generates gargantuan programs (that I kill before it finishes) because
> it keeps choosing MyDefinition, requiring a function application,
> which likely lifts a reference to a function, which might choose
> MyDefinition, etc, in a bad lift chain that generates bigger and
> bigger types.
>
>
> Anyway, does that all help?
>
>
> On Tue, Jul 13, 2021 at 02:55:10PM -0700, Sorawee Porncharoenwase wrote:
> >>
> >> Hmm, it seems like first-order functions would be encoded as a
> >> function application node that only allows a reference as its RHS
> >> rather than allowing arbitrary expressions. But that said, I'm not
> >> sure I fully understand what you're trying to do.
> >>
> >I’m not sure what you mean by that. But:
> >
> > 1. I have no problem with the definition site. That’s easy to deal
> with.
> > 2. I also have no problem with restricting function application. That’s
> > easy to deal with as well.
> > 3. The problem is primarily with a bare variable reference bound to a
> > closure value, which must only occur in function application. For
> example,
> > the following code is invalid.
> >
> >(define (f) (void))
> >
> >(define g f) ;; this is invalid
> >(define h (g))
> >(define a (list f)) ;; this is also invalid
> >(define b (f)) ;; this is ok
> >
> >I have been using choice-filters-to-apply to restrict variable references
> >whose type can-unify? with function-type that doesn't directly appear
> under
> >function application. But this is obviously not ideal because the filtered
> >nodes are mostly those whose type is totally unrestricted. So filtering
> >them would prevent them from being concretized to other non-function types
> >as well. (Also note that I tried unify! these unrestricted type variables
> >with some concrete non-function type variables, but down the road, I get
> an
> >internal error about unification failure.). Perhaps I'm not supposed to
> >unify! inside add-choice-method?
> >
> >That's probably a bug. “Lifting” is what I've called the situation
> >> where a reference is generated that causes a new definition to be
> >> added such that the variable is in scope at the use site. IE the
> >> binding is lifted from the use site to some outer node that contains
> >> definitions. `lift_X` is the name Xsmith gives to definitions that
> >> are created automatically in this way (which is ultimately most
> >> definitions). The exception is caused because somehow the lift ended
> >> up in a place where it wasn't actually in scope. That shouldn't
> >> happen. Anyway, if you point me to a version of a fuzzer that does
> >> this, I'll try to debug it.
> >>
> >#lang clotho
> >
> >(require
> > xsmith
> > racr
> > xsmith/racr-convenience
> > xsmith/canned-components
> > racket/string
> > racket/list
> > racket/pretty)
> >
> >;; We first define a basic component and add a bunch of expressions.
> >
> >(define-basic-spec-component somelisp)
> >
> >(add-basic-expressions somelisp
> > #:ProgramWithSequence #t
> > #:VoidExpression #t
> > #:AssignmentExpression #t
> > #:VariableReference #t
> > #:ProcedureApplication #t
> > #:IfExpression #t
> > #:ExpressionSequence #t
> > #:LetSequential #t
> > #:LambdaWithExpression #t
> > #:Numbers #t
> > #:Booleans #t
> > #:Strings #t
> > #:ImmutableList #t)
> >
> >(add-loop-over-container
> > somelisp
> > #:name Map
> > #:collection-type-constructor (λ (inner) (immutable (list-type inner)))
> > #:loop-type-constructor (λ (inner) (immutable (list-type inner))))
> >
> >(add-to-grammar
> > somelisp
> > [MyProgram #f
> > ([decls : Definition *]
> > [declsTwo : MyDefinition *]
> > [body : Expression])
> > #:prop type-info
> > [(fresh-type-variable)
> > (λ (n t)
> > (hash 'decls (λ (c) (fresh-type-variable))
> > 'declsTwo (λ (c) (fresh-type-variable))
> > 'body (fresh-type-variable)))]]
> > [MyDefinition #f ([type]
> > [name = (fresh-var-name "b_")]
> > [e : ProcedureApplication])
> > #:prop binder-info ()
> > #:prop type-info [(fresh-type-variable) (λ (n t) (hash 'e
> t))]])
> >
> >(add-property
> > somelisp
> > lift-type->ast-binder-type
> > [#f (λ (type) (if (zero? (random 2)) 'MyDefinition 'Definition))])
> >
> >;; Sometimes we have a type variable that is not concrete but needs to be.
> >;; Here we provide a list of options we can pick for an unconstrained
> >;; type variable.
> >(define (type-thunks-for-concretization)
> > (list
> > (λ()int-type)
> > (λ()bool-type)
> > (λ()string-type)
> > (λ()(immutable (list-type (fresh-type-variable))))))
> >
> >(define (somelisp-format-render s-exps)
> > (define out (open-output-string))
> > (for ([symex s-exps])
> > (pretty-print symex out 1))
> > (get-output-string out))
> >
> >(define-xsmith-interface-functions
> > [somelisp]
> > #:program-node MyProgram
> > #:type-thunks type-thunks-for-concretization
> > #:comment-wrap (λ (lines)
> > (string-join
> > (map (λ (l) (format ";; ~a" l)) lines)
> > "\n"))
> > #:format-render somelisp-format-render)
> >
> >(module+ main (somelisp-command-line))
> >
> >
> >> Probably something is going wrong in the `fresh` property. Have you
> >> changed that?
> >>
> >I don’t think so. See the code at the end of the email.
> >
> >> I should change that error message. Anyway, it seems to think there
> >> is no outer node that has a `Definition *` child that can be the
> >> target for lifting a definition. Generally this happens when you
> >> forget to have an outer Program node or something that can hold
> >> definitions.
> >>
> >I don’t think that’s the case, but I could be wrong.
> >
> >#lang clotho
> >
> >(require
> > xsmith
> > racr
> > xsmith/racr-convenience
> > xsmith/canned-components
> > racket/string
> > racket/list
> > racket/pretty)
> >
> >;; We first define a basic component and add a bunch of expressions.
> >
> >(define-basic-spec-component somelisp)
> >
> >(add-basic-expressions somelisp
> > #:ProgramWithSequence #t
> > #:VoidExpression #t
> > #:AssignmentExpression #t
> > #:VariableReference #t
> > #:ProcedureApplication #t
> > #:IfExpression #t
> > #:ExpressionSequence #t
> > #:LetSequential #t
> > #:LambdaWithExpression #t
> > #:Numbers #t
> > #:Booleans #t
> > #:Strings #t
> > #:ImmutableList #t)
> >
> >(add-loop-over-container
> > somelisp
> > #:name Map
> > #:collection-type-constructor (λ (inner) (immutable (list-type inner)))
> > #:loop-type-constructor (λ (inner) (immutable (list-type inner))))
> >
> >(add-to-grammar
> > somelisp
> > [MyProgram #f
> > ([decls : Definition *]
> > [body : SubProgram])
> > #:prop type-info
> > [(fresh-type-variable)
> > (λ (n t)
> > (hash 'decls (λ (c) (fresh-type-variable))
> > 'body (fresh-type-variable)))]]
> > [SubProgram #f
> > ([decls : MyDefinition *]
> > [body : Expression])
> > #:prop type-info
> > [(fresh-type-variable)
> > (λ (n t)
> > (hash 'decls (λ (c) (fresh-type-variable))
> > 'body (fresh-type-variable)))]]
> > [MyDefinition #f ([type]
> > [name = (fresh-var-name "b_")]
> > [e : ProcedureApplication])
> > #:prop binder-info ()
> > #:prop type-info [(fresh-type-variable) (λ (n t) (hash 'e
> t))]])
> >
> >(add-property
> > somelisp
> > lift-type->ast-binder-type
> > [#f (λ (type) (if (zero? (random 2)) 'MyDefinition 'Definition))])
> >
> >;; Sometimes we have a type variable that is not concrete but needs to be.
> >;; Here we provide a list of options we can pick for an unconstrained
> >;; type variable.
> >(define (type-thunks-for-concretization)
> > (list
> > (λ()int-type)
> > (λ()bool-type)
> > (λ()string-type)
> > (λ()(immutable (list-type (fresh-type-variable))))))
> >
> >(define (somelisp-format-render s-exps)
> > (define out (open-output-string))
> > (for ([symex s-exps])
> > (pretty-print symex out 1))
> > (get-output-string out))
> >
> >(define-xsmith-interface-functions
> > [somelisp]
> > #:program-node MyProgram
> > #:type-thunks type-thunks-for-concretization
> > #:comment-wrap (λ (lines)
> > (string-join
> > (map (λ (l) (format ";; ~a" l)) lines)
> > "\n"))
> > #:format-render somelisp-format-render)
> >
> >(module+ main (somelisp-command-line))
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </listarchives/xsmith-dev/attachments/20210715/5b1f0578/attachment.html>
More information about the xsmith-dev
mailing list