diff options
Diffstat (limited to 'FreeRTOS/Test/CBMC/proofs/Queue')
69 files changed, 3166 insertions, 0 deletions
diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/Makefile.json new file mode 100644 index 000000000..4e26b37f8 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/Makefile.json @@ -0,0 +1,47 @@ +# +# 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": "QueueCreateCountingSemaphore", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/QueueCreateCountingSemaphore_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/QueueCreateCountingSemaphore_harness.c new file mode 100644 index 000000000..f079ecbdf --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/QueueCreateCountingSemaphore_harness.c @@ -0,0 +1,44 @@ +/* + * 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 "cbmc.h" + + +void harness(){ + UBaseType_t uxMaxCount; + UBaseType_t uxInitialCount; + + __CPROVER_assume(uxMaxCount != 0); + __CPROVER_assume(uxInitialCount <= uxMaxCount); + + xQueueCreateCountingSemaphore( uxMaxCount, uxInitialCount ); +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/README.md new file mode 100644 index 000000000..b01b0cfa6 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/README.md @@ -0,0 +1,10 @@ +Assuming uxMaxCount != 0 and uxInitialCount <= uxMaxCount, +this harness proves the memory safety of QueueCreateCountingSemaphore. + +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 diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/Makefile.json new file mode 100644 index 000000000..d9a9a8ec8 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/Makefile.json @@ -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 +# + +{ + "ENTRY": "QueueCreateCountingSemaphoreStatic", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0" + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/QueueCreateCountingSemaphoreStatic_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/QueueCreateCountingSemaphoreStatic_harness.c new file mode 100644 index 000000000..cb09c72b9 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/QueueCreateCountingSemaphoreStatic_harness.c @@ -0,0 +1,45 @@ +/* + * 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 "cbmc.h" + + +void harness(){ + UBaseType_t uxMaxCount; + UBaseType_t uxInitialCount; + + //xStaticQueue is required to be not null + StaticQueue_t xStaticQueue; + + //Checked invariant + __CPROVER_assume(uxMaxCount != 0); + __CPROVER_assume(uxInitialCount <= uxMaxCount); + xQueueCreateCountingSemaphoreStatic( uxMaxCount, uxInitialCount, &xStaticQueue ); +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/README.md new file mode 100644 index 000000000..c6103de51 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/README.md @@ -0,0 +1,11 @@ +Assuming uxMaxCount > 0, uxInitialCount <= uxMaxCount and the reference +to the storage area is not null, +this harness proves the memory saftey of QueueCreateCountingSemphoreStatic. + +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 diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/Makefile.json new file mode 100644 index 000000000..6409cd15a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/Makefile.json @@ -0,0 +1,47 @@ +# +# 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": "QueueCreateMutex", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/QueueCreateMutex_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/QueueCreateMutex_harness.c new file mode 100644 index 000000000..3528d9640 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/QueueCreateMutex_harness.c @@ -0,0 +1,38 @@ +/* + * 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 "cbmc.h" + +void harness() { + uint8_t ucQueueType; + + xQueueCreateMutex(ucQueueType); +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/README.md new file mode 100644 index 000000000..7c73daf04 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/README.md @@ -0,0 +1,14 @@ +This harness proves the memory safety of QueueCreateMutex +for totally unconstrained input. + +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 +* vPortGenerateSimulatedInterrupt +* xTaskGetSchedulerState +* xTaskPriorityDisinherit +* xTaskRemoveFromEventList diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/Makefile.json new file mode 100644 index 000000000..7de7e05dc --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/Makefile.json @@ -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 +# + +{ + "ENTRY": "QueueCreateMutexStatic", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0" + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/QueueCreateMutexStatic_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/QueueCreateMutexStatic_harness.c new file mode 100644 index 000000000..36848b6bf --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/QueueCreateMutexStatic_harness.c @@ -0,0 +1,41 @@ +/* + * 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 "cbmc.h" + + +void harness(){ + uint8_t ucQueueType; + + //The mutex storage is assumed to be not null. + StaticQueue_t xStaticQueue; + + xQueueCreateMutexStatic( ucQueueType, &xStaticQueue ); +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/README.md new file mode 100644 index 000000000..1e339f684 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/README.md @@ -0,0 +1,15 @@ +Given that the passed mutex storage area is not null, the QueueCreateMutexStatic +function is memory safe. + +Otherwise an assertion violation is triggered. + +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 +* vPortGenerateSimulatedInterrupt +* xTaskGetSchedulerState +* xTaskPriorityDisinherit diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/Configurations.json new file mode 100644 index 000000000..d7c4e86ed --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/Configurations.json @@ -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" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/QueueGenericCreate_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/QueueGenericCreate_harness.c new file mode 100644 index 000000000..4fa87f8d2 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/QueueGenericCreate_harness.c @@ -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 ); +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/README.md new file mode 100644 index 000000000..3b049bf3b --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/README.md @@ -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 diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/Configurations.json new file mode 100644 index 000000000..0acbc976e --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/Configurations.json @@ -0,0 +1,74 @@ +# +# 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": "QueueGenericCreateStatic", + + # 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/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + { + "QeueuGenericCreateStatic_DynamicAllocation": [ + "CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}", + "CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "configSUPPORT_STATIC_ALLOCATION=1", + "configSUPPORT_DYNAMIC_ALLOCATION=1" + ] + }, + { + "QeueuGenericCreateStatic_NoDynamicAllocation": [ + "CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}", + "CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "configSUPPORT_STATIC_ALLOCATION=1", + "configSUPPORT_DYNAMIC_ALLOCATION=0" + ] + } + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/QueueGenericCreateStatic_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/QueueGenericCreateStatic_harness.c new file mode 100644 index 000000000..553661cb2 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/QueueGenericCreateStatic_harness.c @@ -0,0 +1,62 @@ +/* + * 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; + + size_t uxQueueStorageSize; + uint8_t *pucQueueStorage = (uint8_t *) pvPortMalloc(uxQueueStorageSize); + + StaticQueue_t *pxStaticQueue = + (StaticQueue_t *) pvPortMalloc(sizeof(StaticQueue_t)); + + uint8_t ucQueueType; + + __CPROVER_assume(uxQueueStorageSize < (UINT32_MAX>>8)); + + // QueueGenericReset does not check for multiplication overflow + __CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength); + + // QueueGenericCreateStatic asserts positive queue length + __CPROVER_assume(uxQueueLength > ( UBaseType_t ) 0); + + // QueueGenericCreateStatic asserts the following equivalence + __CPROVER_assume( ( pucQueueStorage && uxItemSize ) || + ( !pucQueueStorage && !uxItemSize ) ); + + // QueueGenericCreateStatic asserts nonnull pointer + __CPROVER_assume(pxStaticQueue); + + xQueueGenericCreateStatic( uxQueueLength, uxItemSize, pucQueueStorage, pxStaticQueue, ucQueueType ); +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/README.md new file mode 100644 index 000000000..fb1466647 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/README.md @@ -0,0 +1,16 @@ +The harness proves memory safety of +QueueGenericCreateStatic under the assumption made in the harness. + +The principal assumption is that (uxItemSize * uxQueueLength) + sizeof(Queue_t) +does not overflow. Further, ucQueueStorage must only be null iff uxItemSize is null. +In addition, the passed queue storage is assumed to be allocated to the right size. + +The configurations for configSUPPORT_DYNAMIC_ALLOCATION set to 0 and 1 are checked. + +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 diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/Makefile.json new file mode 100644 index 000000000..1759310d8 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/Makefile.json @@ -0,0 +1,53 @@ +# +# 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": "QueueGenericReset", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0" + ], + "INC": [ + "." + ], + "GENERATE_HEADER":[ + "queue_datastructure.h" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/QueueGenericReset_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/QueueGenericReset_harness.c new file mode 100644 index 000000000..fbe4883a0 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/QueueGenericReset_harness.c @@ -0,0 +1,45 @@ +/* + * 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_init.h" + +#include "cbmc.h" + +struct QueueDefinition; + +void harness() { + BaseType_t xNewQueue; + + QueueHandle_t xQueue = xUnconstrainedQueue(); + if(xQueue != NULL) + { + xQueueGenericReset(xQueue, xNewQueue); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/README.md new file mode 100644 index 000000000..7645344aa --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/README.md @@ -0,0 +1,12 @@ +Assuming that the QueueHandel_t is not null and the assumptions made +for QueueGenericCreate hold, this harness proves the memory safety of QueueGenericReset. + +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 +* vPortGenerateSimulatedInterrupt +* xTaskRemoveFromEventList diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/Configurations.json new file mode 100644 index 000000000..64e3e6789 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/Configurations.json @@ -0,0 +1,76 @@ +# +# 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": "QueueGenericSend", + "LOCK_BOUND": 2, + "QUEUE_SEND_BOUND":3, + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check", + "--unwindset xQueueGenericSend.0:{QUEUE_SEND_BOUND},prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND}", + "--nondet-static" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.goto" + ], + "DEF": [ + { + "QueueGenericSend_noQueueSets": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configUSE_QUEUE_SETS=0", + "LOCK_BOUND={LOCK_BOUND}", + "QUEUE_SEND_BOUND={QUEUE_SEND_BOUND}" + ] + }, + { + "QueueGenericSend_QueueSets": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configUSE_QUEUE_SETS=1", + "LOCK_BOUND={LOCK_BOUND}", + "QUEUE_SEND_BOUND={QUEUE_SEND_BOUND}" + ] + } + ], + "INC": [ + "." + ], + "GENERATE_HEADER":[ + "queue_datastructure.h" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/QueueGenericSend_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/QueueGenericSend_harness.c new file mode 100644 index 000000000..fae965ad8 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/QueueGenericSend_harness.c @@ -0,0 +1,127 @@ +/* + * 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_init.h" +#include "tasksStubs.h" + +#include "cbmc.h" + +#ifndef LOCK_BOUND + #define LOCK_BOUND 4 +#endif + +#ifndef QUEUE_SEND_BOUND + #define QUEUE_SEND_BOUND 4 +#endif + +#if( configUSE_QUEUE_SETS == 0 ) +BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) +{ + if(pxQueue->uxItemSize > ( UBaseType_t ) 0) + { + __CPROVER_assert(__CPROVER_r_ok(pvItemToQueue, ( size_t ) pxQueue->uxItemSize), "pvItemToQueue region must be readable"); + if(xPosition == queueSEND_TO_BACK){ + __CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize), "pxQueue->pcWriteTo region must be writable"); + }else{ + __CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize), "pxQueue->u.xQueue.pcReadFrom region must be writable"); + } + return pdFALSE; + }else + { + return nondet_BaseType_t(); + } +} +#else + BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) + { + Queue_t *pxQueueSetContainer = pxQueue->pxQueueSetContainer; + configASSERT( pxQueueSetContainer ); + } + + void prvUnlockQueue( Queue_t * const pxQueue ) { + configASSERT( pxQueue ); + if( pxQueue->pxQueueSetContainer != NULL ) + { + prvNotifyQueueSetContainer(pxQueue); + } + listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ); + pxQueue->cTxLock = queueUNLOCKED; + + listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToSend ) ); + pxQueue->cRxLock = queueUNLOCKED; + } + +#endif + +void harness(){ + //Initialise the tasksStubs + vInitTaskCheckForTimeOut(0, QUEUE_SEND_BOUND - 1); + xState = nondet_basetype(); + QueueHandle_t xQueue = + xUnconstrainedQueueBoundedItemSize(2); + + TickType_t xTicksToWait; + if(xState == taskSCHEDULER_SUSPENDED){ + xTicksToWait = 0; + } + + if(xQueue){ + void *pvItemToQueue = pvPortMalloc(xQueue->uxItemSize); + BaseType_t xCopyPosition; + + if(xCopyPosition == queueOVERWRITE){ + xQueue->uxLength = 1; + } + + if(xQueue->uxItemSize == 0) + { + /* uxQueue->xQueueType is a pointer to the head of the queue storage area. + If an item has a sice, this pointer must not be modified after init. + Otherwise some of the write statements will fail. */ + xQueue->uxQueueType = nondet_int8_t(); + pvItemToQueue = 0; + } + /* This code checks explicitly for violations of the pxQueue->uxMessagesWaiting < pxQueue->uxLength + invariant. */ + xQueue->uxMessagesWaiting = nondet_UBaseType_t(); + + /* These values are decremented during a while loop interacting with task.c. + This interaction is currently abstracted away.*/ + xQueue->cTxLock = LOCK_BOUND - 1; + xQueue->cRxLock = LOCK_BOUND - 1; + + if(!pvItemToQueue){ + xQueue->uxItemSize = 0; + } + + xQueueGenericSend( xQueue, pvItemToQueue, xTicksToWait, xCopyPosition ); + } +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/README.md new file mode 100644 index 000000000..9dae1be0a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/README.md @@ -0,0 +1,19 @@ +The harness in this folder proves the memory safety of QueueGenericSend +with and without QueueSets. It is abstracting away the task pool and concurrency +related functions and assumes the parameters to be initialized to valid data structures. +Further, prvCopyDataToQueue, prvUnlockQueue and prvNotifyQueueSetContainer are abstracted away. + +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 +* vPortGenerateSimulatedInterrupt +* vTaskInternalSetTimeOutState +* vTaskMissedYield +* vTaskPlaceOnEventList +* vTaskSuspendAll +* xTaskRemoveFromEventList +* xTaskResumeAll diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/Configurations.json new file mode 100644 index 000000000..92892ca85 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/Configurations.json @@ -0,0 +1,68 @@ +# +# 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": "QueueGenericSendFromISR", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check", + "--nondet-static" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + { + "QueueGenericSendFromISR_noQueueSets": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configUSE_QUEUE_SETS=0" + ] + }, + { + "QueueGenericSendFromISR_QueueSets": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configUSE_QUEUE_SETS=1" + ] + } + ], + "INC": [ + "." + ], + "GENERATE_HEADER":[ + "queue_datastructure.h" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/QueueGenericSendFromISR_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/QueueGenericSendFromISR_harness.c new file mode 100644 index 000000000..0c8a98cf2 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/QueueGenericSendFromISR_harness.c @@ -0,0 +1,85 @@ +/* + * 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_init.h" + +#include "cbmc.h" + +#ifndef ITEM_BOUND + #define ITEM_BOUND 10 +#endif + +#if( configUSE_QUEUE_SETS == 0 ) + BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) + { + if(pxQueue->uxItemSize > ( UBaseType_t ) 0) + { + __CPROVER_assert(__CPROVER_r_ok(pvItemToQueue, ( size_t ) pxQueue->uxItemSize), "pvItemToQueue region must be readable"); + if(xPosition == queueSEND_TO_BACK){ + __CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize), "pxQueue->pcWriteTo region must be writable"); + }else{ + __CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize), "pxQueue->u.xQueue.pcReadFrom region must be writable"); + } + return pdFALSE; + }else + { + return nondet_BaseType_t(); + } + } +#endif + +void harness(){ + QueueHandle_t xQueue = xUnconstrainedQueueBoundedItemSize(ITEM_BOUND); + + + if( xQueue ){ + void *pvItemToQueue = pvPortMalloc(xQueue->uxItemSize); + BaseType_t *xHigherPriorityTaskWoken = pvPortMalloc(sizeof(BaseType_t)); + BaseType_t xCopyPosition; + if(xQueue->uxItemSize == 0) + { + /* uxQueue->xQueueType is a pointer to the head of the queue storage area. + If an item has a size, this pointer must not be modified after init. + Otherwise some of the write statements will fail. */ + xQueue->uxQueueType = nondet_int8_t(); + pvItemToQueue = 0; + } + /* This code checks explicitly for violations of the pxQueue->uxMessagesWaiting < pxQueue->uxLength + invariant. */ + xQueue->uxMessagesWaiting = nondet_UBaseType_t(); + if(!pvItemToQueue){ + xQueue->uxItemSize = 0; + } + if(xCopyPosition == 2 ){ + __CPROVER_assume(xQueue->uxLength == 1); + } + xQueueGenericSendFromISR( xQueue, pvItemToQueue, xHigherPriorityTaskWoken, xCopyPosition ); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/README.md new file mode 100644 index 000000000..cfc20618b --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/README.md @@ -0,0 +1,12 @@ +The harness in this folder proves the memory safety of QueueGenericSendFromISR +with and without QueueSets. It is abstracting away the task pool and concurrency +related functions. Further, it uses a stub for prvCopyDataToQueue. + +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 +* xTaskRemoveFromEventList diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/Makefile.json new file mode 100644 index 000000000..ecc2b6230 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/Makefile.json @@ -0,0 +1,53 @@ +# +# 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": "QueueGetMutexHolder", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0" + ], + "INC": [ + "." + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/QueueGetMutexHolder_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/QueueGetMutexHolder_harness.c new file mode 100644 index 000000000..1bba9b7f8 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/QueueGetMutexHolder_harness.c @@ -0,0 +1,41 @@ +/* + * 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_init.h" +#include "queue.h" + +#include "cbmc.h" + +void harness() { + QueueHandle_t xSemaphore = xUnconstrainedQueue(); + if (xSemaphore) { + xSemaphore->uxQueueType = nondet_uint8_t(); + xQueueGetMutexHolder(xSemaphore); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/README.md new file mode 100644 index 000000000..d028ea9e7 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/README.md @@ -0,0 +1,10 @@ +This harness proves the memory safety of QueueGetMutexHolder assuming the passed +semaphore is not null. + +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 diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/Makefile.json new file mode 100644 index 000000000..647a0d03f --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/Makefile.json @@ -0,0 +1,53 @@ +# +# 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": "QueueGetMutexHolderFromISR", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0" + ], + "INC": [ + "." + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/QueueGetMutexHolderFromISR_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/QueueGetMutexHolderFromISR_harness.c new file mode 100644 index 000000000..a0543a70c --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/QueueGetMutexHolderFromISR_harness.c @@ -0,0 +1,41 @@ +/* + * 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(){ + QueueHandle_t xSemaphore = pvPortMalloc(sizeof(Queue_t)); + if (xSemaphore) { + xQueueGetMutexHolderFromISR( xSemaphore ); + } +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/README.md new file mode 100644 index 000000000..629ea7336 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/README.md @@ -0,0 +1,5 @@ +Assuming that xSemaphore is a pointer to an allocated Queue_t instance, +this harness proves the memory safety of QueueGetMutexHolderFromISR. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/Configurations.json new file mode 100644 index 000000000..ff71fd642 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/Configurations.json @@ -0,0 +1,72 @@ +# +# 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": "QueueGiveFromISR", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check", + "--nondet-static" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + { + "QueueGiveFromISR_default": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configSUPPORT_STATIC_ALLOCATION=1", + "configSUPPORT_DYNAMIC_ALLOCATION=1", + "configUSE_QUEUE_SETS=0" + ] + }, + { + "QueueGiveFromISR_QueueSets": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configSUPPORT_STATIC_ALLOCATION=1", + "configSUPPORT_DYNAMIC_ALLOCATION=1", + "configUSE_QUEUE_SETS=1" + ] + } + ], + "INC": [ + "$(FREERTOS)/Test/CBMC/proofs/CBMCStubLibrary/", + "." + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/QueueGiveFromISR_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/QueueGiveFromISR_harness.c new file mode 100644 index 000000000..b6be1aa80 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/QueueGiveFromISR_harness.c @@ -0,0 +1,43 @@ +/* + * 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_init.h" + +#include "cbmc.h" + +void harness(){ + QueueHandle_t xQueue = xUnconstrainedMutex(); + BaseType_t *xHigherPriorityTaskWoken = pvPortMalloc(sizeof(BaseType_t)); + if(xQueue){ + xQueue->uxMessagesWaiting = nondet_UBaseType_t(); + xQueueGiveFromISR( xQueue, xHigherPriorityTaskWoken ); + } + +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/README.md new file mode 100644 index 000000000..75da9156d --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/README.md @@ -0,0 +1,15 @@ +Assuming the xQueue is allocated to a valid memory block and abstracting +away concurrency and task pool related functions, this harness proves the memory +safety of QueueGiveFromISR. + +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 +* vPortGenerateSimulatedInterrupt +* xTaskGetSchedulerState +* xTaskPriorityDisinherit +* xTaskRemoveFromEventList diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/Makefile.json new file mode 100644 index 000000000..8d1720fcd --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/Makefile.json @@ -0,0 +1,54 @@ +# +# 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": "QueueGiveMutexRecursive", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "configUSE_RECURSIVE_MUTEXES=1" + ], + "INC": [ + "." + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/QueueGiveMutexRecursive_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/QueueGiveMutexRecursive_harness.c new file mode 100644 index 000000000..6df3a36ee --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/QueueGiveMutexRecursive_harness.c @@ -0,0 +1,48 @@ +/* + * 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() { + uint8_t ucQueueType; + QueueHandle_t xMutex = + xQueueCreateMutex( ucQueueType); + if (xMutex) { + xMutex->uxQueueType = ucQueueType; + UBaseType_t uxCounter; + /* This assumption is explained in the queue.c file inside the method body + xQueueGiveMutexRecursive and guards against an underflow error. */ + __CPROVER_assume(uxCounter > 0); + xMutex->u.xSemaphore.uxRecursiveCallCount = uxCounter; + xQueueGiveMutexRecursive(xMutex); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/README.md new file mode 100644 index 000000000..962350e52 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/README.md @@ -0,0 +1,16 @@ +Assuming that the xMutex parameter is initialized to a valid pointer and +abstracting concurrency and task pool related functions, this harness +proves the memory safety of QueueGiveMutexRecursive. + +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 +* vPortGenerateSimulatedInterrupt +* xTaskGetCurrentTaskHandle +* xTaskGetSchedulerState +* xTaskPriorityDisinherit +* xTaskRemoveFromEventList diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/Makefile.json new file mode 100644 index 000000000..6c8806b2c --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/Makefile.json @@ -0,0 +1,52 @@ +# +# 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": "QueueMessagesWaiting", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0" + ], + "INC": [ + "." + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/QueueMessagesWaiting_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/QueueMessagesWaiting_harness.c new file mode 100644 index 000000000..8e5f3d050 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/QueueMessagesWaiting_harness.c @@ -0,0 +1,41 @@ +/* + * 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(){ + QueueHandle_t xQueue = pvPortMalloc(sizeof(Queue_t)); + + if(xQueue){ + uxQueueMessagesWaiting( xQueue ); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/README.md new file mode 100644 index 000000000..811b5abb5 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/README.md @@ -0,0 +1,12 @@ +Assuming the parameter passed to QueueMessagesWaiting is a pointer to a Queue_t +struct, this harness proves the memory safety of QueueMessagesWaiting. +The concurrency related functions vPortEnterCrititcal and vPortExitCritical +are abstracted away. + +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 diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/Makefile.json new file mode 100644 index 000000000..797d788a1 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/Makefile.json @@ -0,0 +1,60 @@ +# +# 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": "QueuePeek", + "LOCK_BOUND":4, + "QUEUE_PEEK_BOUND" :4, + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check", + "--unwindset prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND},xQueuePeek.0:{QUEUE_PEEK_BOUND}", + "--nondet-static" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "LOCK_BOUND={LOCK_BOUND}", + "QUEUE_PEEK_BOUND={QUEUE_PEEK_BOUND}", + "INCLUDE_xTaskGetSchedulerState=1" + ], + "INC": [ + "." + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/QueuePeek_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/QueuePeek_harness.c new file mode 100644 index 000000000..53c2c9050 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/QueuePeek_harness.c @@ -0,0 +1,79 @@ +/* + * 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_init.h" +#include "tasksStubs.h" + +#include "cbmc.h" + +#ifndef LOCK_BOUND + #define LOCK_BOUND 4 +#endif + +#ifndef QUEUE_PEEK_BOUND + #define QUEUE_PEEK_BOUND 4 +#endif + +QueueHandle_t xQueue; + + +/* This method is called to initialize pxTimeOut. + Setting up the data structure is not interesting for the proof, + but the harness uses it to model a release + on the queue after first check. */ +void vTaskInternalSetTimeOutState( TimeOut_t * const pxTimeOut ){ + xQueue-> uxMessagesWaiting = nondet_BaseType_t(); +} + +void harness(){ + xQueue = xUnconstrainedQueueBoundedItemSize(10); + + //Initialise the tasksStubs + vInitTaskCheckForTimeOut(0, QUEUE_PEEK_BOUND - 1); + + TickType_t xTicksToWait; + if(xState == taskSCHEDULER_SUSPENDED){ + xTicksToWait = 0; + } + + if(xQueue){ + __CPROVER_assume(xQueue->cTxLock < LOCK_BOUND - 1); + __CPROVER_assume(xQueue->cRxLock < LOCK_BOUND - 1); + + void *pvItemToQueue = pvPortMalloc(xQueue->uxItemSize); + + /* In case malloc fails as this is otherwise an invariant violation. */ + if(!pvItemToQueue){ + xQueue->uxItemSize = 0; + } + + xQueuePeek( xQueue, pvItemToQueue, xTicksToWait ); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/README.md new file mode 100644 index 000000000..87a791e7c --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/README.md @@ -0,0 +1,18 @@ +Assuming xQueue and pvItemToQueue are non-null pointers allocated to the right +size, this harness proves the memory safety of QueueGenericPeek. Some of the +task pool behavior is abstracted away. Nevertheless, some of the concurrent +behavior has been modeled to allow full coverage of QueuePeek. + +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 +* vPortGenerateSimulatedInterrupt +* vTaskMissedYield +* vTaskPlaceOnEventList +* vTaskSuspendAll +* xTaskRemoveFromEventList +* xTaskResumeAll diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/Makefile.json new file mode 100644 index 000000000..568e517b1 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/Makefile.json @@ -0,0 +1,61 @@ +# +# 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": "QueueReceive", + "LOCK_BOUND": 2, + "QUEUE_RECEIVE_BOUND": 3, + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check", + "--unwindset xQueueReceive.0:{QUEUE_RECEIVE_BOUND},prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND}", + "--nondet-static" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "INCLUDE_xTaskGetSchedulerState=1", + "QUEUE_RECEIVE_BOUND={QUEUE_RECEIVE_BOUND}", + "LOCK_BOUND={LOCK_BOUND}" + ], + "INC": [ + "." + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/QueueReceive_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/QueueReceive_harness.c new file mode 100644 index 000000000..533f69caf --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/QueueReceive_harness.c @@ -0,0 +1,88 @@ +/* + * 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_init.h" +#include "tasksStubs.h" +#include "cbmc.h" + +/* prvUnlockQueue is going to decrement this value to 0 in the loop. + We need a bound for the loop. Using 4 has a reasonable performance resulting + in 3 unwinding iterations of the loop. The loop is mostly modifying a + data structure in task.c that is not in the scope of the proof. */ +#ifndef LOCK_BOUND + #define LOCK_BOUND 4 +#endif + +/* This code checks for time outs. This value is used to bound the time out + wait period. The stub function xTaskCheckForTimeOut used to model + this wait time will be bounded to this define. */ +#ifndef QUEUE_RECEIVE_BOUND + #define QUEUE_RECEIVE_BOUND 4 +#endif + +/* If the item size is not bounded, the proof does not finish in a reasonable + time due to the involved memcpy commands. */ +#ifndef MAX_ITEM_SIZE + #define MAX_ITEM_SIZE 20 +#endif + +QueueHandle_t xQueue; + +/* This method is used to model side effects of concurrency. + The initialization of pxTimeOut is not relevant for this harness. */ +void vTaskInternalSetTimeOutState( TimeOut_t * const pxTimeOut ){ + __CPROVER_assert(__CPROVER_w_ok(&(pxTimeOut->xOverflowCount), sizeof(BaseType_t)), "pxTimeOut should be a valid pointer and xOverflowCount writable"); + __CPROVER_assert(__CPROVER_w_ok(&(pxTimeOut->xTimeOnEntering), sizeof(TickType_t)), "pxTimeOut should be a valid pointer and xTimeOnEntering writable"); + xQueue->uxMessagesWaiting = nondet_BaseType_t(); +} + +void harness(){ + vInitTaskCheckForTimeOut(0, QUEUE_RECEIVE_BOUND - 1); + + xQueue = xUnconstrainedQueueBoundedItemSize(MAX_ITEM_SIZE); + + + TickType_t xTicksToWait; + if(xState == taskSCHEDULER_SUSPENDED){ + xTicksToWait = 0; + } + + if(xQueue){ + xQueue->cTxLock = LOCK_BOUND - 1; + xQueue->cRxLock = LOCK_BOUND - 1; + + void *pvBuffer = pvPortMalloc(xQueue->uxItemSize); + if(!pvBuffer){ + xQueue->uxItemSize = 0; + } + xQueueReceive( xQueue, pvBuffer, xTicksToWait ); + } + +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/README.md new file mode 100644 index 000000000..b76b9c5e0 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/README.md @@ -0,0 +1,17 @@ +Assuming the bound described in the harness, this harness proves memory safety +for the QueueReceive function abstracting away +the task pool and concurrency functions. + +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 +* vPortGenerateSimulatedInterrupt +* vTaskMissedYield +* vTaskPlaceOnEventList +* vTaskSuspendAll +* xTaskRemoveFromEventList +* xTaskResumeAll diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/Makefile.json new file mode 100644 index 000000000..e084d22f2 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/Makefile.json @@ -0,0 +1,54 @@ +# +# 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": "QueueReceiveFromISR", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'" + ], + "INC": [ + "." + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/QueueReceiveFromISR_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/QueueReceiveFromISR_harness.c new file mode 100644 index 000000000..9a4b2cf2a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/QueueReceiveFromISR_harness.c @@ -0,0 +1,53 @@ +/* + * 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_init.h" +#include "cbmc.h" + +/* If the item size is not bounded, the proof does not finish in a reasonable + time due to the involved memcpy commands. */ +#ifndef MAX_ITEM_SIZE + #define MAX_ITEM_SIZE 10 +#endif + +void harness(){ + QueueHandle_t xQueue = + xUnconstrainedQueueBoundedItemSize(MAX_ITEM_SIZE); + + BaseType_t *xHigherPriorityTaskWoken = pvPortMalloc(sizeof(BaseType_t)); + + if(xQueue){ + void *pvBuffer = pvPortMalloc(xQueue->uxItemSize); + if(!pvBuffer){ + xQueue->uxItemSize = 0; + } + xQueueReceiveFromISR( xQueue, pvBuffer, xHigherPriorityTaskWoken ); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/README.md new file mode 100644 index 000000000..7da35e498 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/README.md @@ -0,0 +1,12 @@ +Assuming the bound declared in the harness, this harness proves the memory +safety the QueueReceiveFromISR abstracting +away the task pool and concurrency related functions. + +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 +* xTaskRemoveFromEventList diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/Makefile.json new file mode 100644 index 000000000..07f7c1034 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/Makefile.json @@ -0,0 +1,60 @@ +# +# 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": "QueueSemaphoreTake", + + # This bound on queue size is needed to bound a loop in prvUnlockQueue + "QUEUE_BOUND": 5, + + "CBMCFLAGS": [ + "--unwind 2", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check", + "--nondet-static", + "--unwindset prvUnlockQueue.0:{QUEUE_BOUND},prvUnlockQueue.1:{QUEUE_BOUND},xQueueSemaphoreTake.0:3" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "PRV_UNLOCK_QUEUE_BOUND={QUEUE_BOUND}" + ], + "INC": [ + "." + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/QueueSemaphoreTake_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/QueueSemaphoreTake_harness.c new file mode 100644 index 000000000..21fdbf80e --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/QueueSemaphoreTake_harness.c @@ -0,0 +1,88 @@ +/* + * 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_init.h" +#include "tasksStubs.h" +#include "cbmc.h" + +BaseType_t state; +QueueHandle_t xQueue; +BaseType_t counter; + +BaseType_t xTaskGetSchedulerState(void) +{ + return state; +} + +void vTaskInternalSetTimeOutState( TimeOut_t * const pxTimeOut ) +{ + /* QueueSemaphoreTake might be blocked to wait for + another process to release a token to the semaphore. + This is currently not in the CBMC model. Anyhow, + vTaskInternalSetTimeOutState is set a timeout for + QueueSemaphoreTake operation. We use this to model a successful + release during wait time. */ + UBaseType_t bound; + __CPROVER_assume((bound >= 0 && xQueue->uxLength >= bound)); + xQueue->uxMessagesWaiting = bound; +} + +void harness() +{ + /* Init task stub to make sure that the third loop iteration + simulates a time out */ + vInitTaskCheckForTimeOut(0, 3); + + xQueue = xUnconstrainedMutex(); + TickType_t xTicksToWait; + + if(state == taskSCHEDULER_SUSPENDED){ + xTicksToWait = 0; + } + if (xQueue) { + /* Bounding the loop in prvUnlockQueue to + PRV_UNLOCK_QUEUE_BOUND. As the loop is not relevant + in this proof the value might be set to any + positive 8-bit integer value. We subtract one, + because the bound must be one greater than the + amount of loop iterations. */ + __CPROVER_assert(PRV_UNLOCK_QUEUE_BOUND > 0, "Make sure, a valid macro value is chosen."); + xQueue->cTxLock = PRV_UNLOCK_QUEUE_BOUND - 1; + xQueue->cRxLock = PRV_UNLOCK_QUEUE_BOUND - 1; + ((&(xQueue->xTasksWaitingToReceive))->xListEnd).pxNext->xItemValue = nondet_ticktype(); + + /* This assumptions is required to prevent an overflow in l. 2057 of queue.c + in the prvGetDisinheritPriorityAfterTimeout() function. */ + __CPROVER_assume( ( + ( UBaseType_t ) listGET_ITEM_VALUE_OF_HEAD_ENTRY( &( xQueue->xTasksWaitingToReceive ) ) + <= ( ( UBaseType_t ) configMAX_PRIORITIES))); + xQueueSemaphoreTake(xQueue, xTicksToWait); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/README.md new file mode 100644 index 000000000..27122656a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/README.md @@ -0,0 +1,22 @@ +Assuming the bound specified in the harness and abstracting the task pool and +concurrency functions, this harness proves the memory safety of QueueSemaphoreTake. +Some of the task pool functions are used to model concurrent behavior required +to trigger all branches during the model creation. + +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: + +* pvTaskIncrementMutexHeldCount +* vPortEnterCritical +* vPortExitCritical +* vPortGenerateSimulatedInterrupt +* vTaskMissedYield +* vTaskPlaceOnEventList +* vTaskPriorityDisinheritAfterTimeout +* vTaskSuspendAll +* xTaskPriorityDisinherit +* xTaskPriorityInherit +* xTaskRemoveFromEventList +* xTaskResumeAll diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/Makefile.json new file mode 100644 index 000000000..33b6e6cf2 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/Makefile.json @@ -0,0 +1,52 @@ +# +# 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": "QueueSpacesAvailable", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0" + ], + "INC": [ + "." + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/QueueSpacesAvailable_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/QueueSpacesAvailable_harness.c new file mode 100644 index 000000000..c56f9008e --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/QueueSpacesAvailable_harness.c @@ -0,0 +1,41 @@ +/* + * 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_init.h" +#include "cbmc.h" + +void harness(){ + QueueHandle_t xQueue = xUnconstrainedQueue(); + + // QueueSpacesAvailable asserts nonnull pointer + __CPROVER_assume(xQueue); + + uxQueueSpacesAvailable( xQueue ); +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/README.md new file mode 100644 index 000000000..482b4f6ce --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/README.md @@ -0,0 +1,9 @@ +This harness proves that QueueSpacesAvailable is memory safe. + +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 diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/Makefile.json new file mode 100644 index 000000000..210ead6b4 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/Makefile.json @@ -0,0 +1,62 @@ +# +# 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 +# + +{ + # This bound on queue size is needed to bound a loop in prvUnlockQueue + "PRV_UNLOCK_UNWINDING_BOUND": 4, + + # This is a bound on the timeout cycles + "QueueSemaphoreTake_BOUND": 4, + + "ENTRY": "QueueTakeMutexRecursive", + "CBMCFLAGS": [ + "--unwind {QueueSemaphoreTake_BOUND}", + "--unwindset prvUnlockQueue.0:{PRV_UNLOCK_UNWINDING_BOUND},prvUnlockQueue.1:{PRV_UNLOCK_UNWINDING_BOUND}", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.goto" + ], + "DEF": [ + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "PRV_UNLOCK_UNWINDING_BOUND={PRV_UNLOCK_UNWINDING_BOUND}", + "QueueSemaphoreTake_BOUND={QueueSemaphoreTake_BOUND}" + ], + "INC": [ + "." + ], + "GENERATE_HEADER": [ + "queue_datastructure.h" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/QueueTakeMutexRecursive_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/QueueTakeMutexRecursive_harness.c new file mode 100644 index 000000000..9864321e0 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/QueueTakeMutexRecursive_harness.c @@ -0,0 +1,71 @@ +/* + * 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 "tasksStubs.h" +#include "queue_datastructure.h" +#include "cbmc.h" + +QueueHandle_t xMutex; + +void vTaskInternalSetTimeOutState( TimeOut_t * const pxTimeOut ) +{ + /* QueueSemaphoreTake might be blocked to wait for + another process to release a token to the semaphore. + This is currently not in the CBMC model. Anyhow, + vTaskInternalSetTimeOutState is set a timeout for + QueueSemaphoreTake operation. We use this to model a successful + release during wait time. */ + UBaseType_t bound; + __CPROVER_assume((bound >= 0 && xMutex->uxLength >= bound)); + xMutex->uxMessagesWaiting = bound; +} + +BaseType_t xTaskGetSchedulerState( void ) { + BaseType_t ret; + __CPROVER_assume(ret != taskSCHEDULER_SUSPENDED); + return ret; +} + +void harness() { + uint8_t ucQueueType; + xMutex = xQueueCreateMutex(ucQueueType); + TickType_t xTicksToWait; + + /* Init task stub to make sure that the QueueSemaphoreTake_BOUND - 1 + loop iteration simulates a time out */ + vInitTaskCheckForTimeOut(0, QueueSemaphoreTake_BOUND - 1); + + if(xMutex){ + xMutex->cTxLock = PRV_UNLOCK_UNWINDING_BOUND - 1; + xMutex->cRxLock = PRV_UNLOCK_UNWINDING_BOUND - 1; + xMutex->uxMessagesWaiting = nondet_UBaseType_t(); + xQueueTakeMutexRecursive(xMutex, xTicksToWait); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/README.md new file mode 100644 index 000000000..4513147d9 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/README.md @@ -0,0 +1,23 @@ +Assuming that the parameter is valid mutex data structure and reasonable +bounded, this harness proves the memory safety of QueueTakeMutexRecursive. +Task pool and concurrency functions are abstracted away and replaced with +required stubs to drive coverage. + +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: + +* pvTaskIncrementMutexHeldCount +* vPortEnterCritical +* vPortExitCritical +* vPortGenerateSimulatedInterrupt +* vTaskMissedYield +* vTaskPlaceOnEventList +* vTaskPriorityDisinheritAfterTimeout +* vTaskSuspendAll +* xTaskGetCurrentTaskHandle +* xTaskPriorityDisinherit +* xTaskPriorityInherit +* xTaskRemoveFromEventList +* xTaskResumeAll diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/Configurations.json new file mode 100644 index 000000000..521839c3c --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/Configurations.json @@ -0,0 +1,71 @@ +# +# 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": "prvCopyDataToQueue", + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + { + "prvCopyDataToQueue_default" : [ + "'configPRECONDITION(X)=__CPROVER_assume(X)'", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "configUSE_MUTEXES=1" + + ] + }, + { + "prvCopyDataToQueue_noMutex" : [ + "'configPRECONDITION(X)=__CPROVER_assume(X)'", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "configUSE_MUTEXES=0", + "configUSE_RECURSIVE_MUTEXES=0" + ] + } + ], + "INC": [ + "." + ], + "GENERATE_HEADER":[ + "queue_datastructure.h" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/README.md new file mode 100644 index 000000000..ee6bc03e0 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/README.md @@ -0,0 +1,12 @@ +This harness proves the memory safety of the prvNotifyQueuSetContainer method. +It assumes that the queue is initalized to a valid datastructure. +The concurrency functions are abstracted away. + +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 +* xTaskPriorityDisinherit diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/prvCopyDataToQueue_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/prvCopyDataToQueue_harness.c new file mode 100644 index 000000000..80398bfa2 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/prvCopyDataToQueue_harness.c @@ -0,0 +1,54 @@ +/* + * 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_init.h" +#include "cbmc.h" + +BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ); + +void harness(){ + QueueHandle_t xQueue = xUnconstrainedQueueBoundedItemSize(10); + + + if( xQueue ){ + void *pvItemToQueue = pvPortMalloc(xQueue->uxItemSize); + if( !pvItemToQueue ) + { + xQueue->uxItemSize = 0; + } + if(xQueue->uxItemSize == 0) + { + xQueue->uxQueueType = nondet_int8_t(); + } + BaseType_t xPosition; + prvCopyDataToQueue( xQueue, pvItemToQueue, xPosition ); + } + +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/Configurations.json new file mode 100644 index 000000000..516ea7df1 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/Configurations.json @@ -0,0 +1,73 @@ +# +# 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": "prvNotifyQueueSetContainer", + "LOCK_BOUND": 2, + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check", + "--unwindset prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND}" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + { + "prvNotifyQueueSetContainer_Mutex" : [ + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "configUSE_MUTEXES=1", + "configUSE_RECURSIVE_MUTEXES=1", + "configUSE_QUEUE_SETS=1" + + ] + }, + { + "prvNotifyQueueSetContainer_noMutex" : [ + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "configUSE_MUTEXES=0", + "configUSE_RECURSIVE_MUTEXES=0", + "configUSE_QUEUE_SETS=1" + ] + } + ], + "INC": [ + "." + ], + "GENERATE_HEADER":[ + "queue_datastructure.h" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/README.md new file mode 100644 index 000000000..6dddc4172 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/README.md @@ -0,0 +1,14 @@ +This harness proves the memory safety of the prvNotifyQueuSetContainer method. +It assumes that the queue is initalized to a valid datastructure and added +to a QueueSet. The concurrency functions and task pool functions are abstracted +away. prvCopyDataToQueue is replaced with a stub checking the preconditions +for prvCopyDataToQueue to be sucessful. + +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 +* xTaskRemoveFromEventList diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/prvNotifyQueueSetContainer_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/prvNotifyQueueSetContainer_harness.c new file mode 100644 index 000000000..e9575adab --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/prvNotifyQueueSetContainer_harness.c @@ -0,0 +1,93 @@ +/* + * 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" + +#ifndef LOCK_BOUND + #define LOCK_BOUND 4 +#endif + +BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue, const BaseType_t xCopyPosition ); + +BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) +{ + if(pxQueue->uxItemSize > ( UBaseType_t ) 0) + { + __CPROVER_assert(__CPROVER_r_ok(pvItemToQueue, ( size_t ) pxQueue->uxItemSize), "pvItemToQueue region must be readable"); + if(xPosition == queueSEND_TO_BACK){ + __CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize), "pxQueue->pcWriteTo region must be writable"); + }else{ + __CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize), "pxQueue->u.xQueue.pcReadFrom region must be writable"); + } + return pdFALSE; + }else + { + return nondet_BaseType_t(); + } +} + +QueueSetHandle_t xUnconstrainedQueueSet() +{ + UBaseType_t uxEventQueueLength = 2; + QueueSetHandle_t xSet = xQueueCreateSet(uxEventQueueLength); + if( xSet ) + { + xSet->cTxLock = nondet_int8_t(); + xSet->cRxLock = nondet_int8_t(); + xSet->uxMessagesWaiting = nondet_UBaseType_t(); + xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t(); + xSet->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t(); + } + return xSet; +} + +void harness(){ + UBaseType_t uxQueueLength; + UBaseType_t uxItemSize; + uint8_t ucQueueType; + __CPROVER_assume(uxQueueLength > 0); + __CPROVER_assume(uxItemSize < 10); + /* The implicit assumption for the QueueGenericCreate method is, + that there are no overflows in the computation and the inputs are safe. + There is no check for this in the code base */ + UBaseType_t upper_bound = portMAX_DELAY - sizeof(Queue_t); + __CPROVER_assume(uxItemSize < (upper_bound)/uxQueueLength); + QueueHandle_t xQueue = + xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType); + if( xQueue ){ + xQueueAddToSet(xQueue, xUnconstrainedQueueSet()); + if(xQueue->pxQueueSetContainer) { + __CPROVER_assume(xQueue->pxQueueSetContainer->uxMessagesWaiting < xQueue->pxQueueSetContainer->uxLength); + BaseType_t xCopyPosition = nondet_BaseType_t(); + prvNotifyQueueSetContainer(xQueue, xCopyPosition ); + } + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/Configurations.json new file mode 100644 index 000000000..3d52cb481 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/Configurations.json @@ -0,0 +1,74 @@ +# +# 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": "prvUnlockQueue", + "LOCK_BOUND": 2, + "CBMCFLAGS": [ + "--unwind 1", + "--signed-overflow-check", + "--pointer-overflow-check", + "--unsigned-overflow-check", + "--unwindset prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND}" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/Source/queue.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": [ + { + "prvUnlockQueue_noQueueSets" : [ + "'configPRECONDITION(X)=__CPROVER_assume(X)'", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "LOCK_BOUND={LOCK_BOUND}", + "configUSE_QUEUE_SETS=0" + + ] + }, + { + "prvUnlockQueue_QueueSets" : [ + "'configPRECONDITION(X)=__CPROVER_assume(X)'", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "LOCK_BOUND={LOCK_BOUND}", + "configUSE_QUEUE_SETS=1" + ] + } + ], + "INC": [ + "." + ], + "GENERATE_HEADER":[ + "queue_datastructure.h" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/README.md b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/README.md new file mode 100644 index 000000000..8cd98b22c --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/README.md @@ -0,0 +1,12 @@ +This harness proves the memory safety of the prvUnlockQueue function. +It is abstracting away the prvCopyDataToQueue function and task pools and concurrency functions. + +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 +* vTaskMissedYield +* xTaskRemoveFromEventList diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/prvUnlockQueue_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/prvUnlockQueue_harness.c new file mode 100644 index 000000000..1db424998 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/prvUnlockQueue_harness.c @@ -0,0 +1,103 @@ +/* + * 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" + +#ifndef LOCK_BOUND + #define LOCK_BOUND 4 +#endif + +void prvUnlockQueue( Queue_t * const pxQueue ); + +BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) +{ + if(pxQueue->uxItemSize > ( UBaseType_t ) 0) + { + __CPROVER_assert(__CPROVER_r_ok(pvItemToQueue, ( size_t ) pxQueue->uxItemSize), "pvItemToQueue region must be readable"); + if(xPosition == queueSEND_TO_BACK){ + __CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize), "pxQueue->pcWriteTo region must be writable"); + }else{ + __CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize), "pxQueue->u.xQueue.pcReadFrom region must be writable"); + } + return pdFALSE; + }else + { + return nondet_BaseType_t(); + } +} + +QueueSetHandle_t xUnconstrainedQueueSet() +{ + UBaseType_t uxEventQueueLength = 2; + QueueSetHandle_t xSet = xQueueCreateSet(uxEventQueueLength); + if( xSet ) + { + xSet->cTxLock = nondet_int8_t(); + xSet->cRxLock = nondet_int8_t(); + xSet->uxMessagesWaiting = nondet_UBaseType_t(); + xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t(); + /* This is an invariant checked with a couple of asserts in the code base. + If it is false from the beginning, there is no chance for the proof to succeed*/ + __CPROVER_assume(xSet->uxMessagesWaiting < xSet->uxLength); + xSet->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t(); + } + return xSet; +} + +void harness(){ + UBaseType_t uxQueueLength; + UBaseType_t uxItemSize; + uint8_t ucQueueType; + __CPROVER_assume(uxQueueLength > 0); + __CPROVER_assume(uxItemSize < 10); + /* The implicit assumption for the QueueGenericCreate method is, + that there are no overflows in the computation and the inputs are safe. + There is no check for this in the code base */ + UBaseType_t upper_bound = portMAX_DELAY - sizeof(Queue_t); + __CPROVER_assume(uxItemSize < (upper_bound)/uxQueueLength); + QueueHandle_t xQueue = + xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType); + if(xQueue){ + xQueue->cTxLock = LOCK_BOUND - 1; + xQueue->cRxLock = LOCK_BOUND - 1; + xQueue->uxMessagesWaiting = nondet_UBaseType_t(); + /* This is an invariant checked with a couple of asserts in the code base. + If it is false from the beginning, there is no chance for the proof to succeed*/ + __CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength); + xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t(); + xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t(); + #if( configUSE_QUEUE_SETS == 1) + xQueueAddToSet(xQueue, xUnconstrainedQueueSet()); + #endif + prvUnlockQueue(xQueue); + } +} |