[xsmith-dev] Numeric types not playing nice

[William G Hatch]

Sorry for the delay, I've been busy lately and haven't been able to look at this.

But I finally made some time today.  It's been a while since I wrote this stuff, so I had to look in the source.  What's happening is that when a node gives types to its children, they are each allowed to give a subtype of that type.  So if, say, an add node chooses to type its children as `number`, each child of the add node can choose any subtype of `number` independently.  So effectively they each already get a `fresh-subtype` independently.  Perhaps it would be good to add a feature to force them to be strictly that type and not a subtype, but I'm not going to do that right now.  Feel free to add it yourself if you want!  The code that's doing this is at: https://gitlab.flux.utah.edu/xsmith/xsmith/-/blob/2836e5f03502b5dd63a36c7102a1b3d85d88ec30/xsmith/private/core-properties.rkt?page=2#L1577

Best of luck,
William Hatch


On Sun, Jan 21, 2024 at 11:25:08AM +0000, Vree, E.A. de (Everard, Student B-TCS) wrote:
>I've come across another instance of the problem. I use the MutableArray from canned-components, but sometimes my ArrayLiterals get generated with Int and Float literals, probably due to my Mutable Array being a mutable (array-type number-type). Here's the generated s-exps
>
>(ProcedureApplicationSingle
>         (procedure
>          (LambdaSingleWithExpression
>           (parameter (FormalParameter (type #<bool>) (name "arg_2")))
>           (body
>            (MutableArrayLiteral
>             (expressions
>              ((FloatLiteral (v -425191240.69550025))
>               (IntLiteral (v -65005484))))))))
>         (argument (BoolLiteral (v #t)))))))))
>
>Are you sure there is nothing wrong with my type definitions? Am I missing a way to explicitly subtype them?
>
>Regards,
>Everard de Vree
>________________________________
>Van: Vree, E.A. de (Everard, Student B-TCS) <e.a.devree at student.utwente.nl>
>Verzonden: dinsdag 16 januari 2024 11:41
>Aan: William G Hatch <william at hatch.uno>
>CC: xsmith-dev at flux.utah.edu <xsmith-dev at flux.utah.edu>
>Onderwerp: Re: [xsmith-dev] Numeric types not playing nice
>
>A version of my project is available at https://gitlab.utwente.nl/s2516268/research-project-2023-1B. It contains a very simple fuzzer with many borrowed elements from the python fuzzer from xsmith-examples. I have replaced all the fresh-subtypes with(fresh-type-variable integral-type fractional-type)instead, which seems to cause no more issues. However, if this is a bug it would of course be interesting to my research.
>Thanks for the quick response, and I look forward to hearing from you.
>
>Everard de Vree
>
>________________________________
>Van: William G Hatch <william at hatch.uno>
>Verzonden: dinsdag 16 januari 2024 05:05
>Aan: Vree, E.A. de (Everard, Student B-TCS) <e.a.devree at student.utwente.nl>
>CC: xsmith-dev at flux.utah.edu <xsmith-dev at flux.utah.edu>
>Onderwerp: Re: [xsmith-dev] Numeric types not playing nice
>
>Hmm, that sounds like a bug.  Can you share a link to your code?
>
>This may be one of those corners of Xsmith that was built out but
>never seriously exercised.
>
>On Mon, Jan 15, 2024 at 12:39:31PM +0000, Vree, E.A. de (Everard, Student B-TCS) wrote:
>>Hello everyone,
>>
>>I am currently working on a Haskell fuzzer  and new to Racket and Xsmith in general, so I apologize in advance if this question is trivial. There is something I don't understand about the types in Xsmith:
>>I emulate Haskell's numerical types like this:
>>
>>(define number-type (base-type 'number #:leaf? #f))
>>(define real-type (base-type 'real number-type #:leaf? #f))
>>(define integral-type (base-type 'integral real-type #:leaf? #f))
>>(define int-type (base-type 'int integral-type))
>>(define integer-type (base-type 'integer integral-type))
>>(define fractional-type (base-type 'fractional real-type #:leaf? #f))
>>(define float-type (base-type 'float fractional-type))
>>
>>I then define the type info from the Minus Expression like this:
>>
>>(define numeric-bin-op-subtype (λ (n t) (hash 'l t 'r t)))
>>
>>[Minus [(fresh-subtype-of number-type) numeric-bin-op-subtype]]
>>
>>My assumption was that both Minus children nodes would be constrained to all the non-leaf nodes in either integral-type, or fractional-type. However, Xsmith still generates Minus nodes with 'l integral and 'r fractional, causing a type constraint violation in Haskell. I have since switched to using (fresh-type-variable integral-type fractional-type). This works, but I am still puzzled about fresh-subtypes. REPL experiments confirm that even fresh-subtypes of my real-types can be unified with both fractional-type and integral-type. What happens when a fresh-subtype is created?
>>
>>Regards,
>>
>>Everard de Vree