Thanks! Note that if concretization needs to call up these thunks
during printing it is because you still have unconstrained type
variables at printing time. That's not necessarily a problem,
exactly, but it might mean that thing is not really used.
On Wed, Jul 21, 2021 at 03:45:38PM -0700, Sorawee Porncharoenwase wrote:
>I submitted a PR that fixes the problem.
>current-xsmith-type-constructor-thunks needs to be parameterized for
>printing. Note that this is not only required by my fuzzer, but also by
>several example fuzzers that use type->string. I.e., standard-ml and cish.
>
>On Wed, Jul 21, 2021 at 3:08 PM William G Hatch <william@hatch.uno>
wrote:
>
>> The default-base-type should never show up in a fuzzer that has
>> defined the type property for any node. So this is definitely a bug.
>> I had the default-base-type show up once before, but some other change
>> made me stop seeing it, and I never got to the bottom of it. It's
>> probably because of the #:type-thunks argument that you need for
>> concretizing types of lifted definitions. The default was a list with
>> the default base type. This was always a bad idea. I've just pushed
>> a change that instead errors if the concretization list is used
>> without being parameterized with something new first.
>>
>> At any rate, I think this is an xsmith bug, not a bug in your code.
>> Somewhere the `current-xsmith-type-constructor-thunks` parameter is
>> being called where it hasn't been parameterized. If the new exception
>> that will be raised gives any useful information about where this is
>> happening, let me know.
>>
>> On Wed, Jul 21, 2021 at 11:22:07AM -0700, Sorawee Porncharoenwase wrote:
>> >Sure, I can do that.
>> >
>> >I have another question about type->string. I have been using
type->string
>> >from standard-ml / cish examples.
>> >
>> >(define (type->string t)
>> > (let loop ([t* t])
>> > (define t (concretize-type t*))
>> > (unify! t t*)
>> > (cond
>> > [(can-unify? t (immutable (array-type (fresh-type-variable))))
>> > (define inner (fresh-type-variable))
>> > (unify! t (immutable (array-type inner)))
>> > (format "seq<~a>" (loop inner))]
>> > [(can-unify? t (product-type #f))
>> > (match (product-type-inner-type-list t)
>> > [(list) "()"]
>> > [(list a) (loop a)]
>> > [inners (format "(~a)" (string-join (map loop inners) ",
"))])]
>> > [(can-unify? t (function-type (fresh-type-variable)
>> >(fresh-type-variable)))
>> > (define ret (fresh-type-variable))
>> > (define arg (fresh-type-variable))
>> > (unify! t (function-type arg ret))
>> > (format "(~a -> ~a)" (loop arg) (loop ret))]
>> > [(can-unify? t number-type) "int"]
>> > [(can-unify? t int-type) "int"]
>> > [(can-unify? t bool-type) "bool"]
>> > [(can-unify? t string-type) (if (zero? (random 2)) "string"
>> "seq<char>")]
>> > [else #;(error 'type->string "Type not implemented yet: ~v" t)
>> > "FOOBAR"])))
>> >
>> >The first weird thing is that the number-type branch is necessary,
despite
>> >the fact that I don’t have any float in the program.
>> >
>> >The second weird thing is that sometimes "FOOBAR" is reached because t
is
>> >#<xsmith_default-base-type>. In particular, it generates the following
>> code:
>> >
>> >safeSeqSet((var theArray : seq<seq<FOOBAR>> := []; theArray), 1, [1])
>> ># roughly (vector-set (let ([theArray (vector) : (array (array
>> >FOOBAR))]) theArray) 1 (vector 1))
>> >
>> >where you can see that “FOOBAR” here should really be int.
>> >
>> >In my experiment, replacing default-base-type with int seems to work
well,
>> >but it indicates something is obviously wrong. Here’s the call site of
>> >type->string FWIW:
>> >
>> >[ImmutableArrayLiteral
>> > (λ (n)
>> > (match (ast-children (ast-child 'expressions n))
>> > [(list)
>> > ;; sorry for convoluted logic, but I used to use inner-type for
>> >something and haven't refactored this.
>> > (define inner-type (fresh-type-variable))
>> > (define the-array-type (immutable (array-type inner-type)))
>> > (define the-type (concretize-type ($xsmith_type n)))
>> > (unify! the-type the-array-type)
>> > (text (format "(var theArray : ~a := []; theArray)"
>> >(type->string the-type)))]
>> > [xs (h-append lbracket
>> > (comma-list (pretty-print-children xs))
>> > rbracket)]))]
>> >
>> >Any ideas?
>> >
>> >
>> >On Tue, Jul 20, 2021 at 10:45 AM William G Hatch <william@hatch.uno>
>> wrote:
>> >
>> >> Awesome! We have a git repo where we are keeping track of bugs we
>> >> find with Xsmith. If you want, we could add you to it and you can
add
>> >> any bugs you find to it. Otherwise I will probably put in anything
>> >> you mention like this.
>> >>
>> >> On Tue, Jul 20, 2021 at 09:58:55AM -0700, Sorawee Porncharoenwase
wrote:
>> >> >By the way, here are the results so far:
>> >> >
>> >> >- https://github.com/dafny-lang/dafny/issues/1291
>> >> >- https://github.com/dafny-lang/dafny/issues/1297
>> >> >
>> >> >On Tue, Jul 20, 2021 at 9:57 AM Sorawee Porncharoenwase <
>> >> >sorawee.pwase@gmail.com> wrote:
>> >> >
>> >> >> We are primarily focused on different compiler backends for Dafny
>> (Dafny
>> >> >> can be compiled to Java, C#, Rust, JS, Go, C++, and perhaps more).
>> >> >>
>> >> >> On Tue, Jul 20, 2021 at 9:34 AM William G Hatch <william@hatch.uno
>
>> >> wrote:
>> >> >>
>> >> >>> >> Do you have a roadmap for implementing ...
>> >> >>>
>> >> >>> Not at the moment. Right now I'm focused on getting some of our
>> >> >>> mostly-finished fuzzers *really* finished and ready for fuzzing,
>> >> >>> running some fuzzing campaigns to find some bugs, and some
features
>> >> >>> that are immediately helpful for running fuzzing (eg. some stuff
to
>> >> >>> support feedback-directed fuzzing and choice weighting).
>> >> >>>
>> >> >>>
>> >> >>> >Also, I'm curious about the setup of various fuzzers that you
are
>> >> >>> running.
>> >> >>> >How many programs are you able to generate and test per minute?
Do
>> you
>> >> >>> have
>> >> >>> >any particular parallelization setup that works well for you?
>> >> >>>
>> >> >>> There is a harness repository that we use that was mostly
written by
>> >> >>> Guy Watson:
>> >> >>>
>> >> >>> https://gitlab.flux.utah.edu/xsmith/harness
>> >> >>>
>> >> >>> There is a `harness.py` script that takes a configuration file to
>> run
>> >> >>> an xsmith fuzzer, running its output through various
implementations
>> >> >>> of whatever language, comparing the output, and binning the
result
>> >> >>> (eg. everything matching, diff, crash, everything crashing (IE
bad
>> >> >>> program), xsmith itself crashing, ...). That harness script is
>> >> >>> basically for running a single job, and there are 2 ways of
doing it
>> >> >>> in parallel.
>> >> >>>
>> >> >>> The first one is the `go-button`, which can run fuzzing on
multiple
>> >> >>> machines at once. It is fairly dependent on Emulab/Cloudlab
>> >> >>> (https://www.emulab.net/) to have things set up just right, and
>> >> >>> requires at least 2 machines. It also generates a bunch of live
>> >> >>> graphs about fuzzing. It uses ansible to run setup scripts to
prep
>> >> >>> each machine before starting the fuzz campaign.
>> >> >>>
>> >> >>> I mostly use `local-multi-harness` instead, which just runs on a
>> >> >>> single machine, but runs multiple harness processes. It doesn't
>> >> >>> automatically run the setup scripts like the `go-button` does, so
>> >> >>> eg. if you want to use the `racket-kernel-fuzzer` configuration
you
>> >> >>> need to run the `racket-install.rkt` script first manually.
>> >> >>>
>> >> >>> As far as speed, xsmith is not particularly fast. There is a
server
>> >> >>> mode that at least saves on startup time, but I think the harness
>> >> >>> might not run it particularly well (Guy correct me if I'm wrong
--
>> at
>> >> >>> any rate I haven't been using it with server mode, but that
might be
>> >> >>> because I never bothered changing my config after bugs were
fixed).
>> >> >>> Aside from Racket's slow startup speed (particularly bad with
Xsmith
>> >> >>> because it loads a lot of stuff), the runtime varies a lot based
on
>> >> >>> the max-depth configuration, the size of the grammar, etc.
>> >> >>>
>> >> >>> I haven't focused a lot on performance, necessarily. Basically
>> >> >>> whenever I decide Xsmith is too slow for my taste I spend some
time
>> >> >>> trying to optimize it, and generally make a few gains until I
think
>> >> >>> “that's enough optimization for now”. If you can find any ways
to
>> >> >>> make improvements, that would be great! I might have taken all
of
>> the
>> >> >>> low-hanging fruit in my previous optimization passes, however.
In
>> >> >>> previous optimization passes I got the most out of optimizing in
the
>> >> >>> type system, but I made some major improvements to type checking
>> speed
>> >> >>> last time so it may not dominate anymore.
>> >> >>>
>> >> >>>
>> >> >>> As an aside, a question for you: Are there multiple Dafny
>> >> >>> implementations? Or different optimization levels? Or are you
>> >> >>> running different versions of the compiler against each other?
>> >> >>>
>> >> >>>
>> >> >>>
>> >> >>> On Mon, Jul 19, 2021 at 04:15:04PM -0700, Sorawee Porncharoenwase
>> >> wrote:
>> >> >>> >Also, I'm curious about the setup of various fuzzers that you
are
>> >> >>> running.
>> >> >>> >How many programs are you able to generate and test per minute?
Do
>> you
>> >> >>> have
>> >> >>> >any particular parallelization setup that works well for you?
>> >> >>> >
>> >> >>> >On Fri, Jul 16, 2021 at 8:32 PM Sorawee Porncharoenwase <
>> >> >>> >sorawee.pwase@gmail.com> wrote:
>> >> >>> >
>> >> >>> >> Do you have a roadmap for implementing "Provide mechanism for
>> >> >>> precluding
>> >> >>> >> types in `fresh-type-variable` invocations"? (
>> >> >>> >> https://gitlab.flux.utah.edu/xsmith/xsmith/-/issues/56). I
also
>> >> really
>> >> >>> >> want this feature.
>> >> >>> >>
>> >> >>> >> On Thu, Jul 15, 2021 at 9:22 PM William G Hatch
>> <william@hatch.uno>
>> >> >>> wrote:
>> >> >>> >>
>> >> >>> >>> That would be great, thanks!
>> >> >>> >>>
>> >> >>> >>> On Thu, Jul 15, 2021 at 08:09:13PM -0700, Sorawee
>> Porncharoenwase
>> >> >>> wrote:
>> >> >>> >>> >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@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))
>> >> >>> >>> >>
>> >> >>> >>>
>> >> >>> >>
>> >> >>>
>> >> >>
>> >>
>>