Difference between revisions of "CirqBuff and MBox QuickCheck Models"

From CERES
Jump to: navigation, search
Line 5: Line 5:
  
 
<pre>
 
<pre>
 +
-define(AUTOSAR_SRC, ".").
 
</pre>
 
</pre>
  
Line 10: Line 11:
  
 
<pre>
 
<pre>
 +
-record(cb_state, {ptr, size, elements, data_size}).
 
</pre>
 
</pre>
  
Line 15: Line 17:
  
 
<pre>
 
<pre>
 +
-module(qc_cb_setup).
 +
-export([ setup/0 ]).
 +
 +
-include_lib("eqc/include/eqc_c.hrl").
 +
-include_lib("source_path.hrl").
 +
 +
setup() -> eqc_c:start(cb,
 +
  [ {cppflags, "-std=c99 -I " ++ ?AUTOSAR_SRC ++ "/include"},
 +
    {c_src, ?AUTOSAR_SRC ++ "/src/cirq_buffer.c"} ]).
 
</pre>
 
</pre>
  
Line 20: Line 31:
  
 
<pre>
 
<pre>
 +
-module(qc_cb).
 +
 +
-compile(export_all).
 +
-include_lib("eqc/include/eqc.hrl").
 +
-include_lib("eqc/include/eqc_component.hrl").
 +
-include_lib("cb.hrl"). % Auto-generated
 +
-include_lib("qc_cb.hrl").
 +
 +
initial_state() -> #cb_state{ elements=[] }.
 +
 +
invariant(S) -> length(S#cb_state.elements) =< S#cb_state.size.
 +
 +
postcondition_common(_S, {call, _, create, _, _ }, _Res) -> true;
 +
postcondition_common(S, Call, Res) -> eq(Res, return_value(S, Call)).
 +
 +
create(Size, DataSize) -> cb:'CirqBuffDynCreate'(Size, DataSize).
 +
create_args(_S) -> [nat(), nat()].
 +
create_pre(S, [Size, _DataSize]) -> S#cb_state.ptr == undefined andalso Size > 0.
 +
create_next(S, R, [Size, DataSize]) ->
 +
  S#cb_state{ptr=R, size=Size, data_size = DataSize }.
 +
create_callers() -> [qc_mbox].
 +
create_return(_S, [Size, DataSize]) ->
 +
  #'CirqBufferType' { maxCnt = Size, currCnt = 0, dataSize = DataSize,
 +
    head = 'NULL', tail = 'NULL', bufStart = 'NULL', bufEnd = 'NULL' }.
 +
 +
push(Ptr, Val) ->  DataPtr = eqc_c:create_array(unsigned_char, Val),
 +
  CallRes = cb:'CirqBuffPush'(Ptr, DataPtr), eqc_c:free(DataPtr), CallRes.
 +
