Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update CBMC proofs for llhttp #127

Merged
merged 5 commits into from
Feb 2, 2022
Merged

Update CBMC proofs for llhttp #127

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
4c199bf
Update CBMC proofs
muneebahmed10 Jan 22, 2022
0555e6d
Update execute mocks
muneebahmed10 Jan 22, 2022
e30a765
Rename stub file
muneebahmed10 Feb 2, 2022
5ee726d
Return error fields from stubs
muneebahmed10 Feb 2, 2022
9aa74f6
Undo comment
muneebahmed10 Feb 2, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 9 additions & 9 deletions test/cbmc/include/http_cbmc_state.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand Down
7 changes: 3 additions & 4 deletions test/cbmc/proofs/HTTPClient_ReadHeader/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
7 changes: 3 additions & 4 deletions test/cbmc/proofs/HTTPClient_Send/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -67,7 +66,7 @@ UNWINDSET += strncmp.0:5

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Lines 58-61 should be reevaluated given these warnings: https://d39z7xfr4hj3jh.cloudfront.net/final/f6b58be4-d13f-4665-9be6-c5c08cfb8476/artifacts/HTTPClient_Send/report/html/index.html

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These are all present in the main branch: https://d39z7xfr4hj3jh.cloudfront.net/final/4b7c2384-c743-404b-8e74-9eb0ab5e3b0a/artifacts/HTTPClient_Send/report/html/index.html. They're not a result of these changes. I planned to follow up in the CBMC chat, but I don't think it should block this PR going into dev.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Followed up with CBMC and there's an open issue for this: model-checking/cbmc-starter-kit#88

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
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/Makefile-project-defines
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,17 +26,17 @@
*/
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The makefile for this case needs a loop unwindset updated: https://d39z7xfr4hj3jh.cloudfront.net/final/f6b58be4-d13f-4665-9be6-c5c08cfb8476/artifacts/findHeaderFieldParserCallback/report/html/index.html

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I tested removing that unwindset and the test fails, so it is doing something despite what the warning indicates. I'll ask in the cbmc group.


#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;
Expand Down
6 changes: 3 additions & 3 deletions ...mc/proofs/findHeaderOnHeaderCompleteCallback/findHeaderOnHeaderCompleteCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 );

Expand Down
6 changes: 3 additions & 3 deletions test/cbmc/proofs/findHeaderValueParserCallback/findHeaderValueParserCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
6 changes: 3 additions & 3 deletions test/cbmc/proofs/httpParserOnBodyCallback/httpParserOnBodyCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
6 changes: 3 additions & 3 deletions test/cbmc/proofs/httpParserOnHeaderFieldCallback/httpParserOnHeaderFieldCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
6 changes: 3 additions & 3 deletions test/cbmc/proofs/httpParserOnHeaderValueCallback/httpParserOnHeaderValueCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
6 changes: 3 additions & 3 deletions .../proofs/httpParserOnHeadersCompleteCallback/httpParserOnHeadersCompleteCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
6 changes: 3 additions & 3 deletions test/cbmc/proofs/httpParserOnMessageBeginCallback/httpParserOnMessageBeginCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 );

Expand Down
6 changes: 3 additions & 3 deletions .../proofs/httpParserOnMessageCompleteCallback/httpParserOnMessageCompleteCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 );

Expand Down
6 changes: 3 additions & 3 deletions test/cbmc/proofs/httpParserOnStatusCallback/httpParserOnStatusCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
8 changes: 4 additions & 4 deletions test/cbmc/sources/http_cbmc_state.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 );
}

Expand Down Expand Up @@ -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 );
}

Expand Down
27 changes: 12 additions & 15 deletions ...TPClient_ReadHeader_http_parser_execute.c → ...bs/HTTPClient_ReadHeader_llhttp_execute.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
*/

Expand All @@ -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 );
Expand Down Expand Up @@ -87,5 +84,5 @@ size_t http_parser_execute( http_parser * parser,
pParsingContext->pValueLoc = &pValue;
}

return pParsingContext->fieldFound ? valueLength : 0;
return parser->error;
}
Loading