File 2441-dialyzer-Add-some-PropEr-tests-of-the-erl_... of Package erlang

Overview Repositories Revisions Requests Users Attributes Meta

File 2441-dialyzer-Add-some-PropEr-tests-of-the-erl_types-modu.patch of Package erlang

From ddd090eef76e2d9db54642f5bd55b181f4c9c1d9 Mon Sep 17 00:00:00 2001
From: Hans Bolinder <hasse@erlang.org>
Date: Tue, 24 Aug 2021 12:43:34 +0200
Subject: [PATCH] dialyzer: Add some PropEr tests of the erl_types module

---
 lib/dialyzer/test/Makefile                    |   2 +-
 lib/dialyzer/test/erl_types_SUITE.erl         |  67 ++++-
 .../test/property_test/erl_types_prop.erl     | 229 ++++++++++++++++++
 3 files changed, 292 insertions(+), 6 deletions(-)
 create mode 100644 lib/dialyzer/test/property_test/erl_types_prop.erl

diff --git a/lib/dialyzer/test/Makefile b/lib/dialyzer/test/Makefile
index d5e975453f..60c5ea5c2e 100644
--- a/lib/dialyzer/test/Makefile
+++ b/lib/dialyzer/test/Makefile
@@ -33,7 +33,7 @@ release_tests_spec:
 	$(INSTALL_DIR) "$(RELSYSDIR)"
 	chmod -R u+w "$(RELSYSDIR)"
 	$(INSTALL_DATA) $(AUXILIARY_FILES) "$(RELSYSDIR)"
-	@tar cf - *_SUITE_data | (cd "$(RELSYSDIR)"; tar xf -)
+	@tar cf - *_SUITE_data property_test | (cd "$(RELSYSDIR)"; tar xf -)
 	cd "$(RELSYSDIR)";\
 	erlc dialyzer_common.erl file_utils.erl;\
 	erl -noshell -run dialyzer_common create_all_suites -s erlang halt
diff --git a/lib/dialyzer/test/erl_types_SUITE.erl b/lib/dialyzer/test/erl_types_SUITE.erl
index 0526e0cac8..5674ffd1cb 100644
--- a/lib/dialyzer/test/erl_types_SUITE.erl
+++ b/lib/dialyzer/test/erl_types_SUITE.erl
@@ -14,10 +14,11 @@
 %%
 -module(erl_types_SUITE).
 
--export([all/0,
-         consistency_and_to_string/1,
-         misc/1,
-         map_multiple_representations/1]).
+-export([all/0,groups/0,init_per_group/2,end_per_group/2,
+         consistency_and_to_string/1,misc/1,map_multiple_representations/1,
+         absorption/1,associativity/1,commutativity/1,idempotence/1,
+         identity/1,limit/1
+        ]).
 
 %% Simplify calls into erl_types and avoid importing the entire module.
 -define(M, erl_types).
@@ -25,7 +26,39 @@
 -include_lib("common_test/include/ct.hrl").
 
 all() ->
-    [consistency_and_to_string, misc, map_multiple_representations].
+    [consistency_and_to_string,
+     misc,
+     map_multiple_representations,
+     {group,property_tests}
+    ].
+
+groups() ->
+    [{property_tests,[parallel],
+      [absorption,
+       associativity,
+       commutativity,
+       idempotence,
+       identity,
+       limit]}].
+
+init_per_group(property_tests, Config0) ->
+    case ct_property_test:init_per_suite(Config0) of
+        [_|_]=Config ->
+            try proper_erlang_abstract_code:module() of
+                _ ->
+                    Config
+            catch
+                error:undef ->
+                    {skip, "No proper_erlang_abstract_code module"}
+            end;
+        Other ->
+            Other
+    end;
+init_per_group(_GroupName, Config) ->
+    Config.
+
+end_per_group(_GroupName, Config) ->
+    Config.
 
 consistency_and_to_string(_Config) ->
     %% Check consistency of types
@@ -323,3 +356,27 @@ map_multiple_representations(_Config) ->
             "#{'a'=>atom(), 'b'=>atom()}" = erl_types:t_to_string(T)
     end(),
     ok.