push_args(S) -> [S#cb_state.ptr, vector(S#cb_state.data_size, char())].
 +
push_pre(S) ->
 +
  S#cb_state.ptr /= undefined andalso length(S#cb_state.elements) < S#cb_state.size.
 +
push_next(S, _R, [_Ptr, Value]) ->
 +
  S#cb_state{elements = S#cb_state.elements ++ [Value]}.
 +
push_return(S, _Args) -> % 0.
 +
  if length(S#cb_state.elements) < 128 -> 0; true -> 1 end.
 +
push_callers() -> [qc_mbox].
 +
 +
pop(Ptr, DataSize) ->
 +
  DataPtr = eqc_c:create_array(unsigned_char, [0 || _E <- lists:seq(1, DataSize)]),
 +
  CallRes = cb:'CirqBuffPop'(Ptr, DataPtr),
 +
  DataRes = eqc_c:read_array(DataPtr, DataSize),
 +
  eqc_c:free(DataPtr), {DataRes, CallRes}.
 +
pop_args(S) -> [S#cb_state.ptr, S#cb_state.data_size].
 +
pop_pre(S) ->
 +
  S#cb_state.ptr /= undefined andalso length(S#cb_state.elements) > 0.
 +
pop_next(S, _R, _Args) -> S#cb_state{elements = tl(S#cb_state.elements)}.
 +
pop_return(S, _Args) -> {hd(S#cb_state.elements), 0}.
 +
pop_callers() -> [qc_mbox].
 +
 +
prop_cb_length() -> ?SETUP(fun() -> qc_cb_setup:setup(), fun() -> ok end end,
 +
  ?FORALL(Cmds, commands(?MODULE),
 +
  begin {H, S, Res} = run_commands(Cmds),
 +
    aggregate(command_names(Cmds),
 +
      measure(num_commands,
 +
        commands_length(Cmds),
 +
        pretty_commands(?MODULE, Cmds, {H, S, Res}, Res == ok))) end)).
 +
 +
prop_cb() -> ?SETUP(fun() -> qc_cb_setup:setup(), fun() -> ok end end,
 +
  ?FORALL(Cmds, commands(?MODULE),
 +
  begin {_, _, Res} = run_commands(Cmds), Res == ok end)).
 
</pre>
 
</pre>
  
Line 25: Line 95:
  
 
<pre>
 
<pre>
 +
-record(mbox_state, {ptr, size, elements, cb_state}).
 
</pre>
 
</pre>
  
Line 30: Line 101:
  
 
<pre>
 
<pre>
 +
-include_lib("source_path.hrl").
 +
 +
api_spec() -> #api_spec {
 +
  language = c, mocking = eqc_mocking_c,
 +
  modules  = [ #api_module{ name = mbox, functions = [
 +
    #api_fun_c{ name = 'CirqBuffDynCreate', ret = 'CirqBufferType *',
 +
                args = [ #api_arg_c{type = size_t, name = size, dir = in},
 +
                        #api_arg_c{type = size_t, name = dataSize, dir = in} ],
 +
                classify = {qc_cb, create} },
 +
    #api_fun_c{ name = 'CirqBuffPush', ret = int,
 +
                args = [ #api_arg_c{type = 'CirqBufferType *', name = cPtr, dir = in},
 +
                        #api_arg_c{ type = 'void *', name = dataPtr, dir = in,
 +
                          stored_type = 'unsigned char *',
 +
                          buffer = {true, "cPtr->dataSize"}} ],
 +
                classify = {qc_cb, push} },
 +
    #api_fun_c{ name = 'CirqBuffPop',  ret = int,
 +
                args = [ #api_arg_c{type = 'CirqBufferType *', name = cPtr, dir = in},
 +
                        #api_arg_c{ type = 'void *', name = dataPtr, dir = out,
 +
                          stored_type = 'unsigned char *',
 +
                          buffer = {true, "cPtr->dataSize"}} ],
 +
                classify = {qc_cb, pop} }]}]}.
 +
 +
start_mocking() -> eqc_mocking_c:start_mocking(mbox, ?MODULE:api_spec(),
 +
  [ "Std_Types.h", "cirq_buffer.h", "mbox.h" ],
 +
  [ ?AUTOSAR_SRC ++ "/src/mbox.c" ],
 +
  [ {cppflags, "-std=c99 -I . -I " ++ ?AUTOSAR_SRC ++ "/include"} ]).
 
</pre>
 
</pre>
  
Line 35: Line 132:
  
 
<pre>
 
<pre>
 +
-module(qc_mbox_setup).
 +
 +
-compile(export_all).
 +
 +
-include_lib("eqc/include/eqc_c.hrl").
 +
-include_lib("eqc/include/eqc_mocking.hrl").
 +
 +
-include("qc_mbox_capi.erl").
 
</pre>
 
</pre>
  
Line 40: Line 145:
  
 
<pre>
 
<pre>
 +
-module(qc_mbox).
 +
 +
-compile(export_all).
 +
-include_lib("eqc/include/eqc.hrl").
 +
-include_lib("eqc/include/eqc_component.hrl").
 +
-include_lib("qc_mbox.hrl").
 +
-include_lib("qc_cb.hrl").
 +
 +
-include("mbox.hrl"). % Auto-generated
 +
-include("qc_mbox_capi.erl").
 +
 +
-define(PTR_SIZE, 8). % Change resp. for test running platform (here 64 bit arch.)
 +
 +
initial_state() -> #mbox_state{ elements=[] }.
 +
 +
