Skip to content

Commit

Permalink
Treat empty JSON object in key-value pair as valid (#169)
Browse files Browse the repository at this point in the history 
Treat empty JSON object in key-value pair as valid

Without this change, the following valid JSON document will be evaluated
as invalid:
```
{
    "foo": {}
}
```

This issue was reported here - #168

Signed-off-by: Gaurav Aggarwal <[email protected]>
  • Loading branch information
@aggarg
aggarg authored Jul 20, 2024
1 parent 2bb6294 commit 9ebaeb5
Show file tree
Hide file tree
Showing 4 changed files with 75 additions and 55 deletions.
4 changes: 2 additions & 2 deletions docs/doxygen/include/size_table.md
View file
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
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
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
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

0 comments on commit 9ebaeb5

Please sign in to comment.