machinery for running QuickCheck #505
3
.eqc_ci
Normal file
3
.eqc_ci
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
{build, "rebar3 as eqc compile"}.
|
||||||
|
{test_root, "."}.
|
||||||
|
{test_path, "_build/eqc/lib/aesophia/quickcheck"}. %% here are the properties
|
3
.gitignore
vendored
3
.gitignore
vendored
@ -16,5 +16,8 @@ _build
|
|||||||
.idea
|
.idea
|
||||||
*.iml
|
*.iml
|
||||||
rebar3.crashdump
|
rebar3.crashdump
|
||||||
|
current_counterexample.eqc
|
||||||
|
.qcci
|
||||||
*.erl~
|
*.erl~
|
||||||
*.aes~
|
*.aes~
|
||||||
|
|
||||||
|
109
quickcheck/aeso_heap_eqc.erl
Normal file
109
quickcheck/aeso_heap_eqc.erl
Normal file
@ -0,0 +1,109 @@
|
|||||||
|
%%% File : aeso_heap_eqc.erl
|
||||||
|
%%% Author : Ulf Norell
|
||||||
|
%%% Description :
|
||||||
|
%%% Created : 28 May 2018 by Ulf Norell
|
||||||
|
-module(aeso_heap_eqc).
|
||||||
|
|
||||||
|
-compile([export_all, nowarn_export_all]).
|
||||||
|
-include_lib("eqc/include/eqc.hrl").
|
||||||
|
|
||||||
|
-define(SANDBOX(Code), sandbox(fun() -> Code end)).
|
||||||
|
|
||||||
|
sandbox(Code) ->
|
||||||
|
Parent = self(),
|
||||||
|
Tag = make_ref(),
|
||||||
|
{Pid, Ref} = spawn_monitor(fun() -> Parent ! {Tag, Code()} end),
|
||||||
|
receive
|
||||||
|
{Tag, Res} -> erlang:demonitor(Ref, [flush]), {ok, Res};
|
||||||
|
{'DOWN', Ref, process, Pid, Reason} -> {error, Reason}
|
||||||
|
after 100 ->
|
||||||
|
exit(Pid, kill),
|
||||||
|
{error, loop}
|
||||||
|
end.
|
||||||
|
|
||||||
|
prop_from_binary() ->
|
||||||
|
?FORALL({T, Bin}, {type(), blob()},
|
||||||
|
begin
|
||||||
|
Tag = fun(X) when is_atom(X) -> X; (X) when is_tuple(X) -> element(1, X) end,
|
||||||
|
case ?SANDBOX(aeso_heap:from_binary(T, Bin)) of
|
||||||
|
{ok, Res} -> collect({Tag(T), element(1, Res)}, true);
|
||||||
|
Err -> equals(Err, {ok, '_'})
|
||||||
|
end end).
|
||||||
|
|
||||||
|
type() -> ?LET(Depth, choose(0, 2), type(Depth, true)).
|
||||||
|
type(Depth, TypeRep) ->
|
||||||
|
oneof(
|
||||||
|
[ elements([word, string] ++ [typerep || TypeRep]) ] ++
|
||||||
|
[ ?LETSHRINK([T], [type(Depth - 1, TypeRep)], {list, T}) || Depth > 0 ] ++
|
||||||
|
[ ?LETSHRINK([T], [type(Depth - 1, TypeRep)], {option, T}) || Depth > 0 ] ++
|
||||||
|
[ ?LETSHRINK(Ts, list(type(Depth - 1, TypeRep)), {tuple, Ts}) || Depth > 0 ] ++
|
||||||
|
[ ?LETSHRINK([K, V], vector(2, type(Depth - 1, TypeRep)), {map, K, V}) || Depth > 0 ] ++
|
||||||
|
[]
|
||||||
|
).
|
||||||
|
|
||||||
|
blob() ->
|
||||||
|
?LET(Blobs, list(oneof([ ?LET(Ws, words(), return(from_words(Ws)))
|
||||||
|
, binary() ])),
|
||||||
|
return(list_to_binary(Blobs))).
|
||||||
|
|
||||||
|
words() -> list(word()).
|
||||||
|
word() ->
|
||||||
|
frequency(
|
||||||
|
[ {4, ?LET(N, nat(), 32 * N)}
|
||||||
|
, {1, choose(0, 320)}
|
||||||
|
, {2, -1}
|
||||||
|
, {2, elements(["foo", "zzzzz"])} ]).
|
||||||
|
|
||||||
|
from_words(Ws) ->
|
||||||
|
<< <<(from_word(W))/binary>> || W <- Ws >>.
|
||||||
|
|
||||||
|
from_word(W) when is_integer(W) ->
|
||||||
|
<<W:256>>;
|
||||||
|
from_word(S) when is_list(S) ->
|
||||||
|
Len = length(S),
|
||||||
|
Bin = <<(list_to_binary(S))/binary, 0:(32 - Len)/unit:8>>,
|
||||||
|
<<Len:256, Bin/binary>>.
|
||||||
|
|
||||||
|
typerep() -> ?LET(Depth, choose(0, 2),
|
||||||
|
?LET(T, type(Depth, true), return(typerep(T)))).
|
||||||
|
|
||||||
|
typerep(word) -> word;
|
||||||
|
typerep(string) -> string;
|
||||||
|
typerep(typerep) -> typerep;
|
||||||
|
typerep({tuple, Ts}) -> {tuple, typerep(Ts)};
|
||||||
|
typerep({list, T}) -> {list, typerep(T)};
|
||||||
|
typerep({variant, Cs}) -> {variant, typerep(Cs)};
|
||||||
|
typerep({option, T}) -> {variant, [[], [typerep(T)]]};
|
||||||
|
typerep({map, K, V}) -> {list, typerep({tuple, [K, V]})};
|
||||||
|
typerep([]) -> [];
|
||||||
|
typerep([T | Ts]) -> [typerep(T) | typerep(Ts)].
|
||||||
|
|
||||||
|
value(word) ->
|
||||||
|
<<N:256>> = <<(-1):256>>,
|
||||||
|
choose(0, N);
|
||||||
|
value(string) ->
|
||||||
|
?LET(N, choose(0, 128), binary(N));
|
||||||
|
value(typerep) ->
|
||||||
|
typerep();
|
||||||
|
value({list, T}) ->
|
||||||
|
list(value(T));
|
||||||
|
value({option, T}) ->
|
||||||
|
weighted_default({1, none}, {3, {some, value(T)}});
|
||||||
|
value({tuple, Ts}) ->
|
||||||
|
?LET(Vs, [ value(T) || T <- Ts ], list_to_tuple(Vs));
|
||||||
|
value({map, K, V}) ->
|
||||||
|
map(value(K), value(V));
|
||||||
|
value({variant, Cs}) ->
|
||||||
|
?LET(I, choose(0, length(Cs) - 1),
|
||||||
|
{variant, I, [ value(T) || T <- lists:nth(I + 1, Cs) ]}).
|
||||||
|
|
||||||
|
typed_val() ->
|
||||||
|
?LET(T, type(), ?LET(V, value(T), return({T, V}))).
|
||||||
|
|
||||||
|
prop_roundtrip() ->
|
||||||
|
?FORALL(T, type(),
|
||||||
|
?FORALL(V, value(T),
|
||||||
|
?FORALL(B, choose(0, 4),
|
||||||
|
equals(aeso_heap:from_binary(T, aeso_heap:to_binary(V, B * 32), B * 32),
|
||||||
|
{ok, V})))).
|
||||||
|
|
59
quickcheck/aeso_utils_eqc.erl
Normal file
59
quickcheck/aeso_utils_eqc.erl
Normal file
@ -0,0 +1,59 @@
|
|||||||
|
%%% File : aeso_utils_eqc.erl
|
||||||
|
%%% Author : Ulf Norell
|
||||||
|
%%% Description :
|
||||||
|
%%% Created : 2 Jul 2018 by Ulf Norell
|
||||||
|
-module(aeso_utils_eqc).
|
||||||
|
|
||||||
|
-compile([export_all, nowarn_export_all]).
|
||||||
|
|
||||||
|
-include_lib("eqc/include/eqc.hrl").
|
||||||
|
|
||||||
|
%% QuickCheck property
|
||||||
|
|
||||||
|
graph() ->
|
||||||
|
?LET(M, map(choose(0, 10), list(choose(0, 10))),
|
||||||
|
return(complete(M))).
|
||||||
|
|
||||||
|
complete(G) ->
|
||||||
|
Is = lists:usort(lists:concat(maps:values(G))),
|
||||||
|
maps:merge(maps:from_list([ {I, []} || I <- Is ]), G).
|
||||||
|
|
||||||
|
prop_scc() ->
|
||||||
|
?FORALL(G, graph(),
|
||||||
|
begin
|
||||||
|
SCCs = aeso_utils:scc(G),
|
||||||
|
BadSCC = fun({acyclic, I}) -> reachable_from(G, I, I);
|
||||||
|
({cyclic, Is}) -> [] /= [ {I, J} || I <- Is, J <- Is, not reachable_from(G, I, J) ]
|
||||||
|
end,
|
||||||
|
ToList = fun({acyclic, I}) -> [I];
|
||||||
|
({cyclic, Is}) -> Is end,
|
||||||
|
?WHENFAIL(eqc:format("SCCs = ~p\n", [SCCs]),
|
||||||
|
conjunction(
|
||||||
|
[ {elems, equals(lists:sort(lists:flatmap(ToList, SCCs)), lists:sort(maps:keys(G)))}
|
||||||
|
, {sorted, equals([], [ {I, J} || {I, Js} <- maps:to_list(G),
|
||||||
|
J <- Js,
|
||||||
|
find_component(I, SCCs) < find_component(J, SCCs) ])}
|
||||||
|
, {precise, equals([], [ SCC || SCC <- SCCs, BadSCC(SCC) ])}
|
||||||
|
]))
|
||||||
|
end).
|
||||||
|
|
||||||
|
reachable_from(Graph, I, J) ->
|
||||||
|
reachable_from1(Graph, maps:get(I, Graph, []), J).
|
||||||
|
|
||||||
|
reachable_from1(_, [], _) -> false;
|
||||||
|
reachable_from1(_, [I | _], I) -> true;
|
||||||
|
reachable_from1(Graph, [I | Is], J) ->
|
||||||
|
case maps:get(I, Graph, undefined) of
|
||||||
|
undefined -> reachable_from1(Graph, Is, J);
|
||||||
|
Js -> reachable_from1(maps:remove(I, Graph), Js ++ Is, J)
|
||||||
|
end.
|
||||||
|
|
||||||
|
find_component(X, SCCs) ->
|
||||||
|
ISCCs = lists:zip(SCCs, lists:seq(1, length(SCCs))),
|
||||||
|
HasX = fun({acyclic, Y}) -> X == Y;
|
||||||
|
({cyclic, Ys}) -> lists:member(X, Ys) end,
|
||||||
|
case [ I || {SCC, I} <- ISCCs, HasX(SCC) ] of
|
||||||
|
[I | _] -> I;
|
||||||
|
[] -> false
|
||||||
|
end.
|
||||||
|
|
@ -5,6 +5,13 @@
|
|||||||
, {getopt, "1.0.1"}
|
, {getopt, "1.0.1"}
|
||||||
]}.
|
]}.
|
||||||
|
|
||||||
|
|
||||||
|
{profiles, [ {eqc, [{erl_opts, [{parse_transform, eqc_cover}]},
|
||||||
|
{deps, [{eqc_ci, "1.0.0"}]},
|
||||||
|
{extra_src_dirs, ["quickcheck"]} %% May not be called eqc!
|
||||||
|
]}
|
||||||
|
]}.
|
||||||
|
|
||||||
{escript_incl_apps, [aesophia, aebytecode, getopt]}.
|
{escript_incl_apps, [aesophia, aebytecode, getopt]}.
|
||||||
{escript_main_app, aesophia}.
|
{escript_main_app, aesophia}.
|
||||||
{escript_name, aesophia}.
|
{escript_name, aesophia}.
|
||||||
|
Loading…
x
Reference in New Issue
Block a user