invariant(S) -> length(S#mbox_state.elements) =< S#mbox_state.size.
 +
 +
postcondition_common(_S, {call, _, create, _, _ }, _R) -> true;
 +
postcondition_common(S, Call, Res) -> eq(Res, return_value(S, Call)).
 +
 +
create(Size) -> mbox:'Arc_MBoxCreate'(Size).
 +
create_args(_S) -> [choose(1, 256)].
 +
create_pre(S, [Size]) -> S#mbox_state.ptr == undefined andalso Size > 0.
 +
create_next(S, R, [Size]) -> S#mbox_state{ptr=R, size=Size }.
 +
create_callouts(_S, [Size]) ->
 +
  ?CALLOUT(mbox, 'CirqBuffDynCreate', [Size, ?PTR_SIZE],
 +
  #'CirqBufferType' { maxCnt = Size, currCnt = 0,
 +
    dataSize = 8, head = 'NULL', tail = 'NULL',
 +
    bufStart = 'NULL', bufEnd = 'NULL'}).
 +
 +
post(Ptr, Val) ->
 +
  DataPtr = eqc_c:create_array(unsigned_char, Val),
 +
  CallRes = mbox:'Arc_MBoxPost'(Ptr, DataPtr),
 +
  eqc_c:free(DataPtr), CallRes.
 +
