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

Jump to bottom

Treat empty JSON object in key-value pair as valid #169

Merged
merged 6 commits into from
Jul 20, 2024
Merged

Treat empty JSON object in key-value pair as valid #169

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
170d87c
Treat empty JSON object as valid
aggarg Jul 18, 2024
37a4ca8
Fix formatting
aggarg Jul 18, 2024
d0130a2
Fix CBMC proof failure
aggarg Jul 18, 2024
bfb794c
Update code as per review feedback
aggarg Jul 19, 2024
25423f0
Fix memory statistics
aggarg Jul 19, 2024
4cc9032
Fix CBMC Proofs
aggarg Jul 19, 2024
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
4 changes: 2 additions & 2 deletions docs/doxygen/include/size_table.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,12 @@
</tr>
<tr>
<td>core_json.c</td>
<td><center>3.1K</center></td>
<td><center>3.0K</center></td>
<td><center>2.5K</center></td>
</tr>
<tr>
<td><b>Total estimates</b></td>
<td><b><center>3.1K</center></b></td>
<td><b><center>3.0K</center></b></td>
<td><b><center>2.5K</center></b></td>
</tr>
</table>
86 changes: 39 additions & 47 deletions loop_invariants.patch
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,42 +1,42 @@
diff --git a/source/core_json.c b/source/core_json.c
index 901b2e1..8bdd89c 100644
index d8694f0..761c44b 100644
--- a/source/core_json.c
+++ b/source/core_json.c
@@ -62,6 +62,21 @@ typedef union
#define isSquareOpen_( x ) ( ( x ) == '[' )
#define isSquareClose_( x ) ( ( x ) == ']' )
@@ -63,6 +63,21 @@ typedef union
#define isCurlyOpen_( x ) ( ( x ) == '{' )
#define isCurlyClose_( x ) ( ( x ) == '}' )

