diff --git a/test/prop_quic_types.hrl b/test/prop_quic_types.hrl index 15323167..bd872958 100644 --- a/test/prop_quic_types.hrl +++ b/test/prop_quic_types.hrl @@ -61,14 +61,15 @@ | {conn_acceptors, non_neg_integer()} | {settings, [quicer_setting()]}. +-define(UINT32_MAX, 4294967295). -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()} + | {stream_recv_window_default, 1..?UINT32_MAX} + | {stream_recv_buffer_default, 4096..?UINT32_MAX} | {conn_flow_control_window, uint32()} | {max_stateless_operations, uint32()} | {initial_window_packets, uint32()} @@ -95,6 +96,40 @@ | {max_binding_stateless_operations, uint16()} | {stateless_operation_expiration_ms, uint16()}. +-type quicer_setting_with_range() :: + {max_bytes_per_key, 0..(4 bsl 34 - 1)} + | {handshake_idle_timeout_ms, 0..(1 bsl 62 - 1)} + | {idle_timeout_ms, 0..(1 bsl 62 - 1)} + | {tls_client_max_send_buffer, uint32()} + | {tls_server_max_send_buffer, uint32()} + | {stream_recv_window_default, 1..?UINT32_MAX} + | {stream_recv_buffer_default, 4096..?UINT32_MAX} + | {conn_flow_control_window, uint32()} + | {max_stateless_operations, uint32()} + | {initial_window_packets, uint32()} + | {send_idle_timeout_ms, uint32()} + | {initial_rtt_ms, 1..?UINT32_MAX} + | {max_ack_delay_ms, 1..(1 bsl 14 - 1)} + | {disconnect_timeout_ms, 1..600000} + | {keep_alive_interval_ms, uint32()} + | {congestion_control_algorithm, 0 | 1} + | {peer_bidi_stream_count, uint16()} + | {peer_unidi_stream_count, uint16()} + | {retry_memory_limit, uint16()} + | {load_balancing_mode, 0..2} + | {max_operations_per_drain, uint8()} + | {send_buffering_enabled, 0 | 1} + | {pacing_enabled, 0 | 1} + | {migration_enabled, 0 | 1} + | {datagram_receive_enabled, 0 | 1} + | {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()]} diff --git a/test/prop_stateful_server_conn.erl b/test/prop_stateful_server_conn.erl index a5952ecc..b5056c24 100644 --- a/test/prop_stateful_server_conn.erl +++ b/test/prop_stateful_server_conn.erl @@ -95,6 +95,7 @@ initial_state() -> command(#{handle := Handle}) -> frequency([ {200, {call, quicer, handshake, [Handle, 1000]}}, + {100, {call, quicer, handshake, [Handle, valid_quicer_settings(), 1000]}}, {100, {call, quicer, getopt, [Handle, ?LET({Opt, _}, conn_opt(), Opt)]}}, {100, {call, quicer, async_accept_stream, [Handle, ?LET(Opts, quicer_acceptor_opts(), Opts)]}}, @@ -291,6 +292,9 @@ postcondition(#{handle := _H, state := _S}, {call, quicer, get_connections, _}, true; postcondition(#{state := closed}, {call, _Mod, _Fun, _Args}, {error, closed}) -> true; +%% postcondition(#{state := accepted}, {call, quicer, handshake, _Args}, {error, invalid_parameter}) -> +%% %% handshake with wrong args +%% true; postcondition(#{state := accepted}, {call, _Mod, _Fun, _Args}, {error, closed}) -> %% handshake didnt take place on time true; @@ -327,6 +331,9 @@ step_calls(#{calls := Calls} = S) -> S#{calls := Calls + 1}. %%% Generators +valid_quicer_settings() -> + quicer_prop_gen:valid_quicer_settings(). + %%%%%%%%%%%%%%%%%%%%%%% %%% Listener helper %%% %%%%%%%%%%%%%%%%%%%%%%% diff --git a/test/quicer_prop_gen.erl b/test/quicer_prop_gen.erl index c7e47930..a1750d7e 100644 --- a/test/quicer_prop_gen.erl +++ b/test/quicer_prop_gen.erl @@ -32,6 +32,7 @@ valid_reg_handle/0, valid_handle/0, valid_csend_stream_opts/0, + valid_quicer_settings/0, pid/0, data/0, quicer_send_flags/0, @@ -290,6 +291,20 @@ valid_csend_stream_opts() -> ) ). +%% @see msquic/src/core/settings.c +valid_quicer_settings() -> + ?SUCHTHAT( + Opts, + ?LET(Q, list(quicer_setting_with_range()), Q), + %% Conds below from msquic/src/core/settings.c + quicer_setting_val_is_power_2(stream_recv_window_default, Opts) andalso + quicer_setting_val_is_power_2(stream_recv_window_bidi_local_default, Opts) andalso + quicer_setting_val_is_power_2(stream_recv_window_bidi_remote_default, Opts) andalso + quicer_setting_val_is_power_2(stream_recv_window_unidi_default, Opts) andalso + (proplists:get_value(maximum_mtu, Opts, 1500) > + proplists:get_value(minimum_mtu, Opts, 1248)) + ). + -spec ensure_dummy_listener(non_neg_integer()) -> _. ensure_dummy_listener(Port) -> case is_pid(whereis(?dummy_listener)) of @@ -335,3 +350,11 @@ acceptor_loop(L) -> _ -> acceptor_loop(L) end. + +-spec quicer_setting_val_is_power_2(atom(), proplists:proplist()) -> boolean(). +quicer_setting_val_is_power_2(Key, Opts) -> + is_pow_2(maps:get(Key, maps:from_list(Opts), 2)). +is_pow_2(N) when is_integer(N), N > 0 -> + (N band (N - 1)) == 0; +is_pow_2(_) -> + false.