Add on_status_complete callback

source/core_http_client.c

@@ -354,6 +354,16 @@ static int httpParserOnStatusCallback( llhttp_t * pHttpParser,
                                        const char * pLoc,
                                        size_t length );
 
+/**
+ * @brief Callback invoked during llhttp_execute() when the HTTP response
+ * status parsing is complete.
+ *
+ * @param[in] pHttpParser Parsing object containing state and callback context.
+ *
+ * @return #LLHTTP_CONTINUE_PARSING to continue parsing.
+ */
+static int httpParserOnStatusCompleteCallback( llhttp_t * pHttpParser );
+
 /**
  * @brief Callback invoked during llhttp_execute() when an HTTP response
  * header field is found.
@@ -682,6 +692,38 @@ static int httpParserOnStatusCallback( llhttp_t * pHttpParser,
 
 /*-----------------------------------------------------------*/
 
+static int httpParserOnStatusCompleteCallback( llhttp_t * pHttpParser )
+{
+    HTTPParsingContext_t * pParsingContext = NULL;
+    HTTPResponse_t * pResponse = NULL;
+
+    assert( pHttpParser != NULL );
+    assert( pHttpParser->data != NULL );
+
+    pParsingContext = ( HTTPParsingContext_t * ) ( pHttpParser->data );
+    pResponse = pParsingContext->pResponse;
+
+    assert( pResponse != NULL );
+
+    /* Initialize the first header field and value to be passed to the user
+     * callback. */
+    pParsingContext->pLastHeaderField = NULL;
+    pParsingContext->lastHeaderFieldLen = 0U;
+    pParsingContext->pLastHeaderValue = NULL;
+    pParsingContext->lastHeaderValueLen = 0U;
+
+    /* httpParserOnStatusCompleteCallback() is reached because llhttp_execute()
+     * has successfully read the HTTP response status code. */
+    pResponse->statusCode = ( uint16_t ) ( pHttpParser->status_code );
+
+    LogDebug( ( "Response parsing: StatusCode=%u",
+                ( unsigned int ) pResponse->statusCode ) );
+
+    return LLHTTP_CONTINUE_PARSING;
+}
+
+/*-----------------------------------------------------------*/
+
 static int httpParserOnHeaderFieldCallback( llhttp_t * pHttpParser,
                                             const char * pLoc,
                                             size_t length )
@@ -977,6 +1019,7 @@ static void initializeParsingContextForFirstResponse( HTTPParsingContext_t * pPa
     llhttp_settings_init( &( pParsingContext->llhttpSettings ) );
     pParsingContext->llhttpSettings.on_message_begin = httpParserOnMessageBeginCallback;
     pParsingContext->llhttpSettings.on_status = httpParserOnStatusCallback;
+    pParsingContext->llhttpSettings.on_status_complete = httpParserOnStatusCompleteCallback;
     pParsingContext->llhttpSettings.on_header_field = httpParserOnHeaderFieldCallback;
     pParsingContext->llhttpSettings.on_header_value = httpParserOnHeaderValueCallback;
     pParsingContext->llhttpSettings.on_headers_complete = httpParserOnHeadersCompleteCallback;

source/include/core_http_client_private.h

@@ -247,6 +247,13 @@ typedef struct findHeaderContext
  *          |
  *          v
  * +--------+------------+
+ * |onStatusComplete     |
+ * +--------+------------+
+ *          |
+ *          |
+ *          |
+ *          v
+ * +--------+------------+
  * |onHeaderField        +<---+
  * +--------+------------+    |
  *          |                 |

test/cbmc/proofs/HTTPClient_AddHeader/Makefile

@@ -34,7 +34,7 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnBody
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnHeaderFieldCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnHeaderValueCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnStatusCallback
-
+REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnStatusCompleteCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnHeadersCompleteCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnMessageBeginCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnMessageCompleteCallback

test/cbmc/proofs/HTTPClient_InitializeRequestHeaders/Makefile

@@ -34,6 +34,7 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnBody
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnHeaderFieldCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnHeaderValueCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnStatusCallback
+REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnStatusCompleteCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnHeadersCompleteCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnMessageBeginCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnMessageCompleteCallback

test/cbmc/proofs/HTTPClient_Send/Makefile

@@ -37,6 +37,7 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnBody
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnHeaderFieldCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnHeaderValueCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnStatusCallback
+REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnStatusCompleteCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnHeadersCompleteCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnMessageBeginCallback
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnMessageCompleteCallback

test/cbmc/proofs/httpParserOnStatusCompleteCallback/Makefile

@@ -0,0 +1,21 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: MIT-0
+
+HARNESS_ENTRY=httpParserOnStatusCompleteCallback_harness
+PROOF_UID=httpParserOnStatusCompleteCallback
+HARNESS_FILE=$(HARNESS_ENTRY)
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/http_cbmc_state.c
+
+PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c
+
+EXTERNAL_SAT_SOLVER := kissat
+
+include ../Makefile.common

test/cbmc/proofs/httpParserOnStatusCompleteCallback/README.md

@@ -0,0 +1,10 @@
+httpParserOnStatusCompleteCallback proof
+==============
+
+This directory contains a memory safety proof for httpParserOnStatusCompleteCallback.
+
+To run the proof.
+* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer
+  to your path.
+* Run "make".
+* Open html/index.html in a web browser.

test/cbmc/proofs/httpParserOnStatusCompleteCallback/cbmc-proof.txt

@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.

test/cbmc/proofs/httpParserOnStatusCompleteCallback/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "httpParserOnStatusCompleteCallback",
+  "proof-root": "cbmc/proofs"
+}

test/cbmc/proofs/httpParserOnStatusCompleteCallback/httpParserOnStatusCompleteCallback_harness.c

@@ -0,0 +1,43 @@
+/*
+ * coreHTTP v3.0.0
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * SPDX-License-Identifier: MIT
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/**
+ * @file httpParserOnStatusCompleteCallback_harness.c
+ * @brief Implements the proof harness for httpParserOnStatusCompleteCallback function.
+ */
+
+#include "http_cbmc_state.h"
+#include "llhttp.h"
+#include "core_http_client.h"
+
+int __CPROVER_file_local_core_http_client_c_httpParserOnStatusCompleteCallback( llhttp_t * pHttpParser );
+
+void httpParserOnStatusCompleteCallback_harness()
+{
+    llhttp_t * pHttpParser;
+
+    pHttpParser = allocateHttpSendParser( NULL );
+
+    __CPROVER_file_local_core_http_client_c_httpParserOnStatusCompleteCallback( pHttpParser );
+}