Property based tests to find bugs

[erszcz]

This PR sketches a property based testing framework for Gradualizer. It's based on a vendored version of Proper's Erlang abstract code generator used to property test the Erlang compiler.

On top of that, it uses an ad-hoc construction to define type envs of mutually recursive types - this already allows to find timeouts in normalize runs which I think are the infinite loops found by other testing means such as #324. There's more work needed on that front.

I've not included any src/ fixes found when running the properties so far in this PR, so that it's relatively easy to see if the properties defined here actually find bugs. However, there's already a number of them that I've stashed and will PR separately.

This builds on top of #357, since it deals with creating environments for the properties a little bit. However, if we want to make sure the #357 itself does not introduce new bugs, I can rebase this PR onto the current master which does not include #357 yet.

[josefs]

Lovely! Gradualizer is an obvious candidate for property based testing so adding this is long overdue.
There are so many properties that we ought to check. In particular, it'd be nice to nail down exactly what types looks like after they have been normalized. We've had so many bugs in that area.

I do have some concerns about the details however, see my comments.

[erszcz]

With regard to licensing, I added a test-time dependency on Proper for CI tests, but if we're concerned about GPLv3, I can try making this work with https://github.com/krestenkrab/triq. There are no fancy features used, apart from vendoring Proper's Apache 2.0 Erlang abstract code generators, so I don't expect any problems apart from small API incompatibilities.

[josefs]

With regard to licensing, I added a test-time dependency on Proper for CI tests, but if we're concerned about GPLv3, I can try making this work with https://github.com/krestenkrab/triq. There are no fancy features used, apart from vendoring Proper's Apache 2.0 Erlang abstract code generators, so I don't expect any problems apart from small API incompatibilities.

It's a bit over my head whether we'd be affected by GPLv3 by just doing a test-time dependency. We're not technically linking with the code, and under the spirit of the license it's entirely possible to switch it out with something else. So that suggests that we shouldn't have to change our code to GPLv3. But again, IANAL.

[erszcz]

[...] we shouldn't have to change our code to GPLv3.

I think the same and exactly this lead me to use Proper in the first place. I think we can use it that way at least until someone points out it's not the appropriate way.

[erszcz]

I've rebased this onto #357 so that there's a fast-forward path now and CI kicks in. Failing property based tests don't fail CI builds, but we can see in the details the properties do find issues (though without HTML reports, as available when running things locally, the results are not super readable).

[zuiderkwast]

