Remove {r,w}_ok from is_valid_IotResponseHandle

This commit attempts to preserve the functionality of the memory
checks in is_valid_IotResponseHandle until the issue in
diffblue/cbmc#5194 is sorted out. This
commit is needed because is_valid_IotRequestHandle and
is_valid_IotResponseHandle use the __CPROVER_r_ok and __CPROVER_w_ok
macros, and they are used inside an assume statement, triggering the
issue mentioned in that bug.

Author: karkhaz

tools/cbmc/proofs/HTTP/global_state_HTTP.c

@@ -272,45 +272,52 @@ initialize_IotResponseHandle(IotHttpsResponseHandle_t pResponseHandle) {
 }
 
 int is_valid_IotResponseHandle(IotHttpsResponseHandle_t pResponseHandle) {
-  int required1 =
+  int valid_headers =
+    pResponseHandle->pHeaders != NULL;
+  int valid_body =
+    pResponseHandle->pBody != NULL;
+
+  int valid_parserdata =
+    pResponseHandle->httpParserInfo.readHeaderParser.data == pResponseHandle;
+
+  size_t header_size = __CPROVER_OBJECT_SIZE(pResponseHandle->pHeaders);
+  bool valid_header_pointers =
+    header_size < CBMC_MAX_OBJECT_SIZE &&
+
+    __CPROVER_POINTER_OFFSET(pResponseHandle->pHeaders) < header_size &&
+    __CPROVER_POINTER_OFFSET(pResponseHandle->pHeadersCur) < header_size &&
+    __CPROVER_POINTER_OFFSET(pResponseHandle->pHeadersEnd) < header_size &&
+
     __CPROVER_same_object(pResponseHandle->pHeaders,
 			  pResponseHandle->pHeadersCur) &&
     __CPROVER_same_object(pResponseHandle->pHeaders,
-			  pResponseHandle->pHeadersEnd);
-  int required2 =
+			  pResponseHandle->pHeadersEnd) &&
+
+    pResponseHandle->pHeaders <= pResponseHandle->pHeadersCur &&
+    pResponseHandle->pHeadersCur <=  pResponseHandle->pHeadersEnd;
+
+  size_t body_size = __CPROVER_OBJECT_SIZE(pResponseHandle->pBody);
+  bool valid_body_pointers =
+    body_size < CBMC_MAX_OBJECT_SIZE &&
+
+    __CPROVER_POINTER_OFFSET(pResponseHandle->pBody) < body_size &&
+    __CPROVER_POINTER_OFFSET(pResponseHandle->pBodyCur) < body_size &&
+    __CPROVER_POINTER_OFFSET(pResponseHandle->pBodyEnd) < body_size &&
+
     __CPROVER_same_object(pResponseHandle->pBody,
 			  pResponseHandle->pBodyCur) &&
     __CPROVER_same_object(pResponseHandle->pBody,
-			  pResponseHandle->pBodyEnd);
-  if (!required1 || !required2) return 0;
+			  pResponseHandle->pBodyEnd) &&
 
-  int valid_headers =
-    pResponseHandle->pHeaders != NULL;
-  int valid_header_order =
-    pResponseHandle->pHeaders <= pResponseHandle->pHeadersCur &&
-    pResponseHandle->pHeadersCur <=  pResponseHandle->pHeadersEnd;
-  int valid_body =
-    pResponseHandle->pBody != NULL;
-  int valid_body_order =
     pResponseHandle->pBody <= pResponseHandle->pBodyCur &&
     pResponseHandle->pBodyCur <=  pResponseHandle->pBodyEnd;
-  int valid_parserdata =
-    pResponseHandle->httpParserInfo.readHeaderParser.data == pResponseHandle;
+
   return
     valid_headers &&
-    valid_header_order &&
     valid_body &&
-    valid_body_order &&
     valid_parserdata &&
-    // valid_order and short circuit evaluation prevents integer overflow
-    __CPROVER_r_ok(pResponseHandle->pHeaders,
-		   pResponseHandle->pHeadersEnd - pResponseHandle->pHeaders) &&
-    __CPROVER_w_ok(pResponseHandle->pHeaders,
-		   pResponseHandle->pHeadersEnd - pResponseHandle->pHeaders) &&
-    __CPROVER_r_ok(pResponseHandle->pBody,
-		   pResponseHandle->pBodyEnd - pResponseHandle->pBody) &&
-    __CPROVER_w_ok(pResponseHandle->pBody,
-		   pResponseHandle->pBodyEnd - pResponseHandle->pBody);
+    valid_header_pointers &&
+    valid_body_pointers;
 }
 
 /****************************************************************
@@ -333,32 +340,30 @@ IotHttpsRequestHandle_t allocate_IotRequestHandle() {
 }
 
 int is_valid_IotRequestHandle(IotHttpsRequestHandle_t pRequestHandle) {
-  int required =
+  int valid_headers = pRequestHandle->pHeaders != NULL;
+  int valid_body = pRequestHandle->pBody != NULL;
+
+  size_t header_size = __CPROVER_OBJECT_SIZE(pRequestHandle->pHeaders);
+
+  bool valid_header_pointers =
+    header_size < CBMC_MAX_OBJECT_SIZE &&
+
+    __CPROVER_POINTER_OFFSET(pRequestHandle->pHeaders) < header_size &&
+    __CPROVER_POINTER_OFFSET(pRequestHandle->pHeadersCur) < header_size &&
+    __CPROVER_POINTER_OFFSET(pRequestHandle->pHeadersEnd) < header_size &&
+
     __CPROVER_same_object(pRequestHandle->pHeaders,
 			  pRequestHandle->pHeadersCur) &&
     __CPROVER_same_object(pRequestHandle->pHeaders,
-			  pRequestHandle->pHeadersEnd);
-  if (!required) return 0;
+			  pRequestHandle->pHeadersEnd) &&
 
-  int valid_headers =
-    pRequestHandle->pHeaders != NULL;
-  int valid_order =
     pRequestHandle->pHeaders <= pRequestHandle->pHeadersCur &&
     pRequestHandle->pHeadersCur <=  pRequestHandle->pHeadersEnd;
-  int valid_body =
-    pRequestHandle->pBody != NULL;
-  int bounded_header_buffer =
-    __CPROVER_OBJECT_SIZE(pRequestHandle->pHeaders) < CBMC_MAX_OBJECT_SIZE;
+
   return
     valid_headers &&
-    valid_order &&
     valid_body &&
-    bounded_header_buffer &&
-    // valid_order and short circuit evaluation prevents integer overflow
-    __CPROVER_r_ok(pRequestHandle->pHeaders,
-		   pRequestHandle->pHeadersEnd - pRequestHandle->pHeaders) &&
-    __CPROVER_w_ok(pRequestHandle->pHeaders,
-		   pRequestHandle->pHeadersEnd - pRequestHandle->pHeaders);
+    valid_header_pointers;
 }
 
 /****************************************************************