diff options
Diffstat (limited to 'lib/compiler')
| -rw-r--r-- | lib/compiler/test/beam_types_SUITE.erl | 45 | ||||
| -rw-r--r-- | lib/compiler/test/property_test/beam_types_prop.erl | 117 |
2 files changed, 126 insertions, 36 deletions
diff --git a/lib/compiler/test/beam_types_SUITE.erl b/lib/compiler/test/beam_types_SUITE.erl index 297bd4026e..1b6397301b 100644 --- a/lib/compiler/test/beam_types_SUITE.erl +++ b/lib/compiler/test/beam_types_SUITE.erl @@ -25,18 +25,30 @@ -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]). +-export([absorption/1, + associativity/1, + commutativity/1, + idempotence/1, + identity/1]). + +-export([binary_absorption/1, + integer_absorption/1]). suite() -> [{ct_hooks,[ts_install_cth]}]. all() -> - [{group,property_tests}]. + [{group,property_tests}, + binary_absorption, + integer_absorption]. groups() -> - [{property_tests,[], [consistency, commutativity, - binary_consistency, integer_consistency]}]. + [{property_tests,[parallel], + [absorption, + associativity, + commutativity, + idempotence, + identity]}]. init_per_suite(Config) -> ct_property_test:init_per_suite(Config). @@ -44,15 +56,27 @@ 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). +absorption(Config) when is_list(Config) -> + %% manual test: proper:quickcheck(beam_types_prop:absorption()). + true = ct_property_test:quickcheck(beam_types_prop:absorption(), Config). + +associativity(Config) when is_list(Config) -> + %% manual test: proper:quickcheck(beam_types_prop:associativity()). + true = ct_property_test:quickcheck(beam_types_prop:associativity(), 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) -> +idempotence(Config) when is_list(Config) -> + %% manual test: proper:quickcheck(beam_types_prop:idempotence()). + true = ct_property_test:quickcheck(beam_types_prop:idempotence(), Config). + +identity(Config) when is_list(Config) -> + %% manual test: proper:quickcheck(beam_types_prop:identity()). + true = ct_property_test:quickcheck(beam_types_prop:identity(), Config). + +binary_absorption(Config) when is_list(Config) -> %% These binaries should meet into {binary,12} as that's the best common %% unit for both types. A = #t_bitstring{unit=4}, @@ -66,7 +90,7 @@ binary_consistency(Config) when is_list(Config) -> ok. -integer_consistency(Config) when is_list(Config) -> +integer_absorption(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}}, @@ -78,3 +102,4 @@ integer_consistency(Config) when is_list(Config) -> 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 index 9c103d3886..80966bbfc8 100644 --- a/lib/compiler/test/property_test/beam_types_prop.erl +++ b/lib/compiler/test/property_test/beam_types_prop.erl @@ -22,8 +22,8 @@ -compile([export_all, nowarn_export_all]). -%% This module has only supports proper, as we don't have an eqc license to -%% test with. +%% This module only supports proper, as we don't have an eqc license to test +%% with. -proptest([proper]). @@ -34,31 +34,94 @@ -include_lib("proper/include/proper.hrl"). -define(MOD_eqc,proper). -consistency() -> +%% The default repetitions of 100 is a bit too low to reliably cover all type +%% combinations, so we crank it up a bit. +-define(REPETITIONS, 1000). + +absorption() -> + numtests(?REPETITIONS, absorption_1()). + +absorption_1() -> ?FORALL({TypeA, TypeB}, ?LET(TypeA, type(), ?LET(TypeB, type(), {TypeA, TypeB})), - consistency_check(TypeA, TypeB)). + absorption_check(TypeA, TypeB)). -consistency_check(A, B) -> - consistency_check_1(A, B), - consistency_check_1(B, A), - true. +absorption_check(A, B) -> + %% a ∨ (a ∧ b) = a, + A = beam_types:join(A, beam_types:meet(A, B)), -consistency_check_1(A, B) -> + %% a ∧ (a ∨ b) = a. A = beam_types:meet(A, beam_types:join(A, B)), - A = beam_types:join(A, beam_types:meet(A, B)), - ok. + + true. + +associativity() -> + numtests(?REPETITIONS, associativity_1()). + +associativity_1() -> + ?FORALL({TypeA, TypeB, TypeC}, + ?LET(TypeA, type(), + ?LET(TypeB, type(), + ?LET(TypeC, type(), {TypeA, TypeB, TypeC}))), + associativity_check(TypeA, TypeB, TypeC)). + +associativity_check(A, B, C) -> + %% a ∨ (b ∨ c) = (a ∨ b) ∨ c, + LHS_Join = beam_types:join(A, beam_types:join(B, C)), + RHS_Join = beam_types:join(beam_types:join(A, B), C), + LHS_Join = RHS_Join, + + %% a ∧ (b ∧ c) = (a ∧ b) ∧ c. + LHS_Meet = beam_types:meet(A, beam_types:meet(B, C)), + RHS_Meet = beam_types:meet(beam_types:meet(A, B), C), + LHS_Meet = RHS_Meet, + + true. commutativity() -> + numtests(?REPETITIONS, commutativity_1()). + +commutativity_1() -> ?FORALL({TypeA, TypeB}, ?LET(TypeA, type(), ?LET(TypeB, type(), {TypeA, TypeB})), - commutativity_check(TypeA, TypeB)). + commutativity_check(TypeA, TypeB)). commutativity_check(A, B) -> - true = beam_types:meet(A, B) =:= beam_types:meet(B, A), + %% a ∨ b = b ∨ a, true = beam_types:join(A, B) =:= beam_types:join(B, A), + + %% a ∧ b = b ∧ a. + true = beam_types:meet(A, B) =:= beam_types:meet(B, A), + + true. + +idempotence() -> + numtests(?REPETITIONS, idempotence_1()). + +idempotence_1() -> + ?FORALL(Type, type(), idempotence_check(Type)). + +idempotence_check(Type) -> + %% a ∨ a = a, + Type = beam_types:join(Type, Type), + + %% a ∧ a = a. + Type = beam_types:meet(Type, Type), + + true. + +identity() -> + ?FORALL(Type, type(), identity_check(Type)). + +identity_check(Type) -> + %% a ∨ [bottom element] = a, + Type = beam_types:join(Type, none), + + %% a ∧ [top element] = a. + Type = beam_types:meet(Type, any), + true. %%% @@ -75,7 +138,10 @@ type(Depth) -> other_types()). other_types() -> - [any, gen_atom(), gen_binary(), none]. + [any, + gen_atom(), + gen_binary(), + none]. list_types() -> [cons, list, nil]. @@ -106,21 +172,19 @@ 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)). + ?LET({A, B}, {integer(), 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))). + ?LET({Exact, Elements}, {boolean(), 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)), @@ -134,6 +198,7 @@ gen_element(Depth) -> _ -> true end)). + sized_list(0, _Gen) -> []; sized_list(N, Gen) -> [Gen | sized_list(N - 1, Gen)]. |