CirqBuff and MBox QuickCheck Models
From CERES
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.
Contents
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 )).
