[CoreHttp] Add strncasecmp implementation (#106)

* cbmc changes

* Function changes

* memory statistics changes

* make file changes

* Addressing Review comments

* Addressing PRBR comments

Author: gshvang

docs/doxygen/include/size_table.html

@@ -9,8 +9,8 @@
     </tr>
     <tr>
         <td>core_http_client.c</td>
-        <td><center>3.1K</center></td>
-        <td><center>2.5K</center></td>
+        <td><center>3.2K</center></td>
+        <td><center>2.6K</center></td>
     </tr>
     <tr>
         <td>http_parser.c (http-parser)</td>
@@ -19,7 +19,7 @@
     </tr>
     <tr>
         <td><b>Total estimates</b></td>
-        <td><b><center>18.8K</center></b></td>
-        <td><b><center>15.5K</center></b></td>
+        <td><b><center>18.9K</center></b></td>
+        <td><b><center>15.6K</center></b></td>
     </tr>
 </table>

lexicon.txt

@@ -233,6 +233,7 @@ sendflags
 sendhttpbody
 sendhttpheaders
 sendpartialcall
+sensitivity
 sizeof
 snprintf
 statuscode

source/core_http_client.c

@@ -27,6 +27,7 @@
 
 #include <assert.h>
 #include <string.h>
+#include <ctype.h>
 
 #include "core_http_client.h"
 #include "core_http_client_private.h"
@@ -544,6 +545,22 @@ static void processCompleteHeader( HTTPParsingContext_t * pParsingContext );
  */
 static HTTPStatus_t processHttpParserError( const http_parser * pHttpParser );
 
+/**
+ * @brief Compares at most the first n bytes of str1 and str2 without case sensitivity
+ * and n must be less than the actual size of either string.
+ *
+ * @param[in] str1 First string to be compared.
+ * @param[in] str2 Second string to be compared.
+ * @param[in] n The maximum number of characters to be compared.
+ *
+ * @return One of the following:
+ * 0 if str1 is equal to str2
+ * 1 if str1 is not equal to str2.
+ */
+static int8_t caseInsensitiveStringCmp( const char * str1,
+                                        const char * str2,
+                                        size_t n );
+
 /*-----------------------------------------------------------*/
 
 static uint32_t getZeroTimestampMs( void )
@@ -553,6 +570,25 @@ static uint32_t getZeroTimestampMs( void )
 
 /*-----------------------------------------------------------*/
 
+static int8_t caseInsensitiveStringCmp( const char * str1,
+                                        const char * str2,
+                                        size_t n )
+{
+    size_t i = 0U;
+
+    for( i = 0U; i < n; i++ )
+    {
+        if( toupper( str1[ i ] ) != toupper( str2[ i ] ) )
+        {
+            break;
+        }
+    }
+
+    return ( i == n ) ? 0 : 1;
+}
+
+/*-----------------------------------------------------------*/
+
 static void processCompleteHeader( HTTPParsingContext_t * pParsingContext )
 {
     HTTPResponse_t * pResponse = NULL;
@@ -2237,7 +2273,7 @@ static int findHeaderFieldParserCallback( http_parser * pHttpParser,
     /* Check whether the parsed header matches the header we are looking for. */
     /* Each header field consists of a case-insensitive field name (RFC 7230, section 3.2). */
     if( ( fieldLen == pContext->fieldLen ) &&
-        ( strncasecmp( pContext->pField, pFieldLoc, fieldLen ) == 0 ) )
+        ( caseInsensitiveStringCmp( pContext->pField, pFieldLoc, fieldLen ) == 0 ) )
     {
         LogDebug( ( "Found header field in response: "
                     "HeaderName=%.*s, HeaderLocation=0x%p",

test/cbmc/proofs/findHeaderFieldParserCallback/Makefile

@@ -7,13 +7,13 @@ HARNESS_FILE=$(HARNESS_ENTRY)
 
 # The header field length is bounded, so strncasecmp can be unwound to an expected
 # amount that won't make the proof run too long.
-MAX_HEADER_FIELD_LENGTH=10
+MAX_HEADER_FIELD_LENGTH=11
 
 DEFINES += -DMAX_HEADER_FIELD_LENGTH=$(MAX_HEADER_FIELD_LENGTH)
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
-UNWINDSET += strncasecmp.0:$(MAX_HEADER_FIELD_LENGTH)
+UNWINDSET += __CPROVER_file_local_core_http_client_c_caseInsensitiveStringCmp.0:$(MAX_HEADER_FIELD_LENGTH)
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/http_cbmc_state.c

test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c

@@ -46,7 +46,7 @@ void findHeaderFieldParserCallback_harness()
                       pResponse->pBuffer != NULL &&
                       pResponse->bufferLen > 0 );
 
-    __CPROVER_assume( 0 < fieldLen && fieldLen <= MAX_HEADER_FIELD_LENGTH && fieldLen <= pResponse->bufferLen );
+    __CPROVER_assume( 0 < fieldLen && fieldLen < MAX_HEADER_FIELD_LENGTH && fieldLen <= pResponse->bufferLen );
     __CPROVER_assume( fieldOffset <= pResponse->bufferLen - fieldLen );
     pFieldLoc = pResponse->pBuffer + fieldOffset;