refactor(test): put all property cases to test/props directory

.github/workflows/run_test_case.yaml

@@ -15,12 +15,11 @@ jobs:
         - uses: actions/checkout@v1
         - name: Code dialyzer
           run: |
+            make xref
             make dialyzer
             rm -f rebar.lock
         - name: Run tests
           run: |
-            make xref
-            rm -f rebar.lock
             make eunit
             rm -f rebar.lock
             make ct

Makefile

@@ -14,10 +14,6 @@ RUN_NODE_NAME = emqxdebug@127.0.0.1
 .PHONY: all
 all: compile
 
-.PHONY: dialyzer
-dialyzer:
-	@rebar3 dialyzer
-
 .PHONY: tests
 tests: eunit ct
 
@@ -75,6 +71,14 @@ coveralls:
 xref:
 	@rebar3 xref
 
+.PHONY: dialyzer
+dialyzer:
+	@rebar3 dialyzer
+
+.PHONY: proper
+proper:
+	@rebar3 proper -d test/props -c
+
 .PHONY: deps
 deps:
 	@rebar3 get-deps

rebar.config

@@ -1,5 +1,7 @@
 {minimum_otp_vsn, "21.3"}.
 
+{plugins, [rebar3_proper]}.
+
 {deps,
  [{gproc, {git, "https://github.com/uwiger/gproc", {tag, "0.8.0"}}},
   {jiffy, {git, "https://github.com/emqx/jiffy", {tag, "1.0.4"}}},
@@ -39,7 +41,7 @@
     {deps,
      [{bbmustache, "1.7.0"},
       {emqtt, {git, "https://github.com/emqx/emqtt", {tag, "1.2.0"}}},
-      {emqx_ct_helpers, {git, "https://github.com/emqx/emqx-ct-helpers", {tag, "1.2.2"}}}
+      {emqx_ct_helpers, {git, "https://github.com/emqx/emqx-ct-helpers", {tag, "1.3.0"}}}
      ]},
     {erl_opts, [debug_info]}
    ]}

test/emqx_frame_SUITE.erl

@@ -20,14 +20,10 @@
 -compile(nowarn_export_all).
 
 -include("emqx_mqtt.hrl").
--include_lib("proper/include/proper.hrl").
 -include_lib("eunit/include/eunit.hrl").
 -include_lib("common_test/include/ct.hrl").
 -include_lib("emqx_ct_helpers/include/emqx_ct.hrl").
 
