hashmap_eqc.erl

-module(hashmap_eqc).

%% include some quickcheck headers
-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_statem.hrl").

%% include the eqc-c generated header
-include("hashmap.hrl").

%% function to initialize the model state
-export([initial_state/0]).

%% command functions

-export([hashmap_create_pre/1,
         hashmap_create_args/1,
         hashmap_create/1,
         hashmap_create_next/3]).

-export([hashmap_put_pre/1,
         hashmap_put_args/1,
         hashmap_put/3,
         hashmap_put_next/3]).

-export([hashmap_get_pre/1,
         hashmap_get_args/1,
         hashmap_get/2,
         hashmap_get_post/3]).

-export([hashmap_clear_pre/1,
         hashmap_clear_args/1,
         hashmap_clear/1,
         hashmap_clear_next/3]).

-export([hashmap_delete_pre/1,
         hashmap_delete_args/1,
         hashmap_delete/2,
         hashmap_delete_post/3,
         hashmap_delete_next/3]).

-export([hashmap_compare_pre/1,
         hashmap_compare_args/1,
         hashmap_compare/1,
         hashmap_compare_post/3]).

-export([hashmap_replace_pre/1,
         hashmap_replace_args/1,
         hashmap_replace/3,
         hashmap_replace_next/3]).

-export([hashmap_iter_delete_pre/1,
         hashmap_iter_delete_args/1,
         hashmap_iter_delete/2,
         hashmap_iter_delete_post/3,
         hashmap_iter_delete_next/3]).

%% the property
-export([prop_correct/0]).


-record(state, {hashmap=undefined,
                size,
                map=[]}).

prop_correct() ->
    %% call setup() if we don't have the 'hashmap' module loaded
    case code:which(hashmap) of
        non_existing ->
            setup();
        _ ->
            ok
    end,
    ?FORALL(Cmds,
            noshrink(commands(?MODULE)),
            begin
                Env = [],
                %% run the commands
                {H, S, Res} = run_commands(?MODULE, Cmds, Env),
                case S#state.hashmap of
                    undefined ->
                        %% we didn't actually generate anything, so nothing to cleanup
                        ok;
                    HM ->
                        %% cleanup the hashmap
                        hashmap:hashmap_free(HM),
                        eqc_c:free(HM)
                end,
                %% print out how many times we ran each command as a percentage
                pretty_commands(?MODULE, Cmds, {H, S, Res},
                                aggregate(command_names(Cmds),
                                          eqc:equals(Res, ok)))
            end).

setup() ->
    %% compile and load the C code as an erlang module
    eqc_c:start(hashmap, [{c_src, "hashmap.c"}, {cppflags, "-I ../../include/ -std=c99"},{cflags,"-lm -fsanitize=undefined -fno-sanitize-recover -fstack-protector-strong -fprofile-arcs -ftest-coverage"}, {additional_files, ["iterator.c"]}, {exec_command_line, fun(Exe) -> {os:find_executable("valgrind"), ["--leak-check=full", Exe]} end}]).

-spec initial_state() -> eqc_statem:symbolic_state().
initial_state() ->
    #state{}.

%% commands

hashmap_create_pre(S) ->
    S#state.hashmap == undefined.

hashmap_create_args(_S) ->
    [eqc_gen:choose(4,10)].

hashmap_create(Size) ->
    HM = eqc_c:alloc({struct, hashmap_t}),
        HM.

hashmap_create_next(S, R, [_Size]) ->
    S#state{hashmap=R}.

hashmap_put_pre(S) ->
    S#state.hashmap /= undefined.

