diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/patches')
15 files changed, 1082 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/.gitattributes b/FreeRTOS-Plus/Test/CBMC/patches/.gitattributes new file mode 100644 index 000000000..a41fc7b45 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/.gitattributes @@ -0,0 +1,2 @@ +# It seems git apply does not want crlf line endings on Windows +*.patch eol=lf diff --git a/FreeRTOS-Plus/Test/CBMC/patches/.gitignore b/FreeRTOS-Plus/Test/CBMC/patches/.gitignore new file mode 100644 index 000000000..4dec98ff0 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/.gitignore @@ -0,0 +1,2 @@ +auto_patch* +patched diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch b/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch new file mode 100644 index 000000000..29cde0e77 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch @@ -0,0 +1,79 @@ +This patch removes the volatile qualifier from some global variable +declarations in the tasks.c file. For task pool proofs, we are running +`goto-instrument` with the `--nondet-volatile` flag on, which causes reads from +volatile variable to be nondeterministic (i.e., any possible value can be +returned). This is actually the desired behavior for volatile variables +regarding verification purposes. However, this causes a lot of trouble when +such variables are pointers, since one of the possible values we can get when +dereferencing a volatile pointer is `NULL`. + +In the case of `uxPendedTicks`, a non-volatile copy of the variable is done +before the following loop in tasks.c (lines 2231-2255): + +{ + UBaseType_t uxPendedCounts = uxPendedTicks; /* Non-volatile copy. */ + + if( uxPendedCounts > ( UBaseType_t ) 0U ) + { + do + { + if( xTaskIncrementTick() != pdFALSE ) + { + xYieldPending = pdTRUE; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + --uxPendedCounts; + } while( uxPendedCounts > ( UBaseType_t ) 0U ); + + uxPendedTicks = 0; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } +} + +Here, `uxPendedTicks` could return any value, making it impossible to unwind +(or unroll) this loop in CBMC. Therefore, we require `uxPendedTicks` to behave +as a regular variable so that the loop can be unwound. + +--- +diff --git a/FreeRTOS/Source/tasks.c b/FreeRTOS/Source/tasks.c +index ff657733..8b57d198 100644 +--- a/FreeRTOS/Source/tasks.c ++++ b/FreeRTOS/Source/tasks.c +@@ -331,7 +331,7 @@ typedef tskTCB TCB_t; + + /*lint -save -e956 A manual analysis and inspection has been used to determine + which static variables must be declared volatile. */ +-PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL; ++PRIVILEGED_DATA TCB_t * pxCurrentTCB = NULL; + + /* Lists for ready and blocked tasks. -------------------- + xDelayedTaskList1 and xDelayedTaskList2 could be move to function scople but +@@ -340,8 +340,8 @@ the static qualifier. */ + PRIVILEGED_DATA static List_t pxReadyTasksLists[ configMAX_PRIORITIES ];/*< Prioritised ready tasks. */ + PRIVILEGED_DATA static List_t xDelayedTaskList1; /*< Delayed tasks. */ + PRIVILEGED_DATA static List_t xDelayedTaskList2; /*< Delayed tasks (two lists are used - one for delays that have overflowed the current tick count. */ +-PRIVILEGED_DATA static List_t * volatile pxDelayedTaskList; /*< Points to the delayed task list currently being used. */ +-PRIVILEGED_DATA static List_t * volatile pxOverflowDelayedTaskList; /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */ ++PRIVILEGED_DATA static List_t * pxDelayedTaskList; /*< Points to the delayed task list currently being used. */ ++PRIVILEGED_DATA static List_t * pxOverflowDelayedTaskList; /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */ + PRIVILEGED_DATA static List_t xPendingReadyList; /*< Tasks that have been readied while the scheduler was suspended. They will be moved to the ready list when the scheduler is resumed. */ + + #if( INCLUDE_vTaskDelete == 1 ) +@@ -368,10 +368,10 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseTyp + + /* Other file private variables. --------------------------------*/ + PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseType_t ) 0U; + PRIVILEGED_DATA static volatile TickType_t xTickCount = ( TickType_t ) configINITIAL_TICK_COUNT; + PRIVILEGED_DATA static volatile UBaseType_t uxTopReadyPriority = tskIDLE_PRIORITY; + PRIVILEGED_DATA static volatile BaseType_t xSchedulerRunning = pdFALSE; +-PRIVILEGED_DATA static volatile TickType_t xPendedTicks = ( TickType_t ) 0U; ++PRIVILEGED_DATA static TickType_t xPendedTicks = ( TickType_t ) 0U; + PRIVILEGED_DATA static volatile BaseType_t xYieldPending = pdFALSE; + PRIVILEGED_DATA static volatile BaseType_t xNumOfOverflows = ( BaseType_t ) 0; + PRIVILEGED_DATA static UBaseType_t uxTaskNumber = ( UBaseType_t ) 0U; diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch b/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch new file mode 100644 index 000000000..5a79ae8cd --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch @@ -0,0 +1,22 @@ +diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c +index df2b9c8c..c2265c26 100644 +--- a/FreeRTOS/Source/queue.c ++++ b/FreeRTOS/Source/queue.c +@@ -105,7 +105,7 @@ static BaseType_t prvIsQueueFull( const Queue_t *pxQueue ) PRIVILEGED_FUNCTION; + * Copies an item into the queue, either at the front of the queue or the + * back of the queue. + */ +-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION; ++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION; + + /* + * Copies an item out of a queue. +@@ -1985,7 +1985,7 @@ Queue_t * const pxQueue = xQueue; + #endif /* configUSE_MUTEXES */ + /*-----------------------------------------------------------*/ + +-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) ++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) + { + BaseType_t xReturn = pdFALSE; + UBaseType_t uxMessagesWaiting; diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch b/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch new file mode 100644 index 000000000..9cbe7cf5f --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch @@ -0,0 +1,22 @@ +diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c +index 17a6964e..24a40c29 100644 +--- a/FreeRTOS/Source/queue.c ++++ b/FreeRTOS/Source/queue.c +@@ -207,7 +207,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer + * Checks to see if a queue is a member of a queue set, and if so, notifies + * the queue set that the queue contains data. + */ +- static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION; ++ BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION; + #endif + + /* +@@ -2887,7 +2887,7 @@ Queue_t * const pxQueue = xQueue; + + #if ( configUSE_QUEUE_SETS == 1 ) + +- static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) ++ BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) + { + Queue_t *pxQueueSetContainer = pxQueue->pxQueueSetContainer; + BaseType_t xReturn = pdFALSE; diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch b/FreeRTOS-Plus/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch new file mode 100644 index 000000000..eaae401c6 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch @@ -0,0 +1,22 @@ +diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c +index 17a6964e..60ea3e69 100644 +--- a/FreeRTOS/Source/queue.c ++++ b/FreeRTOS/Source/queue.c +@@ -175,7 +175,7 @@ typedef xQUEUE Queue_t; + * to indicate that a task may require unblocking. When the queue in unlocked + * these lock counts are inspected, and the appropriate action taken. + */ +-static void prvUnlockQueue( Queue_t * const pxQueue ) PRIVILEGED_FUNCTION; ++void prvUnlockQueue( Queue_t * const pxQueue ) PRIVILEGED_FUNCTION; + + /* + * Uses a critical section to determine if there is any data in a queue. +@@ -2175,7 +2175,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer + } + /*-----------------------------------------------------------*/ + +-static void prvUnlockQueue( Queue_t * const pxQueue ) ++void prvUnlockQueue( Queue_t * const pxQueue ) + { + /* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. */ + diff --git a/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h new file mode 100644 index 000000000..28de2bd15 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h @@ -0,0 +1,237 @@ +/* + * FreeRTOS Kernel V10.0.1 + * Copyright (C) 2017 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 + */ + +#ifndef FREERTOS_CONFIG_H +#define FREERTOS_CONFIG_H + +/*----------------------------------------------------------- +* Application specific definitions. +* +* These definitions should be adjusted for your particular hardware and +* application requirements. +* +* THESE PARAMETERS ARE DESCRIBED WITHIN THE 'CONFIGURATION' SECTION OF THE +* FreeRTOS API DOCUMENTATION AVAILABLE ON THE FreeRTOS.org WEB SITE. +* http://www.freertos.org/a00110.html +* +* The bottom of this file contains some constants specific to running the UDP +* stack in this demo. Constants specific to FreeRTOS+TCP itself (rather than +* the demo) are contained in FreeRTOSIPConfig.h. +*----------------------------------------------------------*/ +#define configENABLE_BACKWARD_COMPATIBILITY 1 +#define configUSE_PREEMPTION 1 +#define configUSE_PORT_OPTIMISED_TASK_SELECTION 1 +#define configMAX_PRIORITIES ( 7 ) +#define configTICK_RATE_HZ ( 1000 ) /* In this non-real time simulated environment the tick frequency has to be at least a multiple of the Win32 tick frequency, and therefore very slow. */ +#define configMINIMAL_STACK_SIZE ( ( unsigned short ) 60 ) /* In this simulated case, the stack only has to hold one small structure as the real stack is part of the Win32 thread. */ +#define configTOTAL_HEAP_SIZE ( ( size_t ) ( 2048U * 1024U ) ) +#define configMAX_TASK_NAME_LEN ( 15 ) +#define configUSE_16_BIT_TICKS 0 +#define configIDLE_SHOULD_YIELD 1 +#define configUSE_CO_ROUTINES 0 +#ifndef configUSE_MUTEXES + #define configUSE_MUTEXES 1 +#endif +#ifndef configUSE_RECURSIVE_MUTEXES + #define configUSE_RECURSIVE_MUTEXES 1 +#endif +#define configQUEUE_REGISTRY_SIZE 0 +#define configUSE_APPLICATION_TASK_TAG 1 +#define configUSE_COUNTING_SEMAPHORES 1 +#define configUSE_ALTERNATIVE_API 0 +#define configNUM_THREAD_LOCAL_STORAGE_POINTERS 3 /* FreeRTOS+FAT requires 2 pointers if a CWD is supported. */ +#define configRECORD_STACK_HIGH_ADDRESS 1 + +/* Hook function related definitions. */ +#ifndef configUSE_TICK_HOOK + #define configUSE_TICK_HOOK 0 +#endif +#define configUSE_IDLE_HOOK 1 +#define configUSE_MALLOC_FAILED_HOOK 1 +#define configCHECK_FOR_STACK_OVERFLOW 0 /* Not applicable to the Win32 port. */ + +/* Software timer related definitions. */ +#define configUSE_TIMERS 1 +#define configTIMER_TASK_PRIORITY ( configMAX_PRIORITIES - 1 ) +#define configTIMER_QUEUE_LENGTH 5 +#define configTIMER_TASK_STACK_DEPTH ( configMINIMAL_STACK_SIZE * 2 ) + +/* Event group related definitions. */ +#define configUSE_EVENT_GROUPS 1 + +/* Co-routine definitions. */ +#define configUSE_CO_ROUTINES 0 +#define configMAX_CO_ROUTINE_PRIORITIES ( 2 ) + +/* Memory allocation strategy. */ +#ifndef configSUPPORT_DYNAMIC_ALLOCATION + #define configSUPPORT_DYNAMIC_ALLOCATION 1 +#endif +#ifndef configSUPPORT_STATIC_ALLOCATION + #define configSUPPORT_STATIC_ALLOCATION 1 +#endif + + +/* Set the following definitions to 1 to include the API function, or zero + * to exclude the API function. */ +#define INCLUDE_vTaskPrioritySet 1 +#define INCLUDE_uxTaskPriorityGet 1 +#define INCLUDE_vTaskDelete 1 +#define INCLUDE_vTaskCleanUpResources 0 +#ifndef INCLUDE_vTaskSuspend + #define INCLUDE_vTaskSuspend 1 +#endif +#define INCLUDE_vTaskDelayUntil 1 +#define INCLUDE_vTaskDelay 1 +#define INCLUDE_uxTaskGetStackHighWaterMark 1 +#ifndef INCLUDE_xTaskGetSchedulerState + #define INCLUDE_xTaskGetSchedulerState 1 +#endif +#define INCLUDE_xTimerGetTimerTaskHandle 0 +#define INCLUDE_xTaskGetIdleTaskHandle 0 +#define INCLUDE_xQueueGetMutexHolder 1 +#define INCLUDE_eTaskGetState 1 +#define INCLUDE_xEventGroupSetBitsFromISR 1 +#define INCLUDE_xTimerPendFunctionCall 1 +#define INCLUDE_xTaskGetCurrentTaskHandle 1 +#define INCLUDE_xTaskAbortDelay 1 + +/* This demo makes use of one or more example stats formatting functions. These + * format the raw data provided by the uxTaskGetSystemState() function in to human + * readable ASCII form. See the notes in the implementation of vTaskList() within + * FreeRTOS/Source/tasks.c for limitations. configUSE_STATS_FORMATTING_FUNCTIONS + * is set to 2 so the formatting functions are included without the stdio.h being + * included in tasks.c. That is because this project defines its own sprintf() + * functions. */ +#define configUSE_STATS_FORMATTING_FUNCTIONS 1 + +/* Assert call defined for debug builds. */ +extern void vAssertCalled( const char * pcFile, + uint32_t ulLine ); +#ifndef configASSERT +#define configASSERT( x ) if( ( x ) == 0 ) vAssertCalled( __FILE__, __LINE__ ) +#endif + +/* Remove logging in formal verification */ +#define configPRINTF( X ) + +/* Non-format version thread-safe print. */ +#define configPRINT_STRING( X ) + +/* Application specific definitions follow. **********************************/ + +/* If configINCLUDE_DEMO_DEBUG_STATS is set to one, then a few basic IP trace + * macros are defined to gather some UDP stack statistics that can then be viewed + * through the CLI interface. */ +#define configINCLUDE_DEMO_DEBUG_STATS 1 + +/* The size of the global output buffer that is available for use when there + * are multiple command interpreters running at once (for example, one on a UART + * and one on TCP/IP). This is done to prevent an output buffer being defined by + * each implementation - which would waste RAM. In this case, there is only one + * command interpreter running, and it has its own local output buffer, so the + * global buffer is just set to be one byte long as it is not used and should not + * take up unnecessary RAM. */ +#define configCOMMAND_INT_MAX_OUTPUT_SIZE 1 + +/* Only used when running in the FreeRTOS Windows simulator. Defines the + * priority of the task used to simulate Ethernet interrupts. */ +#define configMAC_ISR_SIMULATOR_PRIORITY ( configMAX_PRIORITIES - 1 ) + +/* This demo creates a virtual network connection by accessing the raw Ethernet + * or WiFi data to and from a real network connection. Many computers have more + * than one real network port, and configNETWORK_INTERFACE_TO_USE is used to tell + * the demo which real port should be used to create the virtual port. The ports + * available are displayed on the console when the application is executed. For + * example, on my development laptop setting configNETWORK_INTERFACE_TO_USE to 4 + * results in the wired network being used, while setting + * configNETWORK_INTERFACE_TO_USE to 2 results in the wireless network being + * used. */ +#define configNETWORK_INTERFACE_TO_USE ( 0L ) + +/* The address of an echo server that will be used by the two demo echo client + * tasks: + * http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_Echo_Clients.html, + * http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/UDP_Echo_Clients.html. */ +#define configECHO_SERVER_ADDR0 192 +#define configECHO_SERVER_ADDR1 168 +#define configECHO_SERVER_ADDR2 2 +#define configECHO_SERVER_ADDR3 6 +#define configTCP_ECHO_CLIENT_PORT 7 + +/* Default MAC address configuration. The demo creates a virtual network + * connection that uses this MAC address by accessing the raw Ethernet/WiFi data + * to and from a real network connection on the host PC. See the + * configNETWORK_INTERFACE_TO_USE definition above for information on how to + * configure the real network connection to use. */ +#define configMAC_ADDR0 0x00 +#define configMAC_ADDR1 0x11 +#define configMAC_ADDR2 0x22 +#define configMAC_ADDR3 0x33 +#define configMAC_ADDR4 0x44 +#define configMAC_ADDR5 0x21 + +/* Default IP address configuration. Used in ipconfigUSE_DHCP is set to 0, or + * ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configIP_ADDR0 192 +#define configIP_ADDR1 168 +#define configIP_ADDR2 0 +#define configIP_ADDR3 105 + +/* Default gateway IP address configuration. Used in ipconfigUSE_DHCP is set to + * 0, or ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configGATEWAY_ADDR0 192 +#define configGATEWAY_ADDR1 168 +#define configGATEWAY_ADDR2 0 +#define configGATEWAY_ADDR3 1 + +/* Default DNS server configuration. OpenDNS addresses are 208.67.222.222 and + * 208.67.220.220. Used in ipconfigUSE_DHCP is set to 0, or ipconfigUSE_DHCP is + * set to 1 but a DNS server cannot be contacted.*/ +#define configDNS_SERVER_ADDR0 208 +#define configDNS_SERVER_ADDR1 67 +#define configDNS_SERVER_ADDR2 222 +#define configDNS_SERVER_ADDR3 222 + +/* Default netmask configuration. Used in ipconfigUSE_DHCP is set to 0, or + * ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configNET_MASK0 255 +#define configNET_MASK1 255 +#define configNET_MASK2 255 +#define configNET_MASK3 0 + +/* The UDP port to which print messages are sent. */ +#define configPRINT_PORT ( 15000 ) + +#define configPROFILING ( 0 ) + +/* Pseudo random number generater used by some demo tasks. */ +extern uint32_t ulRand(); +#define configRAND32() ulRand() + +/* The platform that FreeRTOS is running on. */ +#define configPLATFORM_NAME "WinSim" + +#endif /* FREERTOS_CONFIG_H */ diff --git a/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSIPConfig.h b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSIPConfig.h new file mode 100644 index 000000000..13a2450b9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSIPConfig.h @@ -0,0 +1,305 @@ +/* +FreeRTOS Kernel V10.2.0 +Copyright (C) 2017 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 +*/ + + +/***************************************************************************** +* +* See the following URL for configuration information. +* http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_IP_Configuration.html +* +*****************************************************************************/ + +#ifndef FREERTOS_IP_CONFIG_H +#define FREERTOS_IP_CONFIG_H + +/* Set to 1 to print out debug messages. If ipconfigHAS_DEBUG_PRINTF is set to + * 1 then FreeRTOS_debug_printf should be defined to the function used to print + * out the debugging messages. */ +#define ipconfigHAS_DEBUG_PRINTF 0 +#if ( ipconfigHAS_DEBUG_PRINTF == 1 ) + #define FreeRTOS_debug_printf( X ) configPRINTF( X ) +#endif + +/* Set to 1 to print out non debugging messages, for example the output of the + * FreeRTOS_netstat() command, and ping replies. If ipconfigHAS_PRINTF is set to 1 + * then FreeRTOS_printf should be set to the function used to print out the + * messages. */ +#define FreeRTOS_printf( X ) + + +/* Define the byte order of the target MCU (the MCU FreeRTOS+TCP is executing + * on). Valid options are pdFREERTOS_BIG_ENDIAN and pdFREERTOS_LITTLE_ENDIAN. */ +#define ipconfigBYTE_ORDER pdFREERTOS_LITTLE_ENDIAN + +/* If the network card/driver includes checksum offloading (IP/TCP/UDP checksums) + * then set ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM to 1 to prevent the software + * stack repeating the checksum calculations. */ +#define ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM 1 + +/* Several API's will block until the result is known, or the action has been + * performed, for example FreeRTOS_send() and FreeRTOS_recv(). The timeouts can be + * set per socket, using setsockopt(). If not set, the times below will be + * used as defaults. */ +#define ipconfigSOCK_DEFAULT_RECEIVE_BLOCK_TIME ( 5000 ) +#define ipconfigSOCK_DEFAULT_SEND_BLOCK_TIME ( 5000 ) + +/* Include support for DNS caching. For TCP, having a small DNS cache is very + * useful. When a cache is present, ipconfigDNS_REQUEST_ATTEMPTS can be kept low + * and also DNS may use small timeouts. If a DNS reply comes in after the DNS + * socket has been destroyed, the result will be stored into the cache. The next + * call to FreeRTOS_gethostbyname() will return immediately, without even creating + * a socket. */ +#define ipconfigUSE_DNS_CACHE ( 1 ) +#define ipconfigDNS_REQUEST_ATTEMPTS ( 2 ) + +/* The IP stack executes it its own task (although any application task can make + * use of its services through the published sockets API). ipconfigUDP_TASK_PRIORITY + * sets the priority of the task that executes the IP stack. The priority is a + * standard FreeRTOS task priority so can take any value from 0 (the lowest + * priority) to (configMAX_PRIORITIES - 1) (the highest priority). + * configMAX_PRIORITIES is a standard FreeRTOS configuration parameter defined in + * FreeRTOSConfig.h, not FreeRTOSIPConfig.h. Consideration needs to be given as to + * the priority assigned to the task executing the IP stack relative to the + * priority assigned to tasks that use the IP stack. */ +#define ipconfigIP_TASK_PRIORITY ( configMAX_PRIORITIES - 2 ) + +/* The size, in words (not bytes), of the stack allocated to the FreeRTOS+TCP + * task. This setting is less important when the FreeRTOS Win32 simulator is used + * as the Win32 simulator only stores a fixed amount of information on the task + * stack. FreeRTOS includes optional stack overflow detection, see: + * http://www.freertos.org/Stacks-and-stack-overflow-checking.html. */ +#define ipconfigIP_TASK_STACK_SIZE_WORDS ( configMINIMAL_STACK_SIZE * 5 ) + +/* ipconfigRAND32() is called by the IP stack to generate random numbers for + * things such as a DHCP transaction number or initial sequence number. Random + * number generation is performed via this macro to allow applications to use their + * own random number generation method. For example, it might be possible to + * generate a random number by sampling noise on an analogue input. */ +extern uint32_t ulRand(); +#define ipconfigRAND32() ulRand() + +/* If ipconfigUSE_NETWORK_EVENT_HOOK is set to 1 then FreeRTOS+TCP will call the + * network event hook at the appropriate times. If ipconfigUSE_NETWORK_EVENT_HOOK + * is not set to 1 then the network event hook will never be called. See: + * http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_UDP/API/vApplicationIPNetworkEventHook.shtml. + */ +#define ipconfigUSE_NETWORK_EVENT_HOOK 1 + +/* Sockets have a send block time attribute. If FreeRTOS_sendto() is called but + * a network buffer cannot be obtained then the calling task is held in the Blocked + * state (so other tasks can continue to executed) until either a network buffer + * becomes available or the send block time expires. If the send block time expires + * then the send operation is aborted. The maximum allowable send block time is + * capped to the value set by ipconfigMAX_SEND_BLOCK_TIME_TICKS. Capping the + * maximum allowable send block time prevents prevents a deadlock occurring when + * all the network buffers are in use and the tasks that process (and subsequently + * free) the network buffers are themselves blocked waiting for a network buffer. + * ipconfigMAX_SEND_BLOCK_TIME_TICKS is specified in RTOS ticks. A time in + * milliseconds can be converted to a time in ticks by dividing the time in + * milliseconds by portTICK_PERIOD_MS. */ +#define ipconfigUDP_MAX_SEND_BLOCK_TIME_TICKS ( 5000U / portTICK_PERIOD_MS ) + +/* If ipconfigUSE_DHCP is 1 then FreeRTOS+TCP will attempt to retrieve an IP + * address, netmask, DNS server address and gateway address from a DHCP server. If + * ipconfigUSE_DHCP is 0 then FreeRTOS+TCP will use a static IP address. The + * stack will revert to using the static IP address even when ipconfigUSE_DHCP is + * set to 1 if a valid configuration cannot be obtained from a DHCP server for any + * reason. The static configuration used is that passed into the stack by the + * FreeRTOS_IPInit() function call. */ +#define ipconfigUSE_DHCP 1 +#define ipconfigDHCP_REGISTER_HOSTNAME 1 +#define ipconfigDHCP_USES_UNICAST 1 + +/* If ipconfigDHCP_USES_USER_HOOK is set to 1 then the application writer must + * provide an implementation of the DHCP callback function, + * xApplicationDHCPUserHook(). */ +#define ipconfigUSE_DHCP_HOOK 0 + +/* When ipconfigUSE_DHCP is set to 1, DHCP requests will be sent out at + * increasing time intervals until either a reply is received from a DHCP server + * and accepted, or the interval between transmissions reaches + * ipconfigMAXIMUM_DISCOVER_TX_PERIOD. The IP stack will revert to using the + * static IP address passed as a parameter to FreeRTOS_IPInit() if the + * re-transmission time interval reaches ipconfigMAXIMUM_DISCOVER_TX_PERIOD without + * a DHCP reply being received. */ +#define ipconfigMAXIMUM_DISCOVER_TX_PERIOD \ + ( 120000U / portTICK_PERIOD_MS ) + +/* The ARP cache is a table that maps IP addresses to MAC addresses. The IP + * stack can only send a UDP message to a remove IP address if it knowns the MAC + * address associated with the IP address, or the MAC address of the router used to + * contact the remote IP address. When a UDP message is received from a remote IP + * address the MAC address and IP address are added to the ARP cache. When a UDP + * message is sent to a remote IP address that does not already appear in the ARP + * cache then the UDP message is replaced by a ARP message that solicits the + * required MAC address information. ipconfigARP_CACHE_ENTRIES defines the maximum + * number of entries that can exist in the ARP table at any one time. */ +#define ipconfigARP_CACHE_ENTRIES 6 + +/* ARP requests that do not result in an ARP response will be re-transmitted a + * maximum of ipconfigMAX_ARP_RETRANSMISSIONS times before the ARP request is + * aborted. */ +#define ipconfigMAX_ARP_RETRANSMISSIONS ( 5 ) + +/* ipconfigMAX_ARP_AGE defines the maximum time between an entry in the ARP + * table being created or refreshed and the entry being removed because it is stale. + * New ARP requests are sent for ARP cache entries that are nearing their maximum + * age. ipconfigMAX_ARP_AGE is specified in tens of seconds, so a value of 150 is + * equal to 1500 seconds (or 25 minutes). */ +#define ipconfigMAX_ARP_AGE 150 + +/* Implementing FreeRTOS_inet_addr() necessitates the use of string handling + * routines, which are relatively large. To save code space the full + * FreeRTOS_inet_addr() implementation is made optional, and a smaller and faster + * alternative called FreeRTOS_inet_addr_quick() is provided. FreeRTOS_inet_addr() + * takes an IP in decimal dot format (for example, "192.168.0.1") as its parameter. + * FreeRTOS_inet_addr_quick() takes an IP address as four separate numerical octets + * (for example, 192, 168, 0, 1) as its parameters. If + * ipconfigINCLUDE_FULL_INET_ADDR is set to 1 then both FreeRTOS_inet_addr() and + * FreeRTOS_indet_addr_quick() are available. If ipconfigINCLUDE_FULL_INET_ADDR is + * not set to 1 then only FreeRTOS_indet_addr_quick() is available. */ +#define ipconfigINCLUDE_FULL_INET_ADDR 1 + +/* ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS defines the total number of network buffer that + * are available to the IP stack. The total number of network buffers is limited + * to ensure the total amount of RAM that can be consumed by the IP stack is capped + * to a pre-determinable value. */ +#define ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS 60 + +/* A FreeRTOS queue is used to send events from application tasks to the IP + * stack. ipconfigEVENT_QUEUE_LENGTH sets the maximum number of events that can + * be queued for processing at any one time. The event queue must be a minimum of + * 5 greater than the total number of network buffers. */ +#define ipconfigEVENT_QUEUE_LENGTH \ + ( ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS + 5 ) + +/* The address of a socket is the combination of its IP address and its port + * number. FreeRTOS_bind() is used to manually allocate a port number to a socket + * (to 'bind' the socket to a port), but manual binding is not normally necessary + * for client sockets (those sockets that initiate outgoing connections rather than + * wait for incoming connections on a known port number). If + * ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND is set to 1 then calling + * FreeRTOS_sendto() on a socket that has not yet been bound will result in the IP + * stack automatically binding the socket to a port number from the range + * socketAUTO_PORT_ALLOCATION_START_NUMBER to 0xffff. If + * ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND is set to 0 then calling FreeRTOS_sendto() + * on a socket that has not yet been bound will result in the send operation being + * aborted. */ +#define ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND 1 + +/* Defines the Time To Live (TTL) values used in outgoing UDP packets. */ +#define ipconfigUDP_TIME_TO_LIVE 128 +/* Also defined in FreeRTOSIPConfigDefaults.h. */ +#define ipconfigTCP_TIME_TO_LIVE 128 + +/* USE_TCP: Use TCP and all its features. */ +#define ipconfigUSE_TCP ( 1 ) + +/* USE_WIN: Let TCP use windowing mechanism. */ +#define ipconfigUSE_TCP_WIN ( 1 ) + +/* The MTU is the maximum number of bytes the payload of a network frame can + * contain. For normal Ethernet V2 frames the maximum MTU is 1500. Setting a + * lower value can save RAM, depending on the buffer management scheme used. If + * ipconfigCAN_FRAGMENT_OUTGOING_PACKETS is 1 then (ipconfigNETWORK_MTU - 28) must + * be divisible by 8. */ +#define ipconfigNETWORK_MTU 1200U + +/* Set ipconfigUSE_DNS to 1 to include a basic DNS client/resolver. DNS is used + * through the FreeRTOS_gethostbyname() API function. */ +#define ipconfigUSE_DNS 1 + +/* If ipconfigREPLY_TO_INCOMING_PINGS is set to 1 then the IP stack will + * generate replies to incoming ICMP echo (ping) requests. */ +#define ipconfigREPLY_TO_INCOMING_PINGS 1 + +/* If ipconfigSUPPORT_OUTGOING_PINGS is set to 1 then the + * FreeRTOS_SendPingRequest() API function is available. */ +#define ipconfigSUPPORT_OUTGOING_PINGS 0 + +/* If ipconfigSUPPORT_SELECT_FUNCTION is set to 1 then the FreeRTOS_select() + * (and associated) API function is available. */ +#define ipconfigSUPPORT_SELECT_FUNCTION 0 + +/* If ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES is set to 1 then Ethernet frames + * that are not in Ethernet II format will be dropped. This option is included for + * potential future IP stack developments. */ +#define ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES 1 + +/* If ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES is set to 1 then it is the + * responsibility of the Ethernet interface to filter out packets that are of no + * interest. If the Ethernet interface does not implement this functionality, then + * set ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES to 0 to have the IP stack + * perform the filtering instead (it is much less efficient for the stack to do it + * because the packet will already have been passed into the stack). If the + * Ethernet driver does all the necessary filtering in hardware then software + * filtering can be removed by using a value other than 1 or 0. */ +#define ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES 1 + +/* The windows simulator cannot really simulate MAC interrupts, and needs to + * block occasionally to allow other tasks to run. */ +#define configWINDOWS_MAC_INTERRUPT_SIMULATOR_DELAY ( 20 / portTICK_PERIOD_MS ) + +/* Advanced only: in order to access 32-bit fields in the IP packets with + * 32-bit memory instructions, all packets will be stored 32-bit-aligned, + * plus 16-bits. This has to do with the contents of the IP-packets: all + * 32-bit fields are 32-bit-aligned, plus 16-bit. */ +#define ipconfigPACKET_FILLER_SIZE 2U + +/* Define the size of the pool of TCP window descriptors. On the average, each + * TCP socket will use up to 2 x 6 descriptors, meaning that it can have 2 x 6 + * outstanding packets (for Rx and Tx). When using up to 10 TP sockets + * simultaneously, one could define TCP_WIN_SEG_COUNT as 120. */ +#define ipconfigTCP_WIN_SEG_COUNT 240 + +/* Each TCP socket has a circular buffers for Rx and Tx, which have a fixed + * maximum size. Define the size of Rx buffer for TCP sockets. */ +#define ipconfigTCP_RX_BUFFER_LENGTH ( 10000 ) + +/* Define the size of Tx buffer for TCP sockets. */ +#define ipconfigTCP_TX_BUFFER_LENGTH ( 10000 ) + +/* When using call-back handlers, the driver may check if the handler points to + * real program memory (RAM or flash) or just has a random non-zero value. */ +#define ipconfigIS_VALID_PROG_ADDRESS( x ) ( ( x ) != NULL ) + +/* Include support for TCP keep-alive messages. */ +#define ipconfigTCP_KEEP_ALIVE ( 1 ) +#define ipconfigTCP_KEEP_ALIVE_INTERVAL ( 20 ) /* Seconds. */ + +/* The socket semaphore is used to unblock the MQTT task. */ +#define ipconfigSOCKET_HAS_USER_SEMAPHORE ( 0 ) + +#define ipconfigSOCKET_HAS_USER_WAKE_CALLBACK ( 1 ) +#define ipconfigUSE_CALLBACKS ( 0 ) + + +#define portINLINE __inline + +void vApplicationMQTTGetKeys( const char ** ppcRootCA, + const char ** ppcClientCert, + const char ** ppcClientPrivateKey ); + +#endif /* FREERTOS_IP_CONFIG_H */ diff --git a/FreeRTOS-Plus/Test/CBMC/patches/Makefile b/FreeRTOS-Plus/Test/CBMC/patches/Makefile new file mode 100644 index 000000000..27888e63b --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/Makefile @@ -0,0 +1,24 @@ +BRANCH=freertos + +PATCHED=patched + +default: + git format-patch $(BRANCH)..$(BRANCH)-cbmc-patches + +patch: + if [ ! -f $(PATCHED) ]; then \ + for p in *.patch; do \ + (cd ../../..; patch -p1 < CBMC/patches/$${p}) \ + done; \ + cat > $(PATCHED) < /dev/null; \ + fi + +unpatch: + git checkout ../../../lib + $(RM) $(PATCHED) + +#patching file lib/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h +#patching file lib/include/private/list.h +#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DHCP.c +#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c +#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_TCP_WIN.c diff --git a/FreeRTOS-Plus/Test/CBMC/patches/README.md b/FreeRTOS-Plus/Test/CBMC/patches/README.md new file mode 100644 index 000000000..ec0e5d424 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/README.md @@ -0,0 +1,6 @@ +This directory includes patches to FreeRTOS required to run the CBMC proofs. + +The patches fall into three classes: +* First is a refactoring of prvCheckOptions +* Second is the removal of static attributes from some functions +* Third is two patches dealing with shortcomings of CBMC that should be removed soon.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/patches/__init__.py b/FreeRTOS-Plus/Test/CBMC/patches/__init__.py new file mode 100755 index 000000000..e69de29bb --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/__init__.py diff --git a/FreeRTOS-Plus/Test/CBMC/patches/compute_patch.py b/FreeRTOS-Plus/Test/CBMC/patches/compute_patch.py new file mode 100755 index 000000000..3e854177c --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/compute_patch.py @@ -0,0 +1,241 @@ +#!/usr/bin/env python3 +# +# Generation of patches for CBMC proofs. +# +# 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. + + +import json +import os +import re +import subprocess +import textwrap +import unittest + +from patches_constants import PATCHES_DIR +from patches_constants import HEADERS + + +DEFINE_REGEX_MAKEFILE = re.compile(r"(?:['\"])?([\w]+)") +DEFINE_REGEX_HEADER = re.compile(r"\s*#\s*define\s*([\w]+)") + +class DirtyGitError(Exception): + pass + +class PatchCreationError(Exception): + pass + +def prolog(): + return textwrap.dedent("""\ + This script generates patch files for the header files used + in the cbmc proof. These patches permit setting values of preprocessor + macros as part of the proof configuration. + """) + + +def find_all_defines(): + """Collects all define values in Makefile.json. + + Some of the Makefiles use # in the json to make comments. + As this is non standard json, we need to remove the comment + lines before parsing. Then we extract all defines from the file. + """ + defines = set() + + proof_dir = os.path.abspath(os.path.join(PATCHES_DIR, "..", "proofs")) + + for fldr, _, fyles in os.walk(proof_dir): + if "Makefile.json" in fyles: + file = os.path.join(fldr, "Makefile.json") + key = "DEF" + elif "MakefileCommon.json" in fyles: + file = os.path.join(fldr, "MakefileCommon.json") + key = "DEF " + else: + continue + with open(file, "r") as source: + content = "".join([line for line in source + if line and not line.strip().startswith("#")]) + makefile = json.loads(content) + if key in makefile.keys(): + """This regex parses the define declaration in Makefile.json + 'macro(x)=false' is an example for a declaration. + 'macro' is expected to be matched. + """ + for define in makefile[key]: + matched = DEFINE_REGEX_MAKEFILE.match(define) + if matched: + defines.add(matched.group(1)) + return defines + +def manipulate_headerfile(defines, header_file): + """Wraps all defines used in an ifndef.""" + + # This regex matches the actual define in the header file. + modified_content = "" + with open(header_file, "r") as source: + last = "" + for line in source: + match = DEFINE_REGEX_HEADER.match(line) + if (match and + match.group(1) in defines and + not last.lstrip().startswith("#ifndef")): + full_def = line + # this loop deals with multiline definitions + while line.rstrip().endswith("\\"): + line = next(source) + full_def += line + # indentation for multiline definitions can be improved + modified_content += textwrap.dedent("""\ + #ifndef {target} + {original}\ + #endif + """.format(target=match.group(1), original=full_def)) + else: + modified_content += line + last = line + with open(header_file, "w") as output: + output.write(modified_content) + + +def header_dirty(header_files): + """Check that the header_file is not previously modified.""" + + # Git does not update the modified file list returned by diff-files on + # apply -R (at least not on MacOS). + # Running git status updates git's internal state. + status = subprocess.run(["git", "status"], stdout=subprocess.DEVNULL, + stderr=subprocess.PIPE, universal_newlines=True) + + diff_state = subprocess.run(["git", "diff-files"], stdout=subprocess.PIPE, + stderr=subprocess.PIPE, universal_newlines=True) + + if status.returncode: + raise DirtyGitError(textwrap.dedent("""\ + Could not run git status. Exited: {} + stderr: {} + """.format(status.returncode, status.stderr))) + + if diff_state.returncode: + raise DirtyGitError(textwrap.dedent("""\ + Could not run git diff-files. Exited: {} + stderr: {} + """.format(diff_state.returncode, diff_state.stderr))) + + for header_file in header_files: + if os.path.basename(header_file) + "\n" in diff_state.stdout: + return True + return False + + +def create_patch(defines, header_file): + """Computes a patch enclosing defines used in CBMC proofs with #ifndef.""" + manipulate_headerfile(defines, header_file) + patch = subprocess.run(["git", "diff", header_file], + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, universal_newlines=True) + cleaned = subprocess.run(["git", "checkout", "--", header_file], + stdout=subprocess.DEVNULL, + stderr=subprocess.PIPE, universal_newlines=True) + + if patch.returncode: + raise PatchCreationError(textwrap.dedent("""\ + git diff exited with error code: {} + stderr: {} + """.format(patch.returncode, patch.stderr))) + + if cleaned.returncode: + raise DirtyGitError(textwrap.dedent("""\ + git checkout for cleaning files failed with error code: {} + on file {} + stderr: {} + """.format(cleaned.returncode, header_file, cleaned.stderr))) + + header_path_part = header_file.replace(os.sep, "_") + path_name = "auto_patch_" + header_path_part + ".patch" + path_name = os.path.join(PATCHES_DIR, path_name) + if patch.stdout: + with open(path_name, "w") as patch_file: + patch_file.write(patch.stdout) + + +def create_patches(headers): + defines = find_all_defines() + + if not header_dirty(headers): + for header in headers: + create_patch(defines, header) + else: + raise DirtyGitError(textwrap.dedent("""\ + It seems like one of the header files is in dirty state. + This script cannot patch files in dirty state. + """)) + +# Invoke 'python3 -m unittest compute_patch.py" for running tests. +class TestDefineRegexes(unittest.TestCase): + def test_makefile_regex(self): + input1 = "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}" + input2 = "ipconfigETHERNET_MINIMUM_PACKET_BYTES=50" + input3 = "'configASSERT(X)=__CPROVER_assert(x, \"must hold\")'" + input4 = '"configASSERT (X)=__CPROVER_assert(x, "must hold")"' + input5 = "configASSERT(X)=__CPROVER_assert(x,\"must hold\")" + + match1 = DEFINE_REGEX_MAKEFILE.match(input1) + match2 = DEFINE_REGEX_MAKEFILE.match(input2) + match3 = DEFINE_REGEX_MAKEFILE.match(input3) + match4 = DEFINE_REGEX_MAKEFILE.match(input4) + match5 = DEFINE_REGEX_MAKEFILE.match(input5) + + self.assertIsNotNone(match1) + self.assertIsNotNone(match2) + self.assertIsNotNone(match3) + self.assertIsNotNone(match4) + self.assertIsNotNone(match5) + + self.assertEqual(match1.group(1), + "ipconfigETHERNET_MINIMUM_PACKET_BYTES") + self.assertEqual(match2.group(1), + "ipconfigETHERNET_MINIMUM_PACKET_BYTES") + self.assertEqual(match3.group(1), "configASSERT") + self.assertEqual(match4.group(1), "configASSERT") + self.assertEqual(match5.group(1), "configASSERT") + + + def test_header_regex(self): + input1 = ("#define configASSERT( x ) if( ( x ) == 0 )" + + "vAssertCalled( __FILE__, __LINE__ )") + input2 = "#define ipconfigMAX_ARP_RETRANSMISSIONS ( 5 )" + input3 = "#define ipconfigINCLUDE_FULL_INET_ADDR 1" + + match1 = DEFINE_REGEX_HEADER.match(input1) + match2 = DEFINE_REGEX_HEADER.match(input2) + match3 = DEFINE_REGEX_HEADER.match(input3) + + self.assertIsNotNone(match1) + self.assertIsNotNone(match2) + self.assertIsNotNone(match3) + + self.assertEqual(match1.group(1), "configASSERT") + self.assertEqual(match2.group(1), "ipconfigMAX_ARP_RETRANSMISSIONS") + self.assertEqual(match3.group(1), "ipconfigINCLUDE_FULL_INET_ADDR") + +if __name__ == '__main__': + create_patches(HEADERS) diff --git a/FreeRTOS-Plus/Test/CBMC/patches/patch.py b/FreeRTOS-Plus/Test/CBMC/patches/patch.py new file mode 100755 index 000000000..c2c0883a3 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/patch.py @@ -0,0 +1,36 @@ +#!/usr/bin/env python3 + +import logging +import os +import subprocess +import sys +from glob import glob + +from patches_constants import PATCHES_DIR + +def patch(): + if os.path.isfile("patched"): + sys.exit() + + applied_patches = [] + failed_patches = [] + for tmpfile in glob(os.path.join(PATCHES_DIR, "*.patch")): + print("patch", tmpfile) + result = subprocess.run(["git", "apply", "--ignore-space-change", "--ignore-whitespace", tmpfile], + cwd=os.path.join("..", "..", "..", "..")) + if result.returncode: + failed_patches.append(tmpfile) + logging.error("patching failed: %s", tmpfile) + else: + applied_patches.append(tmpfile) + + with open(os.path.join(PATCHES_DIR, "patched"), "w") as outp: + print("Success:", file=outp) + print("\n".join(map(lambda x: "\t" + x, applied_patches)), file=outp) + + print("Failure:", file=outp) + print("\n".join(map(lambda x: "\t" + x, failed_patches)), file=outp) + + +if __name__ == "__main__": + patch() diff --git a/FreeRTOS-Plus/Test/CBMC/patches/patches_constants.py b/FreeRTOS-Plus/Test/CBMC/patches/patches_constants.py new file mode 100755 index 000000000..1093e6538 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/patches_constants.py @@ -0,0 +1,42 @@ +#!/usr/bin/env python3 +# +# Constants for the generation of patches for CBMC proofs. +# +# 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. + +import os + +PATCHES_DIR = os.path.dirname(os.path.abspath(__file__)) + + +shared_prefix = [ + "." +] +shared_prefix_port = [ + "..", "..", "..", "..", "FreeRTOS", "Source", "portable", "MSVC-MingW" +] + +absolute_prefix = os.path.abspath(os.path.join(PATCHES_DIR, *shared_prefix)) +absolute_prefix_port = os.path.abspath(os.path.join(PATCHES_DIR, *shared_prefix_port)) + +HEADERS = [os.path.join(absolute_prefix, "FreeRTOSConfig.h"), + os.path.join(absolute_prefix, "FreeRTOSIPConfig.h"), + os.path.join(absolute_prefix_port, "portmacro.h")] diff --git a/FreeRTOS-Plus/Test/CBMC/patches/unpatch.py b/FreeRTOS-Plus/Test/CBMC/patches/unpatch.py new file mode 100755 index 000000000..2162971fd --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/patches/unpatch.py @@ -0,0 +1,42 @@ +#!/usr/bin/env python3 +# +# unpatching changes for the CBMC proofs. +# +# 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. + +import subprocess +import os +import sys +from glob import glob + +from patches_constants import PATCHES_DIR + +try: + os.remove(os.path.join(PATCHES_DIR, "patched")) +except FileNotFoundError: + print("Nothing to do here.") + sys.exit(0) +for tmpfile in glob(os.path.join(PATCHES_DIR, "*.patch")): + print("unpatch", tmpfile) + result = subprocess.run(["git", "apply", "-R", "--ignore-space-change", "--ignore-whitespace", tmpfile], + cwd=os.path.join("..", "..", "..", "..")) + if result.returncode: + print("Unpatching failed: {}".format(tmpfile)) |