diff --git a/.eqc_ci b/.eqc_ci new file mode 100644 index 0000000..a3b6f8a --- /dev/null +++ b/.eqc_ci @@ -0,0 +1,3 @@ +{build, "rebar3 as eqc compile"}. +{test_root, "."}. +{test_path, "_build/eqc/lib/aesophia/quickcheck"}. %% here are the properties diff --git a/.gitignore b/.gitignore index 40ca652..ed03531 100644 --- a/.gitignore +++ b/.gitignore @@ -16,3 +16,5 @@ _build .idea *.iml rebar3.crashdump +current_counterexample.eqc +.qcci diff --git a/quickcheck/aeso_heap_eqc.erl b/quickcheck/aeso_heap_eqc.erl new file mode 100644 index 0000000..2585faf --- /dev/null +++ b/quickcheck/aeso_heap_eqc.erl @@ -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) -> + <>; +from_word(S) when is_list(S) -> + Len = length(S), + Bin = <<(list_to_binary(S))/binary, 0:(32 - Len)/unit:8>>, + <>. + +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) -> + <> = <<(-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})))). + diff --git a/quickcheck/aeso_utils_eqc.erl b/quickcheck/aeso_utils_eqc.erl new file mode 100644 index 0000000..3bbce88 --- /dev/null +++ b/quickcheck/aeso_utils_eqc.erl @@ -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. + diff --git a/rebar.config b/rebar.config index ee1cc9c..dd271ad 100644 --- a/rebar.config +++ b/rebar.config @@ -5,6 +5,11 @@ {ref,"720510a"}}} ]}. +{profiles, [ {eqc, [{erl_opts, [{parse_transform, eqc_cover}]}, + {deps, [{eqc_ci, "1.0.0"}]}, + {extra_src_dirs, ["quickcheck"]} %% May not be called eqc! + ]} + ]}. {dialyzer, [ {warnings, [unknown]},