hashmap_put_args(S) ->
    {Keys, _} = lists:unzip(S#state.map),
    [S#state.hashmap, ?SUCHTHAT(X1, eqc_gen:list(eqc_gen:char()), length(X1) > 0 andalso not lists:member(X1, Keys)), ?SUCHTHAT(X2, eqc_gen:list(eqc_gen:char()), length(X2) > 0)].

hashmap_put(Hashmap, Key, Value) ->
    KeyStr = eqc_c:create_string(Key),
    ValueStr = eqc_c:create_string(Value),
    R = hashmap:hashmap_put(Hashmap, KeyStr, length(Key), ValueStr, length(Value)),
    eqc_c:free(KeyStr),
    eqc_c:free(ValueStr),
    R.

hashmap_put_next(S, _R, [_, Key, Value]) ->
    S#state{map=[{Key, Value} | S#state.map]}.

hashmap_get_pre(S) ->
    S#state.hashmap /= undefined.

hashmap_get_args(S = #state{map=Map}) when length(Map) > 0  ->
    [S#state.hashmap, eqc_gen:oneof([eqc_gen:elements(element(1, lists:unzip(S#state.map))), ?SUCHTHAT(X1, eqc_gen:list(eqc_gen:char()), length(X1) > 0)])];
hashmap_get_args(S) ->
    [S#state.hashmap, ?SUCHTHAT(X1, eqc_gen:list(eqc_gen:char()), length(X1) > 0)].

hashmap_get(Hashmap, Key) ->
    Val = eqc_c:alloc({ptr, unsigned_char}),
    ValLen = eqc_c:alloc(unsigned_int),
    KeyStr = eqc_c:create_string(Key),
    R = hashmap:hashmap_get(Hashmap, KeyStr, length(Key), Val, ValLen),
    Len = eqc_c:deref(ValLen),
    RealVal = case Len of
        0 ->
          undefined;
        _ ->
          eqc_c:read_array(eqc_c:deref(Val), Len)
    end,
    eqc_c:free(Val),
    eqc_c:free(ValLen),
    eqc_c:free(KeyStr),
    {R, Len, RealVal}.

hashmap_get_post(S, [_, Key], {R, Len, Val}) ->
    case lists:keyfind(Key, 1, S#state.map) of
        {Key, Value} ->
            R == 0 andalso {Key, Val} == {Key, Value};
        false ->
            R == 1 andalso Len == 0
    end.

hashmap_clear_pre(S) ->
    S#state.hashmap /= undefined.

hashmap_clear_args(S) ->
    [S#state.hashmap].

hashmap_clear(Hashmap) ->
    hashmap:hashmap_clear(Hashmap).

hashmap_clear_next(S, _R, [_]) ->
    S#state{map=[]}.

hashmap_delete_pre(S) ->
    S#state.hashmap /= undefined.

hashmap_delete_args(S = #state{map=Map}) when length(Map) > 0  ->
    [S#state.hashmap, eqc_gen:oneof([eqc_gen:elements(element(1, lists:unzip(S#state.map))), ?SUCHTHAT(X1, eqc_gen:list(eqc_gen:char()), length(X1) > 0)])];
hashmap_delete_args(S) ->
    [S#state.hashmap, ?SUCHTHAT(X1, eqc_gen:list(eqc_gen:char()), length(X1) > 0)].

hashmap_delete(Hashmap, Key) ->
    KeyStr = eqc_c:create_string(Key),
    R = hashmap:hashmap_del(Hashmap, KeyStr, length(Key)),
    eqc_c:free(KeyStr),
    R.

hashmap_delete_post(S, [_, Key], R) ->
    %% check the return code against whether the key was in the map
    case lists:keyfind(Key, 1, S#state.map) of
        {Key, _} ->
            R == 0;
        false ->
            R == 1
    end.

hashmap_delete_next(S, _R, [_, Key]) ->
    S#state{map=lists:keydelete(Key, 1, S#state.map)}.

hashmap_compare_pre(S) ->
    S#state.hashmap /= undefined.

hashmap_compare_args(S) ->
    [S#state.hashmap].

hashmap_compare(Hashmap) ->
    Iter = eqc_c:alloc({struct, iterator_t}),
    hashmap:hashmap_iter_begin(Hashmap, Iter),
    R = dump_hash(Iter, []),
    eqc_c:free(Iter),
    R.

hashmap_compare_post(S, [_], R) ->
    case lists:sort(S#state.map) == lists:sort(R) of
        true ->
            true;
        false ->
            {hash_mismatch, lists:sort(S#state.map), lists:sort(R)}
    end.

hashmap_replace_pre(S) ->
    S#state.hashmap /= undefined andalso length(S#state.map) > 0.

hashmap_replace_args(S) ->
    {Keys, Values} = lists:unzip(S#state.map),
    [S#state.hashmap, eqc_gen:oneof(Keys), ?SUCHTHAT(X2, eqc_gen:list(eqc_gen:char()), length(X2) > 0 andalso not lists:member(X2, Values))].

hashmap_replace(Hashmap, Key, Value) ->
    KeyStr = eqc_c:create_string(Key),
    ValueStr = eqc_c:create_string(Value),
    R = hashmap:hashmap_put(Hashmap, KeyStr, length(Key), ValueStr, length(Value)),
    eqc_c:free(KeyStr),
    eqc_c:free(ValueStr),
    R.

hashmap_replace_next(S, _R, [_, Key, Value]) ->
    S#state{map=lists:keyreplace(Key, 1, S#state.map, {Key, Value})}.

hashmap_iter_delete_pre(S) ->
    S#state.hashmap /= undefined.

hashmap_iter_delete_args(S = #state{map=Map}) when length(Map) > 0  ->
    [S#state.hashmap, eqc_gen:oneof([eqc_gen:elements(element(1, lists:unzip(S#state.map))), ?SUCHTHAT(X1, eqc_gen:list(eqc_gen:char()), length(X1) > 0)])];
hashmap_iter_delete_args(S) ->
    [S#state.hashmap, ?SUCHTHAT(X1, eqc_gen:list(eqc_gen:char()), length(X1) > 0)].

hashmap_iter_delete(Hashmap, Key) ->
    Iter = eqc_c:alloc({struct, iterator_t}),
    hashmap:hashmap_iter_begin(Hashmap, Iter),
    R = iter_delete(Hashmap, Iter, Key),
    eqc_c:free(Iter),
    R.

hashmap_iter_delete_post(S, [_, Key], R) ->
    %% check the return code against whether the key was in the map
    case lists:keyfind(Key, 1, S#state.map) of
        {Key, _} ->
            R == 0;
        false ->
            R == 1
    end.

hashmap_iter_delete_next(S, _R, [_, Key]) ->
    S#state{map=lists:keydelete(Key, 1, S#state.map)}.

%% helpers

dump_hash(Iter, Acc) ->
    case hashmap:iter_next(Iter) of
        'NULL' ->
            Acc;
        Ptr ->
            Pair = eqc_c:deref(eqc_c:cast_ptr({struct, hashmap_pair_t}, Ptr)),
            Key = eqc_c:read_array(eqc_c:cast_ptr(unsigned_char, Pair#hashmap_pair_t.key), Pair#hashmap_pair_t.keylen),
            Val = eqc_c:read_array(eqc_c:cast_ptr(unsigned_char, Pair#hashmap_pair_t.val), Pair#hashmap_pair_t.vallen),
            dump_hash(Iter, [{Key, Val}|Acc])
    end.

iter_delete(Hashmap, Iter, Key) ->
    case hashmap:iter_next(Iter) of
        'NULL' ->
            hashmap:hashmap_delete(Hashmap, Iter);
        Ptr ->
            Pair = eqc_c:deref(eqc_c:cast_ptr({struct, hashmap_pair_t}, Ptr)),
            IterKey = eqc_c:read_array(eqc_c:cast_ptr(unsigned_char, Pair#hashmap_pair_t.key), Pair#hashmap_pair_t.keylen),
            case Key == IterKey of
                true ->
                    hashmap:hashmap_delete(Hashmap, Iter);
                false ->
                    iter_delete(Hashmap, Iter, Key)
            end
    end.