From 241c4775a5e56cbe9006ae90d0fab0f263bc6461 Mon Sep 17 00:00:00 2001 From: William Yang Date: Fri, 16 Feb 2024 16:05:23 +0100 Subject: [PATCH] test(prop): stateful client connection --- c_src/quicer_stream.c | 2 +- include/quicer_types.hrl | 6 +- test/prop_quic_types.hrl | 155 ++++++++++++ test/prop_quicer_nif.erl | 462 +++--------------------------------- test/prop_stateful_conn.erl | 219 +++++++++++++++++ test/quicer_prop_gen.erl | 336 ++++++++++++++++++++++++++ 6 files changed, 752 insertions(+), 428 deletions(-) create mode 100644 test/prop_quic_types.hrl create mode 100644 test/prop_stateful_conn.erl create mode 100644 test/quicer_prop_gen.erl diff --git a/c_src/quicer_stream.c b/c_src/quicer_stream.c index cab3fc5a..0acbadcf 100644 --- a/c_src/quicer_stream.c +++ b/c_src/quicer_stream.c @@ -475,7 +475,7 @@ csend4(ErlNifEnv *env, int argc, const ERL_NIF_TERM argv[]) { if (!enif_get_uint(env, eopen_flag, &open_flag)) { - // if set must be valid. + // if set, must be valid. return ERROR_TUPLE_2(ATOM_BADARG); } } diff --git a/include/quicer_types.hrl b/include/quicer_types.hrl index 5c83a68a..de9f977e 100644 --- a/include/quicer_types.hrl +++ b/include/quicer_types.hrl @@ -220,13 +220,15 @@ %% is sync send or not -type send_flags() :: + csend_flags() | ?QUICER_SEND_FLAG_SYNC. + +-type csend_flags() :: ?QUIC_SEND_FLAG_NONE | ?QUIC_SEND_FLAG_ALLOW_0_RTT | ?QUIC_SEND_FLAG_START | ?QUIC_SEND_FLAG_FIN | ?QUIC_SEND_FLAG_DGRAM_PRIORITY - | ?QUIC_SEND_FLAG_DELAY_SEND - | ?QUICER_SEND_FLAG_SYNC. + | ?QUIC_SEND_FLAG_DELAY_SEND. -type stream_start_flag() :: ?QUIC_STREAM_START_FLAG_NONE diff --git a/test/prop_quic_types.hrl b/test/prop_quic_types.hrl new file mode 100644 index 00000000..abbb6560 --- /dev/null +++ b/test/prop_quic_types.hrl @@ -0,0 +1,155 @@ +%%-------------------------------------------------------------------- +%% Copyright (c) 2024 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. +%%-------------------------------------------------------------------- + +-record(prop_handle, { + type :: reg | listen | conn | stream, + name :: string(), + handle :: reference(), + destructor :: fun() +}). + +-define(dummy_listener, dummy_listener). +-define(DUMMY_PORT, 14567). + +-define(valid_flags(FlagType), + (?SUCHTHAT( + Flag, + ?LET( + Flags, + [FlagType], + begin + lists:foldl( + fun(F, Acc) -> + Acc bor F + end, + 0, + Flags + ) + end + ), + Flag =/= 0 + )) +). + +-type quicer_listen_opts() :: [listen_opt()]. + +-type listen_opt() :: + {alpn, [alpn()]} + | {cert, file:filename()} + | {certfile, file:filename()} + %-| {key, file:filename()}. %% @FIXME reflect in types + | {keyfile, file:filename()} + | {verify, none | peer | verify_peer | verify_none} + | {cacertfile, file:filename()} + | {password, string()} + | {sslkeylogfile, file:filename()} + | {allow_insecure, boolean()} + %-| {quic_registration, reg_handle()} + | {conn_acceptors, non_neg_integer()} + | {settings, [quicer_setting()]}. + +-type quicer_setting() :: + {max_bytes_per_key, uint64()} + | {handshake_idle_timeout_ms, uint64()} + | {idle_timeout_ms, uint64()} + | {tls_client_max_send_buffer, uint32()} + | {tls_server_max_send_buffer, uint32()} + | {stream_recv_window_default, uint32()} + | {stream_recv_buffer_default, uint32()} + | {conn_flow_control_window, uint32()} + | {max_stateless_operations, uint32()} + | {initial_window_packets, uint32()} + | {send_idle_timeout_ms, uint32()} + | {initial_rtt_ms, uint32()} + | {max_ack_delay_ms, uint32()} + | {disconnect_timeout_ms, uint32()} + | {keep_alive_interval_ms, uint32()} + | {peer_bidi_stream_count, uint16()} + | {peer_unidi_stream_count, uint16()} + | {retry_memory_limit, uint16()} + | {load_balancing_mode, uint16()} + | {max_operations_per_drain, uint8()} + | {send_buffering_enabled, uint8()} + | {pacing_enabled, uint8()} + | {migration_enabled, uint8()} + | {datagram_receive_enabled, uint8()} + | {server_resumption_level, 0 | 1 | 2} + | {minimum_mtu, uint16()} + | {maximum_mtu, uint16()} + | {mtu_discovery_search_complete_timeout_us, uint64()} + | {mtu_discovery_missing_probe_count, uint8()} + | {max_binding_stateless_operations, uint16()} + | {stateless_operation_expiration_ms, uint16()}. + +-type quicer_conn_opts() :: [conn_opt()]. +-type conn_opt() :: + {alpn, [string()]} + | {certfile, file:filename()} + | {keyfile, file:filename()} + | {password, string()} + | {verify, none | peer} + | {nst, binary()} + | {cacertfile, file:filename()} + | {sslkeylogfile, file:filename()} + | {local_bidi_stream_count, uint16()} + | {local_unidi_stream_count, uint16()} + | {handshake_idle_timeout_ms, non_neg_integer()} + | {quic_event_mask, uint32()} + | {disable_1rtt_encryption, boolean()} + | {quic_version, uint32()} + | {local_address, string()} + | {remote_address, string()} + | {ideal_processor, uint16()} + | {settings, [quicer_setting()]} + % @TODO + | {statistics, any()} + % @TODO + | {statistics_plat, any()} + | {share_udp_binding, boolean()} + | {max_stream_ids, uint64()} + | {close_reason_phrase, string()} + | {stream_scheduling_scheme, uint16()} + | {datagram_receive_enabled, boolean()} + | {datagram_send_enabled, boolean()} + | {resumption_ticket, [uint8()]} + | {peer_certificate_valid, boolean()} + | {local_interface, uint32()} + % @TODO + | {tls_secrets, binary()} + % @TODO + | {version_settings, any()} + | {cibir_id, [uint8()]} + % @TODO + | {statistics_v2, any()} + % @TODO + | {statistics_v2_plat, any()}. + +-type quicer_acceptor_opts() :: [acceptor_opt()]. +-type acceptor_opt() :: + {active, active_n()} + | quicer_setting(). + +-type quicer_stream_opts() :: [stream_opt()]. +-type stream_opt() :: + {active, active_n()} + | {stream_id, uint62()} + | {priority, uint16()} + | {ideal_send_buffer_size, uint64()} + | {'0rtt_length', uint64()} + | {open_flag, stream_open_flags()} + | {start_flag, stream_start_flags()} + | {event_mask, uint32()} + | {disable_fpbuffer, boolean()}. diff --git a/test/prop_quicer_nif.erl b/test/prop_quicer_nif.erl index 59ea3350..3d37b21b 100644 --- a/test/prop_quicer_nif.erl +++ b/test/prop_quicer_nif.erl @@ -1,150 +1,46 @@ +%%-------------------------------------------------------------------- +%% Copyright (c) 2024 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_quicer_nif). - -include_lib("proper/include/proper.hrl"). -include_lib("quicer/include/quicer_types.hrl"). +-include("prop_quic_types.hrl"). --record(prop_handle, { - type :: reg | listen | conn | stream, - name :: string(), - handle :: reference(), - destructor :: fun() -}). - --define(dummy_listener, dummy_listener). --define(DUMMY_PORT, 14567). - --define(valid_flags(FlagType), - (?SUCHTHAT( - Flag, - ?LET( - Flags, - [FlagType], - begin - lists:foldl( - fun(F, Acc) -> - Acc bor F - end, - 0, - Flags - ) - end - ), - Flag =/= 0 - )) +-import( + quicer_prop_gen, + [ + valid_client_conn_opts/0, + valid_server_listen_opts/0, + valid_stream_shutdown_flags/0, + valid_stream_start_flags/0, + valid_stream_handle/0, + valid_started_connection_handle/0, + valid_opened_connection_handle/0, + valid_connection_handle/0, + valid_listen_on/0, + valid_listen_opts/0, + valid_listen_handle/0, + valid_global_handle/0, + valid_reg_handle/0, + valid_handle/0, + pid/0, + data/0, + quicer_send_flags/0 + ] ). --type quicer_listen_opts() :: [listen_opt()]. - --type listen_opt() :: - {alpn, [alpn()]} - | {cert, file:filename()} - | {certfile, file:filename()} - %-| {key, file:filename()}. %% @FIXME reflect in types - | {keyfile, file:filename()} - | {verify, none | peer | verify_peer | verify_none} - | {cacertfile, file:filename()} - | {password, string()} - | {sslkeylogfile, file:filename()} - | {allow_insecure, boolean()} - %-| {quic_registration, reg_handle()} - | {conn_acceptors, non_neg_integer()} - | {settings, [quicer_setting()]}. - --type quicer_setting() :: - {max_bytes_per_key, uint64()} - | {handshake_idle_timeout_ms, uint64()} - | {idle_timeout_ms, uint64()} - | {tls_client_max_send_buffer, uint32()} - | {tls_server_max_send_buffer, uint32()} - | {stream_recv_window_default, uint32()} - | {stream_recv_buffer_default, uint32()} - | {conn_flow_control_window, uint32()} - | {max_stateless_operations, uint32()} - | {initial_window_packets, uint32()} - | {send_idle_timeout_ms, uint32()} - | {initial_rtt_ms, uint32()} - | {max_ack_delay_ms, uint32()} - | {disconnect_timeout_ms, uint32()} - | {keep_alive_interval_ms, uint32()} - | {peer_bidi_stream_count, uint16()} - | {peer_unidi_stream_count, uint16()} - | {retry_memory_limit, uint16()} - | {load_balancing_mode, uint16()} - | {max_operations_per_drain, uint8()} - | {send_buffering_enabled, uint8()} - | {pacing_enabled, uint8()} - | {migration_enabled, uint8()} - | {datagram_receive_enabled, uint8()} - | {server_resumption_level, 0 | 1 | 2} - | {minimum_mtu, uint16()} - | {maximum_mtu, uint16()} - | {mtu_discovery_search_complete_timeout_us, uint64()} - | {mtu_discovery_missing_probe_count, uint8()} - | {max_binding_stateless_operations, uint16()} - | {stateless_operation_expiration_ms, uint16()}. - --type quicer_conn_opts() :: [conn_opt()]. --type conn_opt() :: - {alpn, [string()]} - | {cert, file:filename()} - | {certfile, file:filename()} - | {key, file:filename()} - | {keyfile, file:filename()} - | {password, string()} - | {verify, none | peer} - | {nst, binary()} - | {cacertfile, file:filename()} - | {sslkeylogfile, file:filename()} - | {local_bidi_stream_count, uint16()} - | {local_unidi_stream_count, uint16()} - | {handshake_idle_timeout_ms, non_neg_integer()} - | {quic_event_mask, uint32()} - | {disable_1rtt_encryption, boolean()} - | {quic_version, uint32()} - | {local_address, string()} - | {remote_address, string()} - | {ideal_processor, uint16()} - | {settings, [quicer_setting()]} - % @TODO - | {statistics, any()} - % @TODO - | {statistics_plat, any()} - | {share_udp_binding, boolean()} - | {max_stream_ids, uint64()} - | {close_reason_phrase, string()} - | {stream_scheduling_scheme, uint16()} - | {datagram_receive_enabled, boolean()} - | {datagram_send_enabled, boolean()} - | {resumption_ticket, [uint8()]} - | {peer_certificate_valid, boolean()} - | {local_interface, uint32()} - % @TODO - | {tls_secrets, binary()} - % @TODO - | {version_settings, any()} - | {cibir_id, [uint8()]} - % @TODO - | {statistics_v2, any()} - % @TODO - | {statistics_v2_plat, any()}. - --type quicer_acceptor_opts() :: [acceptor_opt()]. --type acceptor_opt() :: - {active, active_n()} - | quicer_setting(). - --type quicer_stream_opts() :: [stream_opt()]. --type stream_opt() :: - {active, active_n()} - | {stream_id, uint62()} - | {priority, uint16()} - | {ideal_send_buffer_size, uint64()} - | {'0rtt_length', uint64()} - | {open_flag, stream_open_flags()} - | {start_flag, stream_start_flags()} - | {event_mask, uint32()} - | {disable_fpbuffer, boolean()}. - prop_robust_new_registration_2() -> ?FORALL( {Key, Value}, @@ -838,287 +734,3 @@ prop_controlling_process_with_valid_opts() -> %%% ============================================================================ %%% Generators %%% ============================================================================ -valid_handle() -> - oneof([ - valid_connection_handle(), - valid_stream_handle(), - valid_listen_handle(), - valid_reg_handle(), - valid_global_handle() - ]). - -%% @doc pid of process that dies randomly within 0-1000(ms) -pid() -> - ?LET( - LiveTimeMs, - range(0, 1000), - spawn(fun() -> timer:sleep(LiveTimeMs) end) - ). - -data() -> - oneof([binary(), list(binary())]). - -quicer_send_flags() -> - ?LET( - Flags, - [send_flags()], - begin - lists:foldl( - fun(F, Acc) -> - Acc bor F - end, - 0, - Flags - ) - end - ). - -%% valid reg handle -valid_reg_handle() -> - ?SUCHTHAT( - Handle, - ?LET( - {Name, Profile}, - {reg_name(), registration_profile()}, - begin - case quicer_nif:new_registration(Name, Profile) of - {ok, Handle} -> - #prop_handle{ - type = reg, - name = Name, - handle = Handle, - destructor = fun() -> - quicer_nif:close_registration(Handle) - end - }; - {error, _} -> - error - end - end - ), - Handle =/= error - ). - -reg_name() -> - % latin1_string() - ?LET( - Rand, - integer(), - begin - "foo" ++ integer_to_list(Rand) - end - ). - -valid_global_handle() -> - ?LET(_H, integer(), #prop_handle{ - type = global, - handle = quic_global, - destructor = fun() -> ok end - }). - -valid_listen_handle() -> - ?SUCHTHAT( - Ret, - ?LET( - {On, Opts}, - {valid_listen_on(), valid_listen_opts()}, - begin - case quicer_nif:listen(On, maps:from_list(Opts)) of - {ok, Handle} -> - #prop_handle{ - type = listener, - name = "noname", - handle = Handle, - destructor = fun() -> - quicer_nif:close_listener(Handle) - end - }; - _E -> - ct:pal("listen failed: ~p", [_E]), - error - end - end - ), - Ret =/= error - ). - -valid_listen_opts() -> - ?LET( - Opts, - quicer_listen_opts(), - begin - lists:foldl( - fun proplists:delete/2, - Opts ++ valid_server_listen_opts(), - [ - password, - %% flaky per machine sysconf - stream_recv_buffer_default - ] - ) - end - ). - -valid_listen_on() -> - ?LET( - Port, - range(1025, 65536), - begin - case gen_udp:open(Port, [{reuseaddr, true}]) of - {ok, S} -> - ok = gen_udp:close(S), - Port; - _ -> - quicer_test_lib:select_free_port(quic) - end - end - ). - -%% @doc valid conn handle in different states (opened, started, closed) -valid_connection_handle() -> - oneof([ - valid_opened_connection_handle(), - valid_started_connection_handle() - ]). - -valid_opened_connection_handle() -> - ?LET( - _Rand, - integer(), - begin - {ok, Handle} = quicer_nif:open_connection(), - #prop_handle{ - type = conn, - name = "noname", - handle = Handle, - destructor = fun() -> - quicer_nif:async_shutdown_connection(Handle, 0, 0) - end - } - end - ). - -valid_started_connection_handle() -> - ensure_dummy_listener(?DUMMY_PORT), - ?LET( - _Rand, - integer(), - begin - {ok, Handle} = quicer_nif:async_connect( - "localhost", ?DUMMY_PORT, maps:from_list(valid_client_conn_opts()) - ), - #prop_handle{ - type = conn, - name = "noname", - handle = Handle, - destructor = fun() -> - quicer_nif:async_shutdown_connection(Handle, 0, 0) - end - } - end - ). - -valid_stream_handle() -> - ensure_dummy_listener(?DUMMY_PORT), - ?SUCHTHAT( - Conn, - ?LET( - _Rand, - integer(), - begin - {ok, Conn} = quicer_nif:async_connect( - "localhost", ?DUMMY_PORT, maps:from_list(valid_client_conn_opts()) - ), - receive - {quic, connected, Conn, _} -> - {ok, Stream} = quicer_nif:start_stream(Conn, #{active => 1}), - #prop_handle{ - type = stream, - name = "noname", - handle = Stream, - destructor = - fun() -> - quicer_nif:async_shutdown_connection(Conn, 0, 0) - end - } - after 100 -> - %% @FIXME - error - end - end - ), - Conn =/= error - ). - -valid_stream_start_flags() -> - ?valid_flags(stream_start_flag()). - -valid_stream_shutdown_flags() -> - ?valid_flags(stream_shutdown_flags()). - -latin1_string() -> ?SUCHTHAT(S, string(), io_lib:printable_latin1_list(S)). - -%% Other helpers - -%% @doc Server listen opts must work -valid_server_listen_opts() -> - [ - {alpn, ["proper"]}, - {cacertfile, "./msquic/submodules/openssl/test/certs/rootCA.pem"}, - {certfile, "./msquic/submodules/openssl/test/certs/servercert.pem"}, - {keyfile, "./msquic/submodules/openssl/test/certs/serverkey.pem"} - ]. - -valid_client_conn_opts() -> - [ - {alpn, ["proper"]}, - {cacertfile, "./msquic/submodules/openssl/test/certs/rootCA.pem"}, - {certfile, "./msquic/submodules/openssl/test/certs/servercert.pem"}, - {keyfile, "./msquic/submodules/openssl/test/certs/serverkey.pem"} - ]. - --spec ensure_dummy_listener(non_neg_integer()) -> _. -ensure_dummy_listener(Port) -> - case is_pid(whereis(?dummy_listener)) of - false -> - spawn_dummy_listener(Port); - true -> - ok - end. - -spawn_dummy_listener(Port) -> - Parent = self(), - spawn(fun() -> - register(?dummy_listener, self()), - {ok, L} = quicer_nif:listen(Port, maps:from_list(valid_server_listen_opts())), - spawn_acceptors(L, 4), - Parent ! ready, - receive - finish -> ok - end - end), - receive - ready -> - ok - end. - -spawn_acceptors(_, 0) -> - ok; -spawn_acceptors(L, N) -> - spawn_link(fun() -> - acceptor_loop(L) - end), - spawn_acceptors(L, N - 1). - -acceptor_loop(L) -> - case quicer:accept(L, #{active => true}) of - {ok, Conn} -> - spawn(fun() -> - _ = quicer:handshake(Conn), - timer:sleep(100), - quicer:async_shutdown_connection(Conn, 0, 0) - end), - acceptor_loop(L); - _ -> - acceptor_loop(L) - end. diff --git a/test/prop_stateful_conn.erl b/test/prop_stateful_conn.erl new file mode 100644 index 00000000..b07f0ee1 --- /dev/null +++ b/test/prop_stateful_conn.erl @@ -0,0 +1,219 @@ +%%-------------------------------------------------------------------- +%% Copyright (c) 2024 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_stateful_conn). +-compile([export_all]). +-include_lib("proper/include/proper.hrl"). +-include_lib("quicer/include/quicer_types.hrl"). +-include("prop_quic_types.hrl"). + +%% Model Callbacks +-export([ + command/1, + initial_state/0, + next_state/3, + precondition/2, + postcondition/3 +]). + +%%%%%%%%%%%%%%%%%% +%%% PROPERTIES %%% +%%%%%%%%%%%%%%%%%% +prop_client_state_test(opts) -> + [{numtests, 2000}]. +prop_client_state_test() -> + {ok, _} = listener_start_link(?MODULE), + ?FORALL( + Cmds, + commands(?MODULE), + begin + {History, State, Result} = run_commands(?MODULE, Cmds), + ?WHENFAIL( + io:format( + "History: ~p\nState: ~p\nResult: ~p\n", + [History, State, Result] + ), + aggregate(command_names(Cmds), Result =:= ok) + ) + end + ). + +%%%%%%%%%%%%% +%%% MODEL %%% +%%%%%%%%%%%%% +%% @doc Initial model value at system start. Should be deterministic. +initial_state() -> + {ok, H} = quicer:connect("localhost", 14568, default_conn_opts(), 10000), + #{ + state => connected, + handle => H + }. + +%% @doc List of possible commands to run against the system +%% +command(#{handle := Handle}) -> + oneof([ + {call, quicer, getopt, [Handle, ?LET({Opt, _}, conn_opt(), Opt)]}, + {call, quicer, async_accept_stream, [Handle, ?LET(Opts, quicer_acceptor_opts(), Opts)]}, + {call, quicer, close_connection, [Handle]}, + {call, quicer, async_csend, [ + Handle, + ?LET(Bin, binary(), Bin), + quicer_prop_gen:valid_csend_stream_opts(), + ?valid_flags(send_flags()) + ]}, + {call, quicer, shutdown_connection, [ + Handle, ?valid_flags(conn_shutdown_flag()), ?LET(ErrorCode, uint62(), ErrorCode) + ]} + ]). + +%% @doc Determines whether a command should be valid under the +%% current state. +precondition(#{state := connected}, {call, _Mod, _Fun, _Args}) -> + true; +precondition(#{state := closed}, {call, _Mod, _Fun, _Args}) -> + true; +precondition(_State, {call, _Mod, _Fun, _Args}) -> + false. + +%% @doc Given the state `State' *prior* to the call +%% `{call, Mod, Fun, Args}', determine whether the result +%% `Res' (coming from the actual system) makes sense. +postcondition(_State, {call, quicer, getopt, _Args}, {ok, _}) -> + true; +postcondition(_State, {call, quicer, getopt, [_, password]}, {error, badarg}) -> + true; +postcondition(_State, {call, quicer, getopt, [_, NotSupp]}, {error, not_supported}) when + NotSupp == statistics_plat orelse + NotSupp == resumption_ticket +-> + true; +postcondition(_State, {call, quicer, getopt, [_, SetOnly]}, {error, param_error}) when + SetOnly =:= nst orelse + SetOnly =:= cibir_id orelse + SetOnly =:= cacertfile orelse + SetOnly =:= keyfile orelse + SetOnly =:= certfile orelse + SetOnly =:= password orelse + SetOnly =:= local_interface orelse + SetOnly =:= tls_secrets orelse + SetOnly =:= alpn orelse + SetOnly =:= sslkeylogfile orelse + SetOnly =:= verify orelse + SetOnly =:= handshake_idle_timeout_ms orelse + %% @TODO. unimpl. + SetOnly =:= version_settings orelse + %% @TODO. unimpl. + SetOnly =:= statistics_v2 orelse + %% @TODO. unimpl. + SetOnly =:= statistics_v2_plat orelse + SetOnly =:= quic_event_mask +-> + true; +postcondition(_State, {call, quicer, getopt, [_, SetOnly]}, {error, invalid_parameter}) when + SetOnly =:= local_interface orelse + SetOnly =:= peer_certificate_valid +-> + true; +postcondition(_State, {call, quicer, getopt, [_, close_reason_phrase]}, {error, not_found}) -> + %% @NOTE, msquic returns not_found whne it is not set. + true; +postcondition(_State, {call, quicer, async_csend, _}, {ok, _}) -> + %% relaxed check on csend + true; +postcondition(_State, {call, quicer, async_csend, _Args}, {error, stm_open_error, invalid_state}) -> + true; +postcondition(_State, {call, quicer, async_accept_stream, _Args}, {ok, _}) -> + true; +postcondition( + _State, {call, quicer, async_accept_stream, _Args}, {error, stm_open_error, invalid_state} +) -> + true; +postcondition(_State, {call, quicer, close_connection, _Args}, ok) -> + true; +postcondition(_State, {call, quicer, shutdown_connection, _Args}, ok) -> + true; +%% @FIXME: Fix it in server side callback module, more robust to closed connection +postcondition(_State, {call, quicer, shutdown_connection, _Args}, {error, timeout}) -> + true; +postcondition(_State, {call, quicer, close_connection, [_]}, {error, timeout}) -> + true; +postcondition(#{state := closed}, {call, _Mod, _Fun, _Args} = Call, {error, closed}) -> + true; +postcondition(_State, {call, _Mod, _Fun, _Args} = Call, Res) -> + false. + +%% @doc Assuming the postcondition for a call was true, update the model +%% accordingly for the test to proceed. +next_state(#{state := connected} = State, _Res, {call, quicer, close_connection, _Args}) -> + State#{state := closed}; +next_state(#{state := connected} = State, _Res, {call, quicer, shutdown_connection, _Args}) -> + State#{state := closed}; +next_state(State, _Res, {call, _Mod, _Fun, _Args}) -> + State. + +%%% Generators + +%%%%%%%%%%%%%%%%%%%%%%% +%%% Listener helper %%% +%%%%%%%%%%%%%%%%%%%%%%% +listener_start_link(ListenerName) -> + application:ensure_all_started(quicer), + LPort = 14568, + ListenerOpts = default_listen_opts(), + ConnectionOpts = [ + {conn_callback, quicer_server_conn_callback}, + {stream_acceptors, 32} + | default_conn_opts() + ], + StreamOpts = [ + {stream_callback, quicer_echo_server_stream_callback} + ], + Options = {ListenerOpts, ConnectionOpts, StreamOpts}, + quicer:spawn_listener(ListenerName, LPort, Options). + +%% OS picks the available port +select_port() -> + {ok, S} = gen_udp:open(0, [{reuseaddr, true}]), + {ok, {_, Port}} = inet:sockname(S), + gen_udp:close(S), + Port. + +default_listen_opts() -> + [ + {conn_acceptors, 32}, + {cacertfile, "./msquic/submodules/openssl/test/certs/rootCA.pem"}, + {certfile, "./msquic/submodules/openssl/test/certs/servercert.pem"}, + {keyfile, "./msquic/submodules/openssl/test/certs/serverkey.pem"}, + {alpn, ["prop"]}, + {verify, none}, + {idle_timeout_ms, 0}, + %% some CI runner is slow on this + {handshake_idle_timeout_ms, 10000}, + % QUIC_SERVER_RESUME_AND_ZERORTT + {server_resumption_level, 2}, + {peer_bidi_stream_count, 10} + ]. + +default_conn_opts() -> + [ + {alpn, ["prop"]}, + %% , {sslkeylogfile, "/tmp/SSLKEYLOGFILE"} + {verify, none}, + {idle_timeout_ms, 0}, + {cacertfile, "./msquic/submodules/openssl/test/certs/rootCA.pem"}, + {certfile, "./msquic/submodules/openssl/test/certs/servercert.pem"}, + {keyfile, "./msquic/submodules/openssl/test/certs/serverkey.pem"} + ]. diff --git a/test/quicer_prop_gen.erl b/test/quicer_prop_gen.erl new file mode 100644 index 00000000..75661aa3 --- /dev/null +++ b/test/quicer_prop_gen.erl @@ -0,0 +1,336 @@ +%%-------------------------------------------------------------------- +%% Copyright (c) 2024 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(quicer_prop_gen). + +-export([ + valid_client_conn_opts/0, + valid_server_listen_opts/0, + valid_stream_shutdown_flags/0, + valid_stream_start_flags/0, + valid_stream_handle/0, + valid_started_connection_handle/0, + valid_opened_connection_handle/0, + valid_connection_handle/0, + valid_listen_on/0, + valid_listen_opts/0, + valid_listen_handle/0, + valid_global_handle/0, + valid_reg_handle/0, + valid_handle/0, + valid_csend_stream_opts/0, + pid/0, + data/0, + quicer_send_flags/0 +]). + +-include_lib("proper/include/proper.hrl"). +-include_lib("quicer/include/quicer_types.hrl"). + +-include("prop_quic_types.hrl"). + +valid_handle() -> + oneof([ + valid_connection_handle(), + valid_stream_handle(), + valid_listen_handle(), + valid_reg_handle(), + valid_global_handle() + ]). + +%% @doc pid of process that dies randomly within 0-1000(ms) +pid() -> + ?LET( + LiveTimeMs, + range(0, 1000), + spawn(fun() -> timer:sleep(LiveTimeMs) end) + ). + +data() -> + oneof([binary(), list(binary())]). + +quicer_send_flags() -> + ?LET( + Flags, + [send_flags()], + begin + lists:foldl( + fun(F, Acc) -> + Acc bor F + end, + 0, + Flags + ) + end + ). + +%% valid reg handle +valid_reg_handle() -> + ?SUCHTHAT( + Handle, + ?LET( + {Name, Profile}, + {reg_name(), registration_profile()}, + begin + case quicer_nif:new_registration(Name, Profile) of + {ok, Handle} -> + #prop_handle{ + type = reg, + name = Name, + handle = Handle, + destructor = fun() -> + quicer_nif:close_registration(Handle) + end + }; + {error, _} -> + error + end + end + ), + Handle =/= error + ). + +reg_name() -> + % latin1_string() + ?LET( + Rand, + integer(), + begin + "foo" ++ integer_to_list(Rand) + end + ). + +valid_global_handle() -> + ?LET(_H, integer(), #prop_handle{ + type = global, + handle = quic_global, + destructor = fun() -> ok end + }). + +valid_listen_handle() -> + ?SUCHTHAT( + Ret, + ?LET( + {On, Opts}, + {valid_listen_on(), valid_listen_opts()}, + begin + case quicer_nif:listen(On, maps:from_list(Opts)) of + {ok, Handle} -> + #prop_handle{ + type = listener, + name = "noname", + handle = Handle, + destructor = fun() -> + quicer_nif:close_listener(Handle) + end + }; + _E -> + ct:pal("listen failed: ~p", [_E]), + error + end + end + ), + Ret =/= error + ). + +valid_listen_opts() -> + ?LET( + Opts, + quicer_listen_opts(), + begin + lists:foldl( + fun proplists:delete/2, + Opts ++ valid_server_listen_opts(), + [ + password, + %% flaky per machine sysconf + stream_recv_buffer_default + ] + ) + end + ). + +valid_listen_on() -> + ?LET( + Port, + range(1025, 65536), + begin + case gen_udp:open(Port, [{reuseaddr, true}]) of + {ok, S} -> + ok = gen_udp:close(S), + Port; + _ -> + quicer_test_lib:select_free_port(quic) + end + end + ). + +%% @doc valid conn handle in different states (opened, started, closed) +valid_connection_handle() -> + oneof([ + valid_opened_connection_handle(), + valid_started_connection_handle() + ]). + +valid_opened_connection_handle() -> + ?LET( + _Rand, + integer(), + begin + {ok, Handle} = quicer_nif:open_connection(), + #prop_handle{ + type = conn, + name = "noname", + handle = Handle, + destructor = fun() -> + quicer_nif:async_shutdown_connection(Handle, 0, 0) + end + } + end + ). + +valid_started_connection_handle() -> + ensure_dummy_listener(?DUMMY_PORT), + ?LET( + _Rand, + integer(), + begin + {ok, Handle} = quicer_nif:async_connect( + "localhost", ?DUMMY_PORT, maps:from_list(valid_client_conn_opts()) + ), + #prop_handle{ + type = conn, + name = "noname", + handle = Handle, + destructor = fun() -> + quicer_nif:async_shutdown_connection(Handle, 0, 0) + end + } + end + ). + +valid_stream_handle() -> + ensure_dummy_listener(?DUMMY_PORT), + ?SUCHTHAT( + Conn, + ?LET( + _Rand, + integer(), + begin + {ok, Conn} = quicer_nif:async_connect( + "localhost", ?DUMMY_PORT, maps:from_list(valid_client_conn_opts()) + ), + receive + {quic, connected, Conn, _} -> + {ok, Stream} = quicer_nif:start_stream(Conn, #{active => 1}), + #prop_handle{ + type = stream, + name = "noname", + handle = Stream, + destructor = + fun() -> + quicer_nif:async_shutdown_connection(Conn, 0, 0) + end + } + after 100 -> + %% @FIXME + error + end + end + ), + Conn =/= error + ). + +valid_stream_start_flags() -> + ?valid_flags(stream_start_flag()). + +valid_stream_shutdown_flags() -> + ?valid_flags(stream_shutdown_flags()). + +latin1_string() -> ?SUCHTHAT(S, string(), io_lib:printable_latin1_list(S)). + +%% @doc Server listen opts must work +valid_server_listen_opts() -> + [ + {alpn, ["proper"]}, + {cacertfile, "./msquic/submodules/openssl/test/certs/rootCA.pem"}, + {certfile, "./msquic/submodules/openssl/test/certs/servercert.pem"}, + {keyfile, "./msquic/submodules/openssl/test/certs/serverkey.pem"} + ]. + +valid_client_conn_opts() -> + [ + {alpn, ["proper"]}, + {cacertfile, "./msquic/submodules/openssl/test/certs/rootCA.pem"}, + {certfile, "./msquic/submodules/openssl/test/certs/servercert.pem"}, + {keyfile, "./msquic/submodules/openssl/test/certs/serverkey.pem"} + ]. + +valid_csend_stream_opts() -> + ?LET( + Opts, + quicer_stream_opts(), + maps:without( + [start_flag], + maps:from_list([{active, true} | Opts]) + ) + ). + +-spec ensure_dummy_listener(non_neg_integer()) -> _. +ensure_dummy_listener(Port) -> + case is_pid(whereis(?dummy_listener)) of + false -> + spawn_dummy_listener(Port); + true -> + ok + end. + +spawn_dummy_listener(Port) -> + Parent = self(), + spawn(fun() -> + register(?dummy_listener, self()), + {ok, L} = quicer_nif:listen(Port, maps:from_list(valid_server_listen_opts())), + spawn_acceptors(L, 4), + Parent ! ready, + receive + finish -> ok + end + end), + receive + ready -> + ok + end. + +spawn_acceptors(_, 0) -> + ok; +spawn_acceptors(L, N) -> + spawn_link(fun() -> + acceptor_loop(L) + end), + spawn_acceptors(L, N - 1). + +acceptor_loop(L) -> + case quicer:accept(L, #{active => true}) of + {ok, Conn} -> + spawn(fun() -> + _ = quicer:handshake(Conn), + timer:sleep(100), + quicer:async_shutdown_connection(Conn, 0, 0) + end), + acceptor_loop(L); + _ -> + acceptor_loop(L) + end.