post_args(S) -> [S#mbox_state.ptr, vector(?PTR_SIZE, char())].
 +
post_pre(S) -> S#mbox_state.ptr /= undefined
 +
  andalso length(S#mbox_state.elements) < S#mbox_state.size.
 +
post_next(S, _R, [_Ptr, Value]) ->
 +
  S#mbox_state{elements = S#mbox_state.elements ++ [Value]}.
 +
post_return(_S, _Args) -> 0.
 +
post_callouts(S, [_Ptr, Value]) ->
 +
  ?CALLOUT(mbox, 'CirqBuffPush', [?WILDCARD, Value],
 +
  if length(S#mbox_state.elements) < 128 -> 0; true -> 1 end).
 +
 +
fetch(Ptr) ->
 +
  DataPtr = eqc_c:create_array(unsigned_char, [0 || _E <- lists:seq(1, ?PTR_SIZE)]),
 +
  CallRes = mbox:'Arc_MBoxFetch'(Ptr, DataPtr),
 +
  DataRes = eqc_c:read_array(DataPtr, ?PTR_SIZE),
 +
  eqc_c:free(DataPtr), {DataRes, CallRes}.
 +
fetch_args(S) -> [S#mbox_state.ptr].
 +
fetch_pre(S) ->
 +
  S#mbox_state.ptr /= undefined andalso length(S#mbox_state.elements) > 0.
 +
fetch_next(S, _R, [_Ptr]) -> S#mbox_state{elements = tl(S#mbox_state.elements)}.
 +
fetch_return(S, [_Ptr]) -> {hd(S#mbox_state.elements), 0}.
 +
fetch_callouts(S, [_Ptr]) ->
 +
  ?CALLOUT(mbox, 'CirqBuffPop', [?WILDCARD], { hd(S#mbox_state.elements), 0}).
 +
 +
weight(#mbox_state{ptr = undefined}, Op) -> case Op of create -> 1; _ -> 0 end;
 +
weight(_S, create) -> 0; weight(_S, post) -> 5; weight(_S, fetch) -> 1.
 +
 +
prop_mbox() ->
 +
  ?SETUP(fun() -> qc_mbox:start_mocking(), fun() -> ok end end,
 +
  ?FORALL(Cmds, more_commands(50, commands(?MODULE)),
 +
  begin {H, S, Res} = run_commands(Cmds),
 +
    aggregate(command_names(Cmds),
 +
      pretty_commands(?MODULE, Cmds, {H, S, Res}, Res == ok)) end)).
 
</pre>
 
</pre>
  
Line 45: Line 216:
  
 
<pre>
 
<pre>
 +
-module(qc_cluster).
 +
 +
-compile(export_all).
 +
-include_lib("eqc/include/eqc.hrl").
 +
-include_lib("eqc/include/eqc_cluster.hrl").
 +
-include_lib("source_path.hrl").
 +
 +
components() -> [qc_cb, qc_mbox].
 +
 +
api_spec() -> eqc_cluster:api_spec(?MODULE).
 +
 +
setup_mocking() ->
 +
  eqc_mocking_c:start_mocking(mbox, api_spec(),
 +
    [ "cirq_buffer.h", "mbox.h" ],
 +
    [ ?AUTOSAR_SRC ++ "/src/mbox.c", ?AUTOSAR_SRC ++ "/src/cirq_buffer.c" ],
 +
    [ {cppflags, "-std=c99 -I " ++ ?AUTOSAR_SRC ++ "/include"} ],
 +
    components()).
 +
 +
property_mbox_cluster() ->
 +
  ?SETUP(fun() -> setup_mocking(), fun() -> ok end end,
 +
  ?FORALL(Cmds, commands(?MODULE),
 +
    begin {H, S, Res} = run_commands(Cmds),
 +
      aggregate(command_names(Cmds),
 +
        pretty_commands(?MODULE, Cmds, {H, S, Res}, Res == ok)) end )).
 
</pre>
 
</pre>

Revision as of 18:10, 27 December 2016

This page contains the complete CirqBuff and MBox QuickCheck models described in the paper entitled Modelling of Autosar Libraries for Large Scale Testing by Wojciech Mostowski, Thomas Arts, and John Hughes. The complete model archive can be downloaded here, below the complete model quote. The C source files referenced by the model are available on request, please contact Wojciech Mostowski.


source_path.hrl

-define(AUTOSAR_SRC, ".").

qc_cb.hrl

-record(cb_state, {ptr, size, elements, data_size}).

qc_cb_setup.erl

-module(qc_cb_setup).
-export([ setup/0 ]).

-include_lib("eqc/include/eqc_c.hrl").
-include_lib("source_path.hrl").

setup() -> eqc_c:start(cb,
  [ {cppflags, "-std=c99 -I " ++ ?AUTOSAR_SRC ++ "/include"},
    {c_src, ?AUTOSAR_SRC ++ "/src/cirq_buffer.c"} ]).

qc_cb.erl

-module(qc_cb).

-compile(export_all).
-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_component.hrl").
-include_lib("cb.hrl"). % Auto-generated
-include_lib("qc_cb.hrl").

initial_state() -> #cb_state{ elements=[] }.

invariant(S) -> length(S#cb_state.elements) =< S#cb_state.size.

postcondition_common(_S, {call, _, create, _, _ }, _Res) -> true;
postcondition_common(S, Call, Res) -> eq(Res, return_value(S, Call)).

create(Size, DataSize) -> cb:'CirqBuffDynCreate'(Size, DataSize).
create_args(_S) -> [nat(), nat()].
create_pre(S, [Size, _DataSize]) -> S#cb_state.ptr == undefined andalso Size > 0.
create_next(S, R, [Size, DataSize]) ->
  S#cb_state{ptr=R, size=Size, data_size = DataSize }.
create_callers() -> [qc_mbox].
create_return(_S, [Size, DataSize]) ->
  #'CirqBufferType' { maxCnt = Size, currCnt = 0, dataSize = DataSize,
    head = 'NULL', tail = 'NULL', bufStart = 'NULL', bufEnd = 'NULL' }.

push(Ptr, Val) ->  DataPtr = eqc_c:create_array(unsigned_char, Val),
  CallRes = cb:'CirqBuffPush'(Ptr, DataPtr), eqc_c:free(DataPtr), CallRes.
push_args(S) -> [S#cb_state.ptr, vector(S#cb_state.data_size, char())].
push_pre(S) ->
  S#cb_state.ptr /= undefined andalso length(S#cb_state.elements) < S#cb_state.size.
push_next(S, _R, [_Ptr, Value]) ->
  S#cb_state{elements = S#cb_state.elements ++ [Value]}.
push_return(S, _Args) -> % 0.
  if length(S#cb_state.elements) < 128 -> 0; true -> 1 end.
push_callers() -> [qc_mbox].

pop(Ptr, DataSize) -> 
  DataPtr = eqc_c:create_array(unsigned_char, [0 || _E <- lists:seq(1, DataSize)]),
  CallRes = cb:'CirqBuffPop'(Ptr, DataPtr),
  DataRes = eqc_c:read_array(DataPtr, DataSize),
  eqc_c:free(DataPtr), {DataRes, CallRes}.
pop_args(S) -> [S#cb_state.ptr, S#cb_state.data_size].
pop_pre(S) ->
   S#cb_state.ptr /= undefined andalso length(S#cb_state.elements) > 0.
pop_next(S, _R, _Args) -> S#cb_state{elements = tl(S#cb_state.elements)}.
pop_return(S, _Args) -> {hd(S#cb_state.elements), 0}. 
pop_callers() -> [qc_mbox].

prop_cb_length() -> ?SETUP(fun() -> qc_cb_setup:setup(), fun() -> ok end end,
  ?FORALL(Cmds, commands(?MODULE),
  begin {H, S, Res} = run_commands(Cmds),
    aggregate(command_names(Cmds),
      measure(num_commands,
        commands_length(Cmds), 
        pretty_commands(?MODULE, Cmds, {H, S, Res}, Res == ok))) end)).

prop_cb() -> ?SETUP(fun() -> qc_cb_setup:setup(), fun() -> ok end end,
  ?FORALL(Cmds, commands(?MODULE),
  begin {_, _, Res} = run_commands(Cmds), Res == ok end)).

qc_mbox.hrl

-record(mbox_state, {ptr, size, elements, cb_state}).

qc_mbox_capi.erl

-include_lib("source_path.hrl").

api_spec() -> #api_spec {
  language = c, mocking = eqc_mocking_c,
  modules  = [ #api_module{ name = mbox, functions = [
    #api_fun_c{ name = 'CirqBuffDynCreate', ret = 'CirqBufferType *',
                args = [ #api_arg_c{type = size_t, name = size, dir = in},
                         #api_arg_c{type = size_t, name = dataSize, dir = in} ],
                classify = {qc_cb, create} },
    #api_fun_c{ name = 'CirqBuffPush', ret = int,
                args = [ #api_arg_c{type = 'CirqBufferType *', name = cPtr, dir = in},
                         #api_arg_c{ type = 'void *', name = dataPtr, dir = in,
                           stored_type = 'unsigned char *',
                           buffer = {true, "cPtr->dataSize"}} ],
                classify = {qc_cb, push} },
    #api_fun_c{ name = 'CirqBuffPop',  ret = int,
                args = [ #api_arg_c{type = 'CirqBufferType *', name = cPtr, dir = in},
                         #api_arg_c{ type = 'void *', name = dataPtr, dir = out,
                           stored_type = 'unsigned char *',
                           buffer = {true, "cPtr->dataSize"}} ],
                classify = {qc_cb, pop} }]}]}.

start_mocking() -> eqc_mocking_c:start_mocking(mbox, ?MODULE:api_spec(),
  [ "Std_Types.h", "cirq_buffer.h", "mbox.h" ],
  [ ?AUTOSAR_SRC ++ "/src/mbox.c" ],
  [ {cppflags, "-std=c99 -I . -I " ++ ?AUTOSAR_SRC ++ "/include"} ]).

qc_mbox_setup.erl

-module(qc_mbox_setup).

-compile(export_all).

-include_lib("eqc/include/eqc_c.hrl").
-include_lib("eqc/include/eqc_mocking.hrl").

-include("qc_mbox_capi.erl").

qc_mbox.erl

-module(qc_mbox).

-compile(export_all).
-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_component.hrl").
-include_lib("qc_mbox.hrl").
-include_lib("qc_cb.hrl").

-include("mbox.hrl"). % Auto-generated
-include("qc_mbox_capi.erl").

-define(PTR_SIZE, 8). % Change resp. for test running platform (here 64 bit arch.)

initial_state() -> #mbox_state{ elements=[] }.

invariant(S) -> length(S#mbox_state.elements) =< S#mbox_state.size.

postcondition_common(_S, {call, _, create, _, _ }, _R) -> true;
postcondition_common(S, Call, Res) -> eq(Res, return_value(S, Call)).

create(Size) -> mbox:'Arc_MBoxCreate'(Size).
create_args(_S) -> [choose(1, 256)].
create_pre(S, [Size]) -> S#mbox_state.ptr == undefined andalso Size > 0.
create_next(S, R, [Size]) -> S#mbox_state{ptr=R, size=Size }.
create_callouts(_S, [Size]) -> 
  ?CALLOUT(mbox, 'CirqBuffDynCreate', [Size, ?PTR_SIZE], 
  #'CirqBufferType' { maxCnt = Size, currCnt = 0,
    dataSize = 8, head = 'NULL', tail = 'NULL',
    bufStart = 'NULL', bufEnd = 'NULL'}).

post(Ptr, Val) -> 
  DataPtr = eqc_c:create_array(unsigned_char, Val),
  CallRes = mbox:'Arc_MBoxPost'(Ptr, DataPtr),
  eqc_c:free(DataPtr), CallRes.
post_args(S) -> [S#mbox_state.ptr, vector(?PTR_SIZE, char())].
post_pre(S) -> S#mbox_state.ptr /= undefined
  andalso length(S#mbox_state.elements) < S#mbox_state.size.
post_next(S, _R, [_Ptr, Value]) ->
  S#mbox_state{elements = S#mbox_state.elements ++ [Value]}.
post_return(_S, _Args) -> 0.
post_callouts(S, [_Ptr, Value]) ->
  ?CALLOUT(mbox, 'CirqBuffPush', [?WILDCARD, Value],
  if length(S#mbox_state.elements) < 128 -> 0; true -> 1 end).

fetch(Ptr) -> 
  DataPtr = eqc_c:create_array(unsigned_char, [0 || _E <- lists:seq(1, ?PTR_SIZE)]),
  CallRes = mbox:'Arc_MBoxFetch'(Ptr, DataPtr),
  DataRes = eqc_c:read_array(DataPtr, ?PTR_SIZE),
  eqc_c:free(DataPtr), {DataRes, CallRes}.
fetch_args(S) -> [S#mbox_state.ptr].
fetch_pre(S) -> 
  S#mbox_state.ptr /= undefined andalso length(S#mbox_state.elements) > 0.
fetch_next(S, _R, [_Ptr]) -> S#mbox_state{elements = tl(S#mbox_state.elements)}.
fetch_return(S, [_Ptr]) -> {hd(S#mbox_state.elements), 0}.
fetch_callouts(S, [_Ptr]) -> 
  ?CALLOUT(mbox, 'CirqBuffPop', [?WILDCARD], { hd(S#mbox_state.elements), 0}).

weight(#mbox_state{ptr = undefined}, Op) -> case Op of create -> 1; _ -> 0 end;
weight(_S, create) -> 0; weight(_S, post) -> 5; weight(_S, fetch) -> 1.

prop_mbox() ->
  ?SETUP(fun() -> qc_mbox:start_mocking(), fun() -> ok end end,
  ?FORALL(Cmds, more_commands(50, commands(?MODULE)),
  begin {H, S, Res} = run_commands(Cmds),
    aggregate(command_names(Cmds),
      pretty_commands(?MODULE, Cmds, {H, S, Res}, Res == ok)) end)).

qc_cluster.erl

-module(qc_cluster).

-compile(export_all).
-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_cluster.hrl").
-include_lib("source_path.hrl").

components() -> [qc_cb, qc_mbox].

api_spec() -> eqc_cluster:api_spec(?MODULE).

setup_mocking() ->
  eqc_mocking_c:start_mocking(mbox, api_spec(),
    [ "cirq_buffer.h", "mbox.h" ],
    [ ?AUTOSAR_SRC ++ "/src/mbox.c", ?AUTOSAR_SRC ++ "/src/cirq_buffer.c" ],
    [ {cppflags, "-std=c99 -I " ++ ?AUTOSAR_SRC ++ "/include"} ],
    components()).

property_mbox_cluster() ->
  ?SETUP(fun() -> setup_mocking(), fun() -> ok end end,
  ?FORALL(Cmds, commands(?MODULE),
    begin {H, S, Res} = run_commands(Cmds),
      aggregate(command_names(Cmds),
        pretty_commands(?MODULE, Cmds, {H, S, Res}, Res == ok)) end )).
Retrieved from "https://wiki.hh.se/ceres/index.php?title=CirqBuff_and_MBox_QuickCheck_Models&oldid=6517"