From dc94df08e4819471b73858b863fddd50c0ca38c6 Mon Sep 17 00:00:00 2001 From: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com> Date: Wed, 24 Jan 2024 23:09:58 +0530 Subject: [PATCH] Add on_status_complete callback (#173) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit on_status callback is not called for a response with a status code but without a reason string such as following: ``` HTTP/1.1 400 Server: nginx Date: Fri, 05 Jan 2024 05:25:21 GMT Content-Type: application/json Content-Length: 30 Connection: keep-alive ・・・ ``` It was reported here - https://github.com/FreeRTOS/coreHTTP/issues/171 Signed-off-by: Gaurav Aggarwal --- source/core_http_client.c | 43 +++++++++++++++++++ source/include/core_http_client_private.h | 7 +++ .../cbmc/proofs/HTTPClient_AddHeader/Makefile | 2 +- .../Makefile | 1 + test/cbmc/proofs/HTTPClient_Send/Makefile | 1 + .../Makefile | 21 +++++++++ .../README.md | 10 +++++ .../cbmc-proof.txt | 1 + .../cbmc-viewer.json | 7 +++ ...tpParserOnStatusCompleteCallback_harness.c | 43 +++++++++++++++++++ 10 files changed, 135 insertions(+), 1 deletion(-) create mode 100644 test/cbmc/proofs/httpParserOnStatusCompleteCallback/Makefile create mode 100644 test/cbmc/proofs/httpParserOnStatusCompleteCallback/README.md create mode 100644 test/cbmc/proofs/httpParserOnStatusCompleteCallback/cbmc-proof.txt create mode 100644 test/cbmc/proofs/httpParserOnStatusCompleteCallback/cbmc-viewer.json create mode 100644 test/cbmc/proofs/httpParserOnStatusCompleteCallback/httpParserOnStatusCompleteCallback_harness.c diff --git a/source/core_http_client.c b/source/core_http_client.c index 995143ff..84c87b72 100644 --- a/source/core_http_client.c +++ b/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; diff --git a/source/include/core_http_client_private.h b/source/include/core_http_client_private.h index d53e5d61..680e1894 100644 --- a/source/include/core_http_client_private.h +++ b/source/include/core_http_client_private.h @@ -247,6 +247,13 @@ typedef struct findHeaderContext * | * v * +--------+------------+ + * |onStatusComplete | + * +--------+------------+ + * | + * | + * | + * v + * +--------+------------+ * |onHeaderField +<---+ * +--------+------------+ | * | | diff --git a/test/cbmc/proofs/HTTPClient_AddHeader/Makefile b/test/cbmc/proofs/HTTPClient_AddHeader/Makefile index a9bd0f8b..54419e2f 100644 --- a/test/cbmc/proofs/HTTPClient_AddHeader/Makefile +++ b/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 diff --git a/test/cbmc/proofs/HTTPClient_InitializeRequestHeaders/Makefile b/test/cbmc/proofs/HTTPClient_InitializeRequestHeaders/Makefile index 509eeb59..347a70fc 100644 --- a/test/cbmc/proofs/HTTPClient_InitializeRequestHeaders/Makefile +++ b/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 diff --git a/test/cbmc/proofs/HTTPClient_Send/Makefile b/test/cbmc/proofs/HTTPClient_Send/Makefile index 064330a3..08f41119 100644 --- a/test/cbmc/proofs/HTTPClient_Send/Makefile +++ b/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 diff --git a/test/cbmc/proofs/httpParserOnStatusCompleteCallback/Makefile b/test/cbmc/proofs/httpParserOnStatusCompleteCallback/Makefile new file mode 100644 index 00000000..8cd7faf3 --- /dev/null +++ b/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 diff --git a/test/cbmc/proofs/httpParserOnStatusCompleteCallback/README.md b/test/cbmc/proofs/httpParserOnStatusCompleteCallback/README.md new file mode 100644 index 00000000..dc311a6c --- /dev/null +++ b/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. diff --git a/test/cbmc/proofs/httpParserOnStatusCompleteCallback/cbmc-proof.txt b/test/cbmc/proofs/httpParserOnStatusCompleteCallback/cbmc-proof.txt new file mode 100644 index 00000000..6ed46f12 --- /dev/null +++ b/test/cbmc/proofs/httpParserOnStatusCompleteCallback/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/httpParserOnStatusCompleteCallback/cbmc-viewer.json b/test/cbmc/proofs/httpParserOnStatusCompleteCallback/cbmc-viewer.json new file mode 100644 index 00000000..8f7c48c0 --- /dev/null +++ b/test/cbmc/proofs/httpParserOnStatusCompleteCallback/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "httpParserOnStatusCompleteCallback", + "proof-root": "cbmc/proofs" +} diff --git a/test/cbmc/proofs/httpParserOnStatusCompleteCallback/httpParserOnStatusCompleteCallback_harness.c b/test/cbmc/proofs/httpParserOnStatusCompleteCallback/httpParserOnStatusCompleteCallback_harness.c new file mode 100644 index 00000000..d950af4c --- /dev/null +++ b/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 ); +}