Fix CBMC issues with latest version of CBMC (#104)

Fixes new CBMC errors due to harnesses having additions that could overflow, potentially adding to a null pointer, as well as assumptions that did not prevent cases where pointer addition could go out of bounds. Also fixes a coverage reduction with new version.

Author: archigup

test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c

@@ -47,9 +47,8 @@ void findHeaderFieldParserCallback_harness()
                       pResponse->bufferLen > 0 );
 
     __CPROVER_assume( 0 < fieldLen && fieldLen <= MAX_HEADER_FIELD_LENGTH && fieldLen <= pResponse->bufferLen );
-    __CPROVER_assume( fieldOffset < fieldLen );
+    __CPROVER_assume( fieldOffset <= pResponse->bufferLen - fieldLen );
     pFieldLoc = pResponse->pBuffer + fieldOffset;
-    __CPROVER_assume( pFieldLoc + fieldLen < pResponse->pBuffer + pResponse->bufferLen );
 
     __CPROVER_assume( 0 < fieldContextLen && fieldContextLen < CBMC_MAX_OBJECT_SIZE );
     pFindHeaderContext->pField = ( char * ) malloc( fieldContextLen );

test/cbmc/proofs/findHeaderValueParserCallback/findHeaderValueParserCallback_harness.c

@@ -46,12 +46,13 @@ void findHeaderValueParserCallback_harness()
                       pResponse->pBuffer != NULL &&
                       pResponse->bufferLen > 0 );
 
-    __CPROVER_assume( 0 < valueLen && valueLen <= pResponse->bufferLen );
-    __CPROVER_assume( valueOffset < valueLen );
+    __CPROVER_assume( valueOffset <= pResponse->bufferLen );
+    __CPROVER_assume( valueLen <= pResponse->bufferLen - valueOffset );
     pValueLoc = pResponse->pBuffer + valueOffset;
 
-    __CPROVER_assume( 0 < fieldLen && fieldLen <= pResponse->bufferLen );
-    __CPROVER_assume( fieldOffset < fieldLen );
+    __CPROVER_assume( fieldOffset <= pResponse->bufferLen );
+    __CPROVER_assume( fieldLen > 0 );
+    __CPROVER_assume( fieldLen <= pResponse->bufferLen - fieldOffset );
     pFindHeaderContext->pField = pResponse->pBuffer + fieldOffset;
     pFindHeaderContext->fieldLen = fieldLen;
     pFindHeaderContext->pValueLen = &valueLen;

test/cbmc/proofs/httpParserOnBodyCallback/httpParserOnBodyCallback_harness.c

@@ -45,8 +45,8 @@ void httpParserOnBodyCallback_harness()
     __CPROVER_assume( length < pResponse->bufferLen );
     pLoc = pResponse->pBuffer + length;
 
-    __CPROVER_assume( pLoc + length <
-                      ( pResponse->pBuffer + pResponse->bufferLen ) );
+    __CPROVER_assume( pLoc <
+                      ( pResponse->pBuffer + pResponse->bufferLen - length ) );
 
     __CPROVER_file_local_core_http_client_c_httpParserOnBodyCallback( pHttpParser, pLoc, length );
 }

test/cbmc/proofs/httpParserOnHeaderFieldCallback/httpParserOnHeaderFieldCallback_harness.c

@@ -47,8 +47,8 @@ void httpParserOnHeaderFieldCallback_harness()
     pResponse = pParsingContext->pResponse;
     pResponse->pHeaderParsingCallback = &headerParserCallback;
 
-    __CPROVER_assume( length <= pResponse->bufferLen );
-    __CPROVER_assume( locOffset < length );
+    __CPROVER_assume( locOffset <= pResponse->bufferLen );
+    __CPROVER_assume( length <= pResponse->bufferLen - locOffset );
     pLoc = pResponse->pBuffer + locOffset;
 
     /* This assumption suppresses an overflow error when incrementing pResponse->headerCount. */

test/cbmc/proofs/httpParserOnHeaderValueCallback/httpParserOnHeaderValueCallback_harness.c

@@ -43,8 +43,8 @@ void httpParserOnHeaderValueCallback_harness()
     __CPROVER_assume( pParsingContext->pLastHeaderField != NULL );
 
     pResponse = pParsingContext->pResponse;
-    __CPROVER_assume( length <= pResponse->bufferLen );
-    __CPROVER_assume( locOffset < length );
+    __CPROVER_assume( locOffset <= pResponse->bufferLen );
+    __CPROVER_assume( length <= pResponse->bufferLen - locOffset );
     pLoc = pResponse->pBuffer + locOffset;
 
     __CPROVER_file_local_core_http_client_c_httpParserOnHeaderValueCallback( pHttpParser, pLoc, length );

test/cbmc/proofs/httpParserOnStatusCallback/httpParserOnStatusCallback_harness.c

@@ -42,8 +42,8 @@ void httpParserOnStatusCallback_harness()
     pParsingContext = ( HTTPParsingContext_t * ) pHttpParser->data;
 
     pResponse = pParsingContext->pResponse;
-    __CPROVER_assume( length <= pResponse->bufferLen );
-    __CPROVER_assume( locOffset < length );
+    __CPROVER_assume( locOffset <= pResponse->bufferLen );
+    __CPROVER_assume( length <= pResponse->bufferLen - locOffset );
     pLoc = pResponse->pBuffer + locOffset;
 
     __CPROVER_file_local_core_http_client_c_httpParserOnStatusCallback( pHttpParser, pLoc, length );

test/cbmc/sources/http_cbmc_state.c

@@ -116,10 +116,13 @@ HTTPResponse_t * allocateHttpResponse( HTTPResponse_t * pResponse )
 
         __CPROVER_assume( headerOffset <= pResponse->bufferLen );
 
-        /* It is possible to have no headers in the response so set to NULL or
-         * an offset in the response buffer. */
-        pResponse->pHeaders = nondet_bool() ? NULL :
-                              pResponse->pBuffer + headerOffset;
+        if( pResponse->pBuffer != NULL )
+        {
+            /* It is possible to have no headers in the response so set to NULL or
+             * an offset in the response buffer. */
+            pResponse->pHeaders = nondet_bool() ? NULL :
+                                  pResponse->pBuffer + headerOffset;
+        }
 
         if( pResponse->pHeaders != NULL )
         {
@@ -137,8 +140,11 @@ HTTPResponse_t * allocateHttpResponse( HTTPResponse_t * pResponse )
             __CPROVER_assume( bodyOffset <= pResponse->bufferLen );
         }
 
-        pResponse->pBody = nondet_bool() ? NULL :
-                           pResponse->pBuffer + bodyOffset;
+        if( pResponse->pBuffer != NULL )
+        {
+            pResponse->pBody = nondet_bool() ? NULL :
+                               pResponse->pBuffer + bodyOffset;
+        }
 
         /* The length of the body MUST be between the start of body and the end
          * of the buffer. */