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

aggarg · web-flow · commit 9ebaeb55cce3 · 2024-07-20T17:20:45.000+05:30
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 <aggarg@amazon.com>
diff --git a/docs/doxygen/include/size_table.md b/docs/doxygen/include/size_table.md
@@ -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>
diff --git a/loop_invariants.patch b/loop_invariants.patch
@@ -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 (
@@ -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-- )
@@ -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++ )
@@ -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(
@@ -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(
@@ -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 ] ) )
@@ -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(
@@ -199,4 +191,4 @@ index 901b2e1..8bdd89c 100644
 +    decreases( queryLength - i )
      {
          bool found = false;
- 
+
diff --git a/source/core_json.c b/source/core_json.c
@@ -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.
@@ -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;
 
@@ -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;
diff --git a/test/unit-test/core_json_utest.c b/test/unit-test/core_json_utest.c
@@ -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 )
@@ -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 );
