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

Re: [xsmith-dev] XSmith questions



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))