summaryrefslogtreecommitdiff
path: root/FreeRTOS-Plus/Test/CBMC/proofs/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/proofs/parsing')
-rw-r--r--FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json21
-rw-r--r--FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c29
-rw-r--r--FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json31
-rw-r--r--FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c62
-rw-r--r--FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json23
-rw-r--r--FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c46
6 files changed, 212 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json
new file mode 100644
index 000000000..9ad1ef4e9
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json
@@ -0,0 +1,21 @@
+{
+ "ENTRY": "ProcessIPPacket",
+ "CBMCFLAGS":
+ [
+ "--unwind 1",
+ "--nondet-static"
+ ],
+ "OBJS":
+ [
+ "$(ENTRY)_harness.goto",
+ "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto"
+ ],
+ "DEF":
+ [
+ "FREERTOS_TCP_ENABLE_VERIFICATION"
+ ],
+ "INC":
+ [
+ "$(FREERTOS)/tools/cbmc/include"
+ ]
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c
new file mode 100644
index 000000000..def244a51
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c
@@ -0,0 +1,29 @@
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "queue.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_IP_Private.h"
+
+/* proof is done separately */
+BaseType_t xProcessReceivedTCPPacket(NetworkBufferDescriptor_t *pxNetworkBuffer) { }
+
+/* proof is done separately */
+BaseType_t xProcessReceivedUDPPacket(NetworkBufferDescriptor_t *pxNetworkBuffer, uint16_t usPort) { }
+
+/* This proof was done before. Hence we assume it to be correct here. */
+void vARPRefreshCacheEntry( const MACAddress_t * pxMACAddress, const uint32_t ulIPAddress ) { }
+
+eFrameProcessingResult_t publicProcessIPPacket( IPPacket_t * const pxIPPacket, NetworkBufferDescriptor_t * const pxNetworkBuffer);
+
+void harness() {
+
+ NetworkBufferDescriptor_t * const pxNetworkBuffer = malloc(sizeof(NetworkBufferDescriptor_t));
+ /* Pointer to the start of the Ethernet frame. It should be able to access the whole Ethernet frame.*/
+ pxNetworkBuffer->pucEthernetBuffer = malloc(ipTOTAL_ETHERNET_FRAME_SIZE);
+ /* Minimum length of the pxNetworkBuffer->xDataLength is at least the size of the IPPacket_t. */
+ __CPROVER_assume(pxNetworkBuffer->xDataLength >= sizeof(IPPacket_t) && pxNetworkBuffer->xDataLength <= ipTOTAL_ETHERNET_FRAME_SIZE);
+ IPPacket_t * const pxIPPacket = malloc(sizeof(IPPacket_t));
+ publicProcessIPPacket(pxIPPacket, pxNetworkBuffer);
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json
new file mode 100644
index 000000000..901a72729
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json
@@ -0,0 +1,31 @@
+{
+ "ENTRY": "ProcessReceivedTCPPacket",
+ "CBMCFLAGS":
+ [
+ "--unwind 1",
+ "--unwindset prvTCPSendRepeated.0:13",
+ "--nondet-static"
+ ],
+ "OBJS":
+ [
+ "$(ENTRY)_harness.goto",
+ "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto"
+ ],
+ "INSTFLAGS":
+ [
+ "--remove-function-body prvSingleStepTCPHeaderOptions",
+ "--remove-function-body prvCheckOptions",
+ "--remove-function-body prvTCPPrepareSend",
+ "--remove-function-body prvTCPReturnPacket",
+ "--remove-function-body prvTCPHandleState"
+ ],
+ "DEF":
+ [
+ "FREERTOS_TCP_ENABLE_VERIFICATION"
+ ],
+ "INC":
+ [
+ "$(FREERTOS)/tools/cbmc/include"
+ ]
+}
+
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
new file mode 100644
index 000000000..bf84ecf05
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
@@ -0,0 +1,62 @@
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "queue.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_TCP_IP.h"
+#include "FreeRTOS_Stream_Buffer.h"
+
+/* This proof assumes FreeRTOS_socket, pxTCPSocketLookup and
+pxGetNetworkBufferWithDescriptor are implemented correctly.
+
+It also assumes prvSingleStepTCPHeaderOptions, prvCheckOptions, prvTCPPrepareSend,
+prvTCPHandleState and prvTCPReturnPacket are correct. These functions are
+proved to be correct separately. */
+
+/* Implementation of safe malloc */
+void *safeMalloc(size_t xWantedSize ){
+ if(xWantedSize == 0){
+ return NULL;
+ }
+ uint8_t byte;
+ return byte ? malloc(xWantedSize) : NULL;
+}
+
+/* Abstraction of FreeRTOS_socket */
+Socket_t FreeRTOS_socket( BaseType_t xDomain, BaseType_t xType, BaseType_t xProtocol) {
+ return safeMalloc(sizeof(FreeRTOS_Socket_t));
+}
+
+/* Abstraction of pxTCPSocketLookup */
+FreeRTOS_Socket_t *pxTCPSocketLookup(uint32_t ulLocalIP, UBaseType_t uxLocalPort, uint32_t ulRemoteIP, UBaseType_t uxRemotePort) {
+ FreeRTOS_Socket_t * xRetSocket = safeMalloc(sizeof(FreeRTOS_Socket_t));
+ if (xRetSocket) {
+ xRetSocket->u.xTCP.txStream = safeMalloc(sizeof(StreamBuffer_t));
+ xRetSocket->u.xTCP.pxPeerSocket = safeMalloc(sizeof(StreamBuffer_t));
+ }
+ return xRetSocket;
+}
+
+/* Abstraction of pxGetNetworkBufferWithDescriptor */
+NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){
+ NetworkBufferDescriptor_t *pxNetworkBuffer = safeMalloc(sizeof(NetworkBufferDescriptor_t));
+ if(pxNetworkBuffer) {
+ pxNetworkBuffer->pucEthernetBuffer = safeMalloc(xRequestedSizeBytes);
+ __CPROVER_assume(pxNetworkBuffer->xDataLength == ipSIZE_OF_ETH_HEADER + sizeof(int32_t));
+ }
+ return pxNetworkBuffer;
+}
+
+void harness() {
+ NetworkBufferDescriptor_t *pxNetworkBuffer = safeMalloc(sizeof(NetworkBufferDescriptor_t));
+ if (pxNetworkBuffer) {
+ pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t));
+ }
+ if (pxNetworkBuffer && pxNetworkBuffer->pucEthernetBuffer) {
+ xProcessReceivedTCPPacket(pxNetworkBuffer);
+
+ }
+
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json
new file mode 100644
index 000000000..017f625f0
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json
@@ -0,0 +1,23 @@
+{
+ "ENTRY": "ProcessReceivedUDPPacket",
+ "MAX_RX_PACKETS":1,
+ "USE_LLMNR":1,
+ "USE_NBNS":1,
+ "CBMCFLAGS":
+ [
+ "--unwind 1",
+ "--nondet-static"
+ ],
+ "OBJS":
+ [
+ "$(ENTRY)_harness.goto",
+ "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_UDP_IP.goto",
+ "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto"
+ ],
+ "DEF":
+ [
+ "ipconfigUDP_MAX_RX_PACKETS={MAX_RX_PACKETS}",
+ "ipconfigUSE_LLMNR={USE_LLMNR}",
+ "ipconfigUSE_NBNS={USE_NBNS}"
+ ]
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c
new file mode 100644
index 000000000..0082e5d61
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c
@@ -0,0 +1,46 @@
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "queue.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_ARP.h"
+#include "FreeRTOS_UDP_IP.h"
+#include "FreeRTOS_TCP_IP.h"
+
+/*This proof assumes that pxUDPSocketLookup is implemented correctly. */
+
+/* This proof was done before. Hence we assume it to be correct here. */
+void vARPRefreshCacheEntry(const MACAddress_t * pxMACAddress, const uint32_t ulIPAddress) { }
+
+/* This proof was done before. Hence we assume it to be correct here. */
+BaseType_t xIsDHCPSocket(Socket_t xSocket) { }
+
+/* This proof was done before. Hence we assume it to be correct here. */
+uint32_t ulDNSHandlePacket(NetworkBufferDescriptor_t *pxNetworkBuffer) { }
+
+/* Implementation of safe malloc */
+void *safeMalloc(size_t xWantedSize) {
+ if(xWantedSize == 0) {
+ return NULL;
+ }
+ uint8_t byte;
+ return byte ? malloc(xWantedSize) : NULL;
+}
+
+/* Abstraction of pxUDPSocketLookup */
+FreeRTOS_Socket_t *pxUDPSocketLookup( UBaseType_t uxLocalPort ) {
+ return safeMalloc(sizeof(FreeRTOS_Socket_t));
+}
+
+void harness() {
+ NetworkBufferDescriptor_t *pxNetworkBuffer = safeMalloc(sizeof(NetworkBufferDescriptor_t));
+ if(pxNetworkBuffer) {
+ pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(UDPPacket_t));
+ }
+ uint16_t usPort;
+ if (pxNetworkBuffer && pxNetworkBuffer->pucEthernetBuffer) {
+ xProcessReceivedUDPPacket(pxNetworkBuffer, usPort);
+ }
+}