Update CBMC proofs for llhttp (#127)

* Update CBMC proofs * Update execute mocks * Rename stub file * Return error fields from stubs
FreeRTOS · Feb 2, 2022 · 1c94cde · 1c94cde
1 parent 3902274
commit 1c94cde
Show file tree

Hide file tree

Showing 17 changed files with 75 additions and 80 deletions.
diff --git a/test/cbmc/include/http_cbmc_state.h b/test/cbmc/include/http_cbmc_state.h
@@ -33,7 +33,7 @@
 
 #include "core_http_client.h"
 #include "core_http_client_private.h"
-#include "http_parser.h"
+#include "llhttp.h"
 #include "transport_interface_stubs.h"
 
 struct NetworkContext
@@ -132,14 +132,14 @@ TransportInterface_t * allocateTransportInterface( TransportInterface_t * pTrans
 bool isValidTransportInterface( TransportInterface_t * pTransportInterface );
 
 /**
- * @brief Allocate an #http_parser object that is valid in the context of the
+ * @brief Allocate an #llhttp_t object that is valid in the context of the
  * HTTPClient_Send() function.
  *
- * @param[in] pHttpParser #http_parser object to allocate.
+ * @param[in] pHttpParser #llhttp_t object to allocate.
  *
- * @return NULL or pointer to allocated #http_parser object.
+ * @return NULL or pointer to allocated #llhttp_t object.
  */
-http_parser * allocateHttpSendParser( http_parser * pHttpParser );
+llhttp_t * allocateHttpSendParser( llhttp_t * pHttpParser );
 
 /**
  * @brief Allocate an #HTTPParsingContext_t object.
@@ -160,14 +160,14 @@ HTTPParsingContext_t * allocateHttpSendParsingContext( HTTPParsingContext_t * pH
 bool isValidHttpSendParsingContext( const HTTPParsingContext_t * pHttpParsingContext );
 
 /**
- * @brief Allocate an #http_parser object that is valid in the context of the
+ * @brief Allocate an #llhttp_t object that is valid in the context of the
  * HTTPClient_ReadHeader() function.
  *
- * @param[in] pHttpParser #http_parser object to allocate.
+ * @param[in] pHttpParser #llhttp_t object to allocate.
  *
- * @return NULL or pointer to allocated #http_parser object.
+ * @return NULL or pointer to allocated #llhttp_t object.
  */
-http_parser * allocateHttpReadHeaderParser( http_parser * pHttpParser );
+llhttp_t * allocateHttpReadHeaderParser( llhttp_t * pHttpParser );
 
 /**
  * @brief Allocate an #findHeaderContext_t object.

diff --git a/test/cbmc/proofs/HTTPClient_ReadHeader/Makefile b/test/cbmc/proofs/HTTPClient_ReadHeader/Makefile
@@ -32,15 +32,14 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_findHeaderValueP
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_findHeaderOnHeaderCompleteCallback
 
 # Remove any unused functions for http parser
-REMOVE_FUNCTION_BODY += http_parser_init
-REMOVE_FUNCTION_BODY += http_parser_set_max_header_size
-REMOVE_FUNCTION_BODY += http_parser_settings_init
+REMOVE_FUNCTION_BODY += llhttp_init
+REMOVE_FUNCTION_BODY += llhttp_settings_init
 
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/http_cbmc_state.c
-PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/HTTPClient_ReadHeader_http_parser_execute.c
+PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/HTTPClient_ReadHeader_llhttp_execute.c
 
 PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c
 

diff --git a/test/cbmc/proofs/HTTPClient_Send/Makefile b/test/cbmc/proofs/HTTPClient_Send/Makefile
@@ -42,9 +42,8 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnMess
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnMessageCompleteCallback
 
 # Remove any unused functions for http parser
-REMOVE_FUNCTION_BODY += http_parser_init
-REMOVE_FUNCTION_BODY += http_parser_set_max_header_size
-REMOVE_FUNCTION_BODY += http_parser_settings_init
+REMOVE_FUNCTION_BODY += llhttp_init
+REMOVE_FUNCTION_BODY += llhttp_settings_init
 
 # These functions are removed and replace with stubs that check that the
 # destination parameter is writeable and that the source parameter is readable.
@@ -67,7 +66,7 @@ UNWINDSET += strncmp.0:5
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/http_cbmc_state.c
-PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/HTTPClient_Send_http_parser_execute.c
+PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/transport_interface_stubs.c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/get_time_stub.c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c

diff --git a/test/cbmc/proofs/Makefile-project-defines b/test/cbmc/proofs/Makefile-project-defines
@@ -26,7 +26,7 @@ INCLUDES += -I$(SRCDIR)/test/cbmc/include
 INCLUDES += -I$(SRCDIR)/source/include
 INCLUDES += -I$(SRCDIR)/source/interface
 INCLUDES += -I$(SRCDIR)/source
-INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/http_parser
+INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/llhttp/include
 
 # Preprocessor definitions -D...
 DEFINES += -Dhttp_EXPORTS

diff --git a/test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c b/test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c
@@ -26,17 +26,17 @@
  */
 
 #include "http_cbmc_state.h"
-#include "http_parser.h"
+#include "llhttp.h"
 #include "core_http_client.h"
 
-int __CPROVER_file_local_core_http_client_c_findHeaderFieldParserCallback( http_parser * pHttpParser,
+int __CPROVER_file_local_core_http_client_c_findHeaderFieldParserCallback( llhttp_t * pHttpParser,
                                                                            const char * pFieldLoc,
                                                                            size_t fieldLen );
 
 
 void findHeaderFieldParserCallback_harness()
 {
-    http_parser * pHttpParser;
+    llhttp_t * pHttpParser;
     HTTPResponse_t * pResponse;
     findHeaderContext_t * pFindHeaderContext;
     size_t fieldLen, fieldContextLen, fieldOffset, valueLen, valueOffset;

diff --git a/...mc/proofs/findHeaderOnHeaderCompleteCallback/findHeaderOnHeaderCompleteCallback_harness.c b/...mc/proofs/findHeaderOnHeaderCompleteCallback/findHeaderOnHeaderCompleteCallback_harness.c
@@ -26,14 +26,14 @@
  */
 
 #include "http_cbmc_state.h"
-#include "http_parser.h"
+#include "llhttp.h"
 #include "core_http_client.h"
 
-int __CPROVER_file_local_core_http_client_c_findHeaderOnHeaderCompleteCallback( http_parser * pHttpParser );
+int __CPROVER_file_local_core_http_client_c_findHeaderOnHeaderCompleteCallback( llhttp_t * pHttpParser );
 
 void findHeaderOnHeaderCompleteCallback_harness()
 {
-    http_parser * pHttpParser;
+    llhttp_t * pHttpParser;
 
     pHttpParser = allocateHttpReadHeaderParser( NULL );
 

diff --git a/test/cbmc/proofs/findHeaderValueParserCallback/findHeaderValueParserCallback_harness.c b/test/cbmc/proofs/findHeaderValueParserCallback/findHeaderValueParserCallback_harness.c
@@ -26,16 +26,16 @@
  */
 
 #include "http_cbmc_state.h"
-#include "http_parser.h"
+#include "llhttp.h"
 #include "core_http_client.h"
 
-int __CPROVER_file_local_core_http_client_c_findHeaderValueParserCallback( http_parser * pHttpParser,
+int __CPROVER_file_local_core_http_client_c_findHeaderValueParserCallback( llhttp_t * pHttpParser,
                                                                            const char * pValueLoc,
                                                                            size_t valueLen );
 
 void findHeaderValueParserCallback_harness()
 {
-    http_parser * pHttpParser;
+    llhttp_t * pHttpParser;
     HTTPResponse_t * pResponse;
     findHeaderContext_t * pFindHeaderContext;
     size_t fieldLen, fieldOffset, valueLen, valueOffset;

diff --git a/test/cbmc/proofs/httpParserOnBodyCallback/httpParserOnBodyCallback_harness.c b/test/cbmc/proofs/httpParserOnBodyCallback/httpParserOnBodyCallback_harness.c
@@ -26,15 +26,15 @@
  */
 
 #include "http_cbmc_state.h"
-#include "http_parser.h"
+#include "llhttp.h"
 
-int __CPROVER_file_local_core_http_client_c_httpParserOnBodyCallback( http_parser * pHttpParser,
+int __CPROVER_file_local_core_http_client_c_httpParserOnBodyCallback( llhttp_t * pHttpParser,
                                                                       const char * pLoc,
                                                                       size_t length );
 
 void httpParserOnBodyCallback_harness()
 {
-    http_parser * pHttpParser;
+    llhttp_t * pHttpParser;
     HTTPParsingContext_t * pParsingContext;
     HTTPResponse_t * pResponse;
     size_t length;

diff --git a/test/cbmc/proofs/httpParserOnHeaderFieldCallback/httpParserOnHeaderFieldCallback_harness.c b/test/cbmc/proofs/httpParserOnHeaderFieldCallback/httpParserOnHeaderFieldCallback_harness.c
@@ -26,16 +26,16 @@
  */
 
 #include "http_cbmc_state.h"
-#include "http_parser.h"
+#include "llhttp.h"
 #include "callback_stubs.h"
 
-int __CPROVER_file_local_core_http_client_c_httpParserOnHeaderFieldCallback( http_parser * pHttpParser,
+int __CPROVER_file_local_core_http_client_c_httpParserOnHeaderFieldCallback( llhttp_t * pHttpParser,
                                                                              const char * pLoc,
                                                                              size_t length );
 
 void httpParserOnHeaderFieldCallback_harness()
 {
-    http_parser * pHttpParser;
+    llhttp_t * pHttpParser;
     HTTPParsingContext_t * pParsingContext;
     HTTPResponse_t * pResponse;
     HTTPClient_ResponseHeaderParsingCallback_t headerParserCallback;

diff --git a/test/cbmc/proofs/httpParserOnHeaderValueCallback/httpParserOnHeaderValueCallback_harness.c b/test/cbmc/proofs/httpParserOnHeaderValueCallback/httpParserOnHeaderValueCallback_harness.c
@@ -26,15 +26,15 @@
  */
 
 #include "http_cbmc_state.h"
-#include "http_parser.h"
+#include "llhttp.h"
 
-int __CPROVER_file_local_core_http_client_c_httpParserOnHeaderValueCallback( http_parser * pHttpParser,
+int __CPROVER_file_local_core_http_client_c_httpParserOnHeaderValueCallback( llhttp_t * pHttpParser,
                                                                              const char * pLoc,
                                                                              size_t length );
 
 void httpParserOnHeaderValueCallback_harness()
 {
-    http_parser * pHttpParser;
+    llhttp_t * pHttpParser;
     HTTPParsingContext_t * pParsingContext;
     HTTPResponse_t * pResponse;
     size_t length, locOffset;

diff --git a/.../proofs/httpParserOnHeadersCompleteCallback/httpParserOnHeadersCompleteCallback_harness.c b/.../proofs/httpParserOnHeadersCompleteCallback/httpParserOnHeadersCompleteCallback_harness.c
@@ -26,14 +26,14 @@
  */
 
 #include "http_cbmc_state.h"
-#include "http_parser.h"
+#include "llhttp.h"
 #include "callback_stubs.h"
 
-int __CPROVER_file_local_core_http_client_c_httpParserOnHeadersCompleteCallback( http_parser * pHttpParser );
+int __CPROVER_file_local_core_http_client_c_httpParserOnHeadersCompleteCallback( llhttp_t * pHttpParser );
 
 void httpParserOnHeadersCompleteCallback_harness()
 {
-    http_parser * pHttpParser;
+    llhttp_t * pHttpParser;
     HTTPParsingContext_t * pParsingContext;
     HTTPResponse_t * pResponse;
     HTTPClient_ResponseHeaderParsingCallback_t headerParserCallback;

diff --git a/test/cbmc/proofs/httpParserOnMessageBeginCallback/httpParserOnMessageBeginCallback_harness.c b/test/cbmc/proofs/httpParserOnMessageBeginCallback/httpParserOnMessageBeginCallback_harness.c
@@ -26,13 +26,13 @@
  */
 
 #include "http_cbmc_state.h"
-#include "http_parser.h"
+#include "llhttp.h"
 
-int __CPROVER_file_local_core_http_client_c_httpParserOnMessageBeginCallback( http_parser * pHttpParser );
+int __CPROVER_file_local_core_http_client_c_httpParserOnMessageBeginCallback( llhttp_t * pHttpParser );
 
 void httpParserOnMessageBeginCallback_harness()
 {
-    http_parser * pHttpParser;
+    llhttp_t * pHttpParser;
 
     pHttpParser = allocateHttpSendParser( NULL );
 

diff --git a/.../proofs/httpParserOnMessageCompleteCallback/httpParserOnMessageCompleteCallback_harness.c b/.../proofs/httpParserOnMessageCompleteCallback/httpParserOnMessageCompleteCallback_harness.c
@@ -26,13 +26,13 @@
  */
 
 #include "http_cbmc_state.h"
-#include "http_parser.h"
+#include "llhttp.h"
 
-int __CPROVER_file_local_core_http_client_c_httpParserOnMessageCompleteCallback( http_parser * pHttpParser );
+int __CPROVER_file_local_core_http_client_c_httpParserOnMessageCompleteCallback( llhttp_t * pHttpParser );
 
 void httpParserOnMessageCompleteCallback_harness()
 {
-    http_parser * pHttpParser;
+    llhttp_t * pHttpParser;
 
     pHttpParser = allocateHttpSendParser( NULL );
 

diff --git a/test/cbmc/proofs/httpParserOnStatusCallback/httpParserOnStatusCallback_harness.c b/test/cbmc/proofs/httpParserOnStatusCallback/httpParserOnStatusCallback_harness.c
@@ -26,16 +26,16 @@
  */
 
 #include "http_cbmc_state.h"
-#include "http_parser.h"
+#include "llhttp.h"
 #include "core_http_client.h"
 
-int __CPROVER_file_local_core_http_client_c_httpParserOnStatusCallback( http_parser * pHttpParser,
+int __CPROVER_file_local_core_http_client_c_httpParserOnStatusCallback( llhttp_t * pHttpParser,
                                                                         const char * pLoc,
                                                                         size_t length );
 
 void httpParserOnStatusCallback_harness()
 {
-    http_parser * pHttpParser;
+    llhttp_t * pHttpParser;
     HTTPParsingContext_t * pParsingContext;
     HTTPResponse_t * pResponse;
     size_t length, locOffset;

diff --git a/test/cbmc/sources/http_cbmc_state.c b/test/cbmc/sources/http_cbmc_state.c
@@ -200,13 +200,13 @@ bool isValidTransportInterface( TransportInterface_t * pTransportInterface )
     }
 }
 
-http_parser * allocateHttpSendParser( http_parser * pHttpParser )
+llhttp_t * allocateHttpSendParser( llhttp_t * pHttpParser )
 {
     HTTPParsingContext_t * pHttpParsingContext;
 
     if( pHttpParser == NULL )
     {
-        pHttpParser = malloc( sizeof( http_parser ) );
+        pHttpParser = malloc( sizeof( llhttp_t ) );
         __CPROVER_assume( pHttpParser != NULL );
     }
 
@@ -251,13 +251,13 @@ bool isValidHttpSendParsingContext( const HTTPParsingContext_t * pHttpParsingCon
     return isValid;
 }
 
-http_parser * allocateHttpReadHeaderParser( http_parser * pHttpParser )
+llhttp_t * allocateHttpReadHeaderParser( llhttp_t * pHttpParser )
 {
     HTTPParsingContext_t * pFindHeaderContext;
 
     if( pHttpParser == NULL )
     {
-        pHttpParser = malloc( sizeof( http_parser ) );
+        pHttpParser = malloc( sizeof( llhttp_t ) );
         __CPROVER_assume( pHttpParser != NULL );
     }
 

diff --git a/...TPClient_ReadHeader_http_parser_execute.c → ...bs/HTTPClient_ReadHeader_llhttp_execute.c b/...TPClient_ReadHeader_http_parser_execute.c → ...bs/HTTPClient_ReadHeader_llhttp_execute.c
@@ -21,8 +21,8 @@
  */
 
 /**
- * @file HTTPClient_ReadHeader_http_parser_execute.c
- * @brief A stub function for http_parser_execute for coverage of
+ * @file HTTPClient_ReadHeader_llhttp_execute.c
+ * @brief A stub function for llhttp_execute for coverage of
  * #HTTPClient_ReadHeader.
  */
 
@@ -31,33 +31,30 @@
 
 #include "core_http_client.h"
 #include "core_http_client_private.h"
-#include "http_parser.h"
+#include "llhttp.h"
 
 /**
  * @brief Attains coverage when a variable needs to possibly contain two values.
  */
 bool nondet_bool();
 
-size_t http_parser_execute( http_parser * parser,
-                            const http_parser_settings * settings,
-                            const char * data,
-                            size_t len )
+llhttp_errno_t llhttp_execute( llhttp_t * parser,
+                               const char * data,
+                               size_t len )
 {
     char * pValue;
     size_t fieldLength, fieldOffset, valueLength, valueOffset;
-    unsigned int http_errno;
+    int http_errno;
     findHeaderContext_t * pParsingContext;
 
     __CPROVER_assert( parser != NULL,
-                      "http_parser_execute parser is NULL" );
-    __CPROVER_assert( settings != NULL,
-                      "http_parser_execute settings is NULL" );
+                      "llhttp_execute parser is NULL" );
     __CPROVER_assert( data != NULL,
-                      "http_parser_execute data is NULL" );
+                      "llhttp_execute data is NULL" );
     __CPROVER_assert( len < CBMC_MAX_OBJECT_SIZE,
-                      "http_parser_execute len >= CBMC_MAX_OBJECT_SIZE" );
+                      "llhttp_execute len >= CBMC_MAX_OBJECT_SIZE" );
 
-    parser->http_errno = http_errno;
+    parser->error = http_errno;
 
     __CPROVER_assume( fieldLength <= len );
     __CPROVER_assume( fieldOffset < fieldLength );
@@ -87,5 +84,5 @@ size_t http_parser_execute( http_parser * parser,
         pParsingContext->pValueLoc = &pValue;
     }
 
-    return pParsingContext->fieldFound ? valueLength : 0;
+    return parser->error;
 }