-%%-define(PROPTEST(F), ?assert(proper:quickcheck(F()))).
--define(PROPTEST(F), ?assert(proper:quickcheck(F(), [{to_file, user}]))).
-
 all() ->
     [{group, parse},
      {group, connect},
@@ -49,8 +45,7 @@ groups() ->
        t_parse_frame_too_large
       ]},
      {connect, [parallel],
-      [t_serialize_parse_connect,
-       t_serialize_parse_v3_connect,
+      [t_serialize_parse_v3_connect,
        t_serialize_parse_v4_connect,
        t_serialize_parse_v5_connect,
        t_serialize_parse_connect_without_clientid,
@@ -134,29 +129,6 @@ t_parse_frame_too_large(_) ->
     ?catch_error(frame_too_large, parse_serialize(Packet, #{max_size => 512})),
     ?assertEqual(Packet, parse_serialize(Packet, #{max_size => 2048, version => ?MQTT_PROTO_V4})).
 
-t_serialize_parse_connect(_) ->
-    ?PROPTEST(prop_serialize_parse_connect).
-
-prop_serialize_parse_connect() ->
-    ?FORALL(Opts = #{version := ProtoVer}, parse_opts(),
-            begin
-                ProtoName = proplists:get_value(ProtoVer, ?PROTOCOL_NAMES),
-                Packet = ?CONNECT_PACKET(#mqtt_packet_connect{
-                                            proto_name   = ProtoName,
-                                            proto_ver    = ProtoVer,
-                                            clientid     = <<"clientId">>,
-                                            will_qos     = ?QOS_1,
-                                            will_flag    = true,
-                                            will_retain  = true,
-                                            will_topic   = <<"will">>,
-                                            will_props   = #{},
-                                            will_payload = <<"bye">>,
-                                            clean_start  = true,
-                                            properties = #{}
-                                           }),
-                ok == ?assertEqual(Packet, parse_serialize(Packet, Opts))
-            end).
-
 t_serialize_parse_v3_connect(_) ->
     Bin = <<16,37,0,6,77,81,73,115,100,112,3,2,0,60,0,23,109,111,115,
             113,112,117, 98,47,49,48,52,53,49,45,105,77,97,99,46,108,
@@ -530,9 +502,6 @@ t_serialize_parse_auth_v5(_) ->
     ?assertEqual(Packet, parse_serialize(Packet, #{version => ?MQTT_PROTO_V5,
                                                    strict_mode => true})).
 
-parse_opts() ->
-    ?LET(PropList, [{strict_mode, boolean()}, {version, range(4,5)}], maps:from_list(PropList)).
-
 parse_serialize(Packet) ->
     parse_serialize(Packet, #{strict_mode => true}).
 

test/emqx_reason_codes_SUITE.erl

@@ -20,7 +20,6 @@
 -compile(nowarn_export_all).
 
 -include("emqx_mqtt.hrl").
--include_lib("proper/include/proper.hrl").
 -include_lib("eunit/include/eunit.hrl").
 
 all() -> emqx_ct:all(?MODULE).
@@ -29,124 +28,3 @@ t_frame_error(_) ->
     ?assertEqual(?RC_PACKET_TOO_LARGE, emqx_reason_codes:frame_error(frame_too_large)),
     ?assertEqual(?RC_MALFORMED_PACKET, emqx_reason_codes:frame_error(bad_packet_id)),
     ?assertEqual(?RC_MALFORMED_PACKET, emqx_reason_codes:frame_error(bad_qos)).
-
-t_prop_name_text(_) ->
-    ?assert(proper:quickcheck(prop_name_text(), prop_name_text(opts))).
-
-t_prop_compat(_) ->
-    ?assert(proper:quickcheck(prop_compat(), prop_compat(opts))).
-
-t_prop_connack_error(_) ->
-    ?assert(proper:quickcheck(prop_connack_error(), default_opts([]))).
-
-prop_name_text(opts) ->
-    default_opts([{numtests, 1000}]).
-
-prop_name_text() ->
-    ?FORALL(UnionArgs, union_args(),
-            is_atom(apply_fun(name, UnionArgs)) andalso
-            is_binary(apply_fun(text, UnionArgs))).
-
-prop_compat(opts) ->
-    default_opts([{numtests, 512}]).
-
-prop_compat() ->
-    ?FORALL(CompatArgs, compat_args(),
-            begin
-                Result = apply_fun(compat, CompatArgs),
-                is_number(Result) orelse Result =:= undefined
-            end).
-
-prop_connack_error() ->
-    ?FORALL(CONNACK_ERROR_ARGS, connack_error_args(),
-            is_integer(apply_fun(connack_error, CONNACK_ERROR_ARGS))).
-
-%%--------------------------------------------------------------------
-%% Helper
-%%--------------------------------------------------------------------
-
-default_opts() ->
-    default_opts([]).
-
-default_opts(AdditionalOpts) ->
-    [{to_file, user} | AdditionalOpts].
-
-apply_fun(Fun, Args) ->
-    apply(emqx_reason_codes, Fun, Args).
-
-%%--------------------------------------------------------------------
-%% Generator
-%%--------------------------------------------------------------------
-
-union_args() ->
-    frequency([{6, [real_mqttv3_rc(), mqttv3_version()]},
-               {43, [real_mqttv5_rc(), mqttv5_version()]}]).
-
-compat_args() ->
-    frequency([{18, [connack, compat_rc()]},
-               {2, [suback, compat_rc()]},
-               {1, [unsuback, compat_rc()]}]).
-
-connack_error_args() ->
-    [frequency([{10, connack_error()},
-                {1, unexpected_connack_error()}])].
-
-connack_error() ->
-    oneof([client_identifier_not_valid,
-           bad_username_or_password,
-           bad_clientid_or_password,
-           username_or_password_undefined,
-           password_error,
-           not_authorized,
-           server_unavailable,
-           server_busy,
-           banned,
-           bad_authentication_method]).
-
-unexpected_connack_error() ->
-    oneof([who_knows]).
-
-
-real_mqttv3_rc() ->
-    frequency([{6, mqttv3_rc()},
-               {1, unexpected_rc()}]).
-
-real_mqttv5_rc() ->
-    frequency([{43, mqttv5_rc()},
-               {2, unexpected_rc()}]).
-
-compat_rc() ->
-    frequency([{95, ?SUCHTHAT(RC , mqttv5_rc(), RC >= 16#80 orelse RC =< 2)},
-               {5, unexpected_rc()}]).
-
-mqttv3_rc() ->
-    oneof(mqttv3_rcs()).
-
-mqttv5_rc() ->
-    oneof(mqttv5_rcs()).
-
-unexpected_rc() ->
-    oneof(unexpected_rcs()).
-
-mqttv3_rcs() ->
-    [0, 1, 2, 3, 4, 5].
-
-mqttv5_rcs() ->
-    [16#00, 16#01, 16#02, 16#04, 16#10, 16#11, 16#18, 16#19,
-     16#80, 16#81, 16#82, 16#83, 16#84, 16#85, 16#86, 16#87,
-     16#88, 16#89, 16#8A, 16#8B, 16#8C, 16#8D, 16#8E, 16#8F,
-     16#90, 16#91, 16#92, 16#93, 16#94, 16#95, 16#96, 16#97,
-     16#98, 16#99, 16#9A, 16#9B, 16#9C, 16#9D, 16#9E, 16#9F,
-     16#A0, 16#A1, 16#A2].
-
-unexpected_rcs() ->
-    ReasonCodes = mqttv3_rcs() ++ mqttv5_rcs(),
-    Unexpected = lists:seq(0, 16#FF) -- ReasonCodes,
-    lists:sublist(Unexpected, 5).
-
-mqttv5_version() ->
-    ?MQTT_PROTO_V5.
-
-mqttv3_version() ->
-    oneof([?MQTT_PROTO_V3, ?MQTT_PROTO_V4]).
-

test/emqx_rpc_SUITE.erl

@@ -1,161 +0,0 @@
-%%--------------------------------------------------------------------
-%% Copyright (c) 2020 EMQ Technologies Co., Ltd. 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.
-%%--------------------------------------------------------------------
-
--module(emqx_rpc_SUITE).
-
--compile(export_all).
--compile(nowarn_export_all).
-
--include_lib("proper/include/proper.hrl").
--include_lib("eunit/include/eunit.hrl").
-
-all() -> emqx_ct:all(?MODULE).
-
-t_prop_rpc(_) ->
-    ok = load(),
-    Opts = [{to_file, user}, {numtests, 10}],
-    {ok, _Apps} = application:ensure_all_started(gen_rpc),
-    ok = application:set_env(gen_rpc, call_receive_timeout, 1),
-    ok = emqx_logger:set_log_level(emergency),
-    ?assert(proper:quickcheck(prop_node(), Opts)),
-    ?assert(proper:quickcheck(prop_node_with_key(), Opts)),
-    ?assert(proper:quickcheck(prop_nodes(), Opts)),
-    ?assert(proper:quickcheck(prop_nodes_with_key(), Opts)),
-    ok = application:stop(gen_rpc),
-    ok = unload().
-
-prop_node() ->
-    ?FORALL(Node, nodename(),
-            begin
-                ?assert(emqx_rpc:cast(Node, erlang, system_time, [])),
-                case emqx_rpc:call(Node, erlang, system_time, []) of
-                    {badrpc, _Reason} -> true;
-                    Delivery when is_integer(Delivery) -> true;
-                    _Other -> false
-                end
-            end).
-
-prop_node_with_key() ->
-    ?FORALL({Node, Key}, nodename_with_key(),
-            begin
-                ?assert(emqx_rpc:cast(Key, Node, erlang, system_time, [])),
-                case emqx_rpc:call(Key, Node, erlang, system_time, []) of
-                    {badrpc, _Reason} -> true;
-                    Delivery when is_integer(Delivery) -> true;
-                    _Other -> false
-                end
-            end).
-
-prop_nodes() ->
-    ?FORALL(Nodes, nodesname(),
-            begin
-                case emqx_rpc:multicall(Nodes, erlang, system_time, []) of
-                    {badrpc, _Reason} -> true;
-                    {RealResults, RealBadNodes}
-                      when is_list(RealResults);
-                           is_list(RealBadNodes) ->
-                        true;
-                    _Other -> false
-                end
-            end).
-
-prop_nodes_with_key() ->
-    ?FORALL({Nodes, Key}, nodesname_with_key(),
-            begin
-                case emqx_rpc:multicall(Key, Nodes, erlang, system_time, []) of
-                    {badrpc, _Reason} -> true;
-                    {RealResults, RealBadNodes}
-                      when is_list(RealResults);
-                           is_list(RealBadNodes) ->
-                        true;
-                    _Other -> false
-                end
-            end).
-
-%%--------------------------------------------------------------------
-%%  helper
-%%--------------------------------------------------------------------
-
-load() ->
-    ok = meck:new(gen_rpc, [passthrough, no_history]),
-    ok = meck:expect(gen_rpc, multicall,
-                     fun(Nodes, Mod, Fun, Args) ->
-                             gen_rpc:multicall(Nodes, Mod, Fun, Args, 1)
-                     end).
-
-unload() ->
-    ok = meck:unload(gen_rpc).
-
-%%--------------------------------------------------------------------
-%% Generator
-%%--------------------------------------------------------------------
-
-nodename() ->
-    ?LET({NodePrefix, HostName},
-         {node_prefix(), hostname()},
-         begin
-             Node = NodePrefix ++ "@" ++ HostName,
-             list_to_atom(Node)
-         end).
-
-nodename_with_key() ->
-    ?LET({NodePrefix, HostName, Key},
-         {node_prefix(), hostname(), choose(0, 10)},
-         begin
-             Node = NodePrefix ++ "@" ++ HostName,
-             {list_to_atom(Node), Key}
-         end).
-
-nodesname() ->
-    oneof([list(nodename()), ['emqxct@127.0.0.1']]).
-
-nodesname_with_key() ->
-    oneof([{list(nodename()), choose(0, 10)}, {['emqxct@127.0.0.1'], 1}]).
-
-node_prefix() ->
-    oneof(["emqxct", text_like()]).
-
-text_like() ->
-    ?SUCHTHAT(Text, list(range($a, $z)), (length(Text) =< 5 andalso length(Text) > 0)).
-
-hostname() ->
-    oneof([ipv4_address(), ipv6_address(), "127.0.0.1", "localhost"]).
-
-ipv4_address() ->
-        ?LET({Num1, Num2, Num3, Num4},
-             { choose(0, 255)
-             , choose(0, 255)
-             , choose(0, 255)
-             , choose(0, 255)},
-             make_ip([Num1, Num2, Num3, Num4], ipv4)).
-
-ipv6_address() ->
-        ?LET({Num1, Num2, Num3, Num4, Num5, Num6},
-             { choose(0, 65535)
-             , choose(0, 65535)
-             , choose(0, 65535)
-             , choose(0, 65535)
-             , choose(0, 65535)
-             , choose(0, 65535)},
-             make_ip([Num1, Num2, Num3, Num4, Num5, Num6], ipv6)).
-
-
-make_ip(NumList, ipv4) when is_list(NumList) ->
-    string:join([integer_to_list(Num) || Num <- NumList], ".");
-make_ip(NumList, ipv6) when is_list(NumList) ->
-    string:join([integer_to_list(Num) || Num <- NumList], ":");
-make_ip(_List, _protocol) ->
-    "127.0.0.1".

test/emqx_session_SUITE.erl

@@ -20,7 +20,6 @@
 -compile(nowarn_export_all).
 
 -include("emqx_mqtt.hrl").
--include_lib("proper/include/proper.hrl").
 -include_lib("eunit/include/eunit.hrl").
 
 all() -> emqx_ct:all(?MODULE).

test/emqx_sys_SUITE.erl

@@ -19,16 +19,8 @@
 -compile(export_all).
 -compile(nowarn_export_all).
 
--include_lib("proper/include/proper.hrl").
 -include_lib("eunit/include/eunit.hrl").
 
--define(mock_modules,
-        [ emqx_metrics
-        , emqx_stats
-        , emqx_broker
-        , ekka_mnesia
-        ]).
-
 all() -> emqx_ct:all(?MODULE).
 
 init_per_suite(Config) ->
@@ -66,95 +58,3 @@ t_uptime(_) ->
 
 % t_info(_) ->
 %     error('TODO').
-
-t_prop_sys(_) ->
-    Opts = [{numtests, 100}, {to_file, user}],
-    ok = load(?mock_modules),
-    ?assert(proper:quickcheck(prop_sys(), Opts)),
-    ok = unload(?mock_modules).
-
-prop_sys() ->
-    ?FORALL(Cmds, commands(?MODULE),
-        begin
-            {ok, _Pid} = emqx_sys:start_link(),
-            {History, State, Result} = run_commands(?MODULE, Cmds),
-            ok = emqx_sys:stop(),
-            ?WHENFAIL(io:format("History: ~p\nState: ~p\nResult: ~p\n",
-                                [History,State,Result]),
-                      aggregate(command_names(Cmds), true))
-        end).
-
-load(Modules) ->
-    [mock(Module) || Module <- Modules],
-    ok.
-
-unload(Modules) ->
-    lists:foreach(fun(Module) ->
-                          ok = meck:unload(Module)
-                  end, Modules).
-
-mock(Module) ->
-    ok = meck:new(Module, [passthrough, no_history]),
-    do_mock(Module).
-
-do_mock(emqx_broker) ->
-    meck:expect(emqx_broker, publish,
-                fun(Msg) -> {node(), <<"test">>, Msg} end),
-    meck:expect(emqx_broker, safe_publish,
-                fun(Msg) -> {node(), <<"test">>, Msg} end);
-do_mock(emqx_stats) ->
-    meck:expect(emqx_stats, getstats, fun() -> [0] end);
-do_mock(ekka_mnesia) ->
-    meck:expect(ekka_mnesia, running_nodes, fun() -> [node()] end);
-do_mock(emqx_metrics) ->
-    meck:expect(emqx_metrics, all, fun() -> [{hello, 3}] end).
-
-unmock() ->
-    meck:unload(emqx_broker).
-
-%%%%%%%%%%%%%
-%%% MODEL %%%
-%%%%%%%%%%%%%
-%% @doc Initial model value at system start. Should be deterministic.
-initial_state() ->
-    #{}.
-
-%% @doc List of possible commands to run against the system
-command(_State) ->
-    oneof([{call, emqx_sys, info, []},
-           {call, emqx_sys, version, []},
-           {call, emqx_sys, uptime, []},
-           {call, emqx_sys, datetime, []},
-           {call, emqx_sys, sysdescr, []},
-           {call, emqx_sys, sys_interval, []},
-           {call, emqx_sys, sys_heatbeat_interval, []},
-           %------------ unexpected message ----------------------%
-           {call, emqx_sys, handle_call, [emqx_sys, other, state]},
-           {call, emqx_sys, handle_cast, [emqx_sys, other]},
-           {call, emqx_sys, handle_info, [info, state]}
-          ]).
-
-precondition(_State, {call, _Mod, _Fun, _Args}) ->
-    timer:sleep(1),
-    true.
-
-postcondition(_State, {call, emqx_sys, info, []}, Info) ->
-    is_list(Info) andalso length(Info) =:= 4;
-postcondition(_State, {call, emqx_sys, version, []}, Version) ->
-    is_list(Version);
-postcondition(_State, {call, emqx_sys, uptime, []}, Uptime) ->
-    is_list(Uptime);
-postcondition(_State, {call, emqx_sys, datetime, []}, Datetime) ->
-    is_list(Datetime);
-postcondition(_State, {call, emqx_sys, sysdescr, []}, Sysdescr) ->
-    is_list(Sysdescr);
-postcondition(_State, {call, emqx_sys, sys_interval, []}, SysInterval) ->
-    is_integer(SysInterval) andalso SysInterval > 0;
-postcondition(_State, {call, emqx_sys, sys_heartbeat_interval, []}, SysHeartInterval) ->
-    is_integer(SysHeartInterval) andalso SysHeartInterval > 0;
-postcondition(_State, {call, _Mod, _Fun, _Args}, _Res) ->
-    true.
-
-next_state(State, _Res, {call, _Mod, _Fun, _Args}) ->
-    NewState = State,
-    NewState.

test/emqx_base62_SUITE.erl

@@ -14,24 +14,14 @@
 %% limitations under the License.
 %%--------------------------------------------------------------------
 
--module(emqx_base62_SUITE).
-
--compile(export_all).
--compile(nowarn_export_all).
+-module(prop_emqx_base62).
 
 -include_lib("proper/include/proper.hrl").
--include_lib("eunit/include/eunit.hrl").
-
-all() -> emqx_ct:all(?MODULE).
 
-t_proper_base62(_) ->
-    Opts = [{numtests, 100}, {to_file, user}],
-    ?assert(proper:quickcheck(prop_symmetric(), Opts)),
-    ?assert(proper:quickcheck(prop_size(), Opts)).
+%%--------------------------------------------------------------------
+%% Properties
+%%--------------------------------------------------------------------
 
-%%%%%%%%%%%%%%%%%%
-%%% Properties %%%
-%%%%%%%%%%%%%%%%%%
 prop_symmetric() ->
     ?FORALL(Data, raw_data(),
         begin
@@ -46,9 +36,10 @@ prop_size() ->
              base62_size(Data, Encoded)
          end).
 
-%%%%%%%%%%%%%%%
-%%% Helpers %%%
-%%%%%%%%%%%%%%%
+%%--------------------------------------------------------------------
+%% Helpers
+%%--------------------------------------------------------------------
+
 to_binary(Data) when is_list(Data) ->
     unicode:characters_to_binary(Data);
 to_binary(Data) when is_integer(Data) ->
@@ -73,7 +64,9 @@ base62_size(Data, Encoded) ->
             EncodedSize >= RangeStart andalso EncodedSize =< RangeEnd
     end.
 
-%%%%%%%%%%%%%%%%%%
-%%% Generators %%%
-%%%%%%%%%%%%%%%%%%
-raw_data() -> oneof([integer(), string(), binary()]).
+%%--------------------------------------------------------------------
+%% Generators
+%%--------------------------------------------------------------------
+
+raw_data() ->
+    oneof([integer(), string(), binary()]).

test/props/prop_emqx_frame.erl

@@ -0,0 +1,62 @@
+%%--------------------------------------------------------------------
+%% Copyright (c) 2020 EMQ Technologies Co., Ltd. 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.
+%%--------------------------------------------------------------------
+
+-module(prop_emqx_frame).
+
+-include("emqx_mqtt.hrl").
+-include_lib("proper/include/proper.hrl").
+
+%%--------------------------------------------------------------------
+%% Properties
+%%--------------------------------------------------------------------
+
+prop_serialize_parse_connect() ->
+    ?FORALL(Opts = #{version := ProtoVer}, parse_opts(),
+            begin
+                ProtoName = proplists:get_value(ProtoVer, ?PROTOCOL_NAMES),
+                Packet = ?CONNECT_PACKET(#mqtt_packet_connect{
+                                            proto_name   = ProtoName,
+                                            proto_ver    = ProtoVer,
+                                            clientid     = <<"clientId">>,
+                                            will_qos     = ?QOS_1,
+                                            will_flag    = true,
+                                            will_retain  = true,
+                                            will_topic   = <<"will">>,
+                                            will_props   = #{},
+                                            will_payload = <<"bye">>,
+                                            clean_start  = true,
+                                            properties = #{}
+                                           }),
+                Packet =:= parse_serialize(Packet, Opts)
+            end).
+
+%%--------------------------------------------------------------------
+%% Helpers
+%%--------------------------------------------------------------------
+
+parse_serialize(Packet, Opts) when is_map(Opts) ->
+    Ver = maps:get(version, Opts, ?MQTT_PROTO_V4),
+    Bin = iolist_to_binary(emqx_frame:serialize(Packet, Ver)),
+    ParseState = emqx_frame:initial_parse_state(Opts),
+    {ok, NPacket, <<>>, _} = emqx_frame:parse(Bin, ParseState),
+    NPacket.
+
+%%--------------------------------------------------------------------
+%% Generators
+%%--------------------------------------------------------------------
+
+parse_opts() ->
+    ?LET(PropList, [{strict_mode, boolean()}, {version, range(4,5)}], maps:from_list(PropList)).

test/emqx_psk_SUITE.erl

@@ -14,48 +14,46 @@
 %% limitations under the License.
 %%--------------------------------------------------------------------
 
--module(emqx_psk_SUITE).
 
--compile(export_all).
--compile(nowarn_export_all).
+-module(prop_emqx_psk).
 
 -include_lib("proper/include/proper.hrl").
--include_lib("eunit/include/eunit.hrl").
--include_lib("common_test/include/ct.hrl").
 
-all() -> emqx_ct:all(?MODULE).
+-define(ALL(Vars, Types, Exprs),
+        ?SETUP(fun() ->
+            State = do_setup(),
+            fun() -> do_teardown(State) end
+         end, ?FORALL(Vars, Types, Exprs))).
 
-t_lookup(_) ->
-    ok = load(),
-    ok = emqx_logger:set_log_level(emergency),
-    Opts = [{to_file, user}, {numtests, 10}],
-    ?assert(proper:quickcheck(prop_lookup(), Opts)),
-    ok = unload(),
-    ok = emqx_logger:set_log_level(error).
+%%--------------------------------------------------------------------
+%% Properties
+%%--------------------------------------------------------------------
 
 prop_lookup() ->
-    ?FORALL({ClientPSKID, UserState},
-            {client_pskid(), user_state()},
-            begin
-                case emqx_psk:lookup(psk, ClientPSKID, UserState) of
-                    {ok, _Result} -> true;
-                    error -> true;
-                    _Other -> false
-                end
-            end).
+    ?ALL({ClientPSKID, UserState},
+         {client_pskid(), user_state()},
+         begin
+             case emqx_psk:lookup(psk, ClientPSKID, UserState) of
+                 {ok, _Result} -> true;
+                 error -> true;
+                 _Other -> false
+             end
+         end).
 
 %%--------------------------------------------------------------------
 %% Helper
 %%--------------------------------------------------------------------
 
-load() ->
+do_setup() ->
+    ok = emqx_logger:set_log_level(emergency),
     ok = meck:new(emqx_hooks, [passthrough, no_history]),
     ok = meck:expect(emqx_hooks, run_fold,
                     fun('tls_handshake.psk_lookup', [ClientPSKID], not_found) ->
                             unicode:characters_to_binary(ClientPSKID)
                     end).
 
-unload() ->
+do_teardown(_) ->
+    ok = emqx_logger:set_log_level(error),
     ok = meck:unload(emqx_hooks).
 
 %%--------------------------------------------------------------------
@@ -65,3 +63,4 @@ unload() ->
 client_pskid() -> oneof([string(), integer(), [1, [-1]]]).
 
 user_state() -> term().
+

test/props/prop_emqx_reason_codes.erl

@@ -0,0 +1,123 @@
+%%--------------------------------------------------------------------
+%% Copyright (c) 2020 EMQ Technologies Co., Ltd. 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.
+%%--------------------------------------------------------------------
+
+-module(prop_emqx_reason_codes).
+
+-include("emqx_mqtt.hrl").
+-include_lib("proper/include/proper.hrl").
+
+%%--------------------------------------------------------------------
+%% Properties
+%%--------------------------------------------------------------------
+
+prop_name_text() ->
+    ?FORALL(UnionArgs, union_args(),
+            is_atom(apply_fun(name, UnionArgs)) andalso
+            is_binary(apply_fun(text, UnionArgs))).
+
+prop_compat() ->
+    ?FORALL(CompatArgs, compat_args(),
+            begin
+                Result = apply_fun(compat, CompatArgs),
+                is_number(Result) orelse Result =:= undefined
+            end).
+
+prop_connack_error() ->
+    ?FORALL(CONNACK_ERROR_ARGS, connack_error_args(),
+            is_integer(apply_fun(connack_error, CONNACK_ERROR_ARGS))).
+
+%%--------------------------------------------------------------------
+%% Helper
+%%--------------------------------------------------------------------
+
+apply_fun(Fun, Args) ->
+    apply(emqx_reason_codes, Fun, Args).
+
+%%--------------------------------------------------------------------
+%% Generator
+%%--------------------------------------------------------------------
+
+union_args() ->
+    frequency([{6, [real_mqttv3_rc(), mqttv3_version()]},
+               {43, [real_mqttv5_rc(), mqttv5_version()]}]).
+
+compat_args() ->
+    frequency([{18, [connack, compat_rc()]},
+               {2, [suback, compat_rc()]},
+               {1, [unsuback, compat_rc()]}]).
+
+connack_error_args() ->
+    [frequency([{10, connack_error()},
+                {1, unexpected_connack_error()}])].
+
+connack_error() ->
+    oneof([client_identifier_not_valid,
+           bad_username_or_password,
+           bad_clientid_or_password,
+           username_or_password_undefined,
+           password_error,
+           not_authorized,
+           server_unavailable,
+           server_busy,
+           banned,
+           bad_authentication_method]).
+
+unexpected_connack_error() ->
+    oneof([who_knows]).
+
+
+real_mqttv3_rc() ->
+    frequency([{6, mqttv3_rc()},
+               {1, unexpected_rc()}]).
+
+real_mqttv5_rc() ->
+    frequency([{43, mqttv5_rc()},
+               {2, unexpected_rc()}]).
+
+compat_rc() ->
+    frequency([{95, ?SUCHTHAT(RC , mqttv5_rc(), RC >= 16#80 orelse RC =< 2)},
+               {5, unexpected_rc()}]).
+
+mqttv3_rc() ->
+    oneof(mqttv3_rcs()).
+
+mqttv5_rc() ->
+    oneof(mqttv5_rcs()).
+
+unexpected_rc() ->
+    oneof(unexpected_rcs()).
+
+mqttv3_rcs() ->
+    [0, 1, 2, 3, 4, 5].
+
+mqttv5_rcs() ->
+    [16#00, 16#01, 16#02, 16#04, 16#10, 16#11, 16#18, 16#19,
+     16#80, 16#81, 16#82, 16#83, 16#84, 16#85, 16#86, 16#87,
+     16#88, 16#89, 16#8A, 16#8B, 16#8C, 16#8D, 16#8E, 16#8F,
+     16#90, 16#91, 16#92, 16#93, 16#94, 16#95, 16#96, 16#97,
+     16#98, 16#99, 16#9A, 16#9B, 16#9C, 16#9D, 16#9E, 16#9F,
+     16#A0, 16#A1, 16#A2].
+
+unexpected_rcs() ->
+    ReasonCodes = mqttv3_rcs() ++ mqttv5_rcs(),
+    Unexpected = lists:seq(0, 16#FF) -- ReasonCodes,
+    lists:sublist(Unexpected, 5).
+
+mqttv5_version() ->
+    ?MQTT_PROTO_V5.
+
+mqttv3_version() ->
+    oneof([?MQTT_PROTO_V3, ?MQTT_PROTO_V4]).

test/props/prop_emqx_rpc.erl

@@ -0,0 +1,132 @@
+%%--------------------------------------------------------------------
+%% Copyright (c) 2020 EMQ Technologies Co., Ltd. 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.
+%%--------------------------------------------------------------------
+
+-module(prop_emqx_rpc).
+
+-include_lib("proper/include/proper.hrl").
+-include_lib("eunit/include/eunit.hrl").
+
+-define(ALL(Vars, Types, Exprs),
+        ?SETUP(fun() ->
+            State = do_setup(),
+            fun() -> do_teardown(State) end
+         end, ?FORALL(Vars, Types, Exprs))).
+
+%%--------------------------------------------------------------------
+%% Properties
+%%--------------------------------------------------------------------
+
+prop_node() ->
+    ?ALL(Node, nodename(),
+         begin
+             ?assert(emqx_rpc:cast(Node, erlang, system_time, [])),
+             case emqx_rpc:call(Node, erlang, system_time, []) of
+                 {badrpc, _Reason} -> true;
+                 Delivery when is_integer(Delivery) -> true;
+                 _Other -> false
+             end
+         end).
+
+prop_node_with_key() ->
+    ?ALL({Node, Key}, nodename_with_key(),
+         begin
+             ?assert(emqx_rpc:cast(Key, Node, erlang, system_time, [])),
+             case emqx_rpc:call(Key, Node, erlang, system_time, []) of
+                 {badrpc, _Reason} -> true;
+                 Delivery when is_integer(Delivery) -> true;
+                 _Other -> false
+             end
+         end).
+
+prop_nodes() ->
+    ?ALL(Nodes, nodesname(),
+         begin
+             case emqx_rpc:multicall(Nodes, erlang, system_time, []) of
+                 {badrpc, _Reason} -> true;
+                 {RealResults, RealBadNodes}
+                   when is_list(RealResults);
+                        is_list(RealBadNodes) ->
+                     true;
+                 _Other -> false
+             end
+         end).
+
+prop_nodes_with_key() ->
+    ?ALL({Nodes, Key}, nodesname_with_key(),
+         begin
+             case emqx_rpc:multicall(Key, Nodes, erlang, system_time, []) of
+                 {badrpc, _Reason} -> true;
+                 {RealResults, RealBadNodes}
+                   when is_list(RealResults);
+                        is_list(RealBadNodes) ->
+                     true;
+                 _Other -> false
+             end
+         end).
+
+%%--------------------------------------------------------------------
+%%  Helper
+%%--------------------------------------------------------------------
+
+do_setup() ->
+    {ok, _Apps} = application:ensure_all_started(gen_rpc),
+    ok = application:set_env(gen_rpc, call_receive_timeout, 1),
+    ok = emqx_logger:set_log_level(emergency),
+    ok = meck:new(gen_rpc, [passthrough, no_history]),
+    ok = meck:expect(gen_rpc, multicall,
+                     fun(Nodes, Mod, Fun, Args) ->
+                             gen_rpc:multicall(Nodes, Mod, Fun, Args, 1)
+                     end).
+
+do_teardown(_) ->
+    ok = emqx_logger:set_log_level(debug),
+    ok = application:stop(gen_rpc),
+    ok = meck:unload(gen_rpc).
+
+%%--------------------------------------------------------------------
+%% Generator
+%%--------------------------------------------------------------------
+
+nodename() ->
+    ?LET({NodePrefix, HostName},
+         {node_prefix(), hostname()},
+         begin
+             Node = NodePrefix ++ "@" ++ HostName,
+             list_to_atom(Node)
+         end).
+
+nodename_with_key() ->
+    ?LET({NodePrefix, HostName, Key},
+         {node_prefix(), hostname(), choose(0, 10)},
+         begin
+             Node = NodePrefix ++ "@" ++ HostName,
+             {list_to_atom(Node), Key}
+         end).
+
+nodesname() ->
+    oneof([list(nodename()), [node()]]).
+
+nodesname_with_key() ->
+    oneof([{list(nodename()), choose(0, 10)}, {[node()], 1}]).
+
+node_prefix() ->
+    oneof(["emqxct", text_like()]).
+
+text_like() ->
+    ?SUCHTHAT(Text, list(range($a, $z)), (length(Text) =< 5 andalso length(Text) > 0)).
+
+hostname() ->
+    oneof(["127.0.0.1", "localhost"]).

test/props/prop_emqx_sys.erl

@@ -0,0 +1,133 @@
+%%--------------------------------------------------------------------
+%% Copyright (c) 2020 EMQ Technologies Co., Ltd. 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.
+%%--------------------------------------------------------------------
+
+-module(prop_emqx_sys).
+
+-include_lib("proper/include/proper.hrl").
+
+-export([ initial_state/0
+        , command/1
+        , precondition/2
+        , postcondition/3
+        , next_state/3
+        ]).
+
+-define(mock_modules,
+        [ emqx_metrics
+        , emqx_stats
+        , emqx_broker
+        , ekka_mnesia
+        ]).
+
+-define(ALL(Vars, Types, Exprs),
+        ?SETUP(fun() ->
+            State = do_setup(),
+            fun() -> do_teardown(State) end
+         end, ?FORALL(Vars, Types, Exprs))).
+
+%%--------------------------------------------------------------------
+%% Properties
+%%--------------------------------------------------------------------
+
+prop_sys() ->
+    ?ALL(Cmds, commands(?MODULE),
+        begin
+            {ok, _Pid} = emqx_sys:start_link(),
+            {History, State, Result} = run_commands(?MODULE, Cmds),
+            ok = emqx_sys:stop(),
+            ?WHENFAIL(io:format("History: ~p\nState: ~p\nResult: ~p\n",
+                                [History,State,Result]),
+                      aggregate(command_names(Cmds), true))
+        end).
+
+%%--------------------------------------------------------------------
+%% Helpers
+%%--------------------------------------------------------------------
+
+do_setup() ->
+    ok = emqx_logger:set_log_level(emergency),
+    [mock(Mod) || Mod <- ?mock_modules],
+    ok.
+
+do_teardown(_) ->
+    ok = emqx_logger:set_log_level(error),
+    [ok = meck:unload(Mod) || Mod <- ?mock_modules],
+    ok.
+
+mock(Module) ->
+    ok = meck:new(Module, [passthrough, no_history]),
+    do_mock(Module).
+
+do_mock(emqx_broker) ->
+    meck:expect(emqx_broker, publish,
+                fun(Msg) -> {node(), <<"test">>, Msg} end),
+    meck:expect(emqx_broker, safe_publish,
+                fun(Msg) -> {node(), <<"test">>, Msg} end);
+do_mock(emqx_stats) ->
+    meck:expect(emqx_stats, getstats, fun() -> [0] end);
+do_mock(ekka_mnesia) ->
+    meck:expect(ekka_mnesia, running_nodes, fun() -> [node()] end);
+do_mock(emqx_metrics) ->
+    meck:expect(emqx_metrics, all, fun() -> [{hello, 3}] end).
+
+%%--------------------------------------------------------------------
+%% MODEL
+%%--------------------------------------------------------------------
+
+%% @doc Initial model value at system start. Should be deterministic.
+initial_state() ->
+    #{}.
+
+%% @doc List of possible commands to run against the system
+command(_State) ->
+    oneof([{call, emqx_sys, info, []},
+           {call, emqx_sys, version, []},
+           {call, emqx_sys, uptime, []},
+           {call, emqx_sys, datetime, []},
+           {call, emqx_sys, sysdescr, []},
+           {call, emqx_sys, sys_interval, []},
+           {call, emqx_sys, sys_heatbeat_interval, []},
+           %------------ unexpected message ----------------------%
+           {call, emqx_sys, handle_call, [emqx_sys, other, state]},
+           {call, emqx_sys, handle_cast, [emqx_sys, other]},
+           {call, emqx_sys, handle_info, [info, state]}
+          ]).
+
+precondition(_State, {call, _Mod, _Fun, _Args}) ->
+    timer:sleep(1),
+    true.
+
+postcondition(_State, {call, emqx_sys, info, []}, Info) ->
+    is_list(Info) andalso length(Info) =:= 4;
+postcondition(_State, {call, emqx_sys, version, []}, Version) ->
+    is_list(Version);
+postcondition(_State, {call, emqx_sys, uptime, []}, Uptime) ->
+    is_list(Uptime);
+postcondition(_State, {call, emqx_sys, datetime, []}, Datetime) ->
+    is_list(Datetime);
+postcondition(_State, {call, emqx_sys, sysdescr, []}, Sysdescr) ->
+    is_list(Sysdescr);
+postcondition(_State, {call, emqx_sys, sys_interval, []}, SysInterval) ->
+    is_integer(SysInterval) andalso SysInterval > 0;
+postcondition(_State, {call, emqx_sys, sys_heartbeat_interval, []}, SysHeartInterval) ->
+    is_integer(SysHeartInterval) andalso SysHeartInterval > 0;
+postcondition(_State, {call, _Mod, _Fun, _Args}, _Res) ->
+    true.
+
+next_state(State, _Res, {call, _Mod, _Fun, _Args}) ->
+    NewState = State,
+    NewState.
+