compiler: Break out SSA/beam type definitions into a separate module

3 files changed, 222 insertions, 1 deletions

diff --git a/lib/compiler/test/Makefile b/lib/compiler/test/Makefile
index db8eb7e2e1..2c0767b17f 100644
--- a/lib/compiler/test/Makefile
+++ b/lib/compiler/test/Makefile
@@ -16,6 +16,7 @@ MODULES= \
 	beam_reorder_SUITE \
 	beam_ssa_SUITE \
 	beam_type_SUITE \
+	beam_types_SUITE \
 	beam_utils_SUITE \
 	bif_SUITE \
 	bs_bincomp_SUITE \
@@ -225,6 +226,6 @@ release_tests_spec: make_emakefile
 	$(INSTALL_DATA) $(ERL_DUMMY_FILES) "$(RELSYSDIR)"
 	rm $(ERL_DUMMY_FILES)
 	chmod -R u+w "$(RELSYSDIR)"
-	@tar cf - *_SUITE_data | (cd "$(RELSYSDIR)"; tar xf -)
+	@tar cf - *_SUITE_data property_test | (cd "$(RELSYSDIR)"; tar xf -)
 
 release_docs_spec:
diff --git a/lib/compiler/test/beam_types_SUITE.erl b/lib/compiler/test/beam_types_SUITE.erl
new file mode 100644
index 0000000000..66fd517ec0
--- /dev/null
+++ b/lib/compiler/test/beam_types_SUITE.erl
@@ -0,0 +1,80 @@
+%%
+%% %CopyrightBegin%
+%%
+%% Copyright Ericsson AB 2019. All Rights Reserved.
+%%
+%% Licensed under the Apache License, Version 2.0 (the "License");
+%% you may not use this file except in compliance with the License.
+%% You may obtain a copy of the License at
+%%
+%%     http://www.apache.org/licenses/LICENSE-2.0
+%%
+%% Unless required by applicable law or agreed to in writing, software
+%% distributed under the License is distributed on an "AS IS" BASIS,
+%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+%% See the License for the specific language governing permissions and
+%% limitations under the License.
+%%
+%% %CopyrightEnd%
+%%
+
+-module(beam_types_SUITE).
+
+-include_lib("compiler/src/beam_types.hrl").
+
+-export([all/0, suite/0, groups/0,
+         init_per_suite/1, end_per_suite/1]).
+
+-export([consistency/1, commutativity/1,
+         binary_consistency/1, integer_consistency/1]).
+
+suite() ->
+    [{ct_hooks,[ts_install_cth]}].
+
+all() ->
+    [{group,property_tests}].
+
+groups() ->
+    [{property_tests,[], [consistency, commutativity,
+                          binary_consistency, integer_consistency]}].
+
+init_per_suite(Config) ->
+    ct_property_test:init_per_suite(Config).
+
+end_per_suite(Config) ->
+    Config.
+
+consistency(Config) when is_list(Config) ->
+    %% manual test: proper:quickcheck(beam_types_prop:consistency()).
+    true = ct_property_test:quickcheck(beam_types_prop:consistency(), Config).
+
+commutativity(Config) when is_list(Config) ->
+    %% manual test: proper:quickcheck(beam_types_prop:commutativity()).
+    true = ct_property_test:quickcheck(beam_types_prop:commutativity(), Config).
+
+binary_consistency(Config) when is_list(Config) ->
+    %% These binaries should meet into {binary,12} as that's the best common
+    %% unit for both types.
+    A = {binary, 4},
+    B = {binary, 6},
+
+    {binary, 12} = beam_types:meet(A, B),
+    {binary, 2} = beam_types:join(A, B),
+
+    A = beam_types:meet(A, beam_types:join(A, B)),
+    A = beam_types:join(A, beam_types:meet(A, B)),
+
+    ok.
+
+integer_consistency(Config) when is_list(Config) ->
+    %% Integers that don't overlap fully should never meet.
+    A = #t_integer{elements={3,5}},
+    B = #t_integer{elements={4,6}},
+
+    none = beam_types:meet(A, B),
+    #t_integer{elements={3,6}} = beam_types:join(A, B),
+
+    A = beam_types:meet(A, beam_types:join(A, B)),
+    A = beam_types:join(A, beam_types:meet(A, B)),
+
+    ok.
diff --git a/lib/compiler/test/property_test/beam_types_prop.erl b/lib/compiler/test/property_test/beam_types_prop.erl
new file mode 100644
index 0000000000..815e353853
--- /dev/null
+++ b/lib/compiler/test/property_test/beam_types_prop.erl
@@ -0,0 +1,140 @@
+%%
+%% %CopyrightBegin%
+%%
+%% Copyright Ericsson AB 2019. All Rights Reserved.
+%%
+%% Licensed under the Apache License, Version 2.0 (the "License");
+%% you may not use this file except in compliance with the License.
+%% You may obtain a copy of the License at
+%%
+%%     http://www.apache.org/licenses/LICENSE-2.0
+%%
+%% Unless required by applicable law or agreed to in writing, software
+%% distributed under the License is distributed on an "AS IS" BASIS,
+%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+%% See the License for the specific language governing permissions and
+%% limitations under the License.
+%%
+%% %CopyrightEnd%
+%%
+
+-module(beam_types_prop).
+
+-compile([export_all, nowarn_export_all]).
+
+%% This module has only supports proper, as we don't have an eqc license to
+%% test with.
+
+-proptest([proper]).
+
+-ifdef(PROPER).
+
+-include_lib("compiler/src/beam_types.hrl").
+
+-include_lib("proper/include/proper.hrl").
+-define(MOD_eqc,proper).
+
+consistency() ->
+    ?FORALL({TypeA, TypeB},
+            ?LET(TypeA, type(),
+                 ?LET(TypeB, type(), {TypeA, TypeB})),
+            consistency_check(TypeA, TypeB)).
+
+consistency_check(A, B) ->
+    consistency_check_1(A, B),
+    consistency_check_1(B, A),
+    true.
+
+consistency_check_1(A, B) ->
+    A = beam_types:meet(A, beam_types:join(A, B)),
+    A = beam_types:join(A, beam_types:meet(A, B)),
+    ok.
+
+commutativity() ->
+    ?FORALL({TypeA, TypeB},
+            ?LET(TypeA, type(),
+                 ?LET(TypeB, type(), {TypeA, TypeB})),
+            commutativity_check(TypeA, TypeB)).
+
+commutativity_check(A, B) ->
+    true = beam_types:meet(A, B) =:= beam_types:meet(B, A),
+    true = beam_types:join(A, B) =:= beam_types:join(B, A),
+    true.
+
+%%%
+%%% Generators
+%%%
+
+type() ->
+    type(0).
+
+type(Depth) ->
+    oneof(nested_types(Depth) ++
+              numerical_types() ++
+              list_types() ++
+              other_types()).
+
+other_types() ->
+    [any, gen_atom(), gen_binary(), none].
+
+list_types() ->
+    [cons, list, nil].
+
+numerical_types() ->
+    [gen_integer(), float, number].
+
+nested_types(Depth) when Depth >= 3 -> [];
+nested_types(Depth) -> [map, gen_tuple(Depth + 1)].
+
+gen_atom() ->
+    ?LET(Size, range(0, ?ATOM_SET_SIZE),
+         case Size of
+             0 ->
+                 #t_atom{};
+             _ ->
+                 ?LET(Set, sized_list(Size, atom()),
+                      begin
+                          #t_atom{elements=ordsets:from_list(Set)}
+                      end)
+         end).
+
+gen_binary() ->
+    ?SHRINK({binary, range(1, 128)},
+            [{binary, [1, 2, 3, 5, 7, 8, 16, 32, 64]}]).
+
+gen_integer() ->
+    oneof([gen_integer_bounded(), #t_integer{}]).
+
+gen_integer_bounded() ->
+    ?LET(A, integer(),
+         ?LET(B, integer(),
+              begin
+                  #t_integer{elements={min(A,B), max(A,B)}}
+              end)).
+
+gen_tuple(Depth) ->
+    ?SIZED(Size,
+           ?LET(Exact, oneof([true, false]),
+                ?LET(Elements, gen_tuple_elements(Size, Depth),
+                     begin
+                         #t_tuple{exact=Exact,
+                                  size=Size,
+                                  elements=Elements}
+                     end))).
+
+gen_tuple_elements(Size, Depth) ->
+    ?LET(Types, sized_list(rand:uniform(Size div 4 + 1), gen_element(Depth)),
+         maps:from_list([{rand:uniform(Size), T} || T <- Types])).
+
+gen_element(Depth) ->
+    ?LAZY(?SUCHTHAT(Type, type(Depth),
+                    case Type of
+                        any -> false;
+                        none -> false;
+                        _ -> true
+                    end)).
+
+sized_list(0, _Gen) -> [];
+sized_list(N, Gen) -> [Gen | sized_list(N - 1, Gen)].
+
+-endif.