From 8d06b93a6c4e22a3dfde0c70fb9140f67bf153a0 Mon Sep 17 00:00:00 2001 From: Sebastian Huber Date: Tue, 20 Apr 2021 14:55:58 +0200 Subject: spec: Specify memory allocation directives --- spec/c/if/einval.yml | 12 ++ spec/c/if/enomem.yml | 12 ++ spec/c/if/posix-memalign.yml | 12 ++ spec/c/req/posix-memalign.yml | 301 +++++++++++++++++++++++++++++++++++++++ spec/rtems/malloc/if/calloc.yml | 12 ++ spec/rtems/malloc/if/header.yml | 13 ++ spec/rtems/malloc/if/malloc.yml | 12 ++ spec/rtems/malloc/req/calloc.yml | 200 ++++++++++++++++++++++++++ spec/rtems/malloc/req/malloc.yml | 144 +++++++++++++++++++ 9 files changed, 718 insertions(+) create mode 100644 spec/c/if/einval.yml create mode 100644 spec/c/if/enomem.yml create mode 100644 spec/c/if/posix-memalign.yml create mode 100644 spec/c/req/posix-memalign.yml create mode 100644 spec/rtems/malloc/if/calloc.yml create mode 100644 spec/rtems/malloc/if/header.yml create mode 100644 spec/rtems/malloc/if/malloc.yml create mode 100644 spec/rtems/malloc/req/calloc.yml create mode 100644 spec/rtems/malloc/req/malloc.yml (limited to 'spec') diff --git a/spec/c/if/einval.yml b/spec/c/if/einval.yml new file mode 100644 index 00000000..1466ff98 --- /dev/null +++ b/spec/c/if/einval.yml @@ -0,0 +1,12 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +index-entries: [] +interface-type: unspecified-define +links: +- role: interface-placement + uid: errno-header +name: EINVAL +references: {} +type: interface diff --git a/spec/c/if/enomem.yml b/spec/c/if/enomem.yml new file mode 100644 index 00000000..38eb7253 --- /dev/null +++ b/spec/c/if/enomem.yml @@ -0,0 +1,12 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +index-entries: [] +interface-type: unspecified-define +links: +- role: interface-placement + uid: errno-header +name: ENOMEM +references: {} +type: interface diff --git a/spec/c/if/posix-memalign.yml b/spec/c/if/posix-memalign.yml new file mode 100644 index 00000000..6a45994d --- /dev/null +++ b/spec/c/if/posix-memalign.yml @@ -0,0 +1,12 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +index-entries: [] +interface-type: unspecified-function +links: +- role: interface-placement + uid: stdlib +name: posix_memalign +references: {} +type: interface diff --git a/spec/c/req/posix-memalign.yml b/spec/c/req/posix-memalign.yml new file mode 100644 index 00000000..7698f981 --- /dev/null +++ b/spec/c/req/posix-memalign.yml @@ -0,0 +1,301 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +functional-type: action +links: +- role: interface-function + uid: ../if/posix-memalign +post-conditions: +- name: Status + states: + - name: Zero + test-code: | + T_eq_int( ctx->status, 0 ); + text: | + The return value of ${../if/posix-memalign:/name} shall be equal to zero. + - name: EINVAL + test-code: | + T_eq_int( ctx->status, EINVAL ); + text: | + The return value of ${../if/posix-memalign:/name} shall be equal to + ${../if/einval:/name}. + - name: ENOMEM + test-code: | + T_eq_int( ctx->status, ENOMEM ); + text: | + The return value of ${../if/posix-memalign:/name} shall be equal to + ${../if/enomem:/name}. + test-epilogue: null + test-prologue: null +- name: MemptrVar + states: + - name: AreaBegin + test-code: | + T_eq_ptr( ctx->memptr, &ctx->memptr_obj ); + T_not_null( ctx->memptr_obj ); + text: | + The value of the object referenced by the memptr parameter shall be set + to the begin address of the allocated memory area after the return of the + ${../if/posix-memalign:/name} call. + - name: 'Null' + test-code: | + T_eq_ptr( ctx->memptr, &ctx->memptr_obj ); + T_null( ctx->memptr_obj ); + text: | + The value of the object referenced by the memptr parameter shall be set + to ${../if/null:/name} after the return of the + ${../if/posix-memalign:/name} call. + - name: Nop + test-code: | + T_eq_uptr( (uintptr_t) ctx->memptr_obj, 1 ); + text: | + Objects referenced by the memptr parameter in past calls to + ${../if/posix-memalign:/name} shall not be accessed by the + ${../if/posix-memalign:/name} call. + test-epilogue: null + test-prologue: null +- name: Alignment + states: + - name: Valid + test-code: | + T_eq_uptr( (uintptr_t) ctx->memptr_obj % 128, 0 ); + text: | + The begin address of the allocated memory area shall be an integral + multiple of the alignment parameter. + test-epilogue: null + test-prologue: null +- name: Size + states: + - name: Valid + test-code: | + /* Assume that the next allocation is done from adjacent memory */ + ptr = ctx->memptr_obj; + eno = posix_memalign( &ptr, ctx->alignment, ctx->size ); + T_eq_int( eno, 0 ); + T_not_null( ptr ); + a = (uintptr_t) ptr; + b = (uintptr_t) ctx->memptr_obj; + size = a < b ? b - a : a - b; + T_ge_uptr( size, ctx->size ); + text: | + The size of the allocated memory area shall greater than or equal to the + size parameter. + test-epilogue: null + test-prologue: | + void *ptr; + int eno; + uintptr_t a; + uintptr_t b; + uintptr_t size; +pre-conditions: +- name: Memptr + states: + - name: Valid + test-code: | + ctx->memptr = &ctx->memptr_obj; + text: | + While the memptr parameter references an object of type + ``void *``. + - name: 'Null' + test-code: | + ctx->memptr = NULL; + text: | + While the memptr parameter is equal to ${/c/if/null:/name}. + test-epilogue: null + test-prologue: null +- name: Alignment + states: + - name: Tiny + test-code: | + ctx->alignment = sizeof( void * ) - 1; + text: | + While the alignment parameter is less than sizeof( void * ). + - name: NotPower2 + test-code: | + ctx->alignment = sizeof( void * ) + 1; + text: | + While the alignment parameter is greater than or equal to + sizeof( void * ), while the alignment parameter is not a power of two. + - name: Huge + test-code: | + ctx->alignment = SIZE_MAX / 2 + 1; + text: | + While the alignment parameter is greater than or equal to + sizeof( void * ), while the alignment parameter is a power of two, while + the alignment parameter is too large to allocate a memory area with the + specified alignment. + - name: Valid + test-code: | + ctx->alignment = 128; + text: | + While the alignment parameter is greater than or equal to + sizeof( void * ), while the alignment parameter is a power of two, while + the alignment parameter is small enough to allocate a memory area with + the specified alignment. + test-epilogue: null + test-prologue: null +- name: Size + states: + - name: Huge + test-code: | + ctx->size = SIZE_MAX; + text: | + While the size parameter is not equal to zero, while the size parameter + is too large to allocate a memory area with the specified size. + - name: Zero + test-code: | + ctx->size = 0; + text: | + While the size parameter is equal to zero. + - name: Valid + test-code: | + ctx->size = sizeof( uint64_t ); + text: | + While the size parameter is not equal to zero, while the size parameter + is small enough to allocate a memory area with the specified size. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + ctx->status = posix_memalign( ctx->memptr, ctx->alignment, ctx->size ); +test-brief: null +test-cleanup: null +test-context: +- brief: | + This member provides a memory support context. + description: null + member: | + MemoryContext mem_ctx; +- brief: | + This member provides the object referenced by the memptr parameter. + description: null + member: | + void *memptr_obj +- brief: | + This member contains the return value of the directive call. + description: null + member: | + int status +- brief: | + This member specifies if the memptr parameter value. + description: null + member: | + void **memptr +- brief: | + This member specifies if the alignment parameter value. + description: null + member: | + size_t alignment +- brief: | + This member specifies if the size parameter value. + description: null + member: | + size_t size +test-context-support: null +test-description: null +test-header: null +test-includes: +- stdlib.h +- errno.h +test-local-includes: +- tx-support.h +test-prepare: | + ctx->memptr_obj = (void *)(uintptr_t) 1; +test-setup: + brief: null + code: | + MemorySave( &ctx->mem_ctx ); + description: null +test-stop: null +test-support: null +test-target: testsuites/validation/tc-mem-posix-memalign.c +test-teardown: + brief: null + code: | + MemoryRestore( &ctx->mem_ctx ); + description: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Status: EINVAL + MemptrVar: 'Null' + Alignment: N/A + Size: N/A + pre-conditions: + Memptr: + - Valid + Alignment: + - Tiny + - NotPower2 + Size: all +- enabled-by: true + post-conditions: + Status: EINVAL + MemptrVar: Nop + Alignment: N/A + Size: N/A + pre-conditions: + Memptr: + - 'Null' + Alignment: all + Size: all +- enabled-by: true + post-conditions: + Status: ENOMEM + MemptrVar: 'Null' + Alignment: N/A + Size: N/A + pre-conditions: + Memptr: + - Valid + Alignment: + - Huge + Size: + - Huge + - Valid +- enabled-by: true + post-conditions: + Status: ENOMEM + MemptrVar: 'Null' + Alignment: N/A + Size: N/A + pre-conditions: + Memptr: + - Valid + Alignment: + - Valid + Size: + - Huge +- enabled-by: true + post-conditions: + Status: Zero + MemptrVar: AreaBegin + Alignment: Valid + Size: Valid + pre-conditions: + Memptr: + - Valid + Alignment: + - Valid + Size: + - Valid +- enabled-by: true + post-conditions: + Status: Zero + MemptrVar: 'Null' + Alignment: Valid + Size: N/A + pre-conditions: + Memptr: + - Valid + Alignment: + - Valid + - Huge + Size: + - Zero +type: requirement diff --git a/spec/rtems/malloc/if/calloc.yml b/spec/rtems/malloc/if/calloc.yml new file mode 100644 index 00000000..10f902d2 --- /dev/null +++ b/spec/rtems/malloc/if/calloc.yml @@ -0,0 +1,12 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +index-entries: [] +interface-type: unspecified-function +links: +- role: interface-placement + uid: header +name: rtems_calloc +references: {} +type: interface diff --git a/spec/rtems/malloc/if/header.yml b/spec/rtems/malloc/if/header.yml new file mode 100644 index 00000000..a5e04488 --- /dev/null +++ b/spec/rtems/malloc/if/header.yml @@ -0,0 +1,13 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +brief: This header file defines the Memory Allocation API. +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +index-entries: [] +interface-type: container +links: +- role: interface-placement + uid: /if/domain +path: rtems/malloc.h +prefix: cpukit/include +type: interface diff --git a/spec/rtems/malloc/if/malloc.yml b/spec/rtems/malloc/if/malloc.yml new file mode 100644 index 00000000..aeb8e6e8 --- /dev/null +++ b/spec/rtems/malloc/if/malloc.yml @@ -0,0 +1,12 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +index-entries: [] +interface-type: unspecified-function +links: +- role: interface-placement + uid: header +name: rtems_malloc +references: {} +type: interface diff --git a/spec/rtems/malloc/req/calloc.yml b/spec/rtems/malloc/req/calloc.yml new file mode 100644 index 00000000..8e5b2597 --- /dev/null +++ b/spec/rtems/malloc/req/calloc.yml @@ -0,0 +1,200 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +functional-type: action +links: +- role: interface-function + uid: ../if/calloc +post-conditions: +- name: Status + states: + - name: 'Null' + test-code: | + T_null( ctx->ptr ); + text: | + The return value of ${../if/calloc:/name} shall be equal to + ${/c/if/null:/name}. + - name: AreaBegin + test-code: | + T_not_null( ctx->ptr ); + text: | + The return value of ${../if/calloc:/name} shall be equal to the begin + address of the allocated memory area. + test-epilogue: null + test-prologue: null +- name: Alignment + states: + - name: Valid + test-code: | + T_eq_uptr( (uintptr_t) ctx->ptr % CPU_HEAP_ALIGNMENT, 0 ); + text: | + The begin address of the allocated memory area shall be an integral + multiple of the heap alignment of the ${/glossary/target-arch:/term}. + test-epilogue: null + test-prologue: null +- name: Size + states: + - name: Valid + test-code: | + /* Assume that the next allocation is done from adjacent memory */ + ptr = ctx->ptr; + ctx->ptr = rtems_calloc( ctx->nelem, ctx->elsize ); + T_not_null( ptr ); + a = (uintptr_t) ptr; + b = (uintptr_t) ctx->ptr; + size = a < b ? b - a : a - b; + T_ge_uptr( size, ctx->nelem * ctx->elsize ); + text: | + The size of the allocated memory area shall greater than or equal to the + product of the ``nelem`` and ``elsize`` parameters. + test-epilogue: null + test-prologue: | + void *ptr; + uintptr_t a; + uintptr_t b; + uintptr_t size; +- name: Content + states: + - name: Zero + test-code: | + T_eq_u64( *(uint64_t *) ctx->ptr, 0 ); + text: | + The content of the allocated memory area shall be cleared to zero. + test-epilogue: null + test-prologue: null +pre-conditions: +- name: ElementCount + states: + - name: Huge + test-code: | + ctx->nelem = SIZE_MAX; + text: | + While the ``nelem`` parameter is not equal to zero, while the ``nelem`` + parameter is too large to allocate a memory area with the specified size. + - name: Zero + test-code: | + ctx->nelem = 0; + text: | + While the ``nelem`` parameter is equal to zero. + - name: Valid + test-code: | + ctx->nelem = 1; + text: | + While the ``nelem`` parameter is not equal to zero, while the ``nelem`` + parameter is small enough to allocate a memory area with the specified + size. + test-epilogue: null + test-prologue: null +- name: ElementSize + states: + - name: Huge + test-code: | + ctx->elsize = SIZE_MAX; + text: | + While the ``elsize`` parameter is not equal to zero, while the ``elsize`` + parameter is too large to allocate a memory area with the specified size. + - name: Zero + test-code: | + ctx->elsize = 0; + text: | + While the ``elsize`` parameter is equal to zero. + - name: Valid + test-code: | + ctx->elsize = sizeof( uint64_t ); + text: | + While the ``elsize`` parameter is not equal to zero, while the ``elsize`` + parameter is small enough to allocate a memory area with the specified + size. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + ctx->ptr = rtems_calloc( ctx->nelem, ctx->elsize ); +test-brief: null +test-cleanup: null +test-context: +- brief: | + This member provides a memory support context. + description: null + member: | + MemoryContext mem_ctx; +- brief: | + This member contains the return value of the ${../if/calloc:/name} call. + description: null + member: | + void *ptr +- brief: | + This member specifies if the ``nelem`` parameter value. + description: null + member: | + size_t nelem +- brief: | + This member specifies if the ``elsize`` parameter value. + description: null + member: | + size_t elsize +test-context-support: null +test-description: null +test-header: null +test-includes: +- rtems/malloc.h +test-local-includes: +- tx-support.h +test-prepare: null +test-setup: + brief: null + code: | + MemorySave( &ctx->mem_ctx ); + description: null +test-stop: null +test-support: null +test-target: testsuites/validation/tc-mem-rtems-calloc.c +test-teardown: + brief: null + code: | + MemoryRestore( &ctx->mem_ctx ); + description: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Status: AreaBegin + Alignment: Valid + Size: Valid + Content: Zero + pre-conditions: + ElementCount: + - Valid + ElementSize: + - Valid +- enabled-by: true + post-conditions: + Status: 'Null' + Alignment: Valid + Size: N/A + Content: N/A + pre-conditions: + ElementCount: + - Huge + - Zero + ElementSize: + - Huge + - Zero + - Valid +- enabled-by: true + post-conditions: + Status: 'Null' + Alignment: Valid + Size: N/A + Content: N/A + pre-conditions: + ElementCount: + - Valid + ElementSize: + - Huge + - Zero +type: requirement diff --git a/spec/rtems/malloc/req/malloc.yml b/spec/rtems/malloc/req/malloc.yml new file mode 100644 index 00000000..0d936fa6 --- /dev/null +++ b/spec/rtems/malloc/req/malloc.yml @@ -0,0 +1,144 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +functional-type: action +links: +- role: interface-function + uid: ../if/malloc +post-conditions: +- name: Status + states: + - name: 'Null' + test-code: | + T_null( ctx->ptr ); + text: | + The return value of ${../if/malloc:/name} shall be equal to + ${/c/if/null:/name}. + - name: AreaBegin + test-code: | + T_not_null( ctx->ptr ); + text: | + The return value of ${../if/malloc:/name} shall be equal to the begin + address of the allocated memory area. + test-epilogue: null + test-prologue: null +- name: Alignment + states: + - name: Valid + test-code: | + T_eq_uptr( (uintptr_t) ctx->ptr % CPU_HEAP_ALIGNMENT, 0 ); + text: | + The begin address of the allocated memory area shall be an integral + multiple of the heap alignment of the ${/glossary/target-arch:/term}. + test-epilogue: null + test-prologue: null +- name: Size + states: + - name: Valid + test-code: | + /* Assume that the next allocation is done from adjacent memory */ + ptr = ctx->ptr; + ctx->ptr = rtems_malloc( ctx->size ); + T_not_null( ptr ); + a = (uintptr_t) ptr; + b = (uintptr_t) ctx->ptr; + size = a < b ? b - a : a - b; + T_ge_uptr( size, ctx->size ); + text: | + The size of the allocated memory area shall greater than or equal to the + ``size` parameter. + test-epilogue: null + test-prologue: | + void *ptr; + uintptr_t a; + uintptr_t b; + uintptr_t size; +pre-conditions: +- name: Size + states: + - name: Huge + test-code: | + ctx->size = SIZE_MAX; + text: | + While the ``size`` parameter is not equal to zero, while the ``size`` + parameter is too large to allocate a memory area with the specified size. + - name: Zero + test-code: | + ctx->size = 0; + text: | + While the ``size`` parameter is equal to zero. + - name: Valid + test-code: | + ctx->size = 1; + text: | + While the ``size`` parameter is not equal to zero, while the ``size`` + parameter is small enough to allocate a memory area with the specified + size. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + ctx->ptr = rtems_malloc( ctx->size ); +test-brief: null +test-cleanup: null +test-context: +- brief: | + This member provides a memory support context. + description: null + member: | + MemoryContext mem_ctx; +- brief: | + This member contains the return value of the ${../if/malloc:/name} call. + description: null + member: | + void *ptr +- brief: | + This member specifies if the ``size`` parameter value. + description: null + member: | + size_t size +test-context-support: null +test-description: null +test-header: null +test-includes: +- rtems/malloc.h +test-local-includes: +- tx-support.h +test-prepare: null +test-setup: + brief: null + code: | + MemorySave( &ctx->mem_ctx ); + description: null +test-stop: null +test-support: null +test-target: testsuites/validation/tc-mem-rtems-malloc.c +test-teardown: + brief: null + code: | + MemoryRestore( &ctx->mem_ctx ); + description: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Status: AreaBegin + Alignment: Valid + Size: Valid + pre-conditions: + Size: + - Valid +- enabled-by: true + post-conditions: + Status: 'Null' + Alignment: Valid + Size: N/A + pre-conditions: + Size: + - Huge + - Zero +type: requirement -- cgit v1.2.3