+
+absorption(Config) ->
+    %% manual test: proper:quickcheck(erl_types_prop:absorption()).
+    true = ct_property_test:quickcheck(erl_types_prop:absorption(), Config).
+
+associativity(Config) ->
+    %% manual test: proper:quickcheck(erl_types_prop:associativity()).
+    true = ct_property_test:quickcheck(erl_types_prop:associativity(), Config).
+
+commutativity(Config) ->
+    %% manual test: proper:quickcheck(erl_types_prop:commutativity()).
+    true = ct_property_test:quickcheck(erl_types_prop:commutativity(), Config).
+
+idempotence(Config) ->
+    %% manual test: proper:quickcheck(erl_types_prop:idempotence()).
+    true = ct_property_test:quickcheck(erl_types_prop:idempotence(), Config).
+
+identity(Config) ->
+    %% manual test: proper:quickcheck(erl_types_prop:identity()).
+    true = ct_property_test:quickcheck(erl_types_prop:identity(), Config).
+
+limit(Config) ->
+    %% manual test: proper:quickcheck(erl_types_prop:limit()).
+    true = ct_property_test:quickcheck(erl_types_prop:limit(), Config).
diff --git a/lib/dialyzer/test/property_test/erl_types_prop.erl b/lib/dialyzer/test/property_test/erl_types_prop.erl
new file mode 100644
index 0000000000..ea5043a2c9
--- /dev/null
+++ b/lib/dialyzer/test/property_test/erl_types_prop.erl
@@ -0,0 +1,229 @@
+%%
+%% %CopyrightBegin%
+%%
+%% Copyright Ericsson AB 2020. 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(erl_types_prop).
+-compile([export_all, nowarn_export_all]).
+
+%% This module only supports proper, as we use features of PropEr's
+%% module erlang_abstract_code not available in quickcheck.
+
+-proptest([proper]).
+
+-ifdef(PROPER).
+
+-include_lib("proper/include/proper.hrl").
+
+-define(REPETITIONS, 5000).
+
+absorption() ->
+    numtests(?REPETITIONS, absorption_1()).
+
+absorption_1() ->
+    ?FORALL({TypeA, TypeB},
+            ?LET(TypeA, type(),
+                 ?LET(TypeB, type(), {TypeA, TypeB})),
+            ?WHENFAIL(
+               begin
+                   io:format("TypeA = ~p,\n", [TypeA]),
+                   io:format("TypeB = ~p,\n", [TypeB]),
+                   io:format("~p:absorption_check(TypeA, TypeB).\n",
+                             [?MODULE])
+               end,
+               absorption_check(TypeA, TypeB))).
+
+absorption_check(A, B) ->
+    %% a ∨ (a ∧ b) = a
+    R1 = sup(A, inf(A, B)),
+    %% a ∧ (a ∨ b) = a
+    R2 = inf(A, sup(A, B)),
+    equal(A, R1) andalso equal(A, R2).
+
+associativity() ->
+    numtests(?REPETITIONS, associativity_1()).
+
+associativity_1() ->
+    ?FORALL({TypeA, TypeB, TypeC},
+            ?LET(TypeA, type_without_no_return(),
+                 ?LET(TypeB, type_without_no_return(),
+                      ?LET(TypeC, type_without_no_return(), {TypeA, TypeB, TypeC}))),
+            ?WHENFAIL(
+               begin
+                   io:format("TypeA = ~p,\n", [TypeA]),
+                   io:format("TypeB = ~p,\n", [TypeB]),
+                   io:format("TypeC = ~p,\n", [TypeC]),
+                   io:format("~p:associativity_check(TypeA, TypeB, TypeC).\n",
+                             [?MODULE])
+               end,
+               associativity_check(TypeA, TypeB, TypeC))).
+
+associativity_check(A, B, C) ->
+    %% a ∨ (b ∨ c) = (a ∨ b) ∨ c
+    LHS_Sup = sup(A, sup(B, C)),
+    RHS_Sup = sup(sup(A, B), C),
+    Test1 = equal(LHS_Sup, RHS_Sup),
+    %% a ∧ (b ∧ c) = (a ∧ b) ∧ c
+    LHS_Inf = inf(A, inf(B, C)),
+    RHS_Inf = inf(inf(A, B), C),
+    Test2 = equal(LHS_Inf, RHS_Inf),
+    Test1 and Test2.
+
+commutativity() ->
+    numtests(?REPETITIONS, commutativity_1()).
+
+commutativity_1() ->
+    ?FORALL({TypeA, TypeB},
+            ?LET(TypeA, type(),
+                 ?LET(TypeB, type(), {TypeA, TypeB})),
+            ?WHENFAIL(
+               begin
+                   io:format("TypeA = ~p,\n", [TypeA]),
+                   io:format("TypeB = ~p,\n", [TypeB]),
+                   io:format("~p:commutativity_check(TypeA, TypeB).\n",
+                             [?MODULE])
+               end,
+               commutativity_check(TypeA, TypeB))).
+
+commutativity_check(A, B) ->
+    %% a ∨ b = b ∨ a
+    Sup_AB = sup(A, B),
+    Sup_BA = sup(B, A),
+    true = sup(A, B) =:= sup(B, A),
+    Test1 = equal(Sup_AB, Sup_BA),
+    %% a ∧ b = b ∧ a
+    Inf_AB = inf(A, B),
+    Inf_BA = inf(B, A),
+    Test2 = equal(Inf_AB, Inf_BA),
+    Test1 and Test2.
+
+idempotence() ->
+    numtests(?REPETITIONS, idempotence_1()).
+
+idempotence_1() ->
+    ?FORALL(Type,
+            type(),
+            ?WHENFAIL(
+               begin
+                   io:format("Type = ~p,\n", [Type]),
+                   io:format("~p:idempotence_check(Type).\n", [?MODULE])
+               end,
+               idempotence_check(Type))).
+
+idempotence_check(Type) ->
+    %% a ∨ a = a
+    Sup = sup(Type, Type),
+    Test1 = equal(Sup, Type),
+    %% a ∧ a = a
+    Inf = inf(Type, Type),
+    Test2 = equal(Inf, Type),
+    Test1 and Test2.
+
+identity() ->
+    numtests(?REPETITIONS, identity_1()).
+
+identity_1() ->
+    ?FORALL(Type, type(), identity_check(Type)).
+
+identity_check(Type) ->
+    %% a ∨ [bottom element] = a
+    Sup = sup(Type, none),
+    Test1 = equal(Sup, Type),
+    %% a ∧ [top element] = a
+    Inf = inf(Type, any),
+    Test2 = equal(Inf, Type),
+    Test1 and Test2.
+
+limit() ->
+    numtests(?REPETITIONS, limit_1()).
+
+limit_1() ->
+    ?FORALL(Type,
+            type(),
+            ?WHENFAIL(
+               begin
+                   io:format("Type = ~p,\n", [Type]),
+                   io:format("~p:limit_check(Type).\n", [?MODULE])
+               end,
+               limit_check(Type))).
+
+limit_check(Type1) ->
+    equal(erl_types:t_limit(Type1, 1000), Type1).
+
+inf(A, B) ->
+    erl_types:t_inf(A, B).
+
+sup(A, B) ->
+    erl_types:t_sup(A, B).
+
+equal(A, B) ->
+    erl_types:t_is_equal(A, B).
+
+type_without_no_return() ->
+    ?SUCHTHAT(Type, type(), not has_no_return(Type)).
+
+has_no_return(unit) ->
+    true;
+has_no_return(Tuple) when is_tuple(Tuple) ->
+    has_no_return(tuple_to_list(Tuple));
+has_no_return([T|Ts]) ->
+    has_no_return(T) orelse has_no_return(Ts);
+has_no_return(_) ->
+    false.
+
+type() ->
+    ?LET(Forms,
+         abstr(),
+         begin
+             [F | _] = [T || {attribute, _, K, {_, T, []}} <- Forms,
+                             K =:= type orelse K =:= opaque],
+             form_to_type(F)
+         end).
+
+abstr() ->
+    Opts = [{types, [{Type, 0} || Type <- types()]},
+            {weight, {atom, 10}},
+            {weight, {type_decl, 1}},
+            {weight, {record_decl, 0}},
+            {weight, {function_spec, 0}},
+            {weight, {function_decl, 0}},
+            {weight, {type_variable, 0}}],
+    proper_erlang_abstract_code:module(Opts).
+
+form_to_type(Form) ->
+    Types = [SiteType | _] = types(),
+    TableTypes = [{{type, Type, 0},
+                   {{m, "file", {type, 0, any, []}, []}, any}} ||
+                     Type <- Types],
+    TypeTable = maps:from_list(TableTypes),
+    CodeTable = ets:new(table, [set]),
+    try
+        true = ets:insert(CodeTable, {m, TypeTable}),
+        Site = {type, {m, SiteType, 0}, ""},
+        C = erl_types:cache__new(),
+        ETypes = sets:from_list([]),
+        {T, _} = erl_types:t_from_form(Form, ETypes, Site, CodeTable, #{}, C),
+        T
+    after
+        true = ets:delete(CodeTable)
+    end.
+
+types() ->
+    [t, tt].
+
+-endif.
-- 
2.31.1

Places

File 2441-dialyzer-Add-some-PropEr-tests-of-the-erl_types-modu.patch of Package erlang

Places