+/**
+ * Renaming all loop-contract clauses from CBMC for readability.
+ * For more information about loop contracts in CBMC, see
+ * https://diffblue.github.io/cbmc/contracts-user.html.
+ */
+#ifdef CBMC
+#define loopInvariant(...) __CPROVER_loop_invariant(__VA_ARGS__)
+#define decreases(...) __CPROVER_decreases(__VA_ARGS__)
+#define assigns(...) __CPROVER_assigns(__VA_ARGS__)
+ #define loopInvariant(...) __CPROVER_loop_invariant(__VA_ARGS__)
+ #define decreases(...) __CPROVER_decreases(__VA_ARGS__)
+ #define assigns(...) __CPROVER_assigns(__VA_ARGS__)
+#else
+#define loopInvariant(...)
+#define decreases(...)
+#define assigns(...)
+ #define loopInvariant(...)
+ #define decreases(...)
+ #define assigns(...)
+#endif
+
/**
* @brief Advance buffer index beyond whitespace.
*
@@ -78,6 +93,9 @@ static void skipSpace( const char * buf,
@@ -79,6 +94,9 @@ static void skipSpace( const char * buf,
coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );

for( i = *start; i < max; i++ )
+ assigns( i )
+ loopInvariant( *start <= i && i <= max )
+ decreases( max - i )
{
if( !isspace_( buf[ i ] ) )
{
@@ -102,6 +120,13 @@ static size_t countHighBits( uint8_t c )
@@ -103,6 +121,13 @@ static size_t countHighBits( uint8_t c )
size_t i = 0;

while( ( n & 0x80U ) != 0U )
+ assigns( i, n )
+ loopInvariant (
Expand All @@ -48,7 +48,7 @@ index 901b2e1..8bdd89c 100644
{
i++;
n = ( n & 0x7FU ) << 1U;
@@ -210,6 +235,13 @@ static bool skipUTF8MultiByte( const char * buf,
@@ -211,6 +236,13 @@ static bool skipUTF8MultiByte( const char * buf,
/* The bit count is 1 greater than the number of bytes,
* e.g., when j is 2, we skip one more byte. */
for( j = bitCount - 1U; j > 0U; j-- )
Expand All @@ -61,8 +61,8 @@ index 901b2e1..8bdd89c 100644
+ decreases( j )
{
i++;
@@ -345,6 +377,12 @@ static bool skipOneHexEscape( const char * buf,

@@ -346,6 +378,12 @@ static bool skipOneHexEscape( const char * buf,
if( ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) )
{
for( i += 2U; i < end; i++ )
Expand All @@ -74,58 +74,50 @@ index 901b2e1..8bdd89c 100644
+ decreases( end - i )
{
uint8_t n = hexToInt( buf[ i ] );
@@ -522,6 +560,9 @@ static bool skipString( const char * buf,

@@ -523,6 +561,9 @@ static bool skipString( const char * buf,
i++;

while( i < max )
+ assigns( i )
+ loopInvariant( *start + 1U <= i && i <= max )
+ decreases( max - i )
{
if( buf[ i ] == '"' )
{
@@ -580,6 +621,9 @@ static bool strnEq( const char * a,
@@ -581,6 +622,9 @@ static bool strnEq( const char * a,
coreJSON_ASSERT( ( a != NULL ) && ( b != NULL ) );

for( i = 0; i < n; i++ )
+ assigns( i )
+ loopInvariant( i <= n )
+ decreases( n - i )
{
if( a[ i ] != b[ i ] )
{
@@ -681,6 +725,7 @@ static bool skipAnyLiteral( const char * buf,
* false otherwise.
*/
#define MAX_FACTOR ( MAX_INDEX_VALUE / 10 )
+
static bool skipDigits( const char * buf,
size_t * start,
size_t max,
@@ -695,6 +740,9 @@ static bool skipDigits( const char * buf,
@@ -696,6 +740,9 @@ static bool skipDigits( const char * buf,
saveStart = *start;

for( i = *start; i < max; i++ )
+ assigns( value, i )
+ loopInvariant( *start <= i && i <= max )
+ decreases( max - i )
{
if( !isdigit_( buf[ i ] ) )
{
@@ -944,6 +992,9 @@ static void skipArrayScalars( const char * buf,
@@ -945,6 +992,9 @@ static void skipArrayScalars( const char * buf,
i = *start;

while( i < max )
+ assigns( i )
+ loopInvariant( *start <= i && i <= max )
+ decreases( max - i )
{
if( skipAnyScalar( buf, &i, max ) != true )
{
@@ -986,6 +1037,13 @@ static bool skipObjectScalars( const char * buf,
@@ -991,6 +1041,13 @@ static bool skipObjectScalars( const char * buf,
i = *start;

while( i < max )
+ assigns( i, *start, comma )
+ loopInvariant(
Expand All @@ -137,9 +129,9 @@ index 901b2e1..8bdd89c 100644
{
if( skipString( buf, &i, max ) != true )
{
@@ -1082,6 +1140,14 @@ static JSONStatus_t skipCollection( const char * buf,
@@ -1118,6 +1175,14 @@ static JSONStatus_t skipCollection( const char * buf,
i = *start;

while( i < max )
+ assigns( i, depth, c, __CPROVER_object_whole( stack ), ret )
+ loopInvariant(
Expand All @@ -152,27 +144,27 @@ index 901b2e1..8bdd89c 100644
{
c = buf[ i ];
i++;
@@ -1363,6 +1429,9 @@ static bool objectSearch( const char * buf,
@@ -1407,6 +1472,9 @@ static bool objectSearch( const char * buf,
skipSpace( buf, &i, max );

while( i < max )
+ assigns( i, key, keyLength, value, valueLength )
+ loopInvariant( __CPROVER_loop_entry( i ) <= i && i <= max )
+ decreases( max - i )
{
if( nextKeyValuePair( buf, &i, max, &key, &keyLength,
&value, &valueLength ) != true )
@@ -1430,6 +1499,9 @@ static bool arraySearch( const char * buf,
@@ -1474,6 +1542,9 @@ static bool arraySearch( const char * buf,
skipSpace( buf, &i, max );

while( i < max )
+ assigns( i, currentIndex, value, valueLength )
+ loopInvariant( __CPROVER_loop_entry( i ) <= i && i <= max && currentIndex < i )
+ decreases( max - i )
{
if( nextValue( buf, &i, max, &value, &valueLength ) != true )
{
@@ -1495,6 +1567,9 @@ static bool skipQueryPart( const char * buf,
@@ -1539,6 +1610,9 @@ static bool skipQueryPart( const char * buf,
while( ( i < max ) &&
!isSeparator_( buf[ i ] ) &&
!isSquareOpen_( buf[ i ] ) )
Expand All @@ -182,9 +174,9 @@ index 901b2e1..8bdd89c 100644
{
i++;
}
@@ -1541,6 +1616,17 @@ static JSONStatus_t multiSearch( const char * buf,
@@ -1585,6 +1659,17 @@ static JSONStatus_t multiSearch( const char * buf,
coreJSON_ASSERT( ( max > 0U ) && ( queryLength > 0U ) );

while( i < queryLength )
+ assigns( i, start, queryStart, value, length )
+ loopInvariant(
Expand All @@ -199,4 +191,4 @@ index 901b2e1..8bdd89c 100644
+ decreases( queryLength - i )
{
bool found = false;

26 changes: 20 additions & 6 deletions source/core_json.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,8 @@ typedef union
#define isMatchingBracket_( x, y ) ( isCurlyPair_( x, y ) || isSquarePair_( x, y ) )
#define isSquareOpen_( x ) ( ( x ) == '[' )
#define isSquareClose_( x ) ( ( x ) == ']' )
#define isCurlyOpen_( x ) ( ( x ) == '{' )
#define isCurlyClose_( x ) ( ( x ) == '}' )

/**
* @brief Advance buffer index beyond whitespace.
Expand Down Expand Up @@ -1047,6 +1049,7 @@ static bool skipScalars( const char * buf,
size_t max,
char mode )
{
size_t i = 0U;
bool modeIsOpenBracket = ( bool ) isOpenBracket_( mode );
bool ret = true;

Expand All @@ -1060,13 +1063,24 @@ static bool skipScalars( const char * buf,

skipSpace( buf, start, max );

if( mode == '[' )
{
skipArrayScalars( buf, start, max );
}
else
i = *start;

if( i < max )
{
ret = skipObjectScalars( buf, start, max );
if( mode == '[' )
{
if( !isSquareClose_( buf[ i ] ) )
{
skipArrayScalars( buf, start, max );
}
}
else
{
if( !isCurlyClose_( buf[ i ] ) )
{
ret = skipObjectScalars( buf, start, max );
}
}
}

return ret;
Expand Down
14 changes: 14 additions & 0 deletions test/unit-test/core_json_utest.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -146,6 +146,12 @@
"\":{\"" SECOND_QUERY_KEY "\" : \"" COMPLETE_QUERY_KEY_ANSWER "\"}} "
#define JSON_DOC_LEGAL_TRAILING_SPACE_LENGTH ( sizeof( JSON_DOC_LEGAL_TRAILING_SPACE ) - 1 )

#define JSON_DOC_LEGAL_EMPTY_OBJECT "{\"foo\":{}}"
#define JSON_DOC_LEGAL_EMPTY_OBJECT_LENGTH ( sizeof( JSON_DOC_LEGAL_EMPTY_OBJECT ) - 1 )

#define JSON_DOC_LEGAL_EMPTY_ARRAY "{\"foo\":[]}"
#define JSON_DOC_LEGAL_EMPTY_ARRAY_LENGTH ( sizeof( JSON_DOC_LEGAL_EMPTY_ARRAY ) - 1 )

/* A single scalar is still considered a valid JSON document. */
#define SINGLE_SCALAR "\"l33t\""
#define SINGLE_SCALAR_LENGTH ( sizeof( SINGLE_SCALAR ) - 1 )
Expand Down Expand Up @@ -564,6 +570,14 @@ void test_JSON_Validate_Legal_Documents( void )
JSON_DOC_LEGAL_TRAILING_SPACE_LENGTH );
TEST_ASSERT_EQUAL( JSONSuccess, jsonStatus );

jsonStatus = JSON_Validate( JSON_DOC_LEGAL_EMPTY_OBJECT,
JSON_DOC_LEGAL_EMPTY_OBJECT_LENGTH );
TEST_ASSERT_EQUAL( JSONSuccess, jsonStatus );

jsonStatus = JSON_Validate( JSON_DOC_LEGAL_EMPTY_ARRAY,
JSON_DOC_LEGAL_EMPTY_ARRAY_LENGTH );
TEST_ASSERT_EQUAL( JSONSuccess, jsonStatus );

jsonStatus = JSON_Validate( JSON_DOC_MULTIPLE_VALID_ESCAPES,
JSON_DOC_MULTIPLE_VALID_ESCAPES_LENGTH );
TEST_ASSERT_EQUAL( JSONSuccess, jsonStatus );
Expand Down
Loading