1 /*
2 * coreMQTT Agent v1.1.0
3 * Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
4 *
5 * Permission is hereby granted, free of charge, to any person obtaining a copy of
6 * this software and associated documentation files (the "Software"), to deal in
7 * the Software without restriction, including without limitation the rights to
8 * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
9 * the Software, and to permit persons to whom the Software is furnished to do so,
10 * subject to the following conditions:
11 *
12 * The above copyright notice and this permission notice shall be included in all
13 * copies or substantial portions of the Software.
14 *
15 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
17 * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
18 * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
19 * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
20 * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
21 */
22
23 /**
24 * @file network_interface_stubs.c
25 * @brief Stubs to mock sending and receiving over a network interface.
26 */
27
28 #include "core_mqtt.h"
29 #include "network_interface_stubs.h"
30
31 /* An exclusive bound on the times that the NetworkInterfaceSendStub will be
32 * invoked before returning a loop terminating value. This is usually defined
33 * in the Makefile of the harnessed function. */
34 #ifndef MAX_NETWORK_SEND_TRIES
35 #define MAX_NETWORK_SEND_TRIES 3
36 #endif
37
38 /* An exclusive bound on the times that the NetworkInterfaceReceiveStub will
39 * return an unbound value. At this value and beyond, the
40 * NetworkInterfaceReceiveStub will return zero on every call. */
41 #ifndef MAX_NETWORK_RECV_TRIES
42 #define MAX_NETWORK_RECV_TRIES 4
43 #endif
44
NetworkInterfaceReceiveStub(NetworkContext_t * pNetworkContext,void * pBuffer,size_t bytesToRecv)45 int32_t NetworkInterfaceReceiveStub( NetworkContext_t * pNetworkContext,
46 void * pBuffer,
47 size_t bytesToRecv )
48 {
49 __CPROVER_assert( pBuffer != NULL,
50 "NetworkInterfaceReceiveStub pBuffer is not NULL." );
51
52 __CPROVER_assert( __CPROVER_w_ok( pBuffer, bytesToRecv ),
53 "NetworkInterfaceReceiveStub pBuffer is writable up to bytesToRecv." );
54
55 __CPROVER_havoc_object( pBuffer );
56
57 int32_t bytesOrError;
58 static size_t tries = 0;
59
60 /* It is a bug for the application defined transport send function to return
61 * more than bytesToRecv. */
62 __CPROVER_assume( bytesOrError <= ( int32_t ) bytesToRecv );
63
64 if( tries < ( MAX_NETWORK_RECV_TRIES - 1 ) )
65 {
66 tries++;
67 }
68 else
69 {
70 bytesOrError = 0;
71 }
72
73 return bytesOrError;
74 }
75
NetworkInterfaceSendStub(NetworkContext_t * pNetworkContext,const void * pBuffer,size_t bytesToSend)76 int32_t NetworkInterfaceSendStub( NetworkContext_t * pNetworkContext,
77 const void * pBuffer,
78 size_t bytesToSend )
79 {
80 __CPROVER_assert( pBuffer != NULL,
81 "NetworkInterfaceSendStub pBuffer is not NULL." );
82
83 /* The number of tries to send the message before this invocation. */
84 static size_t tries = 1;
85
86 int32_t bytesOrError;
87
88 /* It is a bug for the application defined transport send function to return
89 * more than bytesToSend. */
90 __CPROVER_assume( bytesOrError <= ( int32_t ) bytesToSend );
91
92 /* If the maximum tries are reached, then return a timeout. In the MQTT library
93 * this stub is wrapped in a loop that will does not end until the bytesOrError
94 * returned is negative. This means we could loop possibly INT32_MAX
95 * iterations. Looping for INT32_MAX times adds no value to the proof.
96 * What matters is that the MQTT library can handle all the possible values
97 * that could be returned. */
98 if( tries < ( MAX_NETWORK_SEND_TRIES - 1 ) )
99 {
100 tries++;
101 }
102 else
103 {
104 tries = 1;
105 bytesOrError = bytesToSend;
106 }
107
108 return bytesOrError;
109 }
110
