diff options
| author | lundinc <lundinc@1d2547de-c912-0410-9cb9-b8ca96c0e9e2> | 2020-08-12 19:11:51 +0000 |
|---|---|---|
| committer | lundinc <lundinc@1d2547de-c912-0410-9cb9-b8ca96c0e9e2> | 2020-08-12 19:11:51 +0000 |
| commit | 42255af1e27a3157d541f0812eaca447c569ca49 (patch) | |
| tree | 5c8702c2f0dc1cb9be1a4d5ff285897d96b97dd2 /FreeRTOS-Plus/Test/CBMC/proofs | |
| parent | f5221dff43de249079c2da081723cb7a456f981f (diff) | |
| download | freertos-master.tar.gz | |
Author: Ming Yue <mingyue86010@gmail.com>
Date: Tue Aug 11 17:06:59 2020 -0700
Remove unused wolfSSL files. (#197)
* Remove unused wolfSSL files.
* Add back some removed ciphers.
* Update VS project file.
commit 0e0edd96e8236b2ea4a6e6018812807be828c77f
Author: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Date: Tue Aug 11 10:50:30 2020 -0700
Use new QEMU test project to improve stream/message buffer tests (#168)
* Add Eclipse/GCC project that targets the LM3S8962 QEMU model.
* Get the Cortex-M QEMU project working.
* Continue working on making stream buffer demo more robust and QEMU project.
* Rename directory CORTEX_LM3S8986_QEMU to CORTEX_LM3S6965_QEMU.
Work on making the Stream Buffer tests more robust.
Check in before adding in the trace recorder.
* Rename CORTEX_LM3S6969_QEMU to CORTEX_LM3S6969_GCC_QEMU.
* Make the StreamBufferDemo.c common demo file (test file) more robust to other test tasks running at an equally high priority.
* Work in progress checkin only - comments in main.c are incorrect.
* Correct comments at the top of FreeRTOS/Demo/CORTEX_LM3S6965_GCC_QEMU/main.c
Make the message buffer tests more robust in the case the a message buffer becomes full when prvSenderTask() has a higher priority than the reader task.
* Disable trace recorder in the LM3S6965 QEMU demo.
* I'm dropping FreeRTOS-Kernel reference update, since this seems to break the CMBC CI.
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit 157a7fc39f19583ac8481e93fa3e1c91b1e1860c
Author: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
Date: Sun Aug 9 22:21:44 2020 -0700
Use chacheable RAM in IAR project for MPU_M7_NUCLEO_H743ZI2 project (#193)
This change updates the IAR project for Nucleo H743ZI2 to use the
cacheable DTC RAM and enables L1 cache. In order to ensure the correct
functioning of cache, the project sets configTEX_S_C_B_SRAM in
FreeRTOSConfig.h to not mark the RAM as shareable.
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
commit f3e43556f90f01b82918ad533b0c616489331919
Author: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
Date: Sun Aug 9 16:23:53 2020 -0700
Add MPU demo projects for NUCLEO-H743ZI2 board (#155)
* Add MPU demo projects for NUCLEO-H743ZI2 board
It contains projects for Keil uVision, STM32CubeIDE and IAR EW. This
demo shows the use of newly added support for 16 MPU regions.
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
* Delete not needed CMSIS files
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
commit 94aa31c3cbae7c929b8a412768b74631f4a6b461
Author: TakayukiMatsuo <62984531+TakayukiMatsuo@users.noreply.github.com>
Date: Sat Aug 8 07:58:14 2020 +0900
Update wolfSSL to the latest version(v.4.4.0) (#186)
* deleted old version wolfSSL before updating
* updated wolfSSL to the latest version(v4.4.0)
* updated wolfSSL to the latest version(v4.4.0)
* added macros for timing resistance
Co-authored-by: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Co-authored-by: Ming Yue <mingyue86010@gmail.com>
commit 68518f5866aac58793c737d9a46dd07a6a816aaf
Author: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Date: Fri Aug 7 14:59:24 2020 -0700
Removed a 16MByte flash image file that was checked in by mistake (several years ago). (#173)
Remove the copies of lwIP that are no longer reference from demo projects.
Co-authored-by: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
commit d4bf09480a2c77b1a25cce35b32293be61ab586f
Author: m17336 <45935231+m17336@users.noreply.github.com>
Date: Thu Aug 6 22:37:08 2020 +0300
Update previous AVR ATmega0 and AVR Dx projecs + addition of equivalent projects in MPLAB.X and IAR (#180)
* Updated indentation in AVR_ATMega4809_Atmel_Studio and AVR_Dx_Atmel_Studio projects, plus small fixes in their readme files.
* Added AVR_ATMega4809_IAR, AVR_ATMega4809_MPLAB.X, AVR_Dx_IAR and AVR_Dx_MPLAB.X demo projects.
* Removed build artefacts and added .gitignore files in AVR_ATMega4809_MPLAB.X and AVR_Dx_MPLAB.X projects.
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit f32a0647c8228ddd066f5d69a85b2e49086e4c95
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Mon Aug 3 16:45:10 2020 -0700
Remove CBMC patch which is not used anymore (#187)
* Delete 0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch
* Delete 0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch
commit 08af68ef9049279b265c3d00e9c48fb9594129a8
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Sat Aug 1 16:38:23 2020 -0700
Remove dependency of CBMC on Patches (#181)
* Changes to DHCP
* CBMC DNS changes
* Changes for TCP_IP
* Changes to TCP_WIN
* Define away static to nothing
* Remove patches
* Changes after Mark's comments v1
* Update MakefileCommon.json
* Correction!
commit a7fec906a415363338449447daf10d7517b78848
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 29 17:39:36 2020 -0700
Misc changes (#183)
commit 07cf5e07e4a05d6775a2f9e753269f43f82cf6ba
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 29 16:15:38 2020 -0700
MISRA compliance changes for FreeRTOS+TCP headers (#165)
* misra changes
* Update FreeRTOS_IP_Private.h
* Update FreeRTOS_IP_Private.h
commit e903ac0fed7ce59916899e404f3e5ae5b08d1478
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 29 16:03:14 2020 -0700
UPD MISRA changes (#164)
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit 97551bf44e7dc7dc1e4484a8fd30f699255e8569
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 29 15:52:00 2020 -0700
MISRA changes in FreeRTOS_TCP_WIN.c (#162)
commit f2611cc5e5999c4c87e040a8c2d2e6b5e77a16a6
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 29 15:38:37 2020 -0700
MISRA compliance changes in FreeRTOS_Sockets{.c/.h} (#161)
* MISRA changes Sockets
* add other changes
* Update FreeRTOSIPConfig.h
* Update FreeRTOSIPConfig.h
* Update FreeRTOSIPConfig.h
* Update FreeRTOSIPConfig.h
* correction
* Add 'U'
* Update FreeRTOS_Sockets.h
* Update FreeRTOS_Sockets.h
* Update FreeRTOS_Sockets.c
* Update FreeRTOS_Sockets.h
* Update after Gary's comments
* Correction reverted
commit ae4d4d38d9b2685bae159b4c87619cdb157c0bf7
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 29 13:56:57 2020 -0700
MISRA compliance changes for FreeRTOS_TCP_IP.c (#160)
* MISRA tcp-ip changes
* Changes after Hein's comments on original PR
* Update FreeRTOS_TCP_IP.c
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit a457f43c66eb0f4be9d8f8678c0e3fb8d7ebd57b
Author: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
Date: Tue Jul 28 13:01:38 2020 -0700
Add missing error state assignment. (#166)
commit 915af50524e15a78ceb6c62b3d33f6562621ee46
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Mon Jul 27 17:30:53 2020 -0700
Add Atmel Studio projects for ATMega4809 and AVR128DA48 (#159)
* Added explicit cast to allow roll over and avoid integer promotion during cycles counters comparison in recmutex.c.
* Fixed type mismatch between declaration and definition of function xAreSemaphoreTasksStillRunning( void ).
* Added Atmel Studio demo projects for ATMega4809 and AVR128DA48.
* Per https://www.freertos.org/upgrading-to-FreeRTOS-V8.html, I'm updating portBASE_TYPE to BaseType_t.
Signed-off-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
* Update register test for ATmega4809
- to cover r28, r29, r31.
- call public API taskYIELD() instead of portYIELD().
* Update ATmega4809 readme.md to include info for serial port setup, and minor wording fix.
Co-authored-by: Alexandru Niculae - M17336 <alexandru.niculae@microchip.com>
commit 4a7a48790d64127f85cc763721b575c51c452833
Author: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
Date: Thu Jul 23 10:22:33 2020 -0700
Add Uncrustify file used for Kernel. (#163)
commit e0d62163b08769fd74f020709c398f994088ca96
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 22 18:06:23 2020 -0700
Sync with +TCP amazon-FreeRTOS (#158)
* DNS.c commit
* IP.c commit
* Add various source & header files
commit 8e36bee30eef2107e128edb58e83ee46e8241a91
Author: Nathan Chong <52972368+nchong-at-aws@users.noreply.github.com>
Date: Tue Jul 21 12:51:20 2020 -0400
Prove buffer lemmas (#124)
* Prove buffer lemmas
* Update queue proofs to latest kernel source
All changes were syntactic due to uncrustify code-formatting
* Strengthen prvCopyDataToQueue proof
* Add extract script for diff comparison
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit c720c18ada40b502436ea811e8d03dca919726d8
Author: Hein Tibosch <hein_tibosch@yahoo.es>
Date: Tue Jul 14 05:35:44 2020 +0800
FreeRTOS+TCP Adding the combined driver for SAM4E and SAME70 v2 (#78)
* Adding a combined +TCP driver for SAM4E and SAME70
* Changes after review from Aniruddha
Co-authored-by: Hein Tibosch <hein@htibosch.net>
Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
commit 4237049b12d9bb6b03694fecf6ea26a353e637c8
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Mon Jul 13 12:07:56 2020 -0700
Add changes from 2225-2227 amazon-FreeRTOS (#134)
commit 7caa32863458c4470d3c620945c30824199f524c
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Jul 10 23:32:30 2020 -0700
Add Full TCP test suite - not using secure sockets (#131)
* Add Full-TCP suite
* delete unnecessary files
* Change after Joshua's comments
commit d7667a0034841f2968f9f9f805030cc608bfbce1
Author: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
Date: Fri Jul 3 15:45:44 2020 -0700
Remove unnecessary semicolon from the linker file (#121)
This was creating problem with the onboard LPCLink debug probe.
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
commit 529c481c39506d0b331bfd0cdea35e5d1aeaaad0
Author: Nathan Chong <52972368+nchong-at-aws@users.noreply.github.com>
Date: Thu Jul 2 15:55:20 2020 -0400
Add VeriFast kernel queue proofs (#117)
commit d5fedeaa96b5b1d3c0f6b9b52a8064ab72ff2821
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 1 13:56:27 2020 -0700
Add checks in FreeRTOS_Socket.c (#104)
* Add fail-safes to FreeRTOS_Socket.c
* Use all 'pd' errors
* Correction after Hein's comments
* Correction after Hein's comments v2
* Changes after Hein's comments
* Update after Gary's comments
commit a9b2aac4e9fda2a259380156df9cc0af51384d2d
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Jun 26 12:09:36 2020 -0700
Folder structure change + Fix broken Projects (#103)
* Update folder structure
* Correct project files
* Move test folder
* Some changes after Yuki's comments
commit 98bfc38bf3404414878dc68ea41753bea4e24c8e
Author: Hein Tibosch <hein_tibosch@yahoo.es>
Date: Thu Jun 25 13:01:45 2020 +0800
FreeRTOS+TCP : add memory statistics and dump packets, v3 (#83)
* FreeRTOS+TCP : add memory statistics and dump packets, v3
* Two changes as requested by Aniruddha
Co-authored-by: Hein Tibosch <hein@htibosch.net>
Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
commit 072a173c9df31c75ff64bde440f3f316cedb9033
Author: S.Burch <8697966+wholl0p@users.noreply.github.com>
Date: Mon Jun 22 23:39:26 2020 +0200
Fixed Imports for Infineon XMC1100 Board (#88)
Co-authored-by: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
commit 2df5eeef5763045c4c74ff0e2a4091b7d19bea89
Author: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Date: Mon Jun 8 14:22:46 2020 -0700
Feature/multiple direct to task notifications (#73)
* Add TaskNotifyArray.c with the single task tests updated to use the task notification array up to the point where the timer is created.
* Continue working on TaskNotifyArray.c to test the new task notification indexes. Next TaskNotifyArray.c will be refactored to break the tests up a bit.
* Refactor and update the comments in TaskNotifyArray.c - no functional changes.
* Change from the task notify "array" to task notification "indexed" nomenclature in the new task notification API functions that work on one particular task notification with the array of task notifications.
* Update the implementation of the taskNOTIFY_TAKE() and taskNOTIFY_WAIT() trace macros to take the array index of the task notification they are acting on.
Rename configNUMBER_OF_TASK_NOTIFICATIONS to configTASK_NOTIFICATION_ARRAY_ENTRIES.
Add FreeRTOS/Demo/Common/Minimal/TaskNotifyArray.c to the Visual Studio project - the file implements tests specific to the behaviour of the indexed task notification functions and should be used in addition to the tests already provided in FreeRTOS/Demo/Common/Minimal/TaskNotify.c.
commit b9e4ecfaf7286d8493d4a96a93fbb325534ad97b
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Jun 5 11:10:58 2020 -0700
Remove Empty and Un-referenced folder from Demo (#86)
commit f11bcc8acc57a23fb03603762e758c25b9d0efb7
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jun 3 16:52:31 2020 -0700
Fix a Bug and corresponding CBMC patch (#84)
* Update remove-static-in-freertos-tcp-ip.patch
* Update FreeRTOS_TCP_IP.c
* Update remove-static-in-freertos-tcp-ip.patch
* Update remove-static-in-freertos-tcp-ip.patch
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit bb9f92f771e5f6ea2b9b09c7e89130a75e562eb7
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Wed Jun 3 10:46:55 2020 -0700
Submodule FreeRTOS/Source 10bbbcf0b..6199b72fb (#82)
commit 6efc39f44be5b269168836e95aebbdb8ae77dce3
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Tue Jun 2 15:09:25 2020 -0700
Add Project for running integration tests v2 (#80)
* Project for integration tests
* relative paths in project files
* relative paths in project files-1
* relative paths in project files-2
* addressed comments
* addressed comments v2
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit 0eb5909fb02bac9dc074ff1bc2fe338d77f73764
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Thu May 28 17:05:24 2020 -0700
readme.md for ATmega328PB Xplained Mini. (#76)
readme.md to get users jump started.
commit cb7edd2323a77f3dbea144c1f48f95582becc99e
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Thu May 28 10:11:58 2020 -0700
Sync with a:FR (#75)
* AFR sync
* AFR sync: CBMC
* AFR sync: CBMC: remove .bak files
* AFR sync: CBMC: more cleanup
* Corrected CBMC proofs
* Corrected CBMC patches
* Corrected CBMC patches-1
* Corrected CBMC patches-2
* remove .bak files (3)
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit 6557291e5407ca7ec6beca53fced1aaa620c5c02
Author: alfred gedeon <alfred2g@hotmail.com>
Date: Wed May 27 14:44:33 2020 -0700
Test: Add Linux Networking support with demo application (#71)
* Test: Add Linux Networking support with demo application
* Test: revert files affected by uncrustify
* Test: revert files affected by uncrustify
Co-authored-by: Alfred Gedeon <gedeonag@amazon.com>
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit 8b079bc394e7b205d72210ce9e052404d782938f
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Wed May 27 10:44:03 2020 -0700
ATmega328PB Xplained Mini -- demo project for ATmega port. (#70)
* Bootstrap a demo from START. No driver is added in this commit.
* Add FreeRTOS source code to project. Remove unnecessary folder nesting.
Heap_4 is used here.
* Copy over main.c, FreeRTOSConfig.h, and regtest.{c, h}.
This commit compiles, but will need some work on timer used.
* This port has 2KB RAM. We are using 1KB for heap.
Further decreasing minimum stack size, and also use stack overflow check 1 to save some stack space.
* Preserve EEPROM set to false.
* End of the line.
* Reduce register test stack size.
32 8-bit register + 10 bytes for stack frame cost. Round up to 50.
* Adding Queue test in Integer test.
- g3 to easy debugging.
- mainCHECK_PERIOD is set to 1000 ticks. Note that this port for now use WDT as tick timer, and period is set to 15ms.
- vErrorChecks, is of highest priority. So if this task gets run before other tasks, the very first check will fail.
* Avoid false alarm.
Since we don't know in which order the tasks are scheduled, clearing any error for the first entry of vErrorChecks.
Signed-off-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
* ParTest.c to init, set, toggle onboard user LED at PB5.
* Added a task to blink onboard user LED.
Need a magic number for stack size.
Signed-off-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
* Explicitly setting timing slicing to 0.
This is to avoid unecessary context switch when multiple tasks are of the same priority.
Signed-off-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
* Add taskYIELD() at the end of the loop in each register test task.
This is to give other tasks of the same priority a chance to run, regardless of scheduling algorithm.
Signed-off-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
* minor, update comment in main.c.
commit 95a3a02f95749fb7a600723076e291f9dee7426c
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri May 22 16:26:59 2020 -0700
FreeRTOS-Plus: Unit testing Infrastructure and examples (#72)
* Added CMock as submodule
* Makefile added
* Removed TEMP from Makefile
* Added configuration files and header files
* Update Makefile
* Test runner working
* make clean
* Example added with README
* Update README.md
* Restored +TCP files
* Cleared +TCP changes
* removed comments from Makefile
* Update README.md
* Update README.md
* Update README.md
* Updated Test/Unit-test/readme.md
commit 5003d17feda25490e655c0f1c15d2b13e395c9f7
Author: Hein Tibosch <hein_tibosch@yahoo.es>
Date: Wed May 6 14:16:56 2020 -0400
FreeRTOS+TCP : renewing DHCP lease while network is down (#53)
Co-authored-by: Hein Tibosch <hein@htibosch.net>
Co-authored-by: Gary Wicker <14828980+gkwicker@users.noreply.github.com>
commit d95624c5d6ba95ec0474867d7165de2c28ed41b7
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Tue May 5 09:57:18 2020 -0700
Move CBMC proofs to FreeRTOS+ directory (#64)
* move CBMC proofs to FreeRTOS+ directory
* Failing proofs corrected
* ParseDNSReply proof added back
* removed queue_init.h from -Plus/Test
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit 95ae7c65758a9473ea16ab08182f056f72331de2
Author: markrtuttle <tuttle@acm.org>
Date: Wed Apr 29 04:27:45 2020 +0000
Change cbmc-viewer invocation in CBMC makefile (#63)
* Exclude FreeRTOS/Demo from CBMC proof reports.
The script cbmc-viewer generates the CBMC proof reports. The script
searches source files for symbol definitions and annotates source
files with coverage information. This patch causes cbmc-viewer to
ignore the directory FreeRTOS/Demo containing 348M of data. The
script now terminates in a few seconds.
* Make report default target for CBMC Makefile.
Modify the Makefile for CBMC proofs to generate the report by default
(and not just property checking) and modify property checking to
ignore failures (due to property assertions failing) and terminating
report generation.
Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>
commit d421ccc89f6f6473dfdd566a00567b0e1fd4cfc3
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Sat Apr 25 16:57:35 2020 -0700
Reword readme.md under ./Test. (#61)
commit 38412865985235b90dbd9da9708b68c4de5918f5
Author: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
Date: Sat Apr 25 16:56:54 2020 -0700
Removed a:FR reference. (#60)
commit 4db195c916c7b13c82ab3a34a499fe606f266810
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Tue Apr 21 15:40:08 2020 -0700
Adding FreeRTOS+TCP CBMC proofs to FreeRTOS/FreeRTOS (#56)
ParseDNSReply is to be added in the next PR.
commit 40a31b6d35a866a3a6c551d95bf08dae855da5bd
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Mon Apr 13 13:58:33 2020 -0700
'uL' -> 'UL'
commit 5b3a289b69fc92089aa8bd4d1b44ab816f326f73
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Mon Apr 13 13:50:53 2020 -0700
Changes after Gary's comments
commit edf68637dd22470a8d4f59fecc15b51379bcfeda
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Apr 10 16:26:03 2020 -0700
Update FreeRTOS_ARP.c
commit 35f3ac32a8899dd714a8a48952a4224fbcebc4aa
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Apr 10 15:56:18 2020 -0700
correct debug output
commit 5e12a70db4b6a8e68a434489683306f040252efa
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Apr 10 15:44:45 2020 -0700
Debugging flag check added
commit 4e8ac8de25ac4088b9c789b88a77cd39df4d9167
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Thu Apr 9 16:57:19 2020 -0700
Comment style consistency and Yuhui's suggestions
commit e43f7cd086096ad60491fedba69927a1e1a82f20
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Thu Apr 9 16:47:41 2020 -0700
Cleanup
commit ab3b51c7a0d880a6bf453ec63ae604e15050f310
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Thu Apr 9 16:33:03 2020 -0700
Update after Gary's comments
commit 97f7009699ffb972c0745dfdb526d1fa4e0faf84
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Apr 8 14:30:15 2020 -0700
Update after richard's comments
commit a9fcafc074cec559dd67961ef44273df6180c2db
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Apr 8 14:07:39 2020 -0700
Corrected the formatting
- visual studio had messed up the formatting
commit c381861014a8043ce30723fc5a8cf5107719c8df
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Apr 8 13:01:12 2020 -0700
commit 2 after gary's comments
commit 75677a8d85fa802cca9058d6e23796d5043a0982
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Apr 8 12:51:10 2020 -0700
Commit after Gary's comments
commit 666c0da366030109db2c0c5e7253cebb2f899db7
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Apr 8 10:56:01 2020 -0700
Update after Yuhui's comments
- removed (void) from before memcpy, memset etc.
- corrected memcpy style as suggested by Yuhui
- Added logging for xNetworkInterfaceOutput. No need to configASSERT
commit 4a1148d15b6b8169d2412f8179f734683b179795
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Apr 1 16:05:36 2020 -0700
Coverity + MISRA compliance
Modified code to conform to the MISRA directives more closely.
commit fa74f7dccf6b1a356993c6a894f8e1173b8c8157
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Thu Apr 2 20:26:10 2020 -0700
Removing writes to read-only PLIC interrupt pending registers.
Signed-off-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit 5b9777e11e16609648fb98d2f9a47553ab238950
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Mar 31 10:45:23 2020 -0700
A readme file to introduce what ./Test directory is about.
commit 211bb4cbd9ae6dfa95e8d8501f37d272bde5ab26
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Mar 24 15:14:24 2020 -0700
Ignore whitespace when working with patches.
commit 8156f64d1c45dd59ef12279f19a99f03e79e1f8a
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Feb 25 18:04:23 2020 -0800
Copying CBMC proofs from aws/amazon-freertos repo ./tools/cbmc to this repo ./FreeRTOS/Test/CBMC as is.
The commit ID in aws/amazon-freertos is 0c8e0217f2a43bdeb364b58ae01c6c259e03ef1b.
commit 9f316c246baafa15c542a5aea81a94f26e3d6507
Author: David Vrabel <david.vrabel@cambridgeconsultants.com>
Date: Mon Mar 16 11:21:46 2020 +0000
Demo/Posix_GCC: add demo application for Posix port using GCC
This is largely a copy of the Windows demo application with a few key
changes:
- heap_3 (use malloc()/free()) so tools like valgrind "just work".
- printf() wrapped in a mutex to prevent deadlocks on the internal
pthread mutexes inside printf().
SCons (https://scons.org/) is used as the build system.
This will be built as a 64-bit application, but note that the memory
allocation trace points only record the lower 32-bits of the address.
commit f78f919b3e2f0d707531a301a8ca07cd02bc4778
Author: Markus Rinne <markus.ka.rinne@gmail.com>
Date: Thu Mar 19 21:00:24 2020 +0200
Fix function comments
commit 1cd2d38d960a3576addb224582c88489bade5141
Author: David Chalco <david@chalco.io>
Date: Fri Mar 20 10:29:05 2020 -0700
unix separators for path and remove .exe suffix from risc compiler (works on windows/mac)
commit 938b19419eded12817737ab0644e94ed2ba7e95d
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Thu Mar 19 18:23:09 2020 -0700
Removing ./FreeRTOS-Labs directory, since:
- IoT libraries are now in LTS branch.
- FAT/POSIX/Light-weight MQTT are in https://github.com/FreeRTOS/FreeRTOS-Labs.
commit 1a4abbc9e91b13fd6394464ade59d5e048320c7c
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Mar 17 19:30:02 2020 -0700
Maintenance -- clean up readme.txt and add url to GitHub. (#38)
* Removing readme.txt, as now we have README.md in place.
The only information missing from README.md is about FAQ.
* Adding FAQ information in README.md.
* Adding a .url to root to redict user to FreeRTOS github home page.
commit 47bb466aa19395b7785bcb830e2e4dd35f6bafc5
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Mar 17 13:07:44 2020 -0700
Update issue templates
Template maintenance.
- adding title prefix.
- adding examples to "additional context" section.
commit f506290041f56867765f8efa70ed2862125bdb7c
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Mar 17 10:15:07 2020 -0700
Create SECURITY.md
Apply the recommended SECURITY.md from AWS to our repo.
commit 8982a2f80a80a2a0a47cf82de07b52101bd9d606
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Fri Mar 13 12:50:10 2020 -0700
Add ./lib directory to make sure Zynq project compiles.
commit ecf0f12aa14ad6fdafe1ef37257cbb4e03e2abd5
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Mar 11 10:19:48 2020 -0700
Sync up with Amazon-freertos repo (10th March 2020) (#34)
* Sync up with amazon-freertos
* Sync up with amazon-freertos
* Sync up with amazon-freertos
commit 0acffef047973e2e61c2201fd69cd9bbd317f674
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Mar 10 10:20:48 2020 -0700
GitHub PR template. (#29)
commit c40a6da2e4cb8042b56d1b174051cbbe9813781a
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Mon Mar 9 11:18:48 2020 -0700
pass payload length when calling UDP callback (#30)
* pass payload length when calling UDP callback
commit 12d580e93d4d9074b9a867632f0681a511b4ad12
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Fri Mar 6 18:16:51 2020 -0800
Update issue templates
Initial issue template. Created following https://help.github.com/en/github/building-a-strong-community/configuring-issue-templates-for-your-repository#configuring-the-template-chooser.
If change is needed, we could go another round.
commit 9debffb5e0e42ff716f58b2270b3af09652294af
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Fri Mar 6 17:27:46 2020 -0800
Update README.md to remove dead link.
See the conversation https://github.com/FreeRTOS/FreeRTOS/commit/42c627b2b88cb3b487fea983d8b566a8bbae54fa#comments .
Linkage for both ```./FreeRTOS/Source``` and ```./FreeRTOS/Demo``` are removed, since it looks weird to only provide linkage to Demo.
commit 7e1a4bf563240501fc45167aee9d929c533939dd
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Mar 6 15:18:09 2020 -0800
Fix DHCP option Client-identifier (#28)
commit 42c627b2b88cb3b487fea983d8b566a8bbae54fa
Author: Yuhui.Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Fri Mar 6 09:15:11 2020 -0800
Update readme and revert relative URL. (#27)
* Reordering: bumping cloning instruction up.
* Rewording readme.md to be clear kernel code is a submodule of this repository.
* Reverting relative URL, since user cannot click through on GitHub page.
(With URL, user could still download the correct version of the code. Reverting simply due to UI issue.)
commit 5751ae9b60e248ebd0b4dd7c58df54364d2bb9d5
Author: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
Date: Fri Mar 6 09:11:42 2020 -0800
Update CORTEX_MPU_M33F_NXP_LPC55S69_MCUXpresso project (#26)
This commit updates the project for LPC55S69 so that it works with the
latest version of MCUXpresso and SDK.
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
commit a9ffffe1f01f45f79e127c15727784984077932f
Author: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
Date: Thu Mar 5 17:16:13 2020 -0800
Using Relative URL For Submoduling. (#24)
commit 52c82076b38fe73d1dc46c97abf74ae9b803696c
Author: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
Date: Thu Mar 5 09:16:31 2020 -0800
use relative path to point to bundled toolchain instead (#25)
commit b877e4ec478de2c24d07ab46241070d7c66f375c
Author: lundinc2 <53273776+lundinc2@users.noreply.github.com>
Date: Tue Feb 25 13:18:38 2020 -0800
Moved vulnerability reporting and code of conduct to top of CONTRIBUTING.md (#20)
commit bef165d46799fb8faa58aaa224f80c16b6538e69
Author: Yuhui.Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Feb 18 22:06:38 2020 -0800
Linking test source file from relative path. (#19)
commit 89e7bbe292afd3912d1f0b2402cc506878bad869
Author: Yuhui.Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Feb 18 17:47:55 2020 -0800
A preliminary .gitignore file, to prevent us checking in files unnecessary. (#18)
https://github.com/github/gitignore.
commit c2a98127acb48c4562233230e66ca5c282688579
Author: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Date: Sun Feb 16 13:19:53 2020 -0800
Minor wording changes in the 'previous releases' section of the readme.me file. (#17)
commit 24c772d1439e5c291c0a29fce0a46996ca8afaa9
Author: Yuhui.Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Fri Feb 14 12:47:01 2020 -0800
Submodule kernel directory. (#16)
* Removing FreeRTOS/Source in readiness for submoduling.
* Submoduling kernel.
* README.md update due to submoduling.
When releasing, please follow these steps:
1. in local directory, clean directory and check "git status" shows "nothing to commit, working tree clean" for ALL subdirectories.
2. copy source code and instructions only to an empty folder. Git related should not be in this folder -- this covers .git, .gitignore, .github, .gitmodules, gitmessages, ......
3. zip the folder from step 2. (create both .zip and .7z)
4. attach .zip and .7z to the release. (e.g. attach these two in new release -- https://github.com/FreeRTOS/FreeRTOS/releases/new)
5. PLEASE download both, unzip, diff with your local git repo. (should not see any difference other than git related.) And, sanity check a couple of projects.
commit c3f8b91652392dc55e0d7067b90a40de5f5f0837
Author: Rashed Talukder <9218468+rashedtalukder@users.noreply.github.com>
Date: Thu Feb 13 17:47:14 2020 -0800
Update readme. Fixed typos and cli commands (#14)
commit 4723b825f2989213c1cdb2ebf4d6793e0292e363
Author: Julian Poidevin <julian-poidevin@users.noreply.github.com>
Date: Fri Feb 14 02:43:36 2020 +0100
Fixed wrong git clone SSH command (#13)
Replaced bad https URL with proper SSH URL
commit fc819b821715c42602819e58499846147a6394f5
Author: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Date: Thu Feb 13 17:42:22 2020 -0800
Correct the xTimerCreate() documentation which said NULL was returned if the timer period was passed into the function as 0, whereas that is not the case. (#15)
Add a note to the documentation for both the xTimerCreate() and xTimerCreateStatic() functions that the timer period must be greater than 0.
commit 1c711ab530b5f0dbd811d7d62e0a3763706ffff4
Author: Rashed Talukder <9218468+rashedtalukder@users.noreply.github.com>
Date: Wed Feb 12 23:00:18 2020 -0800
Updated contributions guidelines (#12)
commit 84fcc0d5317d96c6b086034093c8c1c83e050819
Author: Cobus van Eeden <35851496+cobusve@users.noreply.github.com>
Date: Wed Feb 12 15:05:06 2020 -0800
Updates to Markdown files and readme.txt (#11)
git-svn-id: http://svn.code.sf.net/p/freertos/code/trunk@2826 1d2547de-c912-0410-9cb9-b8ca96c0e9e2
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/proofs')
106 files changed, 5046 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/.gitignore b/FreeRTOS-Plus/Test/CBMC/proofs/.gitignore new file mode 100644 index 000000000..3498c4b3b --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/.gitignore @@ -0,0 +1,10 @@ +# These files are generated by make_type_header_files.py +*_datastructure.h + +Makefile +Makefile.common +cbmc-batch.yaml +**/*.txt +**/*.goto + +!CMakeLists.txt diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c new file mode 100644 index 000000000..523783564 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c @@ -0,0 +1,22 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "list.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +//We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. +//This is the mock to mimic the correct expected bahvior. If this allocation fails, this might invalidate the proof. +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + NetworkBufferDescriptor_t *pxNetworkBuffer = (NetworkBufferDescriptor_t *) malloc(sizeof(NetworkBufferDescriptor_t)); + pxNetworkBuffer->pucEthernetBuffer = malloc(xRequestedSizeBytes); + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + return pxNetworkBuffer; +} + +void harness() +{ + vARPAgeCache(); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json new file mode 100644 index 000000000..83c351d70 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json @@ -0,0 +1,18 @@ +{ + "ENTRY": "ARPAgeCache", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPAgeCache.0:7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/README.md new file mode 100644 index 000000000..3352f8096 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/README.md @@ -0,0 +1,2 @@ +Assuming that xNetworkInterfaceOutput is memory safe, +this harness proves the memory safety of the vARPAgeCache function. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c new file mode 100644 index 000000000..3ec9500cc --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c @@ -0,0 +1,28 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + /* + * The assumption made here is that the buffer pointed by pucEthernerBuffer + * is at least allocated to sizeof(ARPPacket_t) size but eventually a even larger buffer. + * This is not checked inside vARPGenerateRequestPacket. + */ + uint8_t ucBUFFER_SIZE; + __CPROVER_assume( ucBUFFER_SIZE >= sizeof(ARPPacket_t) && ucBUFFER_SIZE < 2 * sizeof(ARPPacket_t) ); + void *xBuffer = malloc(ucBUFFER_SIZE); + + NetworkBufferDescriptor_t xNetworkBuffer2; + xNetworkBuffer2.pucEthernetBuffer = xBuffer; + xNetworkBuffer2.xDataLength = ucBUFFER_SIZE; + + /* vARPGenerateRequestPacket asserts buffer has room for a packet */ + __CPROVER_assume( xNetworkBuffer2.xDataLength >= sizeof(ARPPacket_t) ); + vARPGenerateRequestPacket( &xNetworkBuffer2 ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json new file mode 100644 index 000000000..65c352489 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json @@ -0,0 +1,15 @@ +{ + "ENTRY": "ARPGenerateRequestPacket", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md new file mode 100644 index 000000000..f8fdcc97d --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md @@ -0,0 +1,3 @@ +Given that the pointer target of xNetworkDescriptor.pucEthernetBuffer is allocated +to the size claimed in xNetworkDescriptor.xDataLength, +this harness proves the memory safety of ARPGenerateRequestPacket.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c new file mode 100644 index 000000000..bf188efa1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c @@ -0,0 +1,17 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + + +void harness() +{ + uint32_t ulIPAddress; + MACAddress_t xMACAddress; + + eARPGetCacheEntry( &ulIPAddress, &xMACAddress ); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json new file mode 100644 index 000000000..ecc95a87f --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json @@ -0,0 +1,41 @@ +{ + "ENTRY": "ARPGetCacheEntry", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvCacheLookup.0:7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + { + "ARPGetCacheEntry_default":[ + "ipconfigARP_STORES_REMOTE_ADDRESSES=0", + "ipconfigUSE_LLMNR=0" + ] + }, + { + "ARPGetCacheEntry_LLMNR": [ + "ipconfigARP_STORES_REMOTE_ADDRESSES=0", + "ipconfigUSE_LLMNR=1" + ] + }, + { + "ARPGetCacheEntry_STORE_REMOTE": [ + "ipconfigARP_STORES_REMOTE_ADDRESSES=1", + "ipconfigUSE_LLMNR=0" + ] + }, + { + "ARPGetCacheEntry_REMOTE_LLMNR": [ + "ipconfigARP_STORES_REMOTE_ADDRESSES=1", + "ipconfigUSE_LLMNR=1" + ] + } + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md new file mode 100644 index 000000000..03e987ebd --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md @@ -0,0 +1,4 @@ +The combined proofs in the subdirectories prove that ARPGetCacheEntry +is memory safe for all possible combinations of ipconfigARP_STORES_REMOTE_ADDRESSES +and ipconfigUSE_LLMNR. These are the only configuration +parameters used inside the ARPGetCacheEntry. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c new file mode 100644 index 000000000..442b1df6b --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c @@ -0,0 +1,14 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +void harness(){ + MACAddress_t xMACAddress; + uint32_t ulIPAddress; + eARPGetCacheEntryByMac( &xMACAddress, &ulIPAddress ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json new file mode 100644 index 000000000..0f589a8e2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json @@ -0,0 +1,17 @@ +{ + "ENTRY": "ARPGetCacheEntryByMac", + "CBMCFLAGS": + [ + "--unwind 7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + "ipconfigUSE_ARP_REVERSED_LOOKUP=1", "ipconfigARP_CACHE_ENTRIES=6" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md new file mode 100644 index 000000000..77c17e2e9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md @@ -0,0 +1,4 @@ +ARPGetCacheEntryByMac is memory safe, +if it is enabled. + +ARPGetCacheEntryByMac does not use multiple configurations internally. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c new file mode 100644 index 000000000..f2d8e61ae --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c @@ -0,0 +1,15 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + ARPPacket_t xARPFrame; + + eARPProcessPacket( &xARPFrame ); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json new file mode 100644 index 000000000..48d5d83c9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json @@ -0,0 +1,19 @@ +{ + "ENTRY": "ARPProcessPacket", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]}, + {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]} + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md new file mode 100644 index 000000000..0197851b1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md @@ -0,0 +1,4 @@ +The proofs in the subdirectories show that +ARPProcessPacket is memory safe independent +of the configuration value of +ipconfigARP_USE_CLASH_DETECTION.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c new file mode 100644 index 000000000..6664d3cd0 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c @@ -0,0 +1,15 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + MACAddress_t xMACAddress; + uint32_t ulIPAddress; + vARPRefreshCacheEntry( &xMACAddress, ulIPAddress ); + vARPRefreshCacheEntry( NULL, ulIPAddress ); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json new file mode 100644 index 000000000..6cde60a51 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json @@ -0,0 +1,19 @@ +{ + "ENTRY": "ARPRefreshCacheEntry", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + {"NOT_STORE_REMOTE":["ipconfigARP_STORES_REMOTE_ADDRESSES=0"]}, + {"STORE_REMOTE":["ipconfigARP_STORES_REMOTE_ADDRESSES=1"]} + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md new file mode 100644 index 000000000..0f84300cf --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md @@ -0,0 +1,4 @@ +The proofs in this directory guarantee together that +ARPRefreshCacheEntry is memory safe independent +of the configuration value of +ipconfigARP_STORES_REMOTE_ADDRESSES. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c new file mode 100644 index 000000000..fd02b10a2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c @@ -0,0 +1,13 @@ +// /* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_ARP.h" + + +void harness() +{ + vARPSendGratuitous(); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json new file mode 100644 index 000000000..1f9616ef8 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json @@ -0,0 +1,18 @@ +{ + "ENTRY": "ARPSendGratuitous", + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md new file mode 100644 index 000000000..5bb155221 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md @@ -0,0 +1,6 @@ +Abstracting xQueueGenericSend away +and including tasks.c and FreeRTOS_IP.c: +The ARPSendGratutious function is memory safe, +if xQueueGenericSend is memory safe. + +queue.c is not compiled into the proof binary.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c new file mode 100644 index 000000000..957720133 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c @@ -0,0 +1,13 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + FreeRTOS_ClearARP(); +} + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json new file mode 100644 index 000000000..332106c4e --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json @@ -0,0 +1,15 @@ +{ + "ENTRY": "ClearARP", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md new file mode 100644 index 000000000..2447722c9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md @@ -0,0 +1,2 @@ +This proof demonstrates the memory safety of the ClearARP function in the FreeRTOS_ARP.c file. +No restrictions are made.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json new file mode 100644 index 000000000..13792bb68 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json @@ -0,0 +1,57 @@ +# +# 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": "OutputARPRequest", + "CBMCFLAGS": + [ + "--unwind 20" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + #That is the minimal required size for an ARPPacket_t plus offset in the buffer. + "MINIMUM_PACKET_BYTES": 50, + "DEF": + [ + { + "CBMC_PROOF_ASSUMPTION_HOLDS_Packet_bytes": [ + "CBMC_PROOF_ASSUMPTION_HOLDS=1", + "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}" + ] + }, + { + "CBMC_PROOF_ASSUMPTION_HOLDS_no_packet_bytes": ["CBMC_PROOF_ASSUMPTION_HOLDS=1"] + }, + { + "CBMC_PROOF_ASSUMPTION_DOES_NOT_HOLD": ["CBMC_PROOF_ASSUMPTION_HOLDS=0"] + } + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c new file mode 100644 index 000000000..472f6b1e1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c @@ -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 + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + + +ARPPacket_t xARPPacket; +NetworkBufferDescriptor_t xNetworkBuffer; + +/* STUB! + * We assume that the pxGetNetworkBufferWithDescriptor function is + * implemented correctly and returns a valid data structure. + * This is the mock to mimic the expected behavior. + * If this allocation fails, this might invalidate the proof. + * FreeRTOS_OutputARPRequest calls pxGetNetworkBufferWithDescriptor + * to get a NetworkBufferDescriptor. Then it calls vARPGenerateRequestPacket + * passing this buffer along in the function call. vARPGenerateRequestPacket + * casts the pointer xNetworkBuffer.pucEthernetBuffer into an ARPPacket_t pointer + * and writes a complete ARPPacket to it. Therefore the buffer has to be at least of the size + * of an ARPPacket to gurantee memory safety. + */ +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + #ifdef CBMC_PROOF_ASSUMPTION_HOLDS + #ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES + xNetworkBuffer.pucEthernetBuffer = malloc(ipconfigETHERNET_MINIMUM_PACKET_BYTES); + #else + xNetworkBuffer.pucEthernetBuffer = malloc(xRequestedSizeBytes); + #endif + #else + uint32_t malloc_size; + __CPROVER_assert(!__CPROVER_overflow_mult(2, xRequestedSizeBytes)); + __CPROVER_assume(malloc_size > 0 && malloc_size < 2 * xRequestedSizeBytes); + xNetworkBuffer.pucEthernetBuffer = malloc(malloc_size); + #endif + xNetworkBuffer.xDataLength = xRequestedSizeBytes; + return &xNetworkBuffer; +} + + +void harness() +{ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md new file mode 100644 index 000000000..8a868dda1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md @@ -0,0 +1,29 @@ +This is the memory safety proof for FreeRTOS_OutputARPRequest. + +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: + +* xNetworkInterfaceOutput + +This proof checks FreeRTOS_OutputARPRequest in multiple configuration: + +* The config_CBMC_PROOF_ASSUMPTION_HOLDS_no_packet_bytes proof + guarantees that for a buffer allocated to xDataLength, + the code executed by the FreeRTOS_OutputARPRequest function + call of FreeRTOS_ARP.c is memory safe. +* If the ipconfigETHERNET_MINIMUM_PACKET_BYTES is set and the + buffer allocated by pxGetNetworkBufferWithDescriptor allocates + a buffer of at least ipconfigETHERNET_MINIMUM_PACKET_BYTES, + the config_CBMC_PROOF_ASSUMPTION_HOLDS_Packet_bytes proof + guarantees that the code executed by the + FreeRTOS_OutputARPRequest function call + of FreeRTOS_ARP.c is memory safe. +* The third configuration in the subdirectory + config_CBMC_PROOF_ASSUMPTION_DOES_NOT_HOLD demonstrates + that the code is not memory safe, if the allocation + code violates our assumption. +* All proofs mock the pxGetNetworkBufferWithDescriptor + function for modelling the assumptions about the + buffer management layer. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c new file mode 100644 index 000000000..4975d66ee --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c @@ -0,0 +1,14 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOSIPConfig.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + FreeRTOS_PrintARPCache(); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json new file mode 100644 index 000000000..6588b10d9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json @@ -0,0 +1,17 @@ +{ + "ENTRY": "FreeRTOS_PrintARPCache", + "CBMCFLAGS": + [ + "--unwind 7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + "ipconfigARP_CACHE_ENTRIES=6" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md new file mode 100644 index 000000000..2c44908cd --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md @@ -0,0 +1,4 @@ +FreeRTOS_PrintARPCache_harness.c is memory safe, +assuming vLoggingPrintf is correct and memory safe. + +FreeRTOS_PrintARPCache does not use multiple configurations. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json new file mode 100644 index 000000000..ed1a2aca8 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json @@ -0,0 +1,47 @@ +{ + "ENTRY": "OutputARPRequest", + "MINIMUM_PACKET_BYTES": 50, + "CBMCFLAGS": + [ + "--unwind {MINIMUM_PACKET_BYTES}", + "--unwindset xNetworkBuffersInitialise.0:3,xNetworkBuffersInitialise.1:3,vListInsert.0:3,pxGetNetworkBufferWithDescriptor.0:3,pxGetNetworkBufferWithDescriptor.1:3,vNetworkInterfaceAllocateRAMToBuffers.0:3" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement/BufferAllocation_1.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Source/queue.goto" + ], + "DEF": + [ + { + "minimal_configuration": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=0" + ] + }, + { + "minimal_configuration_minimal_packet_size": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}" + ] + }, + { + "minimal_configuration_linked_rx_messages": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=1" + ] + } + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c new file mode 100644 index 000000000..3dae34a34 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c @@ -0,0 +1,71 @@ +/* This harness is linked against + * libraries/freertos_plus/standard/freertos_plus_tcp/source/portable/BufferManagement/BufferAllocation_1.goto + */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#if( ipconfigUSE_LLMNR == 1 ) + #include "FreeRTOS_DNS.h" +#endif /* ipconfigUSE_LLMNR */ +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" + +void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] ){ + for(int x = 0; x < ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS; x++){ + NetworkBufferDescriptor_t *current = &pxNetworkBuffers[x]; + #ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES + current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t) + (ipconfigETHERNET_MINIMUM_PACKET_BYTES- sizeof(ARPPacket_t))); + #else + current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t)); + #endif + current->xDataLength = sizeof(ARPPacket_t); + } +} + +/* The code expects that the Semaphore creation relying on pvPortMalloc + is successful. This is checked by an assert statement, that gets + triggered when the allocation fails. Nevertheless, the code is perfectly + guarded against a failing Semaphore allocation. To make the assert pass, + it is assumed for now, that pvPortMalloc doesn't fail. Using a model allowing + failures of the allocation might be possible + after removing the assert in l.105 of BufferAllocation_1.c, from a memory + safety point of view. */ +void *pvPortMalloc( size_t xWantedSize ){ + return malloc(xWantedSize); +} + +/* + * This function is implemented by a third party. + * After looking through a couple of samples in the demos folder, it seems + * like the only shared contract is that you want to add the if statement + * for releasing the buffer to the end. Apart from that, it is up to the vendor, + * how to write this code out to the network. + */ +BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor, BaseType_t bReleaseAfterSend ){ + if( bReleaseAfterSend != pdFALSE ) + { + vReleaseNetworkBufferAndDescriptor( pxDescriptor ); + } +} + +void harness() +{ + BaseType_t xRes = xNetworkBuffersInitialise(); + if(xRes == pdPASS){ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md new file mode 100644 index 000000000..ea5eac78d --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md @@ -0,0 +1,27 @@ +This is the memory safety proof for ```FreeRTOS_OutputARPRequest``` +method combined with the BufferAllocation_1.c allocation strategy. + +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 +* vAssertCalled +* xTaskGetSchedulerState +* pvTaskIncrementMutexHeldCount +* xTaskRemoveFromEventList +* xTaskPriorityDisinherit + +This proof checks ```FreeRTOS_OutputARPRequest``` in multiple configurations. +All assume the memory safety of vNetworkInterfaceAllocateRAMToBuffers. +* The ```config_minimal_configuration``` proof sets + ```ipconfigUSE_LINKED_RX_MESSAGES=0```. +* The ```config_minimal_configuration_linked_rx_messages``` proof sets + ```ipconfigUSE_LINKED_RX_MESSAGES=1```. +* The ```minimal_configuration_minimal_packet_size``` proof sets + ```ipconfigETHERNET_MINIMUM_PACKET_BYTES``` to 50. + +All harnesses include the queue.c file, but test only for the happy path. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json new file mode 100644 index 000000000..fb5dd4be2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json @@ -0,0 +1,48 @@ +{ + "ENTRY": "OutputARPRequest", + "MINIMUM_PACKET_BYTES": 50, + "CBMCFLAGS": + [ + "--unwind {MINIMUM_PACKET_BYTES}", + "--unwindset xNetworkBuffersInitialise.0:3,xNetworkBuffersInitialise.1:3,vListInsert.0:3,pxGetNetworkBufferWithDescriptor.0:3,pxGetNetworkBufferWithDescriptor.1:3,vNetworkInterfaceAllocateRAMToBuffers.0:3" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement/BufferAllocation_2.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Source/queue.goto" + ], + "DEF": + [ + { + "minimal_configuration": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=0" + ] + }, + { + "minimal_configuration_minimal_packet_size": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}", + "ipconfigUSE_TCP=1" + ] + }, + { + "minimal_configuration_linked_rx_messages": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=1" + ] + } + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c new file mode 100644 index 000000000..c047a2760 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c @@ -0,0 +1,54 @@ +/* This harness is linked against + * libraries/freertos_plus/standard/freertos_plus_tcp/source/portable/BufferManagement/BufferAllocation_2.goto + */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#if( ipconfigUSE_LLMNR == 1 ) + #include "FreeRTOS_DNS.h" +#endif /* ipconfigUSE_LLMNR */ +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" + +void *pvPortMalloc( size_t xWantedSize ){ + return malloc(xWantedSize); +} + + +void vPortFree( void *pv ){ + free(pv); +} + +/* + * This function function writes a buffer to the network. We stub it + * out here, and assume it has no side effects relevant to memory safety. + */ +BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor, BaseType_t bReleaseAfterSend ){ + if( bReleaseAfterSend != pdFALSE ) + { + vReleaseNetworkBufferAndDescriptor( pxDescriptor ); + } +} + +void harness() +{ + BaseType_t xRes = xNetworkBuffersInitialise(); + if(xRes == pdPASS){ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); + } +} + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md new file mode 100644 index 000000000..5d509a7e8 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md @@ -0,0 +1,49 @@ +This is the memory safety proof for FreeRTOS_OutputARPRequest +method combined with the BufferAllocation_2.c allocation strategy. + +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 +* vAssertCalled +* xTaskGetSchedulerState +* pvTaskIncrementMutexHeldCount +* xTaskRemoveFromEventList +* xTaskPriorityDisinherit + +* pvPortMalloc +* pvPortFree +* xNetworkInterfaceOutput +* vNetworkInterfaceAllocateRAMToBuffers + +This proof disables the tracing library in the header. + +This proof checks FreeRTOS_OutputARPRequest in multiple configuration: + +* The proof in the directory config_minimal_configuration guarantees + that the implementation and interaction between + FreeRTOS_OutputARPRequest and + FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c + are memory save. This proof depends entirely of the implementation + correctness of vNetworkInterfaceAllocateRAMToBuffers. +* The proof in directory minimal_configuration_minimal_packet_size + guarantees that using + FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c + along with the ipconfigETHERNET_MINIMUM_PACKET_BYTES is memory save + as long as TCP is enabled ( ipconfigUSE_TCP 1 ) and + ipconfigETHERNET_MINIMUM_PACKET_BYTES < sizeof( TCPPacket_t ). +* The directory minimal_configuration_minimal_packet_size_no_tcp + reminds that ipconfigETHERNET_MINIMUM_PACKET_BYTES must not be used + if TCP is disabled ( ipconfigUSE_TCP 1 ) along with the + FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c + allocator. +* The proof in directory + config_minimal_configuration_linked_rx_messages guarantees that the + ipconfigUSE_LINKED_RX_MESSAGES define does not interfere with the + memory safety claim. + +All harnesses include the queue.c file, but test only for the happy path. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.c b/FreeRTOS-Plus/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.c new file mode 100644 index 000000000..3fe245f80 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.c @@ -0,0 +1,47 @@ +#include "FreeRTOS.h" +#include "task.h" +#include "tasksStubs.h" + +#ifndef TASK_STUB_COUNTER + #define TASK_STUB_COUNTER 0; +#endif + +/* 5 is a magic number, but we need some number here as a default value. + This value is used to bound any loop depending on xTaskCheckForTimeOut + as a loop bound. It should be overwritten in the Makefile.json adapting + to the performance requirements of the harness. */ +#ifndef TASK_STUB_COUNTER_LIMIT + #define TASK_STUB_COUNTER_LIMIT 5; +#endif + + +static BaseType_t xCounter = TASK_STUB_COUNTER; +static BaseType_t xCounterLimit = TASK_STUB_COUNTER_LIMIT; + +BaseType_t xTaskGetSchedulerState( void ) +{ + return xState; +} + +/* This function is another method apart from overwritting the defines to init the max + loop bound. */ +void vInitTaskCheckForTimeOut(BaseType_t maxCounter, BaseType_t maxCounter_limit) +{ + xCounter = maxCounter; + xCounterLimit = maxCounter_limit; +} + +/* This is mostly called in a loop. For CBMC, we have to bound the loop + to a max limits of calls. Therefore this Stub models a nondet timeout in + max TASK_STUB_COUNTER_LIMIT iterations.*/ +BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait ) { + ++xCounter; + if(xCounter == xCounterLimit) + { + return pdTRUE; + } + else + { + return nondet_basetype(); + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CMakeLists.txt b/FreeRTOS-Plus/Test/CBMC/proofs/CMakeLists.txt new file mode 100644 index 000000000..aaa2e3c8a --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CMakeLists.txt @@ -0,0 +1,40 @@ +list(APPEND cbmc_compile_options + -m32 +) + +list(APPEND cbmc_compile_definitions + CBMC + WINVER=0x400 + _CONSOLE + _CRT_SECURE_NO_WARNINGS + _DEBUG + _WIN32_WINNT=0x0500 + __PRETTY_FUNCTION__=__FUNCTION__ + __free_rtos__ +) + +list(APPEND cbmc_compile_includes + ${CMAKE_SOURCE_DIR}/Source/include + ${CMAKE_SOURCE_DIR}/Source/portable/MSVC-MingW + ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement + ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include + ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/Compiler/MSVC + ${cbmc_dir}/include + ${cbmc_dir}/windows +) + +# Remove --flag for a specific proof with list(REMOVE_ITEM cbmc_flags --flag) +list(APPEND cbmc_flags + --32 + --bounds-check + --pointer-check + --div-by-zero-check + --float-overflow-check + --nan-check + --nondet-static + --pointer-overflow-check + --signed-overflow-check + --undefined-shift-check + --unsigned-overflow-check +) + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c new file mode 100644 index 000000000..fd0900c5e --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c @@ -0,0 +1,100 @@ +/* Standard includes. */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" +#include "FreeRTOS_ARP.h" + +#include "cbmc.h" + +/**************************************************************** + * Signature of function under test + ****************************************************************/ + +void prvCheckOptions( FreeRTOS_Socket_t * pxSocket, + const NetworkBufferDescriptor_t * pxNetworkBuffer ); + +/**************************************************************** + * Declare the buffer size external to the harness so it can be + * accessed by the preconditions of prvSingleStepTCPHeaderOptions, and + * give the buffer size an unconstrained value in the harness itself. + ****************************************************************/ +size_t buffer_size; + +/**************************************************************** + * Function contract proved correct by CheckOptionsOuter + ****************************************************************/ + +size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr, + size_t uxTotalLength, + FreeRTOS_Socket_t * const pxSocket, + BaseType_t xHasSYNFlag ) +{ + /* CBMC model of pointers limits the size of the buffer */ + + /* Preconditions */ + __CPROVER_assert( buffer_size < CBMC_MAX_OBJECT_SIZE, + "prvSingleStepTCPHeaderOptions: buffer_size < CBMC_MAX_OBJECT_SIZE" ); + __CPROVER_assert( 8 <= buffer_size, + "prvSingleStepTCPHeaderOptions: 8 <= buffer_size" ); + __CPROVER_assert( pucPtr != NULL, + "prvSingleStepTCPHeaderOptions: pucPtr != NULL" ); + __CPROVER_assert( uxTotalLength <= buffer_size, + "prvSingleStepTCPHeaderOptions: uxTotalLength <= buffer_size" ); + __CPROVER_assert( pxSocket != NULL, + "prvSingleStepTCPHeaderOptions: pxSocket != NULL" ); + + /* Postconditions */ + size_t index; + __CPROVER_assume( index == 1 || index <= uxTotalLength ); + + return index; +} + +/**************************************************************** + * Proof of CheckOptions + ****************************************************************/ + +void harness() +{ + /* Give buffer_size an unconstrained value */ + size_t buf_size; + + buffer_size = buf_size; + + /* pxSocket can be any socket */ + FreeRTOS_Socket_t pxSocket; + + /* pxNetworkBuffer can be any buffer descriptor with any buffer */ + NetworkBufferDescriptor_t pxNetworkBuffer; + pxNetworkBuffer.pucEthernetBuffer = malloc( buffer_size ); + pxNetworkBuffer.xDataLength = buffer_size; + + /**************************************************************** + * Specification and proof of CheckOptions + ****************************************************************/ + + /* CBMC model of pointers limits the size of the buffer */ + __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); + + /* Bound required to bound iteration over the buffer */ + __CPROVER_assume( buffer_size <= BUFFER_SIZE ); + + /* Buffer must be big enough to hold pxTCPPacket and pxTCPHeader */ + __CPROVER_assume( buffer_size > 47 ); + + prvCheckOptions( &pxSocket, &pxNetworkBuffer ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/Makefile.json new file mode 100644 index 000000000..b6f82621a --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/Makefile.json @@ -0,0 +1,18 @@ +{ + "ENTRY": "CheckOptions", + "CBMCFLAGS": "--unwind 1 --unwindset prvCheckOptions.0:41", + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Stream_Buffer.goto", + "$(FREERTOS)/Source/tasks.goto", + "$(FREERTOS)/Source/list.goto" + ], + "BUFFER_SIZE": 100, + "DEF": + [ + "BUFFER_SIZE={BUFFER_SIZE}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c new file mode 100644 index 000000000..bca2b1792 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c @@ -0,0 +1,94 @@ +/* Standard includes. */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" +#include "FreeRTOS_ARP.h" + +#include "cbmc.h" + +/**************************************************************** + * Signature of function under test + ****************************************************************/ + +void prvReadSackOption( const uint8_t * const pucPtr, + size_t uxIndex, + FreeRTOS_Socket_t * const pxSocket ); + +/**************************************************************** + * Proof of prvReadSackOption function contract + ****************************************************************/ + +void harness() +{ + /* pucPtr points into a buffer */ + size_t buffer_size; + uint8_t * pucPtr = malloc( buffer_size ); + + /* uxIndex in an index into the buffer */ + size_t uxIndex; + + /* pxSocket can be any socket with some initialized values */ + FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); + + pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) ); + + vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xWaitQueue ); + + if( nondet_bool() ) + { + TCPSegment_t * segment = malloc( sizeof( TCPSegment_t ) ); + listSET_LIST_ITEM_OWNER( &segment->xQueueItem, ( void * ) segment ); + vListInsertEnd( &pxSocket->u.xTCP.xTCPWindow.xWaitQueue, &segment->xQueueItem ); + } + + vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xTxSegments ); + + if( nondet_bool() ) + { + TCPSegment_t * segment = malloc( sizeof( TCPSegment_t ) ); + vListInitialiseItem( &segment->xSegmentItem ); + listSET_LIST_ITEM_OWNER( &segment->xQueueItem, ( void * ) segment ); + vListInsertEnd( &pxSocket->u.xTCP.xTCPWindow.xTxSegments, &segment->xQueueItem ); + } + + vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xPriorityQueue ); + + extern List_t xSegmentList; + vListInitialise( &xSegmentList ); + + /**************************************************************** + * Specification and proof of CheckOptions inner loop + ****************************************************************/ + + /* Preconditions */ + + /* CBMC model of pointers limits the size of the buffer */ + __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); + + /* Both preconditions are required to avoid integer overflow in the */ + /* pointer offset of the pointer pucPtr + uxIndex + 8 */ + __CPROVER_assume( uxIndex <= buffer_size ); + __CPROVER_assume( uxIndex + 8 <= buffer_size ); + + /* Assuming quite a bit more about the initialization of pxSocket */ + __CPROVER_assume( pucPtr != NULL ); + __CPROVER_assume( pxSocket != NULL ); + + prvReadSackOption( pucPtr, uxIndex, pxSocket ); + + /* No postconditions required */ +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/Makefile.json new file mode 100644 index 000000000..8730e4f99 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/Makefile.json @@ -0,0 +1,19 @@ +{ + "ENTRY": "CheckOptionsInner", + "CBMCFLAGS": [ + "--unwind 1", + "--unwindset prvTCPWindowTxCheckAck.1:2,prvTCPWindowFastRetransmit.2:2" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Stream_Buffer.goto", + "$(FREERTOS)/Source/tasks.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c new file mode 100644 index 000000000..b8833fc79 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c @@ -0,0 +1,100 @@ +/* Standard includes. */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" +#include "FreeRTOS_ARP.h" + +#include "cbmc.h" + +/**************************************************************** + * Signature of the function under test + ****************************************************************/ + +size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr, + size_t uxTotalLength, + FreeRTOS_Socket_t * const pxSocket, + BaseType_t xHasSYNFlag ); + +/**************************************************************** + * Declare the buffer size external to the harness so it can be + * accessed by the preconditions of prvReadSackOption, and give the + * buffer size an unconstrained value in the harness itself. + ****************************************************************/ + +size_t buffer_size; + +/**************************************************************** + * Function contract proved correct by CheckOptionsInner + ****************************************************************/ + +void prvReadSackOption( const uint8_t * const pucPtr, + size_t uxIndex, + FreeRTOS_Socket_t * const pxSocket ) +{ + /* Preconditions */ + __CPROVER_assert( buffer_size < CBMC_MAX_OBJECT_SIZE, + "prvReadSackOption: buffer_size < CBMC_MAX_OBJECT_SIZE" ); + __CPROVER_assert( uxIndex <= buffer_size, + "prvReadSackOption: uxIndex <= buffer_size" ); + __CPROVER_assert( uxIndex + 8 <= buffer_size, + "prvReadSackOption: uxIndex + 8 <= buffer_size" ); + __CPROVER_assert( pucPtr != NULL, + "prvReadSackOption: pucPtr != NULL" ); + __CPROVER_assert( pxSocket != NULL, + "prvReadSackOption: pxSocket != NULL" ); + + /* No postconditions required */ +} + +/**************************************************************** + * Proof of prvSingleStepTCPHeaderOptions function contract + ****************************************************************/ + +void harness() +{ + /* Give buffer_size an unconstrained value */ + size_t buf_size; + + buffer_size = buf_size; + + uint8_t * pucPtr = malloc( buffer_size ); + size_t uxTotalLength; + FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); + BaseType_t xHasSYNFlag; + + /**************************************************************** + * Specification and proof of CheckOptions outer loop + ****************************************************************/ + + /* CBMC model of pointers limits the size of the buffer */ + __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); + + /* Preconditions */ + __CPROVER_assume( 8 <= buffer_size ); /* ulFirst and ulLast */ + __CPROVER_assume( pucPtr != NULL ); + __CPROVER_assume( uxTotalLength <= buffer_size ); + __CPROVER_assume( pxSocket != NULL ); + + size_t index = prvSingleStepTCPHeaderOptions( pucPtr, + uxTotalLength, + pxSocket, + xHasSYNFlag ); + + /* Postconditions */ + __CPROVER_assert( index == 1 || index <= uxTotalLength, + "prvSingleStepTCPHeaderOptions: index <= uxTotalLength" ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json new file mode 100644 index 000000000..dfecf7886 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json @@ -0,0 +1,20 @@ +{ + "ENTRY": "CheckOptionsOuter", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvSingleStepTCPHeaderOptions.2:32" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Stream_Buffer.goto", + "$(FREERTOS)/Source/tasks.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c new file mode 100644 index 000000000..bbed7b243 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -0,0 +1,102 @@ +/* + * 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 + */ + +/* Standard includes. */ +#include <stdint.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "FreeRTOS_ARP.h" + +/* Static members defined in FreeRTOS_DHCP.c */ +extern DHCPData_t xDHCPData; +extern Socket_t xDHCPSocket; +void prvCreateDHCPSocket(); + +/* Static member defined in freertos_api.c */ +#ifdef CBMC_GETNETWORKBUFFER_FAILURE_BOUND + extern uint32_t GetNetworkBuffer_failure_count; +#endif + +/**************************************************************** + * The signature of the function under test. + ****************************************************************/ + +void vDHCPProcess( BaseType_t xReset ); + +/**************************************************************** + * Abstract prvProcessDHCPReplies proved memory safe in ProcessDHCPReplies. + ****************************************************************/ + +BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType ) +{ + return nondet_BaseType(); +} + +/**************************************************************** + * The proof of vDHCPProcess + ****************************************************************/ + +void harness() +{ + BaseType_t xReset; + + /**************************************************************** + * Initialize the counter used to bound the number of times + * GetNetworkBufferWithDescriptor can fail. + ****************************************************************/ + + #ifdef CBMC_GETNETWORKBUFFER_FAILURE_BOUND + GetNetworkBuffer_failure_count = 0; + #endif + + /**************************************************************** + * Assume a valid socket in most states of the DHCP state machine. + * + * The socket is created in the eWaitingSendFirstDiscover state. + * xReset==True resets the state to eWaitingSendFirstDiscover. + ****************************************************************/ + + if( !( ( xDHCPData.eDHCPState == eWaitingSendFirstDiscover ) || + ( xReset != pdFALSE ) ) ) + { + prvCreateDHCPSocket(); + __CPROVER_assume( xDHCPSocket != NULL ); + } + + vDHCPProcess( xReset ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json new file mode 100644 index 000000000..d96988754 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json @@ -0,0 +1,56 @@ +# +# 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": "DHCPProcess", + + # Minimal buffer size for maximum coverage, see harness for details. + "BUFFER_SIZE": 299, + + # The number of times GetNetworkBufferWithDescriptor can be allowed to fail + # (plus 1). + "FAILURE_BOUND": 2, + + "CBMCFLAGS": "--unwind 4 --unwindset strlen.0:11,memcmp.0:7,prvProcessDHCPReplies.0:8,prvCreatePartDHCPMessage.0:{FAILURE_BOUND} --nondet-static --flush", + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/cbmc.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + + "DEF": + [ + "BUFFER_SIZE={BUFFER_SIZE}", + "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL=1", + "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/README.md new file mode 100644 index 000000000..0de21e6b1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/README.md @@ -0,0 +1,28 @@ +This is the memory safety proof for DHCPProcess function, which is the +function that triggers the DHCP protocol. + +The main stubs in this proof deal with buffer management, which assume +that the buffer is large enough to accomodate a DHCP message plus a +few additional bytes for options (which is the last, variable-sized +field in a DHCP message). We have abstracted away sockets, concurrency +and third-party code. For more details, please check the comments on +the harness file. + +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: + +* FreeRTOS_sendto +* FreeRTOS_setsockopt +* FreeRTOS_socket +* ulRand +* vARPSendGratuitous +* vApplicationIPNetworkEventHook +* vLoggingPrintf +* vPortEnterCritical +* vPortExitCritical +* vReleaseNetworkBufferAndDescriptor +* vSocketBind +* vSocketClose + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/cbmc-viewer.json b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/cbmc-viewer.json new file mode 100644 index 000000000..1bc333788 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/cbmc-viewer.json @@ -0,0 +1,16 @@ +{ "expected-missing-functions": + [ + "vPortEnterCritical", + "vPortExitCritical", + "vSocketBind", + "vSocketClose", + "vTaskSetTimeOutState", + "xTaskGetTickCount", + "xTaskGetCurrentTaskHandle", + "xQueueGenericSend", + "xApplicationGetRandomNumber", + "vLoggingPrintf" + ], + "proof-name": "DHCPProcess", + "proof-root": "tools/cbmc/proofs" +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c new file mode 100644 index 000000000..cbde3397b --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c @@ -0,0 +1,49 @@ +/* + * 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 <stdint.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_DHCP.h" + +/* + * The harness test proceeds to call IsDHCPSocket with an unconstrained value + */ +void harness() +{ + Socket_t xSocket; + BaseType_t xResult; + + xResult = xIsDHCPSocket( xSocket ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json new file mode 100644 index 000000000..eac18fd55 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json @@ -0,0 +1,40 @@ +# +# 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": "IsDHCPSocket", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.goto" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md new file mode 100644 index 000000000..ec2cc5e21 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md @@ -0,0 +1 @@ +This is the memory safety proof for IsDCHPSocket. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c new file mode 100644 index 000000000..10a81ece8 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c @@ -0,0 +1,31 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + +/* Function prvParseDNSReply is proven to be correct separately. +The proof can be found here: https://github.com/aws/amazon-freertos/tree/master/tools/cbmc/proofs/ParseDNSReply */ +uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer, + size_t xBufferLength, + BaseType_t xExpected ) {} + +struct xDNSMessage { + uint16_t usIdentifier; + uint16_t usFlags; + uint16_t usQuestions; + uint16_t usAnswers; + uint16_t usAuthorityRRs; + uint16_t usAdditionalRRs; +}; + +typedef struct xDNSMessage DNSMessage_t; + +void harness() { + NetworkBufferDescriptor_t xNetworkBuffer; + xNetworkBuffer.pucEthernetBuffer = malloc(sizeof(UDPPacket_t)+sizeof(DNSMessage_t)); + ulDNSHandlePacket(&xNetworkBuffer); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json new file mode 100644 index 000000000..6b2530527 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json @@ -0,0 +1,12 @@ +{ + "ENTRY": "DNShandlePacket", + "CBMCFLAGS": "--unwind 1", + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c new file mode 100644 index 000000000..0aa26dcb6 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c @@ -0,0 +1,16 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + + +void harness() { + if( ipconfigUSE_DNS_CACHE != 0 ) { + FreeRTOS_dnsclear(); + } + +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/Makefile.json new file mode 100644 index 000000000..22f54b074 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/Makefile.json @@ -0,0 +1,20 @@ +{ + "ENTRY": "DNSclear", + ################################################################ + # This configuration flag uses DNS cache + "USE_CACHE":1, + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + "DEF": + [ + "ipconfigUSE_DNS_CACHE={USE_CACHE}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c new file mode 100644 index 000000000..d831b5709 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -0,0 +1,94 @@ +/* Standard includes. */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_DHCP.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" + +#include "cbmc.h" + +/**************************************************************** + * We abstract: + * + * All kernel task scheduling functions since we are doing + * sequential verification and the sequential verification of these + * sequential primitives is done elsewhere. + * + * Many methods in the FreeRTOS TCP API in stubs/freertos_api.c + * + * prvParseDNSReply proved memory safe elsewhere + * + * prvCreateDNSMessage + * + * This proof assumes the length of pcHostName is bounded by + * MAX_HOSTNAME_LEN. We have to bound this length because we have to + * bound the iterations of strcmp. + ****************************************************************/ + +/**************************************************************** + * Abstract prvParseDNSReply proved memory save in ParseDNSReply. + * + * We stub out his function to fill the payload buffer with + * unconstrained data and return an unconstrained size. + * + * The function under test uses only the return value of this + * function. + ****************************************************************/ + +uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer, + size_t xBufferLength, + BaseType_t xExpected ) +{ + uint32_t size; + + __CPROVER_havoc_object( pucUDPPayloadBuffer ); + return size; +} + + +/**************************************************************** + * Abstract prvCreateDNSMessage + * + * This function writes a header, a hostname, and a constant amount of + * data into the payload buffer, and returns the amount of data + * written. This abstraction just fills the entire buffer with + * unconstrained data and returns and unconstrained length. + ****************************************************************/ + +size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer, + const char * pcHostName, + TickType_t uxIdentifier ) +{ + __CPROVER_havoc_object( pucUDPPayloadBuffer ); + size_t size; + return size; +} + +/**************************************************************** + * The proof for FreeRTOS_gethostbyname. + ****************************************************************/ + +void harness() +{ + size_t len; + + __CPROVER_assume( len <= MAX_HOSTNAME_LEN ); + char * pcHostName = safeMalloc( len ); + + __CPROVER_assume( len > 0 ); /* prvProcessDNSCache strcmp */ + __CPROVER_assume( pcHostName != NULL ); + pcHostName[ len - 1 ] = NULL; + FreeRTOS_gethostbyname( pcHostName ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json new file mode 100644 index 000000000..e0117e38e --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json @@ -0,0 +1,33 @@ +{ + "ENTRY": "DNSgetHostByName", + + ################################################################ + # This configuration sets callback to 0. + # It also sets MAX_HOSTNAME_LEN to 10 to bound strcmp. + # According to the specification MAX_HOST_NAME is upto 255. + + "callback": 0, + "MAX_HOSTNAME_LEN": 10, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", + + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvProcessDNSCache.0:5,prvGetHostByName.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.1:{HOSTNAME_UNWIND},strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},strcmp.0:{HOSTNAME_UNWIND},strcpy.0:{HOSTNAME_UNWIND}", + "--nondet-static" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/cbmc.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + + "DEF": + [ + "ipconfigDNS_USE_CALLBACKS={callback}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/cbmc-viewer.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/cbmc-viewer.json new file mode 100644 index 000000000..82e9e2b4e --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/cbmc-viewer.json @@ -0,0 +1,9 @@ +{ "expected-missing-functions": + [ + "vLoggingPrintf", + "xApplicationGetRandomNumber", + "xTaskGetTickCount" + ], + "proof-name": "DNSgetHostByName", + "proof-root": "tools/cbmc/proofs" +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c new file mode 100644 index 000000000..b6e30c8f3 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -0,0 +1,110 @@ +/* Standard includes. */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_DHCP.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" + +#include "cbmc.h" + +/**************************************************************** + * We abstract: + * + * All kernel task scheduling functions since we are doing + * sequential verification and the sequential verification of these + * sequential primitives is done elsewhere. + * + * Many methods in the FreeRTOS TCP API in stubs/freertos_api.c + * + * prvParseDNSReply proved memory safe elsewhere + * + * prvCreateDNSMessage + * + * This proof assumes the length of pcHostName is bounded by + * MAX_HOSTNAME_LEN. We have to bound this length because we have to + * bound the iterations of strcmp. + ****************************************************************/ + +/**************************************************************** + * Abstract prvParseDNSReply proved memory safe in ParseDNSReply. + * + * We stub out his function to fill the payload buffer with + * unconstrained data and return an unconstrained size. + * + * The function under test uses only the return value of this + * function. + ****************************************************************/ + +uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer, + size_t xBufferLength, + BaseType_t xExpected ) +{ + __CPROVER_assert(pucUDPPayloadBuffer != NULL, + "Precondition: pucUDPPayloadBuffer != NULL"); + + __CPROVER_havoc_object( pucUDPPayloadBuffer ); + return nondet_uint32(); +} + +/**************************************************************** + * Abstract prvCreateDNSMessage + * + * This function writes a header, a hostname, and a constant amount of + * data into the payload buffer, and returns the amount of data + * written. This abstraction just fills the entire buffer with + * unconstrained data and returns and unconstrained length. + ****************************************************************/ + +size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer, + const char * pcHostName, + TickType_t uxIdentifier ) +{ + __CPROVER_assert(pucUDPPayloadBuffer != NULL, + "Precondition: pucUDPPayloadBuffer != NULL"); + __CPROVER_assert(pcHostName != NULL, + "Precondition: pcHostName != NULL"); + + __CPROVER_havoc_object( pucUDPPayloadBuffer ); + return nondet_sizet(); +} + +/**************************************************************** + * A stub for a function callback. + ****************************************************************/ + +void func(const char * pcHostName, void * pvSearchID, uint32_t ulIPAddress) +{ +} + +/**************************************************************** + * The proof for FreeRTOS_gethostbyname_a. + ****************************************************************/ + +void harness() { + size_t len; + + __CPROVER_assume( len <= MAX_HOSTNAME_LEN ); + char * pcHostName = safeMalloc( len ); + + __CPROVER_assume( len > 0 ); /* prvProcessDNSCache strcmp */ + __CPROVER_assume( pcHostName != NULL ); + pcHostName[ len - 1 ] = NULL; + + FOnDNSEvent pCallback = func; + TickType_t xTimeout; + void *pvSearchID; + + FreeRTOS_gethostbyname_a(pcHostName, pCallback, pvSearchID, xTimeout); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json new file mode 100644 index 000000000..5a3051004 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json @@ -0,0 +1,30 @@ +{ + "ENTRY": "DNSgetHostByName_a", + ################################################################ + # This configuration flag sets callback to 1. It also sets MAX_HOSTNAME_LEN to 10 and MAX_REQ_SIZE to 50 for performance issues. + # According to the specification MAX_HOST_NAME is upto 255. + "callback": 1, + "MAX_HOSTNAME_LEN": 10, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvCreateDNSMessage.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.1:{HOSTNAME_UNWIND},prvGetHostByName.0:{HOSTNAME_UNWIND},prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},strcmp.0:{HOSTNAME_UNWIND},xTaskResumeAll.0:{HOSTNAME_UNWIND},xTaskResumeAll.1:{HOSTNAME_UNWIND},strcpy.0:{HOSTNAME_UNWIND}", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/cbmc.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto" + ], + "DEF": + [ + "ipconfigDNS_USE_CALLBACKS={callback}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}", + # This value is defined only when ipconfigUSE_DNS_CACHE==1 + "ipconfigDNS_CACHE_NAME_LENGTH=254" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/cbmc-viewer.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/cbmc-viewer.json new file mode 100644 index 000000000..a526bee36 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/cbmc-viewer.json @@ -0,0 +1,13 @@ +{ "expected-missing-functions": + [ + "vLoggingPrintf", + "xApplicationGetRandomNumber", + "vListInsertEnd", + "vTaskSetTimeOutState", + "vTaskSuspendAll", + "xTaskGetTickCount", + "xTaskResumeAll" + ], + "proof-name": "DNSgetHostByName_a", + "proof-root": "tools/cbmc/proofs" +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c new file mode 100644 index 000000000..1e5832b20 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c @@ -0,0 +1,49 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" +#include "list.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + + +/* This proof assumes the length of pcHostName is bounded by MAX_HOSTNAME_LEN. This also abstracts the concurrency. */ + +void vDNSInitialise(void); + +void vDNSSetCallBack(const char *pcHostName, void *pvSearchID, FOnDNSEvent pCallbackFunction, TickType_t xTimeout, TickType_t xIdentifier); + +void *safeMalloc(size_t xWantedSize) { /* Returns a NULL pointer if the wanted size is 0. */ + if(xWantedSize == 0) { + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +/* Abstraction of xTaskCheckForTimeOut from task pool. This also abstracts the concurrency. */ +BaseType_t xTaskCheckForTimeOut(TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait) { } + +/* Abstraction of xTaskResumeAll from task pool. This also abstracts the concurrency. */ +BaseType_t xTaskResumeAll(void) { } + +/* The function func mimics the callback function.*/ +void func(const char * pcHostName, void * pvSearchID, uint32_t ulIPAddress) {} + +void harness() { + vDNSInitialise(); /* We initialize the callbacklist in order to be able to check for functions that timed out. */ + size_t pvSearchID; + FOnDNSEvent pCallback = func; + TickType_t xTimeout; + TickType_t xIdentifier; + size_t len; + __CPROVER_assume(len >= 0 && len <= MAX_HOSTNAME_LEN); + char *pcHostName = safeMalloc(len); + if (len && pcHostName) { + pcHostName[len-1] = NULL; + } + vDNSSetCallBack( pcHostName, &pvSearchID, pCallback, xTimeout, xIdentifier); /* Add an item to be able to check the cancel function if the list is non-empty. */ + FreeRTOS_gethostbyname_cancel(&pvSearchID); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json new file mode 100644 index 000000000..02d95ab27 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json @@ -0,0 +1,29 @@ +{ + "ENTRY": "DNSgetHostByName_cancel", + ################################################################ + # This configuration flag sets callback to 1. It also sets MAX_HOSTNAME_LEN to 10 for performance issues. + # According to the specification MAX_HOST_NAME is upto 255. + "callback": 1, + "MAX_HOSTNAME_LEN": 10, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},vDNSCheckCallBack.0:2,strcpy.0:{HOSTNAME_UNWIND}", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto", + "$(FREERTOS)/Source/tasks.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": + [ + "ipconfigDNS_USE_CALLBACKS={callback}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}", + # This value is defined only when ipconfigUSE_DNS_CACHE==1 + "ipconfigDNS_CACHE_NAME_LENGTH=254" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c new file mode 100644 index 000000000..5b725c4ca --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c @@ -0,0 +1,32 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" +#include "list.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + +/* This assumes that the length of the hostname is bounded by MAX_HOSTNAME_LEN. */ +void *safeMalloc(size_t xWantedSize) { + if(xWantedSize == 0) { + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +void harness() { + if(ipconfigUSE_DNS_CACHE != 0) { + size_t len; + __CPROVER_assume(len >= 0 && len <= MAX_HOSTNAME_LEN); + char *pcHostName = safeMalloc(len); /* malloc is replaced by safeMalloc */ + if (len && pcHostName) { + pcHostName[len-1] = NULL; + } + if (pcHostName) { /* guarding against NULL pointer */ + FreeRTOS_dnslookup(pcHostName); + } + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json new file mode 100644 index 000000000..2187bb914 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json @@ -0,0 +1,26 @@ +{ + "ENTRY": "DNSlookup", + ################################################################ + # This configuration uses DNS cache and the MAX_HOSTNAME_LEN is set to 255 according to the specification + "MAX_HOSTNAME_LEN": 255, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", + "USE_CACHE": 1, + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvProcessDNSCache.0:5,strcmp.0:{HOSTNAME_UNWIND}", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + "ipconfigUSE_DNS_CACHE={USE_CACHE}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}" + ], + "OPT" : "-m32" +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json new file mode 100644 index 000000000..083feb6e2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json @@ -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 +# + +{ + "ENTRY": "SendEventToIPTask", + "CBMCFLAGS": [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto", + "$(FREERTOS)/Source/tasks.goto" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/README.md new file mode 100644 index 000000000..4682310df --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/README.md @@ -0,0 +1,13 @@ +This is the memory safety proof for xSendEventToIPTask, a function used +for sending different events to IP-Task. We have abstracted away queues. + +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: + +* uxQueueMessagesWaiting +* xQueueGenericSend + +The coverage is imperfect (97%) because xSendEventToIPTask always +calls xSendEventStructToIPTask with xTimeout==0. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c new file mode 100644 index 000000000..9bdcbf7af --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_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 <stdint.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" + +// The harness test proceeds to call SendEventToIPTask with an unconstrained value +void harness() +{ + eIPEvent_t eEvent; + xSendEventToIPTask( eEvent ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/Makefile.template b/FreeRTOS-Plus/Test/CBMC/proofs/Makefile.template new file mode 100644 index 000000000..a029394c2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/Makefile.template @@ -0,0 +1,160 @@ +default: report + +# ____________________________________________________________________ +# CBMC binaries +# + +GOTO_CC = @GOTO_CC@ +GOTO_INSTRUMENT = goto-instrument +GOTO_ANALYZER = goto-analyzer +VIEWER = cbmc-viewer + +# ____________________________________________________________________ +# Variables +# +# Naming scheme: +# `````````````` +# FOO is the concatenation of the following: +# FOO2: Set of command line +# C_FOO: Value of $FOO common to all harnesses, set in this file +# O_FOO: Value of $FOO specific to the OS we're running on, set in the +# makefile for the operating system +# H_FOO: Value of $FOO specific to a particular harness, set in the +# makefile for that harness + +ENTRY = $(H_ENTRY) +OBJS = $(H_OBJS) + +INC = \ + $(INC2) \ + $(C_INC) $(O_INC) $(H_INC) \ + # empty + +CFLAGS = \ + $(CFLAGS2) \ + $(C_DEF) $(O_DEF) $(H_DEF) $(DEF) \ + $(C_OPT) $(O_OPT) $(H_OPT) $(OPT) \ + -m32 \ + # empty + +CBMCFLAGS = \ + $(CBMCFLAGS2) \ + $(C_CBMCFLAGS) $(O_CBMCFLAGS) $(H_CBMCFLAGS) \ + # empty + +INSTFLAGS = \ + $(INSTFLAGS2) \ + $(C_INSTFLAGS) $(O_INSTFLAGS) $(H_INSTFLAGS) \ + # empty + +# ____________________________________________________________________ +# Rules +# +# Rules for building a:FR object files. These are not harness-specific, +# and several harnesses might depend on a particular a:FR object, so +# define them all once here. + +@RULE_GOTO@ + $(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) @RULE_INPUT@ + +# ____________________________________________________________________ +# Rules +# +# Rules for patching + +patch: + cd $(PROOFS)/../patches && ./patch.py + +unpatch: + cd $(PROOFS)/../patches && ./unpatch.py + +# ____________________________________________________________________ +# Rules +# +# Rules for building the CBMC harness + +queue_datastructure.h: $(H_OBJS_EXCEPT_HARNESS) + python3 @TYPE_HEADER_SCRIPT@ --binary $(FREERTOS)/Source/queue.goto --c-file $(FREERTOS)/Source/queue.c + +$(ENTRY)_harness.goto: $(ENTRY)_harness.c $(H_GENERATE_HEADER) + $(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) @RULE_INPUT@ + +$(ENTRY)1.goto: $(OBJS) + $(GOTO_CC) @COMPILE_LINK@ @RULE_OUTPUT@ --function harness $(OBJS) + +$(ENTRY)2.goto: $(ENTRY)1.goto + $(GOTO_INSTRUMENT) --add-library @RULE_INPUT@ @RULE_OUTPUT@ \ + > $(ENTRY)2.txt 2>&1 + +$(ENTRY)3.goto: $(ENTRY)2.goto + $(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \ + > $(ENTRY)3.txt 2>&1 + +$(ENTRY)4.goto: $(ENTRY)3.goto + $(GOTO_INSTRUMENT) $(INSTFLAGS) --slice-global-inits @RULE_INPUT@ @RULE_OUTPUT@ \ + > $(ENTRY)4.txt 2>&1 +# ____________________________________________________________________ +# After running goto-instrument to remove function bodies the unused +# functions need to be dropped again. + +$(ENTRY)5.goto: $(ENTRY)4.goto + $(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \ + > $(ENTRY)5.txt 2>&1 + +$(ENTRY).goto: $(ENTRY)5.goto + @CP@ @RULE_INPUT@ @RULE_OUTPUT@ + +# ____________________________________________________________________ +# Rules +# +# Rules for running CBMC + +goto: + $(MAKE) patch + $(MAKE) $(ENTRY).goto + +cbmc.txt: $(ENTRY).goto + - cbmc $(CBMCFLAGS) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1 + +property.xml: $(ENTRY).goto + cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1 + +coverage.xml: $(ENTRY).goto + cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1 + +cbmc: cbmc.txt + +property: property.xml + +coverage: coverage.xml + +report: cbmc.txt property.xml coverage.xml + $(VIEWER) \ + --goto $(ENTRY).goto \ + --srcdir $(FREERTOS) \ + --blddir $(FREERTOS) \ + --htmldir html \ + --srcexclude "(.@FORWARD_SLASH@doc|.@FORWARD_SLASH@tests|.@FORWARD_SLASH@vendors)" \ + --result cbmc.txt \ + --property property.xml \ + --block coverage.xml + +# ____________________________________________________________________ +# Rules +# +# Rules for cleaning up + +clean: + @RM@ $(OBJS) $(ENTRY).goto + @RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt + @RM@ cbmc.txt property.xml coverage.xml TAGS TAGS-* + @RM@ *~ \#* + @RM@ queue_datastructure.h + + +veryclean: clean + @RM_RECURSIVE@ html + +distclean: veryclean + cd $(PROOFS)/../patches && ./unpatch.py + cd $(PROOFS) && ./make-remove-makefiles.py diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json new file mode 100644 index 000000000..1d49986d2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json @@ -0,0 +1,47 @@ +{ + "FREERTOS": [ " ../../../../FreeRTOS" ], + "PROOFS": [ "." ], + + "DEF ": [ + "WIN32", + "WINVER=0x400", + "_CONSOLE", + "_CRT_SECURE_NO_WARNINGS", + "_DEBUG", + "_WIN32_WINNT=0x0500", + "__PRETTY_FUNCTION__=__FUNCTION__", + "__free_rtos__", + + "CBMC", + "'configASSERT(X)=__CPROVER_assert(X,\"Assertion Error\")'", + "'configPRECONDITION(X)=__CPROVER_assume(X)'", + "'_static='", + "'_volatile='" + ], + + "INC ": [ + "$(FREERTOS)/Source/include", + "$(FREERTOS)/Source/portable/MSVC-MingW", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/Compiler/MSVC", + "$(FREERTOS)/../FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Minimal_Windows_Simulator/WinPCap", + "$(FREERTOS)/Demo/Common/include", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/include", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/patches", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/windows", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/windows2" + ], + + "CBMCFLAGS ": [ + "--object-bits 7", + "--32", + "--bounds-check", + "--pointer-check" + ], + + "FORWARD_SLASH": ["/"], + + "TYPE_HEADERS": [ + "$(FREERTOS)/Source/queue.c" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/MakefileLinux.json b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileLinux.json new file mode 100644 index 000000000..08442a2ab --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileLinux.json @@ -0,0 +1,36 @@ +{ + "GOTO_CC": [ + "goto-cc" + ], + "COMPILE_LINK": [ + "-o" + ], + "COMPILE_ONLY": [ + "-c", + "-o" + ], + "RULE_INPUT": [ + "$<" + ], + "RULE_OUTPUT": [ + "$@" + ], + "RULE_GOTO": [ + "%.goto : %.c" + ], + "INC": [ + "$(PROOFS)/../windows" + ], + "RM": [ + "$(RM)" + ], + "RM_RECURSIVE": [ + "$(RM) -r" + ], + "CP": [ + "cp" + ], + "TYPE_HEADER_SCRIPT": [ + "$(PROOFS)/make_type_header_files.py" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/MakefileWindows.json b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileWindows.json new file mode 100644 index 000000000..543dd6219 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileWindows.json @@ -0,0 +1,44 @@ +{ + "DEF": [ + "WIN32" + ], + "GOTO_CC": [ + "goto-cl" + ], + "COMPILE_LINK": [ + "/Fe" + ], + "COMPILE_ONLY": [ + "/c", + "/Fo" + ], + "RULE_INPUT": [ + "$**" + ], + "RULE_OUTPUT": [ + "$@" + ], + "RULE_GOTO": [ + ".c.goto:" + ], + "OPT": [ + "/wd4210", + "/wd4127", + "/wd4214", + "/wd4201", + "/wd4244", + "/wd4310" + ], + "RM": [ + "del" + ], + "RM_RECURSIVE": [ + "del /s" + ], + "CP": [ + "copy" + ], + "TYPE_HEADER_SCRIPT": [ + "$(PROOFS)\\make_type_header_files.py" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/Makefile.json new file mode 100644 index 000000000..f372c41da --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/Makefile.json @@ -0,0 +1,68 @@ +# The proof depends on one parameter: +# NETWORK_BUFFER_SIZE is the size of the network buffer being parsed +# The buffer size must be bounded because we must bound the number of +# iterations loops iterating over the buffer. + +{ + "ENTRY": "ParseDNSReply", + +################################################################ +# This is the network buffer size. +# Reasonable values are size > 12 = sizeof(xDNSMessage) + "NETWORK_BUFFER_SIZE": 40, + +################################################################ +# This is the size of the buffer into which the name is copied. +# Set to any positive value. +# In the source, NAME_SIZE=254 and NETWORK_BUFFER_SIZE >> NAME_SIZE +# In the proof, NAME_SIZE >= 4 required for good coverage. + "NAME_SIZE": "10", + +################################################################ +# Loop prvParseDNSReply.0: +# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 915 + "PARSELOOP0": "prvParseDNSReply.0", + +# M = sizeof( DNSMessage_t ) = 12 +# U = sizeof( uint32_t) = 4 +# Loop bound is (NETWORK_BUFFER_SIZE - M) div (U+1) + 1 tight for SIZE >= M +# Loop bound is 1 for 0 <= SIZE < M + "PARSELOOP0_UNWIND": + "__eval 1 if {NETWORK_BUFFER_SIZE} < 12 else ({NETWORK_BUFFER_SIZE} - 12) / 5 + 1", + +################################################################ +# Loop prvParseDNSReply.1: +# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 989 + "PARSELOOP1": "prvParseDNSReply.1", + +# A = sizeof( DNSAnswerRecord_t ) = 10 +# M = sizeof( DNSMessage_t ) = 12 +# U = sizeof( uint32_t) = 4 +# Loop bound is (NETWORK_BUFFER_SIZE - M - A) div (A+1) + A + 1 tight +# for SIZE >= M + A +# Loop bound is (NETWORK_BUFFER_SIZE - M) + 1 for M <= SIZE < M + A +# Loop bound is 1 for 0 <= SIZE < M + "PARSELOOP1_UNWIND": + "__eval 1 if {NETWORK_BUFFER_SIZE} < 12 else ({NETWORK_BUFFER_SIZE} - 11 if {NETWORK_BUFFER_SIZE} < 22 else ({NETWORK_BUFFER_SIZE} - 12 - 10) / 11 + 11)", + +################################################################ + + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset {PARSELOOP0}:{PARSELOOP0_UNWIND},{PARSELOOP1}:{PARSELOOP1_UNWIND},prvProcessDNSCache.0:5" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + + "DEF": + [ + "NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}", + "NAME_SIZE={NAME_SIZE}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/ParseDNSReply_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/ParseDNSReply_harness.c new file mode 100644 index 000000000..3ae1256a0 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/ParseDNSReply_harness.c @@ -0,0 +1,130 @@ +/* Standard includes. */ +#include <stdint.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "list.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DNS.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" +#include "IPTraceMacroDefaults.h" + +#include "cbmc.h" + +/**************************************************************** + * Signature of function under test + ****************************************************************/ + +uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer, + size_t uxBufferLength, + BaseType_t xExpected ); + +/**************************************************************** + * Abstraction of prvReadNameField proved in ReadNameField + ****************************************************************/ + +size_t prvReadNameField( const uint8_t *pucByte, + size_t uxRemainingBytes, + char *pcName, + size_t uxDestLen ) +{ + __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, + "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE"); + __CPROVER_assert(NAME_SIZE < CBMC_MAX_OBJECT_SIZE, + "NAME_SIZE < CBMC_MAX_OBJECT_SIZE"); + __CPROVER_assert(NAME_SIZE >= 4, + "NAME_SIZE >= 4 required for good coverage."); + + + /* Preconditions */ + __CPROVER_assert(uxRemainingBytes < CBMC_MAX_OBJECT_SIZE, + "ReadNameField: uxRemainingBytes < CBMC_MAX_OBJECT_SIZE)"); + __CPROVER_assert(uxDestLen < CBMC_MAX_OBJECT_SIZE, + "ReadNameField: uxDestLen < CBMC_MAX_OBJECT_SIZE)"); + + __CPROVER_assert(uxRemainingBytes <= NETWORK_BUFFER_SIZE, + "ReadNameField: uxRemainingBytes <= NETWORK_BUFFER_SIZE)"); + + /* This precondition in the function contract for prvReadNameField + * fails because prvCheckOptions called prvReadNameField with the + * constant value 254. + __CPROVER_assert(uxDestLen <= NAME_SIZE, + "ReadNameField: uxDestLen <= NAME_SIZE)"); + */ + + __CPROVER_assert( pucByte != NULL , + "ReadNameField: pucByte != NULL )"); + __CPROVER_assert( pcName != NULL , + "ReadNameField: pcName != NULL )"); + + __CPROVER_assert(uxDestLen > 0, + "ReadNameField: uxDestLen > 0)"); + + /* Return value */ + size_t index; + + /* Postconditions */ + __CPROVER_assume( index <= uxDestLen+1 && index <= uxRemainingBytes ); + + return index; +} + +/**************************************************************** + * Abstraction of prvSkipNameField proved in SkipNameField + ****************************************************************/ + +size_t prvSkipNameField( const uint8_t *pucByte, size_t uxLength ) +{ + + __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, + "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE"); + + + /* Preconditions */ + __CPROVER_assert(uxLength < CBMC_MAX_OBJECT_SIZE, + "SkipNameField: uxLength < CBMC_MAX_OBJECT_SIZE)"); + __CPROVER_assert(uxLength <= NETWORK_BUFFER_SIZE, + "SkipNameField: uxLength <= NETWORK_BUFFER_SIZE)"); + __CPROVER_assert(pucByte != NULL, + "SkipNameField: pucByte != NULL)"); + + /* Return value */ + size_t index; + + /* Postconditions */ + __CPROVER_assume(index <= uxLength); + + return index; +} + +/**************************************************************** + * Proof of prvParseDNSReply + ****************************************************************/ + +void harness() { + + size_t uxBufferLength; + BaseType_t xExpected; + uint8_t *pucUDPPayloadBuffer = malloc(uxBufferLength); + + __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, + "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE"); + + __CPROVER_assume(uxBufferLength < CBMC_MAX_OBJECT_SIZE); + __CPROVER_assume(uxBufferLength <= NETWORK_BUFFER_SIZE); + __CPROVER_assume(pucUDPPayloadBuffer != NULL); + + uint32_t index = prvParseDNSReply( pucUDPPayloadBuffer, + uxBufferLength, + xExpected ); + +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json new file mode 100644 index 000000000..c708bac13 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json @@ -0,0 +1,48 @@ +# The proof depends on one parameter: +# BUFFER_SIZE is the size of the buffer being parsed +# The buffer size must be bounded because we must bound the number of +# iterations loops iterating over the buffer. + +{ + "ENTRY": "ProcessDHCPReplies", + +################################################################ +# Buffer header: sizeof(DHCPMessage_t) = 241 +# Buffer header: sizeof(DHCPMessage_IPv4_t) = 240 + "BUFFER_HEADER": 240, + +################################################################ +# Buffer size +# Reasonable sizes are BUFFER_SIZE > BUFFER_HEADER +# Sizes smaller than this causes CBMC to fail in simplify_byte_extract + "BUFFER_SIZE": 252, + +################################################################ +# Buffer payload + "BUFFER_PAYLOAD": "__eval 1 if {BUFFER_SIZE} <= {BUFFER_HEADER} else {BUFFER_SIZE} - {BUFFER_HEADER} + 1", + +################################################################ + + "CBMCFLAGS": [ + # "--nondet-static", + "--unwind 1", + "--unwindset memcmp.0:7,prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/cbmc.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement/BufferAllocation_2.goto", + "$(FREERTOS)/Source/event_groups.goto", + "$(FREERTOS)/Source/list.goto" + ], + + "DEF": + [ + "CBMC_DHCPMESSAGE_HEADER_SIZE={BUFFER_HEADER}", + "CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c new file mode 100644 index 000000000..ec2fb1c8c --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c @@ -0,0 +1,37 @@ +/* Standard includes. */ +#include <stdint.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "FreeRTOS_ARP.h" + + +/**************************************************************** + * Signature of function under test + ****************************************************************/ + +BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType ); + +/**************************************************************** + * The proof for FreeRTOS_gethostbyname. + ****************************************************************/ + +void harness() +{ + /* Omitting model of an unconstrained xDHCPData because xDHCPData is */ + /* the source of uninitialized data only on line 647 to set a */ + /* transaction id is an outgoing message */ + + BaseType_t xExpectedMessageType; + + prvProcessDHCPReplies( xExpectedMessageType ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/README.md new file mode 100644 index 000000000..48fb7c48d --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/README.md @@ -0,0 +1 @@ +This directory contains the proofs checked by CBMC. For each entry point of FreeRTOS tested, there is a directory that contains the test harness and cbmc configuration information needed to check the proof.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/Makefile.json new file mode 100644 index 000000000..05f3d4208 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/Makefile.json @@ -0,0 +1,54 @@ +{ + "ENTRY": "ReadNameField", + +################################################################ +#Enable DNS callbacks or else ReadNameField is not defined + "callbacks": "1", + +################################################################ +# This is the network buffer size. Set to any positive value. + "NETWORK_BUFFER_SIZE" : "10", + +################################################################ +# This is the size of the buffer into which the name is copied. +# Set to any positive value. +# In the source, NAME_SIZE=254 and NETWORK_BUFFER_SIZE >> NAME_SIZE +# In the proof, NAME_SIZE >= 4 required for good coverage. + "NAME_SIZE": "6", + +################################################################ +# Loop prvReadNameField.0: +# should be min of buffer size and name size +# but loop must be unwound at least once, so max of this and 1+1 + "READLOOP0": "prvReadNameField.0", + "READLOOP0_UNWIND": "__eval max(2, min({NETWORK_BUFFER_SIZE}, {NAME_SIZE}+1))", + +################################################################ +# Loop prvReadNameField.1: +# should be min of buffer size and name size +# but loop must be unwound at least twice, so max of this and 2+1 + "READLOOP1": "prvReadNameField.1", + "READLOOP1_UNWIND": "__eval max(3, min({NETWORK_BUFFER_SIZE}, {NAME_SIZE}))", + +################################################################ + + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset {READLOOP0}:{READLOOP0_UNWIND},{READLOOP1}:{READLOOP1_UNWIND}" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + + "DEF": + [ + "NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}", + "NAME_SIZE={NAME_SIZE}", + "ipconfigDNS_USE_CALLBACKS={callbacks}", + "ipconfigDNS_CACHE_NAME_LENGTH=254" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c new file mode 100644 index 000000000..86e30b1fd --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c @@ -0,0 +1,102 @@ +/* Standard includes. */ +#include <stdint.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "list.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DNS.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" +#include "IPTraceMacroDefaults.h" + +#include "cbmc.h" + +/**************************************************************** + * Signature of function under test + ****************************************************************/ + +size_t prvReadNameField( const uint8_t *pucByte, + size_t uxRemainingBytes, + char *pcName, + size_t uxDestLen ); + +/**************************************************************** + * The function under test is not defined in all configurations + ****************************************************************/ + +#if ( ipconfigUSE_DNS_CACHE == 1 ) || ( ipconfigDNS_USE_CALLBACKS == 1 ) + +/* prvReadNameField is defined in this configuration */ + +#else + +/* prvReadNameField is not defined in this configuration, stub it. */ + +size_t prvReadNameField( const uint8_t *pucByte, + size_t uxRemainingBytes, + char *pcName, + size_t uxDestLen ) +{ + return 0; +} + +#endif + + +/**************************************************************** + * Proof of prvReadNameField function contract + ****************************************************************/ + +void harness() { + + __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, + "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE"); + __CPROVER_assert(NAME_SIZE < CBMC_MAX_OBJECT_SIZE, + "NAME_SIZE < CBMC_MAX_OBJECT_SIZE"); + + __CPROVER_assert(NAME_SIZE >= 4, + "NAME_SIZE >= 4 required for good coverage."); + + + size_t uxRemainingBytes; + size_t uxDestLen; + + uint8_t *pucByte = malloc(uxRemainingBytes); + char *pcName = malloc(uxDestLen); + + /* Preconditions */ + + __CPROVER_assume(uxRemainingBytes < CBMC_MAX_OBJECT_SIZE); + __CPROVER_assume(uxDestLen < CBMC_MAX_OBJECT_SIZE); + + __CPROVER_assume(uxRemainingBytes <= NETWORK_BUFFER_SIZE); + __CPROVER_assume(uxDestLen <= NAME_SIZE); + + __CPROVER_assume( pucByte != NULL ); + __CPROVER_assume( pcName != NULL ); + + /* Avoid overflow on uxSourceLen - 1U with uxSourceLen == uxRemainingBytes */ + //__CPROVER_assume(uxRemainingBytes > 0); + + /* Avoid overflow on uxDestLen - 1U */ + __CPROVER_assume(uxDestLen > 0); + + size_t index = prvReadNameField( pucByte, + uxRemainingBytes, + pcName, + uxDestLen ); + + /* Postconditions */ + + __CPROVER_assert( index <= uxDestLen+1 && index <= uxRemainingBytes, + "prvReadNamefield: index <= uxDestLen+1"); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/Makefile.json new file mode 100644 index 000000000..cb2e7a9cc --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/Makefile.json @@ -0,0 +1,32 @@ +{ + "ENTRY": "SkipNameField", + +################################################################ +# This is the network buffer size. This can be set to any positive value. + "NETWORK_BUFFER_SIZE": 10, + +################################################################ +# Loop prvSkipNameField.0: +# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 778 +# bound should be half network buffer size, since chunk length is at least 2 + "SKIPLOOP0": "prvSkipNameField.0", + "SKIPLOOP0_UNWIND": "__eval ({NETWORK_BUFFER_SIZE} + 1) / 2", + +################################################################ + + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset {SKIPLOOP0}:{SKIPLOOP0_UNWIND}" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + "DEF": + [ + "NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c new file mode 100644 index 000000000..2820e444d --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c @@ -0,0 +1,54 @@ +/* Standard includes. */ +#include <stdint.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "list.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DNS.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" +#include "IPTraceMacroDefaults.h" + +#include "cbmc.h" + +/**************************************************************** + * Signature of function under test + ****************************************************************/ + +size_t prvSkipNameField( const uint8_t *pucByte, size_t uxLength ); + +/**************************************************************** + * Proof of prvSkipNameField function contract + ****************************************************************/ + +void harness() { + + __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, + "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE"); + + size_t uxLength; + uint8_t *pucByte = malloc( uxLength ); + + /* Preconditions */ + + __CPROVER_assume(uxLength < CBMC_MAX_OBJECT_SIZE); + __CPROVER_assume(uxLength <= NETWORK_BUFFER_SIZE); + __CPROVER_assume(pucByte != NULL); + + size_t index = prvSkipNameField( pucByte, uxLength ); + + /* Postconditions */ + + __CPROVER_assert(index <= uxLength, + "prvSkipNameField: index <= uxLength"); + +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json new file mode 100644 index 000000000..8f2f3037e --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json @@ -0,0 +1,59 @@ +# +# 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": "TCPHandleState", + "TX_DRIVER":1, + "RX_MESSAGES":1, + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvWinScaleFactor.0:2", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto" + ], + "DEF": + [ + "ipconfigZERO_COPY_TX_DRIVER={TX_DRIVER}", + "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INSTFLAGS": + [ + "--remove-function-body prvTCPPrepareSend", + "--remove-function-body prvTCPReturnPacket" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md new file mode 100644 index 000000000..8f08c5931 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md @@ -0,0 +1,22 @@ +This is the memory safety proof for prvTCPHandleState. + +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: + +* prvTCPPrepareSend (proved independently) +* prvTCPReturnPacket (proved independently) + +* lTCPAddRxdata +* lTCPWindowRxCheck +* lTCPWindowTxAdd +* ulTCPWindowTxAck +* vTCPWindowInit +* xTCPWindowRxEmpty +* xTCPWindowTxDone + +* uxStreamBufferGet +* vReleaseNetworkBufferAndDescriptor +* vSocketWakeUpUser +* xTaskGetTickCount diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c new file mode 100644 index 000000000..03867685a --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c @@ -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 + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_TCP_IP.h" + +#include "../../utility/memory_assignments.c" + +/* This proof assumes that prvTCPPrepareSend and prvTCPReturnPacket are correct. +These functions are proved to be correct separately. */ + +BaseType_t publicTCPHandleState( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer ); + +void harness() { + FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + size_t socketSize = sizeof(FreeRTOS_Socket_t); + if (ensure_memory_is_valid(pxSocket, socketSize)) { + /* ucOptionLength is the number of valid bytes in ulOptionsData[]. + ulOptionsData[] is initialized as uint32_t ulOptionsData[ipSIZE_TCP_OPTIONS/sizeof(uint32_t)]. + This assumption is required for a memcpy function that copies uxOptionsLength + data from pxTCPHeader->ucOptdata to pxTCPWindow->ulOptionsData.*/ + __CPROVER_assume(pxSocket->u.xTCP.xTCPWindow.ucOptionLength == sizeof(uint32_t) * ipSIZE_TCP_OPTIONS/sizeof(uint32_t)); + /* uxRxWinSize is initialized as size_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/ + __CPROVER_assume(pxSocket->u.xTCP.uxRxWinSize >= 0 && pxSocket->u.xTCP.uxRxWinSize <= sizeof(size_t)); + /* uxRxWinSize is initialized as uint16_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/ + __CPROVER_assume(pxSocket->u.xTCP.usInitMSS == sizeof(uint16_t)); + } + + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + size_t bufferSize = sizeof(NetworkBufferDescriptor_t); + if(ensure_memory_is_valid(pxNetworkBuffer, bufferSize)) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t)); + } + if (ensure_memory_is_valid(pxSocket, socketSize) && + ensure_memory_is_valid(pxNetworkBuffer, bufferSize) && + ensure_memory_is_valid(pxNetworkBuffer->pucEthernetBuffer, sizeof(TCPPacket_t)) && + ensure_memory_is_valid(pxSocket->u.xTCP.pxPeerSocket, socketSize)) { + + publicTCPHandleState(pxSocket, &pxNetworkBuffer); + + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json new file mode 100644 index 000000000..5d34818b5 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json @@ -0,0 +1,49 @@ +# +# 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": "TCPPrepareSend", + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto" + ], + "DEF": + [ + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md new file mode 100644 index 000000000..323461918 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md @@ -0,0 +1,15 @@ +This is the memory safety proof for prvTCPPrepareSend. + +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: + +* ulTCPWindowTxGet +* xTCPWindowTxDone + +* xTaskGetTickCount + +* uxStreamBufferGet +* vReleaseNetworkBufferAndDescriptor +* vSocketWakeUpUser diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c new file mode 100644 index 000000000..9c41d7b7f --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c @@ -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 + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_TCP_IP.h" +#include "FreeRTOS_Stream_Buffer.h" + +#include "../../utility/memory_assignments.c" + +/* This proof assumes that pxGetNetworkBufferWithDescriptor is implemented correctly. */ +int32_t publicTCPPrepareSend( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer, UBaseType_t uxOptionsLength ); + +/* Abstraction of pxGetNetworkBufferWithDescriptor. It creates a buffer. */ +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + NetworkBufferDescriptor_t *pxBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated (); + size_t bufferSize = sizeof(NetworkBufferDescriptor_t); + if (ensure_memory_is_valid(pxBuffer, bufferSize)) { + /* The code does not expect pucEthernetBuffer to be equal to NULL if + pxBuffer is not NULL. */ + pxBuffer->pucEthernetBuffer = malloc(xRequestedSizeBytes); + pxBuffer->xDataLength = xRequestedSizeBytes; + } + return pxBuffer; +} + +void harness() { + FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + size_t socketSize = sizeof(FreeRTOS_Socket_t); + size_t bufferSize = sizeof(TCPPacket_t); + if (ensure_memory_is_valid(pxNetworkBuffer, sizeof(*pxNetworkBuffer))) { + pxNetworkBuffer->xDataLength = bufferSize; + /* The code does not expect pucEthernetBuffer to be equal to NULL if + pxNetworkBuffer is not NULL. */ + pxNetworkBuffer->pucEthernetBuffer = malloc(bufferSize); + } + UBaseType_t uxOptionsLength; + if(pxSocket) { + publicTCPPrepareSend(pxSocket, &pxNetworkBuffer, uxOptionsLength ); + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json new file mode 100644 index 000000000..e0f4b2403 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json @@ -0,0 +1,51 @@ +# +# 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": "TCPReturnPacket", + "RX_MESSAGES":1, + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto" + ], + "DEF": + [ + "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md new file mode 100644 index 000000000..1efd644d1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md @@ -0,0 +1,10 @@ +This is the memory safety proof for prvTCPReturnPacket. + +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: + +* usGenerateChecksum +* usGenerateProtocolChecksum +* xNetworkInterfaceOutput diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c new file mode 100644 index 000000000..19552565b --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c @@ -0,0 +1,67 @@ +/* + * 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 + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_TCP_IP.h" + +#include "../../utility/memory_assignments.c" + +/* This proof assumes that pxDuplicateNetworkBufferWithDescriptor is implemented correctly. */ + +void publicTCPReturnPacket( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t *pxNetworkBuffer, uint32_t ulLen, BaseType_t xReleaseAfterSend ); + +/* Abstraction of pxDuplicateNetworkBufferWithDescriptor*/ +NetworkBufferDescriptor_t *pxDuplicateNetworkBufferWithDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer, + BaseType_t xNewLength ) { + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + if (ensure_memory_is_valid(pxNetworkBuffer, sizeof(*pxNetworkBuffer))) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t)); + __CPROVER_assume(pxNetworkBuffer->pucEthernetBuffer); + } + return pxNetworkBuffer; +} + +void harness() { + FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + if (ensure_memory_is_valid(pxNetworkBuffer, sizeof(*pxNetworkBuffer))) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t)); + __CPROVER_assume(pxNetworkBuffer->pucEthernetBuffer); + } + uint32_t ulLen; + BaseType_t xReleaseAfterSend; + /* The code does not expect both of these to be equal to NULL at the same time. */ + __CPROVER_assume(pxSocket != NULL || pxNetworkBuffer != NULL); + publicTCPReturnPacket(pxSocket, pxNetworkBuffer, ulLen, xReleaseAfterSend); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_cbmc_batch_files.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_cbmc_batch_files.py new file mode 100755 index 000000000..622e000c3 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_cbmc_batch_files.py @@ -0,0 +1,53 @@ +#!/usr/bin/env python3 +# +# Generation of the cbmc-batch.yaml files 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 os +import platform +import subprocess + + +def remove_cbmc_yaml_files(): + for dyr, _, files in os.walk("."): + cbmc_batch_files = [os.path.join(os.path.abspath(dyr), file) + for file in files if file == "cbmc-batch.yaml"] + for file in cbmc_batch_files: + os.remove(file) + + +def create_cbmc_yaml_files(): + # The YAML files are only used by CI and are not needed on Windows. + if platform.system() == "Windows": + return + for dyr, _, files in os.walk("."): + harness = [file for file in files if file.endswith("_harness.c")] + if harness and "Makefile" in files: + subprocess.run(["make", "cbmc-batch.yaml"], + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + cwd=os.path.abspath(dyr), + check=True) + +if __name__ == '__main__': + remove_cbmc_yaml_files() + create_cbmc_yaml_files() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_common_makefile.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_common_makefile.py new file mode 100755 index 000000000..efcf1db8d --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_common_makefile.py @@ -0,0 +1,240 @@ +#!/usr/bin/env python3 +# +# Generation of common Makefile 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. + +from pprint import pprint +import json +import sys +import re +import os +import argparse + +def cleanup_whitespace(string): + return re.sub('\s+', ' ', string.strip()) + +################################################################ +# Operating system specific values + +platform_definitions = { + "linux": { + "platform": "linux", + "separator": "/", + "define": "-D", + "include": "-I", + }, + "macos": { + "platform": "darwin", + "separator": "/", + "define": "-D", + "include": "-I", + }, + "windows": { + "platform": "win32", + "separator": "\\", + "define": "/D", + "include": "/I", + }, +} + + +def default_platform(): + for platform, definition in platform_definitions.items(): + if sys.platform == definition["platform"]: + return platform + return "linux" + + +def patch_path_separator(opsys, string): + from_separator = '/' + to_separator = platform_definitions[opsys]["separator"] + + def escape_separator(string): + return string.split(from_separator + from_separator) + + def change_separator(string): + return string.replace(from_separator, to_separator) + + return from_separator.join([change_separator(escaped) + for escaped in escape_separator(string)]) + +def patch_compile_output(opsys, line, key, value): + if opsys != "windows": + return line + + if key in ["COMPILE_ONLY", "COMPILE_LINK"] and value is not None: + if value[-1] == '/Fo': + return re.sub('/Fo\s+', '/Fo', line) + if value[-1] == '/Fe': + return re.sub('/Fe\s+', '/Fe', line) + return line + +################################################################ +# Argument parsing +# + +def get_arguments(): + parser = argparse.ArgumentParser() + parser.add_argument( + "--system", + metavar="OS", + choices=platform_definitions, + default=str(default_platform()), + help="Generate makefiles for operating system OS" + ) + return parser.parse_args() + +################################################################ +# Variable definitions +# +# JSON files give variable definitions for common, operating system, +# and harness specfic values +# + +def read_variable_definitions(filename): + variable = {} + with open(filename) as _file: + for key, values in json.load(_file).items(): + variable[cleanup_whitespace(key)] = [cleanup_whitespace(value) + for value in values] + return variable + +def find_definition_once(key, defines, prefix=None): + + # Try looking up key with and without prefix + prefix = "{}_".format(prefix.rstrip('_')) if prefix else "" + key2 = key[len(prefix):] if key.startswith(prefix) else prefix + key + + for _key in [key, key2]: + _value = defines.get(_key) + if _value is not None: + return _value + + return None + +def find_definition(key, defines): + common_defines, opsys_defines, harness_defines = defines + return (find_definition_once(key, harness_defines, "H") or + find_definition_once(key, opsys_defines, "O") or + find_definition_once(key, common_defines, "C")) + +################################################################ +# Makefile generation + +def construct_definition(opsys, key_prefix, value_prefix, key, definitions): + values = definitions.get(key) + if not values: + return "" + if key in ["INC", "DEF"]: + values = [patch_path_separator(opsys, value) + for value in values] + lines = ["\t{}{} \\".format(value_prefix, value) for value in values] + return "{}_{} = \\\n{}\n\t# empty\n".format(key_prefix, + key, + '\n'.join(lines)) + +def write_define(opsys, define, defines, makefile): + value = find_definition(define, defines) + if value: + if define in ["FREERTOS", "PROOFS"]: + value = os.path.abspath(value[0]) + makefile.write("{} = {}\n".format(define, value)) + +def write_common_defines(opsys, defines, makefile): + common_defines, opsys_defines, harness_defines = defines + + for key_prefix, defines in zip(["C", "O", "H"], + [common_defines, + opsys_defines, + harness_defines]): + for value_prefix, key in zip([platform_definitions[opsys]["include"], + platform_definitions[opsys]["define"], + "", ""], + ["INC", "DEF", "OPT", "CBMCFLAGS"]): + define = construct_definition(opsys, + key_prefix, value_prefix, + key, defines) + if define: + makefile.write(define + "\n") + + +def write_makefile(opsys, template, defines, makefile): + with open(template) as _template: + for line in _template: + line = patch_path_separator(opsys, line) + keys = re.findall('@(\w+)@', line) + values = [find_definition(key, defines) for key in keys] + for key, value in zip(keys, values): + if value is not None: + line = line.replace('@{}@'.format(key), " ".join(value)) + line = patch_compile_output(opsys, line, key, value) + makefile.write(line) + +def write_cbmcbatchyaml_target(opsys, _makefile): + target = """ +################################################################ +# Build configuration file to run cbmc under cbmc-batch in CI + +define encode_options +'=$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')=' +endef + +cbmc-batch.yaml: + @echo "Building $@" + @$(RM) $@ + @echo "jobos: ubuntu16" >> $@ + @echo "cbmcflags: $(call encode_options,$(CBMCFLAGS) --unwinding-assertions)" >> $@ + @echo "goto: $(ENTRY).goto" >> $@ + @echo "expected: $(H_EXPECTED)" >> $@ + +################################################################ +""" + if opsys != "windows": + _makefile.write(target) + +def makefile_from_template(opsys, template, defines, makefile="Makefile"): + with open(makefile, "w") as _makefile: + write_define(opsys, "FREERTOS", defines, _makefile) + write_define(opsys, "PROOFS", defines, _makefile) + write_common_defines(opsys, defines, _makefile) + write_makefile(opsys, template, defines, _makefile) + write_cbmcbatchyaml_target(opsys, _makefile) + +################################################################ +# Main + +def main(): + args = get_arguments() + + common_defines = read_variable_definitions("MakefileCommon.json") + opsys_defines = read_variable_definitions("MakefileWindows.json" + if args.system == "windows" + else "MakefileLinux.json") + harness_defines = {} + + makefile_from_template(args.system, + "Makefile.template", + (common_defines, opsys_defines, harness_defines), + "Makefile.common") + +if __name__ == "__main__": + main() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_configuration_directories.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_configuration_directories.py new file mode 100755 index 000000000..9e006e9ed --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_configuration_directories.py @@ -0,0 +1,163 @@ +#!/usr/bin/env python3 +# +# Creating the CBMC proofs from Configurations.json. +# +# 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 collections +import json +import logging +import os +import pathlib +import shutil +import textwrap + +from make_proof_makefiles import load_json_config_file + +LOGGER = logging.getLogger("ComputeConfigurations") + +def prolog(): + return textwrap.dedent("""\ + This script Generates Makefile.json from Configrations.json. + + Starting in the current directory, it walks down every subdirectory + looking for Configurations.json files. Every found Configurations.json + file is assumed to look similar to the following format: + + { + "ENTRY": "ARPProcessPacket", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/lib/FreeRTOS-Plus-TCP/source/FreeRTOS_ARP.goto" + ], + "DEF": + [ + {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]}, + {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]} + ] + } + + The format is mainly taken from the Makefile.json files. + The only difference is that it expects a list of json object in the DEF + section. This script will generate a Makefile.json in a subdirectory and + copy the harness to each subdirectory. + The key is later taken as the name for the configuration subdirectory + prexied by 'config_'. + + So for the above script, we get two subdirectories: + -config_disableClashDetection + -config_enableClashDetection + + As an example, the resulting Makefile.json for the + config_disableClashDetection directory will be: + + { + "ENTRY": "ARPProcessPacket", + "CBMCFLAGS": [ + "--unwind 1", + "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17", + "--nondet-static" + ], + "OBJS": [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/lib/FreeRTOS-Plus-TCP/source/FreeRTOS_ARP.goto" + ], + "DEF": [ + "ipconfigARP_USE_CLASH_DETECTION=0" + ] + } + + These Makefile.json files then can be turned into Makefiles for running + the proof by executing the make-proof-makefiles.py script. + """) + + +def process(folder, files): + json_content = load_json_config_file(os.path.join(folder, + "Configurations.json")) + try: + def_list = json_content["DEF"] + except KeyError: + LOGGER.error("Expected DEF as key in a Configurations.json files.") + return + for config in def_list: + logging.debug(config) + try: + configname = [name for name in config.keys() + if name != "EXPECTED"][0] + configbody = config[configname] + except (AttributeError, IndexError) as e: + LOGGER.error(e) + LOGGER.error(textwrap.dedent("""\ + The expected layout for an entry in the Configurations.json + file is a dictonary. Here is an example of the expected format: + + "DEF": + [ + {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]}, + {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]} + ] + """)) + LOGGER.error("The offending entry is %s", config) + return + new_config_folder = os.path.join(folder, "config_" + configname) + pathlib.Path(new_config_folder).mkdir(exist_ok=True, parents=True) + harness_copied = False + for file in files: + if file.endswith("harness.c"): + shutil.copy(os.path.join(folder, file), + os.path.join(new_config_folder, file)) + harness_copied = True + + if not harness_copied: + LOGGER.error("Could not find a harness in folder %s.", folder) + LOGGER.error("This folder is not processed do the end!") + return + # The order of keys must be maintained as otherwise the + # make_proof_makefiles script might fail. + current_config = collections.OrderedDict(json_content) + current_config["DEF"] = configbody + if "EXPECTED" in config.keys(): + current_config["EXPECTED"] = config["EXPECTED"] + else: + current_config["EXPECTED"] = True + with open(os.path.join(new_config_folder, "Makefile.json"), + "w") as output_file: + json.dump(current_config, output_file, indent=2) + + +def main(): + for fldr, _, fyles in os.walk("."): + if "Configurations.json" in fyles: + process(fldr, fyles) + + +if __name__ == '__main__': + logging.basicConfig(format="{script}: %(levelname)s %(message)s".format( + script=os.path.basename(__file__))) + main() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_proof_makefiles.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_proof_makefiles.py new file mode 100755 index 000000000..846942ee4 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_proof_makefiles.py @@ -0,0 +1,416 @@ +#!/usr/bin/env python3 +# +# Generation of Makefiles 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 argparse +import ast +import collections +import json +import logging +import operator +import os +import os.path +import platform +import re +import sys +import textwrap +import traceback + + +# ______________________________________________________________________________ +# Compatibility between different python versions +# `````````````````````````````````````````````````````````````````````````````` + +# Python 3 doesn't have basestring +try: + basestring +except NameError: + basestring = str + +# ast.Num was deprecated in python 3.8 +_plat = platform.python_version().split(".") +if _plat[0] == "3" and int(_plat[1]) > 7: + ast_num = ast.Constant +else: + ast_num = ast.Num +# ______________________________________________________________________________ + + +def prolog(): + return textwrap.dedent("""\ + This script generates Makefiles that can be used either on Windows (with + NMake) or Linux (with GNU Make). The Makefiles consist only of variable + definitions; they are intended to be used with a common Makefile that + defines the actual rules. + + The Makefiles are generated from JSON specifications. These are simple + key-value dicts, but can contain variables and computation, as + well as comments (lines whose first character is "#"). If the + JSON file contains the following information: + + { + # 'T was brillig, and the slithy toves + "FOO": "BAR", + "BAZ": "{FOO}", + + # Did gyre and gimble in the wabe; + "QUUX": 30 + "XYZZY": "__eval 5 if {QUUZ} < 5 else min({QUUX}, 60)" + } + + then the resulting Makefile will look like + + H_FOO = BAR + H_BAZ = BAR + H_QUUX = 30 + H_XYZZY = 30 + + The language used for evaluation is highly restricted; arbitrary + python is not allowed. JSON values that are lists will be + joined with whitespace: + + { "FOO": ["BAR", "BAZ", "QUX"] } + + -> + + H_FOO = BAR BAZ QUX + + As a special case, if a key is equal to "DEF", "INC" (and maybe more, + read the code) the list of values is treated as a list of defines or + include paths. Thus, they have -D or /D, or -I or /I, prepended to them + as appropriate for the platform. + + + { "DEF": ["DEBUG", "FOO=BAR"] } + + on Linux -> + + H_DEF = -DDEBUG -DFOO=BAR + + Pathnames are written with a forward slash in the JSON file. In + each value, all slashes are replaced with backslashes if + generating Makefiles for Windows. If you wish to generate a + slash even on Windows, use two slashes---that will be changed + into a single forward slash on both Windows and Linux. + + { + "INC": [ "my/cool/directory" ], + "DEF": [ "HALF=//2" ] + } + + On Windows -> + + H_INC = /Imy\cool\directory + H_DEF = /DHALF=/2 + + When invoked, this script walks the directory tree looking for files + called "Makefile.json". It reads that file and dumps a Makefile in that + same directory. We assume that this script lives in the same directory + as a Makefile called "Makefile.common", which contains the actual Make + rules. The final line of each of the generated Makefiles will be an + include statement, including Makefile.common. + """) + +def load_json_config_file(file): + with open(file) as handle: + lines = handle.read().splitlines() + no_comments = "\n".join([line for line in lines + if line and not line.lstrip().startswith("#")]) + try: + data = json.loads(no_comments, + object_pairs_hook=collections.OrderedDict) + except json.decoder.JSONDecodeError: + traceback.print_exc() + logging.error("parsing file %s", file) + sys.exit(1) + return data + + +def dump_makefile(dyr, system): + data = load_json_config_file(os.path.join(dyr, "Makefile.json")) + + makefile = collections.OrderedDict() + + # Makefile.common expects a variable called OBJS_EXCEPT_HARNESS to be + # set to a list of all the object files except the harness. + if "OBJS" not in data: + logging.error( + "Expected a list of object files in %s/Makefile.json" % dyr) + exit(1) + makefile["OBJS_EXCEPT_HARNESS"] = " ".join( + o for o in data["OBJS"] if not o.endswith("_harness.goto")) + + so_far = collections.OrderedDict() + for name, value in data.items(): + if isinstance(value, list): + new_value = [] + for item in value: + new_value.append(compute(item, so_far, system, name, dyr, True)) + makefile[name] = " ".join(new_value) + else: + makefile[name] = compute(value, so_far, system, name, dyr) + + if (("EXPECTED" not in makefile.keys()) or + str(makefile["EXPECTED"]).lower() == "true"): + makefile["EXPECTED"] = "SUCCESSFUL" + elif str(makefile["EXPECTED"]).lower() == "false": + makefile["EXPECTED"] = "FAILURE" + makefile = ["H_%s = %s" % (k, v) for k, v in makefile.items()] + + # Deal with the case of a harness being nested several levels under + # the top-level proof directory, where the common Makefile lives + common_dir_path = "..%s" % _platform_choices[system]["path-sep"] + common_dir_path = common_dir_path * len(dyr.split(os.path.sep)[1:]) + + with open(os.path.join(dyr, "Makefile"), "w") as handle: + handle.write(("""{contents} + +{include} {common_dir_path}Makefile.common""").format( + contents="\n".join(makefile), + include=_platform_choices[system]["makefile-inc"], + common_dir_path=common_dir_path)) + + +def compute(value, so_far, system, key, harness, appending=False): + if not isinstance(value, (basestring, float, int)): + logging.error(wrap("""\ + in file %s, the key '%s' has value '%s', + which is of the wrong type (%s)"""), + os.path.join(harness, "Makefile.json"), key, + str(value), str(type(value))) + exit(1) + + value = str(value) + try: + var_subbed = value.format(**so_far) + except KeyError as e: + logging.error(wrap("""\ + in file %s, the key '%s' has value '%s', which + contains the variable %s, but that variable has + not previously been set in the file"""), + os.path.join(harness, "Makefile.json"), key, + value, str(e)) + exit(1) + + if var_subbed[:len("__eval")] != "__eval": + tmp = re.sub("//", "__DOUBLE_SLASH__", var_subbed) + tmp = re.sub("/", _platform_choices[system]["path-sep-re"], tmp) + evaluated = re.sub("__DOUBLE_SLASH__", "/", tmp) + else: + to_eval = var_subbed[len("__eval"):].strip() + logging.debug("About to evaluate '%s'", to_eval) + evaluated = eval_expr(to_eval, + os.path.join(harness, "Makefile.json"), + key, value) + + if key == "DEF": + final_value = "%s%s" % (_platform_choices[system]["define"], + evaluated) + elif key == "INC": + final_value = "%s%s" % (_platform_choices[system]["include"], + evaluated) + else: + final_value = evaluated + + # Allow this value to be used for future variable substitution + if appending: + try: + so_far[key] = "%s %s" % (so_far[key], final_value) + except KeyError: + so_far[key] = final_value + logging.debug("Appending final value '%s' to key '%s'", + final_value, key) + else: + so_far[key] = final_value + logging.info("Key '%s' set to final value '%s'", key, final_value) + + return final_value + + +def eval_expr(expr_string, harness, key, value): + """ + Safe evaluation of purely arithmetic expressions + """ + try: + tree = ast.parse(expr_string, mode="eval").body + except SyntaxError: + traceback.print_exc() + logging.error(wrap("""\ + in file %s at key '%s', value '%s' contained the expression + '%s' which is an invalid expression"""), harness, key, + value, expr_string) + exit(1) + + def eval_single_node(node): + logging.debug(node) + if isinstance(node, ast_num): + return node.n + # We're only doing IfExp, which is Python's ternary operator + # (i.e. it's an expression). NOT If, which is a statement. + if isinstance(node, ast.IfExp): + # Let's be strict and only allow actual booleans in the guard + guard = eval_single_node(node.test) + if guard is not True and guard is not False: + logging.error(wrap("""\ + in file %s at key '%s', there was an invalid guard + for an if statement."""), harness, key) + exit(1) + if guard: + return eval_single_node(node.body) + return eval_single_node(node.orelse) + if isinstance(node, ast.Compare): + left = eval_single_node(node.left) + # Don't allow expressions like (a < b) < c + right = eval_single_node(node.comparators[0]) + op = eval_single_node(node.ops[0]) + return op(left, right) + if isinstance(node, ast.BinOp): + left = eval_single_node(node.left) + right = eval_single_node(node.right) + op = eval_single_node(node.op) + return op(left, right) + if isinstance(node, ast.Call): + valid_calls = { + "max": max, + "min": min, + } + if node.func.id not in valid_calls: + logging.error(wrap("""\ + in file %s at key '%s', there was an invalid + call to %s()"""), harness, key, node.func.id) + exit(1) + left = eval_single_node(node.args[0]) + right = eval_single_node(node.args[1]) + return valid_calls[node.func.id](left, right) + try: + return { + ast.Eq: operator.eq, + ast.NotEq: operator.ne, + ast.Lt: operator.lt, + ast.LtE: operator.le, + ast.Gt: operator.gt, + ast.GtE: operator.ge, + + ast.Add: operator.add, + ast.Sub: operator.sub, + ast.Mult: operator.mul, + # Use floordiv (i.e. //) so that we never need to + # cast to an int + ast.Div: operator.floordiv, + }[type(node)] + except KeyError: + logging.error(wrap("""\ + in file %s at key '%s', there was expression that + was impossible to evaluate"""), harness, key) + exit(1) + + return eval_single_node(tree) + + +_platform_choices = { + "linux": { + "platform": "linux", + "path-sep": "/", + "path-sep-re": "/", + "define": "-D", + "include": "-I", + "makefile-inc": "include", + }, + "windows": { + "platform": "win32", + "path-sep": "\\", + "path-sep-re": re.escape("\\"), + "define": "/D", + "include": "/I", + "makefile-inc": "!INCLUDE", + }, +} +# Assuming macos is the same as linux +_mac_os = dict(_platform_choices["linux"]) +_mac_os["platform"] = "darwin" +_platform_choices["macos"] = _mac_os + + +def default_platform(): + for arg_string, os_data in _platform_choices.items(): + if sys.platform == os_data["platform"]: + return arg_string + return "linux" + + +_args = [{ + "flags": ["-s", "--system"], + "metavar": "OS", + "choices": _platform_choices, + "default": str(default_platform()), + "help": textwrap.dedent("""\ + which operating system to generate makefiles for. + Defaults to the current platform (%(default)s); + choices are {choices}""").format( + choices="[%s]" % ", ".join(_platform_choices)), +}, { + "flags": ["-v", "--verbose"], + "help": "verbose output", + "action": "store_true", +}, { + "flags": ["-w", "--very-verbose"], + "help": "very verbose output", + "action": "store_true", + }] + + +def get_args(): + pars = argparse.ArgumentParser( + description=prolog(), + formatter_class=argparse.RawDescriptionHelpFormatter) + for arg in _args: + flags = arg.pop("flags") + pars.add_argument(*flags, **arg) + return pars.parse_args() + + +def set_up_logging(args): + fmt = "{script}: %(levelname)s %(message)s".format( + script=os.path.basename(__file__)) + if args.very_verbose: + logging.basicConfig(format=fmt, level=logging.DEBUG) + elif args.verbose: + logging.basicConfig(format=fmt, level=logging.INFO) + else: + logging.basicConfig(format=fmt, level=logging.WARNING) + +def wrap(string): + return re.sub(r"\s+", " ", re.sub("\n", " ", string)) + +def main(): + args = get_args() + set_up_logging(args) + + for root, _, fyles in os.walk("."): + if "Makefile.json" in fyles: + dump_makefile(root, args.system) + + +if __name__ == "__main__": + main() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_remove_makefiles.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_remove_makefiles.py new file mode 100755 index 000000000..12d0c72f1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_remove_makefiles.py @@ -0,0 +1,48 @@ +#!/usr/bin/env python3 +# +# Removing the generated Makefiles and cbmc-batch.yaml files. +# +# 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 + +from make_cbmc_batch_files import remove_cbmc_yaml_files + +def main(): + try: + os.remove("Makefile.common") + except FileNotFoundError: + pass + + for root, _, files in os.walk("."): + # We do not want to remove hand-written Makefiles, so + # only remove Makefiles that are in the same directory as + # a Makefile.json. Such Makefiles are generated from the + # JSON file. + if "Makefile.json" in files: + try: + os.remove(os.path.join(root, "Makefile")) + except FileNotFoundError: + pass + +if __name__ == "__main__": + remove_cbmc_yaml_files() + main() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_type_header_files.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_type_header_files.py new file mode 100755 index 000000000..a8ac66384 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_type_header_files.py @@ -0,0 +1,162 @@ +#!/usr/bin/env python3 +# +# Compute type header files for c modules +# +# 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 argparse +import logging +import os +import re +import shutil +import subprocess +import sys +from tempfile import TemporaryDirectory + +def epilog(): + return """\ + This program dumps a header file containing the types and macros + contained in the C file passed as input. It uses `goto-instrument` + from the CBMC tool suite instead of the preprocessor, to dump types + and other constructs as well as preprocessor directives. + + This program should be used in cases where types or macros declared + for internal use in a C file use are needed to write a test harness + or CBMC proof. The intention is that the build process will run + this program to dump the header file, and the proof will #include + the header. + """ + +_DEFINE_REGEX_HEADER = re.compile(r"\s*#\s*define\s*([\w]+)") + + +def get_module_name(fyle): + base = os.path.basename(fyle) + return base.split(".")[0] + + +def collect_defines(fyle): + collector_result = "" + continue_define = False + in_potential_def_scope = "" + potential_define = False + potential_define_confirmed = False + with open(fyle) as in_file: + for line in in_file: + matched = _DEFINE_REGEX_HEADER.match(line) + if line.strip().startswith("#if"): + potential_define = True + in_potential_def_scope += line + elif line.strip().startswith("#endif") and potential_define: + if potential_define_confirmed: + in_potential_def_scope += line + collector_result += in_potential_def_scope + in_potential_def_scope = "" + potential_define = False + potential_define_confirmed = False + elif matched and potential_define: + potential_define_confirmed = True + in_potential_def_scope += line + elif matched or continue_define: + continue_define = line.strip("\n").endswith("\\") + collector_result += line + elif potential_define: + in_potential_def_scope += line + return collector_result + + +def make_header_file(goto_binary, fyle, target_folder): + fyle = os.path.normpath(fyle) + with TemporaryDirectory() as tmpdir: + module = get_module_name(fyle) + header_file = "{}_datastructure.h".format(module) + + drop_header_cmd = ["goto-instrument", + "--dump-c-type-header", + module, + goto_binary, + header_file] + res = subprocess.run(drop_header_cmd, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + universal_newlines=True, + cwd=tmpdir) + if res.returncode: + logging.error("Dumping type header for file '%s' failed", fyle) + logging.error("The command `%s` returned %s", + drop_header_cmd, + res.stdout) + logging.error("The return code is %d", int(res.returncode)) + sys.exit(1) + + header = os.path.normpath(os.path.join(tmpdir, header_file)) + collected = collect_defines(fyle) + logging.debug("Dumping the following header file to '%s':\n%s\n" + "// END GENERATED HEADER FILE", header, collected) + with open(header, "a") as out: + print(collected, file=out) + + target_file = os.path.normpath(os.path.join(target_folder, header_file)) + shutil.move(header, target_file) + + +_ARGS = [{ + "flags": ["--c-file"], + "metavar": "F", + "help": "source file to extract types and headers from", + "required": True +}, { + "flags": ["--binary"], + "metavar": "B", + "help": "file compiled from the source file with CBMC's goto-cc compiler", + "required": True +}, { + "flags": ["--out-dir"], + "metavar": "D", + "help": ("directory to write the generated header file to " + "(default: %(default)s)"), + "default": os.path.abspath(os.getcwd()), +}, { + "flags": ["--verbose", "-v"], + "help": "verbose output", + "action": "store_true" +}] + + +if __name__ == '__main__': + pars = argparse.ArgumentParser( + epilog=epilog(), + description="Dump a C file's types and macros to a separate file") + for arg in _ARGS: + flags = arg.pop("flags") + pars.add_argument(*flags, **arg) + + args = pars.parse_args() + + fmt = "{script}: %(levelname)s %(message)s".format( + script=os.path.basename(__file__)) + if args.verbose: + logging.basicConfig(format=fmt, level=logging.DEBUG) + else: + logging.basicConfig(format=fmt, level=logging.INFO) + + make_header_file(args.binary, args.c_file, args.out_dir) diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ninja.py b/FreeRTOS-Plus/Test/CBMC/proofs/ninja.py new file mode 100755 index 000000000..4bfd3c8d4 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ninja.py @@ -0,0 +1,219 @@ +#!/usr/bin/env python3 + +""" +Write a ninja build file to generate reports for cbmc proofs. + +Given a list of folders containing cbmc proofs, write a ninja build +file the generate reports for these proofs. The list of folders may +be given on the command line, in a json file, or found in the file +system. +""" + +# Add task pool + +import sys +import os +import platform +import argparse +import json + +################################################################ +# The command line parser + +def argument_parser(): + """Return the command line parser.""" + + parser = argparse.ArgumentParser( + description='Generate ninja build file for cbmc proofs.', + epilog=""" + Given a list of folders containing cbmc proofs, write a ninja build + file the generate reports for these proofs. The list of folders may + be given on the command line, in a json file, or found in the file + system. + In the json file, there should be a dict mapping the key "proofs" + to a list of folders containing proofs. + The file system, all folders folders under the current directory + containing a file named 'cbmc-batch.yaml' is considered a + proof folder. + This script assumes that the proof is driven by a Makefile + with targets goto, cbmc, coverage, property, and report. + This script does not work with Windows and Visual Studio. + """ + ) + parser.add_argument('folders', metavar='PROOF', nargs='*', + help='Folder containing a cbmc proof') + parser.add_argument('--proofs', metavar='JSON', + help='Json file listing folders containing cbmc proofs') + return parser + +################################################################ +# The list of folders containing proofs +# +# The list of folders will be taken from +# 1. the list PROOFS defined here or +# 2. the command line +# 3. the json file specified on the command line containing a +# dict mapping the key JSON_KEY to a list of folders +# 4. the folders below the current directory containing +# a file named FS_KEY +# + +PROOFS = [ +] + +JSON_KEY = 'proofs' +FS_KEY = 'cbmc-batch.yaml' + +def find_proofs_in_json_file(filename): + """Read the list of folders containing proofs from a json file.""" + + if not filename: + return [] + try: + with open(filename) as proofs: + return json.load(proofs)[JSON_KEY] + except (FileNotFoundError, KeyError): + raise UserWarning("Can't find key {} in json file {}".format(JSON_KEY, filename)) + except json.decoder.JSONDecodeError: + raise UserWarning("Can't parse json file {}".format(filename)) + +def find_proofs_in_filesystem(): + """Locate the folders containing proofs in the filesystem.""" + + proofs = [] + for root, _, files in os.walk('.'): + if FS_KEY in files: + proofs.append(os.path.normpath(root)) + return proofs + +################################################################ +# The strings used to write sections of the ninja file + +NINJA_RULES = """ +################################################################ +# task pool to force sequential builds of goto binaries + +pool goto_pool + depth = 1 + +################################################################ +# proof target rules + +rule build_goto + command = make -C ${folder} goto + pool = goto_pool + +rule build_cbmc + command = make -C ${folder} cbmc + +rule build_coverage + command = make -C ${folder} coverage + +rule build_property + command = make -C ${folder} property + +rule build_report + command = make -C ${folder} report + +rule clean_folder + command = make -C ${folder} clean + +rule veryclean_folder + command = make -C ${folder} veryclean + +rule open_proof + command = open ${folder}/html/index.html + +""" + +NINJA_BUILDS = """ +################################################################ +# {folder} proof targets + +build {folder}/{entry}.goto: build_goto + folder={folder} + +build {folder}/cbmc.txt: build_cbmc {folder}/{entry}.goto + folder={folder} + +build {folder}/coverage.xml: build_coverage {folder}/{entry}.goto + folder={folder} + +build {folder}/property.xml: build_property {folder}/{entry}.goto + folder={folder} + +build {folder}/html/index.html: build_report {folder}/{entry}.goto {folder}/cbmc.txt {folder}/coverage.xml {folder}/property.xml + folder={folder} + +build clean_{folder}: clean_folder + folder={folder} + +build veryclean_{folder}: veryclean_folder + folder={folder} + +build open_{folder}: open_proof + folder={folder} + +build {folder}: phony {folder}/html/index.html + +default {folder} + +""" + +NINJA_GLOBALS = """ +################################################################ +# global targets + +build clean: phony {clean_targets} + +build veryclean: phony {veryclean_targets} + +build open: phony {open_targets} +""" + +################################################################ +# The main function + +def get_entry(folder): + """Find the name of the proof in the proof Makefile.""" + + with open('{}/Makefile'.format(folder)) as makefile: + for line in makefile: + if line.strip().lower().startswith('entry'): + return line[line.find('=')+1:].strip() + if line.strip().lower().startswith('h_entry'): + return line[line.find('=')+1:].strip() + raise UserWarning("Can't find ENTRY in {}/Makefile".format(folder)) + +def write_ninja_build_file(): + """Write a ninja build file to generate proof results.""" + + if platform.system().lower() == 'windows': + print("This script does not run on Windows.") + sys.exit() + + args = argument_parser().parse_args() + + proofs = (PROOFS or + args.folders or + find_proofs_in_json_file(args.proofs) or + find_proofs_in_filesystem()) + + with open('build.ninja', 'w') as ninja: + ninja.write(NINJA_RULES) + for proof in proofs: + entry = get_entry(proof) + ninja.write(NINJA_BUILDS.format(folder=proof, entry=entry)) + targets = lambda kind, folders: ' '.join( + ['{}_{}'.format(kind, folder) for folder in folders] + ) + ninja.write(NINJA_GLOBALS.format( + clean_targets=targets('clean', proofs), + veryclean_targets=targets('veryclean', proofs), + open_targets=targets('open', proofs) + )) + +################################################################ + +if __name__ == "__main__": + write_ninja_build_file() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json new file mode 100644 index 000000000..9ad1ef4e9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json @@ -0,0 +1,21 @@ +{ + "ENTRY": "ProcessIPPacket", + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto" + ], + "DEF": + [ + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c new file mode 100644 index 000000000..def244a51 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c @@ -0,0 +1,29 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" + +/* proof is done separately */ +BaseType_t xProcessReceivedTCPPacket(NetworkBufferDescriptor_t *pxNetworkBuffer) { } + +/* proof is done separately */ +BaseType_t xProcessReceivedUDPPacket(NetworkBufferDescriptor_t *pxNetworkBuffer, uint16_t usPort) { } + +/* This proof was done before. Hence we assume it to be correct here. */ +void vARPRefreshCacheEntry( const MACAddress_t * pxMACAddress, const uint32_t ulIPAddress ) { } + +eFrameProcessingResult_t publicProcessIPPacket( IPPacket_t * const pxIPPacket, NetworkBufferDescriptor_t * const pxNetworkBuffer); + +void harness() { + + NetworkBufferDescriptor_t * const pxNetworkBuffer = malloc(sizeof(NetworkBufferDescriptor_t)); + /* Pointer to the start of the Ethernet frame. It should be able to access the whole Ethernet frame.*/ + pxNetworkBuffer->pucEthernetBuffer = malloc(ipTOTAL_ETHERNET_FRAME_SIZE); + /* Minimum length of the pxNetworkBuffer->xDataLength is at least the size of the IPPacket_t. */ + __CPROVER_assume(pxNetworkBuffer->xDataLength >= sizeof(IPPacket_t) && pxNetworkBuffer->xDataLength <= ipTOTAL_ETHERNET_FRAME_SIZE); + IPPacket_t * const pxIPPacket = malloc(sizeof(IPPacket_t)); + publicProcessIPPacket(pxIPPacket, pxNetworkBuffer); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json new file mode 100644 index 000000000..901a72729 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json @@ -0,0 +1,31 @@ +{ + "ENTRY": "ProcessReceivedTCPPacket", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvTCPSendRepeated.0:13", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto" + ], + "INSTFLAGS": + [ + "--remove-function-body prvSingleStepTCPHeaderOptions", + "--remove-function-body prvCheckOptions", + "--remove-function-body prvTCPPrepareSend", + "--remove-function-body prvTCPReturnPacket", + "--remove-function-body prvTCPHandleState" + ], + "DEF": + [ + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c new file mode 100644 index 000000000..bf84ecf05 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c @@ -0,0 +1,62 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_TCP_IP.h" +#include "FreeRTOS_Stream_Buffer.h" + +/* This proof assumes FreeRTOS_socket, pxTCPSocketLookup and +pxGetNetworkBufferWithDescriptor are implemented correctly. + +It also assumes prvSingleStepTCPHeaderOptions, prvCheckOptions, prvTCPPrepareSend, +prvTCPHandleState and prvTCPReturnPacket are correct. These functions are +proved to be correct separately. */ + +/* Implementation of safe malloc */ +void *safeMalloc(size_t xWantedSize ){ + if(xWantedSize == 0){ + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +/* Abstraction of FreeRTOS_socket */ +Socket_t FreeRTOS_socket( BaseType_t xDomain, BaseType_t xType, BaseType_t xProtocol) { + return safeMalloc(sizeof(FreeRTOS_Socket_t)); +} + +/* Abstraction of pxTCPSocketLookup */ +FreeRTOS_Socket_t *pxTCPSocketLookup(uint32_t ulLocalIP, UBaseType_t uxLocalPort, uint32_t ulRemoteIP, UBaseType_t uxRemotePort) { + FreeRTOS_Socket_t * xRetSocket = safeMalloc(sizeof(FreeRTOS_Socket_t)); + if (xRetSocket) { + xRetSocket->u.xTCP.txStream = safeMalloc(sizeof(StreamBuffer_t)); + xRetSocket->u.xTCP.pxPeerSocket = safeMalloc(sizeof(StreamBuffer_t)); + } + return xRetSocket; +} + +/* Abstraction of pxGetNetworkBufferWithDescriptor */ +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + NetworkBufferDescriptor_t *pxNetworkBuffer = safeMalloc(sizeof(NetworkBufferDescriptor_t)); + if(pxNetworkBuffer) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(xRequestedSizeBytes); + __CPROVER_assume(pxNetworkBuffer->xDataLength == ipSIZE_OF_ETH_HEADER + sizeof(int32_t)); + } + return pxNetworkBuffer; +} + +void harness() { + NetworkBufferDescriptor_t *pxNetworkBuffer = safeMalloc(sizeof(NetworkBufferDescriptor_t)); + if (pxNetworkBuffer) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t)); + } + if (pxNetworkBuffer && pxNetworkBuffer->pucEthernetBuffer) { + xProcessReceivedTCPPacket(pxNetworkBuffer); + + } + +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json new file mode 100644 index 000000000..017f625f0 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json @@ -0,0 +1,23 @@ +{ + "ENTRY": "ProcessReceivedUDPPacket", + "MAX_RX_PACKETS":1, + "USE_LLMNR":1, + "USE_NBNS":1, + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_UDP_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto" + ], + "DEF": + [ + "ipconfigUDP_MAX_RX_PACKETS={MAX_RX_PACKETS}", + "ipconfigUSE_LLMNR={USE_LLMNR}", + "ipconfigUSE_NBNS={USE_NBNS}" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c new file mode 100644 index 000000000..0082e5d61 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c @@ -0,0 +1,46 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_TCP_IP.h" + +/*This proof assumes that pxUDPSocketLookup is implemented correctly. */ + +/* This proof was done before. Hence we assume it to be correct here. */ +void vARPRefreshCacheEntry(const MACAddress_t * pxMACAddress, const uint32_t ulIPAddress) { } + +/* This proof was done before. Hence we assume it to be correct here. */ +BaseType_t xIsDHCPSocket(Socket_t xSocket) { } + +/* This proof was done before. Hence we assume it to be correct here. */ +uint32_t ulDNSHandlePacket(NetworkBufferDescriptor_t *pxNetworkBuffer) { } + +/* Implementation of safe malloc */ +void *safeMalloc(size_t xWantedSize) { + if(xWantedSize == 0) { + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +/* Abstraction of pxUDPSocketLookup */ +FreeRTOS_Socket_t *pxUDPSocketLookup( UBaseType_t uxLocalPort ) { + return safeMalloc(sizeof(FreeRTOS_Socket_t)); +} + +void harness() { + NetworkBufferDescriptor_t *pxNetworkBuffer = safeMalloc(sizeof(NetworkBufferDescriptor_t)); + if(pxNetworkBuffer) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(UDPPacket_t)); + } + uint16_t usPort; + if (pxNetworkBuffer && pxNetworkBuffer->pucEthernetBuffer) { + xProcessReceivedUDPPacket(pxNetworkBuffer, usPort); + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/prepare.py b/FreeRTOS-Plus/Test/CBMC/proofs/prepare.py new file mode 100755 index 000000000..58f9903db --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/prepare.py @@ -0,0 +1,115 @@ +#!/usr/bin/env python3 +# +# Python script for preparing the code base 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 logging +import os +import sys +import textwrap +from subprocess import CalledProcessError + +from make_common_makefile import main as make_common_file +from make_configuration_directories import main as process_configurations +from make_proof_makefiles import main as make_proof_files +from make_cbmc_batch_files import create_cbmc_yaml_files + +CWD = os.getcwd() +sys.path.append(os.path.normpath(os.path.join(CWD, "..", "patches"))) + +#from compute_patch import create_patches +#from compute_patch import DirtyGitError +#from compute_patch import PatchCreationError +from patches_constants import HEADERS + +from compute_patch import find_all_defines +from compute_patch import manipulate_headerfile + +import patch + +PROOFS_DIR = os.path.dirname(os.path.abspath(__file__)) + +LOGGER = logging.getLogger("PrepareLogger") + +################################################################ + +def patch_headers(headers): + """Patch headers so we can define symbols on the command line. + + When building for CBMC, it is convenient to define symbols on the + command line and know that these definitions will override the + definitions of the same symbols in header files. + + The create_patches function takes a list of header files, searches + the Makefile.json files for symbols that will be defined in the + Makefiles, and creates patch files that protect the definition of + those symbols in header files with #ifndef/#endif. In this way, + command line definitions will override header file definitions. + + The create_patches function, however, depends on the fact that all + header files being modified are included in the top-level git + repository. This assumption is violated if header files live in + submodules. + + This function just updates the header files in place without + creating patch files. One potential vulnerability of this + function is that it could cause preexisting patch files to fail if + they patch a file being modified here. + """ + defines = find_all_defines() + for header in headers: + manipulate_headerfile(defines, header) + +################################################################ + +def build(): + process_configurations() + make_common_file() + make_proof_files() + try: + create_cbmc_yaml_files() + except CalledProcessError as e: + logging.error(textwrap.dedent("""\ + An error occured during cbmc-batch generation. + The error message is: {} + """.format(str(e)))) + exit(1) + + # Patch headers directly instead of creating patch files. + patch.patch() + patch_headers(HEADERS) + + #try: + # create_patches(HEADERS) + #except (DirtyGitError, PatchCreationError) as e: + # logging.error(textwrap.dedent("""\ + # An error occured during patch creation. + # The error message is: {} + # """.format(str(e)))) + # exit(1) + +################################################################ + +if __name__ == '__main__': + logging.basicConfig(format="{script}: %(levelname)s %(message)s".format( + script=os.path.basename(__file__))) + build() diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c b/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c new file mode 100644 index 000000000..6bcb9319a --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c @@ -0,0 +1,24 @@ +#define ensure_memory_is_valid( px, length ) (px != NULL) && __CPROVER_w_ok((px), length) + +/* Implementation of safe malloc which returns NULL if the requested size is 0. + Warning: The behavior of malloc(0) is platform dependent. + It is possible for malloc(0) to return an address without allocating memory.*/ +void *safeMalloc(size_t xWantedSize) { + return nondet_bool() ? malloc(xWantedSize) : NULL; +} + +/* Memory assignment for FreeRTOS_Socket_t */ +FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated () { + FreeRTOS_Socket_t *pxSocket = safeMalloc(sizeof(FreeRTOS_Socket_t)); + if (ensure_memory_is_valid(pxSocket, sizeof(FreeRTOS_Socket_t))) { + pxSocket->u.xTCP.rxStream = safeMalloc(sizeof(StreamBuffer_t)); + pxSocket->u.xTCP.txStream = safeMalloc(sizeof(StreamBuffer_t)); + pxSocket->u.xTCP.pxPeerSocket = safeMalloc(sizeof(FreeRTOS_Socket_t)); + } + return pxSocket; +} + +/* Memory assignment for FreeRTOS_Network_Buffer */ +NetworkBufferDescriptor_t * ensure_FreeRTOS_NetworkBuffer_is_allocated () { + return safeMalloc(sizeof(NetworkBufferDescriptor_t)); +} |