[xsmith-dev] XSmith questions

[Sorawee Porncharoenwase]

>
> 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/20210713/4dc1396f/attachment.html>