Very nice! (I haven't looked at the code yet.)

Using Proper is fine as long as we don't "convey" (the word used in the GPLv3 text) releases or escripts, etc. that include Proper. That's my understanding of the license.

[zuiderkwast]

I have looked at everything except the actual property tests. I'll look at them tomorrow. Great in general.

[zuiderkwast]

I guess we can make it a test-only dependency, right?

Although we use a simple Makefile without rebar for building, rebar3 is used when running Gradualizer from the rebar3 plugin.

Btw, when running the property tests using rebar, the beams are built in a different place than what's used for the other tests and the plain build. I suppose it's fine, but the project seems a bit messier this way. How about some simple hand-written lines for git cloning proper in the Makefile?

[erszcz]

I've made Proper a test-only dependency.

[erszcz]

How about some simple hand-written lines for git cloning proper in the Makefile?

Hmmm, to be honest I'm not convinced - I don't really see the benefit of using a custom Makefile in Gradualizer. A lot of work has been put into Rebar3 and not having to write custom Makefile rules is IMO one of the positive outcomes.

Proper is now a test-only dependency, though, so it won't pollute other projects when Gradualizer itself is pulled in as a dependency.

[erszcz]

For some context:

$ rm -rf _build
$ time r3 compile
...

real	0m3.370s
user	0m4.288s
sys	0m0.669s

$ make clean
$ time make
...

real	0m15.742s
user	0m11.484s
sys	0m4.863s

[zuiderkwast]

If this one is always called on a normalized type (is it?), we don't need this clause. It's good if we know whether it needs to be normalized or not and describe that in a comment before the function.

[erszcz]

normalize doesn't handle annotated type variables ({ann_type, _, _} nodes) - I haven't given much thought yet to whether it should or not. I'm not sure either whether it makes sense for these to be passed to GLB, but it certainly happens with the generator we have.

I checked all call sites of has_overlapping_keys - it's always called on normalized types.

In general, normalize is not complete with regard to normalizing types which might recursively contain other types - tuple is not normalized at all, so tuple elements will not be normalized wherever they appear. See fd48ed0 which is part of #361. Tuple elements are ad-hoc normalized in some places, though. For example

Gradualizer/src/typechecker.erl

Line 3582 in b094581

RefTys = [refine(Ty1, Ty2, Env) || {Ty1, Ty2} <- lists:zip(Tys1, Tys2)],

- refine_ty goes through refine, which normalizes its arguments.

Maybe you're right that the correct fix is to seal the leaks in normalize, instead of scattering patches everywhere around the codebase 🤔

=== Location: {gradualizer_prop_SUITE,glb}
=== === Reason: {{ann_type,0,[{var,0,type_variable},{type,0,map,any}]},
                  {type,0,map,
                   [{type,0,map_field_assoc,[{type,0,port,[]},{integer,0,2}]},
                    {type,0,map_field_assoc,
                     [{type,0,union,
                       [{integer,0,5},
                        {type,0,tuple,any},
                        {type,0,record,
                         [{atom,0,r3},
                          {type,0,field_type,
                           [{atom,0,f1},{var,0,type_variable}]}]},
                        {ann_type,0,
                         [{var,0,type_variable},
                          {type,0,range,[{integer,0,3},{integer,0,0}]}]}]},
                      {type,0,map,[]}]}]}}

An exception was raised: error:{bad_generator,any}.

Stacktrace: [{typechecker,'-has_overlapping_keys/2-lc$^0/1-0-',3,
                          [{file,"/Users/erszcz/work/erszcz/gradualizer/src/typechecker.erl"},
                           {line,734}]},
             {typechecker,has_overlapping_keys,2,
                          [{file,"/Users/erszcz/work/erszcz/gradualizer/src/typechecker.erl"},
                           {line,734}]},
             {typechecker,glb_ty,4,
                          [{file,"/Users/erszcz/work/erszcz/gradualizer/src/typechecker.erl"},
                           {line,617}]},
             {typechecker,glb,4,
                          [{file,"/Users/erszcz/work/erszcz/gradualizer/src/typechecker.erl"},
                           {line,493}]},
             {gradualizer_prop,prop_glb_,2,
                               [{file,"gradualizer_prop.erl"},{line,154}]}].

[erszcz]

Just adding {ann_type, ...} to normalize seems to solve the problem :)

[zuiderkwast]

Good. In the past I wanted the ann_type annotations to be deleted by normalize. I don't know why we didn't do it. It's good that at least normalizing the child of the ann_type solves it.

[zuiderkwast]

See #228, #247, #253. Specifically #253 deleted the ann_type clause in normalize and many other places and instead strips the ann_types in remove_pos. Do you know how an ann_type can make it past remove_pos to normalize?

[erszcz]

Ahhh, that explains a lot!

There are multiple properties defined and most of them call internal typechecker functions. The properties should encapsulate the information on invariants which should hold for the inputs to these internal typechecker functions (like, "should params to this function be normalized already or will it normalize them?"). Possibly, some don't do it accurately, yet.

That being said, the problem was originally found by prop_glb. Let's see if it shows up if the property in question is modified to call typelib:remove_pos/1 on the arguments before passing them to glb/3...

[erszcz]

Eagle eye, @zuiderkwast! d72d57e illustrates what I had in mind in the previous comment.

BTW, if I understand you correctly, then every property that uses a generated type as input should actually call typelib:remove_pos on the type, shouldn't it?

[erszcz]

I have looked at everything except the actual property tests.

The property tests so far aren't sophisticated at all. They just call some typechecker functions with a timeout and check if they fail or not. Failure is understood as exiting or erroring, since throwing is a valid way to return diagnostics from nested code. So no invariants other than "it should not crash, but terminate anyway" are currently checked :)

[zuiderkwast]

LGTM

[erszcz]

I applied fixes for the latest comments. I think this is ready to merge unless we need CI on Erlang 22 EDIT: Erlang 22 is reenabled on CI, but without proptests on that version. I also modified the PR title to make it clear it doesn't yet detect any infinite loops - that needs some further work.

[zuiderkwast]

@erszcz Do you have a message for a squash commit? Can I use the top comment of the PR?

[erszcz]

I've modified the properties to always call typelib:remove_pos on generated types.

As for the squash message, maybe this?

This PR sketches a property based testing framework for Gradualizer. It's based on a vendored version of Proper's Erlang abstract code generator used to property test the Erlang compiler.

[zuiderkwast]

Great!