freertos: release the generic version source code
freertos runs on the second core (small one) of the CPU
This commit is contained in:
carbon
@ -0,0 +1,110 @@
|
||||
#
|
||||
# FreeRTOS memory safety proofs with CBMC.
|
||||
# Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
|
||||
#
|
||||
# Permission is hereby granted, free of charge, to any person
|
||||
# obtaining a copy of this software and associated documentation
|
||||
# files (the "Software"), to deal in the Software without
|
||||
# restriction, including without limitation the rights to use, copy,
|
||||
# modify, merge, publish, distribute, sublicense, and/or sell copies
|
||||
# of the Software, and to permit persons to whom the Software is
|
||||
# furnished to do so, subject to the following conditions:
|
||||
#
|
||||
# The above copyright notice and this permission notice shall be
|
||||
# included in all copies or substantial portions of the Software.
|
||||
#
|
||||
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||||
# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
|
||||
# MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
# NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
|
||||
# BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
|
||||
# ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
|
||||
# CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
|
||||
# SOFTWARE.
|
||||
#
|
||||
# http://aws.amazon.com/freertos
|
||||
# http://www.FreeRTOS.org
|
||||
#
|
||||
|
||||
{
|
||||
"ENTRY": "QueueGenericCreate",
|
||||
|
||||
# A CBMC pointer is an object id followed by an offset into the object.
|
||||
# The size of the offset is limited by the size of the object id.
|
||||
"CBMC_OBJECT_BITS": "7",
|
||||
"CBMC_OBJECT_MAX_SIZE": "\"((UINT32_MAX>>(CBMC_OBJECT_BITS+1))\"",
|
||||
|
||||
"CBMCFLAGS":
|
||||
[
|
||||
"--unwind 1",
|
||||
"--signed-overflow-check",
|
||||
"--pointer-overflow-check",
|
||||
"--unsigned-overflow-check"
|
||||
|
||||
],
|
||||
"OBJS":
|
||||
[
|
||||
"$(ENTRY)_harness.goto",
|
||||
"$(FREERTOS)/Source/list.goto",
|
||||
"$(FREERTOS)/Source/queue.goto"
|
||||
],
|
||||
"DEF":
|
||||
[
|
||||
{
|
||||
"QueueGenericCreate_default": [
|
||||
"CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}",
|
||||
"CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}",
|
||||
"configUSE_TRACE_FACILITY=0",
|
||||
"configGENERATE_RUN_TIME_STATS=0",
|
||||
"configUSE_MUTEXES=1",
|
||||
"'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'",
|
||||
"configSUPPORT_STATIC_ALLOCATION=1",
|
||||
"configUSE_QUEUE_SETS=0",
|
||||
"configSUPPORT_DYNAMIC_ALLOCATION=1"
|
||||
]
|
||||
},
|
||||
{
|
||||
"QueueGenericCreate_noMutex": [
|
||||
"CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}",
|
||||
"CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}",
|
||||
"configUSE_TRACE_FACILITY=0",
|
||||
"configGENERATE_RUN_TIME_STATS=0",
|
||||
"configUSE_MUTEXES=0",
|
||||
"configUSE_RECURSIVE_MUTEXES=0",
|
||||
"'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'",
|
||||
"configSUPPORT_STATIC_ALLOCATION=1",
|
||||
"configUSE_QUEUE_SETS=0",
|
||||
"configSUPPORT_DYNAMIC_ALLOCATION=1"
|
||||
]
|
||||
},
|
||||
{
|
||||
"QueueGenericCreate_noSTATIC_ALLOCATION": [
|
||||
"CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}",
|
||||
"CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}",
|
||||
"configUSE_TRACE_FACILITY=0",
|
||||
"configGENERATE_RUN_TIME_STATS=0",
|
||||
"configUSE_MUTEXES=1",
|
||||
"'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'",
|
||||
"configSUPPORT_STATIC_ALLOCATION=0",
|
||||
"configUSE_QUEUE_SETS=0",
|
||||
"configSUPPORT_DYNAMIC_ALLOCATION=1"
|
||||
]
|
||||
},
|
||||
{
|
||||
"QueueGenericCreate_useQueueSets": [
|
||||
"CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}",
|
||||
"CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}",
|
||||
"configUSE_TRACE_FACILITY=0",
|
||||
"configGENERATE_RUN_TIME_STATS=0",
|
||||
"configUSE_MUTEXES=1",
|
||||
"'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'",
|
||||
"configSUPPORT_STATIC_ALLOCATION=1",
|
||||
"configUSE_QUEUE_SETS=1",
|
||||
"configSUPPORT_DYNAMIC_ALLOCATION=1"
|
||||
]
|
||||
}
|
||||
],
|
||||
"GENERATE_HEADER": [
|
||||
"queue_datastructure.h"
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,50 @@
|
||||
/*
|
||||
* FreeRTOS memory safety proofs with CBMC.
|
||||
* Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
|
||||
*
|
||||
* Permission is hereby granted, free of charge, to any person
|
||||
* obtaining a copy of this software and associated documentation
|
||||
* files (the "Software"), to deal in the Software without
|
||||
* restriction, including without limitation the rights to use, copy,
|
||||
* modify, merge, publish, distribute, sublicense, and/or sell copies
|
||||
* of the Software, and to permit persons to whom the Software is
|
||||
* furnished to do so, subject to the following conditions:
|
||||
*
|
||||
* The above copyright notice and this permission notice shall be
|
||||
* included in all copies or substantial portions of the Software.
|
||||
*
|
||||
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||||
* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
|
||||
* MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
|
||||
* BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
|
||||
* ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
|
||||
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
|
||||
* SOFTWARE.
|
||||
*
|
||||
* http://aws.amazon.com/freertos
|
||||
* http://www.FreeRTOS.org
|
||||
*/
|
||||
|
||||
#include "FreeRTOS.h"
|
||||
#include "queue.h"
|
||||
#include "queue_datastructure.h"
|
||||
#include "cbmc.h"
|
||||
|
||||
|
||||
void harness(){
|
||||
UBaseType_t uxQueueLength;
|
||||
UBaseType_t uxItemSize;
|
||||
uint8_t ucQueueType;
|
||||
|
||||
size_t uxQueueStorageSize;
|
||||
__CPROVER_assume(uxQueueStorageSize < (UINT32_MAX>>8));
|
||||
|
||||
// QueueGenericCreate does not check for multiplication overflow
|
||||
__CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength);
|
||||
|
||||
// QueueGenericCreate asserts positive queue length
|
||||
__CPROVER_assume(uxQueueLength > ( UBaseType_t ) 0);
|
||||
|
||||
xQueueGenericCreate( uxQueueLength, uxItemSize, ucQueueType );
|
||||
}
|
||||
13
freertos/Test/CBMC/proofs/Queue/QueueGenericCreate/README.md
Normal file
13
freertos/Test/CBMC/proofs/Queue/QueueGenericCreate/README.md
Normal file
@ -0,0 +1,13 @@
|
||||
The harness and configurations in this folder show memory safety of
|
||||
QueueGenericCreate, given the assumption made in the harness.
|
||||
|
||||
The principal assumption is that (uxItemSize * uxQueueLength) + sizeof(Queue_t)
|
||||
does not overflow.
|
||||
|
||||
This proof is a work-in-progress. Proof assumptions are described in
|
||||
the harness. The proof also assumes the following functions are
|
||||
memory safe and have no side effects relevant to the memory safety of
|
||||
this function:
|
||||
|
||||
* vPortEnterCritical
|
||||
* vPortExitCritical
|
||||
Reference in New Issue
Block a user