From 00677cb9dc08e720fb9e04284a541d5d653ce98f Mon Sep 17 00:00:00 2001 From: cryi Date: Wed, 17 Jan 2024 22:43:33 +0100 Subject: [PATCH 1/9] ability to pause parsing after headers --- source/core_http_client.c | 22 ++++++++++- source/include/core_http_client.h | 45 +++++++++++++++++++++-- source/include/core_http_client_private.h | 5 +++ 3 files changed, 67 insertions(+), 5 deletions(-) diff --git a/source/core_http_client.c b/source/core_http_client.c index 995143ff..eafef123 100644 --- a/source/core_http_client.c +++ b/source/core_http_client.c @@ -870,6 +870,13 @@ static int httpParserOnHeadersCompleteCallback( llhttp_t * pHttpParser ) LogDebug( ( "Response parsing: Found the end of the headers." ) ); + /* If there is HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG opt-in we should stop + * parsing here. */ + if ( pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) { + shouldContinueParse = LLHTTP_PAUSE_PARSING; + pResponse->pBody = (const uint8_t*)pParsingContext->pBufferCur; + } + return shouldContinueParse; } @@ -1101,7 +1108,10 @@ static HTTPStatus_t processLlhttpError( const llhttp_t * pHttpParser ) "found when it shouldn't have been." ) ); returnStatus = HTTPSecurityAlertInvalidContentLength; break; - + case HPE_PAUSED: + LogInfo(("User intervention: Parsing stopped by user.")); + returnStatus = HTTPParserPaused; + break; /* All other error cases cannot be triggered and indicate an error in the * third-party parsing library if found. */ default: @@ -2086,6 +2096,12 @@ HTTPStatus_t HTTPClient_ReceiveAndParseHttpResponse( const TransportInterface_t ( totalReceived < pResponse->bufferLen ) ) ? 1U : 0U; } + if ( returnStatus == HTTPParserPaused && pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG) { + returnStatus = HTTPSuccess; + /* There may be dangling data if we parse with do not parse body flag. To let libraries built on top of corehttp we expose it through body. */ + pResponse->bodyLen = totalReceived - ((uint8_t *)pResponse->pBody - pResponse->pBuffer); + } + if( returnStatus == HTTPSuccess ) { /* If there are errors in receiving from the network or during parsing, @@ -2607,6 +2623,10 @@ const char * HTTPClient_strerror( HTTPStatus_t status ) str = "HTTPSecurityAlertInvalidContentLength"; break; + case HTTPParserPaused: + str = "HTTPParserPaused"; + break; + case HTTPParserInternalError: str = "HTTPParserInternalError"; break; diff --git a/source/include/core_http_client.h b/source/include/core_http_client.h index 8dc2a098..51065fc3 100644 --- a/source/include/core_http_client.h +++ b/source/include/core_http_client.h @@ -153,6 +153,26 @@ */ #define HTTP_RESPONSE_CONNECTION_KEEP_ALIVE_FLAG 0x2U +/** + * @defgroup http_response_option_flags HTTPResponse_t Flags + * @brief Flags for #HTTPResponse_t.respOptionFlags. + * These flags control configurations of response parsing. + * + * Flags should be bitwise-ORed with each other to change the behavior of + * #HTTPClient_ReceiveAndParseHttpResponse and #HTTPClient_Send. + */ + +/** + * @ingroup http_response_option_flags + * @brief Set this flag to indicate that the response body should not be parsed. + * + * Setting this will cause parser to stop after parsing the headers. Portion of raw body + * may be available in #HTTPResponse_t.pBody and #HTTPResponse_t.bodyLen. + * + * This flag is valid only for #HTTPResponse_t respOptionFlags parameter. + */ +#define HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG 0x1U + /** * @ingroup http_constants * @brief Flag that represents End of File byte in the range specification of @@ -292,12 +312,22 @@ typedef enum HTTPStatus HTTPSecurityAlertInvalidContentLength, /** - * @brief An error occurred in the third-party parsing library. + * @brief Represents the state of the HTTP parser when it is paused. * - * Functions that may return this value: - * - #HTTPClient_Send - * - #HTTPClient_ReadHeader + * This state indicates that the parser has encountered a pause condition and is waiting for further input. + * + * @see HTTPClient_Send + * @see HTTPClient_ReceiveAndParseHttpResponse */ + HTTPParserPaused, + + /** + * @brief An error occurred in the third-party parsing library. + * + * Functions that may return this value: + * - #HTTPClient_Send + * - #HTTPClient_ReadHeader + */ HTTPParserInternalError, /** @@ -535,6 +565,13 @@ typedef struct HTTPResponse */ uint8_t areHeadersComplete; + /** + * @brief Flags to activate other response configurations. + * + * Please see @ref http_response_option_flags for more information. + */ + uint32_t respOptionFlags; + /** * @brief Flags of useful headers found in the response. * diff --git a/source/include/core_http_client_private.h b/source/include/core_http_client_private.h index d53e5d61..7383d0e3 100644 --- a/source/include/core_http_client_private.h +++ b/source/include/core_http_client_private.h @@ -166,6 +166,11 @@ */ #define LLHTTP_STOP_PARSING HPE_USER +/** + * @brief Return value for llhttp registered callback to signal pause + */ +#define LLHTTP_PAUSE_PARSING HPE_PAUSED + /** * @brief Return value for llhttp_t.on_headers_complete to signal * that the HTTP response has no body and to halt further execution. From 432454701ee4e5ce518d835a0b51314550c51564 Mon Sep 17 00:00:00 2001 From: V <36897290+cryi@users.noreply.github.com> Date: Wed, 17 Jan 2024 23:03:30 +0100 Subject: [PATCH 2/9] Format (#3) * format --------- Co-authored-by: GitHub Action --- source/core_http_client.c | 14 +++++++++----- source/include/core_http_client.h | 16 ++++++++-------- 2 files changed, 17 insertions(+), 13 deletions(-) diff --git a/source/core_http_client.c b/source/core_http_client.c index eafef123..128a1d51 100644 --- a/source/core_http_client.c +++ b/source/core_http_client.c @@ -872,9 +872,10 @@ static int httpParserOnHeadersCompleteCallback( llhttp_t * pHttpParser ) /* If there is HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG opt-in we should stop * parsing here. */ - if ( pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) { + if( pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) + { shouldContinueParse = LLHTTP_PAUSE_PARSING; - pResponse->pBody = (const uint8_t*)pParsingContext->pBufferCur; + pResponse->pBody = ( const uint8_t * ) pParsingContext->pBufferCur; } return shouldContinueParse; @@ -1108,10 +1109,12 @@ static HTTPStatus_t processLlhttpError( const llhttp_t * pHttpParser ) "found when it shouldn't have been." ) ); returnStatus = HTTPSecurityAlertInvalidContentLength; break; + case HPE_PAUSED: - LogInfo(("User intervention: Parsing stopped by user.")); + LogInfo( ( "User intervention: Parsing stopped by user." ) ); returnStatus = HTTPParserPaused; break; + /* All other error cases cannot be triggered and indicate an error in the * third-party parsing library if found. */ default: @@ -2096,10 +2099,11 @@ HTTPStatus_t HTTPClient_ReceiveAndParseHttpResponse( const TransportInterface_t ( totalReceived < pResponse->bufferLen ) ) ? 1U : 0U; } - if ( returnStatus == HTTPParserPaused && pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG) { + if( ( returnStatus == HTTPParserPaused ) && pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) + { returnStatus = HTTPSuccess; /* There may be dangling data if we parse with do not parse body flag. To let libraries built on top of corehttp we expose it through body. */ - pResponse->bodyLen = totalReceived - ((uint8_t *)pResponse->pBody - pResponse->pBuffer); + pResponse->bodyLen = totalReceived - ( ( uint8_t * ) pResponse->pBody - pResponse->pBuffer ); } if( returnStatus == HTTPSuccess ) diff --git a/source/include/core_http_client.h b/source/include/core_http_client.h index 51065fc3..ebe92ca4 100644 --- a/source/include/core_http_client.h +++ b/source/include/core_http_client.h @@ -171,7 +171,7 @@ * * This flag is valid only for #HTTPResponse_t respOptionFlags parameter. */ -#define HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG 0x1U +#define HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG 0x1U /** * @ingroup http_constants @@ -185,7 +185,7 @@ * - When the requested range is for the last N bytes of the file. * In both cases, this value should be used for the "rangeEnd" parameter. */ -#define HTTP_RANGE_REQUEST_END_OF_FILE -1 +#define HTTP_RANGE_REQUEST_END_OF_FILE -1 /** * @ingroup http_enum_types @@ -322,12 +322,12 @@ typedef enum HTTPStatus HTTPParserPaused, /** - * @brief An error occurred in the third-party parsing library. - * - * Functions that may return this value: - * - #HTTPClient_Send - * - #HTTPClient_ReadHeader - */ + * @brief An error occurred in the third-party parsing library. + * + * Functions that may return this value: + * - #HTTPClient_Send + * - #HTTPClient_ReadHeader + */ HTTPParserInternalError, /** From c6b830855921fb98cde2193743d52485edf4dba3 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Fri, 19 Jan 2024 01:00:10 +0000 Subject: [PATCH 3/9] Fix CBMC proof of Send function --- source/core_http_client.c | 4 ++-- .../cbmc/stubs/HTTPClient_Send_llhttp_execute.c | 17 +++++++++++++++++ 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/source/core_http_client.c b/source/core_http_client.c index 128a1d51..927028c3 100644 --- a/source/core_http_client.c +++ b/source/core_http_client.c @@ -2099,11 +2099,11 @@ HTTPStatus_t HTTPClient_ReceiveAndParseHttpResponse( const TransportInterface_t ( totalReceived < pResponse->bufferLen ) ) ? 1U : 0U; } - if( ( returnStatus == HTTPParserPaused ) && pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) + if( ( returnStatus == HTTPParserPaused ) && ( pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) ) { returnStatus = HTTPSuccess; /* There may be dangling data if we parse with do not parse body flag. To let libraries built on top of corehttp we expose it through body. */ - pResponse->bodyLen = totalReceived - ( ( uint8_t * ) pResponse->pBody - pResponse->pBuffer ); + pResponse->bodyLen = totalReceived - ( size_t )( ( ( uintptr_t ) pResponse->pBody ) - ( ( uintptr_t ) pResponse->pBuffer ) ); } if( returnStatus == HTTPSuccess ) diff --git a/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c b/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c index 8ceb72dd..8f630ba3 100644 --- a/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c +++ b/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c @@ -80,5 +80,22 @@ llhttp_errno_t llhttp_execute( llhttp_t * parser, pParsingContext->lastHeaderValueLen = 0U; } + /* The body pointer is set by the httpParserOnBodyCallback. But since we are + * removing that from CBMC proof execution, the body has to be set here. */ + size_t bodyOffset; + + if( pParsingContext->pResponse->bufferLen == 0 ) + { + bodyOffset = 0; + } + else + { + /* Body offset can be anything as long as it doesn't exceed the buffer length + * and the length of the current data packet. */ + __CPROVER_assume( bodyOffset < pParsingContext->pResponse->bufferLen ); + __CPROVER_assume( bodyOffset < len ); + } + pParsingContext->pResponse->pBody = pParsingContext->pBufferCur + bodyOffset; + return parser->error; } From 183e2a41c8310fe130c87a92a74a73d34803a054 Mon Sep 17 00:00:00 2001 From: GitHub Action Date: Fri, 19 Jan 2024 18:53:09 +0000 Subject: [PATCH 4/9] Uncrustify: triggered by comment. Push. --- source/core_http_client.c | 2 +- test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/source/core_http_client.c b/source/core_http_client.c index 927028c3..f301fa53 100644 --- a/source/core_http_client.c +++ b/source/core_http_client.c @@ -2103,7 +2103,7 @@ HTTPStatus_t HTTPClient_ReceiveAndParseHttpResponse( const TransportInterface_t { returnStatus = HTTPSuccess; /* There may be dangling data if we parse with do not parse body flag. To let libraries built on top of corehttp we expose it through body. */ - pResponse->bodyLen = totalReceived - ( size_t )( ( ( uintptr_t ) pResponse->pBody ) - ( ( uintptr_t ) pResponse->pBuffer ) ); + pResponse->bodyLen = totalReceived - ( size_t ) ( ( ( uintptr_t ) pResponse->pBody ) - ( ( uintptr_t ) pResponse->pBuffer ) ); } if( returnStatus == HTTPSuccess ) diff --git a/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c b/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c index 8f630ba3..f4035b3d 100644 --- a/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c +++ b/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c @@ -95,6 +95,7 @@ llhttp_errno_t llhttp_execute( llhttp_t * parser, __CPROVER_assume( bodyOffset < pParsingContext->pResponse->bufferLen ); __CPROVER_assume( bodyOffset < len ); } + pParsingContext->pResponse->pBody = pParsingContext->pBufferCur + bodyOffset; return parser->error; From 057931ef282487b2532d29c6d2c7e790b35553a7 Mon Sep 17 00:00:00 2001 From: V <36897290+cryi@users.noreply.github.com> Date: Wed, 24 Jan 2024 12:04:16 +0100 Subject: [PATCH 5/9] Update test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c Co-authored-by: Soren Ptak --- test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c b/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c index f4035b3d..f305e5cd 100644 --- a/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c +++ b/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c @@ -84,9 +84,9 @@ llhttp_errno_t llhttp_execute( llhttp_t * parser, * removing that from CBMC proof execution, the body has to be set here. */ size_t bodyOffset; - if( pParsingContext->pResponse->bufferLen == 0 ) + if( pParsingContext->pResponse->bufferLen == 0U ) { - bodyOffset = 0; + bodyOffset = 0U; } else { From 8a52e77b84d2964bcb6b408775ce6b49991d33e4 Mon Sep 17 00:00:00 2001 From: Gaurav Aggarwal Date: Sun, 28 Jan 2024 21:41:41 +0530 Subject: [PATCH 6/9] Code review suggestions Signed-off-by: Gaurav Aggarwal --- source/core_http_client.c | 24 ++++++++++++++++------- source/include/core_http_client.h | 16 ++++++++------- source/include/core_http_client_private.h | 3 ++- test/unit-test/core_http_utest.c | 4 ++++ 4 files changed, 32 insertions(+), 15 deletions(-) diff --git a/source/core_http_client.c b/source/core_http_client.c index 0b338eb6..ada77d2c 100644 --- a/source/core_http_client.c +++ b/source/core_http_client.c @@ -914,10 +914,9 @@ static int httpParserOnHeadersCompleteCallback( llhttp_t * pHttpParser ) /* If there is HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG opt-in we should stop * parsing here. */ - if( pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) + if( ( pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) != 0U ) { shouldContinueParse = LLHTTP_PAUSE_PARSING; - pResponse->pBody = ( const uint8_t * ) pParsingContext->pBufferCur; } return shouldContinueParse; @@ -1236,9 +1235,17 @@ static HTTPStatus_t parseHttpResponse( HTTPParsingContext_t * pParsingContext, llhttp_resume_after_upgrade( &( pParsingContext->llhttpParser ) ); } - /* The next location to parse will always be after what has already - * been parsed. */ - pParsingContext->pBufferCur = parsingStartLoc + parseLen; + if( eReturn == HPE_PAUSED ) + { + /* The next location to parse is where the parser was paused. */ + pParsingContext->pBufferCur = pParsingContext->llhttpParser.error_pos; + } + else + { + /* The next location to parse is after what has already been parsed. */ + pParsingContext->pBufferCur = parsingStartLoc + parseLen; + } + returnStatus = processLlhttpError( &( pParsingContext->llhttpParser ) ); return returnStatus; @@ -2142,10 +2149,13 @@ HTTPStatus_t HTTPClient_ReceiveAndParseHttpResponse( const TransportInterface_t ( totalReceived < pResponse->bufferLen ) ) ? 1U : 0U; } - if( ( returnStatus == HTTPParserPaused ) && ( pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) ) + if( ( returnStatus == HTTPParserPaused ) && + ( ( pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) != 0U ) ) { returnStatus = HTTPSuccess; - /* There may be dangling data if we parse with do not parse body flag. To let libraries built on top of corehttp we expose it through body. */ + /* There may be dangling data if we parse with do not parse body flag. + * We expose this data through body to let the applications access it. */ + pResponse->pBody = ( const uint8_t * ) parsingContext.pBufferCur; pResponse->bodyLen = totalReceived - ( size_t ) ( ( ( uintptr_t ) pResponse->pBody ) - ( ( uintptr_t ) pResponse->pBuffer ) ); } diff --git a/source/include/core_http_client.h b/source/include/core_http_client.h index ebe92ca4..5239c3a1 100644 --- a/source/include/core_http_client.h +++ b/source/include/core_http_client.h @@ -156,7 +156,7 @@ /** * @defgroup http_response_option_flags HTTPResponse_t Flags * @brief Flags for #HTTPResponse_t.respOptionFlags. - * These flags control configurations of response parsing. + * These flags control the behavior of response parsing. * * Flags should be bitwise-ORed with each other to change the behavior of * #HTTPClient_ReceiveAndParseHttpResponse and #HTTPClient_Send. @@ -166,10 +166,11 @@ * @ingroup http_response_option_flags * @brief Set this flag to indicate that the response body should not be parsed. * - * Setting this will cause parser to stop after parsing the headers. Portion of raw body - * may be available in #HTTPResponse_t.pBody and #HTTPResponse_t.bodyLen. + * Setting this will cause parser to stop after parsing the headers. Portion of + * the raw body may be available in #HTTPResponse_t.pBody and + * #HTTPResponse_t.bodyLen. * - * This flag is valid only for #HTTPResponse_t respOptionFlags parameter. + * This flag is valid only for #HTTPResponse_t.respOptionFlags. */ #define HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG 0x1U @@ -312,9 +313,10 @@ typedef enum HTTPStatus HTTPSecurityAlertInvalidContentLength, /** - * @brief Represents the state of the HTTP parser when it is paused. + * @brief Represents the paused state of the HTTP parser. * - * This state indicates that the parser has encountered a pause condition and is waiting for further input. + * This state indicates that the parser has encountered a pause condition + * and is waiting for further input. * * @see HTTPClient_Send * @see HTTPClient_ReceiveAndParseHttpResponse @@ -566,7 +568,7 @@ typedef struct HTTPResponse uint8_t areHeadersComplete; /** - * @brief Flags to activate other response configurations. + * @brief Flags to control the behavior of response parsing. * * Please see @ref http_response_option_flags for more information. */ diff --git a/source/include/core_http_client_private.h b/source/include/core_http_client_private.h index 72b21d6e..3ded00cc 100644 --- a/source/include/core_http_client_private.h +++ b/source/include/core_http_client_private.h @@ -167,7 +167,8 @@ #define LLHTTP_STOP_PARSING HPE_USER /** - * @brief Return value for llhttp registered callback to signal pause + * @brief Return value for llhttp registered callback to signal to pause + * further execution. */ #define LLHTTP_PAUSE_PARSING HPE_PAUSED diff --git a/test/unit-test/core_http_utest.c b/test/unit-test/core_http_utest.c index 04809c2f..ec22b1c2 100644 --- a/test/unit-test/core_http_utest.c +++ b/test/unit-test/core_http_utest.c @@ -1662,6 +1662,10 @@ void test_HTTPClient_strerror( void ) str = HTTPClient_strerror( status ); TEST_ASSERT_EQUAL_STRING( "HTTPSecurityAlertInvalidContentLength", str ); + status = HTTPParserPaused; + str = HTTPClient_strerror( status ); + TEST_ASSERT_EQUAL_STRING( "HTTPParserPaused", str ); + status = HTTPParserInternalError; str = HTTPClient_strerror( status ); TEST_ASSERT_EQUAL_STRING( "HTTPParserInternalError", str ); From dc0bd7fdb7740b82f27314c76ed99e48fb75896f Mon Sep 17 00:00:00 2001 From: Gaurav Aggarwal Date: Sun, 28 Jan 2024 22:31:06 +0530 Subject: [PATCH 7/9] Fix formatting Signed-off-by: Gaurav Aggarwal --- source/core_http_client.c | 1 + 1 file changed, 1 insertion(+) diff --git a/source/core_http_client.c b/source/core_http_client.c index ada77d2c..c4a4533a 100644 --- a/source/core_http_client.c +++ b/source/core_http_client.c @@ -2153,6 +2153,7 @@ HTTPStatus_t HTTPClient_ReceiveAndParseHttpResponse( const TransportInterface_t ( ( pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) != 0U ) ) { returnStatus = HTTPSuccess; + /* There may be dangling data if we parse with do not parse body flag. * We expose this data through body to let the applications access it. */ pResponse->pBody = ( const uint8_t * ) parsingContext.pBufferCur; From 6636d692c47d6f92a9bb13694594ec0e10585c73 Mon Sep 17 00:00:00 2001 From: Gaurav Aggarwal Date: Sun, 28 Jan 2024 22:32:59 +0530 Subject: [PATCH 8/9] Fix memory estimates Signed-off-by: Gaurav Aggarwal --- docs/doxygen/include/size_table.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/doxygen/include/size_table.md b/docs/doxygen/include/size_table.md index 2170e484..4f22c250 100644 --- a/docs/doxygen/include/size_table.md +++ b/docs/doxygen/include/size_table.md @@ -9,7 +9,7 @@ core_http_client.c -
3.2K
+
3.3K
2.6K
@@ -29,7 +29,7 @@ Total estimates -
24.0K
 +
24.1K
20.8K
 From 513532243d4df34cf03846953ea3519a6fae61f6 Mon Sep 17 00:00:00 2001 From: Gaurav Aggarwal Date: Mon, 29 Jan 2024 08:06:08 +0000 Subject: [PATCH 9/9] Fix CBMC proof Signed-off-by: Gaurav Aggarwal --- test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c b/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c index f305e5cd..74b29bb7 100644 --- a/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c +++ b/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c @@ -98,5 +98,17 @@ llhttp_errno_t llhttp_execute( llhttp_t * parser, pParsingContext->pResponse->pBody = pParsingContext->pBufferCur + bodyOffset; + if( parser->error == HPE_PAUSED ) + { + /* When the parser is paused ensure that the error_pos member points to + * a valid location in the response buffer. */ + size_t errorPosOffset; + + __CPROVER_assume( errorPosOffset < pParsingContext->pResponse->bufferLen ); + __CPROVER_assume( errorPosOffset < len ); + + parser->error_pos = pParsingContext->pResponse->pBuffer + errorPosOffset; + } + return parser->error; }