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/Test/VeriFast | |
| 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/Test/VeriFast')
31 files changed, 3959 insertions, 0 deletions
diff --git a/FreeRTOS/Test/VeriFast/Makefile b/FreeRTOS/Test/VeriFast/Makefile new file mode 100644 index 000000000..9e774f61a --- /dev/null +++ b/FreeRTOS/Test/VeriFast/Makefile @@ -0,0 +1,52 @@ +VERIFAST ?= verifast +VERIFAST_ARGS = -I include -c $(EXTRA_VERIFAST_ARGS) + +ifeq ($(NO_COVERAGE), 1) +check_coverage = cat +else +check_coverage = perl -pe \ + 'END { \ + if ($$status) { \ + print "Coverage regression failed: Expected $1 statements verified.\n"; \ + } \ + exit $$status; \ + } \ + $$status=/$1 statements verified/ ? 0 : 1;' +endif + +all: queue + +.PHONY: queue +queue: + @$(VERIFAST) $(VERIFAST_ARGS) queue/create.c | $(call check_coverage,317) + @$(VERIFAST) $(VERIFAST_ARGS) queue/prvCopyDataFromQueue.c | $(call check_coverage,301) + @$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/prvCopyDataToQueue.c | $(call check_coverage,329) + @$(VERIFAST) $(VERIFAST_ARGS) queue/prvIsQueueEmpty.c | $(call check_coverage,282) + @$(VERIFAST) $(VERIFAST_ARGS) queue/prvIsQueueFull.c | $(call check_coverage,282) + @$(VERIFAST) $(VERIFAST_ARGS) queue/prvLockQueue.c | $(call check_coverage,283) + @$(VERIFAST) $(VERIFAST_ARGS) queue/prvUnlockQueue.c | $(call check_coverage,297) + @$(VERIFAST) $(VERIFAST_ARGS) queue/uxQueueMessagesWaiting.c | $(call check_coverage,285) + @$(VERIFAST) $(VERIFAST_ARGS) queue/uxQueueSpacesAvailable.c | $(call check_coverage,283) + @$(VERIFAST) $(VERIFAST_ARGS) queue/vQueueDelete.c | $(call check_coverage,280) + @$(VERIFAST) $(VERIFAST_ARGS) queue/xQueueGenericSend.c | $(call check_coverage,328) + @$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/xQueueGenericSendFromISR.c | $(call check_coverage,310) + @$(VERIFAST) $(VERIFAST_ARGS) queue/xQueueIsQueueEmptyFromISR.c | $(call check_coverage,280) + @$(VERIFAST) $(VERIFAST_ARGS) queue/xQueueIsQueueFullFromISR.c | $(call check_coverage,280) + @$(VERIFAST) $(VERIFAST_ARGS) queue/xQueuePeek.c | $(call check_coverage,328) + @$(VERIFAST) $(VERIFAST_ARGS) queue/xQueuePeekFromISR.c | $(call check_coverage,293) + @$(VERIFAST) $(VERIFAST_ARGS) queue/xQueueReceive.c | $(call check_coverage,330) + @$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/xQueueReceiveFromISR.c | $(call check_coverage,307) + +.PHONY: proof_changes +proof_changes: + @git grep "if[n]*def VERIFAST" | cut -f 3- -d ' ' | sort | uniq + +GIT?=git +NO_CHANGE_CHECKOUT_DIR=no-change-check-freertos-kernel +NO_CHANGE_EXPECTED_HASH=587a83d6476 +.PHONY: synced_with_source_check +synced_with_source_check: + @rm -rf $(NO_CHANGE_CHECKOUT_DIR) + @$(GIT) clone https://github.com/FreeRTOS/FreeRTOS-Kernel.git $(NO_CHANGE_CHECKOUT_DIR) + @cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH) queue.c + @cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH) include/queue.h diff --git a/FreeRTOS/Test/VeriFast/README.md b/FreeRTOS/Test/VeriFast/README.md new file mode 100644 index 000000000..f0deecdfc --- /dev/null +++ b/FreeRTOS/Test/VeriFast/README.md @@ -0,0 +1,122 @@ +# FreeRTOS VeriFast proofs + +This directory contains automated functional correctness proofs of the FreeRTOS +kernel queue data structure. These properties are proven with the +[VeriFast](https://github.com/verifast/verifast) verifier. + +## Proof directory structure + +We split proofs by data structure into separate proof directories. Each file +within a proof directory is a proof of one or more related API functions. A +proof is the source code of the FreeRTOS implementation with VeriFast +annotations (denoted by special comments `/*@ ... @*/`). A set of common +predicates, functions and lemmas used by all proofs is maintained in the +`include/proof` directory. + + - `queue`: proofs for the FreeRTOS queue data structure + +The following figure gives the callgraph of the queue proofs. Green=Proven +functions, Blue=Functions modeled by lock invariants (underlying implementation +assumed to provide these atomicity guarantees), Grey=Assumed stubs. + + + +## Prerequisites + +Proof checking needs VeriFast and proof regression further needs make and perl. + +We recommend installing VeriFast from the nightly builds on the [VeriFast +GitHub page](https://github.com/verifast/verifast). After unpacking the build +tarball, the `verifast` and `vfide` binaries will be in the directory +`verifast-COMMIT/bin/` where `COMMIT` is the Git commit of the VeriFast build. + +Note that for CI we use [VeriFast 19.12](https://github.com/verifast/verifast/releases). + +## Proof checking a single proof in the VeriFast IDE + +To load a proof in the `vfide` VeriFast IDE: + +``` +$ /path/to/vfide -I include queue/xQueueGenericSend.c +``` + +Then click `Verify` and `Verify Program` (or press F5). Note that the following +proofs require arithmetic overflow checking to be turned off (click `Verify` +and uncheck `Check arithmetic overflow`). + + - `queue/prvCopyDataToQueue.c` + - `queue/xQueueGenericSendFromISR.c` + - `queue/xQueueReceiveFromISR.c` + +A successful proof results in the top banner turning green with a statement +similar to: `0 errors found (328 statements verified)`. + +## Proof checking a single proof at the command-line + +The following is an example of checking a proof using the `verifast` +command-line tool. Turn off arithmetic overflow checking where necessary with +the flag `-disable_overflow_check`. + +``` +$ /path/to/verifast -I include -c queue/xQueueGenericSend.c +``` + +A successful proof results in output similar to: + +``` +queue/xQueueGenericSend.c +0 errors found (328 statements verified) +``` + +## Running proof regression + +The following will check all proofs in the repo along with a statement coverage +regression. + +``` +$ VERIFAST=/path/to/verifast make +``` + +If you have made changes to the proofs so the statement coverage no longer +matches then you can temporarily turn off coverage checking: + +``` +$ VERIFAST=/path/to/verifast NO_COVERAGE=1 make +``` + +## Annotation burden + +VeriFast can emit statistics about the number of source code lines and +annotations. These range from .3-2x annotations per line of source code. + +``` +$ VERIFAST=/path/to/verifast ./scripts/annotation_overhead.sh +``` + +## Reading a VeriFast proof + +VeriFast is a modular deductive verifier using separation logic. A quick +introduction is given by [Jacobs and +Piessens](https://people.cs.kuleuven.be/~bart.jacobs/verifast/verifast.pdf). +In particular, Section 1 Introduction, gives a high-level overview of the proof +technique, which uses forward symbolic execution over a symbolic heap. + +Learning how to use VeriFast will help you read and understand the proofs. +The VeriFast +[tutorial](https://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf) is +a good guide. You will need to understand: + + - Sec 4. Functions and Contracts + - Sec 5. Patterns + - Sec 6. Predicates + - Sec 7. Recursive Predicates + - Sec 8. Loops + - Sec 9. Inductive Datatypes + - Sec 10. Inductive Datatypes + - Sec 11. Lemmas + +## Contributors + +We acknowledge and thank the following contributors, listed alphabetically: + + - Bart Jacobs, KU Leuven, https://people.cs.kuleuven.be/~bart.jacobs/ diff --git a/FreeRTOS/Test/VeriFast/docs/callgraph.png b/FreeRTOS/Test/VeriFast/docs/callgraph.png Binary files differnew file mode 100644 index 000000000..283c770b5 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/docs/callgraph.png diff --git a/FreeRTOS/Test/VeriFast/include/proof/common.gh b/FreeRTOS/Test/VeriFast/include/proof/common.gh new file mode 100644 index 000000000..c3b064939 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/include/proof/common.gh @@ -0,0 +1,555 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#ifndef COMMON_H +#define COMMON_H + +#include <listex.gh> + +fixpoint list<t> rotate_left<t>(int n, list<t> xs) { + return append(drop(n, xs), take(n, xs)); +} + +fixpoint list<t> singleton<t>(t x) { + return cons(x, nil); +} + +lemma void note(bool b) + requires b; + ensures b; +{} + +lemma_auto void rotate_length<t>(int n, list<t> xs) + requires 0 <= n && n <= length(xs); + ensures length(rotate_left(n, xs)) == length(xs); +{} + +lemma void take_length_eq<t>(int k, list<t> xs, list<t> ys) + requires 0 <= k && k <= length(xs) && take(k, xs) == ys; + ensures length(ys) == k; +{} + +lemma void leq_bound(int x, int b) + requires b <= x && x <= b; + ensures x == b; +{} + +lemma void mul_mono_l_strict(int x, int y, int n) + requires 0 < n &*& x < y; + ensures x * n < y * n; +{ + for (int i = 1; i < n; i++) + invariant i <= n &*& x * i < y * i; + decreases n - i; + {} +} + +lemma void div_leq(int x, int y, int n) + requires 0 < n && x * n <= y * n; + ensures x <= y; +{ + assert x * n <= y * n; + if (x <= y) { + mul_mono_l(x,y,n); + } else { + mul_mono_l_strict(y,x,n); //< contradiction + } +} + +lemma void div_lt(int x, int y, int n) + requires 0 < n && x * n < y * n; + ensures x < y; +{ + assert x * n <= y * n; + if (x == y) { + } else if (x <= y) { + mul_mono_l(x,y,n); + } else { + assert y < x; + mul_mono_l(y,x,n); //< contradiction + } +} + +lemma_auto void mod_same(int n) + requires 0 < n; + ensures n % n == 0; +{ + div_rem_nonneg(n, n); + if (n / n < 1) {} else if (n / n > 1) { + mul_mono_l(2, n/n, n); + } else {} +} + +lemma void mod_lt(int x, int n) + requires 0 <= x && x < n; + ensures x % n == x; +{ + div_rem_nonneg(x, n); + if (x / n > 0) { + mul_mono_l(1, x / n, n); + } else { + } +} + +lemma void mod_plus_one(int x, int y, int n) + requires 0 <= y && 0 < n && x == (y % n); + ensures ((x+1) % n) == ((y+1) % n); +{ + div_rem_nonneg(y, n); + div_rem_nonneg(y+1, n); + div_rem_nonneg(y%n+1, n); + if (y%n+1 < n) { + mod_lt(y%n+1, n); + assert y%n == y - y/n*n; + assert (y+1)%n == y + 1 - (y + 1)/n*n; + if ((y+1)/n > y/n) { + mul_mono_l(y/n + 1, (y+1)/n, n); + } else if ((y+1)/n < y/n) { + mul_mono_l((y+1)/n + 1, y/n, n); + } + assert y - (y+1)/n*n == y - y/n*n; + assert y+1 - (y+1)/n*n == y - y/n*n + 1; + assert (y+1)%n == y%n + 1; + } else { + assert y%n+1 == n; + assert (y%n+1)%n == 0; + if (y/n + 1 < (y+1)/n) { + mul_mono_l(y/n + 2, (y+1)/n, n); + } else if (y/n + 1 > (y+1)/n) { + mul_mono_l((y+1)/n, y/n, n); + } + assert (y+1)/n == y/n + 1; + note((y+1)/n*n == (y/n + 1)*n); + assert (y+1)%n == 0; + } + assert (y%n+1)%n == (y+1)%n; +} + +lemma void mod_mul(int x, int n, int y) + requires 0 < n && 0 <= x && 0 <= y; + ensures (x*n + y)%n == y%n; +{ + mul_mono_l(0, x, n); + div_rem_nonneg(x*n+y, n); + div_rem_nonneg(y, n); + + if ((x*n+y)/n > x + y/n) { + mul_mono_l(x + y/n + 1, (x*n+y)/n, n); + } else if ((x*n+y)/n < x + y/n) { + mul_mono_l((x*n+y)/n + 1, x + y/n, n); + } + note((x*n + y)/n == x + y/n); + note((x*n + y)/n*n == (x + y/n)*n); +} + +lemma void mod_plus_distr(int x, int y, int n) + requires 0 < n && 0 <= x && 0 <= y; + ensures ((x % n) + y) % n == (x + y) % n; +{ + div_rem_nonneg(x, n); + div_rem_nonneg(x%n+y, n); + div_rem_nonneg(x+y, n); + + assert x == x/n*n + x%n; + mod_mul(x/n, n, x%n + y); +} + +lemma_auto void mod_mod(int x, int n) + requires 0 < n && 0 <= x; + ensures (x % n) % n == (x % n); +{ + mod_plus_distr(x, 0, n); +} + +lemma void mod_plus(int x, int y, int n); + requires 0 < n && 0 <= x && 0 <= y; + ensures (x + y) % n == ((x % n) + (y % n)) % n; + +lemma_auto void mod_range(int x, int n) + requires 0 <= x && 0 < n; + ensures 0 <= (x % n) && (x % n) < n; +{ + div_rem_nonneg(x, n); +} + +lemma void drop_update_le<t>(int i, int j, t x, list<t> xs) + requires 0 <= i && i <= j && j < length(xs); + ensures drop(i, update(j, x, xs)) == update(j - i, x, drop(i, xs)); +{ + switch (xs) { + case nil: + case cons(x0, xs0): + if (i == 0) { + } else { + drop_update_le(i - 1, j - 1, x, xs0); + } + } +} + +lemma void drop_update_ge<t>(int i, int j, t x, list<t> xs) + requires 0 <= j && j < i && i < length(xs); + ensures drop(i, update(j, x, xs)) == drop(i, xs); +{ + switch (xs) { + case nil: + case cons(x0, xs0): + if (j == 0) { + } else { + drop_update_ge(i - 1, j - 1, x, xs0); + } + } +} + +lemma void take_update_le<t>(int i, int j, t x, list<t> xs) + requires 0 <= i && i <= j; + ensures take(i, update(j, x, xs)) == take(i, xs); +{ + switch (xs) { + case nil: + case cons(x0, xs0): + if (i == 0) { + } else { + take_update_le(i - 1, j - 1, x, xs0); + } + } +} + +lemma void take_update_ge<t>(int i, int j, t x, list<t> xs) + requires 0 <= j && j < i && i <= length(xs); + ensures take(i, update(j, x, xs)) == update(j, x, take(i, xs)); +{ + switch (xs) { + case nil: + case cons(x0, xs0): + if (j == 0) { + } else { + take_update_ge(i - 1, j - 1, x, xs0); + } + } +} + +lemma void update_eq_append<t>(int i, t x, list<t> xs) + requires 0 <= i && i < length(xs); + ensures update(i, x, xs) == append(take(i, xs), cons(x, drop(i + 1, xs))); +{ + switch (xs) { + case nil: + case cons(x0, xs0): + if (i == 0) { + } else { + update_eq_append(i - 1, x, xs0); + } + } +} + +lemma void take_append_ge<t>(int n, list<t> xs, list<t> ys) + requires length(xs) <= n; + ensures take(n, append(xs, ys)) == append(xs, take(n - length(xs), ys)); +{ + switch (xs) { + case nil: + case cons(x0, xs0): + take_append_ge(n - 1, xs0, ys); + } +} + +lemma void drop_drop<t>(int m, int n, list<t> xs) + requires 0 <= m && 0 <= n; + ensures drop(m, drop(n, xs)) == drop(m+n, xs); +{ + switch (xs) { + case nil: + case cons(x0, xs0): + if (n == 0) {} else { + drop_drop(m, n-1, xs0); + } + } +} + +lemma void take_take<t>(int m, int n, list<t> xs) + requires 0 <= m && m <= n && n <= length(xs); + ensures take(m, take(n, xs)) == take(m, xs); +{ + switch (xs) { + case nil: + case cons(x0, xs0): + if (m == 0) {} else { + take_take(m - 1, n - 1, xs0); + } + } +} + +lemma void index_of_distinct<t>(list<t> xs, t x1, t x2) + requires mem(x1, xs) == true &*& mem(x2, xs) == true &*& x1 != x2; + ensures index_of(x1, xs) != index_of(x2, xs); +{ + switch (xs) { + case nil: + case cons(h, tl): + if (h == x1 || h == x2) { + /* trivial */ + } else { + index_of_distinct(tl, x1, x2); + } + } +} + +lemma void remove_remove_nth<t>(list<t> xs, t x) + requires mem(x, xs) == true; + ensures remove(x, xs) == remove_nth(index_of(x, xs), xs); +{ + switch (xs) { + case nil: + case cons(h, tl): + if (x == h) { + assert index_of(x, xs) == 0; + } else { + remove_remove_nth(tl, x); + } + } +} + +/* Following lemma from `verifast/bin/rt/_list.java`. Renamed to +avoid clash with listex.c's nth_drop lemma. */ +lemma void nth_drop2<t>(list<t> vs, int i) +requires 0 <= i && i < length(vs); +ensures nth(i, vs) == head(drop(i, vs)); +{ + switch (vs) { + case nil: + case cons(v, vs0): + if (i == 0) { + } else { + nth_drop2(vs0, i - 1); + } + } +} + +lemma void enq_lemma<t>(int k, int i, list<t> xs, list<t> ys, t z) + requires 0 <= k && 0 <= i && 0 < length(xs) && k < length(xs) && i < length(xs) && take(k, rotate_left(i, xs)) == ys; + ensures take(k+1, rotate_left(i, update((i+k)%length(xs), z, xs))) == append(ys, cons(z, nil)); +{ + int j = (i+k)%length(xs); + assert take(k, append(drop(i, xs), take(i, xs))) == ys; + if (i + k < length(xs)) { + mod_lt(i + k, length(xs)); + assert j == i + k; + drop_update_le(i, i + k, z, xs); + assert drop(i, update(i + k, z, xs)) == update(k, z, drop(i, xs)); + take_update_le(i, i + k, z, xs); + assert take(i, update(i + k, z, xs)) == take(i, xs); + take_append(k+1, update(k, z, drop(i, xs)), take(i, xs)); + assert take(k+1, append(update(k, z, drop(i, xs)), take(i, xs))) == take(k+1, update(k, z, drop(i, xs))); + update_eq_append(k, z, drop(i, xs)); + assert update(k, z, drop(i, xs)) == append(take(k, drop(i, xs)), cons(z, drop(k + 1, drop(i, xs)))); + take_append_ge(k+1, take(k, drop(i, xs)), cons(z, drop(k + 1, drop(i, xs)))); + assert take(k+1, append(take(k, drop(i, xs)), cons(z, drop(k + 1, drop(i, xs))))) == + append(take(k, drop(i, xs)), {z}); + take_append(k, drop(i, xs), take(i, xs)); + assert take(k+1, append(take(k, drop(i, xs)), cons(z, drop(k + 1, drop(i, xs))))) == + append(take(k, append(drop(i, xs), take(i, xs))), {z}); + assert take(k+1, update(k, z, drop(i, xs))) == + append(take(k, append(drop(i, xs), take(i, xs))), {z}); + assert take(k+1, append(update(k, z, drop(i, xs)), take(i, xs))) == + append(take(k, append(drop(i, xs), take(i, xs))), {z}); + assert take(k+1, append(drop(i, update(i + k, z, xs)), take(i, update(i + k, z, xs)))) == + append(take(k, append(drop(i, xs), take(i, xs))), {z}); + + } else { + assert i + k < 2 * length(xs); + div_rem_nonneg(i + k, length(xs)); + if ((i + k) / length(xs) > 1) { + mul_mono_l(2, (i + k) / length(xs), length(xs)); + } else if ((i + k) / length(xs) < 1) { + mul_mono_l((i + k) / length(xs), 0, length(xs)); + } + assert j == i + k - length(xs); + assert j < i; + drop_update_ge(i, j, z, xs); + assert drop(i, update(j, z, xs)) == drop(i, xs); + take_update_ge(i, j, z, xs); + assert update(j, z, take(i, xs)) == take(i, update(j, z, xs)); + take_append_ge(k+1, drop(i, xs), take(i, update(j, z, xs))); + assert take(k+1, append(drop(i, update(j, z, xs)), take(i, update(j, z, xs)))) == + append(drop(i, xs), take(j+1, update(j, z, take(i, xs)))); + update_eq_append(j, z, take(i, xs)); + assert update(j, z, take(i, xs)) == append(take(j, take(i, xs)), cons(z, drop(j + 1, take(i, xs)))); + take_take(j, i, xs); + assert update(j, z, take(i, xs)) == append(take(j, xs), cons(z, drop(j+1, take(i, xs)))); + take_append_ge(j+1, take(j, xs), cons(z, drop(j+1, take(i, xs)))); + assert append(drop(i, xs), take(j+1, update(j, z, take(i, xs)))) == + append(drop(i, xs), append(take(j, xs), {z})); + take_append_ge(k, drop(i, xs), take(i, xs)); + append_assoc(drop(i, xs), take(j, xs), {z}); + assert append(drop(i, xs), append(take(j, xs), {z})) == + append(take(k, append(drop(i, xs), take(i, xs))), {z}); + assert append(drop(i, xs), take(j+1, update(j, z, take(i, xs)))) == + append(take(k, append(drop(i, xs), take(i, xs))), {z}); + } + assert take(k+1, append(drop(i, update(j, z, xs)), take(i, update(j, z, xs)))) == + append(take(k, append(drop(i, xs), take(i, xs))), {z}); + assert take(k+1, append(drop(i, update(j, z, xs)), take(i, update(j, z, xs)))) == append(ys, {z}); +} + +lemma void front_enq_lemma<t>(int k, int i, list<t> xs, list<t> ys, t z) + requires 0 < length(xs) && 0 <= k && k < length(xs) && 0 <= i && i < length(xs) && take(k, rotate_left((i+1)%length(xs), xs)) == ys; + ensures take(k+1, rotate_left(i, update(i, z, xs))) == cons(z, ys); +{ + int n = length(xs); + if (i+1 < n) { + mod_lt(i+1, n); + assert i < n; + assert take(k+1, rotate_left(i, update(i, z, xs))) == + take(k+1, append(drop(i, update(i, z, xs)), take(i, update(i, z, xs)))); + drop_update_le(i, i, z, xs); + take_update_le(i, i, z, xs); + assert take(k+1, append(drop(i, update(i, z, xs)), take(i, update(i, z, xs)))) == + take(k+1, append(update(0, z, drop(i, xs)), take(i, xs))); + update_eq_append(0, z, drop(i, xs)); + assert update(0, z, drop(i, xs)) == cons(z, drop(1, drop(i, xs))); + drop_drop(1, i, xs); + assert take(k+1, append(update(0, z, drop(i, xs)), take(i, xs))) == + take(k+1, append(cons(z, drop(i+1, xs)), take(i, xs))); + assert take(k+1, append(cons(z, drop(i+1, xs)), take(i, xs))) == + cons(z, take(k, append(drop(i+1, xs), take(i, xs)))); + + assert ys == take(k, rotate_left(i+1, xs)); + assert ys == take(k, append(drop(i+1, xs), take(i+1, xs))); + if (k <= length(drop(i+1, xs))) { + take_append(k, drop(i+1, xs), take(i+1, xs)); + take_append(k, drop(i+1, xs), take(i, xs)); + } else { + take_append_ge(k, drop(i+1, xs), take(i+1, xs)); + take_append_ge(k, drop(i+1, xs), take(i, xs)); + + assert (i+1) + k < 2 * n; + div_rem_nonneg((i+1) + k, n); + if (((i+1) + k) / n > 1) { + mul_mono_l(2, ((i+1) + k) / n, n); + } else if (((i+1) + k) / n < 1) { + mul_mono_l(((i+1) + k) / n, 0, n); + } + int j = ((i+1)+k)%n; + assert j <= i; + int l = length(drop(i+1, xs)); + assert l == n - i - 1; + take_take(k - l, i + 1, xs); + take_take(k - l, i, xs); + } + } else { + assert i == (n-1); + assert (i + 1) % n == 0; + drop_update_le(i, i, z, xs); + update_eq_append(0, z, xs); + assert take(k+1, rotate_left(i, update(i, z, xs))) == + take(k+1, append(drop(i, update(i, z, xs)), take(i, update(i, z, xs)))); + drop_update_le(i, i, z, xs); + assert take(k+1, rotate_left(i, update(i, z, xs))) == + take(k+1, append(update(0, z, drop(i, xs)), take(i, update(i, z, xs)))); + update_eq_append(0, z, drop(i, xs)); + assert take(k+1, rotate_left(i, update(i, z, xs))) == + take(k+1, append(cons(z, drop(1, drop(i, xs))), take(i, update(i, z, xs)))); + drop_drop(1, i, xs); + assert take(k+1, rotate_left(i, update(i, z, xs))) == + take(k+1, append(cons(z, nil), take(i, update(i, z, xs)))); + take_update_le(i, i, z, xs); + assert take(k+1, rotate_left(i, update(i, z, xs))) == + cons(z, take(k, take(i, xs))); + take_take(k, i, xs); + assert take(k+1, rotate_left(i, update(i, z, xs))) == cons(z, ys); + } +} + +lemma void deq_lemma<t>(int k, int i, list<t> xs, list<t> ys, t z) + requires 0 < k && k <= length(xs) && 0 <= i && i < length(xs) && take(k, rotate_left(i, xs)) == ys && z == head(ys); + ensures take(k-1, rotate_left((i+1)%length(xs), xs)) == tail(ys); +{ + int j = (i+1)%length(xs); + drop_n_plus_one(i, xs); + assert tail(take(k, append(drop(i, xs), take(i, xs)))) == take(k-1, append(drop(i+1, xs), take(i, xs))); + if (i+1 < length(xs)) { + mod_lt(i+1, length(xs)); + assert j == i+1; + if (k-1 <= length(xs)-j) { + take_append(k-1, drop(j, xs), take(j, xs)); + take_append(k-1, drop(j, xs), take(i, xs)); + } else { + assert k+i > length(xs); + take_append_ge(k-1, drop(j, xs), take(j, xs)); + take_append_ge(k-1, drop(j, xs), take(i, xs)); + assert k-1-(length(xs)-j) == k+i-length(xs); + assert k+i-length(xs) <= i; + take_take(k+i-length(xs), j, xs); + take_take(k+i-length(xs), i, xs); + assert take(k+i-length(xs), take(j, xs)) == take(k+i-length(xs), take(i, xs)); + } + } else { + assert i+1 == length(xs); + assert (i+1)%length(xs) == 0; + assert j == 0; + assert append(drop(j, xs), take(j, xs)) == xs; + assert append(drop(i+1, xs), take(i, xs)) == take(i, xs); + take_append_ge(k-1, drop(i+1, xs), take(i, xs)); + take_take(k-1, i, xs); + } + assert take(k-1, append(drop(j, xs), take(j, xs))) == take(k-1, append(drop(i+1, xs), take(i, xs))); + assert take(k-1, append(drop(j, xs), take(j, xs))) == tail(take(k, append(drop(i, xs), take(i, xs)))); +} + +lemma void deq_value_lemma<t>(int k, int i, list<t> xs, list<t> ys) + requires 0 < k && k <= length(ys) && 0 <= i && i < length(xs) && take(k, rotate_left(i, xs)) == ys; + ensures nth(i, xs) == head(ys); +{ + drop_n_plus_one(i, xs); + assert nth(i, xs) == head(take(k, append(drop(i, xs), take(i, xs)))); +} + +lemma void combine_list_no_change<t>(list<t>prefix, t x, list<t>suffix, int i, list<t> xs) + requires 0 <= i && i < length(xs) && prefix == take(i, xs) && x == nth(i, xs) && suffix == drop(i+1, xs); + ensures xs == append(prefix, cons(x, suffix)); +{ + drop_n_plus_one(i, xs); +} + +/* Following lemma from `verifast/examples/vstte2010/problem4.java`. */ +lemma void update_rewrite<t>(list<t> vs, t v, int pos) + requires 0 <= pos && pos < length(vs); + ensures update(pos, v, vs) == append(take(pos, vs), cons(v, (drop(pos+1, vs)))); +{ + switch(vs) { + case nil: + case cons(h, t): + if(pos == 0) { + } else { + update_rewrite(t, v, pos - 1); + } + } +} + +lemma void combine_list_update<t>(list<t>prefix, t x, list<t>suffix, int i, list<t> xs) + requires 0 <= i && i < length(xs) && prefix == take(i, xs) && suffix == drop(i+1, xs); + ensures update(i, x, xs) == append(prefix, cons(x, suffix)); +{ + update_rewrite(xs, x, i); +} + +#endif /* COMMON_H */ diff --git a/FreeRTOS/Test/VeriFast/include/proof/queue.h b/FreeRTOS/Test/VeriFast/include/proof/queue.h new file mode 100644 index 000000000..610bc03d9 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/include/proof/queue.h @@ -0,0 +1,550 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#ifndef QUEUE_H +#define QUEUE_H + +#define VERIFAST +#include <stdlib.h> +#include <stdint.h> +#include <string.h> +#include <threading.h> +/*@#include "common.gh"@*/ + +typedef size_t TickType_t; +typedef size_t UBaseType_t; +typedef ssize_t BaseType_t; + +/* Empty/no-op macros */ +/* Tracing */ +#define traceBLOCKING_ON_QUEUE_PEEK(x) +#define traceBLOCKING_ON_QUEUE_RECEIVE(x) +#define traceBLOCKING_ON_QUEUE_SEND(x) +#define traceQUEUE_CREATE(x) +#define traceQUEUE_CREATE_FAILED(x) +#define traceQUEUE_DELETE(x) +#define traceQUEUE_PEEK(x) +#define traceQUEUE_PEEK_FAILED(x) +#define traceQUEUE_PEEK_FROM_ISR(x) +#define traceQUEUE_PEEK_FROM_ISR_FAILED(x) +#define traceQUEUE_RECEIVE(x) +#define traceQUEUE_RECEIVE_FAILED(x) +#define traceQUEUE_RECEIVE_FROM_ISR(x) +#define traceQUEUE_RECEIVE_FROM_ISR_FAILED(x) +#define traceQUEUE_SEND(x) +#define traceQUEUE_SEND_FAILED(x) +#define traceQUEUE_SEND_FROM_ISR(x) +#define traceQUEUE_SEND_FROM_ISR_FAILED(x) +/* Coverage */ +#define mtCOVERAGE_TEST_MARKER() +/* Asserts */ +#define configASSERT(x) +#define portASSERT_IF_INTERRUPT_PRIORITY_INVALID() + +/* Map portable memory management functions */ +#define pvPortMalloc malloc +#define vPortFree free + +#define queueSEND_TO_BACK ( ( BaseType_t ) 0 ) +#define queueSEND_TO_FRONT ( ( BaseType_t ) 1 ) +#define queueOVERWRITE ( ( BaseType_t ) 2 ) + +#define pdTRUE 1 +#define pdFALSE 0 + +#define pdPASS pdTRUE +#define pdFAIL pdFALSE +#define errQUEUE_FULL 0 +#define errQUEUE_EMPTY 0 + +/* Constants used with the cRxLock and cTxLock structure members. */ +#define queueUNLOCKED ( ( int8_t ) -1 ) +#define queueLOCKED_UNMODIFIED ( ( int8_t ) 0 ) +#define queueINT8_MAX ( ( int8_t ) 127 ) + +typedef struct QueuePointers +{ + int8_t * pcTail; /*< Points to the byte at the end of the queue storage area. Once more byte is allocated than necessary to store the queue items, this is used as a marker. */ + int8_t * pcReadFrom; /*< Points to the last place that a queued item was read from when the structure is used as a queue. */ +} QueuePointers_t; + +typedef struct SemaphoreData +{ +#ifdef VERIFAST /*< do not model xMutexHolder */ + void *xMutexHolder; +#else + TaskHandle_t xMutexHolder; /*< The handle of the task that holds the mutex. */ +#endif + UBaseType_t uxRecursiveCallCount; /*< Maintains a count of the number of times a recursive mutex has been recursively 'taken' when the structure is used as a mutex. */ +} SemaphoreData_t; + +/* VeriFast does not support unions so we replace with a struct */ +struct fake_union_t { + QueuePointers_t xQueue; + SemaphoreData_t xSemaphore; +}; + +typedef struct xLIST { + UBaseType_t uxNumberOfItems; +#ifndef VERIFAST /*< do not model pxIndex and xListEnd of xLIST struct */ + struct xLIST_ITEM *pxIndex; + MiniListItem_t xListEnd; +#endif +} List_t; + +typedef struct QueueDefinition /* The old naming convention is used to prevent breaking kernel aware debuggers. */ +{ + int8_t * pcHead; /*< Points to the beginning of the queue storage area. */ + int8_t * pcWriteTo; /*< Points to the free next place in the storage area. */ + +#ifdef VERIFAST /*< VeriFast does not model unions */ + struct fake_union_t u; +#else + union + { + QueuePointers_t xQueue; /*< Data required exclusively when this structure is used as a queue. */ + SemaphoreData_t xSemaphore; /*< Data required exclusively when this structure is used as a semaphore. */ + } u; +#endif + + List_t xTasksWaitingToSend; /*< List of tasks that are blocked waiting to post onto this queue. Stored in priority order. */ + List_t xTasksWaitingToReceive; /*< List of tasks that are blocked waiting to read from this queue. Stored in priority order. */ + + volatile UBaseType_t uxMessagesWaiting; /*< The number of items currently in the queue. */ + UBaseType_t uxLength; /*< The length of the queue defined as the number of items it will hold, not the number of bytes. */ + UBaseType_t uxItemSize; /*< The size of each items that the queue will hold. */ + + volatile int8_t cRxLock; /*< Stores the number of items received from the queue (removed from the queue) while the queue was locked. Set to queueUNLOCKED when the queue is not locked. */ + volatile int8_t cTxLock; /*< Stores the number of items transmitted to the queue (added to the queue) while the queue was locked. Set to queueUNLOCKED when the queue is not locked. */ + + #if ( ( configSUPPORT_STATIC_ALLOCATION == 1 ) && ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) ) + uint8_t ucStaticallyAllocated; /*< Set to pdTRUE if the memory used by the queue was statically allocated to ensure no attempt is made to free the memory. */ + #endif + + #if ( configUSE_QUEUE_SETS == 1 ) + struct QueueDefinition * pxQueueSetContainer; + #endif + + #if ( configUSE_TRACE_FACILITY == 1 ) + UBaseType_t uxQueueNumber; + uint8_t ucQueueType; + #endif + + /*@struct mutex *irqMask;@*/ /*< Ghost mutex simulates the effect of irq masking */ + /*@struct mutex *schedulerSuspend;@*/ /*< Ghost mutex simulates the effect of scheduler suspension */ + /*@struct mutex *locked;@*/ /*< Ghost mutex simulates the effect of queue locking */ +} xQUEUE; + +typedef xQUEUE Queue_t; + +typedef struct QueueDefinition * QueueHandle_t; + +/*@ +#define QUEUE_SHAPE(q, Storage, N, M, K) \ + malloc_block_QueueDefinition(q) &*& \ + q->pcHead |-> Storage &*& \ + q->pcWriteTo |-> ?WPtr &*& \ + q->u.xQueue.pcTail |-> ?End &*& \ + q->u.xQueue.pcReadFrom |-> ?RPtr &*& \ + q->uxItemSize |-> M &*& \ + q->uxLength |-> N &*& \ + q->uxMessagesWaiting |-> K &*& \ + q->cRxLock |-> ?rxLock &*& \ + q->cTxLock |-> ?txLock &*& \ + struct_QueuePointers_padding(&q->u.xQueue) &*& \ + struct_SemaphoreData_padding(&q->u.xSemaphore) &*& \ + struct_fake_union_t_padding(&q->u) &*& \ + struct_xLIST_padding(&q->xTasksWaitingToSend) &*& \ + struct_xLIST_padding(&q->xTasksWaitingToReceive) &*& \ + q->u.xSemaphore.xMutexHolder |-> _ &*& \ + q->u.xSemaphore.uxRecursiveCallCount |-> _ &*& \ + true + +predicate queue(QueueHandle_t q, int8_t *Storage, size_t N, size_t M, size_t W, size_t R, size_t K, bool is_locked; list<list<char> >abs) = + QUEUE_SHAPE(q, Storage, N, M, K) &*& + 0 < N &*& + 0 < M &*& + 0 <= W &*& W < N &*& + 0 <= R &*& R < N &*& + 0 <= K &*& K <= N &*& + W == (R + 1 + K) % N &*& + (-1) <= rxLock &*& + (-1) <= txLock &*& + (is_locked ? 0 <= rxLock : (-1) == rxLock) &*& + (is_locked ? 0 <= txLock : (-1) == txLock) &*& + WPtr == Storage + (W*M) &*& + RPtr == Storage + (R*M) &*& + End == Storage + (N*M) &*& + buffer(Storage, N, M, ?contents) &*& + length(contents) == N &*& + abs == take(K, rotate_left((R+1)%N, contents)) &*& + malloc_block(Storage, N*M) &*& + true + ; +@*/ + +/* A buffer allows us to interpret a flat character array of `N*M` bytes as a +list of `N` elements where each element is `M` bytes */ +/*@ +predicate buffer(char *buffer, size_t N, size_t M; list<list<char> > elements) = + N == 0 + ? elements == nil + : chars(buffer, M, ?x) &*& buffer(buffer + M, N - 1, M, ?xs) &*& elements == cons(x, xs); + +lemma void buffer_length(char *buffer, size_t N, size_t M) +requires buffer(buffer, N, M, ?elements); +ensures buffer(buffer, N, M, elements) &*& length(elements) == N; +{ + if (N == 0) { + open buffer(buffer, N, M, elements); + close buffer(buffer, N, M, elements); + } else { + open buffer(buffer, N, M, elements); + buffer_length(buffer+M, N-1, M); + } +} +@*/ + +/* +There is no need in the queue proofs to preserve a relationship between `cs` +and `elements` (i.e., `flatten(elements) == cs`) because we only move in one +direction from `cs` to `elements` during queue creation when the contents is +fresh from `malloc` (i.e., uninitialized). If we needed to do a roundtrip from +elements back to cs then this would require a stronger lemma. +*/ +/*@ +lemma void buffer_from_chars(char *buffer, size_t N, size_t M) +requires chars(buffer, N*M, ?cs) &*& 0 <= N &*& 0 < M; +ensures exists<list<list<char> > >(?elements) &*& buffer(buffer, N, M, elements) &*& length(elements) == N; +{ + if (N == 0) { + close exists(nil); + } else { + int i = 0; + while (i < N) + invariant 0 <= i &*& i <= N &*& + chars(buffer, (N-i)*M, ?xs) &*& xs == take((N-i)*M, cs) &*& + buffer(buffer + (N-i)*M, i, M, ?ys); + decreases N-i; + { + mul_mono_l(0, N-i-1, M); + chars_split(buffer, (N-i-1)*M); + mul_mono_l(i, N, M); + mul_mono_l(N-i, N, M); + take_take((N-i-1)*M, (N-i)*M, cs); + i++; + } + close exists(ys); + buffer_length(buffer, N, M); + } +} + +lemma void append_buffer(char *buffer, size_t N1, size_t N2, size_t M) +requires + buffer(buffer, N1, M, ?elements1) &*& + buffer(buffer + N1 * M, N2, M, ?elements2) &*& + 0 <= N1 &*& 0 <= N2; +ensures buffer(buffer, N1+N2, M, append(elements1, elements2)); +{ + if (N1 == 0) { + open buffer(buffer, 0, M, _); + } else if (N2 == 0) { + open buffer(buffer + N1 * M, 0, M, _); + } else { + open buffer(buffer, N1, M, elements1); + append_buffer(buffer + M, N1-1, N2, M); + close buffer(buffer, N1+N2, M, cons(?x, append(xs, elements2))); + } +} + +lemma void split_element<t>(char *buffer, size_t N, size_t M, size_t i) +requires buffer(buffer, N, M, ?elements) &*& 0 <= i &*& i < N; +ensures + buffer(buffer, i, M, take(i, elements)) &*& + chars(buffer + i * M, M, nth(i, elements)) &*& + buffer(buffer + (i + 1) * M, (N-1-i), M, drop(i+1, elements)); +{ + if (i == 0) { + // straightforward + } else { + buffer_length(buffer, N, M); + int j = 0; + while (j < i) + invariant 0 <= j &*& j <= i &*& + buffer(buffer, j, M, take(j, elements)) &*& + buffer(buffer + j * M, N-j, M, drop(j, elements)); + decreases i-j; + { + drop_drop(1, j, elements); + nth_drop2(elements, j); + open buffer(buffer + j * M, N-j, M, drop(j, elements)); + assert chars(buffer + j * M, M, ?x) &*& x == nth(j, elements); + close buffer(buffer + j * M, 1, M, singleton(x)); + append_buffer(buffer, j, 1, M); + take_plus_one(j, elements); + j++; + } + drop_drop(1, j, elements); + nth_drop2(elements, i); + open buffer(buffer + (i+1) * M, (N-1-i), M, _); + } +} + +lemma void join_element(char *buffer, size_t N, size_t M, size_t i) +requires + 0 <= i &*& i < N &*& + buffer(buffer, i, M, ?prefix) &*& + chars(buffer + i * M, M, ?element) &*& + buffer(buffer + (i + 1) * M, (N-1-i), M, ?suffix); +ensures buffer(buffer, N, M, append(prefix, cons(element, suffix))); +{ + if (i == 0) { + open buffer(buffer, i, M, prefix); + assert prefix == nil; + close buffer(buffer, N, M, cons(element, suffix)); + } else { + close buffer(buffer + i * M, N-i, M, cons(element, suffix)); + append_buffer(buffer, i, N-i, M); + } +} + +predicate list(List_t *l;) = + l->uxNumberOfItems |-> _; + +predicate queuelists(QueueHandle_t q;) = + list(&q->xTasksWaitingToSend) &*& + list(&q->xTasksWaitingToReceive); +@*/ + +/* Because prvCopyDataFromQueue does *not* decrement uxMessagesWaiting (K) the +queue predicate above does not hold as a postcondition. If the caller +subsequently decrements K then the queue predicate can be reinstated. */ +/*@ +predicate queue_after_prvCopyDataFromQueue(QueueHandle_t q, int8_t *Storage, size_t N, size_t M, size_t W, size_t R, size_t K, bool is_locked; list<list<char> >abs) = + QUEUE_SHAPE(q, Storage, N, M, K) &*& + 0 < N &*& + 0 < M &*& + 0 <= W &*& W < N &*& + 0 <= R &*& R < N &*& + 0 <= K &*& K <= N &*& + W == (R + K) % N &*& //< Differs from queue predicate + (-1) <= rxLock &*& + (-1) <= txLock &*& + (is_locked ? 0 <= rxLock : (-1) == rxLock) &*& + (is_locked ? 0 <= txLock : (-1) == txLock) &*& + WPtr == Storage + (W*M) &*& + RPtr == Storage + (R*M) &*& + End == Storage + (N*M) &*& + buffer(Storage, N, M, ?contents) &*& + length(contents) == N &*& + abs == take(K, rotate_left(R, contents)) &*& //< Differs from queue predicate + malloc_block(Storage, N*M) &*& + true + ; +@*/ + +/* Can't be called `mutex` as this clashes with VeriFast's predicate */ +/*@ +predicate freertos_mutex(QueueHandle_t q, int8_t *Storage, size_t N, size_t K;) = + QUEUE_SHAPE(q, Storage, N, 0, K) &*& + queuelists(q) &*& + 0 < N &*& + 0 <= K &*& K <= N &*& + (-1) <= rxLock &*& + (-1) <= txLock &*& + WPtr == Storage &*& + RPtr == Storage &*& + End == Storage &*& + malloc_block(Storage, 0) &*& + chars(Storage, 0, _) &*& + true + ; +@*/ + +/* A queuehandle can be shared between tasks and ISRs. Acquiring the ghost +`irqMask` gives access to the core queue resources. The permissions granted +after masking interrupts depends on the caller: +- A task has access to the queue and the queuelists +- An ISR has access to the queue and, if the queue is unlocked, the queuelists */ +/*@ +predicate queuehandle(QueueHandle_t q, size_t N, size_t M, bool is_isr;) = + q->irqMask |-> ?m &*& mutex(m, irqs_masked_invariant(q, N, M, is_isr)); + +predicate_ctor irqs_masked_invariant(QueueHandle_t queue, size_t N, size_t M, bool is_isr)() = + queue(queue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + (is_isr && is_locked ? true : queuelists(queue)); +@*/ + +/* A queuesuspend can be shared between tasks. Acquiring the ghost `schedulerSuspend` gives access to the `locked` mutex. */ +/*@ +predicate_ctor scheduler_suspended_invariant(QueueHandle_t queue)() = + queue->locked |-> ?m &*& + mutex(m, queue_locked_invariant(queue)); + +predicate queuesuspend(QueueHandle_t q;) = + q->schedulerSuspend |-> ?m &*& + mutex(m, scheduler_suspended_invariant(q)); +@*/ + +/* A queuelock is exclusively acquired by a task. Acquiring the ghost `queuelock` gives access to the queue list resources. */ +/*@ +predicate queuelock(QueueHandle_t q;) = + q->locked |-> ?m &*& + mutex(m, queue_locked_invariant(q)); + +predicate_ctor queue_locked_invariant(QueueHandle_t queue)() = + queuelists(queue); +@*/ + +BaseType_t vListInitialise(List_t *list); +/*@requires list(list);@*/ +/*@ensures list(list);@*/ + +BaseType_t listLIST_IS_EMPTY(List_t *list); +/*@requires list->uxNumberOfItems |-> ?len;@*/ +/*@ensures list->uxNumberOfItems |-> len &*& result == (len == 0 ? pdTRUE : pdFALSE);@*/ + +typedef struct xTIME_OUT +{ + BaseType_t xOverflowCount; + TickType_t xTimeOnEntering; +} TimeOut_t; + +/*@ +predicate xTIME_OUT(struct xTIME_OUT *to;) = + to->xOverflowCount |-> _ &*& + to->xTimeOnEntering |-> _ &*& + struct_xTIME_OUT_padding(to); +@*/ + +void vTaskInternalSetTimeOutState( TimeOut_t * x); +/*@requires xTIME_OUT(x);@*/ +/*@ensures xTIME_OUT(x);@*/ + +BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait ); +/*@requires xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/ +/*@ensures xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/ + +BaseType_t xTaskRemoveFromEventList(List_t *list); +/*@requires list(list);@*/ +/*@ensures list(list);@*/ + +void vTaskPlaceOnEventList( List_t * const pxEventList, const TickType_t xTicksToWait ); +/*@requires list(pxEventList);@*/ +/*@ensures list(pxEventList);@*/ + +void vTaskMissedYield(); +/*@requires true;@*/ +/*@ensures true;@*/ + +void vTaskSuspendAll(); +/*@requires exists<QueueHandle_t>(?xQueue) &*& + [1/2]xQueue->schedulerSuspend |-> ?m &*& + [1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/ +/*@ensures [1/2]xQueue->schedulerSuspend |-> m &*& + mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*& + xQueue->locked |-> ?m2 &*& + mutex(m2, queue_locked_invariant(xQueue));@*/ + +BaseType_t xTaskResumeAll( void ); +/*@requires exists<QueueHandle_t>(?xQueue) &*& + [1/2]xQueue->schedulerSuspend |-> ?m &*& + mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*& + xQueue->locked |-> ?m2 &*& + mutex(m2, queue_locked_invariant(xQueue));@*/ +/*@ensures [1/2]xQueue->schedulerSuspend |-> m &*& + [1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/ + +void prvLockQueue( QueueHandle_t xQueue ); +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& + [1/2]queuelock(xQueue); @*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]xQueue->locked |-> ?m &*& + mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*& + queue_locked_invariant(xQueue)();@*/ + +void prvUnlockQueue( QueueHandle_t xQueue ); +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& + [1/2]xQueue->locked |-> ?m &*& + mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*& + queue_locked_invariant(xQueue)();@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]queuelock(xQueue);@*/ + +void setInterruptMask(QueueHandle_t xQueue) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/ +/*@ensures [1/2]xQueue->irqMask |-> ?m &*& + mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*& + queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + queuelists(xQueue);@*/ +{ + /*@open queuehandle(xQueue, N, M, is_isr);@*/ + mutex_acquire(xQueue->irqMask); + /*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/ +} + +void clearInterruptMask(QueueHandle_t xQueue) +/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + [1/2]xQueue->irqMask |-> ?m &*& + mutex_held(m, irqs_masked_invariant(xQueue, N, M, false), currentThread, 1/2) &*& + queuelists(xQueue);@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, false);@*/ +{ + /*@close irqs_masked_invariant(xQueue, N, M, false)();@*/ + mutex_release(xQueue->irqMask); + /*@close [1/2]queuehandle(xQueue, N, M, false);@*/ +} + +#define taskENTER_CRITICAL() setInterruptMask(xQueue) +#define taskEXIT_CRITICAL() clearInterruptMask(xQueue) +#define portYIELD_WITHIN_API() +#define queueYIELD_IF_USING_PREEMPTION() + +UBaseType_t setInterruptMaskFromISR(QueueHandle_t xQueue) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == true;@*/ +/*@ensures [1/2]xQueue->irqMask |-> ?m &*& + mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*& + queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + (is_locked ? true : queuelists(xQueue));@*/ +{ + /*@open queuehandle(xQueue, N, M, is_isr);@*/ + mutex_acquire(xQueue->irqMask); + /*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/ + return 0; +} + +void clearInterruptMaskFromISR(QueueHandle_t xQueue, UBaseType_t uxSavedInterruptStatus) +/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + [1/2]xQueue->irqMask |-> ?m &*& + mutex_held(m, irqs_masked_invariant(xQueue, N, M, true), currentThread, 1/2) &*& + (is_locked ? true : queuelists(xQueue));@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, true);@*/ +{ + /*@close irqs_masked_invariant(xQueue, N, M, true)();@*/ + mutex_release(xQueue->irqMask); + /*@close [1/2]queuehandle(xQueue, N, M, true);@*/ +} + +#define portSET_INTERRUPT_MASK_FROM_ISR() setInterruptMaskFromISR(xQueue) +#define portCLEAR_INTERRUPT_MASK_FROM_ISR(uxSavedInterruptStatus) clearInterruptMaskFromISR(xQueue, uxSavedInterruptStatus) + +#endif /* QUEUE_H */ diff --git a/FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h b/FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h new file mode 100644 index 000000000..c590a6324 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h @@ -0,0 +1,57 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#ifndef QUEUECONTRACTS_H +#define QUEUECONTRACTS_H + +#include "queue.h" + +void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer ); +/*@requires queue(pxQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& 0 < K &*& chars(pvBuffer, M, _);@*/ +/*@ensures queue_after_prvCopyDataFromQueue(pxQueue, Storage, N, M, W, (R+1)%N, K, is_locked, abs) &*& + chars(pvBuffer, M, head(abs));@*/ + +BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ); +/*@requires queue(pxQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + (K < N || xPosition == queueOVERWRITE) &*& + chars(pvItemToQueue, M, ?x) &*& + (xPosition == queueSEND_TO_BACK || xPosition == queueSEND_TO_FRONT || (xPosition == queueOVERWRITE && N == 1));@*/ +/*@ensures + (xPosition == queueSEND_TO_BACK + ? queue(pxQueue, Storage, N, M, (W+1)%N, R, (K+1), is_locked, append(abs, singleton(x))) + : (xPosition == queueSEND_TO_FRONT + ? (R == 0 + ? queue(pxQueue, Storage, N, M, W, (N-1), (K+1), is_locked, cons(x, abs)) + : queue(pxQueue, Storage, N, M, W, (R-1), (K+1), is_locked, cons(x, abs))) + : xPosition == queueOVERWRITE &*& queue(pxQueue, Storage, N, M, W, R, 1, is_locked, singleton(x))) + ) &*& + chars(pvItemToQueue, M, x);@*/ + +BaseType_t prvIsQueueEmpty( Queue_t * pxQueue ); +/*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/ +/*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr);@*/ + +BaseType_t prvIsQueueFull( Queue_t * pxQueue ); +/*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/ +/*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr);@*/ + +#endif /* QUEUECONTRACTS_H */ diff --git a/FreeRTOS/Test/VeriFast/queue/README.md b/FreeRTOS/Test/VeriFast/queue/README.md new file mode 100644 index 000000000..1672bd214 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/README.md @@ -0,0 +1,28 @@ +# FreeRTOS queue proofs + +In the queue predicates and proofs we use the following variable names. + + - `Storage` : The concrete queue storage of `N*M` bytes. The `buffer` + predicate, defined in `include/proof/queue.h` allows us to treat the + storage as a list `contents` of `N` items, each of which is `M` bytes. + - `N` : queue length (i.e., the maximum number of items the queue can store) + - `M` : size in bytes of each element + - `W` : logical index of the write pointer, necessarily between + `0..(N-1)` such that the write pointer `pcWriteTo == Storage + W * M`. + - `R` : logical index of the read pointer, necessarily between + `0..(N-1)` such that the read pointer `pcReadFrom == Storage + R * M`. + - `K` : number of items currently in the queue corresponding to + `uxMessagesWaiting` + +The `queue` predicate, defined in `include/proof/queue.h`, relates the concrete +queue storage to an abstract list `abs` of `K` items. More precisely, the key +queue invariant is: + +``` +abs == take(K, rotate_left((R+1)%N, contents)) &*& +W == (R + 1 + K) % N +``` + +where `(R+1)%N` is the front of the queue, `W` is the back of the queue, +`rotate_left` allows for the wraparound of queue storage, and `take` gives the +first `K` elements. diff --git a/FreeRTOS/Test/VeriFast/queue/create.c b/FreeRTOS/Test/VeriFast/queue/create.c new file mode 100644 index 000000000..4a7902d3b --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/create.c @@ -0,0 +1,267 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" + +/* Simplifying assumption: we do not verify queue initialisation in a + * concurrent environment. We assume the queue initialization (including reset) + * happens-before all concurrent send/receives. */ +#ifdef VERIFAST /*< ***xQueueGenericReset happens-before concurrent behavior*** */ + #define taskENTER_CRITICAL() + #define taskEXIT_CRITICAL() +#endif + +/* The following intermediate queue predicates summarise states used by queue + * initialization but not used elsewhere so we confine them to these proofs + * locally. */ +/*@ +predicate queue_init1(QueueHandle_t q;) = + QUEUE_SHAPE(q, _, _, _, _) &*& + queuelists(q) + ; + +predicate queue_init2(QueueHandle_t q, int8_t *Storage, size_t N, size_t M;) = + QUEUE_SHAPE(q, Storage, N, M, _) &*& + queuelists(q) &*& + 0 < N &*& + chars(Storage, (N*M), _) &*& + malloc_block(Storage, N*M) &*& + Storage + N * M <= (int8_t *)UINTPTR_MAX &*& + true + ; +@*/ + +BaseType_t xQueueGenericReset( QueueHandle_t xQueue, + BaseType_t xNewQueue ) +/*@requires queue_init2(xQueue, ?Storage, ?N, ?M);@*/ +/*@ensures 0 == M + ? freertos_mutex(xQueue, Storage, N, 0) + : queue(xQueue, Storage, N, M, 0, (N-1), 0, false, nil) &*& queuelists(xQueue);@*/ +{ +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; +#endif + + configASSERT( pxQueue ); + + taskENTER_CRITICAL(); + { + pxQueue->u.xQueue.pcTail = pxQueue->pcHead + ( pxQueue->uxLength * pxQueue->uxItemSize ); /*lint !e9016 Pointer arithmetic allowed on char types, especially when it assists conveying intent. */ + pxQueue->uxMessagesWaiting = ( UBaseType_t ) 0U; + pxQueue->pcWriteTo = pxQueue->pcHead; + /*@mul_mono_l(0, N-1, M);@*/ + pxQueue->u.xQueue.pcReadFrom = pxQueue->pcHead + ( ( pxQueue->uxLength - 1U ) * pxQueue->uxItemSize ); /*lint !e9016 Pointer arithmetic allowed on char types, especially when it assists conveying intent. */ + pxQueue->cRxLock = queueUNLOCKED; + pxQueue->cTxLock = queueUNLOCKED; + + if( xNewQueue == pdFALSE ) + { + /* If there are tasks blocked waiting to read from the queue, then + * the tasks will remain blocked as after this function exits the queue + * will still be empty. If there are tasks blocked waiting to write to + * the queue, then one should be unblocked as after this function exits + * it will be possible to write to it. */ + if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToSend ) ) == pdFALSE ) + { + if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToSend ) ) != pdFALSE ) + { + queueYIELD_IF_USING_PREEMPTION(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + /* Ensure the event queues start in the correct state. */ + vListInitialise( &( pxQueue->xTasksWaitingToSend ) ); + vListInitialise( &( pxQueue->xTasksWaitingToReceive ) ); + } + + /*@if (M != 0) { buffer_from_chars(pxQueue->pcHead, N, M); }@*/ + } + taskEXIT_CRITICAL(); + + /* A value is returned for calling semantic consistency with previous + * versions. */ + return pdPASS; +} + +static void prvInitialiseNewQueue( const UBaseType_t uxQueueLength, + const UBaseType_t uxItemSize, + uint8_t * pucQueueStorage, + const uint8_t ucQueueType, + Queue_t * pxNewQueue ) + +/*@requires queue_init1(pxNewQueue) &*& + 0 < uxQueueLength &*& 0 < uxItemSize &*& + malloc_block(pucQueueStorage, uxQueueLength * uxItemSize) &*& + pucQueueStorage + uxQueueLength * uxItemSize <= (uint8_t *)UINTPTR_MAX &*& + uchars(pucQueueStorage, uxQueueLength * uxItemSize,_);@*/ +/*@ensures queue(pxNewQueue, ((int8_t *)(void *)pucQueueStorage), uxQueueLength, uxItemSize, 0, (uxQueueLength-1), 0, false, nil) &*& + queuelists(pxNewQueue);@*/ +{ +#ifndef VERIFAST /*< void cast of unused var */ + /* Remove compiler warnings about unused parameters should + * configUSE_TRACE_FACILITY not be set to 1. */ + ( void ) ucQueueType; +#endif + + if( uxItemSize == ( UBaseType_t ) 0 ) + { + /* No RAM was allocated for the queue storage area, but PC head cannot + * be set to NULL because NULL is used as a key to say the queue is used as + * a mutex. Therefore just set pcHead to point to the queue as a benign + * value that is known to be within the memory map. */ +#ifdef VERIFAST /*< stricter casting */ + pxNewQueue->pcHead = ( int8_t * ) ( void * ) pxNewQueue; +#else + pxNewQueue->pcHead = ( int8_t * ) pxNewQueue; +#endif + } + else + { + /* Set the head to the start of the queue storage area. */ +#ifdef VERIFAST /*< stricter casting */ + pxNewQueue->pcHead = ( int8_t * ) ( void * ) pucQueueStorage; +#else + pxNewQueue->pcHead = ( int8_t * ) pucQueueStorage; +#endif + } + + /* Initialise the queue members as described where the queue type is + * defined. */ + pxNewQueue->uxLength = uxQueueLength; + pxNewQueue->uxItemSize = uxItemSize; + /*@close queue_init2(pxNewQueue, _, uxQueueLength, uxItemSize);@*/ +#ifdef VERIFAST /*< void cast of unused return value */ + xQueueGenericReset( pxNewQueue, pdTRUE ); +#else + ( void ) xQueueGenericReset( pxNewQueue, pdTRUE ); +#endif + + #if ( configUSE_TRACE_FACILITY == 1 ) + { + pxNewQueue->ucQueueType = ucQueueType; + } + #endif /* configUSE_TRACE_FACILITY */ + + #if ( configUSE_QUEUE_SETS == 1 ) + { + pxNewQueue->pxQueueSetContainer = NULL; + } + #endif /* configUSE_QUEUE_SETS */ + + traceQUEUE_CREATE( pxNewQueue ); +} + + + QueueHandle_t xQueueGenericCreate( const UBaseType_t uxQueueLength, + const UBaseType_t uxItemSize, + const uint8_t ucQueueType ) + /*@requires 0 < uxQueueLength &*& + 0 < uxItemSize &*& + 0 < uxQueueLength * uxItemSize &*& + uxQueueLength * uxItemSize <= UINT_MAX;@*/ + /*@ensures result == NULL + ? true + : queue(result, _, uxQueueLength, uxItemSize, 0, (uxQueueLength-1), 0, false, nil) &*& + queuelists(result) &*& + result->irqMask |-> _ &*& + result->schedulerSuspend |-> _ &*& + result->locked |-> _;@*/ + { + Queue_t * pxNewQueue; + size_t xQueueSizeInBytes; + uint8_t * pucQueueStorage; + + configASSERT( uxQueueLength > ( UBaseType_t ) 0 ); + + /* Allocate enough space to hold the maximum number of items that + * can be in the queue at any time. It is valid for uxItemSize to be + * zero in the case the queue is used as a semaphore. */ + xQueueSizeInBytes = ( size_t ) ( uxQueueLength * uxItemSize ); /*lint !e961 MISRA exception as the casts are only redundant for some ports. */ + + /* Check for multiplication overflow. */ + configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) ); + +#ifdef VERIFAST /*< ***model single malloc of struct and buffer*** */ + pxNewQueue = ( Queue_t * ) pvPortMalloc( sizeof( Queue_t ) ); +#else + /* Allocate the queue and storage area. Justification for MISRA + * deviation as follows: pvPortMalloc() always ensures returned memory + * blocks are aligned per the requirements of the MCU stack. In this case + * pvPortMalloc() must return a pointer that is guaranteed to meet the + * alignment requirements of the Queue_t structure - which in this case + * is an int8_t *. Therefore, whenever the stack alignment requirements + * are greater than or equal to the pointer to char requirements the cast + * is safe. In other cases alignment requirements are not strict (one or + * two bytes). */ + pxNewQueue = ( Queue_t * ) pvPortMalloc( sizeof( Queue_t ) + xQueueSizeInBytes ); /*lint !e9087 !e9079 see comment above. */ +#endif + + if( pxNewQueue != NULL ) + { +#ifdef VERIFAST /*< ***model single malloc of struct and buffer*** */ + pucQueueStorage = ( uint8_t * ) pvPortMalloc( xQueueSizeInBytes ); + + if( pucQueueStorage == NULL ) + { + vPortFree( pxNewQueue ); + return NULL; + } + + /*@malloc_block_limits(pucQueueStorage);@*/ +#else + /* Jump past the queue structure to find the location of the queue + * storage area. */ + pucQueueStorage = ( uint8_t * ) pxNewQueue; + pucQueueStorage += sizeof( Queue_t ); /*lint !e9016 Pointer arithmetic allowed on char types, especially when it assists conveying intent. */ +#endif + + #if ( configSUPPORT_STATIC_ALLOCATION == 1 ) + { + /* Queues can be created either statically or dynamically, so + * note this task was created dynamically in case it is later + * deleted. */ + pxNewQueue->ucStaticallyAllocated = pdFALSE; + } + #endif /* configSUPPORT_STATIC_ALLOCATION */ + + prvInitialiseNewQueue( uxQueueLength, uxItemSize, pucQueueStorage, ucQueueType, pxNewQueue ); + } + else + { + traceQUEUE_CREATE_FAILED( ucQueueType ); + mtCOVERAGE_TEST_MARKER(); + } + + return pxNewQueue; + } diff --git a/FreeRTOS/Test/VeriFast/queue/prvCopyDataFromQueue.c b/FreeRTOS/Test/VeriFast/queue/prvCopyDataFromQueue.c new file mode 100644 index 000000000..f986a58c2 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/prvCopyDataFromQueue.c @@ -0,0 +1,89 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" + +static void prvCopyDataFromQueue( Queue_t * const pxQueue, + void * const pvBuffer ) +/*@requires queue(pxQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& 0 < K &*& chars(pvBuffer, M, _);@*/ +/*@ensures queue_after_prvCopyDataFromQueue(pxQueue, Storage, N, M, W, (R+1)%N, K, is_locked, abs) &*& + chars(pvBuffer, M, head(abs));@*/ +{ + if( pxQueue->uxItemSize != ( UBaseType_t ) 0 ) + { + /*@assert buffer(Storage, N, M, ?contents);@*/ + /*@mul_mono_l(R, N-1, M);@*/ + pxQueue->u.xQueue.pcReadFrom += pxQueue->uxItemSize; /*lint !e9016 Pointer arithmetic on char types ok, especially in this use case where it is the clearest way of conveying intent. */ + + if( pxQueue->u.xQueue.pcReadFrom >= pxQueue->u.xQueue.pcTail ) /*lint !e946 MISRA exception justified as use of the relational operator is the cleanest solutions. */ + { + /*@div_leq(N, R+1, M);@*/ /* now we know R == N-1 */ + pxQueue->u.xQueue.pcReadFrom = pxQueue->pcHead; + } + else + { + /*@{ + div_lt(R+1, N, M); // now we know R+1 < N + mod_lt(R+1, N); // so, R+1 == (R+1)%N + note(pxQueue->u.xQueue.pcReadFrom == Storage + ((R + 1) * M)); + note( Storage + ((R + 1) * M) == Storage + (((R + 1) % N) * M)); + }@*/ + mtCOVERAGE_TEST_MARKER(); + } + + /*@mod_plus(R+1, K, N);@*/ + /*@mod_mod(R+1, N);@*/ + /*@split_element(Storage, N, M, (R+1)%N);@*/ + /*@assert + buffer(Storage, (R+1)%N, M, ?prefix) &*& + chars(Storage + ((R+1)%N) * M, M, ?element) &*& + buffer(Storage + ((R+1)%N + 1) * M, (N-1-(R+1)%N), M, ?suffix);@*/ +#ifdef VERIFAST /*< void cast of unused return value */ + memcpy( ( void * ) pvBuffer, ( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize ); +#else + ( void ) memcpy( ( void * ) pvBuffer, ( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize ); /*lint !e961 !e418 !e9087 MISRA exception as the casts are only redundant for some ports. Also previous logic ensures a null pointer can only be passed to memcpy() when the count is 0. Cast to void required by function signature and safe as no alignment requirement and copy length specified in bytes. */ +#endif + /*@{ + combine_list_no_change(prefix, element, suffix, (R+1)%N, contents); + join_element(Storage, N, M, (R+1)%N); + length_take(K, contents); + take_length_eq(K, rotate_left((R+1)%N, contents), abs); + deq_value_lemma(K, (R+1)%N, contents, abs); + }@*/ + } +} + +void caller_reinstates_queue_predicate( Queue_t * const pxQueue, + void * const pvBuffer ) +/*@requires queue(pxQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + 0 < K &*& + chars(pvBuffer, M, _);@*/ +/*@ensures + queue(pxQueue, Storage, N, M, W, (R+1)%N, K-1, is_locked, tail(abs)) &*& + chars(pvBuffer, M, head(abs));@*/ +{ + prvCopyDataFromQueue( pxQueue, pvBuffer ); + /*@open queue_after_prvCopyDataFromQueue(pxQueue, Storage, N, M, W, (R+1)%N, K, is_locked, abs);@*/ + /*@assert buffer(Storage, N, M, ?contents);@*/ + pxQueue->uxMessagesWaiting = pxQueue->uxMessagesWaiting - 1; + /*@deq_lemma(K, (R+1)%N, contents, abs, head(abs));@*/ +} diff --git a/FreeRTOS/Test/VeriFast/queue/prvCopyDataToQueue.c b/FreeRTOS/Test/VeriFast/queue/prvCopyDataToQueue.c new file mode 100644 index 000000000..eded6d049 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/prvCopyDataToQueue.c @@ -0,0 +1,186 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" + +static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, + const void * pvItemToQueue, + const BaseType_t xPosition ) +/*@requires queue(pxQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + (K < N || xPosition == queueOVERWRITE) &*& + chars(pvItemToQueue, M, ?x) &*& + (xPosition == queueSEND_TO_BACK || xPosition == queueSEND_TO_FRONT || (xPosition == queueOVERWRITE && N == 1));@*/ +/*@ensures + (xPosition == queueSEND_TO_BACK + ? queue(pxQueue, Storage, N, M, (W+1)%N, R, (K+1), is_locked, append(abs, singleton(x))) + : (xPosition == queueSEND_TO_FRONT + ? (R == 0 + ? queue(pxQueue, Storage, N, M, W, (N-1), (K+1), is_locked, cons(x, abs)) + : queue(pxQueue, Storage, N, M, W, (R-1), (K+1), is_locked, cons(x, abs))) + : xPosition == queueOVERWRITE &*& queue(pxQueue, Storage, N, M, W, R, 1, is_locked, singleton(x))) + ) &*& + chars(pvItemToQueue, M, x);@*/ +{ + BaseType_t xReturn = pdFALSE; + UBaseType_t uxMessagesWaiting; + + /* This function is called from a critical section. */ + + uxMessagesWaiting = pxQueue->uxMessagesWaiting; + + /* The abstract list of list of chars of `Storage` is `contents` */ + /*@assert buffer(Storage, N, M, ?contents);@*/ + if( pxQueue->uxItemSize == ( UBaseType_t ) 0 ) + { + /* This case is unreachable for queues */ + /*@assert false;@*/ + #if ( configUSE_MUTEXES == 1 ) + { + if( pxQueue->uxQueueType == queueQUEUE_IS_MUTEX ) + { + /* The mutex is no longer being held. */ + xReturn = xTaskPriorityDisinherit( pxQueue->u.xSemaphore.xMutexHolder ); + pxQueue->u.xSemaphore.xMutexHolder = NULL; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + #endif /* configUSE_MUTEXES */ + } + else if( xPosition == queueSEND_TO_BACK ) + { +#ifdef VERIFAST /*< void cast of unused return value */ + /* Now we focus the proof on the logical element of the buffer that + * will be updated using the following lemma to split the buffer into 3 + * parts: a prefix, the element we want to update, and the suffix. This + * enables the subsequent memcpy to verify. */ + /*@split_element(Storage, N, M, W);@*/ + /*@assert + buffer(Storage, W, M, ?prefix) &*& + chars(Storage + W * M, M, _) &*& + buffer(Storage + (W + 1) * M, (N-1-W), M, ?suffix);@*/ + memcpy( ( void * ) pxQueue->pcWriteTo, pvItemToQueue, ( size_t ) pxQueue->uxItemSize ); + /* After the update we stitch the buffer back together */ + /*@join_element(Storage, N, M, W);@*/ + /*@combine_list_update(prefix, x, suffix, W, contents);@*/ +#else + ( void ) memcpy( ( void * ) pxQueue->pcWriteTo, pvItemToQueue, ( size_t ) pxQueue->uxItemSize ); /*lint !e961 !e418 !e9087 MISRA exception as the casts are only redundant for some ports, plus previous logic ensures a null pointer can only be passed to memcpy() if the copy size is 0. Cast to void required by function signature and safe as no alignment requirement and copy length specified in bytes. */ +#endif + /*@mul_mono_l(W, N-1, M);@*/ + pxQueue->pcWriteTo += pxQueue->uxItemSize; /*lint !e9016 Pointer arithmetic on char types ok, especially in this use case where it is the clearest way of conveying intent. */ + + if( pxQueue->pcWriteTo >= pxQueue->u.xQueue.pcTail ) /*lint !e946 MISRA exception justified as comparison of pointers is the cleanest solution. */ + { + /*@div_leq(N, W+1, M);@*/ /* now we know W == N-1 so (W+1)%N == 0 */ + pxQueue->pcWriteTo = pxQueue->pcHead; + } + else + { + /*@{ + div_lt(W+1, N, M); // now we know W+1 < N + mod_lt(W+1, N); // so, W+1 == (W+1)%N + note(pxQueue->pcWriteTo == Storage + ((W + 1) * M)); + note( Storage + ((W + 1) * M) == Storage + (((W + 1) % N) * M)); + }@*/ + mtCOVERAGE_TEST_MARKER(); + } + } + else + { +#ifdef VERIFAST /*< void cast of unused return value */ + /*@split_element(Storage, N, M, R);@*/ + /*@assert + buffer(Storage, R, M, ?prefix) &*& + chars(Storage + R * M, M, _) &*& + buffer(Storage + (R + 1) * M, (N-1-R), M, ?suffix);@*/ + memcpy( ( void * ) pxQueue->u.xQueue.pcReadFrom, pvItemToQueue, ( size_t ) pxQueue->uxItemSize ); + /*@join_element(Storage, N, M, R);@*/ + /*@combine_list_update(prefix, x, suffix, R, contents);@*/ +#else + ( void ) memcpy( ( void * ) pxQueue->u.xQueue.pcReadFrom, pvItemToQueue, ( size_t ) pxQueue->uxItemSize ); /*lint !e961 !e9087 !e418 MISRA exception as the casts are only redundant for some ports. Cast to void required by function signature and safe as no alignment requirement and copy length specified in bytes. Assert checks null pointer only used when length is 0. */ +#endif + pxQueue->u.xQueue.pcReadFrom -= pxQueue->uxItemSize; + + if( pxQueue->u.xQueue.pcReadFrom < pxQueue->pcHead ) /*lint !e946 MISRA exception justified as comparison of pointers is the cleanest solution. */ + { + pxQueue->u.xQueue.pcReadFrom = ( pxQueue->u.xQueue.pcTail - pxQueue->uxItemSize ); + /*@{ div_leq(R-1, 0, M); leq_bound(R, 0); }@*/ + /*@assert R == 0;@*/ + /*@assert pxQueue->u.xQueue.pcReadFrom == Storage + (N-1) * M;@*/ + } + else + { + /*@assert 0 < R;@*/ + /*@assert pxQueue->u.xQueue.pcReadFrom == Storage + (R-1) * M;@*/ + mtCOVERAGE_TEST_MARKER(); + } + + /*@ + if (R == 0) + { + mod_plus(N, (K+1), N); mod_same(N); mod_mod(K+1, N); + assert W == ((N-1) + 1 + (K+1)) % N; + } + @*/ + if( xPosition == queueOVERWRITE ) + { + if( uxMessagesWaiting > ( UBaseType_t ) 0 ) + { + /* An item is not being added but overwritten, so subtract + * one from the recorded number of items in the queue so when + * one is added again below the number of recorded items remains + * correct. */ + --uxMessagesWaiting; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + + pxQueue->uxMessagesWaiting = uxMessagesWaiting + ( UBaseType_t ) 1; + + /*@ + if (xPosition == queueSEND_TO_BACK) + { + enq_lemma(K, (R+1)%N, contents, abs, x); + mod_plus_one(W, R + 1 + K, N); + mod_plus_distr(R+1, K, N); + } + else if (xPosition == queueSEND_TO_FRONT) + { + front_enq_lemma(K, R, contents, abs, x); + if (0 < R) + { + mod_lt(R, N); + } + } + @*/ + return xReturn; +} diff --git a/FreeRTOS/Test/VeriFast/queue/prvIsQueueEmpty.c b/FreeRTOS/Test/VeriFast/queue/prvIsQueueEmpty.c new file mode 100644 index 000000000..3dc5000a8 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/prvIsQueueEmpty.c @@ -0,0 +1,49 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" +#define taskENTER_CRITICAL() setInterruptMask( pxQueue ) +#define taskEXIT_CRITICAL() clearInterruptMask( pxQueue ) + +static BaseType_t prvIsQueueEmpty( const Queue_t * pxQueue ) +/*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/ +/*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr);@*/ +{ + BaseType_t xReturn; + + taskENTER_CRITICAL(); + /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + { + if( pxQueue->uxMessagesWaiting == ( UBaseType_t ) 0 ) + { + xReturn = pdTRUE; + } + else + { + xReturn = pdFALSE; + } + } + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + taskEXIT_CRITICAL(); + + return xReturn; +} diff --git a/FreeRTOS/Test/VeriFast/queue/prvIsQueueFull.c b/FreeRTOS/Test/VeriFast/queue/prvIsQueueFull.c new file mode 100644 index 000000000..4e37e2b1c --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/prvIsQueueFull.c @@ -0,0 +1,49 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" +#define taskENTER_CRITICAL() setInterruptMask( pxQueue ) +#define taskEXIT_CRITICAL() clearInterruptMask( pxQueue ) + +static BaseType_t prvIsQueueFull( const Queue_t * pxQueue ) +/*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/ +/*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr);@*/ +{ + BaseType_t xReturn; + + taskENTER_CRITICAL(); + /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + { + if( pxQueue->uxMessagesWaiting == pxQueue->uxLength ) + { + xReturn = pdTRUE; + } + else + { + xReturn = pdFALSE; + } + } + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + taskEXIT_CRITICAL(); + + return xReturn; +} diff --git a/FreeRTOS/Test/VeriFast/queue/prvLockQueue.c b/FreeRTOS/Test/VeriFast/queue/prvLockQueue.c new file mode 100644 index 000000000..32e786beb --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/prvLockQueue.c @@ -0,0 +1,69 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" + +/* In this case we cannot wrap the macro in a function call to give a function + * contract because we require annotations within the macro body, which is not + * supported by VeriFast */ +#define prvLockQueue( pxQueue ) \ + taskENTER_CRITICAL(); \ + { \ + if( ( pxQueue )->cRxLock == queueUNLOCKED ) \ + { \ + ( pxQueue )->cRxLock = queueLOCKED_UNMODIFIED; \ + } \ + if( ( pxQueue )->cTxLock == queueUNLOCKED ) \ + { \ + ( pxQueue )->cTxLock = queueLOCKED_UNMODIFIED; \ + } \ + } \ + taskEXIT_CRITICAL() + +void wrapper_prvLockQueue( QueueHandle_t xQueue ) + +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& + [1/2]queuelock(xQueue);@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]xQueue->locked |-> ?m &*& + mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*& + queue_locked_invariant(xQueue)();@*/ +{ + taskENTER_CRITICAL(); + /*@open queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + { + if( ( xQueue )->cRxLock == queueUNLOCKED ) + { + ( xQueue )->cRxLock = queueLOCKED_UNMODIFIED; + } + + if( ( xQueue )->cTxLock == queueUNLOCKED ) + { + ( xQueue )->cTxLock = queueLOCKED_UNMODIFIED; + } + } + /*@close queue(xQueue, Storage, N, M, W, R, K, true, abs);@*/ + taskEXIT_CRITICAL(); +#ifdef VERIFAST /*< ghost action */ + mutex_acquire( xQueue->locked ); +#endif +} diff --git a/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c b/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c new file mode 100644 index 000000000..079573b2f --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c @@ -0,0 +1,162 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" +#define taskENTER_CRITICAL() setInterruptMask( pxQueue ) +#define taskEXIT_CRITICAL() clearInterruptMask( pxQueue ) + +/* VeriFast: we make one major change. We merge the critical regions for + * decrementing `cTxLock` and `cRxLock`. */ + +static void prvUnlockQueue( Queue_t * const pxQueue ) +/*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& + [1/2]pxQueue->locked |-> ?m &*& + mutex_held(m, queue_locked_invariant(pxQueue), currentThread, 1/2) &*& + queue_locked_invariant(pxQueue)();@*/ +/*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr) &*& + [1/2]queuelock(pxQueue);@*/ +{ + /* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. */ + + /* The lock counts contains the number of extra data items placed or + * removed from the queue while the queue was locked. When a queue is + * locked items can be added or removed, but the event lists cannot be + * updated. */ + taskENTER_CRITICAL(); + /*@open queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, _, ?abs);@*/ + { + int8_t cTxLock = pxQueue->cTxLock; + + /* See if data was added to the queue while it was locked. */ + while( cTxLock > queueLOCKED_UNMODIFIED ) + /*@invariant queuelists(pxQueue);@*/ + { + /* Data was posted while the queue was locked. Are any tasks + * blocked waiting for data to become available? */ + #if ( configUSE_QUEUE_SETS == 1 ) + { + if( pxQueue->pxQueueSetContainer != NULL ) + { + if( prvNotifyQueueSetContainer( pxQueue ) != pdFALSE ) + { + /* The queue is a member of a queue set, and posting to + * the queue set caused a higher priority task to unblock. + * A context switch is required. */ + vTaskMissedYield(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + /* Tasks that are removed from the event list will get + * added to the pending ready list as the scheduler is still + * suspended. */ + if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE ) + { + if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE ) + { + /* The task waiting has a higher priority so record that a + * context switch is required. */ + vTaskMissedYield(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + break; + } + } + } + #else /* configUSE_QUEUE_SETS */ + { + /* Tasks that are removed from the event list will get added to + * the pending ready list as the scheduler is still suspended. */ + if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE ) + { + if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE ) + { + /* The task waiting has a higher priority so record that + * a context switch is required. */ + vTaskMissedYield(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + break; + } + } + #endif /* configUSE_QUEUE_SETS */ + + --cTxLock; + } + + pxQueue->cTxLock = queueUNLOCKED; + } +#ifndef VERIFAST /*< ***merge cTxLock and cRxLock critical regions*** */ + taskEXIT_CRITICAL(); + + /* Do the same for the Rx lock. */ + taskENTER_CRITICAL(); +#endif + { + int8_t cRxLock = pxQueue->cRxLock; + + while( cRxLock > queueLOCKED_UNMODIFIED ) + /*@invariant queuelists(pxQueue);@*/ + { + if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToSend ) ) == pdFALSE ) + { + if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToSend ) ) != pdFALSE ) + { + vTaskMissedYield(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + + --cRxLock; + } + else + { + break; + } + } + + pxQueue->cRxLock = queueUNLOCKED; + } + /*@close queue(pxQueue, Storage, N, M, W, R, K, false, abs);@*/ + taskEXIT_CRITICAL(); +#ifdef VERIFAST /*< ghost action */ + mutex_release( pxQueue->locked ); +#endif +} diff --git a/FreeRTOS/Test/VeriFast/queue/uxQueueMessagesWaiting.c b/FreeRTOS/Test/VeriFast/queue/uxQueueMessagesWaiting.c new file mode 100644 index 000000000..8e94c513f --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/uxQueueMessagesWaiting.c @@ -0,0 +1,69 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" + +/* It may seem that the read of `pxQueue->uxMessagesWaiting` is required to be + * contained in a critical region to be thread-safe. However, it is impossible for + * this read to be involved in a data race due to the atomicity mechanism used by + * tasks and ISRs: masking and enabling interrupts. If we assume (1) a + * uniprocessor system and (2) that higher priority ISRs never call queue API + * functions then masking interrupts ensures *strong isolation* meaning critical + * regions protected by interrupt masking/enabling are isolated from other + * critical regions and code outside of critical regions. */ + +UBaseType_t uxQueueMessagesWaitingFromISR( const QueueHandle_t xQueue ) +/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ +/*@ensures queue(xQueue, Storage, N, M, W, R, K, is_locked, abs) &*& result == K;@*/ +{ + UBaseType_t uxReturn; + +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; +#endif + + configASSERT( pxQueue ); + uxReturn = pxQueue->uxMessagesWaiting; + + return uxReturn; +} + +UBaseType_t uxQueueMessagesWaiting( const QueueHandle_t xQueue ) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr);@*/ +{ + UBaseType_t uxReturn; + + configASSERT( xQueue ); + + taskENTER_CRITICAL(); + { + /*@assert queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + uxReturn = ( ( Queue_t * ) xQueue )->uxMessagesWaiting; + /*@close queue(xQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + } + taskEXIT_CRITICAL(); + + return uxReturn; +} /*lint !e818 Pointer cannot be declared const as xQueue is a typedef not pointer. */ diff --git a/FreeRTOS/Test/VeriFast/queue/uxQueueSpacesAvailable.c b/FreeRTOS/Test/VeriFast/queue/uxQueueSpacesAvailable.c new file mode 100644 index 000000000..5408b15fe --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/uxQueueSpacesAvailable.c @@ -0,0 +1,49 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" + +UBaseType_t uxQueueSpacesAvailable( const QueueHandle_t xQueue ) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr);@*/ +{ + UBaseType_t uxReturn; + +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; +#endif + + configASSERT( pxQueue ); + + taskENTER_CRITICAL(); + /*@assert queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + { + uxReturn = pxQueue->uxLength - pxQueue->uxMessagesWaiting; + /*@assert uxReturn == N - K;@*/ + } + /*@close queue(xQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + taskEXIT_CRITICAL(); + + return uxReturn; +} /*lint !e818 Pointer cannot be declared const as xQueue is a typedef not pointer. */ diff --git a/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c b/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c new file mode 100644 index 000000000..84e97fe59 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c @@ -0,0 +1,80 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" +#define configSUPPORT_DYNAMIC_ALLOCATION 1 +#define configSUPPORT_STATIC_ALLOCATION 0 + +void vQueueDelete( QueueHandle_t xQueue ) +/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + queuelists(xQueue) &*& + xQueue->irqMask |-> _ &*& + xQueue->schedulerSuspend |-> _ &*& + xQueue->locked |-> _;@*/ +/*@ensures true;@*/ +{ +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; +#endif + + configASSERT( pxQueue ); + traceQUEUE_DELETE( pxQueue ); + + #if ( configQUEUE_REGISTRY_SIZE > 0 ) + { + vQueueUnregisterQueue( pxQueue ); + } + #endif + + #if ( ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) && ( configSUPPORT_STATIC_ALLOCATION == 0 ) ) + { + /* The queue can only have been allocated dynamically - free it + * again. */ + vPortFree( pxQueue ); +#ifdef VERIFAST /*< leak ghost state on deletion */ + /*@leak buffer(_, _, _, _);@*/ + /*@leak malloc_block(_, _);@*/ +#endif + } + #elif ( ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) && ( configSUPPORT_STATIC_ALLOCATION == 1 ) ) + { + /* The queue could have been allocated statically or dynamically, so + * check before attempting to free the memory. */ + if( pxQueue->ucStaticallyAllocated == ( uint8_t ) pdFALSE ) + { + vPortFree( pxQueue ); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + #else /* if ( ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) && ( configSUPPORT_STATIC_ALLOCATION == 0 ) ) */ + { + /* The queue must have been statically allocated, so is not going to be + * deleted. Avoid compiler warnings about the unused parameter. */ + ( void ) pxQueue; + } + #endif /* configSUPPORT_DYNAMIC_ALLOCATION */ +} diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c b/FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c new file mode 100644 index 000000000..330ab005c --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c @@ -0,0 +1,285 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" +#include "proof/queuecontracts.h" + +BaseType_t xQueueGenericSend( QueueHandle_t xQueue, + const void * const pvItemToQueue, + TickType_t xTicksToWait, + const BaseType_t xCopyPosition ) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& + [1/2]queuesuspend(xQueue) &*& + chars(pvItemToQueue, M, ?x) &*& + (xCopyPosition == queueSEND_TO_BACK || xCopyPosition == queueSEND_TO_FRONT || (xCopyPosition == queueOVERWRITE && N == 1));@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]queuesuspend(xQueue) &*& + chars(pvItemToQueue, M, x);@*/ +{ + BaseType_t xEntryTimeSet = pdFALSE, xYieldRequired; + TimeOut_t xTimeOut; +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; + + configASSERT( pxQueue ); + configASSERT( !( ( pvItemToQueue == NULL ) && ( pxQueue->uxItemSize != ( UBaseType_t ) 0U ) ) ); + configASSERT( !( ( xCopyPosition == queueOVERWRITE ) && ( pxQueue->uxLength != 1 ) ) ); + #if ( ( INCLUDE_xTaskGetSchedulerState == 1 ) || ( configUSE_TIMERS == 1 ) ) + { + configASSERT( !( ( xTaskGetSchedulerState() == taskSCHEDULER_SUSPENDED ) && ( xTicksToWait != 0 ) ) ); + } + #endif +#endif + + /*lint -save -e904 This function relaxes the coding standard somewhat to + * allow return statements within the function itself. This is done in the + * interest of execution time efficiency. */ + for( ; ; ) + /*@invariant [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]queuesuspend(xQueue) &*& + chars(pvItemToQueue, M, x) &*& + u_integer(&xTicksToWait, _) &*& + (xCopyPosition == queueSEND_TO_BACK || xCopyPosition == queueSEND_TO_FRONT || (xCopyPosition == queueOVERWRITE && N == 1)) &*& + xTIME_OUT(&xTimeOut);@*/ + { + taskENTER_CRITICAL(); + { + /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + /* Is there room on the queue now? The running task must be the + * highest priority task wanting to access the queue. If the head item + * in the queue is to be overwritten then it does not matter if the + * queue is full. */ + if( ( pxQueue->uxMessagesWaiting < pxQueue->uxLength ) || ( xCopyPosition == queueOVERWRITE ) ) + { + traceQUEUE_SEND( pxQueue ); + + /* VeriFast: we do not verify this configuration option */ + #if ( configUSE_QUEUE_SETS == 1 ) + { + const UBaseType_t uxPreviousMessagesWaiting = pxQueue->uxMessagesWaiting; + + xYieldRequired = prvCopyDataToQueue( pxQueue, pvItemToQueue, xCopyPosition ); + + if( pxQueue->pxQueueSetContainer != NULL ) + { + if( ( xCopyPosition == queueOVERWRITE ) && ( uxPreviousMessagesWaiting != ( UBaseType_t ) 0 ) ) + { + /* Do not notify the queue set as an existing item + * was overwritten in the queue so the number of items + * in the queue has not changed. */ + mtCOVERAGE_TEST_MARKER(); + } + else if( prvNotifyQueueSetContainer( pxQueue ) != pdFALSE ) + { + /* The queue is a member of a queue set, and posting + * to the queue set caused a higher priority task to + * unblock. A context switch is required. */ + queueYIELD_IF_USING_PREEMPTION(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + /* If there was a task waiting for data to arrive on the + * queue then unblock it now. */ + if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE ) + { + if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE ) + { + /* The unblocked task has a priority higher than + * our own so yield immediately. Yes it is ok to + * do this from within the critical section - the + * kernel takes care of that. */ + queueYIELD_IF_USING_PREEMPTION(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else if( xYieldRequired != pdFALSE ) + { + /* This path is a special case that will only get + * executed if the task was holding multiple mutexes + * and the mutexes were given back in an order that is + * different to that in which they were taken. */ + queueYIELD_IF_USING_PREEMPTION(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + } + #else /* configUSE_QUEUE_SETS */ + { + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + xYieldRequired = prvCopyDataToQueue( pxQueue, pvItemToQueue, xCopyPosition ); + + /* If there was a task waiting for data to arrive on the + * queue then unblock it now. */ + if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE ) + { + if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE ) + { + /* The unblocked task has a priority higher than + * our own so yield immediately. Yes it is ok to do + * this from within the critical section - the kernel + * takes care of that. */ + queueYIELD_IF_USING_PREEMPTION(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else if( xYieldRequired != pdFALSE ) + { + /* This path is a special case that will only get + * executed if the task was holding multiple mutexes and + * the mutexes were given back in an order that is + * different to that in which they were taken. */ + queueYIELD_IF_USING_PREEMPTION(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + #endif /* configUSE_QUEUE_SETS */ + + /*@ + if (xCopyPosition == queueSEND_TO_BACK) + { + close queue(pxQueue, Storage, N, M, (W+1)%N, R, (K+1), is_locked, append(abs, singleton(x))); + } + else if (xCopyPosition == queueSEND_TO_FRONT) + { + close queue(pxQueue, Storage, N, M, W, (R == 0 ? (N-1) : (R-1)), (K+1), is_locked, cons(x, abs)); + } + else if (xCopyPosition == queueOVERWRITE) + { + close queue(pxQueue, Storage, N, M, W, R, 1, is_locked, singleton(x)); + } + @*/ + taskEXIT_CRITICAL(); + return pdPASS; + } + else + { + if( xTicksToWait == ( TickType_t ) 0 ) + { + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + /* The queue was full and no block time is specified (or + * the block time has expired) so leave now. */ + taskEXIT_CRITICAL(); + + /* Return to the original privilege level before exiting + * the function. */ + traceQUEUE_SEND_FAILED( pxQueue ); + return errQUEUE_FULL; + } + else if( xEntryTimeSet == pdFALSE ) + { + /* The queue was full and a block time was specified so + * configure the timeout structure. */ + vTaskInternalSetTimeOutState( &xTimeOut ); + xEntryTimeSet = pdTRUE; + } + else + { + /* Entry time was already set. */ + mtCOVERAGE_TEST_MARKER(); + } + } + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + } + taskEXIT_CRITICAL(); + + /* Interrupts and other tasks can send to and receive from the queue + * now the critical section has been exited. */ + + /*@close exists(pxQueue);@*/ + vTaskSuspendAll(); + prvLockQueue( pxQueue ); + + /* Update the timeout state to see if it has expired yet. */ + if( xTaskCheckForTimeOut( &xTimeOut, &xTicksToWait ) == pdFALSE ) + { + if( prvIsQueueFull( pxQueue ) != pdFALSE ) + { + traceBLOCKING_ON_QUEUE_SEND( pxQueue ); + /*@open queue_locked_invariant(xQueue)();@*/ + vTaskPlaceOnEventList( &( pxQueue->xTasksWaitingToSend ), xTicksToWait ); + + /* Unlocking the queue means queue events can effect the + * event list. It is possible that interrupts occurring now + * remove this task from the event list again - but as the + * scheduler is suspended the task will go onto the pending + * ready last instead of the actual ready list. */ + /*@close queue_locked_invariant(xQueue)();@*/ + prvUnlockQueue( pxQueue ); + + /* Resuming the scheduler will move tasks from the pending + * ready list into the ready list - so it is feasible that this + * task is already in a ready list before it yields - in which + * case the yield will not cause a context switch unless there + * is also a higher priority task in the pending ready list. */ + /*@close exists(pxQueue);@*/ + if( xTaskResumeAll() == pdFALSE ) + { + portYIELD_WITHIN_API(); + } + } + else + { + /* Try again. */ + prvUnlockQueue( pxQueue ); +#ifdef VERIFAST /*< void cast of unused return value */ + /*@close exists(pxQueue);@*/ + xTaskResumeAll(); +#else + ( void ) xTaskResumeAll(); +#endif + } + } + else + { + /* The timeout has expired. */ + prvUnlockQueue( pxQueue ); +#ifdef VERIFAST /*< void cast of unused return value */ + /*@close exists(pxQueue);@*/ + xTaskResumeAll(); +#else + ( void ) xTaskResumeAll(); +#endif + + traceQUEUE_SEND_FAILED( pxQueue ); + return errQUEUE_FULL; + } + } /*lint -restore */ +} diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c new file mode 100644 index 000000000..2baa7e5e8 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c @@ -0,0 +1,235 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" +#include "proof/queuecontracts.h" + +BaseType_t xQueueGenericSendFromISR( QueueHandle_t xQueue, + const void * const pvItemToQueue, + BaseType_t * const pxHigherPriorityTaskWoken, + const BaseType_t xCopyPosition ) +/*@requires + [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == true &*& + chars(pvItemToQueue, M, ?x) &*& + integer(pxHigherPriorityTaskWoken, _) &*& + (xCopyPosition == queueSEND_TO_BACK || xCopyPosition == queueSEND_TO_FRONT || (xCopyPosition == queueOVERWRITE && N == 1));@*/ +/*@ensures + [1/2]queuehandle(xQueue, N, M, is_isr) &*& + chars(pvItemToQueue, M, x) &*& + integer(pxHigherPriorityTaskWoken, _);@*/ +{ + BaseType_t xReturn; + UBaseType_t uxSavedInterruptStatus; + +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; + + configASSERT( pxQueue ); + configASSERT( !( ( pvItemToQueue == NULL ) && ( pxQueue->uxItemSize != ( UBaseType_t ) 0U ) ) ); + configASSERT( !( ( xCopyPosition == queueOVERWRITE ) && ( pxQueue->uxLength != 1 ) ) ); +#endif + + /* RTOS ports that support interrupt nesting have the concept of a maximum + * system call (or maximum API call) interrupt priority. Interrupts that are + * above the maximum system call priority are kept permanently enabled, even + * when the RTOS kernel is in a critical section, but cannot make any calls to + * FreeRTOS API functions. If configASSERT() is defined in FreeRTOSConfig.h + * then portASSERT_IF_INTERRUPT_PRIORITY_INVALID() will result in an assertion + * failure if a FreeRTOS API function is called from an interrupt that has been + * assigned a priority above the configured maximum system call priority. + * Only FreeRTOS functions that end in FromISR can be called from interrupts + * that have been assigned a priority at or (logically) below the maximum + * system call interrupt priority. FreeRTOS maintains a separate interrupt + * safe API to ensure interrupt entry is as fast and as simple as possible. + * More information (albeit Cortex-M specific) is provided on the following + * link: http://www.freertos.org/RTOS-Cortex-M3-M4.html */ + portASSERT_IF_INTERRUPT_PRIORITY_INVALID(); + + /* Similar to xQueueGenericSend, except without blocking if there is no room + * in the queue. Also don't directly wake a task that was blocked on a queue + * read, instead return a flag to say whether a context switch is required or + * not (i.e. has a task with a higher priority than us been woken by this + * post). */ + uxSavedInterruptStatus = portSET_INTERRUPT_MASK_FROM_ISR(); + /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + { + if( ( pxQueue->uxMessagesWaiting < pxQueue->uxLength ) || ( xCopyPosition == queueOVERWRITE ) ) + { + const int8_t cTxLock = pxQueue->cTxLock; + const UBaseType_t uxPreviousMessagesWaiting = pxQueue->uxMessagesWaiting; + + traceQUEUE_SEND_FROM_ISR( pxQueue ); + + /* Semaphores use xQueueGiveFromISR(), so pxQueue will not be a + * semaphore or mutex. That means prvCopyDataToQueue() cannot result + * in a task disinheriting a priority and prvCopyDataToQueue() can be + * called here even though the disinherit function does not check if + * the scheduler is suspended before accessing the ready lists. */ +#ifdef VERIFAST /*< void cast of unused return value */ + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + prvCopyDataToQueue( pxQueue, pvItemToQueue, xCopyPosition ); +#else + ( void ) prvCopyDataToQueue( pxQueue, pvItemToQueue, xCopyPosition ); +#endif + /*@open queue(pxQueue, _, N, M, _, _, _, _, _);@*/ + + /* The event list is not altered if the queue is locked. This will + * be done when the queue is unlocked later. */ + if( cTxLock == queueUNLOCKED ) + { + /* VeriFast: we do not verify this configuration option */ + #if ( configUSE_QUEUE_SETS == 1 ) + { + if( pxQueue->pxQueueSetContainer != NULL ) + { + if( ( xCopyPosition == queueOVERWRITE ) && ( uxPreviousMessagesWaiting != ( UBaseType_t ) 0 ) ) + { + /* Do not notify the queue set as an existing item + * was overwritten in the queue so the number of items + * in the queue has not changed. */ + mtCOVERAGE_TEST_MARKER(); + } + else if( prvNotifyQueueSetContainer( pxQueue ) != pdFALSE ) + { + /* The queue is a member of a queue set, and posting + * to the queue set caused a higher priority task to + * unblock. A context switch is required. */ + if( pxHigherPriorityTaskWoken != NULL ) + { + *pxHigherPriorityTaskWoken = pdTRUE; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE ) + { + if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE ) + { + /* The task waiting has a higher priority so + * record that a context switch is required. */ + if( pxHigherPriorityTaskWoken != NULL ) + { + *pxHigherPriorityTaskWoken = pdTRUE; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + } + #else /* configUSE_QUEUE_SETS */ + { + if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE ) + { + if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE ) + { + /* The task waiting has a higher priority so record that a + * context switch is required. */ + if( pxHigherPriorityTaskWoken != NULL ) + { + *pxHigherPriorityTaskWoken = pdTRUE; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + + /* Not used in this path. */ +#ifndef VERIFAST /*< void cast of unused var */ + ( void ) uxPreviousMessagesWaiting; +#endif + } + #endif /* configUSE_QUEUE_SETS */ + } + else + { + /* Increment the lock count so the task that unlocks the queue + * knows that data was posted while it was locked. */ + configASSERT( cTxLock != queueINT8_MAX ); + + pxQueue->cTxLock = ( int8_t ) ( cTxLock + 1 ); + } + + xReturn = pdPASS; + /*@ + if (xCopyPosition == queueSEND_TO_BACK) + { + close queue(pxQueue, Storage, N, M, (W+1)%N, R, (K+1), is_locked, append(abs, singleton(x))); + } + else if (xCopyPosition == queueSEND_TO_FRONT) + { + if (R == 0) + { + close queue(pxQueue, Storage, N, M, W, (N-1), (K+1), is_locked, cons(x, abs)); + } + else + { + close queue(pxQueue, Storage, N, M, W, (R-1), (K+1), is_locked, cons(x, abs)); + } + } else if (xCopyPosition == queueOVERWRITE) + { + close queue(pxQueue, Storage, N, M, W, R, 1, is_locked, singleton(x)); + } + @*/ + } + else + { + traceQUEUE_SEND_FROM_ISR_FAILED( pxQueue ); + xReturn = errQUEUE_FULL; + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + } + } + portCLEAR_INTERRUPT_MASK_FROM_ISR( uxSavedInterruptStatus ); + + return xReturn; +} diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueEmptyFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueEmptyFromISR.c new file mode 100644 index 000000000..5c859fab2 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueEmptyFromISR.c @@ -0,0 +1,50 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" + +BaseType_t xQueueIsQueueEmptyFromISR( const QueueHandle_t xQueue ) +/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ +/*@ensures queue(xQueue, Storage, N, M, W, R, K, is_locked, abs) &*& + result == ((K == 0) ? pdTRUE : pdFALSE);@*/ +{ + BaseType_t xReturn; + +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; +#endif + + configASSERT( pxQueue ); + + if( pxQueue->uxMessagesWaiting == ( UBaseType_t ) 0 ) + { + xReturn = pdTRUE; + } + else + { + xReturn = pdFALSE; + } + + return xReturn; +} /*lint !e818 xQueue could not be pointer to const because it is a typedef. */ diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c new file mode 100644 index 000000000..9ea51b756 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c @@ -0,0 +1,50 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" + +BaseType_t xQueueIsQueueFullFromISR( const QueueHandle_t xQueue ) +/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ +/*@ensures queue(xQueue, Storage, N, M, W, R, K, is_locked, abs) &*& + result == ((K == N) ? pdTRUE : pdFALSE);@*/ +{ + BaseType_t xReturn; + +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; +#endif + + configASSERT( pxQueue ); + + if( pxQueue->uxMessagesWaiting == pxQueue->uxLength ) + { + xReturn = pdTRUE; + } + else + { + xReturn = pdFALSE; + } + + return xReturn; +} /*lint !e818 xQueue could not be pointer to const because it is a typedef. */ diff --git a/FreeRTOS/Test/VeriFast/queue/xQueuePeek.c b/FreeRTOS/Test/VeriFast/queue/xQueuePeek.c new file mode 100644 index 000000000..1ef4edb7d --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/xQueuePeek.c @@ -0,0 +1,208 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" +#include "proof/queuecontracts.h" + +BaseType_t xQueuePeek( QueueHandle_t xQueue, + void * const pvBuffer, + TickType_t xTicksToWait ) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& + [1/2]queuesuspend(xQueue) &*& + chars(pvBuffer, M, ?x);@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]queuesuspend(xQueue) &*& + (result == pdPASS ? chars(pvBuffer, M, _) : chars(pvBuffer, M, x));@*/ +{ + BaseType_t xEntryTimeSet = pdFALSE; + TimeOut_t xTimeOut; + int8_t * pcOriginalReadPosition; +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; + + /* Check the pointer is not NULL. */ + configASSERT( ( pxQueue ) ); + + /* The buffer into which data is received can only be NULL if the data size + * is zero (so no data is copied into the buffer. */ + configASSERT( !( ( ( pvBuffer ) == NULL ) && ( ( pxQueue )->uxItemSize != ( UBaseType_t ) 0U ) ) ); + + /* Cannot block if the scheduler is suspended. */ + #if ( ( INCLUDE_xTaskGetSchedulerState == 1 ) || ( configUSE_TIMERS == 1 ) ) + { + configASSERT( !( ( xTaskGetSchedulerState() == taskSCHEDULER_SUSPENDED ) && ( xTicksToWait != 0 ) ) ); + } + #endif +#endif + + /*lint -save -e904 This function relaxes the coding standard somewhat to + * allow return statements within the function itself. This is done in the + * interest of execution time efficiency. */ + for( ; ; ) + /*@invariant [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]queuesuspend(xQueue) &*& + chars(pvBuffer, M, x) &*& + u_integer(&xTicksToWait, _) &*& + xTIME_OUT(&xTimeOut);@*/ + { + taskENTER_CRITICAL(); + /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + { + const UBaseType_t uxMessagesWaiting = pxQueue->uxMessagesWaiting; + + /* Is there data in the queue now? To be running the calling task + * must be the highest priority task wanting to access the queue. */ + if( uxMessagesWaiting > ( UBaseType_t ) 0 ) + { + /* Remember the read position so it can be reset after the data + * is read from the queue as this function is only peeking the + * data, not removing it. */ + pcOriginalReadPosition = pxQueue->u.xQueue.pcReadFrom; + + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + prvCopyDataFromQueue( pxQueue, pvBuffer ); + traceQUEUE_PEEK( pxQueue ); + + /* The data is not being removed, so reset the read pointer. */ + pxQueue->u.xQueue.pcReadFrom = pcOriginalReadPosition; + + /* The data is being left in the queue, so see if there are + * any other tasks waiting for the data. */ + if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE ) + { + if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE ) + { + /* The task waiting has a higher priority than this task. */ + queueYIELD_IF_USING_PREEMPTION(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + taskEXIT_CRITICAL(); + return pdPASS; + } + else + { + if( xTicksToWait == ( TickType_t ) 0 ) + { + /* The queue was empty and no block time is specified (or + * the block time has expired) so leave now. */ + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + taskEXIT_CRITICAL(); + traceQUEUE_PEEK_FAILED( pxQueue ); + return errQUEUE_EMPTY; + } + else if( xEntryTimeSet == pdFALSE ) + { + /* The queue was empty and a block time was specified so + * configure the timeout structure ready to enter the blocked + * state. */ + vTaskInternalSetTimeOutState( &xTimeOut ); + xEntryTimeSet = pdTRUE; + } + else + { + /* Entry time was already set. */ + mtCOVERAGE_TEST_MARKER(); + } + } + } + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + taskEXIT_CRITICAL(); + + /* Interrupts and other tasks can send to and receive from the queue + * now the critical section has been exited. */ + + /*@close exists<QueueHandle_t>(pxQueue);@*/ + vTaskSuspendAll(); + prvLockQueue( pxQueue ); + + /* Update the timeout state to see if it has expired yet. */ + if( xTaskCheckForTimeOut( &xTimeOut, &xTicksToWait ) == pdFALSE ) + { + /* Timeout has not expired yet, check to see if there is data in the + * queue now, and if not enter the Blocked state to wait for data. */ + if( prvIsQueueEmpty( pxQueue ) != pdFALSE ) + { + traceBLOCKING_ON_QUEUE_PEEK( pxQueue ); + /*@open queue_locked_invariant(xQueue)();@*/ + vTaskPlaceOnEventList( &( pxQueue->xTasksWaitingToReceive ), xTicksToWait ); + /*@close queue_locked_invariant(xQueue)();@*/ + prvUnlockQueue( pxQueue ); + + /*@close exists<QueueHandle_t>(pxQueue);@*/ + if( xTaskResumeAll() == pdFALSE ) + { + portYIELD_WITHIN_API(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + /* There is data in the queue now, so don't enter the blocked + * state, instead return to try and obtain the data. */ + prvUnlockQueue( pxQueue ); +#ifdef VERIFAST /*< void cast of unused return value */ + /*@close exists<QueueHandle_t>(pxQueue);@*/ + xTaskResumeAll(); +#else + ( void ) xTaskResumeAll(); +#endif + } + } + else + { + /* The timeout has expired. If there is still no data in the queue + * exit, otherwise go back and try to read the data again. */ + prvUnlockQueue( pxQueue ); +#ifdef VERIFAST /*< void cast of unused return value */ + /*@close exists<QueueHandle_t>(pxQueue);@*/ + xTaskResumeAll(); +#else + ( void ) xTaskResumeAll(); +#endif + + if( prvIsQueueEmpty( pxQueue ) != pdFALSE ) + { + traceQUEUE_PEEK_FAILED( pxQueue ); + return errQUEUE_EMPTY; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + } /*lint -restore */ +} diff --git a/FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c new file mode 100644 index 000000000..0eb22ce62 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c @@ -0,0 +1,90 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" +#include "proof/queuecontracts.h" + +BaseType_t xQueuePeekFromISR( QueueHandle_t xQueue, + void * const pvBuffer ) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == true &*& + chars(pvBuffer, M, ?x);@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& + (result == pdPASS ? chars(pvBuffer, M, _) : chars(pvBuffer, M, x));@*/ +{ + BaseType_t xReturn; + UBaseType_t uxSavedInterruptStatus; + int8_t * pcOriginalReadPosition; +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; + + configASSERT( pxQueue ); + configASSERT( !( ( pvBuffer == NULL ) && ( pxQueue->uxItemSize != ( UBaseType_t ) 0U ) ) ); + configASSERT( pxQueue->uxItemSize != 0 ); /* Can't peek a semaphore. */ +#endif + + /* RTOS ports that support interrupt nesting have the concept of a maximum + * system call (or maximum API call) interrupt priority. Interrupts that are + * above the maximum system call priority are kept permanently enabled, even + * when the RTOS kernel is in a critical section, but cannot make any calls to + * FreeRTOS API functions. If configASSERT() is defined in FreeRTOSConfig.h + * then portASSERT_IF_INTERRUPT_PRIORITY_INVALID() will result in an assertion + * failure if a FreeRTOS API function is called from an interrupt that has been + * assigned a priority above the configured maximum system call priority. + * Only FreeRTOS functions that end in FromISR can be called from interrupts + * that have been assigned a priority at or (logically) below the maximum + * system call interrupt priority. FreeRTOS maintains a separate interrupt + * safe API to ensure interrupt entry is as fast and as simple as possible. + * More information (albeit Cortex-M specific) is provided on the following + * link: http://www.freertos.org/RTOS-Cortex-M3-M4.html */ + portASSERT_IF_INTERRUPT_PRIORITY_INVALID(); + + uxSavedInterruptStatus = portSET_INTERRUPT_MASK_FROM_ISR(); + /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + { + /* Cannot block in an ISR, so check there is data available. */ + if( pxQueue->uxMessagesWaiting > ( UBaseType_t ) 0 ) + { + traceQUEUE_PEEK_FROM_ISR( pxQueue ); + + /* Remember the read position so it can be reset as nothing is + * actually being removed from the queue. */ + pcOriginalReadPosition = pxQueue->u.xQueue.pcReadFrom; + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + prvCopyDataFromQueue( pxQueue, pvBuffer ); + pxQueue->u.xQueue.pcReadFrom = pcOriginalReadPosition; + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + + xReturn = pdPASS; + } + else + { + xReturn = pdFAIL; + traceQUEUE_PEEK_FROM_ISR_FAILED( pxQueue ); + } + } + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + portCLEAR_INTERRUPT_MASK_FROM_ISR( uxSavedInterruptStatus ); + + return xReturn; +} diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueReceive.c b/FreeRTOS/Test/VeriFast/queue/xQueueReceive.c new file mode 100644 index 000000000..804f62a52 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/xQueueReceive.c @@ -0,0 +1,206 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" +#include "proof/queuecontracts.h" + +BaseType_t xQueueReceive( QueueHandle_t xQueue, + void * const pvBuffer, + TickType_t xTicksToWait ) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& + [1/2]queuesuspend(xQueue) &*& + chars(pvBuffer, M, ?x);@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]queuesuspend(xQueue) &*& + (result == pdPASS ? chars(pvBuffer, M, _) : chars(pvBuffer, M, x));@*/ +{ + BaseType_t xEntryTimeSet = pdFALSE; + TimeOut_t xTimeOut; +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; + + /* Check the pointer is not NULL. */ + configASSERT( ( pxQueue ) ); + + /* The buffer into which data is received can only be NULL if the data size + * is zero (so no data is copied into the buffer). */ + configASSERT( !( ( ( pvBuffer ) == NULL ) && ( ( pxQueue )->uxItemSize != ( UBaseType_t ) 0U ) ) ); + + /* Cannot block if the scheduler is suspended. */ + #if ( ( INCLUDE_xTaskGetSchedulerState == 1 ) || ( configUSE_TIMERS == 1 ) ) + { + configASSERT( !( ( xTaskGetSchedulerState() == taskSCHEDULER_SUSPENDED ) && ( xTicksToWait != 0 ) ) ); + } + #endif +#endif + + /*lint -save -e904 This function relaxes the coding standard somewhat to + * allow return statements within the function itself. This is done in the + * interest of execution time efficiency. */ + for( ; ; ) + /*@invariant [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]queuesuspend(xQueue) &*& + chars(pvBuffer, M, x) &*& + u_integer(&xTicksToWait, _) &*& + xTIME_OUT(&xTimeOut);@*/ + { + taskENTER_CRITICAL(); + /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + { + const UBaseType_t uxMessagesWaiting = pxQueue->uxMessagesWaiting; + + /* Is there data in the queue now? To be running the calling task + * must be the highest priority task wanting to access the queue. */ + if( uxMessagesWaiting > ( UBaseType_t ) 0 ) + { + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + /* Data available, remove one item. */ + prvCopyDataFromQueue( pxQueue, pvBuffer ); + /*@open queue_after_prvCopyDataFromQueue(pxQueue, Storage, N, M, W, (R+1)%N, K, is_locked, abs);@*/ + traceQUEUE_RECEIVE( pxQueue ); + pxQueue->uxMessagesWaiting = uxMessagesWaiting - ( UBaseType_t ) 1; + + /*@assert + pxQueue->pcHead |-> ?buffer &*& + buffer(buffer, N, M, ?contents);@*/ + /*@deq_lemma(K, (R+1)%N, contents, abs, head(abs));@*/ + /* There is now space in the queue, were any tasks waiting to + * post to the queue? If so, unblock the highest priority waiting + * task. */ + if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToSend ) ) == pdFALSE ) + { + if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToSend ) ) != pdFALSE ) + { + queueYIELD_IF_USING_PREEMPTION(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + + /*@close queue(pxQueue, Storage, N, M, W, (R+1)%N, K-1, is_locked, tail(abs));@*/ + /*@assert chars(pvBuffer, M, head(abs));@*/ + taskEXIT_CRITICAL(); + return pdPASS; + } + else + { + if( xTicksToWait == ( TickType_t ) 0 ) + { + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + /* The queue was empty and no block time is specified (or + * the block time has expired) so leave now. */ + taskEXIT_CRITICAL(); + traceQUEUE_RECEIVE_FAILED( pxQueue ); + return errQUEUE_EMPTY; + } + else if( xEntryTimeSet == pdFALSE ) + { + /* The queue was empty and a block time was specified so + * configure the timeout structure. */ + vTaskInternalSetTimeOutState( &xTimeOut ); + xEntryTimeSet = pdTRUE; + } + else + { + /* Entry time was already set. */ + mtCOVERAGE_TEST_MARKER(); + } + } + } + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + taskEXIT_CRITICAL(); + + /* Interrupts and other tasks can send to and receive from the queue + * now the critical section has been exited. */ + + /*@close exists(pxQueue);@*/ + vTaskSuspendAll(); + prvLockQueue( pxQueue ); + + /* Update the timeout state to see if it has expired yet. */ + if( xTaskCheckForTimeOut( &xTimeOut, &xTicksToWait ) == pdFALSE ) + { + /* The timeout has not expired. If the queue is still empty place + * the task on the list of tasks waiting to receive from the queue. */ + if( prvIsQueueEmpty( pxQueue ) != pdFALSE ) + { + traceBLOCKING_ON_QUEUE_RECEIVE( pxQueue ); + /*@open queue_locked_invariant(xQueue)();@*/ + vTaskPlaceOnEventList( &( pxQueue->xTasksWaitingToReceive ), xTicksToWait ); + /*@close queue_locked_invariant(xQueue)();@*/ + prvUnlockQueue( pxQueue ); + + /*@close exists(pxQueue);@*/ + if( xTaskResumeAll() == pdFALSE ) + { + portYIELD_WITHIN_API(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + /* The queue contains data again. Loop back to try and read the + * data. */ + prvUnlockQueue( pxQueue ); +#ifdef VERIFAST /*< void cast of unused return value */ + /*@close exists(pxQueue);@*/ + xTaskResumeAll(); +#else + ( void ) xTaskResumeAll(); +#endif + } + } + else + { + /* Timed out. If there is no data in the queue exit, otherwise loop + * back and attempt to read the data. */ + prvUnlockQueue( pxQueue ); +#ifdef VERIFAST /*< void cast of unused return value */ + /*@close exists(pxQueue);@*/ + xTaskResumeAll(); +#else + ( void ) xTaskResumeAll(); +#endif + + if( prvIsQueueEmpty( pxQueue ) != pdFALSE ) + { + traceQUEUE_RECEIVE_FAILED( pxQueue ); + return errQUEUE_EMPTY; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + } /*lint -restore */ +} diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c new file mode 100644 index 000000000..0af8f8e30 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c @@ -0,0 +1,136 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#include "proof/queue.h" +#include "proof/queuecontracts.h" + +BaseType_t xQueueReceiveFromISR( QueueHandle_t xQueue, + void * const pvBuffer, + BaseType_t * const pxHigherPriorityTaskWoken ) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == true &*& + chars(pvBuffer, M, ?x) &*& + pxHigherPriorityTaskWoken == NULL ? true : integer(pxHigherPriorityTaskWoken, _);@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& + (result == pdPASS ? chars(pvBuffer, M, _) : chars(pvBuffer, M, x)) &*& + (pxHigherPriorityTaskWoken == NULL ? true : integer(pxHigherPriorityTaskWoken, _));@*/ +{ + BaseType_t xReturn; + UBaseType_t uxSavedInterruptStatus; +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; + + configASSERT( pxQueue ); + configASSERT( !( ( pvBuffer == NULL ) && ( pxQueue->uxItemSize != ( UBaseType_t ) 0U ) ) ); +#endif + + /* RTOS ports that support interrupt nesting have the concept of a maximum + * system call (or maximum API call) interrupt priority. Interrupts that are + * above the maximum system call priority are kept permanently enabled, even + * when the RTOS kernel is in a critical section, but cannot make any calls to + * FreeRTOS API functions. If configASSERT() is defined in FreeRTOSConfig.h + * then portASSERT_IF_INTERRUPT_PRIORITY_INVALID() will result in an assertion + * failure if a FreeRTOS API function is called from an interrupt that has been + * assigned a priority above the configured maximum system call priority. + * Only FreeRTOS functions that end in FromISR can be called from interrupts + * that have been assigned a priority at or (logically) below the maximum + * system call interrupt priority. FreeRTOS maintains a separate interrupt + * safe API to ensure interrupt entry is as fast and as simple as possible. + * More information (albeit Cortex-M specific) is provided on the following + * link: http://www.freertos.org/RTOS-Cortex-M3-M4.html */ + portASSERT_IF_INTERRUPT_PRIORITY_INVALID(); + + uxSavedInterruptStatus = portSET_INTERRUPT_MASK_FROM_ISR(); + /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + { + const UBaseType_t uxMessagesWaiting = pxQueue->uxMessagesWaiting; + + /* Cannot block in an ISR, so check there is data available. */ + if( uxMessagesWaiting > ( UBaseType_t ) 0 ) + { + const int8_t cRxLock = pxQueue->cRxLock; + + traceQUEUE_RECEIVE_FROM_ISR( pxQueue ); + + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + prvCopyDataFromQueue( pxQueue, pvBuffer ); + /*@open queue_after_prvCopyDataFromQueue(pxQueue, Storage, N, M, W, (R+1)%N, K, is_locked, abs);@*/ + pxQueue->uxMessagesWaiting = uxMessagesWaiting - ( UBaseType_t ) 1; + /*@assert buffer(Storage, N, M, ?contents);@*/ + /*@deq_lemma(K, (R+1)%N, contents, abs, head(abs));@*/ + + /* If the queue is locked the event list will not be modified. + * Instead update the lock count so the task that unlocks the queue + * will know that an ISR has removed data while the queue was + * locked. */ + if( cRxLock == queueUNLOCKED ) + { + if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToSend ) ) == pdFALSE ) + { + if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToSend ) ) != pdFALSE ) + { + /* The task waiting has a higher priority than us so + * force a context switch. */ + if( pxHigherPriorityTaskWoken != NULL ) + { + *pxHigherPriorityTaskWoken = pdTRUE; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + /* Increment the lock count so the task that unlocks the queue + * knows that data was removed while it was locked. */ + configASSERT( cRxLock != queueINT8_MAX ); + + pxQueue->cRxLock = ( int8_t ) ( cRxLock + 1 ); + } + + /*@close queue(pxQueue, Storage, N, M, W, (R+1)%N, K-1, is_locked, tail(abs));@*/ + /*@assert chars(pvBuffer, M, head(abs));@*/ + xReturn = pdPASS; + } + else + { + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + xReturn = pdFAIL; + traceQUEUE_RECEIVE_FROM_ISR_FAILED( pxQueue ); + } + } + portCLEAR_INTERRUPT_MASK_FROM_ISR( uxSavedInterruptStatus ); + + return xReturn; +} diff --git a/FreeRTOS/Test/VeriFast/scripts/annotation_overhead.sh b/FreeRTOS/Test/VeriFast/scripts/annotation_overhead.sh new file mode 100755 index 000000000..3384ea1aa --- /dev/null +++ b/FreeRTOS/Test/VeriFast/scripts/annotation_overhead.sh @@ -0,0 +1,3 @@ +#!/bin/bash -eu + +NO_COVERAGE=1 EXTRA_VERIFAST_ARGS=-stats make queue | grep overhead: | sort | uniq diff --git a/FreeRTOS/Test/VeriFast/scripts/callgraph.md b/FreeRTOS/Test/VeriFast/scripts/callgraph.md new file mode 100644 index 000000000..5316a6121 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/scripts/callgraph.md @@ -0,0 +1,20 @@ +# Generate callgraph + +## Requirements + + - python3 + - pycparser + - graphviz/dot + - [inconsolata](https://fonts.google.com/specimen/Inconsolata) + +## Instructions + +``` +cd scripts +git clone https://github.com/eliben/pycparser.git #< you need this for pycparser's libc headers even if pycparser is installed +mkdir fake_include +touch fake_include/threading.h +gcc -E -I pycparser/utils/fake_libc_include/ -I ../include/ -I fake_include/ ../queue/*.c > out.pp +./callgraph.py > out.dot +dot -Nfontname=inconsolata -Tpng -o callgraph.png out.dot +``` diff --git a/FreeRTOS/Test/VeriFast/scripts/callgraph.py b/FreeRTOS/Test/VeriFast/scripts/callgraph.py new file mode 100755 index 000000000..ca6fa4ee8 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/scripts/callgraph.py @@ -0,0 +1,83 @@ +#!/usr/bin/env python3 + +from __future__ import print_function +from pycparser import c_parser, c_ast, parse_file +import sys + +ignore_callee = set(['mutex_acquire', 'mutex_release']) +ignore_caller = set(['caller_reinstates_queue_predicate']) +proven = [ + 'prvCopyDataFromQueue', + 'prvCopyDataToQueue', + 'prvInitialiseNewQueue', + 'prvIsQueueEmpty', + 'prvIsQueueFull', + 'prvLockQueue', + 'prvUnlockQueue', + 'uxQueueMessagesWaiting', + 'uxQueueSpacesAvailable', + 'vQueueDelete', + 'xQueueGenericCreate', + 'xQueueGenericReset', + 'xQueueGenericSend', + 'xQueueGenericSendFromISR', + 'xQueueIsQueueEmptyFromISR', + 'xQueueIsQueueFullFromISR', + 'xQueuePeek', + 'xQueuePeekFromISR', + 'xQueueReceive', + 'xQueueReceiveFromISR', +] + +modeled = [ + 'setInterruptMask', + 'clearInterruptMask', + 'setInterruptMaskFromISR', + 'clearInterruptMaskFromISR', + 'vTaskSuspendAll', + 'xTaskResumeAll', +] + +CALLMAP = set() + + +class FuncCallVisitor(c_ast.NodeVisitor): + def __init__(self, caller): + self.caller = caller + + def visit_FuncCall(self, node): + callee = node.name.name + if callee not in ignore_callee: + CALLMAP.add((node.name.name, self.caller)) + + +class FuncDefVisitor(c_ast.NodeVisitor): + def visit_FuncDef(self, node): + caller = node.decl.name + if caller in ignore_caller: + return + if caller.startswith('wrapper_'): + caller = caller[8:] + v = FuncCallVisitor(caller) + v.visit(node) + + +def show_func_calls(filename): + ast = parse_file(filename, use_cpp=False) + v = FuncDefVisitor() + v.visit(ast) + + +if __name__ == "__main__": + filename = 'out.pp' + show_func_calls(filename) + print('digraph G {') + print(' rankdir=LR;') + print(' node [style = filled, colorscheme = set13;];') + for f in proven: + print(' %s [fillcolor = 3];' % f) + for f in modeled: + print(' %s [fillcolor = 2];' % f) + for (callee, caller) in CALLMAP: + print(' %s -> %s;' % (callee, caller)) + print('}') diff --git a/FreeRTOS/Test/VeriFast/scripts/diff_files.md b/FreeRTOS/Test/VeriFast/scripts/diff_files.md new file mode 100644 index 000000000..59f62d364 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/scripts/diff_files.md @@ -0,0 +1,40 @@ +# Generate diffs between FreeRTOS source and proofs + +## Requirements + + - python3 + - ctags 5.8 + - diff 3.4+ + - [diff2html](https://diff2html.xyz/) + +## Instructions + +The following will extract per-function files from the original FreeRTOS source +implementation and the proof directory. + + +``` +cd scripts +./generate_diff_files.sh +# will extract to ./FreeRTOS-Kernel/generated and ./queue/generated +``` + +Then use `diff` for a side-by-side comparison. Note that the `--color=always` +flag needs v3.4+: + +``` +diff --color=always --width=$COLUMNS --suppress-common-lines --side-by-side FreeRTOS-Kernel/generated queue/generated | less -r +``` + +Or generate a html report using `diff2html`: + +``` +diff -u FreeRTOS-Kernel/generated queue/generated | diff2html -i stdin +``` + +The expectation is that the proofs make minimal changes to the original source +implementation in the form of: + + - VeriFast annotations `/*@...@*/` and `//*...` + - Additional comments explaining the proof `/*...*/` + - Flagged changes within `#if[n]def VERIFAST` diff --git a/FreeRTOS/Test/VeriFast/scripts/extract.py b/FreeRTOS/Test/VeriFast/scripts/extract.py new file mode 100755 index 000000000..0b74d79a9 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/scripts/extract.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 +from __future__ import print_function +import sys +from enum import Enum + + +class Extractor(object): + @staticmethod + def __parse_ctags(tags_filename): + def convert_excmd(excmd): + assert excmd.endswith(';"') + linenum = excmd[:-2] # remove ';"' + return int(linenum) + result = {} + with open(tags_filename) as f: + for line in f: + if line.startswith('!'): + continue + parts = line.split('\t') + funcname = parts[0] + funcfile = parts[1] + linenum = convert_excmd(parts[2]) + result[funcname] = (funcfile, linenum) + return result + + def __init__(self, tags_filename): + self.map = Extractor.__parse_ctags(tags_filename) + + class State(Enum): + INIT = 0 + HEAD = 1 + BODY = 2 + + def text_of_funcname(self, funcname): + if funcname not in self.map: + return [] + funcfile, linenum = self.map[funcname] + result = [] + state, bracecount = Extractor.State.INIT, 0 + with open(funcfile) as f: + for i, line in enumerate(f, start=1): # ctags counts linenums from 1 + if state == Extractor.State.INIT and linenum <= i: + state = Extractor.State.HEAD + if state == Extractor.State.HEAD: + result.append(line) + lbrace = line.count('{') + rbrace = line.count('}') + bracecount += lbrace + bracecount -= rbrace + if '{' in line: + state = Extractor.State.BODY + continue + if state == Extractor.State.BODY: + result.append(line) + lbrace = line.count('{') + rbrace = line.count('}') + bracecount += lbrace + bracecount -= rbrace + if bracecount == 0: + break + return result + + +if __name__ == "__main__": + if len(sys.argv) != 3: + print("Usage: %s <tagfile> <funcname>" % sys.argv[0]) + sys.exit(1) + tag_filename = sys.argv[1] + funcname = sys.argv[2] + extractor = Extractor('tags') + result = extractor.text_of_funcname(funcname) + print(''.join(result)) + sys.exit(0) diff --git a/FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh b/FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh new file mode 100755 index 000000000..55f9cfbd2 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh @@ -0,0 +1,47 @@ +#!/bin/bash -eu + +FUNCS=( + prvCopyDataFromQueue + prvCopyDataToQueue + prvInitialiseNewQueue + prvIsQueueEmpty + prvIsQueueFull + prvUnlockQueue + uxQueueMessagesWaiting + uxQueueSpacesAvailable + vQueueDelete + xQueueGenericCreate + xQueueGenericReset + xQueueGenericSend + xQueueGenericSendFromISR + xQueueIsQueueEmptyFromISR + xQueueIsQueueFullFromISR + xQueuePeek + xQueuePeekFromISR + xQueueReceive + xQueueReceiveFromISR +) + +if [ ! -d "FreeRTOS-Kernel" ]; then + git clone https://github.com/FreeRTOS/FreeRTOS-Kernel.git +fi +pushd FreeRTOS-Kernel > /dev/null +rm -rf tags generated +ctags --excmd=number queue.c +mkdir generated +for f in ${FUNCS[@]}; do + ../extract.py tags $f > generated/$f.c +done +popd > /dev/null +echo "created: FreeRTOS-Kernel/generated" + +ln -fs ../queue . +pushd queue > /dev/null +rm -rf tags generated +ctags --excmd=number *.c +mkdir generated +for f in ${FUNCS[@]}; do + ../scripts/extract.py tags $f > generated/$f.c +done +popd > /dev/null +echo "created: queue/generated" |
